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

2 files changed, 210 insertions, 0 deletions

diff --git a/lib/pattern.ml b/lib/pattern.ml
new file mode 100644
index 0000000..823162c
--- /dev/null
+++ b/lib/pattern.ml
@@ -0,0 +1,140 @@
+type t =
+  | Var of string
+  | Integer of Z.t
+  | Rational of Q.t
+  | String of string
+  | Nil
+  | Record of t Label.Map.t
+
+let rec of_term (term : Term.t) =
+  match term with
+  | Term.Integer z -> Integer z
+  | Term.Rational q -> Rational q
+  | Term.String s -> String s
+  | Term.Nil -> Nil
+  | Term.Record map -> Record (Label.Map.map of_term map)
+
+let rec to_term = function
+  | Var _ -> None
+  | Integer z -> Some (Term.integer z)
+  | Rational q ->
+      (* Rebuilding through the smart constructor keeps canonicity a
+         single-point invariant. The denominator is nonzero by
+         construction, so this cannot fail. *)
+      Result.to_option (Term.rational ~num:(Q.num q) ~den:(Q.den q))
+  | String s -> Some (Term.string s)
+  | Nil -> Some Term.nil
+  | Record map ->
+      let closed =
+        Label.Map.fold
+          (fun label pattern acc ->
+            match (acc, to_term pattern) with
+            | Some bindings, Some term -> Some ((label, term) :: bindings)
+            | _ -> None)
+          map (Some [])
+      in
+      Option.bind closed (fun bindings -> Result.to_option (Term.record bindings))
+
+let is_ground pattern = Option.is_some (to_term pattern)
+
+let vars pattern =
+  let rec collect acc = function
+    | Var v -> if List.mem v acc then acc else v :: acc
+    | Integer _ | Rational _ | String _ | Nil -> acc
+    | Record map -> Label.Map.fold (fun _ p acc -> collect acc p) map acc
+  in
+  List.rev (collect [] pattern)
+
+let forced_label name =
+  match Label.of_string name with Ok l -> l | Error _ -> assert false
+
+let head_label = forced_label "head"
+let tail_label = forced_label "tail"
+
+let cons ~head ~tail =
+  Record Label.Map.(empty |> add head_label head |> add tail_label tail)
+
+let rec equal a b =
+  match (a, b) with
+  | Var x, Var y -> String.equal x y
+  | Integer x, Integer y -> Z.equal x y
+  | Rational x, Rational y -> Q.equal x y
+  | String x, String y -> String.equal x y
+  | Nil, Nil -> true
+  | Record x, Record y -> Label.Map.equal equal x y
+  | _ -> false
+
+let strictly_contains pattern ~sub =
+  let rec inside p = equal p sub || strictly p
+  and strictly = function
+    | Record map -> Label.Map.exists (fun _ p -> inside p) map
+    | _ -> false
+  in
+  strictly pattern
+
+let rec pp fmt = function
+  | Var v -> Format.pp_print_string fmt v
+  | Integer z -> Z.pp_print fmt z
+  | Rational q -> Q.pp_print fmt q
+  | String s -> Format.fprintf fmt "%S" s
+  | Nil -> Format.pp_print_string fmt "#()"
+  | Record map ->
+      Format.fprintf fmt "@[<hv 1>{";
+      let first = ref true in
+      Label.Map.iter
+        (fun label p ->
+          if not !first then Format.fprintf fmt "@ ";
+          first := false;
+          Format.fprintf fmt "%a %a" Label.pp label pp p)
+        map;
+      Format.fprintf fmt "}@]"
+
+module Subst = struct
+  module M = Map.Make (String)
+
+  type pattern = t
+  type nonrec t = pattern M.t
+
+  let empty = M.empty
+
+  let rec walk subst pattern =
+    match pattern with
+    | Var v -> (
+        match M.find_opt v subst with
+        | Some bound -> walk subst bound
+        | None -> pattern)
+    | _ -> pattern
+
+  let rec resolve subst pattern =
+    match walk subst pattern with
+    | Record map -> Record (Label.Map.map (resolve subst) map)
+    | other -> other
+
+  let rec occurs subst v pattern =
+    match walk subst pattern with
+    | Var w -> String.equal v w
+    | Record map -> Label.Map.exists (fun _ p -> occurs subst v p) map
+    | _ -> false
+
+  let rec unify subst a b =
+    let a = walk subst a and b = walk subst b in
+    match (a, b) with
+    | Var x, Var y when String.equal x y -> Some subst
+    | Var x, other | other, Var x ->
+        if occurs subst x other then None else Some (M.add x other subst)
+    | Integer x, Integer y -> if Z.equal x y then Some subst else None
+    | Rational x, Rational y -> if Q.equal x y then Some subst else None
+    | String x, String y -> if String.equal x y then Some subst else None
+    | Nil, Nil -> Some subst
+    | Record x, Record y ->
+        if
+          Label.Map.cardinal x = Label.Map.cardinal y
+          && Label.Map.for_all (fun label _ -> Label.Map.mem label y) x
+        then
+          Label.Map.fold
+            (fun label p acc ->
+              Option.bind acc (fun s -> unify s p (Label.Map.find label y)))
+            x (Some subst)
+        else None
+    | _ -> None
+end
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