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

1 files changed, 29 insertions, 0 deletions

diff --git a/lib/builtin.mli b/lib/builtin.mli
new file mode 100644
index 0000000..d7017e3
--- /dev/null
+++ b/lib/builtin.mli
@@ -0,0 +1,29 @@
+(** The builtin relations every world carries.
+
+    Builtins are relations with operational capabilities beyond
+    scanning: they check membership against the host (the domain
+    relations), evaluate and solve (arithmetic), unify (equality),
+    and generate boundedly (Between). The VM consults this module
+    before the world.
+
+    A builtin never enumerates an infinite domain. When its
+    arguments are too unbound to decide, the answer is {!Stuck}, and
+    the planner tries it again later or rejects the plan; totality
+    is preserved either way. *)
+
+type outcome =
+  | Solved of Pattern.Subst.t list
+      (** Zero or more ways to satisfy the goal. The empty list is
+          failure. *)
+  | Stuck
+      (** Not decidable at the current bindings; retry once more
+          variables are ground. *)
+
+val is_builtin : string -> bool
+(** Whether a name is a builtin. The loader uses it for reference
+    checking, so user relations cannot shadow builtins. *)
+
+val run : Pattern.Subst.t -> string -> Pattern.t Label.Map.t -> outcome option
+(** Executes one builtin goal under the substitution. [None] when
+    the name is not a builtin, so the VM falls through to the
+    world. *)