the next generation of the in-browser educational proof assistant
parse for Schematic
+9
+9
src/HOTerm.res
+9
src/HOTerm.res
···
393
393
| ListS({xs: array<simple>})
394
394
| AtomS({name: string})
395
395
| VarS({idx: int})
396
+
| SchematicS({schematic: int})
396
397
| LambdaS({name: string, body: simple})
397
398
let rec parseSimple = (str: string): (simple, string) => {
398
399
let (t0, rest) = tokenize(str)
···
432
433
}
433
434
| RParen => raise(ParseError("unexpected right parenthesis"))
434
435
| VarT(idx) => (VarS({idx: idx}), rest)
436
+
| SchematicT(schematic) => (SchematicS({schematic: schematic}), rest)
435
437
| AtomT(name) => (AtomS({name: name}), rest)
436
438
| DotT => raise(ParseError("unexpected dot"))
437
439
| EOF => raise(ParseError("unexpected end of file"))
···
480
482
Symbol({name: name})
481
483
}
482
484
| VarS({idx}) => Var({idx: idx})
485
+
| SchematicS({schematic}) =>
486
+
Schematic({
487
+
schematic,
488
+
allowed: env
489
+
->Map.values
490
+
->Core__Iterator.toArray,
491
+
})
483
492
| LambdaS({name, body}) =>
484
493
Lam({
485
494
name,