the next generation of the in-browser educational proof assistant
use schematicRegexpString
+18
-6
+18
-6
src/HOTerm.res
+18
-6
src/HOTerm.res
···
331
331
->String.concat(")")
332
332
}
333
333
let symbolRegexpString = "^([^\\s()]+)"
334
-
let varRegexpString = "^\\\\([0-9]+)$"
335
-
let schematicRegexpString = "^\\?([0-9]+)$"
336
334
let nameRES = "^([^\\s.\\[\\]()]+)\\."
337
335
exception ParseError(string)
338
-
type token = LParen | RParen | VarT(int) | AtomT(string) | DotT | EOF
336
+
type token = LParen | RParen | VarT(int) | SchematicT(int) | AtomT(string) | DotT | EOF
339
337
let trim = (str: string): string => {
340
338
str->String.trim
341
339
}
340
+
let varRegexpString = "^\\\\([0-9]+)$"
341
+
let schematicRegexpString = "^\\?([0-9]+)$"
342
342
let tokenize = (str0: string): (token, string) => {
343
343
let str = str0->trim
344
344
if str->String.length == 0 {
···
351
351
| "." => (DotT, rest())
352
352
| "\\" => {
353
353
let re = RegExp.fromStringWithFlags(varRegexpString, ~flags="y")
354
-
switch re->RegExp.exec(rest()) {
355
-
| None => raise(ParseError("invalid variable"))
354
+
switch re->RegExp.exec(str) {
355
+
| None =>
356
+
let re1 = RegExp.fromStringWithFlags(schematicRegexpString, ~flags="y")
357
+
switch re1->RegExp.exec(str) {
358
+
| None => raise(ParseError("invalid variable or schematic"))
359
+
| Some(res) =>
360
+
switch RegExp.Result.matches(res) {
361
+
| [n] => (
362
+
SchematicT(n->Int.fromString->Option.getUnsafe),
363
+
String.sliceToEnd(str, ~start=RegExp.lastIndex(re1)),
364
+
)
365
+
| _ => raise(ParseError("invalid schematic"))
366
+
}
367
+
}
356
368
| Some(res) =>
357
369
switch RegExp.Result.matches(res) {
358
370
| [n] => (
359
371
VarT(n->Int.fromString->Option.getUnsafe),
360
-
String.sliceToEnd(rest(), ~start=RegExp.lastIndex(re)),
372
+
String.sliceToEnd(str, ~start=RegExp.lastIndex(re)),
361
373
)
362
374
| _ => raise(ParseError("invalid variable"))
363
375
}