symbolic discharge: universals over infinite domains decided by intervals

1 files changed, 233 insertions, 6 deletions

diff --git a/lib/vm.ml b/lib/vm.ml
index a518aa5..8a09f3f 100644
--- a/lib/vm.ml
+++ b/lib/vm.ml
@@ -236,6 +236,217 @@ module Make (W : World.WORLD) = struct
         | None -> Unknown
   end
 
+  (* Symbolic discharge (decision 10, rung three, first fragment):
+     universals whose quantifier is an infinite domain are decided
+     algebraically when quantifier and body both read as kind and
+     interval constraints over the one quantified variable. Holds
+     means every member is covered; Fails is always backed by a
+     concrete counterexample; anything outside the fragment stays
+     deferred. Subtype inclusions (a Natural is an Integer is a
+     Rational) are decided here, literally, per decision 12. *)
+  module Symbolic = struct
+    type side = {
+      is_int : bool;  (** members are integers *)
+      is_str : bool;
+      has_domain : bool;  (** some domain goal declared the kind *)
+      lower : Propagate.bound option;
+      upper : Propagate.bound option;
+    }
+
+    let free = { is_int = false; is_str = false; has_domain = false; lower = None; upper = None }
+
+    (* One goal read as a constraint on [var]; None = outside the
+       fragment. Goals without variables evaluate outright. *)
+    let read subst var side (name, bindings) =
+      let value = Label.Map.find_opt Propagate.value_l bindings
+      and left = Label.Map.find_opt Propagate.left_l bindings
+      and right = Label.Map.find_opt Propagate.right_l bindings in
+      let ground_goal () =
+        match Builtin.run subst name bindings with
+        | Some (Builtin.Solved []) -> Some `Contradiction
+        | Some (Builtin.Solved _) -> Some `Trivial
+        | _ -> None
+      in
+      let is_var = function
+        | Pattern.Var v -> String.equal v var
+        | _ -> false
+      in
+      match (name, value, left, right) with
+      | ("Integer" | "Natural"), Some v, _, _ when is_var v ->
+          let side = { side with is_int = true; has_domain = true } in
+          if String.equal name "Natural" then
+            Some
+              (`Side
+                {
+                  side with
+                  lower =
+                    Some
+                      (match side.lower with
+                      | None -> { Propagate.value = Q.zero; strict = false }
+                      | Some b ->
+                          Propagate.stronger_lower b
+                            { Propagate.value = Q.zero; strict = false });
+                })
+          else Some (`Side side)
+      | "Rational", Some v, _, _ when is_var v ->
+          Some (`Side { side with has_domain = true })
+      | "String", Some v, _, _ when is_var v ->
+          Some (`Side { side with is_str = true; has_domain = true })
+      | ( ("LessThan" | "LessThanEqual" | "GreaterThan" | "GreaterEqual"),
+          _,
+          Some l,
+          Some r ) -> (
+          let strict =
+            String.equal name "LessThan" || String.equal name "GreaterThan"
+          in
+          let less =
+            String.equal name "LessThan" || String.equal name "LessThanEqual"
+          in
+          let with_bound upper bound =
+            if upper then
+              `Side
+                {
+                  side with
+                  upper =
+                    Some
+                      (match side.upper with
+                      | None -> bound
+                      | Some b -> Propagate.stronger_upper b bound);
+                }
+            else
+              `Side
+                {
+                  side with
+                  lower =
+                    Some
+                      (match side.lower with
+                      | None -> bound
+                      | Some b -> Propagate.stronger_lower b bound);
+                }
+          in
+          match (l, r) with
+          | v, g when is_var v && Option.is_some (Propagate.numeric_value g) ->
+              Some
+                (with_bound less
+                   { Propagate.value = Option.get (Propagate.numeric_value g); strict })
+          | g, v when is_var v && Option.is_some (Propagate.numeric_value g) ->
+              Some
+                (with_bound (not less)
+                   { Propagate.value = Option.get (Propagate.numeric_value g); strict })
+          | _ -> None)
+      | _, _, _, _ ->
+          if
+            Label.Map.for_all
+              (fun _ p -> Pattern.vars p = [])
+              bindings
+          then ground_goal ()
+          else None
+
+    let read_side subst var goals =
+      List.fold_left
+        (fun acc goal ->
+          match acc with
+          | None | Some `Contradiction -> acc
+          | Some (`Side side) -> (
+              match read subst var side goal with
+              | Some (`Side _ as s) -> Some s
+              | Some `Trivial -> Some (`Side side)
+              | Some `Contradiction -> Some `Contradiction
+              | None -> None))
+        (Some (`Side free)) goals
+
+    (* Does the quantifier's lower bound guarantee the body's? For
+       integer kinds compare tightened endpoints; missing body bound
+       is no demand, missing quantifier bound cannot guarantee one. *)
+    let lower_entails ~int q b =
+      match b with
+      | None -> true
+      | Some b -> (
+          match q with
+          | None -> false
+          | Some q ->
+              if int then Z.geq (Propagate.lower_int q) (Propagate.lower_int b)
+              else
+                Q.gt q.Propagate.value b.Propagate.value
+                || (Q.equal q.Propagate.value b.Propagate.value
+                   && ((not b.strict) || q.strict)))
+
+    let upper_entails ~int q b =
+      match b with
+      | None -> true
+      | Some b -> (
+          match q with
+          | None -> false
+          | Some q ->
+              if int then Z.leq (Propagate.upper_int q) (Propagate.upper_int b)
+              else
+                Q.lt q.Propagate.value b.Propagate.value
+                || (Q.equal q.Propagate.value b.Propagate.value
+                   && ((not b.strict) || q.strict)))
+
+    (* A rational interval that is one integer point. *)
+    let single_integer_point q =
+      match (q.lower, q.upper) with
+      | Some lo, Some hi ->
+          (not lo.Propagate.strict)
+          && (not hi.Propagate.strict)
+          && Q.equal lo.value hi.value
+          && Z.equal (Q.den lo.value) Z.one
+      | _ -> false
+
+    let entails q b =
+      if q.is_str then
+        if b.is_int || 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
+        `Fails
+      else if
+        lower_entails ~int:q.is_int q.lower b.lower
+        && upper_entails ~int:q.is_int q.upper b.upper
+      then `Holds
+      else `Fails
+
+    let discharge subst quantifier_goals body_goals =
+      let apply_only goals =
+        List.fold_left
+          (fun acc goal ->
+            Option.bind acc (fun goals ->
+                match goal with
+                | World.Apply (name, bindings) ->
+                    Some
+                      ((name, Label.Map.map (Pattern.Subst.resolve subst) bindings)
+                      :: goals)
+                | _ -> None))
+          (Some []) goals
+      in
+      match (apply_only quantifier_goals, apply_only body_goals) with
+      | Some quantifier, Some body -> (
+          let vars =
+            List.concat_map
+              (fun (_, bindings) ->
+                Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings [])
+              quantifier
+            |> List.sort_uniq String.compare
+          in
+          match vars with
+          | [ var ] -> (
+              match (read_side subst var quantifier, read_side subst var body) with
+              | Some (`Side q), Some (`Side b) ->
+                  if q.has_domain then entails q b else `Unknown
+              | Some (`Side q), Some `Contradiction ->
+                  (* The body is falsified outright; any member of a
+                     nonempty quantifier is a counterexample. *)
+                  if q.has_domain then `Fails else `Unknown
+              | Some `Contradiction, _ ->
+                  (* An empty quantifier satisfies any universal. *)
+                  `Holds
+              | _ -> `Unknown)
+          | _ -> `Unknown)
+      | _ -> `Unknown
+  end
+
+
   let rec try_goal world subst goal =
     match goal with
     | Negated denial ->
@@ -252,15 +463,31 @@ module Make (W : World.WORLD) = struct
         Run [ (subst, flatten a); (subst, flatten b) ]
     | Positive ((World.And _ | World.Not _) as expr) -> Run [ (subst, flatten expr) ]
     | Positive (World.Forall (quantifier, body)) -> (
-        (* Universal over the quantifier's solutions. Runs only when
-           the quantifier is decidable and closed; an undetermined
-           quantifier or body defers the universal, and an infinite
-           one therefore never runs. *)
+        (* Universal over the quantifier's solutions. Runs when the
+           quantifier is decidable and closed; otherwise symbolic
+           discharge gets a chance before the universal defers, so
+           truths over infinite domains are proven, never
+           enumerated. *)
+        let rec conjuncts = function
+          | World.And (a, b) -> conjuncts a @ conjuncts b
+          | expr -> [ expr ]
+        in
+        let symbolically () =
+          match
+            Symbolic.discharge subst (conjuncts quantifier) (conjuncts body)
+          with
+          | `Holds -> Run [ (subst, []) ]
+          | `Fails -> Run []
+          | `Unknown -> Wait { residuatable = false }
+        in
         match search world subst (flatten quantifier) with
-        | exception Stuck _ -> Wait { residuatable = false }
+        | exception Stuck _ -> symbolically ()
         | quantified ->
             if List.exists (fun (_, residue) -> residue <> []) quantified then
-              Wait { residuatable = false }
+              (* The quantifier residuated: an infinite or
+                 underdetermined domain. Enumeration is off the
+                 table; proof is not. *)
+              symbolically ()
             else
               let body_status (s, _) =
                 match search world s (flatten body) with