arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 18:30:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

Test quantified type assumptions

Browse Source
This commit is contained in:
Arne Keller 2021-06-17 09:00:30 +02:00
parent b55c63acc0
commit ce881354a0
2 changed files with 47 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
src/test/java/edu/kit/typicalc/model/ModelImplTest.java
View File

@ -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()
);
}
@Test
void quantifiedTypeAssumption() {
ModelImpl model = new ModelImpl();
Map<String, String> assumptions = new HashMap<>();
assumptions.put("id", "∀ t1 : t1 -> t1");
Result<TypeInfererInterface, ParseError> 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)
);
}
}

24
src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java
View File

@ -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<String, String> assumptions = new HashMap<>();
assumptions.put("id", "∀ t1 : t1 -> t1");
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(assumptions);
assertTrue(type.isOk());
Map<VarTerm, TypeAbstraction> types = type.unwrap();
assertEquals(1, types.size());
Map.Entry<VarTerm, TypeAbstraction> assumption = types.entrySet().stream().findFirst().get();
assertEquals(new VarTerm("id"), assumption.getKey());
Set<TypeVariable> 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<String, ParseError> tests = new HashMap<>();