diff options
Diffstat (limited to 'lib/program.ml')
| -rw-r--r-- | lib/program.ml | 40 |
1 files changed, 40 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 |