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

Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

Browse Source
This commit is contained in:
ucrhh 2021-02-11 10:37:12 +01:00
commit 1385aae34e
16 changed files with 70 additions and 75 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/main/java/edu/kit/typicalc/model/Tree.java
View File

@ -1,19 +1,10 @@
package edu.kit.typicalc.model;
import edu.kit.typicalc.model.step.*;
import edu.kit.typicalc.model.term.AbsTerm;
import edu.kit.typicalc.model.term.AppTerm;
import edu.kit.typicalc.model.term.ConstTerm;
import edu.kit.typicalc.model.term.LambdaTerm;
import edu.kit.typicalc.model.term.LetTerm;
import edu.kit.typicalc.model.term.TermVisitorTree;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.term.*;
import edu.kit.typicalc.model.type.*;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.*;
/**
* Models the proof tree formed when the type of a lambda term is inferred.
@ -126,7 +117,7 @@ public class Tree implements TermVisitorTree {
@Override
public InferenceStep visit(AbsTerm absTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
Map<VarTerm, TypeAbstraction> extendedTypeAssumptions = new HashMap<>(typeAssumptions);
Map<VarTerm, TypeAbstraction> extendedTypeAssumptions = new LinkedHashMap<>(typeAssumptions);
Type assType = typeVarFactory.nextTypeVariable();
TypeAbstraction assAbs = new TypeAbstraction(assType);
extendedTypeAssumptions.put(absTerm.getVariable(), assAbs);
@ -152,7 +143,7 @@ public class Tree implements TermVisitorTree {
InferenceStep premise;
if (typeInfererLet.getType().isPresent()) {
Map<VarTerm, TypeAbstraction> extendedTypeAssumptions = new HashMap<>(typeAssumptions);
Map<VarTerm, TypeAbstraction> extendedTypeAssumptions = new LinkedHashMap<>(typeAssumptions);
extendedTypeAssumptions.replaceAll((key, value) -> {
Type newType = value.getInnerType();
for (Substitution substitution : typeInfererLet.getMGU().orElseThrow(IllegalStateException::new)) {

9
src/main/java/edu/kit/typicalc/model/TypeInferer.java
View File

@ -7,12 +7,7 @@ import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import edu.kit.typicalc.model.type.TypeVariableKind;
import java.util.ArrayDeque;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Optional;
import java.util.Set;
import java.util.*;
/**
* The type inferer is responsible for the whole type inference of a given lambda term, taking
@ -64,7 +59,7 @@ public class TypeInferer implements TypeInfererInterface {
TypeVariableFactory typeVarFactory = new TypeVariableFactory(TypeVariableKind.GENERATED_TYPE_ASSUMPTION);
Set<VarTerm> freeVariables = lambdaTerm.getFreeVariables();
Map<VarTerm, TypeAbstraction> generatedTypeAss = new HashMap<>();
Map<VarTerm, TypeAbstraction> generatedTypeAss = new LinkedHashMap<>();
for (VarTerm varTerm : freeVariables) {
generatedTypeAss.put(varTerm, new TypeAbstraction(typeVarFactory.nextTypeVariable()));
}

4
src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java
View File

@ -7,7 +7,7 @@ import edu.kit.typicalc.util.Result;
import org.apache.commons.lang3.tuple.ImmutablePair;
import org.apache.commons.lang3.tuple.Pair;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
@ -20,7 +20,7 @@ public class TypeAssumptionParser { // TODO: document type syntax? or refer to o
private static final Pattern TYPE_VARIABLE_PATTERN = Pattern.compile("t(\\d+)");
public Result<Map<VarTerm, TypeAbstraction>, ParseError> parse(Map<String, String> oldAssumptions) {
Map<VarTerm, TypeAbstraction> typeAssumptions = new HashMap<>();
Map<VarTerm, TypeAbstraction> typeAssumptions = new LinkedHashMap<>();
for (Map.Entry<String, String> entry : oldAssumptions.entrySet()) {
VarTerm var = new VarTerm(entry.getKey());
Result<TypeAbstraction, ParseError> typeAbs = parseType(entry.getValue());

4
src/test/java/edu/kit/typicalc/model/ConclusionTest.java
View File

@ -9,14 +9,14 @@ import nl.jqno.equalsverifier.EqualsVerifier;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.Test;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import static org.junit.jupiter.api.Assertions.assertEquals;
class ConclusionTest {
private static final Map<VarTerm, TypeAbstraction> TYPE_ASSUMPTIONS = new HashMap<>();
private static final Map<VarTerm, TypeAbstraction> TYPE_ASSUMPTIONS = new LinkedHashMap<>();
private static final LambdaTerm LAMBDA_TERM = new VarTerm("var");
private static final Type TYPE = new NamedType("type");

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

@ -2,19 +2,19 @@ package edu.kit.typicalc.model;
import org.junit.jupiter.api.Test;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import static org.junit.jupiter.api.Assertions.*;
import static org.junit.jupiter.api.Assertions.assertTrue;
class ModelImplTest {
@Test
void getTypeInferer() {
ModelImpl model = new ModelImpl();
Map<String, String> map = new HashMap<>();
Map<String, String> map = new LinkedHashMap<>();
map.put("x", "int");
Map<String, String> map2 = new HashMap<>();
Map<String, String> map2 = new LinkedHashMap<>();
map2.put("a.x", "3.int");
assertTrue(model.getTypeInferer("test.x.x.test", map2).isError());
assertTrue(model.getTypeInferer("x", map2).isError());

6
src/test/java/edu/kit/typicalc/model/TreeTest.java
View File

@ -13,7 +13,7 @@ import static org.junit.jupiter.api.Assertions.assertThrows;
class TreeTest {
private static final Map<VarTerm, TypeAbstraction> TYPE_ASSUMPTIONS = new HashMap<>();
private static final Map<VarTerm, TypeAbstraction> TYPE_ASSUMPTIONS = new LinkedHashMap<>();
private static final ConstTerm CONST = new IntegerTerm(10);
private static final VarTerm VAR = new VarTerm("var");
private static final AbsTerm ABS = new AbsTerm(VAR, VAR);
@ -46,7 +46,7 @@ class TreeTest {
@Test
void missingTypeAssumptionForVar() {
Map<VarTerm, TypeAbstraction> ass = new HashMap<>();
Map<VarTerm, TypeAbstraction> ass = new LinkedHashMap<>();
assertThrows(IllegalStateException.class, () -> {
new Tree(ass, VAR);
});
@ -87,7 +87,7 @@ class TreeTest {
Tree tree = new Tree(TYPE_ASSUMPTIONS, ABS);
Map<VarTerm, TypeAbstraction> varTypeAss = new HashMap<>(TYPE_ASSUMPTIONS);
Map<VarTerm, TypeAbstraction> varTypeAss = new LinkedHashMap<>(TYPE_ASSUMPTIONS);
varTypeAss.put(VAR, new TypeAbstraction(variable2));
Conclusion varConclusion = new Conclusion(varTypeAss, VAR, variable3);
Constraint varConstraint = new Constraint(variable2, variable3);

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

@ -5,7 +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 static edu.kit.typicalc.model.type.NamedType.BOOLEAN;
@ -17,7 +17,7 @@ class TypeAssumptionParserTest {
@Test
void simpleType() {
TypeAssumptionParser parser = new TypeAssumptionParser();
HashMap<String, String> assumptions = new HashMap<>();
Map<String, String> assumptions = new LinkedHashMap<>();
assumptions.put("a", "int");
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(assumptions);
assertTrue(type.isOk());
@ -31,7 +31,7 @@ class TypeAssumptionParserTest {
@Test
void typeVariablesOneDigitIndex() {
TypeAssumptionParser parser = new TypeAssumptionParser();
HashMap<String, String> assumptions = new HashMap<>();
Map<String, String> assumptions = new LinkedHashMap<>();
assumptions.put("x", "t1");
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(assumptions);
assertTrue(type.isOk());
@ -41,7 +41,7 @@ class TypeAssumptionParserTest {
assertEquals(new VarTerm("x"), assumption.getKey());
assertEquals(new TypeAbstraction(new TypeVariable(TypeVariableKind.USER_INPUT, 1)), assumption.getValue());
HashMap<String, String> assumptions2 = new HashMap<>();
Map<String, String> assumptions2 = new LinkedHashMap<>();
assumptions2.put("x", "t001");
Result<Map<VarTerm, TypeAbstraction>, ParseError> type2 = parser.parse(assumptions2);
assertTrue(type.isOk());
@ -55,7 +55,7 @@ class TypeAssumptionParserTest {
@Test
void typeVariablesMultipleDigitIndex() {
TypeAssumptionParser parser = new TypeAssumptionParser();
HashMap<String, String> assumptions = new HashMap<>();
Map<String, String> assumptions = new LinkedHashMap<>();
assumptions.put("x", "t123456");
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(assumptions);
assertTrue(type.isOk());
@ -69,7 +69,7 @@ class TypeAssumptionParserTest {
@Test
void namedTypeStartingWithT() {
TypeAssumptionParser parser = new TypeAssumptionParser();
HashMap<String, String> assumptions = new HashMap<>();
Map<String, String> assumptions = new LinkedHashMap<>();
assumptions.put("x", "tau1");
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(assumptions);
assertTrue(type.isOk());
@ -83,7 +83,7 @@ class TypeAssumptionParserTest {
@Test
void functionType() {
TypeAssumptionParser parser = new TypeAssumptionParser();
HashMap<String, String> assumptions = new HashMap<>();
Map<String, String> assumptions = new LinkedHashMap<>();
assumptions.put("id", "int -> int");
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(assumptions);
assertTrue(type.isOk());
@ -93,7 +93,7 @@ class TypeAssumptionParserTest {
assertEquals(new VarTerm("id"), assumption.getKey());
assertEquals(new TypeAbstraction(new FunctionType(INT, INT)), assumption.getValue());
HashMap<String, String> assumptions2 = new HashMap<>();
Map<String, String> assumptions2 = new LinkedHashMap<>();
assumptions2.put("f", "int -> int -> int");
type = parser.parse(assumptions2);
if (type.isError()) {
@ -115,7 +115,7 @@ class TypeAssumptionParserTest {
@Test
void functionTypeWithVariables() {
TypeAssumptionParser parser = new TypeAssumptionParser();
HashMap<String, String> assumptions = new HashMap<>();
Map<String, String> assumptions = new LinkedHashMap<>();
assumptions.put("fun", "t0 -> t0");
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(assumptions);
assertTrue(type.isOk());
@ -130,7 +130,7 @@ class TypeAssumptionParserTest {
@Test
void complicatedTypes() {
TypeAssumptionParser parser = new TypeAssumptionParser();
HashMap<String, String> assumptions = new HashMap<>();
Map<String, String> assumptions = new LinkedHashMap<>();
assumptions.put("id", "(int -> int) -> (boolean -> boolean)");
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(assumptions);
if (type.isError()) {
@ -148,7 +148,7 @@ class TypeAssumptionParserTest {
new FunctionType(BOOLEAN, BOOLEAN)
)), assumption.getValue());
parser = new TypeAssumptionParser();
HashMap<String, String> assumptions2 = new HashMap<>();
Map<String, String> assumptions2 = new LinkedHashMap<>();
assumptions2.put("id", "((int -> int) -> (boolean -> boolean)) -> ((int2 -> boolean2) -> (boolean2 -> int2))");
type = parser.parse(assumptions2);
if (type.isError()) {
@ -178,7 +178,7 @@ class TypeAssumptionParserTest {
@Test
void longFunction() {
TypeAssumptionParser parser = new TypeAssumptionParser();
HashMap<String, String> assumptions = new HashMap<>();
Map<String, String> assumptions = new LinkedHashMap<>();
assumptions.put("fun", "(a -> b -> c) -> d");
Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse(assumptions);
assertTrue(type.isOk());

9
src/test/java/edu/kit/typicalc/model/step/AbsStepDefaultTest.java
View File

@ -6,13 +6,14 @@ import edu.kit.typicalc.model.term.IntegerTerm;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.NamedType;
import edu.kit.typicalc.model.type.TypeAbstraction;
import org.junit.jupiter.api.Test;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.Test;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import static org.junit.jupiter.api.Assertions.*;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertNotEquals;
class AbsStepDefaultTest {
static InferenceStep premise = null;
@ -22,7 +23,7 @@ class AbsStepDefaultTest {
static TypeAbstraction typeAbstraction = null;
@BeforeAll
static void setUp() {
Map<VarTerm, TypeAbstraction> map = new HashMap<>();
Map<VarTerm, TypeAbstraction> map = new LinkedHashMap<>();
VarTerm term = new VarTerm("test");
namedType = new NamedType("testType");
typeAbstraction = new TypeAbstraction(namedType);

7
src/test/java/edu/kit/typicalc/model/step/AbsStepWithLetTest.java
View File

@ -9,10 +9,11 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.Test;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import static org.junit.jupiter.api.Assertions.*;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertNotEquals;
class AbsStepWithLetTest {
static InferenceStep premise = null;
@ -22,7 +23,7 @@ class AbsStepWithLetTest {
static TypeAbstraction typeAbstraction = null;
@BeforeAll
static void setUp() {
Map<VarTerm, TypeAbstraction> map = new HashMap<>();
Map<VarTerm, TypeAbstraction> map = new LinkedHashMap<>();
VarTerm term = new VarTerm("test");
namedType = new NamedType("testType");
typeAbstraction = new TypeAbstraction(namedType);

7
src/test/java/edu/kit/typicalc/model/step/AppStepDefaultTest.java
View File

@ -9,10 +9,11 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.Test;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import static org.junit.jupiter.api.Assertions.*;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertNotEquals;
class AppStepDefaultTest {
static InferenceStep premise1 = null;
@ -23,7 +24,7 @@ class AppStepDefaultTest {
static TypeAbstraction typeAbstraction = null;
@BeforeAll
static void setUp() {
Map<VarTerm, TypeAbstraction> map = new HashMap<>();
Map<VarTerm, TypeAbstraction> map = new LinkedHashMap<>();
VarTerm term = new VarTerm("test");
namedType = new NamedType("testType");
typeAbstraction = new TypeAbstraction(namedType);

7
src/test/java/edu/kit/typicalc/model/step/ConstStepDefaultTest.java
View File

@ -9,10 +9,11 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.Test;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import static org.junit.jupiter.api.Assertions.*;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertNotEquals;
class ConstStepDefaultTest {
static Conclusion conclusion = null;
@ -21,7 +22,7 @@ class ConstStepDefaultTest {
static TypeAbstraction typeAbstraction = null;
@BeforeAll
static void setUp() {
Map<VarTerm, TypeAbstraction> map = new HashMap<>();
Map<VarTerm, TypeAbstraction> map = new LinkedHashMap<>();
VarTerm term = new VarTerm("test");
namedType = new NamedType("testType");
typeAbstraction = new TypeAbstraction(namedType);

7
src/test/java/edu/kit/typicalc/model/step/LetStepDefaultTest.java
View File

@ -9,10 +9,11 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.Test;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import static org.junit.jupiter.api.Assertions.*;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertNotEquals;
class LetStepDefaultTest {
static InferenceStep premise = null;
@ -23,7 +24,7 @@ class LetStepDefaultTest {
static TestTypeInfererLet typeInferer = null;
@BeforeAll
static void setUp() {
Map<VarTerm, TypeAbstraction> map = new HashMap<>();
Map<VarTerm, TypeAbstraction> map = new LinkedHashMap<>();
VarTerm term = new VarTerm("test");
namedType = new NamedType("testType");
typeAbstraction = new TypeAbstraction(namedType);

11
src/test/java/edu/kit/typicalc/model/step/StepFactoryDefaultTest.java
View File

@ -6,14 +6,15 @@ import edu.kit.typicalc.model.term.IntegerTerm;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.NamedType;
import edu.kit.typicalc.model.type.TypeAbstraction;
import org.junit.jupiter.api.Test;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.Test;
import java.util.LinkedHashMap;
import java.util.Map;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertTrue;
import java.util.HashMap;
import java.util.Map;
class StepFactoryDefaultTest {
static InferenceStep premise = null;
@ -23,7 +24,7 @@ class StepFactoryDefaultTest {
static TypeAbstraction typeAbstraction = null;
@BeforeAll
static void setUp() {
Map<VarTerm, TypeAbstraction> map = new HashMap<>();
Map<VarTerm, TypeAbstraction> map = new LinkedHashMap<>();
VarTerm term = new VarTerm("test");
namedType = new NamedType("testType");
typeAbstraction = new TypeAbstraction(namedType);

11
src/test/java/edu/kit/typicalc/model/step/StepFactoryWithLetTest.java
View File

@ -6,14 +6,15 @@ import edu.kit.typicalc.model.term.IntegerTerm;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.NamedType;
import edu.kit.typicalc.model.type.TypeAbstraction;
import org.junit.jupiter.api.Test;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.Test;
import java.util.LinkedHashMap;
import java.util.Map;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertNull;
import java.util.HashMap;
import java.util.Map;
class StepFactoryWithLetTest {
static InferenceStep premise = null;
@ -24,7 +25,7 @@ class StepFactoryWithLetTest {
@BeforeAll
static void setUp() {
Map<VarTerm, TypeAbstraction> map = new HashMap<>();
Map<VarTerm, TypeAbstraction> map = new LinkedHashMap<>();
VarTerm term = new VarTerm("test");
namedType = new NamedType("testType");
typeAbstraction = new TypeAbstraction(namedType);

7
src/test/java/edu/kit/typicalc/model/step/VarStepDefaultTest.java
View File

@ -9,10 +9,11 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.Test;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import static org.junit.jupiter.api.Assertions.*;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertNotEquals;
class VarStepDefaultTest {
static InferenceStep premise = null;
@ -22,7 +23,7 @@ class VarStepDefaultTest {
static TypeAbstraction typeAbstraction = null;
@BeforeAll
static void setUp() {
Map<VarTerm, TypeAbstraction> map = new HashMap<>();
Map<VarTerm, TypeAbstraction> map = new LinkedHashMap<>();
VarTerm term = new VarTerm("test");
namedType = new NamedType("testType");
typeAbstraction = new TypeAbstraction(namedType);

7
src/test/java/edu/kit/typicalc/model/step/VarStepWithLetTest.java
View File

@ -9,10 +9,11 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.Test;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import static org.junit.jupiter.api.Assertions.*;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertNotEquals;
class VarStepWithLetTest {
static InferenceStep premise = null;
@ -22,7 +23,7 @@ class VarStepWithLetTest {
static TypeAbstraction typeAbstraction = null;
@BeforeAll
static void setUp() {
Map<VarTerm, TypeAbstraction> map = new HashMap<>();
Map<VarTerm, TypeAbstraction> map = new LinkedHashMap<>();
VarTerm term = new VarTerm("test");
namedType = new NamedType("testType");
typeAbstraction = new TypeAbstraction(namedType);