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

1 files changed, 67 insertions, 0 deletions

diff --git a/lib/world.mli b/lib/world.mli
new file mode 100644
index 0000000..76ad316
--- /dev/null
+++ b/lib/world.mli
@@ -0,0 +1,67 @@
+(** Worlds: the store of relations, and the loader that builds the
+    standalone one.
+
+    Decision 4 of the integration document: the VM is parameterized
+    over a world. This module gives the module type every host
+    satisfies, the standalone in-memory world, and the loader that
+    admits a parsed program into it. Admission is where totality is
+    enforced: a program that gets a world is a program whose queries
+    terminate. *)
+
+(** A compiled relational expression: what rule bodies and queries
+    are made of after names are resolved. *)
+type expr =
+  | Apply of string * Pattern.t Label.Map.t
+  | And of expr * expr
+  | Or of expr * expr
+
+type rule = {
+  rule_name : string;
+  head : Pattern.t Label.Map.t;
+  body : expr;
+  witness : Label.t option;
+      (** For a recursive rule, the label whose argument strictly
+          decreases. The VM requires it ground before unfolding,
+          which is what turns the admission proof into runtime
+          termination. [None] on non-recursive rules. *)
+}
+
+(** The builtin domains a schema may constrain an attribute by. *)
+type domain = D_integer | D_natural | D_rational | D_string
+
+(** How a relation is defined. *)
+type def =
+  | Table of { schema : (Label.t * domain) list; facts : Term.t Label.Map.t list }
+      (** Extensional: a schema and finite stored tuples. *)
+  | Rules of rule list  (** Intensional: defined by admitted rules. *)
+
+(** What a host must answer for the VM to run: which relation lives
+    under a name. Builtins are the VM's own and are not consulted
+    here. *)
+module type WORLD = sig
+  type t
+
+  val find : t -> string -> def option
+end
+
+type error
+
+val pp_error : Format.formatter -> error -> unit
+
+(** The standalone world: an immutable catalog loaded from program
+    text. This is Sol as a separate language; there are no branches,
+    no transitions, only the pure fragment. *)
+module Standalone : sig
+  type t
+
+  val find : t -> string -> def option
+
+  val load : Ast.statement list -> (t * expr list, error) result
+  (** Admits a program: registers relations, checks every fact
+      against its schema and domains, compiles rules and queries,
+      and enforces totality. Rejected, not deferred: a recursive
+      rule without a structural decrease witness, a mutual
+      recursion cycle, an unknown relation, or an ill-typed fact is
+      an [error], and no world exists. Returns the world and the
+      query expressions in program order. *)
+end