the next generation of the in-browser educational proof assistant
add logic to apply substitutions to proofs.
+44
-8
+26
-6
src/Method.res
+26
-6
src/Method.res
···
15
15
module Context: module type of Context(Term, Judgment)
16
16
type t<'a>
17
17
let keywords: array<string>
18
+
let substitute: (t<'a>, Term.subst) => t<'a>
18
19
let check: (t<'a>, Context.t, Judgment.t, ('a, Rule.t) => 'b) => result<t<'b>, string>
19
20
let apply: (Context.t, Judgment.t, Term.gen, (Rule.t => 'a)) => Dict.t<(t<'a>, Term.subst)>
20
-
let uncheck: (t<'a>, 'a => 'b) => t<'b>
21
+
let map: (t<'a>, 'a => 'b) => t<'b>
21
22
let parse: (
22
23
string,
23
24
~keyword: string,
···
41
42
instantiation: array<Term.t>,
42
43
subgoals: array<'a>,
43
44
}
44
-
let uncheck = (it: t<'a>, f) => {
45
+
let map = (it: t<'a>, f) => {
45
46
{
46
47
ruleName: it.ruleName,
47
48
instantiation: it.instantiation,
48
49
subgoals: it.subgoals->Array.map(f),
50
+
}
51
+
}
52
+
let substitute = (it: t<'a>, subst: Term.subst) => {
53
+
{
54
+
ruleName: it.ruleName,
55
+
instantiation: it.instantiation->Array.map(t => t->Term.substitute(subst)),
56
+
subgoals: it.subgoals
49
57
}
50
58
}
51
59
exception InternalParseError(string)
···
184
192
proof: 'a,
185
193
show: 'a,
186
194
}
187
-
let uncheck = (it: t<'a>, f) => {
195
+
let map = (it: t<'a>, f) => {
188
196
{
189
197
rule: it.rule,
190
198
proof: f(it.proof),
191
199
show: f(it.show),
200
+
}
201
+
}
202
+
let substitute = (it: t<'a>, subst: Term.subst) => {
203
+
{
204
+
rule: it.rule->Rule.substitute(subst),
205
+
proof: it.proof,
206
+
show: it.show
192
207
}
193
208
}
194
209
let keywords = ["have"]
···
238
253
module Rule = Rule.Make(Term, Judgment)
239
254
module Context = Context(Term, Judgment)
240
255
type t<'a> = First(Method1.t<'a>) | Second(Method2.t<'a>)
241
-
let uncheck = (it, f) =>
256
+
let map = (it, f) =>
257
+
switch it {
258
+
| First(m) => First(Method1.map(m, f))
259
+
| Second(m) => Second(Method2.map(m, f))
260
+
}
261
+
let substitute = (it, subst) =>
242
262
switch it {
243
-
| First(m) => First(Method1.uncheck(m, f))
244
-
| Second(m) => Second(Method2.uncheck(m, f))
263
+
| First(m) => First(Method1.substitute(m, subst))
264
+
| Second(m) => Second(Method2.substitute(m, subst))
245
265
}
246
266
let keywords = Array.concat(Method1.keywords, Method2.keywords)
247
267
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
+18
-2
src/Proof.res
+18
-2
src/Proof.res
···
30
30
->Array.concat(["?"])
31
31
->Array.find(kw => String.trim(input)->String.startsWith(kw))
32
32
}
33
+
let rec substitute = (prf: t, subst: Term.subst) => {
34
+
fixes: prf.fixes,
35
+
assumptions: prf.assumptions,
36
+
method: prf.method->Option.map(m =>
37
+
m->Method.substitute(subst)->Method.map(m => m->substitute(subst))
38
+
)
39
+
}
33
40
let rec prettyPrint = (prf: t, ~scope, ~indentation=0) => {
34
41
let mtd = switch prf.method {
35
42
| None => "?"
···
122
129
fixes,
123
130
assumptions,
124
131
method: switch method {
125
-
| Do(m) => Some(m->Method.uncheck(uncheck))
132
+
| Do(m) => Some(m->Method.map(uncheck))
126
133
| Goal(_) => None
127
134
}
128
135
}
129
136
}
130
137
let rec check = (ctx: Context.t, prf: t, rule: Rule.t) => {
131
138
let ruleStr = Rule.prettyPrintInline(rule, ~scope=[])
132
-
Console.log(("CHECK", ctx, prf, ruleStr))
133
139
switch enter(ctx, prf, rule) {
134
140
| Ok(ctx') =>
135
141
switch prf.method {
···
166
172
| Error(e) => ProofError({raw: prf, rule, msg: e})
167
173
}
168
174
} // result<checked,string>
175
+
176
+
let substituteChecked = (prf: checked,ctx: Context.t, subst: Term.subst) => {
177
+
switch prf {
178
+
| Checked(prf) =>
179
+
check(ctx,Checked(prf)->uncheck->substitute(subst),prf.rule->Rule.substitute(subst))
180
+
| ProofError({raw, rule, msg}) =>
181
+
ProofError({raw: raw->substitute(subst), rule: rule->Rule.substitute(subst), msg})
182
+
}
183
+
184
+
}
169
185
}
170
186
171
187
/*