blob: ac62781d7a329bbc9a272cdbac6694804f9748a0 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
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
|
