diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/program.ml | 40 | ||||
| -rw-r--r-- | lib/program.mli | 22 |
2 files changed, 62 insertions, 0 deletions
diff --git a/lib/program.ml b/lib/program.ml new file mode 100644 index 0000000..ac62781 --- /dev/null +++ b/lib/program.ml @@ -0,0 +1,40 @@ +type error = + | Load of World.error + | Integrity of { relation : string; label : string } + | Undecidable_criterion of { relation : string; label : string } + +let pp_error fmt = function + | Load error -> World.pp_error fmt error + | Integrity { relation; label } -> + Format.fprintf fmt "integrity violation on %s at %s:" relation label + | Undecidable_criterion { relation; label } -> + Format.fprintf fmt "criterion on %s at %s: is not decidable" relation label + +let load statements = + match World.Standalone.load statements with + | Error error -> Error (Load error) + | Ok (world, queries, pendings) -> + let rec admit = function + | [] -> Ok (world, queries) + | pending :: rest -> ( + let { World.pending_relation; pending_label; pending_body } = + pending + in + match Vm.Standalone.solve world pending_body with + | Ok (_ :: _) -> admit rest + | Ok [] -> + Error + (Integrity + { + relation = pending_relation; + label = Label.to_string pending_label; + }) + | Error (Vm.Non_total_plan _) -> + Error + (Undecidable_criterion + { + relation = pending_relation; + label = Label.to_string pending_label; + })) + in + admit pendings 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}. *) |