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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
(* End-to-end: source text through parsing, admission, and solving. *)
let load source =
match Sol.Front.parse_string source with
| Error message -> Alcotest.failf "parse error: %s" message
| Ok statements -> Sol.World.Standalone.load statements
let run source =
match load source with
| Error error -> Alcotest.failf "load error: %a" Sol.World.pp_error error
| Ok (world, queries) ->
List.map
(fun query ->
match Sol.Vm.Standalone.solve world query with
| Ok solutions -> solutions
| Error error ->
Alcotest.failf "solve error: %a" Sol.Vm.pp_error error)
queries
let show solutions =
solutions
|> List.map (fun solution ->
solution
|> List.map (fun (v, p) -> Format.asprintf "%s=%a" v Sol.Pattern.pp p)
|> String.concat ",")
|> String.concat "; "
let check_answers description source expected =
match run source with
| [ solutions ] -> Alcotest.(check string) description expected (show solutions)
| results ->
Alcotest.failf "expected one query, got %d" (List.length results)
(* Facts, joins, and rules over stored relations. *)
let people =
{|
Relation named: Person schema: #( [name domain: String] [age domain: Integer] )
[Person name: "Marcos" age: 30]
[Person name: "Ana" age: 12]
[Person name: "Rui" age: 70]
Rule name: "adults" head: [Adult name: N] body:
[Person name: N age: A] :and [GreaterEqual left: A right: 18]
|}
let test_scan () =
check_answers "all people"
(people ^ {| Query expression: [Person name: N age: A] |})
{|A=30,N="Marcos"; A=12,N="Ana"; A=70,N="Rui"|}
let test_rule_join () =
check_answers "adults via rule"
(people ^ {| Query expression: [Adult name: N] |})
{|N="Marcos"; N="Rui"|}
let test_conjunction_is_commutative () =
let forward =
people
^ {| Query expression: [Person name: N age: A] :and [GreaterThan left: A right: 20] |}
and backward =
people
^ {| Query expression: [GreaterThan left: A right: 20] :and [Person name: N age: A] |}
in
Alcotest.(check string)
"order on the page means nothing"
(show (List.hd (run forward)))
(show (List.hd (run backward)))
(* Arithmetic solves backwards; the numeric tower stays minimal
shape. *)
let test_plus_backward () =
check_answers "X + 5 = 12"
{| Query expression: [Plus left: X right: 5 result: 12] |} "X=7"
let test_times_rational () =
check_answers "3 * X = 2 solves in the rationals"
{| Query expression: [Times left: 3 right: X result: 2] |} "X=2/3"
let test_rational_collapse_in_arithmetic () =
check_answers "1/2 + 1/2 collapses to the integer 1"
{| Query expression: [Plus left: 1/2 right: 1/2 result: R] |} "R=1"
(* Structural recursion, admitted by the decrease witness. *)
let length_rules =
{|
Rule name: "length nil" head: [Length list: #() result: 0] body: [True]
Rule name: "length cons" head: [Length list: #(H | T) result: R] body:
[Length list: T result: P] :and [Plus left: 1 right: P result: R]
|}
let test_length () =
check_answers "length of #(1 2 3)"
(length_rules ^ {| Query expression: [Length list: #(1 2 3) result: R] |})
"R=3"
let test_length_of_strings () =
check_answers "length is polymorphic over members"
(length_rules
^ {| Query expression: [Length list: #("a" "b") result: R] |})
"R=2"
(* Bounded generation is the only enumeration. *)
let test_between_generates () =
check_answers "between enumerates its finite range"
{| Query expression: [Between value: X lower: 1 upper: 4] :and [GreaterThan left: X right: 2] |}
"X=3; X=4"
let test_disjunction () =
check_answers "disjunction branches"
{| Query expression: [Equal left: X right: 1] :or [Equal left: X right: 2] |}
"X=1; X=2"
(* Totality: what must be rejected, is. *)
let test_loop_rule_rejected () =
match load {| Rule name: "loop" head: [Loop value: X] body: [Loop value: X] |} with
| Error _ -> ()
| Ok _ -> Alcotest.fail "a rule with no structural decrease must be rejected"
let test_mutual_recursion_rejected () =
match
load
{|
Rule name: "a" head: [A value: X] body: [B value: X]
Rule name: "b" head: [B value: X] body: [A value: X]
|}
with
| Error _ -> ()
| Ok _ -> Alcotest.fail "mutual recursion must be rejected"
let test_unbounded_membership_is_non_total_plan () =
match load {| Query expression: [Integer value: X] |} with
| Error error -> Alcotest.failf "load error: %a" Sol.World.pp_error error
| Ok (world, [ query ]) -> (
match Sol.Vm.Standalone.solve world query with
| Error (Sol.Vm.Non_total_plan _) -> ()
| Ok _ -> Alcotest.fail "must be rejected as a non-total plan")
| Ok _ -> Alcotest.fail "expected one query"
let test_domain_constrains_when_ground () =
check_answers "membership checks once ground"
{| Query expression: [Between value: X lower: -2 upper: 2] :and [Natural value: X] |}
"X=0; X=1; X=2"
(* Integrity control at loading: facts must satisfy their schema. *)
let test_fact_domain_violation () =
match
load
{|
Relation named: Score schema: #( [value domain: Natural] )
[Score value: -3]
|}
with
| Error _ -> ()
| Ok _ -> Alcotest.fail "a fact violating its domain must be rejected"
let () =
Alcotest.run "sol-vm"
[
( "relations",
[
Alcotest.test_case "scan" `Quick test_scan;
Alcotest.test_case "rule and join" `Quick test_rule_join;
Alcotest.test_case "commutative conjunction" `Quick
test_conjunction_is_commutative;
] );
( "arithmetic",
[
Alcotest.test_case "plus backward" `Quick test_plus_backward;
Alcotest.test_case "times rational" `Quick test_times_rational;
Alcotest.test_case "minimal shape" `Quick
test_rational_collapse_in_arithmetic;
] );
( "recursion",
[
Alcotest.test_case "length" `Quick test_length;
Alcotest.test_case "length over strings" `Quick test_length_of_strings;
] );
( "search",
[
Alcotest.test_case "bounded generation" `Quick test_between_generates;
Alcotest.test_case "disjunction" `Quick test_disjunction;
] );
( "totality",
[
Alcotest.test_case "loop rejected" `Quick test_loop_rule_rejected;
Alcotest.test_case "mutual recursion rejected" `Quick
test_mutual_recursion_rejected;
Alcotest.test_case "unbounded membership rejected" `Quick
test_unbounded_membership_is_non_total_plan;
Alcotest.test_case "membership once ground" `Quick
test_domain_constrains_when_ground;
Alcotest.test_case "fact domain violation" `Quick
test_fact_domain_violation;
] );
]
|
