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
|
type outcome = Solved of Pattern.Subst.t list | Stuck
let forced_label name =
match Label.of_string name with Ok l -> l | Error _ -> assert false
let value_l = forced_label "value"
let left_l = forced_label "left"
let right_l = forced_label "right"
let result_l = forced_label "result"
let lower_l = forced_label "lower"
let upper_l = forced_label "upper"
let names =
[
"True";
"World";
"Integer";
"Natural";
"Rational";
"String";
"Equal";
"Plus";
"Times";
"LessThan";
"LessThanEqual";
"GreaterThan";
"GreaterEqual";
"Between";
]
let is_builtin name = List.mem name names
let fail = Solved []
let yes subst = Solved [ subst ]
(* Numeric view: integers and rationals compute together in Q, and
results come back through Term.rational, which restores the
minimal shape. An integer-valued result is an Integer. *)
let to_q = function
| Pattern.Integer z -> Some (Q.of_bigint z)
| Pattern.Rational q -> Some q
| _ -> None
let of_q q =
match Term.rational ~num:(Q.num q) ~den:(Q.den q) with
| Ok term -> Pattern.of_term term
| Error `Zero_denominator -> assert false
let arg subst bindings label =
Option.map (Pattern.Subst.resolve subst) (Label.Map.find_opt label bindings)
(* Domain membership. Unbound arguments are Stuck, never
enumerated: membership is not generation. The inclusions are the
literal ones of decision 12. *)
let domain_check subst bindings check =
match arg subst bindings value_l with
| None -> Stuck
| Some pattern ->
if Pattern.is_ground pattern then if check pattern then yes subst else fail
else Stuck
let comparison subst bindings compare =
match (arg subst bindings left_l, arg subst bindings right_l) with
| Some left, Some right -> (
match (to_q left, to_q right) with
| Some l, Some r -> if compare (Q.compare l r) 0 then yes subst else fail
| _ ->
if Pattern.is_ground left && Pattern.is_ground right then fail
else Stuck)
| _ -> Stuck
(* Plus and Times solve backwards: any two ground numeric arguments
determine the third by unification. Times through zero cannot
determine the missing factor and stays Stuck rather than guess. *)
let arithmetic subst bindings ~forward ~from_result_left ~from_result_right =
let left = arg subst bindings left_l
and right = arg subst bindings right_l
and result = Label.Map.find_opt result_l bindings in
let unify_result value =
match result with
| Some pattern -> (
match Pattern.Subst.unify subst pattern value with
| Some subst -> yes subst
| None -> fail)
| None -> yes subst
in
let solve_side binding solved =
match binding with
| Some pattern -> (
match solved with
| Some value -> (
match Pattern.Subst.unify subst pattern value with
| Some subst -> yes subst
| None -> fail)
| None -> Stuck)
| None -> Stuck
in
match (Option.bind left to_q, Option.bind right to_q) with
| Some l, Some r -> unify_result (of_q (forward l r))
| Some l, None -> (
match Option.bind result (fun p -> to_q (Pattern.Subst.resolve subst p)) with
| Some res ->
solve_side right (Option.map of_q (from_result_left res l))
| None -> Stuck)
| None, Some r -> (
match Option.bind result (fun p -> to_q (Pattern.Subst.resolve subst p)) with
| Some res ->
solve_side left (Option.map of_q (from_result_right res r))
| None -> Stuck)
| None, None -> Stuck
let between subst bindings =
let value = Label.Map.find_opt value_l bindings
and lower = arg subst bindings lower_l
and upper = arg subst bindings upper_l in
match (lower, upper) with
| Some (Pattern.Integer lo), Some (Pattern.Integer hi) -> (
match Option.map (Pattern.Subst.resolve subst) value with
| Some (Pattern.Integer v) ->
if Z.geq v lo && Z.leq v hi then yes subst else fail
| Some (Pattern.Var _) | None ->
(* Bounded generation: the one place enumeration is
admitted, because the range is finite by construction. *)
let rec enumerate v acc =
if Z.gt v hi then List.rev acc
else
let acc =
match value with
| Some pattern -> (
match
Pattern.Subst.unify subst pattern (Pattern.Integer v)
with
| Some subst -> subst :: acc
| None -> acc)
| None -> subst :: acc
in
enumerate (Z.succ v) acc
in
Solved (enumerate lo [])
| Some _ -> fail)
| Some p, Some q when Pattern.is_ground p && Pattern.is_ground q -> fail
| _ -> Stuck
let run subst name bindings =
match name with
| "True" -> Some (yes subst)
(* The universe: true of every tuple, per the specification. Its
role is to scope denial, as in [World] :not [Adult person: P]. *)
| "World" -> Some (yes subst)
| "Integer" ->
Some
(domain_check subst bindings (function
| Pattern.Integer _ -> true
| _ -> false))
| "Natural" ->
Some
(domain_check subst bindings (function
| Pattern.Integer z -> Z.geq z Z.zero
| _ -> false))
| "Rational" ->
Some
(domain_check subst bindings (function
| Pattern.Integer _ | Pattern.Rational _ -> true
| _ -> false))
| "String" ->
Some
(domain_check subst bindings (function
| Pattern.String _ -> true
| _ -> false))
| "Equal" -> (
match
(Label.Map.find_opt left_l bindings, Label.Map.find_opt right_l bindings)
with
| Some left, Some right ->
Some
(match Pattern.Subst.unify subst left right with
| Some subst -> yes subst
| None -> fail)
| _ -> Some Stuck)
| "Plus" ->
Some
(arithmetic subst bindings ~forward:Q.add
~from_result_left:(fun res l -> Some (Q.sub res l))
~from_result_right:(fun res r -> Some (Q.sub res r)))
| "Times" ->
Some
(arithmetic subst bindings ~forward:Q.mul
~from_result_left:(fun res l ->
if Q.equal l Q.zero then None else Some (Q.div res l))
~from_result_right:(fun res r ->
if Q.equal r Q.zero then None else Some (Q.div res r)))
| "LessThan" -> Some (comparison subst bindings ( < ))
| "LessThanEqual" -> Some (comparison subst bindings ( <= ))
| "GreaterThan" -> Some (comparison subst bindings ( > ))
| "GreaterEqual" -> Some (comparison subst bindings ( >= ))
| "Between" -> Some (between subst bindings)
| _ -> None
|
