the next generation of the in-browser educational proof assistant
1module IntCmp = Belt.Id.MakeComparable({
2 type t = int
3 let cmp = Pervasives.compare
4})
5
6type rec t =
7 | Symbol({name: string, constructor: bool})
8 | Var({idx: int})
9 | Schematic({schematic: int})
10 | Lam({name: string, body: t})
11 | App({func: t, arg: t})
12 // Unallowed is used internally in unify, where Nipkow 1993 uses Var(-infinity)
13 | Unallowed
14type meta = string
15type schematic = int
16type subst = Belt.Map.Int.t<t>
17let substHas = (subst: subst, schematic: schematic) => subst->Belt.Map.Int.has(schematic)
18let substGet = (subst: subst, schematic: schematic) => subst->Belt.Map.Int.get(schematic)
19let mapSubst = (m: subst, f: t => t): subst => {
20 m->Belt.Map.Int.map(f)
21}
22let substEqual = (m1, m2) => m1 == m2
23let makeSubst = () => {
24 Belt.Map.Int.empty
25}
26let mergeSubsts = (m1: subst, m2: subst) =>
27 Belt.Map.Int.merge(m1, m2, (_, o1, o2) =>
28 switch (o1, o2) {
29 | (Some(v), _) | (_, Some(v)) => Some(v)
30 | (None, None) => None
31 }
32 )
33let rec equivalent = (a: t, b: t) => {
34 switch (a, b) {
35 | (Symbol({name: na}), Symbol({name: nb})) => na == nb
36 | (Var({idx: ia}), Var({idx: ib})) => ia == ib
37 | (Schematic({schematic: sa}), Schematic({schematic: sb})) => sa == sb
38 | (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => equivalent(ba, bb)
39 | (App({func: fa, arg: aa}), App({func: fb, arg: ab})) => equivalent(fa, fb) && equivalent(aa, ab)
40 | (Unallowed, Unallowed) => false
41 | (_, _) => false
42 }
43}
44type gen = ref<int>
45let seen = (g: gen, s: int) => {
46 if s >= g.contents {
47 g := s + 1
48 }
49}
50let fresh = (g: gen, ~replacing as _=?) => {
51 let v = g.contents
52 g := g.contents + 1
53 v
54}
55let rec schematicsIn = (subst: subst, it: t): Belt.Set.t<schematic, IntCmp.identity> =>
56 switch it {
57 | Schematic({schematic, _}) if subst->substHas(schematic) =>
58 let found = subst->substGet(schematic)->Option.getExn
59 schematicsIn(subst, found)
60 | Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
61 | Lam({body}) => schematicsIn(subst, body)
62 | App({func, arg}) => Belt.Set.union(schematicsIn(subst, func), schematicsIn(subst, arg))
63 | Unallowed | Symbol(_) | Var(_) => Belt.Set.make(~id=module(IntCmp))
64 }
65let occ = (schematic: schematic, subst: subst, t: t): bool => {
66 let set = schematicsIn(subst, t)
67 set->Belt.Set.has(schematic)
68}
69let rec freeVarsIn = (subst: subst, it: t): Belt.Set.t<int, IntCmp.identity> =>
70 switch it {
71 | Schematic({schematic, _}) if subst->substHas(schematic) =>
72 let found = subst->substGet(schematic)->Option.getExn
73 freeVarsIn(subst, found)
74 | Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
75 | Lam({name: _, body}) =>
76 freeVarsIn(subst, body)
77 ->Belt.Set.toArray
78 ->Array.filterMap(v =>
79 if v >= 1 {
80 Some(v - 1)
81 } else {
82 None
83 }
84 )
85 ->Belt.Set.fromArray(~id=module(IntCmp))
86 | App({func, arg}) => Belt.Set.union(freeVarsIn(subst, func), freeVarsIn(subst, arg))
87 | Unallowed | Symbol(_) | Schematic(_) => Belt.Set.make(~id=module(IntCmp))
88 }
89let freeVarsContains = (term: t, subst: subst, idx: int): bool => {
90 let set = freeVarsIn(subst, term)
91 set->Belt.Set.has(idx)
92}
93// f might map an index to a new one (Ok(newIdx)) or to a term (Error(t) with t(from)).
94// Note that Ok and Error here are not used for success or failure; they are just two cases distinguishing between an index and a term.
95let rec mapbind0 = (term: t, f: int => result<int, int => t>, ~from: int=0): t =>
96 switch term {
97 | Symbol(_) => term
98 | Var({idx}) =>
99 if idx >= from {
100 switch f(idx - from) {
101 | Ok(newIdx) =>
102 let new = newIdx + from
103 if new < 0 {
104 throw(Util.Err("mapbind: negative index"))
105 }
106 Var({
107 idx: new,
108 })
109 | Error(t) => t(from)
110 }
111 } else {
112 term
113 }
114 | Schematic({schematic}) =>
115 Schematic({
116 schematic: schematic,
117 })
118 | Lam({name, body}) =>
119 Lam({
120 name,
121 body: mapbind0(body, f, ~from=from + 1),
122 })
123 | App({func, arg}) =>
124 App({
125 func: mapbind0(func, f, ~from),
126 arg: mapbind0(arg, f, ~from),
127 })
128 | Unallowed => Unallowed
129 }
130let mapbind = (term: t, f: int => int, ~from: int=0): t => mapbind0(term, idx => Ok(f(idx)), ~from)
131let upshift = (term: t, amount: int, ~from: int=0) => mapbind(term, idx => idx + amount, ~from)
132let downshift = (term: t, amount: int, ~from: int=1) => {
133 if amount > from {
134 throw(Util.Err("downshift amount must be less than from"))
135 }
136 mapbind(term, idx => idx - amount, ~from)
137}
138let lookup = (term: t, subst: array<(t, t)>): option<t> => {
139 subst
140 ->Array.find(((from, _)) => equivalent(term, from))
141 ->Option.map(((_, to)) => to)
142}
143let upshift_tt = (subst: array<(t, t)>, ~amount: int=1): array<(t, t)> => {
144 subst->Array.map(((a, b)) => (upshift(a, amount), upshift(b, amount)))
145}
146// where pattern unification used mapbind we will need to use discharge for FCU
147//
148// When `prune` is true, it marks “dead” variables as Unallowed. Nipkow 1993 uses Var(-infinity) for this in the de Bruijn’s notation implementation.
149// Nipkow 1993's non de Bruijn implementation handle this logic in `proj`. Similarly Makoto Hamana's paper uses `elem` and `subst` in `prune`
150let rec discharge = (subst: array<(t, t)>, term: t, ~prune: bool): t => {
151 switch lookup(term, subst) {
152 | Some(found) => found
153 | None =>
154 switch term {
155 | App({func, arg}) =>
156 App({func: discharge(subst, func, ~prune), arg: discharge(subst, arg, ~prune)})
157 // Lam case is not actually needed by FCU
158 | Lam({name, body}) => Lam({name, body: discharge(upshift_tt(subst), body, ~prune)})
159 | Var(_) if prune => Unallowed
160 | Var(_) | Schematic(_) | Symbol(_) | Unallowed => term
161 }
162 }
163}
164let emptySubst: subst = Belt.Map.Int.empty
165let substAdd = (subst: subst, schematic: schematic, term: t) => {
166 assert(schematic >= 0)
167 assert(subst->Belt.Map.Int.has(schematic) == false)
168 subst->Belt.Map.Int.set(schematic, term)
169}
170let rec substitute = (term: t, subst: subst) =>
171 switch term {
172 | Schematic({schematic, _}) =>
173 switch Belt.Map.Int.get(subst, schematic) {
174 | None => term
175 | Some(found) => found
176 }
177 | Lam({name, body}) =>
178 Lam({
179 name,
180 // upshift is not needed for pattern unification, but it is safer to have upshift here
181 body: substitute(body, subst->Belt.Map.Int.map(t => upshift(t, 1))),
182 })
183 | App({func, arg}) =>
184 App({
185 func: substitute(func, subst),
186 arg: substitute(arg, subst),
187 })
188 | Var(_) | Unallowed | Symbol(_) => term
189 }
190
191let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
192 switch term {
193 | Symbol(_) => term
194 | Var({idx: var}) =>
195 if var < from {
196 term
197 } else if var - from < Array.length(substs) && var - from >= 0 {
198 Option.getExn(substs[var - from])
199 } else {
200 Var({idx: var - Array.length(substs)})
201 }
202 | Schematic({schematic}) =>
203 Schematic({
204 schematic: schematic,
205 })
206 | Lam({name, body}) =>
207 Lam({
208 name,
209 body: substDeBruijn(body, substs->Array.map(term => upshift(term, 1)), ~from=from + 1),
210 })
211 | App({func, arg}) =>
212 App({
213 func: substDeBruijn(func, substs, ~from),
214 arg: substDeBruijn(arg, substs, ~from),
215 })
216 | Unallowed => Unallowed
217 }
218// beta reduced and eta reduced
219let rec reduce = (term: t): t => {
220 switch term {
221 | Lam({body: App({func, arg: Var({idx: 0})})}) if !(func->freeVarsContains(emptySubst, 0)) =>
222 reduce(downshift(func, 1))
223 | App({func, arg}) =>
224 switch reduce(func) {
225 | Lam({body}) => reduce(substDeBruijn(body, [arg]))
226 | func => App({func, arg: reduce(arg)})
227 }
228 | Lam({name, body}) =>
229 Lam({
230 name,
231 body: reduce(body),
232 })
233 | Symbol(_) | Var(_) | Schematic(_) => term
234
235 | Unallowed => Unallowed
236 }
237}
238let reduceSubst = (subst: subst): subst => {
239 subst->Belt.Map.Int.map(x => reduce(substitute(x, subst)))
240}
241let rec lams = (amount: int, term: t): t => {
242 assert(amount >= 0)
243 if amount <= 0 {
244 term
245 } else {
246 Lam({
247 name: "x",
248 body: lams(amount - 1, term),
249 })
250 }
251}
252let rec idx = (is: array<t>, j: t): option<int> => {
253 if is->Array.length == 0 {
254 None
255 } else {
256 let head = is[0]->Option.getExn
257 let tail = is->Array.sliceToEnd(~start=1)
258 if equivalent(head, j) {
259 Some(tail->Array.length)
260 } else {
261 idx(tail, j)
262 }
263 }
264}
265let idx1' = (is: array<t>, j: t): t => {
266 switch idx(is, j) {
267 | None => Unallowed
268 | Some(idx) => Var({idx: idx})
269 }
270}
271let _idx1 = (is: array<t>, j: int): t => idx1'(is, Var({idx: j}))
272let idx2' = (is: array<t>, j: t): result<int, int => t> => {
273 switch idx(is, j) {
274 | None => Error(_ => Unallowed)
275 | Some(idx) => Ok(idx)
276 }
277}
278let _idx2 = (is: array<t>, j: int) => idx2'(is, Var({idx: j}))
279let rec app = (term: t, args: array<t>): t => {
280 if args->Array.length == 0 {
281 term
282 } else {
283 let head = args[0]->Option.getExn
284 let rest = args->Array.sliceToEnd(~start=1)
285 app(App({func: term, arg: head}), rest)
286 }
287}
288exception UnifyFail(string)
289let rec red = (term: t, is: array<t>): t => {
290 switch term {
291 | _ if is->Array.length == 0 => term
292 | Lam({body}) => red(substDeBruijn(body, [is[0]->Option.getExn]), is->Array.sliceToEnd(~start=1))
293 | term => app(term, is)
294 }
295}
296let lam = (is: array<t>, g: t, js: array<t>): t => {
297 lams(is->Array.length, app(g, js->Array.map(j => idx1'(is, j))))
298}
299let rec strip = (term: t): (t, array<t>) => {
300 switch term {
301 | App({func, arg}) =>
302 let (peeledFunc, peeledArgs) = strip(func)
303 (peeledFunc, Array.concat(peeledArgs, [arg]))
304 | _ => (term, [])
305 }
306}
307let rec devar = (subst: subst, term: t): t => {
308 let (func, args) = strip(term)
309 switch func {
310 | Schematic({schematic}) if substHas(subst, schematic) =>
311 devar(subst, red(substGet(subst, schematic)->Option.getExn, args))
312 | _ => term
313 }
314}
315let mkvars = (n: int): array<t> => {
316 Belt.Array.init(n, i => n - i - 1)->Array.map(x => Var({idx: x}))
317}
318let rec proj_allowed = (subst: subst, term: t): bool => {
319 let term' = devar(subst, term)
320 switch term' {
321 | Lam(_) | Unallowed | Schematic(_) | Symbol(_) => false
322 | Var(_) => true // pattern unification only allows this
323 // FCU allows this:
324 | App(_) =>
325 switch strip(term') {
326 | (Symbol(_) | Var(_), args) => Array.every(args, x => proj_allowed(subst, x))
327 | _ => false
328 }
329 }
330}
331// this function is called proj in Nipkow 1993 and it is called pruning in FCU paper
332let rec proj = (subst: subst, term: t, ~gen: option<gen>): subst => {
333 switch strip(devar(subst, term)) {
334 | (Lam({name: _, body}), args) if args->Array.length == 0 => proj(subst, body, ~gen)
335 | (Unallowed, _args) => throw(UnifyFail("unallowed"))
336 | (Symbol(_) | Var(_), args) => Array.reduce(args, subst, (acc, a) => proj(acc, a, ~gen))
337 | (Schematic({schematic}), args) => {
338 assert(!substHas(subst, schematic))
339 if gen->Option.isNone {
340 throw(UnifyFail("no gen provided"))
341 }
342 let h = Schematic({schematic: fresh(Option.getExn(gen))})
343 subst->substAdd(
344 schematic,
345 lams(
346 args->Array.length,
347 app(
348 h,
349 Belt.Array.init(args->Array.length, j => {
350 if proj_allowed(subst, args[j]->Option.getExn) {
351 Some(Var({idx: args->Belt.Array.length - j - 1}))
352 } else {
353 None
354 }
355 })->Array.keepSome,
356 ),
357 ),
358 )
359 }
360 | _ => throw(UnifyFail("not a symbol, var or schematic"))
361 }
362}
363let flexflex = (
364 sa: schematic,
365 xs: array<t>,
366 sb: schematic,
367 ys: array<t>,
368 subst: subst,
369 ~gen: option<gen>,
370): subst => {
371 if gen->Option.isNone {
372 throw(UnifyFail("no gen provided"))
373 }
374 if sa == sb {
375 if xs->Array.length != ys->Array.length {
376 throw(UnifyFail("flexible schematics have different number of arguments"))
377 }
378 let len = xs->Array.length
379 let h = Schematic({schematic: fresh(Option.getExn(gen))})
380 let xs = Belt.Array.init(len, k => {
381 let a = xs[k]->Option.getExn
382 let b = ys[k]->Option.getExn
383 if equivalent(a, b) {
384 Some(Var({idx: len - k - 1}))
385 } else {
386 None
387 }
388 })->Array.keepSome
389 subst->substAdd(sa, lams(len, app(h, xs)))
390 } else {
391 let common = xs->Array.filter(x => ys->Belt.Array.some(y => equivalent(x, y)))
392 let h = Schematic({schematic: fresh(Option.getExn(gen))})
393 subst->substAdd(sa, lam(xs, h, common))->substAdd(sb, lam(ys, h, common))
394 }
395}
396let flexrigid = (sa: schematic, xs: array<t>, b: t, subst: subst, ~gen: option<gen>): subst => {
397 if occ(sa, subst, b) {
398 throw(UnifyFail("flexible schematic occurs in rigid term"))
399 }
400 // pattern unification
401 // let u = b->mapbind0(bind => idx2(xs, bind))
402 // FCU
403 let zn = mkvars(xs->Array.length)
404 // we reversed it so that the last one will be picked if there are duplicates. This behaviour helps certain real world cases.
405 let u = discharge(Belt.Array.reverse(Belt.Array.zip(xs, zn)), b, ~prune=true)
406 proj(subst->substAdd(sa, lams(xs->Array.length, u)), u, ~gen)
407}
408let rec unifyTerm = (a: t, b: t, subst: subst, ~gen: option<gen>): subst =>
409 switch (devar(subst, a), devar(subst, b)) {
410 | (Symbol({name: na}), Symbol({name: nb})) =>
411 if na == nb {
412 subst
413 } else {
414 throw(UnifyFail("symbols do not match"))
415 }
416 | (Var({idx: ia}), Var({idx: ib})) =>
417 if ia == ib {
418 subst
419 } else {
420 throw(UnifyFail("variables do not match"))
421 }
422 | (Schematic({schematic: sa}), Schematic({schematic: sb})) if sa == sb => subst
423 | (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => unifyTerm(ba, bb, subst, ~gen)
424 | (Lam({name: _, body: ba}), b) =>
425 unifyTerm(ba, App({func: upshift(b, 1), arg: Var({idx: 0})}), subst, ~gen)
426 | (a, Lam({name: _, body: bb})) =>
427 unifyTerm(App({func: upshift(a, 1), arg: Var({idx: 0})}), bb, subst, ~gen)
428 | (a, b) =>
429 switch (strip(a), strip(b)) {
430 | ((Schematic({schematic: sa}), xs), (Schematic({schematic: sb}), ys)) =>
431 flexflex(sa, xs, sb, ys, subst, ~gen)
432 | ((Schematic({schematic: sa}), xs), _) => flexrigid(sa, xs, b, subst, ~gen)
433 | (_, (Schematic({schematic: sb}), ys)) => flexrigid(sb, ys, a, subst, ~gen)
434 | ((a, xs), (b, ys)) =>
435 switch (a, b) {
436 | (Symbol(_) | Var(_), Symbol(_) | Var(_)) => rigidrigid(a, xs, b, ys, subst, ~gen)
437 | _ => throw(UnifyFail("no rules match"))
438 }
439 }
440 }
441and unifyArray = (xs: array<t>, ys: array<t>, subst: subst, ~gen: option<gen>): subst => {
442 if xs->Array.length != ys->Array.length {
443 throw(UnifyFail("arrays have different lengths"))
444 }
445 Belt.Array.zip(xs, ys)->Belt.Array.reduce(subst, (acc, (x, y)) => unifyTerm(x, y, acc, ~gen))
446}
447and rigidrigid = (
448 a: t,
449 xs: array<t>,
450 b: t,
451 ys: array<t>,
452 subst: subst,
453 ~gen: option<gen>,
454): subst => {
455 if !equivalent(a, b) {
456 throw(UnifyFail("rigid terms do not match"))
457 }
458 if xs->Array.length != ys->Array.length {
459 throw(UnifyFail("rigid terms have different number of arguments"))
460 }
461 unifyArray(xs, ys, subst, ~gen)
462}
463let unify = (a: t, b: t, ~gen=?) =>
464 Seq.fromArray(
465 try {
466 [unifyTerm(a, b, emptySubst, ~gen)]
467 } catch {
468 | UnifyFail(_) => []
469 },
470 )
471let rec rewrite = (term: t, from: t, to: t, ~subst: subst, ~gen: option<gen>): (subst, t) => {
472 try {
473 let subst1 = unifyTerm(term, from, subst, ~gen)
474 (subst1, to)
475 } catch {
476 | UnifyFail(_) =>
477 switch term {
478 | Schematic({schematic}) if subst->substHas(schematic) =>
479 rewrite(subst->substGet(schematic)->Option.getExn, from, to, ~subst, ~gen)
480 | Var(_) | Unallowed | Symbol(_) | Schematic(_) => (subst, term)
481 | Lam({name, body}) => {
482 let (subst1, body1) = rewrite(body, from, to, ~subst, ~gen)
483 (subst1, Lam({name, body: body1}))
484 }
485 | App({func, arg}) => {
486 let (subst1, func') = rewrite(func, from, to, ~subst, ~gen)
487 let (subst2, arg') = rewrite(arg, from, to, ~subst=subst1, ~gen)
488 (subst2, App({func: func', arg: arg'}))
489 }
490 }
491 }
492}
493let place = (x: int, ~scope: array<string>) =>
494 app(
495 Schematic({
496 schematic: x,
497 }),
498 Array.fromInitializer(~length=Array.length(scope), i => Var({idx: i})),
499 )
500
501let prettyPrintVar = (idx: int, scope: array<string>) =>
502 switch scope[idx] {
503 | Some(n) if Array.indexOf(scope, n) == idx => n
504 | _ => "\\"->String.concat(String.make(idx))
505 }
506let makeGen = () => {
507 ref(0)
508}
509let rec stripLam = (it: t): (array<string>, t) =>
510 switch it {
511 | Lam({name, body}) =>
512 let (names, body) = stripLam(body)
513 (Array.concat([name], names), body)
514 | _ => ([], it)
515 }
516let rec prettyPrint = (it: t, ~scope: array<string>) =>
517 switch it {
518 | Symbol({name, constructor}) =>
519 if constructor {
520 String.concat("@", name)
521 } else {
522 name
523 }
524 | Var({idx}) => prettyPrintVar(idx, scope)
525 | Schematic({schematic}) => "?"->String.concat(String.make(schematic))
526 | Lam(_) =>
527 let (names, body) = stripLam(it)
528 let (func, args) = strip(body)
529 let bodies = Array.concat([func], args)
530 let innerScope = Array.concat(Array.toReversed(names), scope)
531 "("
532 ->String.concat(Array.join(names->Array.map(name => String.concat(name, ".")), " "))
533 ->String.concat(" ")
534 ->String.concat(Array.join(bodies->Array.map(e => prettyPrint(e, ~scope=innerScope)), " "))
535 ->String.concat(")")
536 | App(_) =>
537 let (func, args) = strip(it)
538 "("
539 ->String.concat(prettyPrint(func, ~scope))
540 ->String.concat(" ")
541 ->String.concat(Array.join(args->Array.map(e => prettyPrint(e, ~scope)), " "))
542 ->String.concat(")")
543 | Unallowed => ""
544 }
545let prettyPrintSubst = (sub: subst, ~scope: array<string>) =>
546 Util.prettyPrintIntMap(sub, ~showV=t => prettyPrint(t, ~scope))
547let symbolRegexpString = "^([^\\s()]+)"
548let nameRES = "^([^\\s.\\[\\]()]+)\\."
549exception ParseError(string)
550type token =
551 | LParen
552 | RParen
553 | VarT(int)
554 | SchematicT(int)
555 | AtomT(string)
556 | ConsT(string)
557 | NameT(string)
558 | EOF
559let varRegexpString = "^\\\\([0-9]+)"
560let schematicRegexpString = "^\\?([0-9]+)"
561let tokenize = (str0: string): (token, string) => {
562 let str = str0->String.trimStart
563 if str->String.length == 0 {
564 (EOF, "")
565 } else {
566 let rest = () => str->String.sliceToEnd(~start=1)
567 switch str->String.charAt(0) {
568 | "(" => (LParen, rest())
569 | ")" => (RParen, rest())
570 | "\\" => {
571 let re = RegExp.fromStringWithFlags(varRegexpString, ~flags="y")
572 switch re->RegExp.exec(str) {
573 | None => throw(ParseError("invalid variable"))
574 | Some(res) =>
575 switch RegExp.Result.matches(res) {
576 | [n] => (
577 VarT(n->Int.fromString->Option.getExn),
578 String.sliceToEnd(str, ~start=RegExp.lastIndex(re)),
579 )
580 | _ => throw(ParseError("invalid variable"))
581 }
582 }
583 }
584 | "?" => {
585 let re = RegExp.fromStringWithFlags(schematicRegexpString, ~flags="y")
586 switch re->RegExp.exec(str) {
587 | None => throw(ParseError("invalid schematic"))
588 | Some(res) =>
589 switch RegExp.Result.matches(res) {
590 | [n] => (
591 SchematicT(n->Int.fromString->Option.getExn),
592 String.sliceToEnd(str, ~start=RegExp.lastIndex(re)),
593 )
594 | _ => throw(ParseError("invalid schematic"))
595 }
596 }
597 }
598 | "@" =>
599 let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
600 switch re->RegExp.exec(rest()) {
601 | None => throw(ParseError("invalid symbol"))
602 | Some(res) =>
603 switch RegExp.Result.matches(res) {
604 | [n] => (ConsT(n), String.sliceToEnd(rest(), ~start=RegExp.lastIndex(re)))
605 | _ => throw(ParseError("invalid symbol"))
606 }
607 }
608 | _ => {
609 let reName = RegExp.fromStringWithFlags(nameRES, ~flags="y")
610 switch reName->RegExp.exec(str) {
611 | Some(res) =>
612 switch RegExp.Result.matches(res) {
613 | [n] => (NameT(n), String.sliceToEnd(str, ~start=RegExp.lastIndex(reName)))
614 | _ => throw(ParseError("invalid symbol"))
615 }
616 | None =>
617 let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
618 switch re->RegExp.exec(str) {
619 | None => throw(ParseError("invalid symbol"))
620 | Some(res) =>
621 switch RegExp.Result.matches(res) {
622 | [n] => (AtomT(n), String.sliceToEnd(str, ~start=RegExp.lastIndex(re)))
623 | _ => throw(ParseError("invalid symbol"))
624 }
625 }
626 }
627 }
628 }
629 }
630}
631type rec simple =
632 | ListS({xs: array<simple>})
633 | AtomS({name: string, constructor: bool})
634 | VarS({idx: int})
635 | SchematicS({schematic: int})
636 | LambdaS({name: string, body: simple})
637let rec parseSimple = (str: string): (simple, string) => {
638 let (t0, rest) = tokenize(str)
639 switch t0 {
640 | LParen => {
641 let (t1, rest1) = tokenize(rest)
642 switch t1 {
643 | NameT(name) => {
644 let (result, rest2) = parseSimple("("->String.concat(rest1))
645 (LambdaS({name, body: result}), rest2)
646 }
647 | RParen => (ListS({xs: []}), rest1)
648 | _ => {
649 let (head, rest2) = parseSimple(rest)
650 let (tail, rest3) = parseSimple("("->String.concat(rest2))
651 switch tail {
652 | ListS({xs}) => (ListS({xs: Array.concat([head], xs)}), rest3)
653 | _ => throw(Util.Unreachable("bug"))
654 }
655 }
656 }
657 }
658 | RParen => throw(ParseError("unexpected right parenthesis"))
659 | VarT(idx) => (VarS({idx: idx}), rest)
660 | SchematicT(schematic) => (SchematicS({schematic: schematic}), rest)
661 | AtomT(name) => (AtomS({name, constructor: false}), rest)
662 | ConsT(name) => (AtomS({name, constructor: true}), rest)
663 | NameT(name) => {
664 let (result, rest1) = parseSimple(rest)
665 (LambdaS({name, body: result}), rest1)
666 }
667 | EOF => throw(ParseError("unexpected end of file"))
668 }
669}
670type env = Map.t<string, int>
671let incrEnv = (env: env): env => {
672 let nu: env = Map.make()
673 Map.entries(env)->Iterator.forEach(opt =>
674 switch opt {
675 | None => ()
676 | Some((key, value)) => nu->Map.set(key, value + 1)
677 }
678 )
679 nu
680}
681let envFromScope = (scope: array<string>): env => {
682 let nu: env = Map.make()
683 scope->Array.forEachWithIndex((name, idx) => {
684 nu->Map.set(name, idx)
685 })
686 nu
687}
688let envPushLambda = (env: env, name: string): env => {
689 let nu = incrEnv(env)
690 nu->Map.set(name, 0)
691 nu
692}
693let rec parseAll = (simple: simple, ~env: env, ~gen=?): t => {
694 switch simple {
695 | ListS({xs}) => {
696 let ts = xs->Array.map(x => parseAll(x, ~env, ~gen?))
697 if ts->Array.length == 0 {
698 throw(ParseError("empty list"))
699 } else {
700 ts
701 ->Array.sliceToEnd(~start=1)
702 ->Array.reduce(ts[0]->Option.getExn, (acc, x) => App({func: acc, arg: x}))
703 }
704 }
705 | AtomS({name, constructor}) =>
706 if constructor {
707 Symbol({name, constructor: true})
708 } else if env->Map.has(name) {
709 let idx = env->Map.get(name)->Option.getExn
710 Var({idx: idx})
711 } else {
712 Symbol({name, constructor: false})
713 }
714 | VarS({idx}) => Var({idx: idx})
715 | SchematicS({schematic}) =>
716 switch gen {
717 | Some(g) => {
718 seen(g, schematic)
719 Schematic({schematic: schematic})
720 }
721 | None => throw(ParseError("Schematics not allowed here"))
722 }
723 | LambdaS({name, body}) =>
724 Lam({
725 name,
726 body: parseAll(body, ~env=envPushLambda(env, name), ~gen?),
727 })
728 }
729}
730let prettyPrintMeta = (str: string) => {
731 String.concat(str, ".")
732}
733let parseMeta = (str: string) => {
734 let re = RegExp.fromStringWithFlags(nameRES, ~flags="y")
735 switch re->RegExp.exec(str->String.trim) {
736 | None => Error("not a meta name")
737 | Some(res) =>
738 switch RegExp.Result.matches(res) {
739 | [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re)))
740 | _ => Error("impossible happened")
741 }
742 }
743}
744let parse = (str: string, ~scope: array<string>, ~gen=?) => {
745 try {
746 let (simple, rest) = parseSimple(str)
747 Ok((parseAll(simple, ~env=envFromScope(scope), ~gen?), rest))
748 } catch {
749 | ParseError(msg) => Error(msg)
750 }
751}
752
753let concrete = t =>
754 switch t {
755 | Schematic(_) => false
756 | _ => true
757 }
758let mapTerms = (t, f) => f(t)