the next generation of the in-browser educational proof assistant
add sequence size limit
avoids crashing on infinite sequences
+11
-3
+11
-3
src/Method.res
+11
-3
src/Method.res
···
34
34
) => string
35
35
}
36
36
37
+
let seqSizeLimit = 100
38
+
37
39
module Derivation = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
38
40
module Rule = Rule.Make(Term, Judgment)
39
41
module Context = Context(Term, Judgment)
···
141
143
let insts = rule->Rule.schematise(gen, ~scope=ctx.fixes)
142
144
let res = rule->Rule.instantiate(insts)
143
145
let substs = Judgment.unify(res.conclusion, j, ~gen)
144
-
substs->Seq.forEach(subst => {
146
+
substs
147
+
->Seq.take(seqSizeLimit)
148
+
->Seq.forEach(subst => {
145
149
let new = {
146
150
ruleName: key,
147
151
instantiation: insts,
···
361
365
possibleElims->Array.forEach(((elimName, elim)) => {
362
366
let ruleInsts = rule->Rule.schematise(gen, ~scope=ctx.fixes)
363
367
let rule' = rule->Rule.instantiate(ruleInsts)
364
-
Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion)->Seq.forEach(
368
+
Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion)
369
+
->Seq.take(seqSizeLimit)
370
+
->Seq.forEach(
365
371
elimSub => {
366
372
let rule'' = rule'->Rule.substituteBare(elimSub)
367
-
Judgment.unify(rule''.conclusion, j, ~gen)->Seq.forEach(
373
+
Judgment.unify(rule''.conclusion, j, ~gen)
374
+
->Seq.take(seqSizeLimit)
375
+
->Seq.forEach(
368
376
ruleSub => {
369
377
let new = {
370
378
ruleName,