Add test for 7fb33b8

This commit is contained in:
Arne Keller 2021-07-05 09:25:55 +02:00
parent 8dd5753ee0
commit 9c8d9423fc

View File

@ -1,8 +1,7 @@
package edu.kit.typicalc.model; package edu.kit.typicalc.model;
import edu.kit.typicalc.model.parser.ParseError; import edu.kit.typicalc.model.parser.ParseError;
import edu.kit.typicalc.model.step.AbsStepDefault; import edu.kit.typicalc.model.step.*;
import edu.kit.typicalc.model.step.VarStepDefault;
import edu.kit.typicalc.model.term.AbsTerm; import edu.kit.typicalc.model.term.AbsTerm;
import edu.kit.typicalc.model.term.LambdaTerm; import edu.kit.typicalc.model.term.LambdaTerm;
import edu.kit.typicalc.model.term.VarTerm; import edu.kit.typicalc.model.term.VarTerm;
@ -90,4 +89,15 @@ class ModelImplTest {
typeInference.getMGU().get().get(3) typeInference.getMGU().get().get(3)
); );
} }
@Test
void letTermTypeAssumptions() {
Model model = new ModelImpl();
TypeInfererInterface typer = model.getTypeInferer("(let g = λx.x in g) g", new HashMap<>()).unwrap();
AppStep first = (AppStep) typer.getFirstInferenceStep();
LetStep second = (LetStep) first.getPremise1();
VarStep third = (VarStep) second.getPremise();
VarTerm[] vars = third.getConclusion().getTypeAssumptions().keySet().toArray(new VarTerm[1]);
assertEquals(0, vars[0].uniqueIndex());
}
} }