the next generation of the in-browser educational proof assistant
flex-rigid
+10
-3
+10
-3
src/HOTerm.res
+10
-3
src/HOTerm.res
···
268
268
if gen->Option.isNone || map->Array.find(v => v->Option.isNone)->Option.isSome {
269
269
None
270
270
} else {
271
-
let map1 = map->Array.map(v => v->Option.getUnsafe)
271
+
let substV: substVar = Map.make()
272
+
Array.reverse(map)
273
+
map->Array.forEachWithIndex((v, i) =>
274
+
switch v {
275
+
| Some(idx) => substV->Map.set(idx, i)
276
+
| None => raise(Unreachable("bug"))
277
+
}
278
+
)
272
279
let allowed: array<int> = Array.fromInitializer(~length=a.args->Array.length, i => i)
273
280
let hs: array<t> = Array.fromInitializer(~length=b.args->Array.length, _ => Schematic({
274
281
schematic: Option.getUnsafe(gen).contents,
275
282
allowed,
276
283
}))
277
-
switch unifyArray(Belt.Array.zip(raise(TODO("TODO")), hs), ~gen?) {
284
+
switch unifyArray(Belt.Array.zip(b.args->Array.map(x => substVar(x, substV)), hs), ~gen?) {
278
285
| Some(s) => {
279
-
let term: t = raise(TODO("TODO"))
286
+
let term: t = substitute(lam(a.args->Array.length, app(b.func, hs)), s)
280
287
Some(singletonSubst(schematic, term))
281
288
}
282
289
| None => None