forked from
liamoc.net/holbert-ng
the next generation of the in-browser educational proof assistant
Atom for HOTerm
+1016
-746
+785
-666
src/HOTerm.res
+785
-666
src/HOTerm.res
···
3
3
let cmp = Pervasives.compare
4
4
})
5
5
6
-
type rec t =
7
-
| Symbol({name: string, constructor: bool})
8
-
| Var({idx: int})
9
-
| Schematic({schematic: int})
10
-
| Lam({name: string, body: t})
11
-
| App({func: t, arg: t})
12
-
// Unallowed is used internally in unify, where Nipkow 1993 uses Var(-infinity)
13
-
| Unallowed
14
-
type meta = string
15
-
type schematic = int
16
-
type subst = Belt.Map.Int.t<t>
17
-
let substHas = (subst: subst, schematic: schematic) => subst->Belt.Map.Int.has(schematic)
18
-
let substGet = (subst: subst, schematic: schematic) => subst->Belt.Map.Int.get(schematic)
19
-
let mapSubst = (m: subst, f: t => t): subst => {
20
-
m->Belt.Map.Int.map(f)
21
-
}
22
-
let substEqual = (m1, m2) => m1 == m2
23
-
let makeSubst = () => {
24
-
Belt.Map.Int.empty
25
-
}
26
-
let mergeSubsts = (m1: subst, m2: subst) =>
27
-
Belt.Map.Int.merge(m1, m2, (_, o1, o2) =>
28
-
switch (o1, o2) {
29
-
| (Some(v), _) | (_, Some(v)) => Some(v)
30
-
| (None, None) => None
6
+
module type ATOM = AtomDef.ATOM
7
+
8
+
module DefaultAtom = {
9
+
module BaseAtom = AtomDef.MakeBaseAtom({
10
+
type t = string
11
+
})
12
+
type t = string
13
+
type subst = Map.t<int, string>
14
+
let unify = (a, b, ~gen as _=?) =>
15
+
if a == b {
16
+
Seq.once(Map.make())
17
+
} else {
18
+
Seq.empty
19
+
}
20
+
let prettyPrint = (name, ~scope as _: array<string>) => name
21
+
let symbolRegexpString = "^([^\\s()]+)"
22
+
let parse = (str0, ~scope as _: array<string>, ~gen as _=?) => {
23
+
let str = str0->String.trimStart
24
+
let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
25
+
switch re->RegExp.exec(str) {
26
+
| None => Error("invalid symbol")
27
+
| Some(res) =>
28
+
switch RegExp.Result.matches(res) {
29
+
| [name] => Ok((name, String.sliceToEnd(str, ~start=RegExp.lastIndex(re))))
30
+
| _ => Error("invalid symbol")
31
+
}
31
32
}
32
-
)
33
-
let rec equivalent = (a: t, b: t) => {
34
-
switch (a, b) {
35
-
| (Symbol({name: na}), Symbol({name: nb})) => na == nb
36
-
| (Var({idx: ia}), Var({idx: ib})) => ia == ib
37
-
| (Schematic({schematic: sa}), Schematic({schematic: sb})) => sa == sb
38
-
| (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => equivalent(ba, bb)
39
-
| (App({func: fa, arg: aa}), App({func: fb, arg: ab})) => equivalent(fa, fb) && equivalent(aa, ab)
40
-
| (Unallowed, Unallowed) => false
41
-
| (_, _) => false
42
33
}
34
+
let substitute = (name, _) => name
35
+
let substDeBruijn = (name, _, ~from as _=?) => name
36
+
let concrete = _ => true
37
+
let upshift = (t, _, ~from as _=?) => t
38
+
let coerce = _ => None
43
39
}
44
-
type gen = ref<int>
45
-
let seen = (g: gen, s: int) => {
46
-
if s >= g.contents {
47
-
g := s + 1
40
+
41
+
module Make = (Atom: AtomDef.ATOM): {
42
+
type rec t =
43
+
| Symbol({name: Atom.t, constructor: bool})
44
+
| Var({idx: int})
45
+
| Schematic({schematic: int})
46
+
| Lam({name: string, body: t})
47
+
| App({func: t, arg: t})
48
+
| Unallowed
49
+
50
+
include Signatures.TERM
51
+
with type t := t
52
+
and type meta = string
53
+
and type schematic = int
54
+
and type subst = Belt.Map.Int.t<t>
55
+
56
+
let emptySubst: subst
57
+
let strip: t => (t, array<t>)
58
+
let app: (t, array<t>) => t
59
+
let mkvars: int => array<t>
60
+
let mapTerms: (t, t => t) => t
61
+
exception UnifyFail(string)
62
+
let substAdd: (subst, schematic, t) => subst
63
+
let unifyTerm: (t, t, subst, ~gen: option<gen>) => Seq.t<subst>
64
+
let reduceSubst: subst => subst
65
+
let rewrite: (t, t, t, ~subst: subst, ~gen: option<gen>) => (subst, t)
66
+
} => {
67
+
type rec t =
68
+
| Symbol({name: Atom.t, constructor: bool})
69
+
| Var({idx: int})
70
+
| Schematic({schematic: int})
71
+
| Lam({name: string, body: t})
72
+
| App({func: t, arg: t})
73
+
// Unallowed is used internally in unify, where Nipkow 1993 uses Var(-infinity)
74
+
| Unallowed
75
+
type meta = string
76
+
type schematic = int
77
+
type subst = Belt.Map.Int.t<t>
78
+
let substHas = (subst: subst, schematic: schematic) => subst->Belt.Map.Int.has(schematic)
79
+
let substGet = (subst: subst, schematic: schematic) => subst->Belt.Map.Int.get(schematic)
80
+
let mapSubst = (m: subst, f: t => t): subst => {
81
+
m->Belt.Map.Int.map(f)
48
82
}
49
-
}
50
-
let fresh = (g: gen, ~replacing as _=?) => {
51
-
let v = g.contents
52
-
g := g.contents + 1
53
-
v
54
-
}
55
-
let rec schematicsIn = (subst: subst, it: t): Belt.Set.t<schematic, IntCmp.identity> =>
56
-
switch it {
57
-
| Schematic({schematic, _}) if subst->substHas(schematic) =>
58
-
let found = subst->substGet(schematic)->Option.getExn
59
-
schematicsIn(subst, found)
60
-
| Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
61
-
| Lam({body}) => schematicsIn(subst, body)
62
-
| App({func, arg}) => Belt.Set.union(schematicsIn(subst, func), schematicsIn(subst, arg))
63
-
| Unallowed | Symbol(_) | Var(_) => Belt.Set.make(~id=module(IntCmp))
83
+
let substEqual = (m1, m2) => m1 == m2
84
+
let makeSubst = () => {
85
+
Belt.Map.Int.empty
64
86
}
65
-
let occ = (schematic: schematic, subst: subst, t: t): bool => {
66
-
let set = schematicsIn(subst, t)
67
-
set->Belt.Set.has(schematic)
68
-
}
69
-
let rec freeVarsIn = (subst: subst, it: t): Belt.Set.t<int, IntCmp.identity> =>
70
-
switch it {
71
-
| Schematic({schematic, _}) if subst->substHas(schematic) =>
72
-
let found = subst->substGet(schematic)->Option.getExn
73
-
freeVarsIn(subst, found)
74
-
| Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
75
-
| Lam({name: _, body}) =>
76
-
freeVarsIn(subst, body)
77
-
->Belt.Set.toArray
78
-
->Array.filterMap(v =>
79
-
if v >= 1 {
80
-
Some(v - 1)
81
-
} else {
82
-
None
87
+
let mergeSubsts = (m1: subst, m2: subst) =>
88
+
Belt.Map.Int.merge(m1, m2, (_, o1, o2) =>
89
+
switch (o1, o2) {
90
+
| (Some(v), _) | (_, Some(v)) => Some(v)
91
+
| (None, None) => None
83
92
}
84
93
)
85
-
->Belt.Set.fromArray(~id=module(IntCmp))
86
-
| App({func, arg}) => Belt.Set.union(freeVarsIn(subst, func), freeVarsIn(subst, arg))
87
-
| Unallowed | Symbol(_) | Schematic(_) => Belt.Set.make(~id=module(IntCmp))
94
+
let rec equivalent = (a: t, b: t) => {
95
+
switch (a, b) {
96
+
| (Symbol({name: a}), Symbol({name: b})) => a == b
97
+
| (Var({idx: ia}), Var({idx: ib})) => ia == ib
98
+
| (Schematic({schematic: sa}), Schematic({schematic: sb})) => sa == sb
99
+
| (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => equivalent(ba, bb)
100
+
| (App({func: fa, arg: aa}), App({func: fb, arg: ab})) =>
101
+
equivalent(fa, fb) && equivalent(aa, ab)
102
+
| (Unallowed, Unallowed) => false
103
+
| (_, _) => false
104
+
}
105
+
}
106
+
type gen = ref<int>
107
+
let seen = (g: gen, s: int) => {
108
+
if s >= g.contents {
109
+
g := s + 1
110
+
}
111
+
}
112
+
let fresh = (g: gen, ~replacing as _=?) => {
113
+
let v = g.contents
114
+
g := g.contents + 1
115
+
v
116
+
}
117
+
let rec schematicsIn = (subst: subst, it: t): Belt.Set.t<schematic, IntCmp.identity> =>
118
+
switch it {
119
+
| Schematic({schematic, _}) if subst->substHas(schematic) =>
120
+
let found = subst->substGet(schematic)->Option.getExn
121
+
schematicsIn(subst, found)
122
+
| Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
123
+
| Lam({body}) => schematicsIn(subst, body)
124
+
| App({func, arg}) => Belt.Set.union(schematicsIn(subst, func), schematicsIn(subst, arg))
125
+
| Unallowed | Symbol(_) | Var(_) => Belt.Set.make(~id=module(IntCmp))
126
+
}
127
+
let occ = (schematic: schematic, subst: subst, t: t): bool => {
128
+
let set = schematicsIn(subst, t)
129
+
set->Belt.Set.has(schematic)
88
130
}
89
-
let freeVarsContains = (term: t, subst: subst, idx: int): bool => {
90
-
let set = freeVarsIn(subst, term)
91
-
set->Belt.Set.has(idx)
92
-
}
93
-
// f might map an index to a new one (Ok(newIdx)) or to a term (Error(t) with t(from)).
94
-
// Note that Ok and Error here are not used for success or failure; they are just two cases distinguishing between an index and a term.
95
-
let rec mapbind0 = (term: t, f: int => result<int, int => t>, ~from: int=0): t =>
96
-
switch term {
97
-
| Symbol(_) => term
98
-
| Var({idx}) =>
99
-
if idx >= from {
100
-
switch f(idx - from) {
101
-
| Ok(newIdx) =>
102
-
let new = newIdx + from
103
-
if new < 0 {
104
-
throw(Util.Err("mapbind: negative index"))
131
+
let rec freeVarsIn = (subst: subst, it: t): Belt.Set.t<int, IntCmp.identity> =>
132
+
switch it {
133
+
| Schematic({schematic, _}) if subst->substHas(schematic) =>
134
+
let found = subst->substGet(schematic)->Option.getExn
135
+
freeVarsIn(subst, found)
136
+
| Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
137
+
| Lam({name: _, body}) =>
138
+
freeVarsIn(subst, body)
139
+
->Belt.Set.toArray
140
+
->Array.filterMap(v =>
141
+
if v >= 1 {
142
+
Some(v - 1)
143
+
} else {
144
+
None
145
+
}
146
+
)
147
+
->Belt.Set.fromArray(~id=module(IntCmp))
148
+
| App({func, arg}) => Belt.Set.union(freeVarsIn(subst, func), freeVarsIn(subst, arg))
149
+
| Unallowed | Symbol(_) | Schematic(_) => Belt.Set.make(~id=module(IntCmp))
150
+
}
151
+
let freeVarsContains = (term: t, subst: subst, idx: int): bool => {
152
+
let set = freeVarsIn(subst, term)
153
+
set->Belt.Set.has(idx)
154
+
}
155
+
// f might map an index to a new one (Ok(newIdx)) or to a term (Error(t) with t(from)).
156
+
// Note that Ok and Error here are not used for success or failure; they are just two cases distinguishing between an index and a term.
157
+
let rec _mapbind0 = (term: t, f: int => result<int, int => t>, ~from: int=0): t =>
158
+
switch term {
159
+
| Symbol(_) => term
160
+
| Var({idx}) =>
161
+
if idx >= from {
162
+
switch f(idx - from) {
163
+
| Ok(newIdx) =>
164
+
let new = newIdx + from
165
+
if new < 0 {
166
+
throw(Util.Err("mapbind: negative index"))
167
+
}
168
+
Var({
169
+
idx: new,
170
+
})
171
+
| Error(t) => t(from)
105
172
}
106
-
Var({
107
-
idx: new,
108
-
})
109
-
| Error(t) => t(from)
173
+
} else {
174
+
term
110
175
}
111
-
} else {
112
-
term
176
+
| Schematic({schematic}) =>
177
+
Schematic({
178
+
schematic: schematic,
179
+
})
180
+
| Lam({name, body}) =>
181
+
Lam({
182
+
name,
183
+
body: _mapbind0(body, f, ~from=from + 1),
184
+
})
185
+
| App({func, arg}) =>
186
+
App({
187
+
func: _mapbind0(func, f, ~from),
188
+
arg: _mapbind0(arg, f, ~from),
189
+
})
190
+
| Unallowed => Unallowed
113
191
}
114
-
| Schematic({schematic}) =>
115
-
Schematic({
116
-
schematic: schematic,
117
-
})
118
-
| Lam({name, body}) =>
119
-
Lam({
120
-
name,
121
-
body: mapbind0(body, f, ~from=from + 1),
122
-
})
123
-
| App({func, arg}) =>
124
-
App({
125
-
func: mapbind0(func, f, ~from),
126
-
arg: mapbind0(arg, f, ~from),
127
-
})
128
-
| Unallowed => Unallowed
129
-
}
130
-
let mapbind = (term: t, f: int => int, ~from: int=0): t => mapbind0(term, idx => Ok(f(idx)), ~from)
131
-
let upshift = (term: t, amount: int, ~from: int=0) => mapbind(term, idx => idx + amount, ~from)
132
-
let downshift = (term: t, amount: int, ~from: int=1) => {
133
-
if amount > from {
134
-
throw(Util.Err("downshift amount must be less than from"))
135
-
}
136
-
mapbind(term, idx => idx - amount, ~from)
137
-
}
138
-
let lookup = (term: t, subst: array<(t, t)>): option<t> => {
139
-
subst
140
-
->Array.find(((from, _)) => equivalent(term, from))
141
-
->Option.map(((_, to)) => to)
142
-
}
143
-
let upshift_tt = (subst: array<(t, t)>, ~amount: int=1): array<(t, t)> => {
144
-
subst->Array.map(((a, b)) => (upshift(a, amount), upshift(b, amount)))
145
-
}
146
-
// where pattern unification used mapbind we will need to use discharge for FCU
147
-
//
148
-
// When `prune` is true, it marks “dead” variables as Unallowed. Nipkow 1993 uses Var(-infinity) for this in the de Bruijn’s notation implementation.
149
-
// Nipkow 1993's non de Bruijn implementation handle this logic in `proj`. Similarly Makoto Hamana's paper uses `elem` and `subst` in `prune`
150
-
let rec discharge = (subst: array<(t, t)>, term: t, ~prune: bool): t => {
151
-
switch lookup(term, subst) {
152
-
| Some(found) => found
153
-
| None =>
192
+
let rec upshift = (term: t, amount: int, ~from: int=0) =>
154
193
switch term {
194
+
| Symbol({name, constructor}) => Symbol({name: Atom.upshift(name, amount, ~from), constructor})
195
+
| Var({idx}) =>
196
+
Var({
197
+
idx: if idx >= from {
198
+
idx + amount
199
+
} else {
200
+
idx
201
+
},
202
+
})
203
+
| Schematic({schematic}) => Schematic({schematic: schematic})
204
+
| Lam({name, body}) => Lam({name, body: upshift(body, amount, ~from=from + 1)})
155
205
| App({func, arg}) =>
156
-
App({func: discharge(subst, func, ~prune), arg: discharge(subst, arg, ~prune)})
157
-
// Lam case is not actually needed by FCU
158
-
| Lam({name, body}) => Lam({name, body: discharge(upshift_tt(subst), body, ~prune)})
159
-
| Var(_) if prune => Unallowed
160
-
| Var(_) | Schematic(_) | Symbol(_) | Unallowed => term
206
+
App({func: upshift(func, amount, ~from), arg: upshift(arg, amount, ~from)})
207
+
| Unallowed => Unallowed
208
+
}
209
+
let downshift = (term: t, amount: int, ~from: int=1) => {
210
+
if amount > from {
211
+
throw(Util.Err("downshift amount must be less than from"))
161
212
}
213
+
upshift(term, -amount, ~from)
214
+
}
215
+
let lookup = (term: t, subst: array<(t, t)>): option<t> => {
216
+
subst
217
+
->Array.find(((from, _)) => equivalent(term, from))
218
+
->Option.map(((_, to)) => to)
162
219
}
163
-
}
164
-
let emptySubst: subst = Belt.Map.Int.empty
165
-
let substAdd = (subst: subst, schematic: schematic, term: t) => {
166
-
assert(schematic >= 0)
167
-
assert(subst->Belt.Map.Int.has(schematic) == false)
168
-
subst->Belt.Map.Int.set(schematic, term)
169
-
}
170
-
let rec substitute = (term: t, subst: subst) =>
171
-
switch term {
172
-
| Schematic({schematic, _}) =>
173
-
switch Belt.Map.Int.get(subst, schematic) {
174
-
| None => term
220
+
let upshift_tt = (subst: array<(t, t)>, ~amount: int=1): array<(t, t)> => {
221
+
subst->Array.map(((a, b)) => (upshift(a, amount), upshift(b, amount)))
222
+
}
223
+
// where pattern unification used mapbind we will need to use discharge for FCU
224
+
//
225
+
// When `prune` is true, it marks “dead” variables as Unallowed. Nipkow 1993 uses Var(-infinity) for this in the de Bruijn’s notation implementation.
226
+
// Nipkow 1993's non de Bruijn implementation handle this logic in `proj`. Similarly Makoto Hamana's paper uses `elem` and `subst` in `prune`
227
+
let rec discharge = (subst: array<(t, t)>, term: t, ~prune: bool): t => {
228
+
switch lookup(term, subst) {
175
229
| Some(found) => found
230
+
| None =>
231
+
switch term {
232
+
| App({func, arg}) =>
233
+
App({func: discharge(subst, func, ~prune), arg: discharge(subst, arg, ~prune)})
234
+
// Lam case is not actually needed by FCU
235
+
| Lam({name, body}) => Lam({name, body: discharge(upshift_tt(subst), body, ~prune)})
236
+
| Var(_) if prune => Unallowed
237
+
| Var(_) | Schematic(_) | Symbol(_) | Unallowed => term
238
+
}
176
239
}
177
-
| Lam({name, body}) =>
178
-
Lam({
179
-
name,
180
-
// upshift is not needed for pattern unification, but it is safer to have upshift here
181
-
body: substitute(body, subst->Belt.Map.Int.map(t => upshift(t, 1))),
182
-
})
183
-
| App({func, arg}) =>
184
-
App({
185
-
func: substitute(func, subst),
186
-
arg: substitute(arg, subst),
187
-
})
188
-
| Var(_) | Unallowed | Symbol(_) => term
189
240
}
241
+
let emptySubst: subst = Belt.Map.Int.empty
242
+
let substAdd = (subst: subst, schematic: schematic, term: t) => {
243
+
assert(schematic >= 0)
244
+
assert(subst->Belt.Map.Int.has(schematic) == false)
245
+
subst->Belt.Map.Int.set(schematic, term)
246
+
}
247
+
let rec substitute = (term: t, subst: subst) =>
248
+
switch term {
249
+
| Schematic({schematic, _}) =>
250
+
switch Belt.Map.Int.get(subst, schematic) {
251
+
| None => term
252
+
| Some(found) => found
253
+
}
254
+
| Lam({name, body}) =>
255
+
Lam({
256
+
name,
257
+
// upshift is not needed for pattern unification, but it is safer to have upshift here
258
+
body: substitute(body, subst->Belt.Map.Int.map(t => upshift(t, 1))),
259
+
})
260
+
| App({func, arg}) =>
261
+
App({
262
+
func: substitute(func, subst),
263
+
arg: substitute(arg, subst),
264
+
})
265
+
| Symbol({name, constructor}) => {
266
+
let symbolSubst = subst->Belt.Map.Int.reduce(Map.make(), (acc, k, v) => {
267
+
switch v {
268
+
| Symbol({name}) => {
269
+
acc->Map.set(k, name)
270
+
acc
271
+
}
272
+
| _ => acc
273
+
}
274
+
})
275
+
Symbol({name: Atom.substitute(name, symbolSubst), constructor})
276
+
}
277
+
| Var(_) | Unallowed => term
278
+
}
190
279
191
-
let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
192
-
switch term {
193
-
| Symbol(_) => term
194
-
| Var({idx: var}) =>
195
-
if var < from {
280
+
let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
281
+
switch term {
282
+
| Symbol({name, constructor}) =>
283
+
Symbol({
284
+
name: Atom.substDeBruijn(
285
+
name,
286
+
substs->Array.map(t =>
287
+
switch t {
288
+
| Symbol({name}) => Some(name)
289
+
| _ => None
290
+
}
291
+
),
292
+
~from,
293
+
),
294
+
constructor,
295
+
})
296
+
| Var({idx: var}) =>
297
+
if var < from {
298
+
term
299
+
} else if var - from < Array.length(substs) && var - from >= 0 {
300
+
Option.getExn(substs[var - from])
301
+
} else {
302
+
Var({idx: var - Array.length(substs)})
303
+
}
304
+
| Schematic({schematic}) =>
305
+
Schematic({
306
+
schematic: schematic,
307
+
})
308
+
| Lam({name, body}) =>
309
+
Lam({
310
+
name,
311
+
body: substDeBruijn(body, substs->Array.map(term => upshift(term, 1)), ~from=from + 1),
312
+
})
313
+
| App({func, arg}) =>
314
+
App({
315
+
func: substDeBruijn(func, substs, ~from),
316
+
arg: substDeBruijn(arg, substs, ~from),
317
+
})
318
+
| Unallowed => Unallowed
319
+
}
320
+
// beta reduced and eta reduced
321
+
let rec reduce = (term: t): t => {
322
+
switch term {
323
+
| Lam({body: App({func, arg: Var({idx: 0})})}) if !(func->freeVarsContains(emptySubst, 0)) =>
324
+
reduce(downshift(func, 1))
325
+
| App({func, arg}) =>
326
+
switch reduce(func) {
327
+
| Lam({body}) => reduce(substDeBruijn(body, [arg]))
328
+
| func => App({func, arg: reduce(arg)})
329
+
}
330
+
| Lam({name, body}) =>
331
+
Lam({
332
+
name,
333
+
body: reduce(body),
334
+
})
335
+
| Symbol(_) | Var(_) | Schematic(_) => term
336
+
337
+
| Unallowed => Unallowed
338
+
}
339
+
}
340
+
let reduceSubst = (subst: subst): subst => {
341
+
subst->Belt.Map.Int.map(x => reduce(substitute(x, subst)))
342
+
}
343
+
let rec lams = (amount: int, term: t): t => {
344
+
assert(amount >= 0)
345
+
if amount <= 0 {
196
346
term
197
-
} else if var - from < Array.length(substs) && var - from >= 0 {
198
-
Option.getExn(substs[var - from])
347
+
} else {
348
+
Lam({
349
+
name: "x",
350
+
body: lams(amount - 1, term),
351
+
})
352
+
}
353
+
}
354
+
let rec idx = (is: array<t>, j: t): option<int> => {
355
+
if is->Array.length == 0 {
356
+
None
199
357
} else {
200
-
Var({idx: var - Array.length(substs)})
358
+
let head = is[0]->Option.getExn
359
+
let tail = is->Array.sliceToEnd(~start=1)
360
+
if equivalent(head, j) {
361
+
Some(tail->Array.length)
362
+
} else {
363
+
idx(tail, j)
364
+
}
201
365
}
202
-
| Schematic({schematic}) =>
203
-
Schematic({
204
-
schematic: schematic,
205
-
})
206
-
| Lam({name, body}) =>
207
-
Lam({
208
-
name,
209
-
body: substDeBruijn(body, substs->Array.map(term => upshift(term, 1)), ~from=from + 1),
210
-
})
211
-
| App({func, arg}) =>
212
-
App({
213
-
func: substDeBruijn(func, substs, ~from),
214
-
arg: substDeBruijn(arg, substs, ~from),
215
-
})
216
-
| Unallowed => Unallowed
217
366
}
218
-
// beta reduced and eta reduced
219
-
let rec reduce = (term: t): t => {
220
-
switch term {
221
-
| Lam({body: App({func, arg: Var({idx: 0})})}) if !(func->freeVarsContains(emptySubst, 0)) =>
222
-
reduce(downshift(func, 1))
223
-
| App({func, arg}) =>
224
-
switch reduce(func) {
225
-
| Lam({body}) => reduce(substDeBruijn(body, [arg]))
226
-
| func => App({func, arg: reduce(arg)})
367
+
let idx1' = (is: array<t>, j: t): t => {
368
+
switch idx(is, j) {
369
+
| None => Unallowed
370
+
| Some(idx) => Var({idx: idx})
227
371
}
228
-
| Lam({name, body}) =>
229
-
Lam({
230
-
name,
231
-
body: reduce(body),
232
-
})
233
-
| Symbol(_) | Var(_) | Schematic(_) => term
234
-
235
-
| Unallowed => Unallowed
236
372
}
237
-
}
238
-
let reduceSubst = (subst: subst): subst => {
239
-
subst->Belt.Map.Int.map(x => reduce(substitute(x, subst)))
240
-
}
241
-
let rec lams = (amount: int, term: t): t => {
242
-
assert(amount >= 0)
243
-
if amount <= 0 {
244
-
term
245
-
} else {
246
-
Lam({
247
-
name: "x",
248
-
body: lams(amount - 1, term),
249
-
})
373
+
let _idx1 = (is: array<t>, j: int): t => idx1'(is, Var({idx: j}))
374
+
let idx2' = (is: array<t>, j: t): result<int, int => t> => {
375
+
switch idx(is, j) {
376
+
| None => Error(_ => Unallowed)
377
+
| Some(idx) => Ok(idx)
378
+
}
250
379
}
251
-
}
252
-
let rec idx = (is: array<t>, j: t): option<int> => {
253
-
if is->Array.length == 0 {
254
-
None
255
-
} else {
256
-
let head = is[0]->Option.getExn
257
-
let tail = is->Array.sliceToEnd(~start=1)
258
-
if equivalent(head, j) {
259
-
Some(tail->Array.length)
380
+
let _idx2 = (is: array<t>, j: int) => idx2'(is, Var({idx: j}))
381
+
let rec app = (term: t, args: array<t>): t => {
382
+
if args->Array.length == 0 {
383
+
term
260
384
} else {
261
-
idx(tail, j)
385
+
let head = args[0]->Option.getExn
386
+
let rest = args->Array.sliceToEnd(~start=1)
387
+
app(App({func: term, arg: head}), rest)
262
388
}
263
389
}
264
-
}
265
-
let idx1' = (is: array<t>, j: t): t => {
266
-
switch idx(is, j) {
267
-
| None => Unallowed
268
-
| Some(idx) => Var({idx: idx})
390
+
exception UnifyFail(string)
391
+
let rec red = (term: t, is: array<t>): t => {
392
+
switch term {
393
+
| _ if is->Array.length == 0 => term
394
+
| Lam({body}) =>
395
+
red(substDeBruijn(body, [is[0]->Option.getExn]), is->Array.sliceToEnd(~start=1))
396
+
| term => app(term, is)
397
+
}
269
398
}
270
-
}
271
-
let _idx1 = (is: array<t>, j: int): t => idx1'(is, Var({idx: j}))
272
-
let idx2' = (is: array<t>, j: t): result<int, int => t> => {
273
-
switch idx(is, j) {
274
-
| None => Error(_ => Unallowed)
275
-
| Some(idx) => Ok(idx)
399
+
let lam = (is: array<t>, g: t, js: array<t>): t => {
400
+
lams(is->Array.length, app(g, js->Array.map(j => idx1'(is, j))))
276
401
}
277
-
}
278
-
let _idx2 = (is: array<t>, j: int) => idx2'(is, Var({idx: j}))
279
-
let rec app = (term: t, args: array<t>): t => {
280
-
if args->Array.length == 0 {
281
-
term
282
-
} else {
283
-
let head = args[0]->Option.getExn
284
-
let rest = args->Array.sliceToEnd(~start=1)
285
-
app(App({func: term, arg: head}), rest)
402
+
let rec strip = (term: t): (t, array<t>) => {
403
+
switch term {
404
+
| App({func, arg}) =>
405
+
let (peeledFunc, peeledArgs) = strip(func)
406
+
(peeledFunc, Array.concat(peeledArgs, [arg]))
407
+
| _ => (term, [])
408
+
}
286
409
}
287
-
}
288
-
exception UnifyFail(string)
289
-
let rec red = (term: t, is: array<t>): t => {
290
-
switch term {
291
-
| _ if is->Array.length == 0 => term
292
-
| Lam({body}) => red(substDeBruijn(body, [is[0]->Option.getExn]), is->Array.sliceToEnd(~start=1))
293
-
| term => app(term, is)
410
+
let rec devar = (subst: subst, term: t): t => {
411
+
let (func, args) = strip(term)
412
+
switch func {
413
+
| Schematic({schematic}) if substHas(subst, schematic) =>
414
+
devar(subst, red(substGet(subst, schematic)->Option.getExn, args))
415
+
| _ => term
416
+
}
294
417
}
295
-
}
296
-
let lam = (is: array<t>, g: t, js: array<t>): t => {
297
-
lams(is->Array.length, app(g, js->Array.map(j => idx1'(is, j))))
298
-
}
299
-
let rec strip = (term: t): (t, array<t>) => {
300
-
switch term {
301
-
| App({func, arg}) =>
302
-
let (peeledFunc, peeledArgs) = strip(func)
303
-
(peeledFunc, Array.concat(peeledArgs, [arg]))
304
-
| _ => (term, [])
418
+
let mkvars = (n: int): array<t> => {
419
+
Belt.Array.init(n, i => n - i - 1)->Array.map(x => Var({idx: x}))
305
420
}
306
-
}
307
-
let rec devar = (subst: subst, term: t): t => {
308
-
let (func, args) = strip(term)
309
-
switch func {
310
-
| Schematic({schematic}) if substHas(subst, schematic) =>
311
-
devar(subst, red(substGet(subst, schematic)->Option.getExn, args))
312
-
| _ => term
421
+
let rec proj_allowed = (subst: subst, term: t): bool => {
422
+
let term' = devar(subst, term)
423
+
switch term' {
424
+
| Lam(_) | Unallowed | Schematic(_) | Symbol(_) => false
425
+
| Var(_) => true // pattern unification only allows this
426
+
// FCU allows this:
427
+
| App(_) =>
428
+
switch strip(term') {
429
+
| (Symbol(_) | Var(_), args) => Array.every(args, x => proj_allowed(subst, x))
430
+
| _ => false
431
+
}
432
+
}
313
433
}
314
-
}
315
-
let mkvars = (n: int): array<t> => {
316
-
Belt.Array.init(n, i => n - i - 1)->Array.map(x => Var({idx: x}))
317
-
}
318
-
let rec proj_allowed = (subst: subst, term: t): bool => {
319
-
let term' = devar(subst, term)
320
-
switch term' {
321
-
| Lam(_) | Unallowed | Schematic(_) | Symbol(_) => false
322
-
| Var(_) => true // pattern unification only allows this
323
-
// FCU allows this:
324
-
| App(_) =>
325
-
switch strip(term') {
326
-
| (Symbol(_) | Var(_), args) => Array.every(args, x => proj_allowed(subst, x))
327
-
| _ => false
434
+
// this function is called proj in Nipkow 1993 and it is called pruning in FCU paper
435
+
let rec proj = (subst: subst, term: t, ~gen: option<gen>): subst => {
436
+
switch strip(devar(subst, term)) {
437
+
| (Lam({name: _, body}), args) if args->Array.length == 0 => proj(subst, body, ~gen)
438
+
| (Unallowed, _args) => throw(UnifyFail("unallowed"))
439
+
| (Symbol(_) | Var(_), args) => Array.reduce(args, subst, (acc, a) => proj(acc, a, ~gen))
440
+
| (Schematic({schematic}), args) => {
441
+
assert(!substHas(subst, schematic))
442
+
if gen->Option.isNone {
443
+
throw(UnifyFail("no gen provided"))
444
+
}
445
+
let h = Schematic({schematic: fresh(Option.getExn(gen))})
446
+
subst->substAdd(
447
+
schematic,
448
+
lams(
449
+
args->Array.length,
450
+
app(
451
+
h,
452
+
Belt.Array.init(args->Array.length, j => {
453
+
if proj_allowed(subst, args[j]->Option.getExn) {
454
+
Some(Var({idx: args->Belt.Array.length - j - 1}))
455
+
} else {
456
+
None
457
+
}
458
+
})->Array.keepSome,
459
+
),
460
+
),
461
+
)
462
+
}
463
+
| _ => throw(UnifyFail("not a symbol, var or schematic"))
328
464
}
329
465
}
330
-
}
331
-
// this function is called proj in Nipkow 1993 and it is called pruning in FCU paper
332
-
let rec proj = (subst: subst, term: t, ~gen: option<gen>): subst => {
333
-
switch strip(devar(subst, term)) {
334
-
| (Lam({name: _, body}), args) if args->Array.length == 0 => proj(subst, body, ~gen)
335
-
| (Unallowed, _args) => throw(UnifyFail("unallowed"))
336
-
| (Symbol(_) | Var(_), args) => Array.reduce(args, subst, (acc, a) => proj(acc, a, ~gen))
337
-
| (Schematic({schematic}), args) => {
338
-
assert(!substHas(subst, schematic))
339
-
if gen->Option.isNone {
340
-
throw(UnifyFail("no gen provided"))
466
+
let flexflex = (
467
+
sa: schematic,
468
+
xs: array<t>,
469
+
sb: schematic,
470
+
ys: array<t>,
471
+
subst: subst,
472
+
~gen: option<gen>,
473
+
): subst => {
474
+
if gen->Option.isNone {
475
+
throw(UnifyFail("no gen provided"))
476
+
}
477
+
if sa == sb {
478
+
if xs->Array.length != ys->Array.length {
479
+
throw(UnifyFail("flexible schematics have different number of arguments"))
341
480
}
481
+
let len = xs->Array.length
342
482
let h = Schematic({schematic: fresh(Option.getExn(gen))})
343
-
subst->substAdd(
344
-
schematic,
345
-
lams(
346
-
args->Array.length,
347
-
app(
348
-
h,
349
-
Belt.Array.init(args->Array.length, j => {
350
-
if proj_allowed(subst, args[j]->Option.getExn) {
351
-
Some(Var({idx: args->Belt.Array.length - j - 1}))
352
-
} else {
353
-
None
354
-
}
355
-
})->Array.keepSome,
356
-
),
357
-
),
358
-
)
483
+
let xs = Belt.Array.init(len, k => {
484
+
let a = xs[k]->Option.getExn
485
+
let b = ys[k]->Option.getExn
486
+
if equivalent(a, b) {
487
+
Some(Var({idx: len - k - 1}))
488
+
} else {
489
+
None
490
+
}
491
+
})->Array.keepSome
492
+
subst->substAdd(sa, lams(len, app(h, xs)))
493
+
} else {
494
+
let common = xs->Array.filter(x => ys->Belt.Array.some(y => equivalent(x, y)))
495
+
let h = Schematic({schematic: fresh(Option.getExn(gen))})
496
+
subst->substAdd(sa, lam(xs, h, common))->substAdd(sb, lam(ys, h, common))
359
497
}
360
-
| _ => throw(UnifyFail("not a symbol, var or schematic"))
361
498
}
362
-
}
363
-
let flexflex = (
364
-
sa: schematic,
365
-
xs: array<t>,
366
-
sb: schematic,
367
-
ys: array<t>,
368
-
subst: subst,
369
-
~gen: option<gen>,
370
-
): subst => {
371
-
if gen->Option.isNone {
372
-
throw(UnifyFail("no gen provided"))
499
+
let flexrigid = (sa: schematic, xs: array<t>, b: t, subst: subst, ~gen: option<gen>): subst => {
500
+
if occ(sa, subst, b) {
501
+
throw(UnifyFail("flexible schematic occurs in rigid term"))
502
+
}
503
+
// pattern unification
504
+
// let u = b->_mapbind0(bind => idx2(xs, bind))
505
+
// FCU
506
+
let zn = mkvars(xs->Array.length)
507
+
// we reversed it so that the last one will be picked if there are duplicates. This behaviour helps certain real world cases.
508
+
let u = discharge(Belt.Array.reverse(Belt.Array.zip(xs, zn)), b, ~prune=true)
509
+
proj(subst->substAdd(sa, lams(xs->Array.length, u)), u, ~gen)
373
510
}
374
-
if sa == sb {
375
-
if xs->Array.length != ys->Array.length {
376
-
throw(UnifyFail("flexible schematics have different number of arguments"))
377
-
}
378
-
let len = xs->Array.length
379
-
let h = Schematic({schematic: fresh(Option.getExn(gen))})
380
-
let xs = Belt.Array.init(len, k => {
381
-
let a = xs[k]->Option.getExn
382
-
let b = ys[k]->Option.getExn
383
-
if equivalent(a, b) {
384
-
Some(Var({idx: len - k - 1}))
511
+
let rec integrateAtomSubst = (atomSubst: Atom.subst, subst: subst, ~gen: option<gen>): subst =>
512
+
atomSubst
513
+
->Map.entries
514
+
->Iterator.toArray
515
+
->Array.reduce(subst, (acc, (schematic, term)) =>
516
+
if acc->substHas(schematic) {
517
+
unifyTermFirst(
518
+
acc->substGet(schematic)->Option.getExn,
519
+
Symbol({name: term, constructor: false}),
520
+
acc,
521
+
~gen,
522
+
)
385
523
} else {
386
-
None
524
+
acc->substAdd(schematic, Symbol({name: term, constructor: false}))
387
525
}
388
-
})->Array.keepSome
389
-
subst->substAdd(sa, lams(len, app(h, xs)))
390
-
} else {
391
-
let common = xs->Array.filter(x => ys->Belt.Array.some(y => equivalent(x, y)))
392
-
let h = Schematic({schematic: fresh(Option.getExn(gen))})
393
-
subst->substAdd(sa, lam(xs, h, common))->substAdd(sb, lam(ys, h, common))
394
-
}
395
-
}
396
-
let flexrigid = (sa: schematic, xs: array<t>, b: t, subst: subst, ~gen: option<gen>): subst => {
397
-
if occ(sa, subst, b) {
398
-
throw(UnifyFail("flexible schematic occurs in rigid term"))
399
-
}
400
-
// pattern unification
401
-
// let u = b->mapbind0(bind => idx2(xs, bind))
402
-
// FCU
403
-
let zn = mkvars(xs->Array.length)
404
-
// we reversed it so that the last one will be picked if there are duplicates. This behaviour helps certain real world cases.
405
-
let u = discharge(Belt.Array.reverse(Belt.Array.zip(xs, zn)), b, ~prune=true)
406
-
proj(subst->substAdd(sa, lams(xs->Array.length, u)), u, ~gen)
407
-
}
408
-
let rec unifyTerm = (a: t, b: t, subst: subst, ~gen: option<gen>): subst =>
409
-
switch (devar(subst, a), devar(subst, b)) {
410
-
| (Symbol({name: na}), Symbol({name: nb})) =>
411
-
if na == nb {
412
-
subst
413
-
} else {
414
-
throw(UnifyFail("symbols do not match"))
526
+
)
527
+
and unifyAtom = (a: Atom.t, b: Atom.t, subst: subst, ~gen: option<gen>): Seq.t<subst> =>
528
+
Atom.unify(a, b)->Seq.filterMap(atomSubst =>
529
+
try {
530
+
Some(integrateAtomSubst(atomSubst, subst, ~gen))
531
+
} catch {
532
+
| UnifyFail(_) => None
533
+
}
534
+
)
535
+
and unifyTerm = (a: t, b: t, subst: subst, ~gen: option<gen>): Seq.t<subst> =>
536
+
switch (devar(subst, a), devar(subst, b)) {
537
+
| (Symbol({name: a}), Symbol({name: b})) => unifyAtom(a, b, subst, ~gen)
538
+
| (Var({idx: ia}), Var({idx: ib})) =>
539
+
if ia == ib {
540
+
Seq.once(subst)
541
+
} else {
542
+
Seq.empty
543
+
}
544
+
| (Schematic({schematic: sa}), Schematic({schematic: sb})) if sa == sb => Seq.once(subst)
545
+
| (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => unifyTerm(ba, bb, subst, ~gen)
546
+
| (Lam({name: _, body: ba}), b) =>
547
+
unifyTerm(ba, App({func: upshift(b, 1), arg: Var({idx: 0})}), subst, ~gen)
548
+
| (a, Lam({name: _, body: bb})) =>
549
+
unifyTerm(App({func: upshift(a, 1), arg: Var({idx: 0})}), bb, subst, ~gen)
550
+
| (a, b) =>
551
+
switch (strip(a), strip(b)) {
552
+
| ((Schematic({schematic: sa}), xs), (Schematic({schematic: sb}), ys)) =>
553
+
try {
554
+
Seq.once(flexflex(sa, xs, sb, ys, subst, ~gen))
555
+
} catch {
556
+
| UnifyFail(_) => Seq.empty
557
+
}
558
+
| ((Schematic({schematic: sa}), xs), _) =>
559
+
try {
560
+
Seq.once(flexrigid(sa, xs, b, subst, ~gen))
561
+
} catch {
562
+
| UnifyFail(_) => Seq.empty
563
+
}
564
+
| (_, (Schematic({schematic: sb}), ys)) =>
565
+
try {
566
+
Seq.once(flexrigid(sb, ys, a, subst, ~gen))
567
+
} catch {
568
+
| UnifyFail(_) => Seq.empty
569
+
}
570
+
| ((a, xs), (b, ys)) =>
571
+
switch (a, b) {
572
+
| (Symbol(_) | Var(_), Symbol(_) | Var(_)) =>
573
+
unifyTerm(a, b, subst, ~gen)->Seq.flatMap(subst => unifyArray(xs, ys, subst, ~gen))
574
+
| _ => Seq.empty
575
+
}
576
+
}
415
577
}
416
-
| (Var({idx: ia}), Var({idx: ib})) =>
417
-
if ia == ib {
418
-
subst
578
+
and unifyArray = (xs: array<t>, ys: array<t>, subst: subst, ~gen: option<gen>): Seq.t<subst> => {
579
+
if xs->Array.length != ys->Array.length {
580
+
Seq.empty
581
+
} else if xs->Array.length == 0 {
582
+
Seq.once(subst)
419
583
} else {
420
-
throw(UnifyFail("variables do not match"))
584
+
let x = xs[0]->Option.getExn
585
+
let y = ys[0]->Option.getExn
586
+
let restXs = xs->Array.sliceToEnd(~start=1)
587
+
let restYs = ys->Array.sliceToEnd(~start=1)
588
+
unifyTerm(x, y, subst, ~gen)->Seq.flatMap(subst => unifyArray(restXs, restYs, subst, ~gen))
421
589
}
422
-
| (Schematic({schematic: sa}), Schematic({schematic: sb})) if sa == sb => subst
423
-
| (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => unifyTerm(ba, bb, subst, ~gen)
424
-
| (Lam({name: _, body: ba}), b) =>
425
-
unifyTerm(ba, App({func: upshift(b, 1), arg: Var({idx: 0})}), subst, ~gen)
426
-
| (a, Lam({name: _, body: bb})) =>
427
-
unifyTerm(App({func: upshift(a, 1), arg: Var({idx: 0})}), bb, subst, ~gen)
428
-
| (a, b) =>
429
-
switch (strip(a), strip(b)) {
430
-
| ((Schematic({schematic: sa}), xs), (Schematic({schematic: sb}), ys)) =>
431
-
flexflex(sa, xs, sb, ys, subst, ~gen)
432
-
| ((Schematic({schematic: sa}), xs), _) => flexrigid(sa, xs, b, subst, ~gen)
433
-
| (_, (Schematic({schematic: sb}), ys)) => flexrigid(sb, ys, a, subst, ~gen)
434
-
| ((a, xs), (b, ys)) =>
435
-
switch (a, b) {
436
-
| (Symbol(_) | Var(_), Symbol(_) | Var(_)) => rigidrigid(a, xs, b, ys, subst, ~gen)
590
+
}
591
+
and unifyTermFirst = (a: t, b: t, subst: subst, ~gen: option<gen>): subst =>
592
+
switch unifyTerm(a, b, subst, ~gen)->Seq.head {
593
+
| Some(subst) => subst
594
+
| None =>
595
+
switch (devar(subst, a), devar(subst, b)) {
596
+
| (Symbol(_), Symbol(_)) => throw(UnifyFail("symbols do not match"))
597
+
| (Var(_), Var(_)) => throw(UnifyFail("variables do not match"))
437
598
| _ => throw(UnifyFail("no rules match"))
438
599
}
439
600
}
440
-
}
441
-
and unifyArray = (xs: array<t>, ys: array<t>, subst: subst, ~gen: option<gen>): subst => {
442
-
if xs->Array.length != ys->Array.length {
443
-
throw(UnifyFail("arrays have different lengths"))
444
-
}
445
-
Belt.Array.zip(xs, ys)->Belt.Array.reduce(subst, (acc, (x, y)) => unifyTerm(x, y, acc, ~gen))
446
-
}
447
-
and rigidrigid = (
448
-
a: t,
449
-
xs: array<t>,
450
-
b: t,
451
-
ys: array<t>,
452
-
subst: subst,
453
-
~gen: option<gen>,
454
-
): subst => {
455
-
if !equivalent(a, b) {
456
-
throw(UnifyFail("rigid terms do not match"))
457
-
}
458
-
if xs->Array.length != ys->Array.length {
459
-
throw(UnifyFail("rigid terms have different number of arguments"))
460
-
}
461
-
unifyArray(xs, ys, subst, ~gen)
462
-
}
463
-
let unify = (a: t, b: t, ~gen=?) =>
464
-
Seq.fromArray(
601
+
let unify = (a: t, b: t, ~gen=?) => unifyTerm(a, b, emptySubst, ~gen)
602
+
let rec rewrite = (term: t, from: t, to: t, ~subst: subst, ~gen: option<gen>): (subst, t) => {
465
603
try {
466
-
[unifyTerm(a, b, emptySubst, ~gen)]
604
+
let subst1 = unifyTermFirst(term, from, subst, ~gen)
605
+
(subst1, to)
467
606
} catch {
468
-
| UnifyFail(_) => []
469
-
},
470
-
)
471
-
let rec rewrite = (term: t, from: t, to: t, ~subst: subst, ~gen: option<gen>): (subst, t) => {
472
-
try {
473
-
let subst1 = unifyTerm(term, from, subst, ~gen)
474
-
(subst1, to)
475
-
} catch {
476
-
| UnifyFail(_) =>
477
-
switch term {
478
-
| Schematic({schematic}) if subst->substHas(schematic) =>
479
-
rewrite(subst->substGet(schematic)->Option.getExn, from, to, ~subst, ~gen)
480
-
| Var(_) | Unallowed | Symbol(_) | Schematic(_) => (subst, term)
481
-
| Lam({name, body}) => {
482
-
let (subst1, body1) = rewrite(body, from, to, ~subst, ~gen)
483
-
(subst1, Lam({name, body: body1}))
484
-
}
485
-
| App({func, arg}) => {
486
-
let (subst1, func') = rewrite(func, from, to, ~subst, ~gen)
487
-
let (subst2, arg') = rewrite(arg, from, to, ~subst=subst1, ~gen)
488
-
(subst2, App({func: func', arg: arg'}))
607
+
| UnifyFail(_) =>
608
+
switch term {
609
+
| Schematic({schematic}) if subst->substHas(schematic) =>
610
+
rewrite(subst->substGet(schematic)->Option.getExn, from, to, ~subst, ~gen)
611
+
| Var(_) | Unallowed | Symbol(_) | Schematic(_) => (subst, term)
612
+
| Lam({name, body}) => {
613
+
let (subst1, body1) = rewrite(body, from, to, ~subst, ~gen)
614
+
(subst1, Lam({name, body: body1}))
615
+
}
616
+
| App({func, arg}) => {
617
+
let (subst1, func') = rewrite(func, from, to, ~subst, ~gen)
618
+
let (subst2, arg') = rewrite(arg, from, to, ~subst=subst1, ~gen)
619
+
(subst2, App({func: func', arg: arg'}))
620
+
}
489
621
}
490
622
}
491
623
}
492
-
}
493
-
let place = (x: int, ~scope: array<string>) =>
494
-
app(
495
-
Schematic({
496
-
schematic: x,
497
-
}),
498
-
Array.fromInitializer(~length=Array.length(scope), i => Var({idx: i})),
499
-
)
624
+
let place = (x: int, ~scope: array<string>) =>
625
+
app(
626
+
Schematic({
627
+
schematic: x,
628
+
}),
629
+
Array.fromInitializer(~length=Array.length(scope), i => Var({idx: i})),
630
+
)
500
631
501
-
let prettyPrintVar = (idx: int, scope: array<string>) =>
502
-
switch scope[idx] {
503
-
| Some(n) if Array.indexOf(scope, n) == idx => n
504
-
| _ => "\\"->String.concat(String.make(idx))
632
+
let prettyPrintVar = (idx: int, scope: array<string>) =>
633
+
switch scope[idx] {
634
+
| Some(n) if Array.indexOf(scope, n) == idx => n
635
+
| _ => "\\"->String.concat(String.make(idx))
636
+
}
637
+
let makeGen = () => {
638
+
ref(0)
505
639
}
506
-
let makeGen = () => {
507
-
ref(0)
508
-
}
509
-
let rec stripLam = (it: t): (array<string>, t) =>
510
-
switch it {
511
-
| Lam({name, body}) =>
512
-
let (names, body) = stripLam(body)
513
-
(Array.concat([name], names), body)
514
-
| _ => ([], it)
515
-
}
516
-
let rec prettyPrint = (it: t, ~scope: array<string>) =>
517
-
switch it {
518
-
| Symbol({name, constructor}) =>
519
-
if constructor {
520
-
String.concat("@", name)
521
-
} else {
522
-
name
640
+
let rec stripLam = (it: t): (array<string>, t) =>
641
+
switch it {
642
+
| Lam({name, body}) =>
643
+
let (names, body) = stripLam(body)
644
+
(Array.concat([name], names), body)
645
+
| _ => ([], it)
646
+
}
647
+
let rec prettyPrint = (it: t, ~scope: array<string>) =>
648
+
switch it {
649
+
| Symbol({name, constructor}) =>
650
+
if constructor {
651
+
String.concat("@", Atom.prettyPrint(name, ~scope))
652
+
} else {
653
+
Atom.prettyPrint(name, ~scope)
654
+
}
655
+
| Var({idx}) => prettyPrintVar(idx, scope)
656
+
| Schematic({schematic}) => "?"->String.concat(String.make(schematic))
657
+
| Lam(_) =>
658
+
let (names, body) = stripLam(it)
659
+
let (func, args) = strip(body)
660
+
let bodies = Array.concat([func], args)
661
+
let innerScope = Array.concat(Array.toReversed(names), scope)
662
+
"("
663
+
->String.concat(Array.join(names->Array.map(name => String.concat(name, ".")), " "))
664
+
->String.concat(" ")
665
+
->String.concat(Array.join(bodies->Array.map(e => prettyPrint(e, ~scope=innerScope)), " "))
666
+
->String.concat(")")
667
+
| App(_) =>
668
+
let (func, args) = strip(it)
669
+
"("
670
+
->String.concat(prettyPrint(func, ~scope))
671
+
->String.concat(" ")
672
+
->String.concat(Array.join(args->Array.map(e => prettyPrint(e, ~scope)), " "))
673
+
->String.concat(")")
674
+
| Unallowed => ""
675
+
}
676
+
let prettyPrintSubst = (sub: subst, ~scope: array<string>) =>
677
+
Util.prettyPrintIntMap(sub, ~showV=t => prettyPrint(t, ~scope))
678
+
let nameRES = "^([^\\s.\\[\\]()]+)\\."
679
+
exception ParseError(string)
680
+
type token =
681
+
| LParen
682
+
| RParen
683
+
| VarT(int)
684
+
| SchematicT(int)
685
+
| AtomT(Atom.t)
686
+
| ConsT(Atom.t)
687
+
| NameT(string)
688
+
| EOF
689
+
let varRegexpString = "^\\\\([0-9]+)"
690
+
let schematicRegexpString = "^\\?([0-9]+)"
691
+
let atomToken = (str: string, ~scope: array<string>, ~gen=?) => {
692
+
switch Atom.parse(str, ~scope, ~gen?) {
693
+
| Ok((atom, rest)) => (atom, rest)
694
+
| Error(msg) => throw(ParseError(msg))
523
695
}
524
-
| Var({idx}) => prettyPrintVar(idx, scope)
525
-
| Schematic({schematic}) => "?"->String.concat(String.make(schematic))
526
-
| Lam(_) =>
527
-
let (names, body) = stripLam(it)
528
-
let (func, args) = strip(body)
529
-
let bodies = Array.concat([func], args)
530
-
let innerScope = Array.concat(Array.toReversed(names), scope)
531
-
"("
532
-
->String.concat(Array.join(names->Array.map(name => String.concat(name, ".")), " "))
533
-
->String.concat(" ")
534
-
->String.concat(Array.join(bodies->Array.map(e => prettyPrint(e, ~scope=innerScope)), " "))
535
-
->String.concat(")")
536
-
| App(_) =>
537
-
let (func, args) = strip(it)
538
-
"("
539
-
->String.concat(prettyPrint(func, ~scope))
540
-
->String.concat(" ")
541
-
->String.concat(Array.join(args->Array.map(e => prettyPrint(e, ~scope)), " "))
542
-
->String.concat(")")
543
-
| Unallowed => ""
544
696
}
545
-
let prettyPrintSubst = (sub: subst, ~scope: array<string>) =>
546
-
Util.prettyPrintIntMap(sub, ~showV=t => prettyPrint(t, ~scope))
547
-
let symbolRegexpString = "^([^\\s()]+)"
548
-
let nameRES = "^([^\\s.\\[\\]()]+)\\."
549
-
exception ParseError(string)
550
-
type token =
551
-
| LParen
552
-
| RParen
553
-
| VarT(int)
554
-
| SchematicT(int)
555
-
| AtomT(string)
556
-
| ConsT(string)
557
-
| NameT(string)
558
-
| EOF
559
-
let varRegexpString = "^\\\\([0-9]+)"
560
-
let schematicRegexpString = "^\\?([0-9]+)"
561
-
let tokenize = (str0: string): (token, string) => {
562
-
let str = str0->String.trimStart
563
-
if str->String.length == 0 {
564
-
(EOF, "")
565
-
} else {
566
-
let rest = () => str->String.sliceToEnd(~start=1)
567
-
switch str->String.charAt(0) {
568
-
| "(" => (LParen, rest())
569
-
| ")" => (RParen, rest())
570
-
| "\\" => {
571
-
let re = RegExp.fromStringWithFlags(varRegexpString, ~flags="y")
572
-
switch re->RegExp.exec(str) {
573
-
| None => throw(ParseError("invalid variable"))
574
-
| Some(res) =>
575
-
switch RegExp.Result.matches(res) {
576
-
| [n] => (
577
-
VarT(n->Int.fromString->Option.getExn),
578
-
String.sliceToEnd(str, ~start=RegExp.lastIndex(re)),
579
-
)
580
-
| _ => throw(ParseError("invalid variable"))
697
+
let scopeVarToken = (str: string, scope: array<string>): option<(int, string)> => {
698
+
let result = ref(None)
699
+
scope->Array.forEachWithIndex((name, idx) => {
700
+
let len = String.length(name)
701
+
let matches =
702
+
String.slice(str, ~start=0, ~end=len) == name &&
703
+
switch str->String.charAt(len) {
704
+
| "" | " " | "\t" | "\n" | "\r" | "(" | ")" => true
705
+
| _ => false
581
706
}
582
-
}
707
+
if result.contents == None && matches {
708
+
result := Some((idx, str->String.sliceToEnd(~start=len)))
583
709
}
584
-
| "?" => {
585
-
let re = RegExp.fromStringWithFlags(schematicRegexpString, ~flags="y")
586
-
switch re->RegExp.exec(str) {
587
-
| None => throw(ParseError("invalid schematic"))
588
-
| Some(res) =>
589
-
switch RegExp.Result.matches(res) {
590
-
| [n] => (
591
-
SchematicT(n->Int.fromString->Option.getExn),
592
-
String.sliceToEnd(str, ~start=RegExp.lastIndex(re)),
593
-
)
594
-
| _ => throw(ParseError("invalid schematic"))
710
+
})
711
+
result.contents
712
+
}
713
+
let tokenize = (str0: string, ~scope: array<string>, ~gen=?): (token, string) => {
714
+
let str = str0->String.trimStart
715
+
if str->String.length == 0 {
716
+
(EOF, "")
717
+
} else {
718
+
let rest = () => str->String.sliceToEnd(~start=1)
719
+
switch str->String.charAt(0) {
720
+
| "(" => (LParen, rest())
721
+
| ")" => (RParen, rest())
722
+
| "\\" => {
723
+
let re = RegExp.fromStringWithFlags(varRegexpString, ~flags="y")
724
+
switch re->RegExp.exec(str) {
725
+
| None => throw(ParseError("invalid variable"))
726
+
| Some(res) =>
727
+
switch RegExp.Result.matches(res) {
728
+
| [n] => (
729
+
VarT(n->Int.fromString->Option.getExn),
730
+
String.sliceToEnd(str, ~start=RegExp.lastIndex(re)),
731
+
)
732
+
| _ => throw(ParseError("invalid variable"))
733
+
}
595
734
}
596
735
}
597
-
}
598
-
| "@" =>
599
-
let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
600
-
switch re->RegExp.exec(rest()) {
601
-
| None => throw(ParseError("invalid symbol"))
602
-
| Some(res) =>
603
-
switch RegExp.Result.matches(res) {
604
-
| [n] => (ConsT(n), String.sliceToEnd(rest(), ~start=RegExp.lastIndex(re)))
605
-
| _ => throw(ParseError("invalid symbol"))
606
-
}
607
-
}
608
-
| _ => {
609
-
let reName = RegExp.fromStringWithFlags(nameRES, ~flags="y")
610
-
switch reName->RegExp.exec(str) {
611
-
| Some(res) =>
612
-
switch RegExp.Result.matches(res) {
613
-
| [n] => (NameT(n), String.sliceToEnd(str, ~start=RegExp.lastIndex(reName)))
614
-
| _ => throw(ParseError("invalid symbol"))
615
-
}
616
-
| None =>
617
-
let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
736
+
| "?" => {
737
+
let re = RegExp.fromStringWithFlags(schematicRegexpString, ~flags="y")
618
738
switch re->RegExp.exec(str) {
619
-
| None => throw(ParseError("invalid symbol"))
739
+
| None => throw(ParseError("invalid schematic"))
620
740
| Some(res) =>
621
741
switch RegExp.Result.matches(res) {
622
-
| [n] => (AtomT(n), String.sliceToEnd(str, ~start=RegExp.lastIndex(re)))
742
+
| [n] => (
743
+
SchematicT(n->Int.fromString->Option.getExn),
744
+
String.sliceToEnd(str, ~start=RegExp.lastIndex(re)),
745
+
)
746
+
| _ => throw(ParseError("invalid schematic"))
747
+
}
748
+
}
749
+
}
750
+
| "@" =>
751
+
let (raw, rest) = atomToken(rest(), ~scope, ~gen?)
752
+
(ConsT(raw), rest)
753
+
| _ => {
754
+
let reName = RegExp.fromStringWithFlags(nameRES, ~flags="y")
755
+
switch reName->RegExp.exec(str) {
756
+
| Some(res) =>
757
+
switch RegExp.Result.matches(res) {
758
+
| [n] => (NameT(n), String.sliceToEnd(str, ~start=RegExp.lastIndex(reName)))
623
759
| _ => throw(ParseError("invalid symbol"))
624
760
}
761
+
| None =>
762
+
switch scopeVarToken(str, scope) {
763
+
| Some((idx, rest)) => (VarT(idx), rest)
764
+
| None =>
765
+
let (atom, rest) = atomToken(str, ~scope, ~gen?)
766
+
(AtomT(atom), rest)
767
+
}
625
768
}
626
769
}
627
770
}
628
771
}
629
772
}
630
-
}
631
-
type rec simple =
632
-
| ListS({xs: array<simple>})
633
-
| AtomS({name: string, constructor: bool})
634
-
| VarS({idx: int})
635
-
| SchematicS({schematic: int})
636
-
| LambdaS({name: string, body: simple})
637
-
let rec parseSimple = (str: string): (simple, string) => {
638
-
let (t0, rest) = tokenize(str)
639
-
switch t0 {
640
-
| LParen => {
641
-
let (t1, rest1) = tokenize(rest)
642
-
switch t1 {
643
-
| NameT(name) => {
644
-
let (result, rest2) = parseSimple("("->String.concat(rest1))
645
-
(LambdaS({name, body: result}), rest2)
646
-
}
647
-
| RParen => (ListS({xs: []}), rest1)
648
-
| _ => {
649
-
let (head, rest2) = parseSimple(rest)
650
-
let (tail, rest3) = parseSimple("("->String.concat(rest2))
651
-
switch tail {
652
-
| ListS({xs}) => (ListS({xs: Array.concat([head], xs)}), rest3)
653
-
| _ => throw(Util.Unreachable("bug"))
773
+
type rec simple =
774
+
| ListS({xs: array<simple>})
775
+
| AtomS({name: Atom.t, constructor: bool})
776
+
| VarS({idx: int})
777
+
| SchematicS({schematic: int})
778
+
| LambdaS({name: string, body: simple})
779
+
let rec parseSimple = (str: string, ~scope: array<string>, ~gen=?): (simple, string) => {
780
+
let (t0, rest) = tokenize(str, ~scope, ~gen?)
781
+
switch t0 {
782
+
| LParen => {
783
+
let (t1, rest1) = tokenize(rest, ~scope, ~gen?)
784
+
switch t1 {
785
+
| NameT(name) => {
786
+
let (result, rest2) = parseSimple(
787
+
"("->String.concat(rest1),
788
+
~scope=Array.concat([name], scope),
789
+
~gen?,
790
+
)
791
+
(LambdaS({name, body: result}), rest2)
792
+
}
793
+
| RParen => (ListS({xs: []}), rest1)
794
+
| _ => {
795
+
let (head, rest2) = parseSimple(rest, ~scope, ~gen?)
796
+
let (tail, rest3) = parseSimple("("->String.concat(rest2), ~scope, ~gen?)
797
+
switch tail {
798
+
| ListS({xs}) => (ListS({xs: Array.concat([head], xs)}), rest3)
799
+
| _ => throw(Util.Unreachable("bug"))
800
+
}
654
801
}
655
802
}
656
803
}
657
-
}
658
-
| RParen => throw(ParseError("unexpected right parenthesis"))
659
-
| VarT(idx) => (VarS({idx: idx}), rest)
660
-
| SchematicT(schematic) => (SchematicS({schematic: schematic}), rest)
661
-
| AtomT(name) => (AtomS({name, constructor: false}), rest)
662
-
| ConsT(name) => (AtomS({name, constructor: true}), rest)
663
-
| NameT(name) => {
664
-
let (result, rest1) = parseSimple(rest)
665
-
(LambdaS({name, body: result}), rest1)
804
+
| RParen => throw(ParseError("unexpected right parenthesis"))
805
+
| VarT(idx) => (VarS({idx: idx}), rest)
806
+
| SchematicT(schematic) => (SchematicS({schematic: schematic}), rest)
807
+
| AtomT(name) => (AtomS({name, constructor: false}), rest)
808
+
| ConsT(name) => (AtomS({name, constructor: true}), rest)
809
+
| NameT(name) => {
810
+
let (result, rest1) = parseSimple(rest, ~scope=Array.concat([name], scope), ~gen?)
811
+
(LambdaS({name, body: result}), rest1)
812
+
}
813
+
| EOF => throw(ParseError("unexpected end of file"))
666
814
}
667
-
| EOF => throw(ParseError("unexpected end of file"))
668
815
}
669
-
}
670
-
type env = Map.t<string, int>
671
-
let incrEnv = (env: env): env => {
672
-
let nu: env = Map.make()
673
-
Map.entries(env)->Iterator.forEach(opt =>
674
-
switch opt {
675
-
| None => ()
676
-
| Some((key, value)) => nu->Map.set(key, value + 1)
677
-
}
678
-
)
679
-
nu
680
-
}
681
-
let envFromScope = (scope: array<string>): env => {
682
-
let nu: env = Map.make()
683
-
scope->Array.forEachWithIndex((name, idx) => {
684
-
nu->Map.set(name, idx)
685
-
})
686
-
nu
687
-
}
688
-
let envPushLambda = (env: env, name: string): env => {
689
-
let nu = incrEnv(env)
690
-
nu->Map.set(name, 0)
691
-
nu
692
-
}
693
-
let rec parseAll = (simple: simple, ~env: env, ~gen=?): t => {
694
-
switch simple {
695
-
| ListS({xs}) => {
696
-
let ts = xs->Array.map(x => parseAll(x, ~env, ~gen?))
697
-
if ts->Array.length == 0 {
698
-
throw(ParseError("empty list"))
699
-
} else {
700
-
ts
701
-
->Array.sliceToEnd(~start=1)
702
-
->Array.reduce(ts[0]->Option.getExn, (acc, x) => App({func: acc, arg: x}))
816
+
let rec parseAll = (simple: simple, ~gen=?): t => {
817
+
switch simple {
818
+
| ListS({xs}) => {
819
+
let ts = xs->Array.map(x => parseAll(x, ~gen?))
820
+
if ts->Array.length == 0 {
821
+
throw(ParseError("empty list"))
822
+
} else {
823
+
ts
824
+
->Array.sliceToEnd(~start=1)
825
+
->Array.reduce(ts[0]->Option.getExn, (acc, x) => App({func: acc, arg: x}))
826
+
}
827
+
}
828
+
| AtomS({name, constructor}) => Symbol({name, constructor})
829
+
| VarS({idx}) => Var({idx: idx})
830
+
| SchematicS({schematic}) =>
831
+
switch gen {
832
+
| Some(g) => {
833
+
seen(g, schematic)
834
+
Schematic({schematic: schematic})
835
+
}
836
+
| None => throw(ParseError("Schematics not allowed here"))
703
837
}
838
+
| LambdaS({name, body}) =>
839
+
Lam({
840
+
name,
841
+
body: parseAll(body, ~gen?),
842
+
})
704
843
}
705
-
| AtomS({name, constructor}) =>
706
-
if constructor {
707
-
Symbol({name, constructor: true})
708
-
} else if env->Map.has(name) {
709
-
let idx = env->Map.get(name)->Option.getExn
710
-
Var({idx: idx})
711
-
} else {
712
-
Symbol({name, constructor: false})
713
-
}
714
-
| VarS({idx}) => Var({idx: idx})
715
-
| SchematicS({schematic}) =>
716
-
switch gen {
717
-
| Some(g) => {
718
-
seen(g, schematic)
719
-
Schematic({schematic: schematic})
844
+
}
845
+
let prettyPrintMeta = (str: string) => {
846
+
String.concat(str, ".")
847
+
}
848
+
let parseMeta = (str: string) => {
849
+
let re = RegExp.fromStringWithFlags(nameRES, ~flags="y")
850
+
switch re->RegExp.exec(str->String.trim) {
851
+
| None => Error("not a meta name")
852
+
| Some(res) =>
853
+
switch RegExp.Result.matches(res) {
854
+
| [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re)))
855
+
| _ => Error("impossible happened")
720
856
}
721
-
| None => throw(ParseError("Schematics not allowed here"))
722
857
}
723
-
| LambdaS({name, body}) =>
724
-
Lam({
725
-
name,
726
-
body: parseAll(body, ~env=envPushLambda(env, name), ~gen?),
727
-
})
728
858
}
729
-
}
730
-
let prettyPrintMeta = (str: string) => {
731
-
String.concat(str, ".")
732
-
}
733
-
let parseMeta = (str: string) => {
734
-
let re = RegExp.fromStringWithFlags(nameRES, ~flags="y")
735
-
switch re->RegExp.exec(str->String.trim) {
736
-
| None => Error("not a meta name")
737
-
| Some(res) =>
738
-
switch RegExp.Result.matches(res) {
739
-
| [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re)))
740
-
| _ => Error("impossible happened")
859
+
let parse = (str: string, ~scope: array<string>, ~gen=?) => {
860
+
try {
861
+
let (simple, rest) = parseSimple(str, ~scope, ~gen?)
862
+
Ok((parseAll(simple, ~gen?), rest))
863
+
} catch {
864
+
| ParseError(msg) => Error(msg)
741
865
}
742
866
}
743
-
}
744
-
let parse = (str: string, ~scope: array<string>, ~gen=?) => {
745
-
try {
746
-
let (simple, rest) = parseSimple(str)
747
-
Ok((parseAll(simple, ~env=envFromScope(scope), ~gen?), rest))
748
-
} catch {
749
-
| ParseError(msg) => Error(msg)
750
-
}
867
+
868
+
let concrete = t =>
869
+
switch t {
870
+
| Schematic(_) => false
871
+
| Symbol({name}) => Atom.concrete(name)
872
+
| _ => true
873
+
}
874
+
let mapTerms = (t, f) => f(t)
751
875
}
752
876
753
-
let concrete = t =>
754
-
switch t {
755
-
| Schematic(_) => false
756
-
| _ => true
757
-
}
758
-
let mapTerms = (t, f) => f(t)
877
+
include Make(DefaultAtom)
+31
-1
src/HOTerm.resi
+31
-1
src/HOTerm.resi
···
1
+
module type ATOM = AtomDef.ATOM
2
+
3
+
module Make: (Atom: AtomDef.ATOM) =>
4
+
{
5
+
type rec t =
6
+
| Symbol({name: Atom.t, constructor: bool})
7
+
| Var({idx: int})
8
+
| Schematic({schematic: int})
9
+
| Lam({name: string, body: t})
10
+
| App({func: t, arg: t})
11
+
| Unallowed
12
+
13
+
include Signatures.TERM
14
+
with type t := t
15
+
and type meta = string
16
+
and type schematic = int
17
+
and type subst = Belt.Map.Int.t<t>
18
+
19
+
let emptySubst: subst
20
+
let strip: t => (t, array<t>)
21
+
let app: (t, array<t>) => t
22
+
let mkvars: int => array<t>
23
+
let mapTerms: (t, t => t) => t
24
+
exception UnifyFail(string)
25
+
let substAdd: (subst, schematic, t) => subst
26
+
let unifyTerm: (t, t, subst, ~gen: option<gen>) => Seq.t<subst>
27
+
let reduceSubst: subst => subst
28
+
let rewrite: (t, t, t, ~subst: subst, ~gen: option<gen>) => (subst, t)
29
+
}
30
+
1
31
type rec t =
2
32
| Symbol({name: string, constructor: bool})
3
33
| Var({idx: int})
···
21
51
// exposed for testing purposes
22
52
exception UnifyFail(string)
23
53
let substAdd: (subst, schematic, t) => subst
24
-
let unifyTerm: (t, t, subst, ~gen: option<gen>) => subst
54
+
let unifyTerm: (t, t, subst, ~gen: option<gen>) => Seq.t<subst>
25
55
let reduceSubst: subst => subst
26
56
let rewrite: (t, t, t, ~subst: subst, ~gen: option<gen>) => (subst, t)
+4
-4
src/HOTermMethod.res
+4
-4
src/HOTermMethod.res
···
12
12
module Rule = Rule.Make(HOTerm, Judgment)
13
13
module Context = Context(HOTerm, Judgment)
14
14
module Results = MethodResults(HOTerm)
15
-
15
+
16
16
let extractEqualityTermsFromJudgment = (judgment: Judgment.t): option<(HOTerm.t, HOTerm.t)> => {
17
17
let term: HOTerm.t = judgment
18
18
switch HOTerm.strip(term) {
···
202
202
}
203
203
})
204
204
205
-
ret->Dict.toArray->Array.map(((s,(a,b))) => Results.Action(s,a,b))
205
+
ret->Dict.toArray->Array.map(((s, (a, b))) => Results.Action(s, a, b))
206
206
}
207
207
208
208
let check = (it: t<'a>, ctx: Context.t, goal: Judgment.t, f: ('a, Rule.t) => 'b) => {
···
337
337
ret->Dict.set(`constructor_neq ${lhs} ${rhs}`, ((), HOTerm.makeSubst()))
338
338
| _ => ()
339
339
}
340
-
ret->Dict.toArray->Array.map(((s,(a,b))) => Results.Action(s,a,b))
340
+
ret->Dict.toArray->Array.map(((s, (a, b))) => Results.Action(s, a, b))
341
341
}
342
342
343
343
let check = (_it: t<'a>, _ctx: Context.t, goal: Judgment.t, _f: ('a, Rule.t) => 'b) =>
···
446
446
})
447
447
| _ => ()
448
448
}
449
-
ret->Dict.toArray->Array.map(((s,(a,b))) => Results.Action(s,a,b))
449
+
ret->Dict.toArray->Array.map(((s, (a, b))) => Results.Action(s, a, b))
450
450
}
451
451
452
452
let check = (it: t<'a>, ctx: Context.t, goal: Judgment.t, _f: ('a, Rule.t) => 'b) => {
+79
-61
src/ProofView.res
+79
-61
src/ProofView.res
···
17
17
module ResultsView = {
18
18
type menuState<'a> = {
19
19
history: list<array<Results.t<MethodView.Method.t<Proof.checked>>>>, // Stack of previous menus
20
-
current: array<Results.t<MethodView.Method.t<Proof.checked>>>, // What is currently visible
20
+
current: array<Results.t<MethodView.Method.t<Proof.checked>>>, // What is currently visible
21
21
}
22
22
type props = {
23
23
initialNodes: array<Results.t<MethodView.Method.t<Proof.checked>>>,
24
-
onApply: (MethodView.Method.t<Proof.checked>, Term.subst) => (),
25
-
onBlur: (ReactEvent.Focus.t) => ()
24
+
onApply: (MethodView.Method.t<Proof.checked>, Term.subst) => unit,
25
+
onBlur: ReactEvent.Focus.t => unit,
26
26
}
27
27
@react.componentWithProps
28
28
let make = (props: props) => {
29
-
let (state, setState) = React.useState(_ => {
30
-
history: list{},
31
-
current: props.initialNodes,
29
+
let (state, setState) = React.useState(_ => {
30
+
history: list{},
31
+
current: props.initialNodes,
32
+
})
33
+
34
+
let goBack = _ => {
35
+
setState(prev => {
36
+
switch prev.history {
37
+
| list{parent, ...rest} => {current: parent, history: rest}
38
+
| list{} => prev // Already at the root
39
+
}
40
+
})
41
+
}
42
+
43
+
let drillDown = (newNodes: array<Results.t<'a>>) => {
44
+
setState(prev => {
45
+
history: list{prev.current, ...prev.history},
46
+
current: newNodes,
32
47
})
33
-
34
-
let goBack = _ => {
35
-
setState(prev => {
36
-
switch prev.history {
37
-
| list{parent, ...rest} => {current: parent, history: rest}
38
-
| list{} => prev // Already at the root
48
+
}
49
+
50
+
<div className="drill-down-container">
51
+
{state.history != list{}
52
+
? <button tabIndex=0 onBlur={props.onBlur} onClick={goBack} className="back-button">
53
+
{React.string("← Back")}
54
+
</button>
55
+
: React.null}
56
+
57
+
<div className="menu-options">
58
+
{state.current
59
+
->Array.mapWithIndex((node, i) => {
60
+
switch node {
61
+
| Action(label, nextTree, subst) =>
62
+
<button
63
+
tabIndex=0
64
+
onBlur={props.onBlur}
65
+
key={label ++ i->Int.toString}
66
+
onClick={_ => props.onApply(nextTree, subst)}
67
+
>
68
+
{React.string(label ++ "")}
69
+
</button>
70
+
71
+
| Group(label, children) =>
72
+
<button
73
+
tabIndex=0
74
+
onBlur={props.onBlur}
75
+
key={label ++ i->Int.toString}
76
+
onClick={_ => drillDown(children)}
77
+
>
78
+
{React.string(label ++ " →")}
79
+
</button>
80
+
81
+
| Delay(label, getChildren) =>
82
+
<button
83
+
tabIndex=0
84
+
onBlur={props.onBlur}
85
+
key={label ++ i->Int.toString}
86
+
onClick={_ => drillDown(getChildren())}
87
+
>
88
+
{React.string(label ++ " ...")}
89
+
</button>
39
90
}
40
91
})
41
-
}
42
-
43
-
let drillDown = (newNodes: array<Results.t<'a>>) => {
44
-
setState(prev => {
45
-
history: list{prev.current, ...prev.history},
46
-
current: newNodes,
47
-
})
48
-
}
49
-
50
-
<div className="drill-down-container">
51
-
{state.history != list{}
52
-
? <button tabIndex=0 onBlur={props.onBlur} onClick={goBack} className="back-button"> {React.string("← Back")} </button>
53
-
: React.null}
54
-
55
-
<div className="menu-options">
56
-
{state.current->Array.mapWithIndex((node, i) => {
57
-
switch node {
58
-
| Action(label, nextTree, subst) =>
59
-
<button tabIndex=0 onBlur={props.onBlur} key={label ++ i->Int.toString} onClick={_ => props.onApply(nextTree, subst)}>
60
-
{React.string(label ++ "")}
61
-
</button>
62
-
63
-
| Group(label, children) =>
64
-
<button tabIndex=0 onBlur={props.onBlur} key={label ++ i->Int.toString} onClick={_ => drillDown(children)}>
65
-
{React.string(label ++ " →")}
66
-
</button>
67
-
68
-
| Delay(label, getChildren) =>
69
-
<button tabIndex=0 onBlur={props.onBlur} key={label ++ i->Int.toString} onClick={_ => drillDown(getChildren())}>
70
-
{React.string(label ++ " ...")}
71
-
</button>
72
-
}
73
-
})->React.array}
74
-
</div>
92
+
->React.array}
75
93
</div>
76
-
}
94
+
</div>
77
95
}
78
-
79
-
96
+
}
97
+
80
98
type props = {
81
99
proof: Proof.checked,
82
100
scope: array<Term.meta>,
···
118
136
let portal = switch sidebarRef.current->Nullable.toOption {
119
137
| None => React.null
120
138
| Some(node) =>
121
-
let res = options(props.gen);
122
-
Portal.createPortal(
139
+
let res = options(props.gen)
140
+
Portal.createPortal(
123
141
<>
124
-
{
125
-
<ResultsView initialNodes=res
126
-
onBlur
127
-
onApply={(opt,subst)=>
128
-
props.onChange(
129
-
Proof.Checked({fixes, assumptions, method: Do(opt), rule}),
130
-
subst,
131
-
)}
132
-
></ResultsView>
133
-
}
142
+
{<ResultsView
143
+
initialNodes=res
144
+
onBlur
145
+
onApply={(opt, subst) =>
146
+
props.onChange(
147
+
Proof.Checked({fixes, assumptions, method: Do(opt), rule}),
148
+
subst,
149
+
)}
150
+
>
151
+
</ResultsView>}
134
152
</>,
135
153
node,
136
154
)
+1
-1
src/SidebarContext.res
+1
-1
src/SidebarContext.res
+72
-1
tests/HOTermTest.res
+72
-1
tests/HOTermTest.res
···
3
3
4
4
module Util = TestUtil.MakeTerm(HOTerm)
5
5
6
+
module Symbol = AtomDef.MakeAtomAndView(
7
+
Symbolic.Atom,
8
+
Symbolic.AtomView,
9
+
AtomDef.NilAtomList,
10
+
AtomDef.NilAtomListView,
11
+
)
12
+
module StringSymbol = AtomDef.MakeAtomAndView(
13
+
StringA.Atom,
14
+
StringA.AtomView,
15
+
Symbol.Atom,
16
+
Symbol.AtomView,
17
+
)
18
+
module StringHOTerm = HOTerm.Make(StringSymbol.Atom)
19
+
module StringUtil = TestUtil.MakeTerm(StringHOTerm)
20
+
let wrapString = s => StringHOTerm.Symbol({
21
+
name: AtomDef.AnyValue(StringA.BaseAtom.Tag, s),
22
+
constructor: false,
23
+
})
24
+
let wrapSymbol = s => StringHOTerm.Symbol({
25
+
name: AtomDef.AnyValue(Symbolic.BaseAtom.Tag, s),
26
+
constructor: false,
27
+
})
28
+
6
29
let testUnify0 = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?, ~reduce=false) => {
7
30
let gen = HOTerm.makeGen()
8
31
let (a, _) = HOTerm.parse(at, ~scope=[], ~gen)->Result.getExn
9
32
let (b, _) = HOTerm.parse(bt, ~scope=[], ~gen)->Result.getExn
10
33
try {
11
-
let res0 = HOTerm.unifyTerm(a, b, HOTerm.emptySubst, ~gen=Some(gen))
34
+
let res0 = HOTerm.unifyTerm(a, b, HOTerm.emptySubst, ~gen=Some(gen))->Seq.head->Option.getExn
12
35
let res = if reduce {
13
36
HOTerm.reduceSubst(res0)
14
37
} else {
···
58
81
zoraBlock("parse var", t => {
59
82
t->block("single digit", t => t->Util.testParse("\\1", Var({idx: 1})))
60
83
t->block("multi digit", t => t->Util.testParse("\\234", Var({idx: 234})))
84
+
t->block("scope", t => t->Util.testParse("0", ~scope=["0"], Var({idx: 0})))
61
85
})
62
86
63
87
zoraBlock("parse schematic", t => {
···
141
165
t->Util.testParsePrettyPrint("(x. y. z. y)", "(x. y. z. y)")
142
166
t->Util.testParsePrettyPrint("(x. y. z. x)", "(x. y. z. x)")
143
167
t->Util.testParsePrettyPrint("(x. y. z. z y x)", "(x. y. z. z y x)")
168
+
})
169
+
})
170
+
171
+
zoraBlock("string HOTerm functor", t => {
172
+
t->block("parse string atom", t => {
173
+
t->StringUtil.testParse(`"x y"`, wrapString([StringA.String("x"), StringA.String("y")]))
174
+
t->StringUtil.testParse(`"$s"`, ~scope=["s"], wrapString([StringA.Var({idx: 0})]))
175
+
t->StringUtil.testParsePrettyPrint(`"x y"`, `"x y"`)
176
+
})
177
+
t->block("parse symbolic atom", t => {
178
+
t->StringUtil.testParse("x", wrapSymbol("x"))
179
+
t->StringUtil.testParse(
180
+
"@cons",
181
+
StringHOTerm.Symbol({
182
+
name: AtomDef.AnyValue(Symbolic.BaseAtom.Tag, "cons"),
183
+
constructor: true,
184
+
}),
185
+
)
186
+
t->StringUtil.testParse(
187
+
"(x. x)",
188
+
StringHOTerm.Lam({name: "x", body: StringHOTerm.Var({idx: 0})}),
189
+
)
190
+
})
191
+
t->block("unify string atom", t => {
192
+
let parse = input => t->StringUtil.parse(input)
193
+
let emptySubst = StringHOTerm.emptySubst
194
+
let substAdd = StringHOTerm.substAdd
195
+
t->equal(
196
+
StringHOTerm.unify(parse(`"a ?0() c"`), parse(`"a b c"`))->Seq.head,
197
+
Some(emptySubst->substAdd(0, wrapString([StringA.String("b")]))),
198
+
)
199
+
t->equal(
200
+
StringHOTerm.unify(parse(`(P "?1() a" "?1()")`), parse(`(P "a ?1()" "a")`))->Seq.head,
201
+
Some(emptySubst->substAdd(1, wrapString([StringA.String("a")]))),
202
+
)
203
+
let choices =
204
+
StringHOTerm.unify(parse(`"?1() a"`), parse(`"a ?1()"`))
205
+
->Seq.take(2)
206
+
->Seq.toArray
207
+
t->equal(
208
+
choices,
209
+
[
210
+
emptySubst->substAdd(1, wrapString([])),
211
+
emptySubst->substAdd(1, wrapString([StringA.String("a")])),
212
+
],
213
+
)
214
+
t->equal(StringHOTerm.unify(parse(`"a"`), parse(`"b"`))->Seq.head, None)
144
215
})
145
216
})
146
217
+44
-12
tests/RuleTest.res
+44
-12
tests/RuleTest.res
···
31
31
}
32
32
}
33
33
34
+
module Symbol = AtomDef.MakeAtomAndView(
35
+
Symbolic.Atom,
36
+
Symbolic.AtomView,
37
+
AtomDef.NilAtomList,
38
+
AtomDef.NilAtomListView,
39
+
)
40
+
module StringSymbol = AtomDef.MakeAtomAndView(
41
+
StringA.Atom,
42
+
StringA.AtomView,
43
+
Symbol.Atom,
44
+
Symbol.AtomView,
45
+
)
46
+
34
47
zoraBlock("string terms", t => {
35
-
module Symbol = AtomDef.MakeAtomAndView(
36
-
Symbolic.Atom,
37
-
Symbolic.AtomView,
38
-
AtomDef.NilAtomList,
39
-
AtomDef.NilAtomListView,
40
-
)
41
-
module StringSymbol = AtomDef.MakeAtomAndView(
42
-
StringA.Atom,
43
-
StringA.AtomView,
44
-
Symbol.Atom,
45
-
Symbol.AtomView,
46
-
)
47
48
module StringSExp = SExp.Make(StringSymbol.Atom)
48
49
let wrapString = (s): StringSExp.t => Atom(AtomDef.AnyValue(StringA.BaseAtom.Tag, s))
49
50
let wrapSymbol = (s): StringSExp.t => Atom(AnyValue(Symbolic.BaseAtom.Tag, s))
···
70
71
},
71
72
)
72
73
})
74
+
75
+
zoraBlock("string HOTerms", t => {
76
+
module StringHOTerm = HOTerm.Make(StringSymbol.Atom)
77
+
let wrapString = (s): StringHOTerm.t => Symbol({
78
+
name: AtomDef.AnyValue(StringA.BaseAtom.Tag, s),
79
+
constructor: false,
80
+
})
81
+
let wrapSymbol = (s): StringHOTerm.t => Symbol({
82
+
name: AtomDef.AnyValue(Symbolic.BaseAtom.Tag, s),
83
+
constructor: false,
84
+
})
85
+
let app = StringHOTerm.app
86
+
module T = MakeTest(StringHOTerm, StringHOTerm)
87
+
t->T.testParseInner(
88
+
`[s1. ("$s1" p) |- ("($s1)" p)]`,
89
+
{
90
+
vars: ["s1"],
91
+
premises: [
92
+
{
93
+
vars: [],
94
+
premises: [],
95
+
conclusion: app(wrapString([StringA.Var({idx: 0})]), [wrapSymbol("p")]),
96
+
},
97
+
],
98
+
conclusion: app(
99
+
wrapString([StringA.String("("), StringA.Var({idx: 0}), StringA.String(")")]),
100
+
[wrapSymbol("p")],
101
+
),
102
+
},
103
+
)
104
+
})