the next generation of the in-browser educational proof assistant
1open Signatures
2// the tree sitter plugin hates backslashes in string literals unless they're on the top
3// level..
4let ruleNamePattern = "^[^|()\\s\\-—][^()\\s]*"
5let vinculumRES = "^\\n?\\s*[-—][-—][\\-—]+[ \t]*([^()|\\s\\-—][^()\\s]*)?"
6module Make = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
7 type rec t = {vars: array<Term.meta>, premises: array<t>, conclusion: Judgment.t}
8 let rec substitute = (rule: t, subst: Term.subst) => {
9 let subst' = subst->Term.mapSubst(v => v->Term.upshift(Array.length(rule.vars)))
10 {
11 vars: rule.vars,
12 premises: rule.premises->Array.map(premise => premise->substitute(subst')),
13 conclusion: rule.conclusion->Judgment.substitute(subst')->Judgment.reduce,
14 }
15 }
16 let rec substDeBruijn = (rule: t, substs: array<Term.t>, ~from: int=0) => {
17 let len = Array.length(rule.vars)
18 let substs' = substs->Array.map(v => v->Term.upshift(len, ~from))
19 {
20 vars: rule.vars,
21 premises: rule.premises->Array.map(premise =>
22 premise->substDeBruijn(substs', ~from=from + len)
23 ),
24 conclusion: rule.conclusion
25 ->Judgment.substDeBruijn(substs', ~from=from + len)
26 ->Judgment.reduce,
27 }
28 }
29 let rec upshift = (rule: t, amount: int, ~from: int=0) => {
30 let len = Array.length(rule.vars)
31 {
32 vars: rule.vars,
33 premises: rule.premises->Array.map(r => r->upshift(amount, ~from=from + len)),
34 conclusion: rule.conclusion->Judgment.upshift(amount, ~from=from + len),
35 }
36 }
37 type bare = {premises: array<t>, conclusion: Judgment.t}
38 let substituteBare = (rule: bare, subst: Term.subst) => {
39 {
40 premises: rule.premises->Array.map(premise => premise->substitute(subst)),
41 conclusion: rule.conclusion->Judgment.substitute(subst)->Judgment.reduce,
42 }
43 }
44 let instantiate = (rule: t, terms: array<Term.t>) => {
45 assert(Array.length(terms) == Array.length(rule.vars))
46 let terms' = [...terms]
47 Array.reverse(terms')
48 {
49 premises: rule.premises->Array.map(r => r->substDeBruijn(terms')),
50 conclusion: rule.conclusion->Judgment.substDeBruijn(terms')->Judgment.reduce,
51 }
52 }
53 let genSchemaInsts = (rule: t, gen: Term.gen, ~scope: array<Term.meta>) => {
54 rule.vars->Array.map(m => Term.place(gen->Term.fresh(~replacing=m), ~scope))
55 }
56 let parseRuleName = str => {
57 let re = RegExp.fromStringWithFlags(ruleNamePattern, ~flags="y")
58 switch re->RegExp.exec(String.trim(str)) {
59 | None => Error("expected rule name")
60 | Some(res) =>
61 switch res[0] {
62 | Some(Some(n)) if String.trim(n) != "" =>
63 Ok(n, String.sliceToEnd(String.trim(str), ~start=RegExp.lastIndex(re)))
64 | _ => Error("expected rule name")
65 }
66 }
67 }
68 let parseVinculum = str => {
69 let re = RegExp.fromStringWithFlags(vinculumRES, ~flags="y")
70 switch re->RegExp.exec(str) {
71 | None => Error("expected vinculum")
72 | Some(res) =>
73 switch res[1] {
74 | Some(Some(n)) if String.trim(n) != "" =>
75 Ok(n, String.sliceToEnd(str, ~start=RegExp.lastIndex(re)))
76 | _ => Ok("", String.sliceToEnd(str, ~start=RegExp.lastIndex(re)))
77 }
78 }
79 }
80 exception InternalParseError(string)
81 let rec parseInner = (string, ~scope=[]: array<Term.meta>, ~gen=?) => {
82 if string->String.trim->String.get(0) == Some("[") {
83 let cur = ref(String.make(string->String.trim->String.sliceToEnd(~start=1)))
84 let it = ref(Error(""))
85 let vars = []
86 while {
87 it := Term.parseMeta(cur.contents)
88 it.contents->Result.isOk
89 } {
90 let (str, rest) = Result.getExn(it.contents)
91 Array.unshift(vars, str)
92 cur := rest
93 }
94 let premises = []
95 switch {
96 while (
97 cur.contents->String.trim->String.slice(~start=0, ~end=2) != "|-" &&
98 cur.contents->String.trim->String.get(0) != Some("]")
99 ) {
100 switch parseInner(cur.contents, ~scope=vars->Array.concat(scope), ~gen?) {
101 | Ok(p, rest) => {
102 cur := rest
103 premises->Array.push(p)
104 }
105 | Error(_) => throw(InternalParseError("expected turnstile or premise"))
106 }
107 }
108 if cur.contents->String.trim->String.get(0) == Some("]") {
109 let rest = cur.contents->String.trim->String.sliceToEnd(~start=1)
110 cur := rest
111 switch premises {
112 | [{vars: [], premises: [], conclusion: e}] =>
113 Ok(({vars, premises: [], conclusion: e}, rest))
114 | _ => Error("Conclusion appears to be multiple terms")
115 }
116 } else {
117 cur := cur.contents->String.trim->String.sliceToEnd(~start=2)
118 switch Judgment.parse(cur.contents, ~scope=vars->Array.concat(scope), ~gen?) {
119 | Ok(conclusion, rest) =>
120 if rest->String.trim->String.get(0) == Some("]") {
121 cur := rest->String.trim->String.sliceToEnd(~start=1)
122 Ok(({vars, premises, conclusion}, cur.contents))
123 } else {
124 Error("Expected closing bracket")
125 }
126 | Error(e) => Error(e)
127 }
128 }
129 } {
130 | exception InternalParseError(e) => Error(e)
131 | v => v
132 }
133 } else {
134 switch Judgment.parse(string, ~scope, ~gen?) {
135 | Ok(conclusion, rest) => Ok(({vars: [], premises: [], conclusion}, rest))
136 | Error(e) => Error(e)
137 }
138 }
139 }
140 let parseTopLevel = (string, ~gen=?, ~scope=[]) => {
141 let cur = ref(String.make(string))
142 let it = ref(Error(""))
143 let vars = []
144 switch {
145 while {
146 it := Term.parseMeta(cur.contents)
147 it.contents->Result.isOk
148 } {
149 let (str, rest) = Result.getExn(it.contents)
150 Array.unshift(vars, str)
151 cur := rest
152 }
153 let it = ref(Error(""))
154 let premises = []
155 while {
156 it := parseVinculum(cur.contents)
157 it.contents->Result.isError
158 } {
159 switch parseInner(cur.contents, ~scope=vars->Array.concat(scope), ~gen?) {
160 | Ok(p, rest) => {
161 cur := rest
162 premises->Array.push(p)
163 }
164 | Error(e) => throw(InternalParseError(e))
165 }
166 }
167 let (ruleName, rest) = it.contents->Result.getExn
168 cur := rest
169 switch Judgment.parse(cur.contents, ~scope=vars->Array.concat(scope), ~gen?) {
170 | Ok(conclusion, rest) => Ok((({vars, premises, conclusion}, ruleName), rest))
171 | Error(e) => Error(e)
172 }
173 } {
174 | exception InternalParseError(e) => Error(e)
175 | v => v
176 }
177 }
178
179 let rec prettyPrintInline = (rule: t, ~scope=[]: array<Term.meta>) => {
180 switch rule {
181 | {vars: [], premises: [], conclusion: c} => Judgment.prettyPrint(c, ~scope)
182 | _ => {
183 let vars' = Array.copy(rule.vars)
184 Array.reverse(vars')
185 "["
186 ->String.concat(
187 vars'
188 ->Array.map(Term.prettyPrintMeta)
189 ->Array.join("")
190 ->String.concat(" ")
191 ->String.concat(
192 if Array.length(rule.premises) == 0 {
193 Judgment.prettyPrint(rule.conclusion, ~scope=[...rule.vars, ...scope])
194 } else {
195 rule.premises
196 ->Array.map(r => prettyPrintInline(r, ~scope=[...rule.vars, ...scope]))
197 ->Array.join(" ")
198 ->String.concat(" |- ")
199 ->String.concat(
200 Judgment.prettyPrint(rule.conclusion, ~scope=[...rule.vars, ...scope]),
201 )
202 },
203 ),
204 )
205 ->String.concat("]")
206 }
207 }
208 }
209 let prettyPrintTopLevel = (rule: t, ~name="", ~scope=[]: array<Term.meta>) => {
210 let vinculise = (strs: array<string>) => {
211 let l = strs->Array.map(String.length)->Array.concat([4])->Math.Int.maxMany
212 strs->Array.concat(["-"->String.repeat(l)->String.concat(" ")->String.concat(name)])
213 }
214 let myReverse = arr => {
215 Array.reverse(arr)
216 arr
217 }
218 rule.vars
219 ->Array.map(Term.prettyPrintMeta)
220 ->myReverse
221 ->Array.join("")
222 ->String.concat(Util.newline)
223 ->String.concat(
224 rule.premises
225 ->Array.map(r => prettyPrintInline(r, ~scope=[...rule.vars, ...scope]))
226 ->vinculise
227 ->Array.concat([Judgment.prettyPrint(rule.conclusion, ~scope=[...rule.vars, ...scope])])
228 ->Array.map(s => String.concat(" ", s))
229 ->Array.join(Util.newline),
230 )
231 }
232}