From c530682030e80ee2de2c263471e5eda7a3392e84 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 03:07:56 -0300 Subject: working vm: parser, admission with totality checks, solver and repl --- lib/vm.mli | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 lib/vm.mli (limited to 'lib/vm.mli') 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 -- cgit v1.2.3