the next generation of the in-browser educational proof assistant
call gen in flex-rigid
+8
-8
+8
-8
src/HOTerm.res
+8
-8
src/HOTerm.res
···
24
24
| (_, _) => false
25
25
}
26
26
}
27
+
type gen = ref<int>
28
+
let seen = (g: gen, s: int) => {
29
+
if s >= g.contents {
30
+
g := s + 1
31
+
}
32
+
}
27
33
let rec schematicsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
28
34
switch it {
29
35
| Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
···
219
225
| _ => None
220
226
}
221
227
)
222
-
if map->Array.find(v => v->Option.isNone)->Option.isSome {
228
+
if gen->Option.isNone || map->Array.find(v => v->Option.isNone)->Option.isSome {
223
229
None
224
230
} else {
225
231
let map1 = map->Array.map(v => v->Option.getUnsafe)
226
232
let allowed: array<int> = Array.fromInitializer(~length=a.args->Array.length, i => i)
227
233
let hs: array<t> = Array.fromInitializer(~length=b.args->Array.length, _ => Schematic({
228
-
schematic: raise(TODO("TODO")),
234
+
schematic: Option.getUnsafe(gen).contents,
229
235
allowed,
230
236
}))
231
237
switch unifyArray(Belt.Array.zip(raise(TODO("TODO")), hs), ~gen?) {
···
288
294
schematic: x,
289
295
allowed: Array.fromInitializer(~length=Array.length(scope), i => i),
290
296
})
291
-
type gen = ref<int>
292
-
let seen = (g: gen, s: int) => {
293
-
if s >= g.contents {
294
-
g := s + 1
295
-
}
296
-
}
297
297
let fresh = (g: gen, ~replacing as _=?) => {
298
298
let v = g.contents
299
299
g := g.contents + 1