Merge pull request #1330 from mathics/ConditionalExpression-basic

basic implementation of ConditionalExpression, Assuming and

Author: rocky

CHANGES.rst

@@ -10,6 +10,7 @@ New builtins
 
 * ``Arg``
 * ``Dispatch``
+* ``FullSimplify``
 * ``LetterNumber`` #1298. The ``alphabet`` parameter supports only a minimal number of languages.
 * ``Nand`` and ``Nor`` logical functions.
 * ``Series``,  ``O`` and ``SeriesData``
@@ -21,19 +22,23 @@ New builtins
 Enhancements
 ++++++++++++
 
+* a function `evaluate_predicate` allows for a basic predicate evaluation using `$Assumptions`.
 * ``Attributes`` accepts a string parameter.
 * ``ColorNegate`` for colors is supported.
 * ``D`` and ``Derivative`` improvements.
 * ``FileNames`` returns a sorted list (#1250).
 * ``FindRoot`` now receives several optional parameters like ``Method`` and ``MaxIterations``.
-* ``FixedPoint`` now supports the ``SameTest`` option.
+* ``FixedPoint`` now supports the ``SameTest`` option.  
 * ``Prime`` and ``PrimePi`` now accept a list parameter and have the ``NumericFunction`` attribute.
 * ``ReplaceRepeated`` and ``FixedPoint`` now supports the ``MaxIteration`` option (#1260).
+* ``Simplify`` performs a more sophisticated set of simplifications.
+* ``Simplify`` accepts a second parameter that temporarily overwrites ``$Assumptions``.
 * ``StringTake`` now accepts form containing a list of strings and specification (#1297).
 * ``Table`` [*expr*, *n*] is supported.
 * ``ToString`` accepts an optional *form* parameter.
 * ``ToExpression`` handles multi-line string input
 * The implementation of Streams was redone.
+  
 
 
 Bug fixes

mathics/builtin/algebra.py

@@ -3,6 +3,7 @@
 Algebraic Manipulation
 """
 
+
 from mathics.version import __version__  # noqa used in loading to check consistency.
 
 from mathics.builtin.base import Builtin
@@ -15,10 +16,13 @@
     Number,
     Symbol,
     SymbolFalse,
+    SymbolList,
     SymbolNull,
     SymbolTrue,
 )
 from mathics.core.convert import from_sympy, sympy_symbol_prefix
+from mathics.builtin.scoping import dynamic_scoping
+from mathics.builtin.inference import evaluate_predicate
 
 import sympy
 
@@ -288,6 +292,8 @@ class Simplify(Builtin):
     <dl>
     <dt>'Simplify[$expr$]'
         <dd>simplifies $expr$.
+    <dt>'Simplify[$expr$, $assump$]'
+        <dd>simplifies $expr$ assuming $assump$ instead of $Assumptions$.
     </dl>
 
     >> Simplify[2*Sin[x]^2 + 2*Cos[x]^2]
@@ -297,6 +303,16 @@ class Simplify(Builtin):
     >> Simplify[f[x]]
      = f[x]
 
+    Simplify over conditional expressions uses $Assumptions, or $assump$
+    to evaluate the condition:
+    # TODO: enable this once the logic for conditional expression
+    # be restaured.
+    # >> $Assumptions={a <= 0};
+    # >> Simplify[ConditionalExpression[1, a > 0]]
+    # = Undefined
+    # >> Simplify[ConditionalExpression[1, a > 0], { a > 0 }]
+    # = 1
+
     #> Simplify[a*x^2+b*x^2]
      = x ^ 2 (a + b)
 
@@ -308,11 +324,31 @@ class Simplify(Builtin):
     rules = {
         "Simplify[list_List]": "Simplify /@ list",
         "Simplify[rule_Rule]": "Simplify /@ rule",
-        "Simplify[eq_Equal]": "Simplify /@ eq",
+        "Simplify[list_List, assum_]": "Simplify[#1, assum]& /@ list",
+        "Simplify[rule_Rule, assum_]": "Simplify[#1, assum]& /@ rule",
+        "Simplify[0^a_, assum_]": "ConditionalExpression[0,Simplify[a>0]]",
+        "Simplify[b_^a_, assum_]": "ConditionalExpression[b,Simplify[{Or[a>0, b!=0]}]]",
     }
 
+    def apply_assuming(self, expr, assumptions, evaluation):
+        "%(name)s[expr_, assumptions_]"
+        assumptions = assumptions.evaluate(evaluation)
+        return dynamic_scoping(
+            lambda ev: self.apply(expr, ev),
+            {"System`$Assumptions": assumptions},
+            evaluation,
+        )
+
     def apply(self, expr, evaluation):
-        "Simplify[expr_]"
+        "%(name)s[expr_]"
+        # Check first if we are dealing with a logic expression...
+        expr = evaluate_predicate(expr, evaluation)
+        if expr.is_atom():
+            return expr
+        # else, use sympy:
+        leaves = [self.apply(leaf, evaluation) for leaf in expr._leaves]
+        head = self.apply(expr.get_head(), evaluation)
+        expr = Expression(head, *leaves)
 
         sympy_expr = expr.to_sympy()
         if sympy_expr is None:
@@ -321,6 +357,31 @@ def apply(self, expr, evaluation):
         return from_sympy(sympy_result)
 
 
+class FullSimplify(Simplify):
+    """
+    <dl>
+    <dt>'FullSimplify[$expr$]'
+        <dd>simplifies $expr$ using an extended set of simplification rules.
+    <dt>'FullSimplify[$expr$, $assump$]'
+        <dd>simplifies $expr$ assuming $assump$ instead of $Assumptions$.
+    </dl>
+    TODO: implement the extension. By now, this does the same than Simplify...
+
+    >> FullSimplify[2*Sin[x]^2 + 2*Cos[x]^2]
+     = 2
+
+    """
+
+    rules = {
+        "FullSimplify[list_List]": "FullSimplify /@ list",
+        "FullSimplify[rule_Rule]": "FullSimplify /@ rule",
+        "FullSimplify[eq_Equal]": "FullSimplify /@ eq",
+        "FullSimplify[list_List, assum_]": "FullSimplify[#1, assum]& /@ list",
+        "FullSimplify[rule_Rule, assum_]": "FullSimplify[#1, assum]& /@ rule",
+        "FullSimplify[eq_Equal, assum_]": "FullSimplify[#1, assum]& /@ eq",
+    }
+
+
 class Together(Builtin):
     """
     <dl>
@@ -1264,7 +1325,7 @@ def apply(self, expr, form, evaluation):
         if expr == Integer0:
             return Expression("List")
         elif e_null and f_null:
-            return Expression("List", Integer0)
+            return Expression(SymbolList, Integer0)
         elif e_null and not f_null:
             return Expression("List", SymbolNull)
         elif f_null:

mathics/builtin/arithmetic.py

@@ -42,13 +42,16 @@
     SymbolFalse,
     SymbolUndefined,
     SymbolSequence,
+    SymbolList,
     from_mpmath,
     from_python,
 )
 from mathics.core.numbers import min_prec, dps, SpecialValueError
 
 from mathics.builtin.lists import _IterationFunction
-from mathics.core.convert import from_sympy, SympyExpression
+from mathics.core.convert import from_sympy, SympyExpression, sympy_symbol_prefix
+from mathics.builtin.scoping import dynamic_scoping
+from mathics.builtin.inference import get_assumptions_list, evaluate_predicate
 
 
 @lru_cache(maxsize=1024)
@@ -741,7 +744,7 @@ def apply(self, items, evaluation):
         elif number.sameQ(Integer(-1)) and leaves and leaves[0].has_form("Plus", None):
             leaves[0] = Expression(
                 leaves[0].get_head(),
-                *[Expression("Times", Integer(-1), leaf) for leaf in leaves[0].leaves]
+                *[Expression("Times", Integer(-1), leaf) for leaf in leaves[0].leaves],
             )
             number = None
 
@@ -2222,7 +2225,7 @@ class Piecewise(SympyFunction):
     ## Piecewise({{0, Or[x < 0, x > 0]}}, Indeterminate).
 
     >> Integrate[Piecewise[{{1, x <= 0}, {-1, x > 0}}], x]
-     = Piecewise[{{x, x <= 0}, {-x, True}}]
+     = Piecewise[{{x, x <= 0}}, -x]
 
     >> Integrate[Piecewise[{{1, x <= 0}, {-1, x > 0}}], {x, -1, 2}]
      = -1
@@ -2244,15 +2247,18 @@ class Piecewise(SympyFunction):
 
     def apply(self, items, evaluation):
         "%(name)s[items__]"
-        result = self.to_sympy(Expression("Piecewise", *items.get_sequence()))
+        result = self.to_sympy(Expression("Piecewise", *items.get_sequence()),
+                               evaluation=evaluation
+        )
         if result is None:
             return
         if not isinstance(result, sympy.Piecewise):
-            return from_sympy(result)
+            result = from_sympy(result)
+            return result
 
     def to_sympy(self, expr, **kwargs):
         leaves = expr.leaves
-
+        evaluation = kwargs.get("evaluation", None)
         if len(leaves) not in (1, 2):
             return
 
@@ -2263,6 +2269,8 @@ def to_sympy(self, expr, **kwargs):
             if len(case.leaves) != 2:
                 return
             then, cond = case.leaves
+            if evaluation:
+                cond = evaluate_predicate(cond, evaluation)
 
             sympy_cond = None
             if isinstance(cond, Symbol):
@@ -2320,11 +2328,11 @@ def apply(self, expr, evaluation):
 
 class Assumptions(Predefined):
     """
-    <dl>
-    <dt>'$Assumptions'
-      <dd>is the default setting for the Assumptions option used in such
-   functions as Simplify, Refine, and Integrate.
-    </dl>
+     <dl>
+     <dt>'$Assumptions'
+       <dd>is the default setting for the Assumptions option used in such
+    functions as Simplify, Refine, and Integrate.
+     </dl>
     """
 
     name = "$Assumptions"
@@ -2338,84 +2346,113 @@ class Assuming(Builtin):
     """
     <dl>
     <dt>'Assuming[$cond$, $expr$]'
-      <dd>Evaluates $expr$ assuming the conditions $cond$
+      <dd>Evaluates $expr$ assuming the conditions $cond$.
     </dl>
     >> $Assumptions = { x > 0 }
      = {x > 0}
-    >> Assuming[y>0, $Assumptions]
-     = {x > 0, y > 0}
+    >> Assuming[y>0, ConditionalExpression[y x^2, y>0]//Simplify]
+     = x ^ 2 y
+    >> Assuming[Not[y>0], ConditionalExpression[y x^2, y>0]//Simplify]
+     = Undefined
+    >> ConditionalExpression[y x ^ 2, y > 0]//Simplify
+     = ConditionalExpression[x ^ 2 y, y > 0]
     """
 
     attributes = ("HoldRest",)
 
-    def apply_assuming(self, cond, expr, evaluation):
-        "Assuming[cond_, expr_]"
-        cond = cond.evaluate(evaluation)
-        if cond.is_true():
+    def apply_assuming(self, assumptions, expr, evaluation):
+        "Assuming[assumptions_, expr_]"
+        assumptions = assumptions.evaluate(evaluation)
+        if assumptions.is_true():
             cond = []
-        elif cond.is_symbol() or not cond.has_form("List", None):
-            cond = [cond]
+        elif assumptions.is_symbol() or not assumptions.has_form("List", None):
+            cond = [assumptions]
         else:
-            cond = cond.leaves
-        assumptions = evaluation.definitions.get_definition(
-            "System`$Assumptions", only_if_exists=True
+            cond = assumptions._leaves
+        cond = tuple(cond) + get_assumptions_list(evaluation)
+        list_cond = Expression("List", *cond)
+        # TODO: reduce the list of predicates
+        return dynamic_scoping(
+            lambda ev: expr.evaluate(ev), {"System`$Assumptions": list_cond}, evaluation
         )
 
-        if assumptions:
-            assumptions = assumptions.ownvalues
-            if len(assumptions) > 0:
-                assumptions = assumptions[0].replace
-            else:
-                assumptions = None
-        if assumptions:
-            if assumptions.is_symbol() or not assumptions.has_form("List", None):
-                assumptions = [assumptions]
-            else:
-                assumptions = assumptions.leaves
-            cond = assumptions + tuple(cond)
-        Expression(
-            "Set", Symbol("System`$Assumptions"), Expression("List", *cond)
-        ).evaluate(evaluation)
-        ret = expr.evaluate(evaluation)
-        if assumptions:
-            Expression(
-                "Set", Symbol("System`$Assumptions"), Expression("List", *assumptions)
-            ).evaluate(evaluation)
-        else:
-            Expression(
-                "Set", Symbol("System`$Assumptions"), Expression("List", SymbolTrue)
-            ).evaluate(evaluation)
-        return ret
-
 
 class ConditionalExpression(Builtin):
     """
     <dl>
-    <dt>'ConditionalExpression[$expr$, $cond$]'
-      <dd>returns $expr$ if $cond$ evaluates to $True$, $Undefined$ if
-          $cond$ evaluates to $False$.
+      <dt>'ConditionalExpression[$expr$, $cond$]'
+      <dd>returns $expr$ if $cond$ evaluates to $True$, $Undefined$ if $cond$ evaluates to $False$.
     </dl>
 
+    >> ConditionalExpression[x^2, True]
+     = x ^ 2
+
+     >> ConditionalExpression[x^2, False]
+     = Undefined
+
     >> f = ConditionalExpression[x^2, x>0]
      = ConditionalExpression[x ^ 2, x > 0]
     >> f /. x -> 2
      = 4
     >> f /. x -> -2
      = Undefined
+    'ConditionalExpression' uses assumptions to evaluate the condition:
+    >> $Assumptions = x > 0;
+    >> ConditionalExpression[x ^ 2, x>0]//Simplify
+     = x ^ 2
+    >> $Assumptions = True;
+    # >> ConditionalExpression[ConditionalExpression[s,x>a], x<b]
+    # = ConditionalExpression[s, And[x>a, x<b]]
     """
 
+    sympy_name = "Piecewise"
+
     rules = {
         "ConditionalExpression[expr_, True]": "expr",
         "ConditionalExpression[expr_, False]": "Undefined",
+        "ConditionalExpression[ConditionalExpression[expr_, cond1_], cond2_]": "ConditionalExpression[expr, And@@Flatten[{cond1, cond2}]]",
+        "ConditionalExpression[expr1_, cond_] + expr2_": "ConditionalExpression[expr1+expr2, cond]",
+        "ConditionalExpression[expr1_, cond_]  expr2_": "ConditionalExpression[expr1 expr2, cond]",
+        "ConditionalExpression[expr1_, cond_]^expr2_": "ConditionalExpression[expr1^expr2, cond]",
+        "expr1_ ^ ConditionalExpression[expr2_, cond_]": "ConditionalExpression[expr1^expr2, cond]",
     }
 
     def apply_generic(self, expr, cond, evaluation):
         "ConditionalExpression[expr_, cond_]"
-        cond = cond.evaluate(evaluation)
+        # What we need here is a way to evaluate
+        # cond as a predicate, using assumptions.
+        # Let's delegate this to the And (and Or) symbols...
+        if not cond.is_atom() and cond._head == SymbolList:
+            cond = Expression("System`And", *(cond._leaves))
+        else:
+            cond = Expression("System`And", cond)
         if cond is None:
             return
         if cond.is_true():
             return expr
         if cond == SymbolFalse:
             return SymbolUndefined
         return
+
+    def to_sympy(self, expr, **kwargs):
+        leaves = expr.leaves
+        if len(leaves) != 2:
+            return
+        expr, cond = leaves
+
+        sympy_cond = None
+        if isinstance(cond, Symbol):
+            if cond == SymbolTrue:
+                sympy_cond = True
+            elif cond == SymbolFalse:
+                sympy_cond = False
+        if sympy_cond is None:
+            sympy_cond = cond.to_sympy(**kwargs)
+            if not (sympy_cond.is_Relational or sympy_cond.is_Boolean):
+                return
+
+        sympy_cases = (
+            (expr.to_sympy(**kwargs), sympy_cond),
+            (sympy.Symbol(sympy_symbol_prefix + "System`Undefined"), True),
+        )
+        return sympy.Piecewise(*sympy_cases)