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

1 files changed, 37 insertions, 0 deletions

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