diff --git a/src/test/java/edu/kit/typicalc/model/ModelImplTest.java b/src/test/java/edu/kit/typicalc/model/ModelImplTest.java index 2595cae..af1ebfd 100644 --- a/src/test/java/edu/kit/typicalc/model/ModelImplTest.java +++ b/src/test/java/edu/kit/typicalc/model/ModelImplTest.java @@ -1,6 +1,7 @@ package edu.kit.typicalc.model; import edu.kit.typicalc.model.parser.ParseError; +import edu.kit.typicalc.model.parser.TypeAssumptionParser; import edu.kit.typicalc.model.step.AbsStepDefault; import edu.kit.typicalc.model.step.VarStepDefault; import edu.kit.typicalc.model.term.AbsTerm; @@ -15,9 +16,7 @@ import edu.kit.typicalc.model.type.TypeVariableKind; import edu.kit.typicalc.util.Result; import org.junit.jupiter.api.Test; -import java.util.LinkedHashMap; -import java.util.List; -import java.util.Map; +import java.util.*; import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertTrue; @@ -66,4 +65,27 @@ class ModelImplTest { ), typeInference.getFirstInferenceStep() ); } -} \ No newline at end of file + + @Test + void quantifiedTypeAssumption() { + ModelImpl model = new ModelImpl(); + Map assumptions = new HashMap<>(); + assumptions.put("id", "∀ t1 : t1 -> t1"); + + Result result = model.getTypeInferer("(id id) (id true)", assumptions); + assertTrue(result.isOk()); + TypeInfererInterface typeInference = result.unwrap(); + assertTrue(typeInference.getType().isPresent()); + assertEquals( + new NamedType("boolean"), + typeInference.getType().get()); + // spot check unification steps + assertEquals( + new Substitution(new TypeVariable(TypeVariableKind.TREE, 4), new FunctionType( + new FunctionType(new NamedType("boolean"), new NamedType("boolean")), + new FunctionType(new NamedType("boolean"), new NamedType("boolean")) + )), + typeInference.getMGU().get().get(3) + ); + } +} diff --git a/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java b/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java index 024acea..a7f69e1 100644 --- a/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java +++ b/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java @@ -5,9 +5,7 @@ import edu.kit.typicalc.model.type.*; import edu.kit.typicalc.util.Result; import org.junit.jupiter.api.Test; -import java.util.HashMap; -import java.util.LinkedHashMap; -import java.util.Map; +import java.util.*; import static edu.kit.typicalc.model.type.NamedType.BOOLEAN; import static edu.kit.typicalc.model.type.NamedType.INT; @@ -194,6 +192,26 @@ class TypeAssumptionParserTest { )), assumption.getValue()); } + @Test + void allQuantified() { + TypeAssumptionParser parser = new TypeAssumptionParser(); + Map assumptions = new HashMap<>(); + assumptions.put("id", "∀ t1 : t1 -> t1"); + Result, ParseError> type = parser.parse(assumptions); + assertTrue(type.isOk()); + Map types = type.unwrap(); + assertEquals(1, types.size()); + Map.Entry assumption = types.entrySet().stream().findFirst().get(); + assertEquals(new VarTerm("id"), assumption.getKey()); + Set quantified = new HashSet<>(); + quantified.add(new TypeVariable(TypeVariableKind.USER_INPUT, 1)); + assertEquals(new TypeAbstraction( + new FunctionType( + new TypeVariable(TypeVariableKind.USER_INPUT, 1), + new TypeVariable(TypeVariableKind.USER_INPUT, 1) + ), quantified), assumption.getValue()); + } + @Test void errors() { Map tests = new HashMap<>();