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 piece =
7 | String(string)
8 | Var({idx: int})
9 | Schematic({schematic: int, allowed: array<int>})
10type t = array<piece>
11type meta = string
12type schematic = int
13
14module BaseAtom = AtomDef.MakeBaseAtom({
15 type t = t
16})
17
18module Atom = {
19 module BaseAtom = BaseAtom
20 type t = t
21 type subst = Map.t<schematic, t>
22 let substitute = (term: t, subst: subst) =>
23 Array.flatMap(term, piece => {
24 switch piece {
25 | Schematic({schematic, _}) =>
26 switch Map.get(subst, schematic) {
27 | None => [piece]
28 | Some(found) => found
29 }
30 | _ => [piece]
31 }
32 })
33 let schematicsCountsIn: t => Belt.Map.Int.t<int> = (term: t) =>
34 Array.reduce(term, Belt.Map.Int.empty, (m, p) =>
35 switch p {
36 | Schematic({schematic, _}) =>
37 m->Belt.Map.Int.update(schematic, o =>
38 o
39 ->Option.map(v => v + 1)
40 ->Option.orElse(Some(1))
41 )
42 | _ => m
43 }
44 )
45 let maxSchematicCount = (term: t) => {
46 schematicsCountsIn(term)->Belt.Map.Int.maximum->Option.map(Pair.second)->Option.getOr(0)
47 }
48 let freeVarsIn = (term: t): Belt.Set.t<int, IntCmp.identity> =>
49 Array.map(term, piece => {
50 switch piece {
51 | Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
52 | _ => Belt.Set.make(~id=module(IntCmp))
53 }
54 })->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s1, s2) => Belt.Set.union(s1, s2))
55
56 let combineSubst = (s: subst, t: subst) => {
57 let nu = Map.make()
58 Map.entries(s)->Iterator.forEach(opt =>
59 switch opt {
60 | None => ()
61 | Some((key, term)) => nu->Map.set(key, term->substitute(t))
62 }
63 )
64 Map.entries(t)->Iterator.forEach(opt =>
65 switch opt {
66 | None => ()
67 | Some((key, term)) => nu->Map.set(key, term->substitute(s))
68 }
69 )
70 nu
71 }
72
73 let emptySubst: subst = Map.make()
74 let singletonSubst: (int, t) => subst = (schematic, term) => {
75 let s = Map.make()
76 s->Map.set(schematic, term)
77 s
78 }
79
80 let uncons = (xs: array<'a>): ('a, array<'a>) => {
81 switch xs {
82 | [] => Error("expected nonempty array")->Result.getExn
83 | _ => (xs[0]->Option.getExn, Array.sliceToEnd(xs, ~start=1))
84 }
85 }
86
87 type graphSub = Eps | PieceLitSub(piece) | SchemaSub(int, array<int>)
88 let unify = (s: array<piece>, t: array<piece>, ~gen as _=?): Seq.t<subst> => {
89 let match = (p1: piece, p2: piece) => {
90 switch (p1, p2) {
91 | (String(na), String(nb)) if na == nb => true
92 | (Var({idx: ia}), Var({idx: ib})) if ia == ib => true
93 | (_, _) => false
94 }
95 }
96
97 let rec oneSide = (s, t) => {
98 switch (s, t) {
99 | ([], []) => [emptySubst]
100 | ([], _) => []
101 | (_, _) => {
102 let (s1, ss) = uncons(s)
103 switch s1 {
104 | Schematic({schematic, allowed}) =>
105 Belt.Array.range(0, Array.length(t))
106 ->Array.map(i => {
107 let subTerm = Array.slice(t, ~start=0, ~end=i)
108 let freeVars = freeVarsIn(subTerm)
109 let allowedVars = Belt.Set.fromArray(allowed, ~id=module(IntCmp))
110 if Belt.Set.subset(freeVars, allowedVars) {
111 let s1 = singletonSubst(schematic, subTerm)
112 oneSide(
113 substitute(ss, s1),
114 Array.sliceToEnd(t, ~start=i)->substitute(s1),
115 )->Array.map(s2 => combineSubst(s1, s2))
116 } else {
117 []
118 }
119 })
120 ->Array.flat
121 | _ =>
122 switch t {
123 | [] => []
124 | _ => {
125 let (t1, ts) = uncons(t)
126 if match(s1, t1) {
127 oneSide(ss, ts)
128 } else {
129 []
130 }
131 }
132 }
133 }
134 }
135 }
136 }
137
138 let pigPug = (s, t) => {
139 let search = (targetCycles: int): (array<subst>, bool) => {
140 let moreSolsMightExist = ref(false)
141 // seen is an assoc list
142 let rec inner = (s, t, cycle: int, seen: array<((t, t), int)>): array<
143 array<(int, graphSub)>,
144 > => {
145 let (newSeen, thisCycle) = switch seen->Array.findIndexOpt(((e, _)) => e == (s, t)) {
146 | Some(i) => {
147 let (_, thisCycle) = seen[i]->Option.getExn
148 let newSeen = seen->Array.mapWithIndex((e, j) => i == j ? ((s, t), cycle + 1) : e)
149 (newSeen, thisCycle)
150 }
151
152 | None => (Array.concat([((s, t), 1)], seen), 0)
153 }
154 let cycle = max(thisCycle, cycle)
155 let searchSub = (schematic: int, allowed: array<int>, edge: graphSub): array<
156 array<(int, graphSub)>,
157 > => {
158 let piece = Schematic({schematic, allowed})
159 let sub = switch edge {
160 | Eps => singletonSubst(schematic, [])
161 | PieceLitSub(p) => singletonSubst(schematic, [p, piece])
162 | SchemaSub(s2, a2) =>
163 singletonSubst(schematic, [Schematic({schematic: s2, allowed: a2}), piece])
164 }
165 inner(substitute(s, sub), substitute(t, sub), cycle, newSeen)->Array.map(path =>
166 Array.concat(path, [(schematic, edge)])
167 )
168 }
169 if cycle > targetCycles {
170 moreSolsMightExist := true
171 []
172 } else {
173 switch (s[0], t[0]) {
174 | (None, None) => cycle == targetCycles ? [[]] : []
175 | (Some(Schematic({schematic, allowed})), other)
176 | (other, Some(Schematic({schematic, allowed}))) =>
177 switch other {
178 | None => searchSub(schematic, allowed, Eps)
179 | Some(p) =>
180 switch p {
181 | String(_) =>
182 Array.concat(
183 searchSub(schematic, allowed, PieceLitSub(p)),
184 searchSub(schematic, allowed, Eps),
185 )
186 | Schematic({schematic: s2, allowed: a2}) =>
187 if schematic == s2 {
188 inner(
189 s->Array.sliceToEnd(~start=1),
190 t->Array.sliceToEnd(~start=1),
191 cycle,
192 newSeen,
193 )
194 } else {
195 Array.concat(
196 searchSub(schematic, allowed, Eps),
197 searchSub(schematic, allowed, SchemaSub(s2, a2)),
198 )
199 }
200 | Var({idx}) =>
201 if Belt.Set.Int.fromArray(allowed)->Belt.Set.Int.has(idx) {
202 Array.concat(
203 searchSub(schematic, allowed, PieceLitSub(p)),
204 searchSub(schematic, allowed, Eps),
205 )
206 } else {
207 searchSub(schematic, allowed, Eps)
208 }
209 }
210 }
211 | (p1, p2) if p1 == p2 =>
212 inner(s->Array.sliceToEnd(~start=1), t->Array.sliceToEnd(~start=1), cycle, newSeen)
213 | _ => []
214 }
215 }
216 }
217 let paths = inner(s, t, 0, [])
218 let substs = paths->Array.map(path => {
219 let sub = Map.make()
220 path->Array.forEach(((schem, edge)) => {
221 Map.set(
222 sub,
223 schem,
224 switch edge {
225 | Eps => []
226 | PieceLitSub(p) => Array.concat(Map.get(sub, schem)->Option.getOr([]), [p])
227 | SchemaSub(s2, _) =>
228 Array.concat(
229 Map.get(sub, schem)->Option.getOr([]),
230 Map.get(sub, s2)->Option.getOr([]),
231 )
232 },
233 )
234 })
235 sub
236 })
237 let substsSorted = substs->Array.toSorted((s1, s2) => {
238 let substLength = s =>
239 s
240 ->Util.mapMapValues(Array.length)
241 ->Map.values
242 ->Iterator.toArray
243 ->Array.reduce(0, (acc, v) => acc + v)
244 let (s1Length, s2Length) = (substLength(s1), substLength(s2))
245 s1Length < s2Length
246 ? Ordering.less
247 : s2Length < s1Length
248 ? Ordering.greater
249 : Ordering.equal
250 })
251 (substsSorted, moreSolsMightExist.contents)
252 }
253 Seq.unfold((0, true), ((c, moreSolsMightExist)) => {
254 if moreSolsMightExist {
255 let (substs, moreSolsMightExist) = search(c)
256 Some(substs->Seq.fromArray, (c + 1, moreSolsMightExist))
257 } else {
258 None
259 }
260 })->Seq.flatten
261 }
262
263 // naive: assume schematics appear in at most one side
264 let maxCountS = maxSchematicCount(s)
265 let maxCountT = maxSchematicCount(t)
266 if maxCountS == 0 {
267 Seq.fromArray(oneSide(t, s))
268 } else if maxCountT == 0 {
269 Seq.fromArray(oneSide(s, t))
270 } else if max(maxCountS, maxCountT) <= 2 {
271 pigPug(s, t)
272 } else {
273 Seq.fromArray([])
274 }
275 }
276
277 // law: unify(a,b) == [{}] iff equivalent(a,b)
278 let substDeBruijn = (string: t, substs: array<option<t>>, ~from: int=0) => {
279 let to = Array.length(substs)
280 Array.flatMap(string, piece =>
281 switch piece {
282 | String(_) => [piece]
283 | Var({idx: var}) =>
284 if var < from {
285 [piece]
286 } else if var - from < to {
287 switch Option.getUnsafe(substs[var - from]) {
288 | Some(v) => v
289 | None =>
290 throw(SExp.SubstNotCompatible(`index ${Int.toString(var - from)} not of sort string`))
291 }
292 } else {
293 [Var({idx: var - to})]
294 }
295 | Schematic({schematic, allowed}) => [
296 Schematic({
297 schematic,
298 allowed: Array.filterMap(allowed, i =>
299 if i < from + to {
300 None
301 } else {
302 Some(i - (from + to))
303 }
304 ),
305 }),
306 ]
307 }
308 )
309 }
310
311 let upshift = (term: t, amount: int, ~from: int=0) =>
312 Array.map(term, piece => {
313 switch piece {
314 | String(_) => piece
315 | Var({idx}) =>
316 Var({
317 idx: if idx >= from {
318 idx + amount
319 } else {
320 idx
321 },
322 })
323 | Schematic({schematic, allowed}) =>
324 Schematic({
325 schematic,
326 allowed: Array.map(allowed, i =>
327 if i >= from {
328 i + amount
329 } else {
330 i
331 }
332 ),
333 })
334 }
335 })
336
337 type gen = ref<int>
338
339 let prettyPrint = (term: t, ~scope: array<string>) =>
340 `"${Array.map(term, piece => {
341 switch piece {
342 | String(str) => str
343 | Var({idx}) => Util.prettyPrintVar(idx, scope)
344 | Schematic({schematic, allowed}) => Util.prettyPrintSchematic(schematic, allowed, scope)
345 }
346 })->Array.join(" ")}"`
347
348 type remaining = string
349 type errorMessage = string
350 type ident = string
351 let parse: (string, ~scope: array<meta>, ~gen: gen=?) => result<(t, remaining), errorMessage> = (
352 str: string,
353 ~scope: array<ident>,
354 ~gen as _=?,
355 ) => {
356 let pos = ref(0)
357 let seenCloseString = ref(false)
358 let acc = ref(Ok([]))
359
360 let error = (msg: errorMessage) => {
361 let codeAroundLoc = String.slice(str, ~start=pos.contents, ~end=pos.contents + 5)
362 acc := Error(`problem here: ${codeAroundLoc}...: ${msg}`)
363 }
364
365 let execRe = Util.execRe
366 let advance = n => {
367 pos := pos.contents + n
368 }
369 let advance1 = () => advance(1)
370 let add = (token, ~nAdvance=?) => {
371 acc.contents
372 ->Result.map(acc => {
373 Array.push(acc, token)
374 })
375 ->ignore
376 Option.map(nAdvance, advance)->ignore
377 }
378 let execRe = re => execRe(re, String.sliceToEnd(str, ~start=pos.contents))
379 let stringLit = () => {
380 let identRegex = RegExp.fromString(`^${Util.identRegexStr}`)
381 let symbolRegex = /^([!@#\$%\^~&*_+\-={};':|,.<>\/?]+)/
382 let numberRegex = /^(\d+)/
383 switch execRe(identRegex)
384 ->Option.orElse(execRe(symbolRegex))
385 ->Option.orElse(execRe(numberRegex)) {
386 | Some([match], l) => add(String(match), ~nAdvance=l)
387 | Some(_) => error("regex string lit error")
388 | None => error("expected string")
389 }
390 }
391 let escaped = () => {
392 let escapedRegex = /\\([\$\?\\\"])/
393 switch execRe(escapedRegex) {
394 | Some([char], l) => add(String(char), ~nAdvance=l)
395 | Some(_) => error("regex escaped error")
396 | None => error("expected valid escaped character")
397 }
398 }
399 let readInt = s => Int.fromString(s)->Option.getExn
400 let schema = () => {
401 let schemaRegex = /\?(\d+)\(((?:\d+\s*)*)\)/
402 switch execRe(schemaRegex) {
403 | Some([idStr, allowedStr], l) => {
404 let schematic = readInt(idStr)
405 let allowed =
406 allowedStr
407 ->String.trim
408 ->String.splitByRegExp(/\s+/)
409 ->Array.keepSome
410 ->Array.filter(s => s != "")
411 ->Array.map(readInt)
412 add(Schematic({schematic, allowed}), ~nAdvance=l)
413 }
414 | Some(_) => error("schema lit regex error")
415 | None => error("expected schematic literal")
416 }
417 }
418 let var = () => {
419 let varLitRegex = /^\$\\(\d+)/
420 let varScopeRegex = /^\$([a-zA-Z]\w*)/
421 switch execRe(varLitRegex) {
422 | Some([match], l) => add(Var({idx: readInt(match)}), ~nAdvance=l)
423 | Some(_) => error("var lit regex error")
424 | None =>
425 switch execRe(varScopeRegex) {
426 | Some([ident], l) =>
427 switch Array.indexOfOpt(scope, ident) {
428 | Some(idx) => add(Var({idx: idx}), ~nAdvance=l)
429 | None => error("expected variable in scope")
430 }
431 | Some(_) => error("var regex error")
432 | None => error("expected var")
433 }
434 }
435 }
436
437 // consume leading whitespace + open quote
438 switch execRe(/^\s*"/) {
439 | Some(_, l) => pos := l
440 | None => error("expected open quote")
441 }
442 while (
443 pos.contents < String.length(str) && Result.isOk(acc.contents) && !seenCloseString.contents
444 ) {
445 let c = String.get(str, pos.contents)->Option.getExn
446 switch c {
447 | "\"" => {
448 advance1()
449 seenCloseString := true
450 }
451 | "$" => var()
452 | "?" => schema()
453 | " " | "\t" | "\r" | "\n" => advance1()
454 | ")" | "(" | "[" | "]" => add(String(c), ~nAdvance=1)
455 | "\\" => escaped()
456 | _ => stringLit()
457 }
458 }
459
460 acc.contents->Result.map(r => (r, str->String.sliceToEnd(~start=pos.contents)))
461 }
462 let concrete = t =>
463 t->Array.every(p =>
464 switch p {
465 | Schematic(_) => false
466 | _ => true
467 }
468 )
469 let coerce = (AtomDef.AnyValue(tag, a)) =>
470 switch tag {
471 | Symbolic.BaseAtom.Tag => Some([String(a)])
472 | AtomDef.VarBase.Tag =>
473 Some([
474 switch a {
475 | Var({idx}) => Var({idx: idx})
476 | Schematic({schematic, allowed}) => Schematic({schematic, allowed})
477 },
478 ])
479 | _ => None
480 }
481}
482
483module AtomView = {
484 type props = {name: t, scope: array<string>}
485 type idx_props = {idx: int, scope: array<string>}
486 let viewVar = (props: idx_props) =>
487 switch props.scope[props.idx] {
488 | Some(n) if Array.indexOf(props.scope, n) == props.idx =>
489 <span className="term-metavar"> {React.string(n)} </span>
490 | _ =>
491 <span className="term-metavar-unnamed">
492 {React.string("\\")}
493 {React.int(props.idx)}
494 </span>
495 }
496
497 let parenthesise = f =>
498 Array.flat([
499 [<span className="symbol" key={"-1"}> {React.string("(")} </span>],
500 f,
501 [<span className="symbol" key={"-2"}> {React.string(")")} </span>],
502 ])
503
504 let intersperse = a => Util.intersperse(a, ~with=React.string(" "))
505
506 module Piece = {
507 @react.component
508 let make = (~piece: piece, ~scope) =>
509 switch piece {
510 | Var({idx}) => viewVar({idx, scope})
511 | String(s) => <span className="term-const"> {React.string(s)} </span>
512 | Schematic({schematic: s, allowed: vs}) =>
513 <span className="term-schematic">
514 {React.string("?")}
515 {React.int(s)}
516 <span className="term-schematic-telescope">
517 {vs
518 ->Array.mapWithIndex((v, i) =>
519 React.createElement(viewVar, Util.withKey({idx: v, scope}, i))
520 )
521 ->intersperse
522 ->parenthesise
523 ->React.array}
524 </span>
525 </span>
526 }
527 }
528
529 @react.componentWithProps
530 let make = ({name, scope}) =>
531 <span className="term-compound">
532 {React.string("\"")}
533 {name
534 ->Array.mapWithIndex((piece, i) => {
535 let key = Int.toString(i)
536 <Piece piece scope key />
537 })
538 ->intersperse
539 ->React.array}
540 {React.string("\"")}
541 </span>
542}