blob: b0e363b04cb3136709dd533fafe2d3b732d8f8eb (
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
41
42
43
44
45
46
47
48
49
50
51
52
|
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
(* Membership must be proven outright: an answer that is
itself conditioned on residual constraints does not
admit a fact. *)
| Ok solutions
when List.exists (fun s -> s.Vm.residue = []) solutions ->
admit rest
| Ok (_ :: _) ->
Error
(Undecidable_criterion
{
relation = pending_relation;
label = Label.to_string pending_label;
})
| 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
|
