the next generation of the in-browser educational proof assistant
add sub-menu for introduction rules with more than 1 sub
authored by
Josh Brown
and committed by
Tangled
ed06123c
b86f70a3
+33
-14
+33
-14
src/Method.res
+33
-14
src/Method.res
···
161
161
}
162
162
}
163
163
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
164
-
let ret = Dict.make()
165
164
ctx
166
165
->Context.facts
167
166
->Dict.toArray
168
167
->Array.filterMap(((key, rule)) => {
169
168
let insts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
170
169
let res = rule->Rule.instantiate(insts)
171
-
if Judgment.concrete(res.conclusion) {
172
-
Some((key, res, insts))
173
-
} else {
170
+
if !Judgment.concrete(res.conclusion) {
174
171
None
175
-
}
176
-
})
177
-
->Array.forEach(((key, res, insts)) => {
178
-
let substs = Judgment.unify(res.conclusion, j, ~gen)
179
-
substs
180
-
->Seq.take(seqSizeLimit)
181
-
->Seq.forEach(subst => {
172
+
} else {
173
+
let substs = Judgment.unify(res.conclusion, j, ~gen)->Seq.take(seqSizeLimit)->Seq.toArray
182
174
let new = {
183
175
ruleName: key,
184
176
instantiation: insts,
185
177
subgoals: res.premises->Array.map(f),
186
178
}
187
-
ret->Dict.set("intro " ++ key, (new, subst))
188
-
})
179
+
switch substs {
180
+
| [] => None
181
+
| [subst] => Some(Results.Action(`intro ${key}`, new, subst))
182
+
| _ =>
183
+
Some(
184
+
Delay(
185
+
`intro ${key}`,
186
+
() =>
187
+
substs->Array.map(subst => {
188
+
let s =
189
+
rule.vars
190
+
->Belt.Array.reverse
191
+
->Belt.Array.zip(insts->Array.map(t => t->Term.substitute(subst)))
192
+
->Array.map(
193
+
((v, x)) => {
194
+
let metaS = Term.prettyPrintMeta(v)
195
+
// not very clean, but don't particularly want to
196
+
// pollute TERM with another method for printing bare meta
197
+
let metaWithoutDot =
198
+
metaS->String.slice(~start=0, ~end=String.length(metaS) - 1)
199
+
`${metaWithoutDot} |-> ${Term.prettyPrint(x, ~scope=ctx.fixes)}`
200
+
},
201
+
)
202
+
->Array.join(", ")
203
+
Results.Action(s, new, subst)
204
+
}),
205
+
),
206
+
)
207
+
}
208
+
}
189
209
})
190
-
ret->Dict.toArray->Array.map(((key, (new, subst))) => Results.Action(key, new, subst))
191
210
}
192
211
let check = (it: t<'a>, ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
193
212
switch ctx->Context.facts->Dict.get(it.ruleName) {