the next generation of the in-browser educational proof assistant
Merge pull request #24 from joshcbrown/method-context-locality
Add fact locality to method context for useful elimination suggestions
authored by
Liam O'Connor
and committed by
GitHub
374b2fc4
e40b6b3a
+21
-12
+8
-4
src/HOTermMethod.res
+8
-4
src/HOTermMethod.res
···
159
159
let apply = (ctx: Context.t, j: Judgment.t, gen: HOTerm.gen, f: Rule.t => 'a) => {
160
160
let ret: Dict.t<(t<'a>, Judgment.subst)> = Dict.make()
161
161
162
-
ctx.facts->Dict.forEachWithKey((eqRule, name) => {
162
+
ctx
163
+
->Context.facts
164
+
->Dict.forEachWithKey((eqRule, name) => {
163
165
if isEqualityRule(eqRule) {
164
166
let insts = eqRule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
165
167
let instantiatedRule = eqRule->Rule.instantiate(insts)
···
203
205
}
204
206
205
207
let check = (it: t<'a>, ctx: Context.t, goal: Judgment.t, f: ('a, Rule.t) => 'b) => {
206
-
switch ctx.facts->Dict.get(it.equalityName) {
208
+
switch ctx->Context.facts->Dict.get(it.equalityName) {
207
209
| None => Error(`Cannot find equality '${it.equalityName}'`)
208
210
| Some(eqRule) if !isEqualityRule(eqRule) =>
209
211
Error(`'${it.equalityName}' is not a valid equality (has premises)`)
···
429
431
let ret = Dict.make()
430
432
switch j->Judgment.reduce->HOTerm.strip {
431
433
| (HOTerm.Symbol({name: "="}), [lhs, rhs]) =>
432
-
ctx.facts->Dict.forEachWithKey((fact, name) => {
434
+
ctx
435
+
->Context.facts
436
+
->Dict.forEachWithKey((fact, name) => {
433
437
switch extractConstructorEquality(fact.conclusion) {
434
438
| Some((_cName, lArgs, rArgs)) =>
435
439
Belt.Array.zip(lArgs, rArgs)->Array.forEachWithIndex(((la, ra), idx) =>
···
449
453
}
450
454
451
455
let check = (it: t<'a>, ctx: Context.t, goal: Judgment.t, _f: ('a, Rule.t) => 'b) => {
452
-
switch (ctx.facts->Dict.get(it.source), goal->Judgment.reduce->HOTerm.strip) {
456
+
switch (ctx->Context.facts->Dict.get(it.source), goal->Judgment.reduce->HOTerm.strip) {
453
457
| (None, _) => Error(`Cannot find equality '${it.source}'`)
454
458
| (Some(fact), (HOTerm.Symbol({name: "="}), [lhs, rhs])) =>
455
459
switch extractConstructorEquality(fact.conclusion) {
+10
-6
src/Method.res
+10
-6
src/Method.res
···
4
4
module Rule = Rule.Make(Term, Judgment)
5
5
type t = {
6
6
fixes: array<Term.meta>,
7
-
facts: Dict.t<Rule.t>,
7
+
localFacts: Dict.t<Rule.t>,
8
+
globalFacts: Dict.t<Rule.t>,
8
9
}
10
+
let facts = t => t.localFacts->Dict.copy->Dict.assign(t.globalFacts)
9
11
}
10
12
11
13
module type PROOF_METHOD = {
···
139
141
}
140
142
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
141
143
let ret = Dict.make()
142
-
ctx.facts
144
+
ctx
145
+
->Context.facts
143
146
->Dict.toArray
144
147
->Array.filterMap(((key, rule)) => {
145
148
let insts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
···
167
170
ret
168
171
}
169
172
let check = (it: t<'a>, ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
170
-
switch ctx.facts->Dict.get(it.ruleName) {
173
+
switch ctx->Context.facts->Dict.get(it.ruleName) {
171
174
| None => Error("Cannot find rule '"->String.concat(it.ruleName)->String.concat("'"))
172
175
| Some(rule) if Array.length(rule.vars) == Array.length(it.instantiation) => {
173
176
let {premises, conclusion} = Rule.instantiate(rule, it.instantiation)
···
314
317
}
315
318
316
319
let check = (it: t<'a>, ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
317
-
switch (ctx.facts->Dict.get(it.ruleName), ctx.facts->Dict.get(it.elimName)) {
320
+
let facts = ctx->Context.facts
321
+
switch (facts->Dict.get(it.ruleName), facts->Dict.get(it.elimName)) {
318
322
| (None, _) => Error(`Cannot find rule '${it.ruleName}'`)
319
323
| (_, None) => Error(`Cannot find elimination fact '${it.elimName}'`)
320
324
| (Some(rule), Some(elim)) if rule.premises->Array.length > 0 => {
···
359
363
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
360
364
let ret = Dict.make()
361
365
let possibleRules =
362
-
ctx.facts
366
+
ctx.globalFacts
363
367
->Dict.toArray
364
368
->Array.filter(((_, r)) =>
365
369
r.premises->Array.length > 0 && {
···
368
372
}
369
373
)
370
374
let possibleElims =
371
-
ctx.facts
375
+
ctx.localFacts
372
376
->Dict.toArray
373
377
->Array.filter(((_, r)) => r.premises->Array.length == 0 && r.vars->Array.length == 0)
374
378
possibleRules->Array.forEach(((ruleName, rule)) => {
+2
-1
src/Proof.res
+2
-1
src/Proof.res
···
116
116
let newFacts = Dict.fromArray(Belt.Array.zip(prf.assumptions, rule.premises))
117
117
Ok({
118
118
Context.fixes: rule.vars->Array.concat(ctx.fixes),
119
-
facts: Dict.copy(ctx.facts)->Dict.assign(newFacts),
119
+
localFacts: Dict.copy(ctx.localFacts)->Dict.assign(newFacts),
120
+
globalFacts: ctx.globalFacts,
120
121
})
121
122
} else {
122
123
Error(
+1
-1
src/Theorem.res
+1
-1
src/Theorem.res
···
47
47
}
48
48
let make = props => {
49
49
let ruleStyle = props.imports.ruleStyle->Option.getOr(Hybrid)
50
-
let ctx: Context.t = {fixes: [], facts: props.imports.facts}
50
+
let ctx: Context.t = {fixes: [], globalFacts: props.imports.facts, localFacts: Dict.make()}
51
51
let checked = Proof.check(ctx, props.content.proof, props.content.rule)
52
52
let sidebarRef = React.useRef(Nullable.null)
53
53
let proofChanged = (proof, subst) => {