forked from
liamoc.net/holbert-ng
the next generation of the in-browser educational proof assistant
format Method.res
authored by
Josh Brown
and committed by
Tangled
b86f70a3
5c5a3cb6
+47
-45
+47
-45
src/Method.res
+47
-45
src/Method.res
···
9
9
let facts = t => t.localFacts->Dict.copy->Dict.assign(t.globalFacts)
10
10
}
11
11
12
-
module MethodResults = (Term : TERM) => {
13
-
12
+
module MethodResults = (Term: TERM) => {
14
13
// Currently all three options produce a button
15
14
// with both Group and Delay producing sub-menus
16
15
// I may change Group in future to just present
17
16
// a boxed group of buttons without nesting it in sub-menus.
18
17
// So use Delay() if sub-menus is what you actually want.
19
-
type rec t<'a> = Action(string, 'a, Term.subst)
20
-
| Delay(string, () => array<t<'a>>)
21
-
| Group(string, array<t<'a>>)
22
-
23
-
24
-
25
-
let rec map = (x: t<'a>, f: 'a => 'b ) =>
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) =>
26
24
switch x {
27
-
| Action(str, a, sub) => Action(str,f(a), sub)
28
-
| Delay(str, g) => Delay(str, () => g(())->Array.map(x => x->map(f)))
25
+
| Action(str, a, sub) => Action(str, f(a), sub)
26
+
| Delay(str, g) => Delay(str, () => g()->Array.map(x => x->map(f)))
29
27
| Group(str, gs) => Group(str, gs->Array.map(x => x->map(f)))
30
28
}
31
-
}
32
-
33
-
29
+
}
34
30
35
31
module type PROOF_METHOD = {
36
32
module Term: TERM
···
191
187
ret->Dict.set("intro " ++ key, (new, subst))
192
188
})
193
189
})
194
-
ret->Dict.toArray->Array.map(((key, (new, subst))) => Results.Action(key,new,subst))
190
+
ret->Dict.toArray->Array.map(((key, (new, subst))) => Results.Action(key, new, subst))
195
191
}
196
192
let check = (it: t<'a>, ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
197
193
switch ctx->Context.facts->Dict.get(it.ruleName) {
···
400
396
->Dict.toArray
401
397
->Array.filter(((_, r)) => r.premises->Array.length == 0 && r.vars->Array.length == 0)
402
398
possibleElims->Array.map(((elimName, elim)) => {
403
-
Results.Delay("elim " + elimName,() => {
404
-
let subtree = []
405
-
possibleRules->Array.forEach(((ruleName, rule)) => {
406
-
let ruleInsts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
407
-
let rule' = rule->Rule.instantiate(ruleInsts)
408
-
Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion, ~gen)
409
-
->Seq.take(seqSizeLimit)
410
-
->Seq.forEach(
411
-
elimSub => {
412
-
let rule'' = rule'->Rule.substituteBare(elimSub)
413
-
Judgment.unify(rule''.conclusion, j, ~gen)
414
-
->Seq.take(seqSizeLimit)
415
-
->Seq.forEach(
416
-
ruleSub => {
417
-
let new = {
418
-
ruleName,
419
-
elimName,
420
-
instantiation: ruleInsts,
421
-
subgoals: rule.premises->Array.sliceToEnd(~start=1)->Array.map(f),
422
-
}
423
-
let subst = Term.mergeSubsts(elimSub, ruleSub)
424
-
subtree->Array.push(Results.Action("with " ++ ruleName, new, subst))
425
-
},
426
-
)
427
-
},
428
-
)
429
-
})
430
-
subtree
431
-
})
399
+
Results.Delay(
400
+
"elim " + elimName,
401
+
() => {
402
+
let subtree = []
403
+
possibleRules->Array.forEach(((ruleName, rule)) => {
404
+
let ruleInsts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
405
+
let rule' = rule->Rule.instantiate(ruleInsts)
406
+
Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion, ~gen)
407
+
->Seq.take(seqSizeLimit)
408
+
->Seq.forEach(
409
+
elimSub => {
410
+
let rule'' = rule'->Rule.substituteBare(elimSub)
411
+
Judgment.unify(rule''.conclusion, j, ~gen)
412
+
->Seq.take(seqSizeLimit)
413
+
->Seq.forEach(
414
+
ruleSub => {
415
+
let new = {
416
+
ruleName,
417
+
elimName,
418
+
instantiation: ruleInsts,
419
+
subgoals: rule.premises->Array.sliceToEnd(~start=1)->Array.map(f),
420
+
}
421
+
let subst = Term.mergeSubsts(elimSub, ruleSub)
422
+
subtree->Array.push(Results.Action("with " ++ ruleName, new, subst))
423
+
},
424
+
)
425
+
},
426
+
)
427
+
})
428
+
subtree
429
+
},
430
+
)
432
431
})
433
432
}
434
433
}
···
517
516
let keywords = Array.concat(Method1.keywords, Method2.keywords)
518
517
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
519
518
let d1 = Method1.apply(ctx, j, gen, f)->Array.map(me => me->Results.map(m => First(m)))
520
-
Array.pushMany(d1,Method2.apply(ctx, j, gen, f)->Array.map(me => me->Results.map(m => Second(m))))
519
+
Array.pushMany(
520
+
d1,
521
+
Method2.apply(ctx, j, gen, f)->Array.map(me => me->Results.map(m => Second(m))),
522
+
)
521
523
d1
522
524
}
523
525
let check = (it, ctx, j, f) =>