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/builtin.mli | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 lib/builtin.mli (limited to 'lib/builtin.mli') 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. *) -- cgit v1.2.3