the next generation of the in-browser educational proof assistant
fix parser lib
+123
-195
+41
-22
src/Parser.res
+41
-22
src/Parser.res
···
21
21
))
22
22
}
23
23
24
-
let map = (p: t<'a>, f: 'a => 'b): t<'b> => (str, state) =>
25
-
p(str, state)->Result.map(((res, state)) => (f(res), state))
24
+
let map = (p: t<'a>, f: 'a => 'b): t<'b> =>
25
+
(str, state) => p(str, state)->Result.map(((res, state)) => (f(res), state))
26
26
let pure = (a): t<'a> => (_, state) => Ok((a, state))
27
-
let bind = (p1: t<'a>, p2: 'a => t<'b>): t<'b> => (str, state) =>
28
-
p1(str, state)->Result.flatMap(((res, state)) => p2(res)(str, state))
27
+
let bind = (p1: t<'a>, p2: 'a => t<'b>): t<'b> =>
28
+
(str, state) => p1(str, state)->Result.flatMap(((res, state)) => p2(res)(str, state))
29
29
let apply = (p: t<'a>, pf: t<'a => 'b>): t<'b> => p->bind(a => pf->map(f => f(a)))
30
30
let then = (p1: t<'a>, p2: t<'b>): t<'b> => p1->bind(_ => p2)
31
31
let thenIgnore = (p1: t<'a>, p2: t<'b>): t<'a> => p1->bind(res => p2->map(_ => res))
···
33
33
let fail = (info): t<'a> => (_, state) => Error({message: info, pos: state.pos})
34
34
let void = (p: t<'a>): t<unit> => p->map(_ => ())
35
35
// backtracks by default
36
-
let optional = (p: t<'a>): t<option<'a>> => (str, state) => {
37
-
switch p(str, state) {
38
-
| Ok((res, state)) => Ok((Some(res), state))
39
-
| Error(_) => Ok((None, state))
40
-
}
41
-
}
42
-
let or = (p1: t<'a>, p2: t<'a>): t<'a> => (str, state) =>
43
-
switch p1(str, state) {
44
-
| Ok(r) => Ok(r)
45
-
| Error(_) => p2(str, state)
36
+
let optional = (p: t<'a>): t<option<'a>> =>
37
+
(str, state) => {
38
+
switch p(str, state) {
39
+
| Ok((res, state)) => Ok((Some(res), state))
40
+
| Error(_) => Ok((None, state))
41
+
}
46
42
}
43
+
let or = (p1: t<'a>, p2: t<'a>): t<'a> =>
44
+
(str, state) =>
45
+
switch p1(str, state) {
46
+
| Ok(r) => Ok(r)
47
+
| Error(_) => p2(str, state)
48
+
}
47
49
let choice = (ps: array<t<'a>>): t<'a> => {
48
50
ps->Array.reduce(fail("no matches"), or)
49
51
}
···
142
144
}
143
145
)
144
146
145
-
let peek = (n): t<string> => (str, state) => {
146
-
let res = str->String.slice(~start=state.pos.idx, ~end=state.pos.idx + n)
147
-
Ok((res, state))
148
-
}
147
+
let peek = (n): t<string> =>
148
+
(str, state) => {
149
+
let res = str->String.slice(~start=state.pos.idx, ~end=state.pos.idx + n)
150
+
Ok((res, state))
151
+
}
149
152
150
153
type length = int
151
154
let takeWhileMany = (f: string => option<length>) =>
···
167
170
}
168
171
)
169
172
170
-
let dbg = (p: t<'a>, ~label): t<'a> => {
173
+
let dbg = (p: t<'a>, label): t<'a> => {
171
174
let dbgInfo = title =>
172
175
getCurrentStr->bind(str =>
173
176
getState->map(state => {
···
184
187
})
185
188
}
186
189
187
-
let lexeme = p => p->thenIgnore(regex(%re(`/^\s*/`))->void)
190
+
let lexeme = p => p->thenIgnore(regex(/^\s*/)->void)
188
191
let token = s => string(s)->lexeme
189
192
190
-
let decimal = regex1(%re(`/(\d+)/`))->map(xStr => xStr->Int.fromString->Option.getExn)
191
-
let whitespace = regex(%re(`/\s*/`))->void
193
+
let decimal = regex1(/(\d+)/)->map(xStr => xStr->Int.fromString->Option.getExn)
194
+
let whitespace = regex(/\s*/)->void
195
+
196
+
let lift = (f: string => result<('a, string), string>): t<'a> =>
197
+
getCurrentStr->bind(str =>
198
+
switch f(str) {
199
+
| Ok((res, remaining)) => {
200
+
let length = String.length(str) - String.length(remaining)
201
+
consume(length)->map(_ => res)
202
+
}
203
+
| Error(msg) => fail(msg)
204
+
}
205
+
)
206
+
let liftParse = (
207
+
f: (string, ~scope: array<'m>, ~gen: 'g=?) => result<('a, string), string>,
208
+
~scope: array<'m>,
209
+
~gen: option<'g>=?,
210
+
): t<'a> => lift(s => f(s, ~scope, ~gen?))
+41
-145
src/SExp.res
+41
-145
src/SExp.res
···
250
250
251
251
let prettyPrintSubst = (sub, ~scope) =>
252
252
Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope))
253
-
let symbolRegexpString = `^([^\\s()\\[\\]]+)`
254
-
let varRegexpString = "^\\\\([0-9]+)$"
255
-
let schematicRegexpString = "^\\?([0-9]+)$"
256
-
type lexeme = LParen | RParen | VarT(int) | AtomT(Atom.t) | SchematicT(int)
257
253
let nameRES = "^([^\\s.\\[\\]()]+)\\."
258
254
let prettyPrintMeta = (str: string) => {
259
255
String.concat(str, ".")
···
269
265
}
270
266
}
271
267
}
272
-
let parse = (str: string, ~scope: array<string>, ~gen=?) => {
273
-
let cur = ref(String.make(str))
274
-
let lex: unit => option<lexeme> = () => {
275
-
let str = String.trim(cur.contents)
276
-
cur := str
277
-
let checkVariable = (candidate: string) => {
278
-
let varRegexp = RegExp.fromString(varRegexpString)
279
-
switch Array.indexOf(scope, candidate) {
280
-
| -1 =>
281
-
switch varRegexp->RegExp.exec(candidate) {
282
-
| Some(res') =>
283
-
switch RegExp.Result.matches(res') {
284
-
| [idx] => Some(idx->Int.fromString->Option.getUnsafe)
285
-
| _ => None
286
-
}
287
-
| None => None
268
+
let mkParser = (~scope: array<string>, ~gen=?): Parser.t<t> => {
269
+
open Parser
270
+
let varLit = string("\\")->then(decimal)
271
+
let ident = regex1(/([^\s\(\)]+)/)
272
+
let varIdx =
273
+
varLit
274
+
->or(
275
+
ident->bind(id =>
276
+
switch scope->Array.indexOfOpt(id) {
277
+
| Some(idx) => pure(idx)
278
+
| None => fail("expected variable")
288
279
}
289
-
| idx => Some(idx)
290
-
}
291
-
}
292
-
if String.get(str, 0) == Some("(") {
293
-
cur := String.sliceToEnd(str, ~start=1)
294
-
Some(LParen)
295
-
} else if String.get(str, 0) == Some(")") {
296
-
cur := String.sliceToEnd(str, ~start=1)
297
-
Some(RParen)
298
-
} else {
299
-
let symbolRegexp = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
300
-
switch symbolRegexp->RegExp.exec(str) {
301
-
| None => None
302
-
| Some(res) =>
303
-
switch RegExp.Result.matches(res) {
304
-
| [symb] => {
305
-
let specialSymb = tok => {
306
-
cur := String.sliceToEnd(str, ~start=RegExp.lastIndex(symbolRegexp))
307
-
Some(tok)
308
-
}
309
-
let regularSymb = () => {
310
-
// FIX: not ideal to throw away symbol error message
311
-
Console.log(("current", cur.contents))
312
-
Atom.parse(cur.contents, ~scope)
313
-
->Util.Result.ok
314
-
->Option.map(((s, rest)) => {
315
-
cur := rest
316
-
Console.log(("parsed", s, cur.contents))
317
-
AtomT(s)
318
-
})
319
-
}
320
-
switch checkVariable(symb) {
321
-
| Some(idx) => specialSymb(VarT(idx))
322
-
| None => {
323
-
let schematicRegexp = RegExp.fromString(schematicRegexpString)
324
-
switch schematicRegexp->RegExp.exec(symb) {
325
-
| None => regularSymb()
326
-
| Some(res') =>
327
-
switch RegExp.Result.matches(res') {
328
-
| [s] => specialSymb(SchematicT(s->Int.fromString->Option.getUnsafe))
329
-
| _ => regularSymb()
330
-
}
331
-
}
332
-
}
333
-
}
334
-
}
335
-
| _ => None
336
-
}
337
-
}
338
-
}
339
-
}
280
+
),
281
+
)
282
+
->lexeme
283
+
let var = varIdx->map(idx => Var({idx: idx}))
340
284
341
-
let peek = () => {
342
-
// a bit slow, better would be to keep a backlog of lexed tokens..
343
-
let str = String.make(cur.contents)
344
-
let tok = lex()
345
-
cur := str
346
-
tok
347
-
}
348
-
exception ParseError(string)
349
-
let rec parseExp = () => {
350
-
let tok = peek()
351
-
switch tok {
352
-
| Some(AtomT(s)) => {
353
-
let _ = lex()
354
-
Some(Atom(s))
355
-
}
356
-
| Some(VarT(idx)) => {
357
-
let _ = lex()
358
-
Some(Var({idx: idx}))
359
-
}
360
-
| Some(SchematicT(num)) => {
361
-
let _ = lex()
362
-
switch lex() {
363
-
| Some(LParen) => {
364
-
let it = ref(None)
365
-
let bits = []
366
-
let getVar = (t: option<lexeme>) =>
367
-
switch t {
368
-
| Some(VarT(idx)) => Some(idx)
369
-
| _ => None
370
-
}
371
-
while {
372
-
it := lex()
373
-
it.contents->getVar->Option.isSome
374
-
} {
375
-
Array.push(bits, it.contents->getVar->Option.getUnsafe)
376
-
}
377
-
switch it.contents {
378
-
| Some(RParen) =>
379
-
switch gen {
380
-
| Some(g) => {
381
-
seen(g, num)
382
-
Some(Schematic({schematic: num, allowed: bits}))
383
-
}
384
-
| None => throw(ParseError("Schematics not allowed here"))
385
-
}
386
-
| _ => throw(ParseError("Expected closing parenthesis"))
387
-
}
388
-
}
389
-
| _ => throw(ParseError("Expected opening parenthesis"))
390
-
}
391
-
}
392
-
| Some(LParen) => {
393
-
let _ = lex()
394
-
let bits = []
395
-
let it = ref(None)
396
-
while {
397
-
it := parseExp()
398
-
it.contents->Option.isSome
399
-
} {
400
-
Array.push(bits, it.contents->Option.getUnsafe)
401
-
}
402
-
switch lex() {
403
-
| Some(RParen) => Some(Compound({subexps: bits}))
404
-
| _ => throw(ParseError("Expected closing parenthesis"))
405
-
}
406
-
}
407
-
| _ => None
408
-
}
409
-
}
410
-
switch parseExp() {
411
-
| exception ParseError(s) => Error(s)
412
-
| None => Error("No expression to parse")
413
-
| Some(e) => Ok((e, cur.contents))
414
-
}
285
+
let schemaLit =
286
+
string("?")
287
+
->then(decimal)
288
+
->bind(schematic =>
289
+
many(varIdx)
290
+
->between(token("("), token(")"))
291
+
->map(allowed => {
292
+
gen->Option.map(g => allowed->Array.forEach(n => seen(g, n)))->ignore
293
+
Schematic({schematic, allowed})
294
+
})
295
+
)
296
+
let inner = fix(f =>
297
+
choice([
298
+
schemaLit,
299
+
var,
300
+
liftParse(Atom.parse, ~scope, ~gen?)->map(a => Atom(a)),
301
+
many(f)
302
+
->between(token("("), token(")"))
303
+
->map(subexps => Compound({subexps: subexps})),
304
+
])->lexeme
305
+
)
306
+
whitespace->then(inner)
307
+
}
308
+
309
+
let parse = (str: string, ~scope: array<string>, ~gen=?) => {
310
+
Parser.runParser(mkParser(~scope, ~gen?), str)->Result.mapError(e => e.message)
415
311
}
416
312
417
313
let rec concrete = t =>
+5
-5
src/StringA.res
+5
-5
src/StringA.res
···
479
479
}
480
480
481
481
let parenthesise = f =>
482
-
[
483
-
<span className="symbol" key={"-1"}> {React.string("(")} </span>,
484
-
...f,
485
-
<span className="symbol" key={"-2"}> {React.string(")")} </span>,
486
-
]
482
+
Array.flat([
483
+
[<span className="symbol" key={"-1"}> {React.string("(")} </span>],
484
+
f,
485
+
[<span className="symbol" key={"-2"}> {React.string(")")} </span>],
486
+
])
487
487
488
488
let intersperse = a => Util.intersperse(a, ~with=React.string(" "))
489
489
+36
-23
tests/RuleTest.res
+36
-23
tests/RuleTest.res
···
31
31
}
32
32
}
33
33
34
-
// zoraBlock("string terms", t => {
35
-
// module T = MakeTest(StringSExp, StringSExpJ)
36
-
// t->T.testParseInner(
37
-
// `[s1. ("$s1" p) |- ("($s1)" p)]`,
38
-
// {
39
-
// vars: ["s1"],
40
-
// premises: [
41
-
// {
42
-
// vars: [],
43
-
// premises: [],
44
-
// conclusion: StringSExp.Compound(
45
-
// [StringA.Atom.Var({idx: 0})],
46
-
// SExp.pAtom("p")->StringA.AtomJudgment.ConstS->StringSymbolic.Atom,
47
-
// ),
48
-
// },
49
-
// ],
50
-
// conclusion: (
51
-
// [StringA.Atom.String("("), StringA.Atom.Var({idx: 0}), StringA.Atom.String(")")],
52
-
// SExp.pAtom("p")->StringA.AtomJudgment.ConstS->StringSymbolic.Atom,
53
-
// ),
54
-
// },
55
-
// )
56
-
// })
34
+
zoraBlock("string terms", t => {
35
+
module StringSymbol = AtomDef.MakeAtomAndView(
36
+
Coercible.StringA,
37
+
StringA.AtomView,
38
+
Coercible.Symbolic,
39
+
Symbolic.AtomView,
40
+
)
41
+
module StringSExp = SExp.Make(StringSymbol.Atom)
42
+
module T = MakeTest(StringSExp, StringSExp)
43
+
t->T.testParseInner(
44
+
`[s1. ("$s1" p) |- ("($s1)" p)]`,
45
+
{
46
+
vars: ["s1"],
47
+
premises: [
48
+
{
49
+
vars: [],
50
+
premises: [],
51
+
conclusion: StringSExp.Compound({
52
+
subexps: [
53
+
[StringA.Var({idx: 0})]->StringSymbol.Atom.Left->StringSExp.Atom,
54
+
"p"->StringSymbol.Atom.Right->StringSExp.Atom,
55
+
],
56
+
}),
57
+
},
58
+
],
59
+
conclusion: StringSExp.Compound({
60
+
subexps: [
61
+
[StringA.String("("), StringA.Var({idx: 0}), StringA.String(")")]
62
+
->StringSymbol.Atom.Left
63
+
->StringSExp.Atom,
64
+
"p"->StringSymbol.Atom.Right->StringSExp.Atom,
65
+
],
66
+
}),
67
+
},
68
+
)
69
+
})