the next generation of the in-browser educational proof assistant
call fresh
+6
-6
+6
-6
src/HOTerm.res
+6
-6
src/HOTerm.res
···
30
30
g := s + 1
31
31
}
32
32
}
33
+
let fresh = (g: gen, ~replacing as _=?) => {
34
+
let v = g.contents
35
+
g := g.contents + 1
36
+
v
37
+
}
33
38
let rec schematicsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
34
39
switch it {
35
40
| Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
···
351
356
)
352
357
let allowed: array<int> = Array.fromInitializer(~length=a.args->Array.length, i => i)
353
358
let hs: array<t> = Array.fromInitializer(~length=b.args->Array.length, _ => Schematic({
354
-
schematic: Option.getUnsafe(gen).contents,
359
+
schematic: fresh(Option.getUnsafe(gen)),
355
360
allowed,
356
361
}))
357
362
switch unifyArray(Belt.Array.zip(b.args->Array.map(x => substVar(x, substV)), hs), ~gen?) {
···
381
386
schematic: x,
382
387
allowed: Array.fromInitializer(~length=Array.length(scope), i => i),
383
388
})
384
-
let fresh = (g: gen, ~replacing as _=?) => {
385
-
let v = g.contents
386
-
g := g.contents + 1
387
-
v
388
-
}
389
389
let prettyPrintVar = (idx: int, scope: array<string>) =>
390
390
switch scope[idx] {
391
391
| Some(n) if Array.indexOf(scope, n) == idx && false => n