the next generation of the in-browser educational proof assistant
1open Signatures
2module Context = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
3 module Rule = Rule.Make(Term, Judgment)
4 type t = {
5 fixes: array<Term.meta>,
6 localFacts: Dict.t<Rule.t>,
7 globalFacts: Dict.t<Rule.t>,
8 }
9 let facts = t => t.localFacts->Dict.copy->Dict.assign(t.globalFacts)
10}
11
12module MethodResults = (Term: TERM) => {
13 // Currently all three options produce a button
14 // with both Group and Delay producing sub-menus
15 // I may change Group in future to just present
16 // a boxed group of buttons without nesting it in sub-menus.
17 // So use Delay() if sub-menus is what you actually want.
18 type rec t<'a> =
19 | Action(string, 'a, Term.subst)
20 | Delay(string, unit => array<t<'a>>)
21 | Group(string, array<t<'a>>)
22
23 let rec map = (x: t<'a>, f: 'a => 'b) =>
24 switch x {
25 | Action(str, a, sub) => Action(str, f(a), sub)
26 | Delay(str, g) => Delay(str, () => g()->Array.map(x => x->map(f)))
27 | Group(str, gs) => Group(str, gs->Array.map(x => x->map(f)))
28 }
29}
30
31module type PROOF_METHOD = {
32 module Term: TERM
33 module Judgment: JUDGMENT with module Term := Term
34 module Rule: module type of Rule.Make(Term, Judgment)
35 module Context: module type of Context(Term, Judgment)
36 module Results: module type of MethodResults(Term)
37 type t<'a>
38 let keywords: array<string>
39 let substitute: (t<'a>, Term.subst) => t<'a>
40 let check: (t<'a>, Context.t, Judgment.t, ('a, Rule.t) => 'b) => result<t<'b>, string>
41 let apply: (Context.t, Judgment.t, Term.gen, Rule.t => 'a) => array<Results.t<t<'a>>>
42 let map: (t<'a>, 'a => 'b) => t<'b>
43 let parse: (
44 string,
45 ~keyword: string,
46 ~scope: array<Term.meta>,
47 ~gen: Term.gen,
48 ~subparser: (string, ~scope: array<Term.meta>, ~gen: Term.gen) => result<('a, string), string>,
49 ) => result<(t<'a>, string), string>
50 let prettyPrint: (
51 t<'a>,
52 ~scope: array<Term.meta>,
53 ~indentation: int=?,
54 ~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string,
55 ) => string
56}
57
58let seqSizeLimit = 100
59let newline = Util.newline
60
61module Derivation = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
62 module Rule = Rule.Make(Term, Judgment)
63 module Context = Context(Term, Judgment)
64 module Results = MethodResults(Term)
65 type t<'a> = {
66 ruleName: string,
67 instantiation: array<Term.t>,
68 subgoals: array<'a>,
69 }
70 let map = (it: t<'a>, f) => {
71 {
72 ruleName: it.ruleName,
73 instantiation: it.instantiation,
74 subgoals: it.subgoals->Array.map(f),
75 }
76 }
77 let substitute = (it: t<'a>, subst: Term.subst) => {
78 {
79 ruleName: it.ruleName,
80 instantiation: it.instantiation->Array.map(t => t->Term.substitute(subst)),
81 subgoals: it.subgoals,
82 }
83 }
84 exception InternalParseError(string)
85 let keywords = ["by"]
86 let prettyPrint = (
87 it: t<'a>,
88 ~scope,
89 ~indentation=0,
90 ~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string,
91 ) => {
92 let args = it.instantiation->Array.map(t => Term.prettyPrint(t, ~scope))
93 "by ("
94 ->String.concat(Array.join([it.ruleName]->Array.concat(args), " "))
95 ->String.concat(") {")
96 ->String.concat(
97 if Array.length(it.subgoals) > 0 {
98 newline
99 } else {
100 ""
101 },
102 )
103 ->String.concat(
104 it.subgoals
105 ->Array.map(s => subprinter(s, ~scope, ~indentation=indentation + 2))
106 ->Array.join(newline),
107 )
108 ->String.concat("}")
109 }
110 let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => {
111 let cur = ref(String.trim(input))
112 if cur.contents->String.get(0) == Some("(") {
113 switch Rule.parseRuleName(cur.contents->String.sliceToEnd(~start=1)) {
114 | Ok((ruleName, rest)) => {
115 cur := rest
116 let instantiation = []
117 let it = ref(Error(""))
118 while {
119 it := Term.parse(cur.contents, ~scope, ~gen)
120 it.contents->Result.isOk
121 } {
122 let (val, rest) = it.contents->Result.getExn
123 Array.push(instantiation, val)
124 cur := String.trim(rest)
125 }
126 if cur.contents->String.get(0) == Some(")") {
127 cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
128 let subgoals = []
129 if cur.contents->String.get(0) == Some("{") {
130 cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
131 try {
132 while cur.contents->String.get(0) != Some("}") {
133 switch subparser(cur.contents, ~scope, ~gen) {
134 | Ok((sg, rest)) => {
135 Array.push(subgoals, sg)
136 cur := String.trim(rest)
137 }
138 | Error(e) => throw(InternalParseError(e))
139 }
140 }
141 if cur.contents->String.get(0) == Some("}") {
142 cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
143 Ok(({ruleName, instantiation, subgoals}, cur.contents))
144 } else {
145 Error("} or subgoal proof expected")
146 }
147 } catch {
148 | InternalParseError(e) => Error(e)
149 }
150 } else {
151 Error("{ expected")
152 }
153 } else {
154 Error(") or term expected")
155 }
156 }
157 | Error(e) => Error(e)
158 }
159 } else {
160 Error("Expected (")
161 }
162 }
163 let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
164 ctx
165 ->Context.facts
166 ->Dict.toArray
167 ->Array.filterMap(((key, rule)) => {
168 let insts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
169 let res = rule->Rule.instantiate(insts)
170 if !Judgment.concrete(res.conclusion) {
171 None
172 } else {
173 let substs = Judgment.unify(res.conclusion, j, ~gen)->Seq.take(seqSizeLimit)->Seq.toArray
174 let new = {
175 ruleName: key,
176 instantiation: insts,
177 subgoals: res.premises->Array.map(f),
178 }
179 switch substs {
180 | [] => None
181 | [subst] => Some(Results.Action(`intro ${key}`, new, subst))
182 | _ =>
183 Some(
184 Delay(
185 `intro ${key}`,
186 () =>
187 substs->Array.map(subst => {
188 let s =
189 rule.vars
190 ->Belt.Array.reverse
191 ->Belt.Array.zip(insts->Array.map(t => t->Term.substitute(subst)))
192 ->Array.map(
193 ((v, x)) => {
194 let metaS = Term.prettyPrintMeta(v)
195 // not very clean, but don't particularly want to
196 // pollute TERM with another method for printing bare meta
197 let metaWithoutDot =
198 metaS->String.slice(~start=0, ~end=String.length(metaS) - 1)
199 `${metaWithoutDot} |-> ${Term.prettyPrint(x, ~scope=ctx.fixes)}`
200 },
201 )
202 ->Array.join(", ")
203 Results.Action(s, new, subst)
204 }),
205 ),
206 )
207 }
208 }
209 })
210 }
211 let check = (it: t<'a>, ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
212 switch ctx->Context.facts->Dict.get(it.ruleName) {
213 | None => Error("Cannot find rule '"->String.concat(it.ruleName)->String.concat("'"))
214 | Some(rule) if Array.length(rule.vars) == Array.length(it.instantiation) => {
215 let {premises, conclusion} = Rule.instantiate(rule, it.instantiation)
216 if Judgment.equivalent(conclusion, j) {
217 if Array.length(it.subgoals) == Array.length(premises) {
218 Ok({
219 ruleName: it.ruleName,
220 instantiation: it.instantiation,
221 subgoals: Belt.Array.zipBy(it.subgoals, premises, f),
222 })
223 } else {
224 Error("Incorrect number of subgoals")
225 }
226 } else {
227 let concString = Judgment.prettyPrint(conclusion, ~scope=ctx.fixes)
228 let goalString = Judgment.prettyPrint(j, ~scope=ctx.fixes)
229 Error(
230 "Conclusion of rule '"
231 ->String.concat(concString)
232 ->String.concat("' doesn't match goal '")
233 ->String.concat(goalString)
234 ->String.concat("'"),
235 )
236 }
237 }
238 | _ => Error("Incorrect number of binders")
239 }
240 }
241 let updateAtKey = (it: t<'a>, key: int, f: 'a => 'a) => {
242 let newsgs = it.subgoals->Array.copy
243 newsgs->Array.set(key, f(newsgs[key]->Option.getExn))
244 {...it, subgoals: newsgs}
245 }
246}
247
248module Elimination = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
249 module Rule = Rule.Make(Term, Judgment)
250 module Context = Context(Term, Judgment)
251 module Results = MethodResults(Term)
252 type t<'a> = {
253 ruleName: string,
254 elimName: string,
255 instantiation: array<Term.t>,
256 subgoals: array<'a>,
257 }
258 exception InternalParseError(string)
259 let keywords = ["elim"]
260 let prettyPrint = (
261 it: t<'a>,
262 ~scope,
263 ~indentation=0,
264 ~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string,
265 ) => {
266 let subgoalsSpacer = if Array.length(it.subgoals) > 0 {
267 newline
268 } else {
269 ""
270 }
271 let instantiation = Array.join(
272 it.instantiation->Array.map(t => Term.prettyPrint(t, ~scope)),
273 " ",
274 )
275 let subgoalsStr =
276 it.subgoals
277 ->Array.map(s => subprinter(s, ~scope, ~indentation=indentation + 2))
278 ->Array.join(newline)
279 `elim (${it.ruleName} ${it.elimName} ${instantiation}) {${subgoalsSpacer}${subgoalsStr}}`
280 }
281
282 let map = (it: t<'a>, f) => {
283 {
284 ruleName: it.ruleName,
285 elimName: it.elimName,
286 instantiation: it.instantiation,
287 subgoals: it.subgoals->Array.map(f),
288 }
289 }
290
291 let substitute = (it: t<'a>, subst: Term.subst) => {
292 {
293 ruleName: it.ruleName,
294 elimName: it.elimName,
295 instantiation: it.instantiation->Array.map(t => t->Term.substitute(subst)),
296 subgoals: it.subgoals,
297 }
298 }
299
300 let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => {
301 let cur = ref(String.trim(input))
302 if cur.contents->String.get(0) == Some("(") {
303 Rule.parseRuleName(cur.contents->String.sliceToEnd(~start=1))->Result.flatMap(((
304 ruleName,
305 rest,
306 )) => {
307 cur := rest
308 Rule.parseRuleName(cur.contents)->Result.flatMap(((elimName, rest)) => {
309 cur := rest
310 let instantiation = []
311 let it = ref(Error(""))
312 while {
313 it := Term.parse(cur.contents, ~scope, ~gen)
314 it.contents->Result.isOk
315 } {
316 let (val, rest) = it.contents->Result.getExn
317 Array.push(instantiation, val)
318 cur := String.trim(rest)
319 }
320 if cur.contents->String.get(0) == Some(")") {
321 cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
322 let subgoals = []
323 if cur.contents->String.get(0) == Some("{") {
324 cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
325 try {
326 while cur.contents->String.get(0) != Some("}") {
327 switch subparser(cur.contents, ~scope, ~gen) {
328 | Ok((sg, rest)) => {
329 Array.push(subgoals, sg)
330 cur := String.trim(rest)
331 }
332 | Error(e) => throw(InternalParseError(e))
333 }
334 }
335 if cur.contents->String.get(0) == Some("}") {
336 cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
337 let res = {ruleName, elimName, instantiation, subgoals}
338 Console.log(("parsed elim", res))
339 Ok((res, cur.contents))
340 } else {
341 Error("} or subgoal proof expected")
342 }
343 } catch {
344 | InternalParseError(e) => Error(e)
345 }
346 } else {
347 Error("{ expected")
348 }
349 } else {
350 Error(") or term expected")
351 }
352 })
353 })
354 } else {
355 Error("Expected (")
356 }
357 }
358
359 let check = (it: t<'a>, ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
360 let facts = ctx->Context.facts
361 switch (facts->Dict.get(it.ruleName), facts->Dict.get(it.elimName)) {
362 | (None, _) => Error(`Cannot find rule '${it.ruleName}'`)
363 | (_, None) => Error(`Cannot find elimination fact '${it.elimName}'`)
364 | (Some(rule), Some(elim)) if rule.premises->Array.length > 0 => {
365 let {premises, conclusion} = Rule.instantiate(rule, it.instantiation)
366 let elimPremise = premises[0]->Option.getExn
367 let remainingPremises = premises->Array.sliceToEnd(~start=1)
368 if elimPremise.premises->Array.length > 0 {
369 Error(`Premise to eliminate in rule ${it.ruleName} has non-empty premises`)
370 } else if elim.premises->Array.length > 0 {
371 Error(`Elimination motive (?) ${it.elimName} has non-empty premises`)
372 } else if !Judgment.equivalent(elimPremise.conclusion, elim.conclusion) {
373 Error(`Premise to eliminate and elimination motive (?) ${it.elimName} do not match`)
374 } else if !Judgment.equivalent(conclusion, j) {
375 let concString = Judgment.prettyPrint(conclusion, ~scope=ctx.fixes)
376 let goalString = Judgment.prettyPrint(j, ~scope=ctx.fixes)
377 Error(`Conclusion of rule '${concString}' doesn't match goal '${goalString}'`)
378 } else if Array.length(it.subgoals) != Array.length(remainingPremises) {
379 let subgoalsRem = Array.length(it.subgoals)->Int.toString
380 let premsRem = Array.length(remainingPremises)->Int.toString
381 Error(
382 `Number of subgoals (${subgoalsRem}) doesn't match rule ${it.ruleName}'s remaining number (${premsRem})`,
383 )
384 } else {
385 Ok({
386 ruleName: it.ruleName,
387 elimName: it.elimName,
388 instantiation: it.instantiation,
389 subgoals: Belt.Array.zipBy(it.subgoals, remainingPremises, f),
390 })
391 }
392 }
393 | (Some(_), Some(_)) => Error(`Rule ${it.ruleName} doesn't have any premises`)
394 }
395 }
396
397 let updateAtKey = (it: t<'a>, key: int, f: 'a => 'a) => {
398 let newsgs = it.subgoals->Array.copy
399 newsgs->Array.set(key, f(newsgs[key]->Option.getExn))
400 {...it, subgoals: newsgs}
401 }
402
403 let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
404 let possibleRules =
405 ctx.globalFacts
406 ->Dict.toArray
407 ->Array.filter(((_, r)) =>
408 r.premises->Array.length > 0 && {
409 let fst = r.premises[0]->Option.getExn
410 fst.premises->Array.length == 0 && fst.vars->Array.length == 0
411 }
412 )
413 let possibleElims =
414 ctx.localFacts
415 ->Dict.toArray
416 ->Array.filter(((_, r)) => r.premises->Array.length == 0 && r.vars->Array.length == 0)
417 possibleElims->Array.map(((elimName, elim)) => {
418 Results.Delay(
419 "elim " + elimName,
420 () => {
421 let subtree = []
422 possibleRules->Array.forEach(((ruleName, rule)) => {
423 let ruleInsts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
424 let rule' = rule->Rule.instantiate(ruleInsts)
425 Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion, ~gen)
426 ->Seq.take(seqSizeLimit)
427 ->Seq.forEach(
428 elimSub => {
429 let rule'' = rule'->Rule.substituteBare(elimSub)
430 Judgment.unify(rule''.conclusion, j, ~gen)
431 ->Seq.take(seqSizeLimit)
432 ->Seq.forEach(
433 ruleSub => {
434 let new = {
435 ruleName,
436 elimName,
437 instantiation: ruleInsts,
438 subgoals: rule.premises->Array.sliceToEnd(~start=1)->Array.map(f),
439 }
440 let subst = Term.mergeSubsts(elimSub, ruleSub)
441 subtree->Array.push(Results.Action("with " ++ ruleName, new, subst))
442 },
443 )
444 },
445 )
446 })
447 subtree
448 },
449 )
450 })
451 }
452}
453
454module Lemma = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
455 module Rule = Rule.Make(Term, Judgment)
456 module Context = Context(Term, Judgment)
457 module Results = MethodResults(Term)
458 type t<'a> = {
459 rule: Rule.t,
460 proof: 'a,
461 show: 'a,
462 }
463 let map = (it: t<'a>, f) => {
464 {
465 rule: it.rule,
466 proof: f(it.proof),
467 show: f(it.show),
468 }
469 }
470 let substitute = (it: t<'a>, subst: Term.subst) => {
471 {
472 rule: it.rule->Rule.substitute(subst),
473 proof: it.proof,
474 show: it.show,
475 }
476 }
477 let keywords = ["have"]
478 let prettyPrint = (
479 it: t<'a>,
480 ~scope,
481 ~indentation=0,
482 ~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string,
483 ) => {
484 "have "
485 ->String.concat(Rule.prettyPrintInline(it.rule, ~scope))
486 ->String.concat(newline)
487 ->String.concat(subprinter(it.proof, ~scope, ~indentation))
488 ->String.concat(newline)
489 ->String.concat(subprinter(it.show, ~scope, ~indentation))
490 }
491 let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => {
492 //todo add toplevel
493 switch Rule.parseInner(input, ~scope, ~gen) {
494 | Ok((rule, rest)) =>
495 switch subparser(rest, ~scope, ~gen) {
496 | Ok((proof, rest')) =>
497 switch String.trim(rest')->subparser(~scope, ~gen) {
498 | Ok((show, rest'')) => Ok({rule, proof, show}, rest'')
499 | Error(e) => Error(e)
500 }
501 | Error(e) => Error(e)
502 }
503 | Error(e) => Error(e)
504 }
505 }
506 let apply = (_ctx: Context.t, _j: Judgment.t, _gen: Term.gen, _f: Rule.t => 'a) => {
507 []
508 }
509 let check = (it: t<'a>, _ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
510 let first = f(it.proof, it.rule)
511 let second = f(it.show, {vars: [], premises: [it.rule], conclusion: j})
512 Ok({rule: it.rule, proof: first, show: second})
513 }
514}
515module Combine = (
516 Term: TERM,
517 Judgment: JUDGMENT with module Term := Term,
518 Method1: PROOF_METHOD with module Term := Term and module Judgment := Judgment,
519 Method2: PROOF_METHOD with module Term := Term and module Judgment := Judgment,
520) => {
521 module Rule = Rule.Make(Term, Judgment)
522 module Context = Context(Term, Judgment)
523 module Results = MethodResults(Term)
524 type t<'a> = First(Method1.t<'a>) | Second(Method2.t<'a>)
525 let map = (it, f) =>
526 switch it {
527 | First(m) => First(Method1.map(m, f))
528 | Second(m) => Second(Method2.map(m, f))
529 }
530 let substitute = (it, subst) =>
531 switch it {
532 | First(m) => First(Method1.substitute(m, subst))
533 | Second(m) => Second(Method2.substitute(m, subst))
534 }
535 let keywords = Array.concat(Method1.keywords, Method2.keywords)
536 let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
537 let d1 = Method1.apply(ctx, j, gen, f)->Array.map(me => me->Results.map(m => First(m)))
538 Array.pushMany(
539 d1,
540 Method2.apply(ctx, j, gen, f)->Array.map(me => me->Results.map(m => Second(m))),
541 )
542 d1
543 }
544 let check = (it, ctx, j, f) =>
545 switch it {
546 | First(m) => m->Method1.check(ctx, j, f)->Result.map(x => First(x))
547 | Second(m) => m->Method2.check(ctx, j, f)->Result.map(x => Second(x))
548 }
549 let prettyPrint = (it: t<'a>, ~scope, ~indentation=0, ~subprinter) =>
550 switch it {
551 | First(m) => m->Method1.prettyPrint(~scope, ~indentation, ~subprinter)
552 | Second(m) => m->Method2.prettyPrint(~scope, ~indentation, ~subprinter)
553 }
554 let parse = (input, ~keyword, ~scope, ~gen, ~subparser) => {
555 if Method1.keywords->Array.indexOf(keyword) > -1 {
556 Method1.parse(input, ~keyword, ~scope, ~gen, ~subparser)->Result.map(((x, r)) => (
557 First(x),
558 r,
559 ))
560 } else {
561 Method2.parse(input, ~keyword, ~scope, ~gen, ~subparser)->Result.map(((x, r)) => (
562 Second(x),
563 r,
564 ))
565 }
566 }
567}