algebraic identities of plus and times discharge symbolically

1 files changed, 49 insertions, 2 deletions

diff --git a/lib/vm.ml b/lib/vm.ml
index 8a09f3f..4a11c4d 100644
--- a/lib/vm.ml
+++ b/lib/vm.ml
@@ -110,6 +110,7 @@ module Make (W : World.WORLD) = struct
     let value_l = forced_label "value"
     let left_l = forced_label "left"
     let right_l = forced_label "right"
+    let result_l = forced_label "result"
 
     type bound = { value : Q.t; strict : bool }
 
@@ -249,11 +250,20 @@ module Make (W : World.WORLD) = struct
       is_int : bool;  (** members are integers *)
       is_str : bool;
       has_domain : bool;  (** some domain goal declared the kind *)
+      needs_num : bool;  (** the body demands a numeric member *)
       lower : Propagate.bound option;
       upper : Propagate.bound option;
     }
 
-    let free = { is_int = false; is_str = false; has_domain = false; lower = None; upper = None }
+    let free =
+      {
+        is_int = false;
+        is_str = false;
+        has_domain = false;
+        needs_num = false;
+        lower = None;
+        upper = None;
+      }
 
     (* One goal read as a constraint on [var]; None = outside the
        fragment. Goals without variables evaluate outright. *)
@@ -334,6 +344,42 @@ module Make (W : World.WORLD) = struct
                 (with_bound (not less)
                    { Propagate.value = Option.get (Propagate.numeric_value g); strict })
           | _ -> None)
+      | ("Plus" | "Times"), _, Some l, Some r -> (
+          (* The algebraic identities of the numeric relations:
+             membership statements that hold for every numeric
+             member, so a numeric quantifier discharges them and a
+             string quantifier refutes them. Anything beyond the
+             identities stays outside the fragment. *)
+          let result = Label.Map.find_opt Propagate.result_l bindings in
+          let is_zero = function
+            | Pattern.Integer z -> Z.equal z Z.zero
+            | _ -> false
+          and is_one = function
+            | Pattern.Integer z -> Z.equal z Z.one
+            | _ -> false
+          in
+          let identity =
+            match (name, l, r, result) with
+            | "Plus", v, unit_, Some v' when is_var v && is_zero unit_ && is_var v' ->
+                true
+            | "Plus", unit_, v, Some v' when is_var v && is_zero unit_ && is_var v' ->
+                true
+            | "Times", v, unit_, Some v' when is_var v && is_one unit_ && is_var v' ->
+                true
+            | "Times", unit_, v, Some v' when is_var v && is_one unit_ && is_var v' ->
+                true
+            | "Times", v, zero, Some zero' when is_var v && is_zero zero && is_zero zero'
+              ->
+                true
+            | "Times", zero, v, Some zero' when is_var v && is_zero zero && is_zero zero'
+              ->
+                true
+            | _ -> false
+          in
+          if identity then Some (`Side { side with needs_num = true })
+          else if Label.Map.for_all (fun _ p -> Pattern.vars p = []) bindings then
+            ground_goal ()
+          else None)
       | _, _, _, _ ->
           if
             Label.Map.for_all
@@ -396,7 +442,8 @@ module Make (W : World.WORLD) = struct
 
     let entails q b =
       if q.is_str then
-        if b.is_int || b.lower <> None || b.upper <> None then `Fails
+        if b.is_int || b.needs_num || b.lower <> None || b.upper <> None then
+          `Fails
         else `Holds
       else if b.is_str then `Fails
       else if b.is_int && (not q.is_int) && not (single_integer_point q) then