the next generation of the in-browser educational proof assistant
rename `schematise`
+5
-4
+2
-2
src/Method.res
+2
-2
src/Method.res
···
140
140
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
141
141
let ret = Dict.make()
142
142
ctx.facts->Dict.forEachWithKey((rule, key) => {
143
-
let insts = rule->Rule.schematise(gen, ~scope=ctx.fixes)
143
+
let insts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
144
144
let res = rule->Rule.instantiate(insts)
145
145
let substs = Judgment.unify(res.conclusion, j, ~gen)
146
146
substs
···
363
363
->Array.filter(((_, r)) => r.premises->Array.length == 0 && r.vars->Array.length == 0)
364
364
possibleRules->Array.forEach(((ruleName, rule)) => {
365
365
possibleElims->Array.forEach(((elimName, elim)) => {
366
-
let ruleInsts = rule->Rule.schematise(gen, ~scope=ctx.fixes)
366
+
let ruleInsts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
367
367
let rule' = rule->Rule.instantiate(ruleInsts)
368
368
Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion)
369
369
->Seq.take(seqSizeLimit)
+3
-2
src/Rule.res
+3
-2
src/Rule.res
···
6
6
module Make = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
7
7
type rec t = {vars: array<Term.meta>, premises: array<t>, conclusion: Judgment.t}
8
8
let rec substitute = (rule: t, subst: Judgment.subst) => {
9
-
let subst' = subst->Judgment.mapSubst(v => v->Judgment.upshiftSubstCodom(Array.length(rule.vars)))
9
+
let subst' =
10
+
subst->Judgment.mapSubst(v => v->Judgment.upshiftSubstCodom(Array.length(rule.vars)))
10
11
{
11
12
vars: rule.vars,
12
13
premises: rule.premises->Array.map(premise => premise->substitute(subst')),
···
50
51
conclusion: rule.conclusion->Judgment.substDeBruijn(terms')->Judgment.reduce,
51
52
}
52
53
}
53
-
let schematise = (rule: t, gen: Term.gen, ~scope: array<Judgment.meta>) => {
54
+
let genSchemaInsts = (rule: t, gen: Term.gen, ~scope: array<Judgment.meta>) => {
54
55
rule.vars->Array.map(m => Judgment.placeSubstCodom(gen->Term.fresh(~replacing=m), ~scope))
55
56
}
56
57
let parseRuleName = str => {