the next generation of the in-browser educational proof assistant
use env
+24
-6
+24
-6
src/HOTerm.res
+24
-6
src/HOTerm.res
···
427
427
}
428
428
type env = Map.t<string, int>
429
429
let incrEnv = (env: env): env => {
430
-
let nu = Map.make()
430
+
let nu: env = Map.make()
431
431
Map.entries(env)->Iterator.forEach(opt =>
432
432
switch opt {
433
433
| None => ()
···
436
436
)
437
437
nu
438
438
}
439
-
let rec parseAll = (simple: simple, ~scope: array<string>, ~gen=?): t => {
439
+
let envFromScope = (scope: array<string>): env => {
440
+
let nu: env = Map.make()
441
+
scope->Array.forEachWithIndex((name, idx) => {
442
+
nu->Map.set(name, idx)
443
+
})
444
+
nu
445
+
}
446
+
let envPushLambda = (env: env, name: string): env => {
447
+
let nu = incrEnv(env)
448
+
nu->Map.set(name, 0)
449
+
nu
450
+
}
451
+
let rec parseAll = (simple: simple, ~env: env, ~gen=?): t => {
440
452
switch simple {
441
453
| ListS({xs}) => {
442
-
let ts = xs->Array.map(x => parseAll(x, ~scope, ~gen?))
454
+
let ts = xs->Array.map(x => parseAll(x, ~env, ~gen?))
443
455
if ts->Array.length == 0 {
444
456
raise(ParseError("empty list"))
445
457
} else {
···
448
460
->Array.reduce(ts[0]->Option.getUnsafe, (acc, x) => App({func: acc, arg: x}))
449
461
}
450
462
}
451
-
| AtomS({name}) => Symbol({name: name})
463
+
| AtomS({name}) =>
464
+
if env->Map.has(name) {
465
+
let idx = env->Map.get(name)->Option.getUnsafe
466
+
Var({idx: idx})
467
+
} else {
468
+
Symbol({name: name})
469
+
}
452
470
| VarS({idx}) => Var({idx: idx})
453
471
| LambdaS({name, body}) =>
454
472
Lam({
455
473
name,
456
-
body: parseAll(body, ~scope, ~gen?),
474
+
body: parseAll(body, ~env=envPushLambda(env, name), ~gen?),
457
475
})
458
476
}
459
477
}
···
474
492
let parse = (str: string, ~scope: array<string>, ~gen=?) => {
475
493
try {
476
494
let (simple, rest) = parseSimple(str)
477
-
Ok((parseAll(simple, ~scope, ~gen?), rest))
495
+
Ok((parseAll(simple, ~env=envFromScope(scope), ~gen?), rest))
478
496
} catch {
479
497
| ParseError(msg) => Error(msg)
480
498
}