negation, quantifiers and membership criteria as schema domains

1 files changed, 76 insertions, 30 deletions

diff --git a/lib/vm.ml b/lib/vm.ml
index bde087a..e65cd68 100644
--- a/lib/vm.ml
+++ b/lib/vm.ml
@@ -10,19 +10,34 @@ type solution = (string * Pattern.t) list
 module Make (W : World.WORLD) = struct
   exception Stuck of string list
 
+  (* A goal is a proposition to establish or a denial to refute.
+     Conjunction flattens; [u :not d] contributes the universe
+     positively and the denial negatively. *)
+  type goal = Positive of World.expr | Negated of World.expr
+
   let rec flatten = function
     | World.And (a, b) -> flatten a @ flatten b
-    | goal -> [ goal ]
+    | World.Not (universe, denial) -> flatten universe @ [ Negated denial ]
+    | expr -> [ Positive expr ]
 
   let rec expr_vars = function
     | World.Apply (_, bindings) ->
         Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings []
-    | World.And (a, b) | World.Or (a, b) -> expr_vars a @ expr_vars b
+    | World.And (a, b) | World.Or (a, b) | World.Not (a, b) | World.Forall (a, b)
+      ->
+        expr_vars a @ expr_vars b
 
   let goal_name = function
-    | World.Apply (name, _) -> name
-    | World.And _ -> ":and"
-    | World.Or _ -> ":or"
+    | Positive (World.Apply (name, _)) -> name
+    | Positive (World.Or _) -> ":or"
+    | Positive (World.And _) -> ":and"
+    | Positive (World.Not _) | Negated _ -> ":not"
+    | Positive (World.Forall _) -> "ForAll"
+
+  let unresolved_vars subst expr =
+    expr_vars expr
+    |> List.filter (fun v ->
+           not (Pattern.is_ground (Pattern.Subst.resolve subst (Pattern.Var v))))
 
   (* Rule variables are renamed apart at every unfolding. The suffix
      character cannot be lexed, so renamed variables are unforgeable
@@ -42,6 +57,8 @@ module Make (W : World.WORLD) = struct
             World.Apply (name, Label.Map.map rename bindings)
         | World.And (a, b) -> World.And (rename_expr a, rename_expr b)
         | World.Or (a, b) -> World.Or (rename_expr a, rename_expr b)
+        | World.Not (a, b) -> World.Not (rename_expr a, rename_expr b)
+        | World.Forall (a, b) -> World.Forall (rename_expr a, rename_expr b)
       in
       (Label.Map.map rename rule.World.head, rename_expr rule.World.body)
 
@@ -59,12 +76,30 @@ module Make (W : World.WORLD) = struct
 
   (* Executing one goal yields branches: an extended substitution
      and the extra goals it owes (rule bodies, disjuncts). [None]
-     means not decidable yet. *)
-  let try_goal world subst goal =
+     means not decidable yet; the planner retries it later, and
+     rejects the plan if nothing ever runs. *)
+  let rec try_goal world subst goal =
     match goal with
-    | World.Or (a, b) -> Some [ (subst, flatten a); (subst, flatten b) ]
-    | World.And _ -> Some [ (subst, flatten goal) ]
-    | World.Apply (name, bindings) -> (
+    | Negated denial ->
+        if unresolved_vars subst denial = [] then
+          match search world subst (flatten denial) with
+          | [] -> Some [ (subst, []) ]
+          | _ -> Some []
+        else None
+    | Positive (World.Or (a, b)) -> Some [ (subst, flatten a); (subst, flatten b) ]
+    | Positive (World.And _ | World.Not _) ->
+        Some [ (subst, flatten (match goal with Positive e -> e | _ -> assert false)) ]
+    | Positive (World.Forall (quantifier, body)) -> (
+        (* Universal over the quantifier's solutions. Decidable only
+           when the quantifier itself is; a stuck quantifier defers
+           the universal, and an infinite one therefore never runs. *)
+        match search world subst (flatten quantifier) with
+        | exception Stuck _ -> None
+        | quantified ->
+            let holds s = search world s (flatten body) <> [] in
+            if List.for_all holds quantified then Some [ (subst, []) ] else Some []
+        )
+    | Positive (World.Apply (name, bindings)) -> (
         match Builtin.run subst name bindings with
         | Some (Builtin.Solved substs) ->
             Some (List.map (fun s -> (s, [])) substs)
@@ -107,31 +142,42 @@ module Make (W : World.WORLD) = struct
                    rather than a crash. *)
                 None))
 
+  and search world subst goals =
+    match goals with
+    | [] -> [ subst ]
+    | _ -> (
+        let rec select scanned = function
+          | [] -> None
+          | goal :: rest -> (
+              match try_goal world subst goal with
+              | Some branches -> Some (branches, List.rev_append scanned rest)
+              | None -> select (goal :: scanned) rest)
+        in
+        match select [] goals with
+        | Some (branches, remaining) ->
+            List.concat_map
+              (fun (subst, extra) -> search world subst (extra @ remaining))
+              branches
+        | None -> raise (Stuck (List.map goal_name goals)))
+
+  (* Solution variables: the free variables of the query. Whatever
+     occurs only under a universal is bound per quantifier solution
+     and is nobody's answer. *)
+  let rec outer_vars = function
+    | World.Apply (_, bindings) ->
+        Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings []
+    | World.And (a, b) | World.Or (a, b) | World.Not (a, b) ->
+        outer_vars a @ outer_vars b
+    | World.Forall _ -> []
+
   let solve world expr =
-    let rec search subst goals =
-      match goals with
-      | [] -> [ subst ]
-      | _ -> (
-          let rec select scanned = function
-            | [] -> None
-            | goal :: rest -> (
-                match try_goal world subst goal with
-                | Some branches -> Some (branches, List.rev_append scanned rest)
-                | None -> select (goal :: scanned) rest)
-          in
-          match select [] goals with
-          | Some (branches, remaining) ->
-              List.concat_map
-                (fun (subst, extra) -> search subst (extra @ remaining))
-                branches
-          | None -> raise (Stuck (List.map goal_name goals)))
-    in
     let variables =
       List.fold_left
         (fun acc v -> if List.mem v acc then acc else acc @ [ v ])
-        [] (expr_vars expr)
+        [] (outer_vars expr)
+      |> List.filter (fun v -> not (String.contains v '@'))
     in
-    match search Pattern.Subst.empty (flatten expr) with
+    match search world Pattern.Subst.empty (flatten expr) with
     | exception Stuck goals -> Error (Non_total_plan goals)
     | substs ->
         let read subst =