the next generation of the in-browser educational proof assistant
1type sourceloc = {
2 line: int,
3 col: int,
4 idx: int,
5}
6
7type info = {
8 msg?: string,
9 expects: array<string>,
10}
11
12type err = {
13 info: info,
14 pos: sourceloc,
15}
16
17type state = {pos: sourceloc}
18
19type t<'a> = (string, state) => result<('a, state), err>
20
21let infoPretty = (info: info) => {
22 let expectedMsg = switch info.expects {
23 | [] => None
24 | [expect] => Some(`expected ${expect}`)
25 | _ => {
26 let n = Array.length(info.expects)
27 let first = info.expects->Array.slice(~start=0, ~end=n - 1)->Array.join(", ")
28 Some(`expected ${first}, or ${info.expects[n - 1]->Option.getUnsafe}`)
29 }
30 }
31 switch (info.msg, expectedMsg) {
32 | (Some(infoMsg), Some(expectedMsg)) => `parse failed: ${infoMsg}\n ${expectedMsg}`
33 | (None, Some(msg)) | (Some(msg), None) => `parse failed: ${msg}`
34 | (None, None) => `parse failed`
35 }
36}
37let initialState = {pos: {line: 1, col: 1, idx: 0}}
38let runParser = (p: t<'a>, str: string): result<('a, string), string> => {
39 p(str, initialState)
40 ->Result.map(((res, state)) => (res, str->String.sliceToEnd(~start=state.pos.idx)))
41 ->Result.mapError(err => {
42 `around ${str->String.slice(~start=err.pos.idx, ~end=err.pos.idx + 5)}:\n${infoPretty(
43 err.info,
44 )}`
45 })
46}
47
48let map = (p: t<'a>, f: 'a => 'b): t<'b> =>
49 (str, state) => p(str, state)->Result.map(((res, state)) => (f(res), state))
50let mapError = (p: t<'a>, f: err => err) => (str, state) => p(str, state)->Result.mapError(f)
51let label = (p: t<'a>, label: string) =>
52 p->mapError(err => {...err, info: {...err.info, expects: [label]}})
53let pure = (a): t<'a> => (_, state) => Ok((a, state))
54let bind = (p1: t<'a>, p2: 'a => t<'b>): t<'b> =>
55 (str, state) => p1(str, state)->Result.flatMap(((res, state)) => p2(res)(str, state))
56let apply = (p: t<'a>, pf: t<'a => 'b>): t<'b> => p->bind(a => pf->map(f => f(a)))
57let then = (p1: t<'a>, p2: t<'b>): t<'b> => p1->bind(_ => p2)
58let thenIgnore = (p1: t<'a>, p2: t<'b>): t<'a> => p1->bind(res => p2->map(_ => res))
59
60let fail = (info): t<'a> => (_, state) => Error({info: {msg: info, expects: []}, pos: state.pos})
61let expected = (expects: array<string>, ~msg=?): t<'a> =>
62 (_, state) => Error({info: {?msg, expects}, pos: state.pos})
63let void = (p: t<'a>): t<unit> => p->map(_ => ())
64// backtracks by default
65let or = (p1: t<'a>, p2: t<'a>): t<'a> =>
66 (str, state) =>
67 switch p1(str, state) {
68 | Ok(r) => Ok(r)
69 | Error(e1) =>
70 p2(str, state)->Result.mapError(e2 => {
71 ...e2,
72 info: {expects: Array.concat(e1.info.expects, e2.info.expects)},
73 })
74 }
75let optional = (p: t<'a>): t<option<'a>> => p->map(a => Some(a))->or(pure(None))
76let choice = (ps: array<t<'a>>): t<'a> => {
77 ps->Array.reduce(fail("no matches"), or)
78}
79
80let getState: t<state> = (_, state) => Ok((state, state))
81let setState = (newState: state): t<unit> => (_, _) => Ok(((), newState))
82let modifyState = (f: state => state) => getState->bind(state => setState(f(state)))
83let readStr: t<string> = (str, state) => Ok((str, state))
84let getCurrentStr: t<string> = (str, state) => Ok((
85 str->String.sliceToEnd(~start=state.pos.idx),
86 state,
87))
88
89let eof: t<bool> = getState->bind(state => readStr->map(str => state.pos.idx >= str->String.length))
90
91// fixpoints using references as a layer of indirection are necessary because
92// the compiler complains very ambiguously about not knowing the size of
93// (directly) recursive combinators
94let fix = (f: t<'a> => t<'a>): t<'a> => {
95 let pRef = ref(fail("umm"))
96 pRef := f((str, state) => pRef.contents(str, state))
97 pRef.contents
98}
99
100let many = p =>
101 fix(f =>
102 optional(p)->bind(o =>
103 switch o {
104 | Some(res) => f->map(l => l->List.add(res))
105 | None => pure(list{})
106 }
107 )
108 )->map(List.toArray)
109let between = (inner: t<'a>, o1: t<string>, o2: t<string>): t<'a> => o1->then(inner)->thenIgnore(o2)
110let consume = (l: int): t<string> =>
111 getCurrentStr->bind(str => {
112 if str->String.length < l {
113 fail("tried to consume too much")
114 } else {
115 let consumed = str->String.slice(~start=0, ~end=l)
116 let vOffset = consumed->String.split("\n")->Array.length - 1
117 let hOffset = consumed->String.length - consumed->String.lastIndexOfOpt("\n")->Option.getOr(0)
118 modifyState(state => {
119 pos: {
120 col: vOffset > 0 ? hOffset : state.pos.col + hOffset,
121 line: state.pos.line + vOffset,
122 idx: state.pos.idx + l,
123 },
124 })->then(pure(consumed))
125 }
126 })
127
128let execRe = (re, str) => {
129 re
130 ->RegExp.exec(str)
131 ->Option.map(result => {
132 open RegExp.Result
133 (matches(result), fullMatch(result)->String.length)
134 })
135}
136
137// this will be released in Core in 12.0.0.4, remove then
138@get external regexpFlags: RegExp.t => string = "flags"
139
140let string = s =>
141 getCurrentStr->bind(str =>
142 if str->String.startsWith(s) {
143 consume(String.length(s))->then(pure(s))
144 } else {
145 expected([`literal ${s}`])
146 }
147 )
148
149let regex = (re: RegExp.t): t<array<string>> => {
150 let wrapped = {
151 let source = re->RegExp.source
152 if source->String.startsWith("^") {
153 re
154 } else {
155 RegExp.fromStringWithFlags(`^${source}`, ~flags=re->regexpFlags)
156 }
157 }
158 getCurrentStr->bind(str =>
159 switch execRe(wrapped, str) {
160 | Some((matches, l)) => consume(l)->then(pure(matches))
161 | None => expected([`regex pattern ${re->RegExp.source}`])
162 }
163 )
164}
165
166let regex1 = (re: RegExp.t): t<string> =>
167 regex(re)->bind(matches =>
168 switch matches {
169 | [x] => pure(x)
170 | _ => fail("more than one match")
171 }
172 )
173
174let peek = (n): t<string> =>
175 (str, state) => {
176 let res = str->String.slice(~start=state.pos.idx, ~end=state.pos.idx + n)
177 Ok((res, state))
178 }
179
180type length = int
181let takeWhileMany = (f: string => option<length>) =>
182 fix(p =>
183 getCurrentStr->bind(str =>
184 switch f(str) {
185 | Some(length) => consume(length)->bind(s => p->map(s' => String.concat(s, s')))
186 | None => pure("")
187 }
188 )
189 )
190
191let takeWhile = (f: string => bool) =>
192 takeWhileMany(s =>
193 if f(s) {
194 Some(1)
195 } else {
196 None
197 }
198 )
199
200let dbg = (p: t<'a>, label): t<'a> => {
201 let dbgInfo = title =>
202 getCurrentStr->bind(str =>
203 getState->map(state => {
204 let currSurr = `${str->String.slice(~start=0, ~end=10)}...`
205 let stateStr = `${state.pos.line->Int.toString}:${state.pos.col->Int.toString}`
206 Console.log(`${title} ${label} at:\n${currSurr}\nstate: ${stateStr}`)
207 })
208 )
209 dbgInfo("enter")
210 ->then(p)
211 ->bind(res => {
212 Console.log(("successfully parsed", res))
213 dbgInfo("exit")->map(_ => res)
214 })
215}
216
217let lexeme = p => p->thenIgnore(regex(/^\s*/)->void)
218let token = s => string(s)->lexeme
219
220let decimal = regex1(/(\d+)/)->map(xStr => xStr->Int.fromString->Option.getExn)
221let whitespace = regex(/\s*/)->void
222
223let lift = (f: string => result<('a, string), string>): t<'a> =>
224 getCurrentStr->bind(str =>
225 switch f(str) {
226 | Ok((res, remaining)) => {
227 let length = String.length(str) - String.length(remaining)
228 consume(length)->map(_ => res)
229 }
230 | Error(msg) => fail(msg)
231 }
232 )
233let liftParse = (
234 f: (string, ~scope: array<'m>, ~gen: 'g=?) => result<('a, string), string>,
235 ~scope: array<'m>,
236 ~gen: option<'g>=?,
237): t<'a> => lift(s => f(s, ~scope, ~gen?))