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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
(* Decision 4, exercised: a host builds its own world in OCaml, no
parsing involved, and links the same solver. This is the shape of
the RNT embedding: the kernel's catalog answers [find], and the
engine runs in-process. *)
let label s =
match Sol.Label.of_string s with
| Ok l -> l
| Error (`Invalid_label s) -> Alcotest.failf "invalid label: %s" s
let int n = Sol.Term.integer (Z.of_int n)
(* A toy kernel catalog: one stored relation, served from an OCaml
structure rather than program text. *)
module Kernel_world = struct
type t = unit
let tuple pairs =
List.fold_left
(fun map (name, term) -> Sol.Label.Map.add (label name) term map)
Sol.Label.Map.empty pairs
let sensors =
Sol.World.Table
{
schema = [ (label "id", Sol.World.Primitive Sol.World.D_integer) ];
facts =
[
tuple [ ("id", int 1); ("reading", int 40) ];
tuple [ ("id", int 2); ("reading", int 75) ];
tuple [ ("id", int 3); ("reading", int 12) ];
];
}
let find () name =
match name with "Sensor" -> Some sensors | _ -> None
end
module Kernel_vm = Sol.Vm.Make (Kernel_world)
(* The host compiles query text itself through the exposed
expression compiler; its own catalog answers for relations. *)
let solve source =
match Sol.Front.parse_string ("Query expression: " ^ source) with
| Error message -> Alcotest.failf "parse error: %s" message
| Ok [ Sol.Ast.Directive ("Query", [ ("expression", node) ]) ] -> (
match Sol.World.expr_of_node node with
| Error error -> Alcotest.failf "compile error: %a" Sol.World.pp_error error
| Ok query -> Kernel_vm.solve () query)
| Ok _ -> Alcotest.fail "expected one query statement"
let show solutions =
solutions
|> List.map (fun { Sol.Vm.bindings; residue } ->
List.map
(fun (v, p) -> Format.asprintf "%s=%a" v Sol.Pattern.pp p)
bindings
@ List.map (Format.asprintf "%a" Sol.Vm.pp_residual) residue
|> String.concat ",")
|> String.concat "; "
let test_kernel_scan () =
match solve {| [Sensor id: I reading: R] :and [GreaterThan left: R right: 30] |} with
| Ok solutions ->
Alcotest.(check string) "hot sensors" "I=1,R=40; I=2,R=75" (show solutions)
| Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error
let test_kernel_totality () =
(* A universal over an infinite domain whose body the symbolic
fragment cannot read: neither enumerable nor provable, so it
must be rejected, embedding or not. *)
match
solve
{| [ForAll variable: X quantifier: [Integer value: X] body: [Sensor id: X]] |}
with
| Error (Sol.Vm.Non_total_plan _) -> ()
| Ok _ -> Alcotest.fail "the embedded engine must keep the totality guard"
let test_kernel_residuation () =
match solve {| [Integer value: X] |} with
| Ok [ { Sol.Vm.residue = [ ("Integer", _) ]; _ } ] -> ()
| Ok _ -> Alcotest.fail "open membership must residuate in the embedding too"
| Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error
let () =
Alcotest.run "sol-embedding"
[
( "kernel world",
[
Alcotest.test_case "scan over host relations" `Quick test_kernel_scan;
Alcotest.test_case "totality guard survives embedding" `Quick
test_kernel_totality;
Alcotest.test_case "residuation survives embedding" `Quick
test_kernel_residuation;
] );
]
|
