the next generation of the in-browser educational proof assistant
Merge pull request #5 from mio-19/mio
Functions-as-Constructors Unification
authored by
Liam O'Connor
and committed by
GitHub
9c7d9851
5a6da2fd
+137
-65
+77
-65
src/HOTerm.res
+77
-65
src/HOTerm.res
···
27
27
| (Schematic({schematic: sa}), Schematic({schematic: sb})) => sa == sb
28
28
| (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => equivalent(ba, bb)
29
29
| (App({func: fa, arg: aa}), App({func: fb, arg: ab})) => equivalent(fa, fb) && equivalent(aa, ab)
30
+
| (Unallowed, Unallowed) => false
30
31
| (_, _) => false
31
32
}
32
33
}
···
123
124
}
124
125
mapbind(term, idx => idx - amount, ~from)
125
126
}
127
+
let lookup = (term: t, subst: array<(t, t)>): option<t> => {
128
+
subst
129
+
->Array.find(((from, _)) => equivalent(term, from))
130
+
->Option.map(((_, to)) => to)
131
+
}
132
+
let upshift_tt = (subst: array<(t, t)>, ~amount: int=1): array<(t, t)> => {
133
+
subst->Array.map(((a, b)) => (upshift(a, amount), upshift(b, amount)))
134
+
}
135
+
// where pattern unification used mapbind we will need to use discharge for FCU
136
+
let rec discharge = (subst: array<(t, t)>, term: t, ~prune: bool): t => {
137
+
switch lookup(term, subst) {
138
+
| Some(found) => found
139
+
| None =>
140
+
switch term {
141
+
| App({func, arg}) =>
142
+
App({func: discharge(subst, func, ~prune), arg: discharge(subst, arg, ~prune)})
143
+
// Lam case is not actually needed by FCU
144
+
| Lam({name, body}) => Lam({name, body: discharge(upshift_tt(subst), body, ~prune)})
145
+
| Var(_) if prune => Unallowed
146
+
| Var(_) | Schematic(_) | Symbol(_) | Unallowed => term
147
+
}
148
+
}
149
+
}
126
150
let emptySubst: subst = Belt.Map.Int.empty
127
151
let substAdd = (subst: subst, schematic: schematic, term: t) => {
128
152
assert(schematic >= 0)
···
214
238
})
215
239
}
216
240
}
217
-
let rec idx = (is: array<t>, j: int): option<int> => {
241
+
let rec idx = (is: array<t>, j: t): option<int> => {
218
242
if is->Array.length == 0 {
219
243
None
220
244
} else {
221
245
let head = is[0]->Option.getExn
222
246
let tail = is->Array.sliceToEnd(~start=1)
223
-
if equivalent(head, Var({idx: j})) {
247
+
if equivalent(head, j) {
224
248
Some(tail->Array.length)
225
249
} else {
226
250
idx(tail, j)
227
251
}
228
252
}
229
253
}
230
-
let idx1 = (is: array<t>, j: int): t => {
254
+
let idx1' = (is: array<t>, j: t): t => {
231
255
switch idx(is, j) {
232
256
| None => Unallowed
233
257
| Some(idx) => Var({idx: idx})
234
258
}
235
259
}
236
-
let idx2 = (is: array<t>, j: int): result<int, int => t> => {
260
+
let idx1 = (is: array<t>, j: int): t => idx1'(is, Var({idx: j}))
261
+
let idx2' = (is: array<t>, j: t): result<int, int => t> => {
237
262
switch idx(is, j) {
238
263
| None => Error(_ => Unallowed)
239
264
| Some(idx) => Ok(idx)
240
265
}
241
266
}
267
+
let idx2 = (is: array<t>, j: int) => idx2'(is, Var({idx: j}))
242
268
let rec app = (term: t, args: array<t>): t => {
243
269
if args->Array.length == 0 {
244
270
term
···
249
275
}
250
276
}
251
277
exception UnifyFail(string)
252
-
let isvar = (term: t): bool =>
278
+
let rec red = (term: t, is: array<t>): t => {
253
279
switch term {
254
-
| Var(_) => true
255
-
| _ => false
256
-
}
257
-
let rec red = (term: t, is: array<t>, js: array<t>): t => {
258
-
switch term {
259
-
| Lam({name, body}) if is->Array.length > 0 && isvar(is[0]->Option.getExn) => {
260
-
let head = is[0]->Option.getExn
261
-
let rest = is->Array.sliceToEnd(~start=1)
262
-
red(body, rest, Array.concat([head], js))
263
-
}
264
-
| _ =>
265
-
app(
266
-
term->mapbind(k =>
267
-
switch js[k]->Option.getExn {
268
-
| Var({idx}) => idx
269
-
| _ => raise(UnifyFail("expected variable in red"))
270
-
}
271
-
),
272
-
is,
273
-
)
280
+
| _ if is->Array.length == 0 => term
281
+
| Lam({body}) => red(substDeBruijn(body, [is[0]->Option.getExn]), is->Array.sliceToEnd(~start=1))
282
+
| term => app(term, is)
274
283
}
275
284
}
276
-
// app with beta reduction
277
-
let rec app1 = (term: t, args: array<t>): t =>
278
-
if args->Array.length == 0 {
279
-
term
280
-
} else {
281
-
let head = args[0]->Option.getExn
282
-
let rest = args->Array.sliceToEnd(~start=1)
283
-
switch term {
284
-
| Lam({body}) => app1(substDeBruijn(body, [head]), rest)
285
-
| _ => app1(App({func: term, arg: head}), rest)
286
-
}
287
-
}
288
-
let lam = (is: array<t>, g: t, js: array<int>): t => {
289
-
lams(is->Array.length, app(g, js->Array.map(j => idx1(is, j))))
285
+
let lam = (is: array<t>, g: t, js: array<t>): t => {
286
+
lams(is->Array.length, app(g, js->Array.map(j => idx1'(is, j))))
290
287
}
291
288
let rec strip = (term: t): (t, array<t>) => {
292
289
switch term {
···
300
297
let (func, args) = strip(term)
301
298
switch func {
302
299
| Schematic({schematic}) if substHas(subst, schematic) =>
303
-
devar(subst, red(substGet(subst, schematic)->Option.getExn, args, []))
300
+
devar(subst, red(substGet(subst, schematic)->Option.getExn, args))
304
301
| _ => term
305
302
}
306
303
}
304
+
let mkvars = (n: int): array<t> => {
305
+
Belt.Array.init(n, i => n - i - 1)->Array.map(x => Var({idx: x}))
306
+
}
307
+
let rec proj_allowed = (subst: subst, term: t): bool => {
308
+
let term' = devar(subst, term)
309
+
switch term' {
310
+
| Lam(_) => false
311
+
| Unallowed => false
312
+
| Schematic(_) => false
313
+
| Symbol(_) => false
314
+
| Var(_) => true // pattern unification only allows this
315
+
// FCU allows this, right?
316
+
| App(_) =>
317
+
switch strip(term') {
318
+
| (Symbol(_) | Var(_), args) => Array.every(args, x => proj_allowed(subst, x))
319
+
| _ => false
320
+
}
321
+
}
322
+
}
323
+
// this function is called proj in Nipkow 1993 and it is called pruning in FCU paper
307
324
let rec proj = (subst: subst, term: t, ~gen: option<gen>): subst => {
308
325
switch strip(devar(subst, term)) {
309
326
| (Lam({name, body}), args) if args->Array.length == 0 => proj(subst, body, ~gen)
···
322
339
app(
323
340
h,
324
341
Belt.Array.init(args->Array.length, j => {
325
-
switch args[j]->Option.getExn {
326
-
| Var({idx}) => Some(Var({idx: args->Belt.Array.length - j - 1}))
327
-
| _ => None
342
+
if proj_allowed(subst, args[j]->Option.getExn) {
343
+
Some(Var({idx: args->Belt.Array.length - j - 1}))
344
+
} else {
345
+
None
328
346
}
329
347
})->Array.keepSome,
330
348
),
···
354
372
let xs = Belt.Array.init(len, k => {
355
373
let a = xs[k]->Option.getExn
356
374
let b = ys[k]->Option.getExn
357
-
switch (a, b) {
358
-
| (Var(_), Var(_)) if equivalent(a, b) => Some(Var({idx: len - k - 1}))
359
-
| _ => None
375
+
if equivalent(a, b) {
376
+
Some(Var({idx: len - k - 1}))
377
+
} else {
378
+
None
360
379
}
361
380
})->Array.keepSome
362
381
subst->substAdd(sa, lams(len, app(h, xs)))
363
382
} else {
364
-
let y_vars = Belt.Set.fromArray(
365
-
ys->Array.filterMap(y =>
366
-
switch y {
367
-
| Var({idx}) => Some(idx)
368
-
| _ => None
369
-
}
370
-
),
371
-
~id=module(IntCmp),
372
-
)
373
-
let common = xs->Array.filterMap(x =>
374
-
switch x {
375
-
| Var({idx}) if y_vars->Belt.Set.has(idx) => Some(idx)
376
-
| _ => None
377
-
}
378
-
)
383
+
let common = xs->Array.filter(x => ys->Belt.Array.some(y => equivalent(x, y)))
379
384
let h = Schematic({schematic: fresh(Option.getExn(gen))})
380
385
subst->substAdd(sa, lam(xs, h, common))->substAdd(sb, lam(ys, h, common))
381
386
}
···
384
389
if occ(sa, subst, b) {
385
390
raise(UnifyFail("flexible schematic occurs in rigid term"))
386
391
}
387
-
let u = b->mapbind0(bind => idx2(xs, bind))
392
+
// pattern unification
393
+
//let u = b->mapbind0(bind => idx2(xs, bind))
394
+
// FCU
395
+
let zn = mkvars(xs->Array.length)
396
+
let u = discharge(Belt.Array.zip(xs, zn), b, ~prune=true)
388
397
proj(subst->substAdd(sa, lams(xs->Array.length, u)), u, ~gen)
389
398
}
390
399
let rec unifyTerm = (a: t, b: t, subst: subst, ~gen: option<gen>): subst =>
···
407
416
unifyTerm(ba, App({func: upshift(b, 1), arg: Var({idx: 0})}), subst, ~gen)
408
417
| (a, Lam({name: _, body: bb})) =>
409
418
unifyTerm(App({func: upshift(a, 1), arg: Var({idx: 0})}), bb, subst, ~gen)
410
-
| (_, _) =>
419
+
| (a, b) =>
411
420
switch (strip(a), strip(b)) {
412
421
| ((Schematic({schematic: sa}), xs), (Schematic({schematic: sb}), ys)) =>
413
422
flexflex(sa, xs, sb, ys, subst, ~gen)
414
423
| ((Schematic({schematic: sa}), xs), _) => flexrigid(sa, xs, b, subst, ~gen)
415
424
| (_, (Schematic({schematic: sb}), ys)) => flexrigid(sb, ys, a, subst, ~gen)
416
-
| ((a, xs), (b, ys)) => rigidrigid(a, xs, b, ys, subst, ~gen)
417
-
| (_, _) => raise(UnifyFail("no rules match"))
425
+
| ((a, xs), (b, ys)) =>
426
+
switch (a, b) {
427
+
| (Symbol(_) | Var(_), Symbol(_) | Var(_)) => rigidrigid(a, xs, b, ys, subst, ~gen)
428
+
| _ => raise(UnifyFail("no rules match"))
429
+
}
418
430
}
419
431
}
420
432
and unifyArray = (xs: array<t>, ys: array<t>, subst: subst, ~gen: option<gen>): subst => {
+60
tests/HOTermTest.res
+60
tests/HOTermTest.res
···
17
17
switch subst {
18
18
| None => t->ok(true, ~msg=msg->Option.getOr("unification succeeded"))
19
19
| Some(subst) =>
20
+
t->equal(subst->Belt.Map.Int.size, res->Belt.Map.Int.size)
20
21
subst->Belt.Map.Int.forEach((k, v) => {
21
22
let expected = subst->Belt.Map.Int.getExn(k)
22
23
if res->Belt.Map.Int.has(k) == false {
···
165
166
),
166
167
)
167
168
t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, Symbol({name: "y"})))
169
+
})
170
+
t->block("flex-rigid3", t => {
171
+
let x = "(?0 \\10)"
172
+
let y = "(fst \\10)"
173
+
t->testUnify(x, y, ~subst=emptySubst->substAdd(0, Symbol({name: "fst"})))
174
+
})
175
+
t->block("flex-rigid", t => {
176
+
let x = "(?0 \\10)"
177
+
let y = "(r (fst \\10))"
178
+
t->Util.testUnify(
179
+
x,
180
+
y,
181
+
~subst=emptySubst->substAdd(
182
+
0,
183
+
Lam({
184
+
name: "x",
185
+
body: App({
186
+
func: Symbol({name: "r"}),
187
+
arg: App({func: Symbol({name: "fst"}), arg: Var({idx: 0})}),
188
+
}),
189
+
}),
190
+
),
191
+
)
192
+
})
193
+
t->block("flex-rigid-fcu-2", t => {
194
+
let x = "(?0 (fst \\10))"
195
+
let y = "(r (fst (fst \\10)))"
196
+
t->Util.testUnify(
197
+
x,
198
+
y,
199
+
~subst=emptySubst->substAdd(
200
+
0,
201
+
HOTerm.parse("(x. (r (fst x)))", ~scope=[])->Result.getExn->fst,
202
+
),
203
+
)
204
+
})
205
+
t->block("flex-rigid-fcu-3", t => {
206
+
let x = "(?1 (fst \\10) (snd \\1))"
207
+
let y = "(r (q (snd \\1) (fst \\10)))"
208
+
t->Util.testUnify(
209
+
x,
210
+
y,
211
+
~subst=emptySubst->substAdd(
212
+
1,
213
+
HOTerm.parse("(x. x. (r (q \\0 \\1)))", ~scope=[])->Result.getExn->fst,
214
+
),
215
+
)
216
+
})
217
+
t->block("flex-rigid-fcu-4", t => {
218
+
let x = "(?1 (fst \\10) \\1)"
219
+
let y = "(r (q (snd \\1) (fst \\10)))"
220
+
t->Util.testUnify(
221
+
x,
222
+
y,
223
+
~subst=emptySubst->substAdd(
224
+
1,
225
+
HOTerm.parse("(x. x. (r (q (snd \\0) \\1)))", ~scope=[])->Result.getExn->fst,
226
+
),
227
+
)
168
228
})
169
229
t->block("?0 \\0", t => {
170
230
let x = "(?0 \\0)"