negation, quantifiers and membership criteria as schema domains

1 files changed, 22 insertions, 0 deletions

diff --git a/lib/program.mli b/lib/program.mli
new file mode 100644
index 0000000..c271212
--- /dev/null
+++ b/lib/program.mli
@@ -0,0 +1,22 @@
+(** Whole-program admission: the entry point hosts use.
+
+    The loader admits what it can decide alone; membership criteria
+    need the solver, so this module finishes admission by running
+    every pending criterion against the fully loaded world. Order of
+    facts in the source does not matter: integrity is judged against
+    the complete extension, the way a committed state would be. *)
+
+type error =
+  | Load of World.error
+  | Integrity of { relation : string; label : string }
+      (** A fact's attribute failed its membership criterion. *)
+  | Undecidable_criterion of { relation : string; label : string }
+      (** The criterion's plan was rejected as non-total. *)
+
+val pp_error : Format.formatter -> error -> unit
+
+val load :
+  Ast.statement list -> (World.Standalone.t * World.expr list, error) result
+(** Parses nothing and solves queries for nobody: admits. Returns
+    the world and the query expressions, ready for
+    {!Vm.Standalone.solve}. *)