negation, quantifiers and membership criteria as schema domains

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