diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/program.mli | 22 |
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}. *) |