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

1 files changed, 70 insertions, 0 deletions

diff --git a/lib/pattern.mli b/lib/pattern.mli
new file mode 100644
index 0000000..5fc16c6
--- /dev/null
+++ b/lib/pattern.mli
@@ -0,0 +1,70 @@
+(** Open terms and unification.
+
+    A pattern is a {!Term.t} that may contain logic variables. Goals,
+    rule heads, and rule bodies are made of patterns; solving a query
+    means finding substitutions that close them back into terms.
+    Unification here is the join mechanism of the whole language:
+    shared variables across conjoined propositions unify, and that is
+    what a join is. *)
+
+type t =
+  | Var of string
+  | Integer of Z.t
+  | Rational of Q.t
+  | String of string
+  | Nil
+  | Record of t Label.Map.t
+
+val of_term : Term.t -> t
+(** Injects a closed term. Canonicity carries over unchanged. *)
+
+val to_term : t -> Term.t option
+(** Closes a pattern back into a term. [None] if any variable
+    remains, so [Some] is proof of groundness. *)
+
+val is_ground : t -> bool
+
+val vars : t -> string list
+(** Free variables, each reported once. The solver reports solutions
+    for exactly these. *)
+
+val cons : head:t -> tail:t -> t
+(** One sequence cell over open terms, [{head: _ tail: _}]. The
+    loader elaborates [#( ... )] in rule heads and bodies with
+    this. *)
+
+val equal : t -> t -> bool
+(** Syntactic equality, variables by name. Used by the totality
+    checker to compare head and body arguments. *)
+
+val strictly_contains : t -> sub:t -> bool
+(** Whether [sub] occurs strictly inside the pattern, at depth one or
+    more. This is the structural decrease witness of the admission
+    checker: a recursive call is safe when its argument is strictly
+    contained in the head's. *)
+
+val pp : Format.formatter -> t -> unit
+
+(** Substitutions bind variables to patterns. They only grow;
+    unification never revokes a binding. *)
+module Subst : sig
+  type pattern := t
+  type t
+
+  val empty : t
+
+  val walk : t -> pattern -> pattern
+  (** Follows variable bindings one level: the result is either a
+      non-variable or an unbound variable. The solver's view of "what
+      is this argument right now". *)
+
+  val resolve : t -> pattern -> pattern
+  (** Applies the substitution everywhere, recursively. Used to read
+      answers out and to test groundness of arguments. *)
+
+  val unify : t -> pattern -> pattern -> t option
+  (** Extends the substitution so both sides are equal, or reports
+      impossibility. Records unify only on identical label sets.
+      Runs an occurs check: Sol terms are finite, so a solution that
+      would need an infinite term is a failure, not a loop. *)
+end