working vm: parser, admission with totality checks, solver and repl

2 files changed, 193 insertions, 0 deletions

diff --git a/lib/vm.ml b/lib/vm.ml
new file mode 100644
index 0000000..bde087a
--- /dev/null
+++ b/lib/vm.ml
@@ -0,0 +1,156 @@
+type error = Non_total_plan of string list
+
+let pp_error fmt (Non_total_plan goals) =
+  Format.fprintf fmt
+    "non-total plan rejected: no decidable goal among %s (bind more arguments or bound the search)"
+    (String.concat ", " goals)
+
+type solution = (string * Pattern.t) list
+
+module Make (W : World.WORLD) = struct
+  exception Stuck of string list
+
+  let rec flatten = function
+    | World.And (a, b) -> flatten a @ flatten b
+    | goal -> [ goal ]
+
+  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
+
+  let goal_name = function
+    | World.Apply (name, _) -> name
+    | World.And _ -> ":and"
+    | World.Or _ -> ":or"
+
+  (* Rule variables are renamed apart at every unfolding. The suffix
+     character cannot be lexed, so renamed variables are unforgeable
+     from source text. *)
+  let freshen =
+    let counter = ref 0 in
+    fun rule ->
+      incr counter;
+      let stamp = "@" ^ string_of_int !counter in
+      let rec rename = function
+        | Pattern.Var v -> Pattern.Var (v ^ stamp)
+        | Pattern.Record map -> Pattern.Record (Label.Map.map rename map)
+        | ground -> ground
+      in
+      let rec rename_expr = function
+        | World.Apply (name, bindings) ->
+            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)
+      in
+      (Label.Map.map rename rule.World.head, rename_expr rule.World.body)
+
+  (* Unify a goal's bindings against a rule head or a stored tuple.
+     Goal labels absent from the head fail the branch; head labels
+     absent from the goal are existential. *)
+  let unify_bindings subst goal_bindings target_bindings =
+    Label.Map.fold
+      (fun label pattern acc ->
+        Option.bind acc (fun subst ->
+            match Label.Map.find_opt label target_bindings with
+            | Some target -> Pattern.Subst.unify subst pattern target
+            | None -> None))
+      goal_bindings (Some subst)
+
+  (* 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 =
+    match goal with
+    | World.Or (a, b) -> Some [ (subst, flatten a); (subst, flatten b) ]
+    | World.And _ -> Some [ (subst, flatten goal) ]
+    | World.Apply (name, bindings) -> (
+        match Builtin.run subst name bindings with
+        | Some (Builtin.Solved substs) ->
+            Some (List.map (fun s -> (s, [])) substs)
+        | Some Builtin.Stuck -> None
+        | None -> (
+            match W.find world name with
+            | Some (World.Table { facts; _ }) ->
+                Some
+                  (List.filter_map
+                     (fun tuple ->
+                       let target = Label.Map.map Pattern.of_term tuple in
+                       Option.map
+                         (fun s -> (s, []))
+                         (unify_bindings subst bindings target))
+                     facts)
+            | Some (World.Rules rules) ->
+                let witness_ground rule =
+                  match rule.World.witness with
+                  | None -> true
+                  | Some label -> (
+                      match Label.Map.find_opt label bindings with
+                      | Some pattern ->
+                          Pattern.is_ground (Pattern.Subst.resolve subst pattern)
+                      | None -> false)
+                in
+                if List.for_all witness_ground rules then
+                  Some
+                    (List.filter_map
+                       (fun rule ->
+                         let head, body = freshen rule in
+                         Option.map
+                           (fun s -> (s, flatten body))
+                           (unify_bindings subst bindings head))
+                       rules)
+                else None
+            | None ->
+                (* Unreachable on admitted programs: the loader
+                   checks references. An embedded host that lies
+                   about its catalog surfaces here as a stuck goal
+                   rather than a crash. *)
+                None))
+
+  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)
+    in
+    match search Pattern.Subst.empty (flatten expr) with
+    | exception Stuck goals -> Error (Non_total_plan goals)
+    | substs ->
+        let read subst =
+          List.map
+            (fun v -> (v, Pattern.Subst.resolve subst (Pattern.Var v)))
+            variables
+        in
+        let equal_solution a b =
+          List.for_all2 (fun (_, p) (_, q) -> Pattern.equal p q) a b
+        in
+        let solutions =
+          List.fold_left
+            (fun acc subst ->
+              let solution = read subst in
+              if List.exists (equal_solution solution) acc then acc
+              else acc @ [ solution ])
+            [] substs
+        in
+        Ok solutions
+end
+
+module Standalone = Make (World.Standalone)
diff --git a/lib/vm.mli b/lib/vm.mli
new file mode 100644
index 0000000..6ce3f93
--- /dev/null
+++ b/lib/vm.mli
@@ -0,0 +1,37 @@
+(** The solver: proof search over an admitted world.
+
+    Functorized over {!World.WORLD} (decision 4): the standalone
+    binary instantiates it with {!World.Standalone}; RNT instantiates
+    it with its own catalog and links the same engine in-process.
+
+    Execution is dynamic goal selection: at each step the engine
+    runs any goal that is decidable at the current bindings, so
+    conjunction stays honestly commutative and order on the page
+    means nothing. A conjunction where no goal can ever run (an
+    unbounded membership, an unbounded recursion) is rejected as a
+    non-total plan, never attempted. Together with admission-time
+    rule checking, this is what makes every accepted query
+    terminate. *)
+
+type error =
+  | Non_total_plan of string list
+      (** No remaining goal is decidable; the relation names of the
+          stuck goals, for the message. *)
+
+val pp_error : Format.formatter -> error -> unit
+
+(** One answer: each free variable of the query, resolved. Ground in
+    the common case; open exactly when the query admits any value
+    there. *)
+type solution = (string * Pattern.t) list
+
+module Make (W : World.WORLD) : sig
+  val solve : W.t -> World.expr -> (solution list, error) result
+  (** All answers to the query, duplicates collapsed. Total: the
+      world was admitted, so search terminates; the only failure is
+      a plan the engine refuses to run. *)
+end
+
+module Standalone : sig
+  val solve : World.Standalone.t -> World.expr -> (solution list, error) result
+end