the next generation of the in-browser educational proof assistant
implement sexp parser with new lib
+59
-14
+54
-13
src/Parser.res
+54
-13
src/Parser.res
···
4
4
idx: int,
5
5
}
6
6
7
-
type parserError<'info> = {
7
+
type err<'info> = {
8
8
message: 'info,
9
9
pos: sourceloc,
10
10
}
11
11
12
-
type parserState = {pos: sourceloc}
12
+
type state = {pos: sourceloc}
13
13
14
-
type t<'a> = (string, parserState) => result<('a, parserState), parserError<string>>
14
+
type t<'a> = (string, state) => result<('a, state), err<string>>
15
15
16
16
let initialState = {pos: {line: 1, col: 1, idx: 0}}
17
-
let runParser = (p: t<'a>, str: string): result<('a, string), parserError<string>> => {
17
+
let runParser = (p: t<'a>, str: string): result<('a, string), err<string>> => {
18
18
p(str, initialState)->Result.map(((res, state)) => (
19
19
res,
20
20
str->String.sliceToEnd(~start=state.pos.idx),
···
27
27
let bind = (p1: t<'a>, p2: 'a => t<'b>): t<'b> => (str, state) =>
28
28
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
-
31
30
let then = (p1: t<'a>, p2: t<'b>): t<'b> => p1->bind(_ => p2)
32
31
let thenIgnore = (p1: t<'a>, p2: t<'b>): t<'a> => p1->bind(res => p2->map(_ => res))
32
+
33
+
let fail = (info): t<'a> => (_, state) => Error({message: info, pos: state.pos})
34
+
let void = (p: t<'a>): t<unit> => p->map(_ => ())
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
+
}
33
42
let or = (p1: t<'a>, p2: t<'a>): t<'a> => (str, state) =>
34
43
switch p1(str, state) {
35
44
| Ok(r) => Ok(r)
36
45
| Error(_) => p2(str, state)
37
46
}
38
-
let fail = (info): t<'a> => (_, state) => Error({message: info, pos: state.pos})
39
-
let void = (p: t<'a>): t<unit> => p->map(_ => ())
47
+
let choice = (ps: array<t<'a>>): t<'a> => {
48
+
ps->Array.reduce(fail("no matches"), or)
49
+
}
40
50
41
-
let getState: t<parserState> = (_, state) => Ok((state, state))
42
-
let setState = (newState: parserState): t<unit> => (_, _) => Ok(((), newState))
43
-
let modifyState = (f: parserState => parserState) => getState->bind(state => setState(f(state)))
51
+
let getState: t<state> = (_, state) => Ok((state, state))
52
+
let setState = (newState: state): t<unit> => (_, _) => Ok(((), newState))
53
+
let modifyState = (f: state => state) => getState->bind(state => setState(f(state)))
44
54
let readStr: t<string> = (str, state) => Ok((str, state))
45
55
let getCurrentStr: t<string> = (str, state) => Ok((
46
56
str->String.sliceToEnd(~start=state.pos.idx),
···
49
59
50
60
let eof: t<bool> = getState->bind(state => readStr->map(str => state.pos.idx >= str->String.length))
51
61
52
-
// fixpoints are necessary because rescript compiler complains very ambiguously
53
-
// about not knowing the size of recursive combinators
62
+
// fixpoints using references as a layer of indirection are necessary because
63
+
// the compiler complains very ambiguously about not knowing the size of
64
+
// (directly) recursive combinators
54
65
let fix = (f: t<'a> => t<'a>): t<'a> => {
55
66
let pRef = ref(fail("umm"))
56
67
pRef := f((str, state) => pRef.contents(str, state))
57
68
pRef.contents
58
69
}
59
70
71
+
let many = p =>
72
+
fix(f =>
73
+
optional(p)->bind(o =>
74
+
switch o {
75
+
| Some(res) => f->map(l => l->List.add(res))
76
+
| None => pure(list{})
77
+
}
78
+
)
79
+
)->map(List.toArray)
80
+
let between = (inner: t<'a>, o1: t<string>, o2: t<string>): t<'a> => o1->then(inner)->thenIgnore(o2)
60
81
let consume = (l: int): t<string> =>
61
82
getCurrentStr->bind(str => {
62
83
if str->String.length < l {
···
92
113
if str->String.startsWith(s) {
93
114
consume(String.length(s))->then(pure(s))
94
115
} else {
95
-
fail("doesn't start with string")
116
+
fail(`${str->String.slice(~start=0, ~end=10)} doesn't start with string ${s}`)
96
117
}
97
118
)
98
119
···
146
167
}
147
168
)
148
169
170
+
let dbg = (p: t<'a>, ~label): t<'a> => {
171
+
let dbgInfo = title =>
172
+
getCurrentStr->bind(str =>
173
+
getState->map(state => {
174
+
let currSurr = `${str->String.slice(~start=0, ~end=10)}...`
175
+
let stateStr = `${state.pos.line->Int.toString}:${state.pos.col->Int.toString}`
176
+
Console.log(`${title} ${label} at:\n${currSurr}\nstate: ${stateStr}`)
177
+
})
178
+
)
179
+
dbgInfo("enter")
180
+
->then(p)
181
+
->bind(res => {
182
+
Console.log(("successfully parsed", res))
183
+
dbgInfo("exit")->map(_ => res)
184
+
})
185
+
}
186
+
149
187
let lexeme = p => p->thenIgnore(regex(%re(`/^\s*/`))->void)
150
188
let token = s => string(s)->lexeme
189
+
190
+
let decimal = regex1(%re(`/(\d+)/`))->map(xStr => xStr->Int.fromString->Option.getExn)
191
+
let whitespace = regex(%re(`/\s*/`))->void
+1
-1
src/Rule.res
+1
-1
src/Rule.res
···
2
2
// the tree sitter plugin hates backslashes in string literals unless they're on the top
3
3
// level..
4
4
let ruleNamePattern = "^[^|()\\s\\-—][^()\\s]*"
5
-
let vinculumRES = "^\s*\\n\\s*[-—][-—][\\-—]+[ \t]*([^()|\\s\\-—][^()\\s]*)?"
5
+
let vinculumRES = "^\\n?\\s*[-—][-—][\\-—]+[ \t]*([^()|\\s\\-—][^()\\s]*)?"
6
6
module Make = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
7
7
type rec t = {vars: array<Term.meta>, premises: array<t>, conclusion: Judgment.t}
8
8
let rec substitute = (rule: t, subst: Term.subst) => {
+4
tests/ParserTests.res
+4
tests/ParserTests.res
···
10
10
}
11
11
12
12
zoraBlock("parse", t => {
13
+
open Parser
13
14
t->testParse(P.string("a"), "a", ~expect="a")
14
15
t->testParse(P.token("a"), "a \n\r", ~expect="a")
15
16
t->testParse(P.string("a")->P.or(P.string("b")), "b", ~expect="b")
16
17
let abs =
17
18
P.takeWhile(s => s->String.startsWith("a"))->P.bind(res => P.string("b")->P.map(b => (res, b)))
18
19
t->testParse(abs, "aaaab", ~expect=("aaaa", "b"))
20
+
let brackets = many(lexeme(decimal))->between(token("("), token(")"))
21
+
t->testParse(brackets, "(1)", ~expect=[1])
22
+
t->testParse(brackets, "(1 2 3)", ~expect=[1, 2, 3])
19
23
})