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

.gitlab-ci.yml

@@ -1,8 +1,6 @@
 build:
   script:
-    - mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp checkstyle:check
-    - mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp test
-    - mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp jacoco:prepare-agent test jacoco:report
+    - mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp checkstyle:check jacoco:prepare-agent test jacoco:report
     - python3 /opt/cover2cover.py target/site/jacoco/jacoco.xml src/main/java > target/site/cobertura.xml
     - python3 /opt/source2filename.py target/site/cobertura.xml
     - /opt/calcCoverage.sh < target/site/cobertura.xml

pom.xml

@@ -209,13 +209,6 @@
                 <groupId>org.jacoco</groupId>
                 <artifactId>jacoco-maven-plugin</artifactId>
                 <version>0.8.6</version>
-                <executions>
-                    <execution>
-                        <goals>
-                            <goal>prepare-agent</goal>
-                        </goals>
-                    </execution>
-                </executions>
             </plugin>
 
             <plugin>
@@ -353,4 +346,4 @@
             </plugin>
         </plugins>
     </reporting>
-</project>
+</project>

src/main/java/edu/kit/typicalc/model/Tree.java

@@ -42,7 +42,7 @@ public class Tree implements TermVisitorTree {
      * @param lambdaTerm the lambda term to generate the tree for
      */
     protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm) {
-        this(typeAssumptions, lambdaTerm, new TypeVariableFactory(TypeVaribaleKind.TREE));
+        this(typeAssumptions, lambdaTerm, new TypeVariableFactory(TypeVariableKind.TREE));
     }
 
     /**

src/main/java/edu/kit/typicalc/model/TypeInferer.java

@@ -5,7 +5,7 @@ import edu.kit.typicalc.model.term.LambdaTerm;
 import edu.kit.typicalc.model.term.VarTerm;
 import edu.kit.typicalc.model.type.Type;
 import edu.kit.typicalc.model.type.TypeAbstraction;
-import edu.kit.typicalc.model.type.TypeVaribaleKind;
+import edu.kit.typicalc.model.type.TypeVariableKind;
 
 import java.util.HashMap;
 import java.util.List;
@@ -55,7 +55,7 @@ public class TypeInferer implements TypeInfererInterface {
     }
 
     private Map<VarTerm, TypeAbstraction> createAssForFreeVariables(LambdaTerm lambdaTerm) {
-        TypeVariableFactory typeVarFactory = new TypeVariableFactory(TypeVaribaleKind.GENERATED_TYPE_ASSUMPTION);
+        TypeVariableFactory typeVarFactory = new TypeVariableFactory(TypeVariableKind.GENERATED_TYPE_ASSUMPTION);
         Set<VarTerm> freeVariables = lambdaTerm.getFreeVariables();
 
         Map<VarTerm, TypeAbstraction> generatedTypeAss = new HashMap<>();

src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java

@@ -1,7 +1,7 @@
 package edu.kit.typicalc.model;
 
 import edu.kit.typicalc.model.type.TypeVariable;
-import edu.kit.typicalc.model.type.TypeVaribaleKind;
+import edu.kit.typicalc.model.type.TypeVariableKind;
 
 /**
  * Provides unique type variables on demand.
@@ -10,7 +10,7 @@ public class TypeVariableFactory {
 
     private static final int FIRST_VARIABLE_INDEX = 1;
 
-    private final TypeVaribaleKind kind;
+    private final TypeVariableKind kind;
     private int nextVariableIndex;
 
     /**
@@ -18,7 +18,7 @@ public class TypeVariableFactory {
      *
      * @param kind the kind of the created type variables
      */
-    protected TypeVariableFactory(TypeVaribaleKind kind) {
+    protected TypeVariableFactory(TypeVariableKind kind) {
         this.kind = kind;
         nextVariableIndex = FIRST_VARIABLE_INDEX;
     }

src/main/java/edu/kit/typicalc/model/package-info.java

@@ -1,15 +1,15 @@
+/**
+  * The model package contains all classes needed to model the typed lambda calculus and the type inference algorithm.
+  * To do so, it contains the sub-packages term, type, step and parser.
+  * The model package itself contains the ModelInterface, functioning as an interface for the presenter
+  * and the classes executing the type inference algorithm.
+  * The class TypeInferer combines the three separated parts of the algorithm:
+  * the building of the tree, execution of the unification and calculation of the most general unifier and final type.
+  * An instance of TypeInferer, fitting the lambda term from the user input, is passed to the view to obtain the data
+  * needed for the visualization of the computed steps of the algorithm.
+ */
 @NonNullFields
 @NonNullApi
-/**
- * The model package contains all classes needed to model the typed lambda calculus and the type inference algorithm.
- * To do so, it contains the sub-packages term, type, step and parser.
- * The model package itself contains the ModelInterface, functioning as an interface for the presenter
- * and the classes executing the type inference algorithm.
- * The class TypeInferer combines the three separated parts of the algorithm:
- * the building of the tree, execution of the unification and calculation of the most general unifier and final type.
- * An instance of TypeInferer, fitting the lambda term from the user input, is passed to the view to obtain the data
- * needed for the visualization of the computed steps of the algorithm.
- */
 package edu.kit.typicalc.model;
 
 import org.springframework.lang.NonNullApi;

src/main/java/edu/kit/typicalc/model/parser/package-info.java

@@ -1,9 +1,9 @@
+/**
+  * The parser package contains all classes needed to parse the input strings from the user to an abstract form
+  * consisting of classes provided by the the model, term and type package.
+ */
 @NonNullApi
 @NonNullFields
-/**
- * The parser package contains all classes needed to parse the input strings from the user to an abstract form
- * consisting of classes provided by the the model, term and type package.
- */
 package edu.kit.typicalc.model.parser;
 
 import org.springframework.lang.NonNullApi;

src/main/java/edu/kit/typicalc/model/step/package-info.java

@@ -1,10 +1,10 @@
+/**
+  * The step package models the inference steps that are executed while generating the prof tree.
+  * To represent the different kinds of typing rules that can be applied, InferenceStep has various subclasses.
+  * These subclasses can be produced by factories, appropriate to the desired context.
+ */
 @NonNullFields
 @NonNullApi
-/**
- * The step package models the inference steps that are executed while generating the prof tree.
- * To represent the different kinds of typing rules that can be applied, InferenceStep has various subclasses.
- * These subclasses can be produced by factories, appropriate to the desired context.
- */
 package edu.kit.typicalc.model.step;
 
 import org.springframework.lang.NonNullApi;

src/main/java/edu/kit/typicalc/model/term/package-info.java

@@ -1,9 +1,9 @@
+/**
+  * The term package models the different kinds of lambda terms:
+  * application, abstraction, variable constant and let-polymorphism.
+ */
 @NonNullFields
 @NonNullApi
-/**
- * The term package models the different kinds of lambda terms:
- * application, abstraction, variable constant and let-polymorphism.
- */
 package edu.kit.typicalc.model.term;
 
 import org.springframework.lang.NonNullApi;

src/main/java/edu/kit/typicalc/model/type/TypeVariable.java

@@ -10,7 +10,7 @@ import java.util.Objects;
  */
 public class TypeVariable extends Type {
 
-    private final TypeVaribaleKind kind;
+    private final TypeVariableKind kind;
     private final int index;
 
     /**
@@ -19,7 +19,7 @@ public class TypeVariable extends Type {
      * @param kind the kind of type variable
      * @param index the index of this variable
      */
-    public TypeVariable(TypeVaribaleKind kind, int index) {
+    public TypeVariable(TypeVariableKind kind, int index) {
         this.kind = kind;
         this.index = index;
     }
@@ -28,7 +28,7 @@ public class TypeVariable extends Type {
      * Returns the kind of the type variable.
      * @return the variable's kind
      */
-    public TypeVaribaleKind getKind() {
+    public TypeVariableKind getKind() {
         return kind;
     }
 

src/main/java/edu/kit/typicalc/model/type/TypeVariableKind.java

@@ -3,7 +3,7 @@ package edu.kit.typicalc.model.type;
 /**
  * Describes the kind of type variable (the context it was generated / it is used in).
  */
-public enum TypeVaribaleKind {
+public enum TypeVariableKind {
 
     /**
      * Used if the type variable was created from user input.

src/main/java/edu/kit/typicalc/model/type/package-info.java

@@ -1,8 +1,8 @@
+/**
+  * The type package models all types that can be assigned to lambda terms.
+ */
 @NonNullApi
 @NonNullFields
-/**
- * The type package models all types that can be assigned to lambda terms.
- */
 package edu.kit.typicalc.model.type;
 
 import org.springframework.lang.NonNullApi;

src/test/java/edu/kit/typicalc/model/ConclusionTest.java

@@ -0,0 +1,45 @@
+package edu.kit.typicalc.model;
+
+import edu.kit.typicalc.model.term.LambdaTerm;
+import edu.kit.typicalc.model.term.VarTerm;
+import edu.kit.typicalc.model.type.NamedType;
+import edu.kit.typicalc.model.type.Type;
+import edu.kit.typicalc.model.type.TypeAbstraction;
+import org.junit.jupiter.api.BeforeAll;
+import org.junit.jupiter.api.Test;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.Map;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+class ConclusionTest {
+
+    private static final Map<VarTerm, TypeAbstraction> typeAssumptions = new HashMap<>();
+    private static final LambdaTerm lambdaTerm = new VarTerm("var");
+    private static final Type type = new NamedType("type");
+
+    @BeforeAll
+    static void setUp() {
+        typeAssumptions.put(new VarTerm("var2"), new TypeAbstraction(new NamedType("type2"), new ArrayList<>()));
+    }
+
+    @Test
+    void getTypeAssumptionsTest() {
+        Conclusion conclusion = new Conclusion(typeAssumptions, lambdaTerm, type);
+        assertEquals(typeAssumptions, conclusion.getTypeAssumptions());
+    }
+
+    @Test
+    void getLambdaTermTest() {
+        Conclusion conclusion = new Conclusion(typeAssumptions, lambdaTerm, type);
+        assertEquals(lambdaTerm, conclusion.getLambdaTerm());
+    }
+
+    @Test
+    void getTypeTest() {
+        Conclusion conclusion = new Conclusion(typeAssumptions, lambdaTerm, type);
+        assertEquals(type, conclusion.getType());
+    }
+}

src/test/java/edu/kit/typicalc/model/ConstraintTest.java

@@ -2,16 +2,16 @@ package edu.kit.typicalc.model;
 
 import edu.kit.typicalc.model.type.Type;
 import edu.kit.typicalc.model.type.TypeVariable;
-import edu.kit.typicalc.model.type.TypeVaribaleKind;
+import edu.kit.typicalc.model.type.TypeVariableKind;
 import nl.jqno.equalsverifier.EqualsVerifier;
 import org.junit.jupiter.api.Test;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
 
-public class ConstraintTest {
+class ConstraintTest {
 
-    private static final Type type1 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 1);
-    private static final Type type2 = new TypeVariable(TypeVaribaleKind.TREE, 2);
+    private static final Type type1 = new TypeVariable(TypeVariableKind.USER_INPUT, 1);
+    private static final Type type2 = new TypeVariable(TypeVariableKind.TREE, 2);
 
     @Test
     void equalsTest() {

src/test/java/edu/kit/typicalc/model/SubstitutionTest.java

@@ -2,7 +2,7 @@ package edu.kit.typicalc.model;
 
 import edu.kit.typicalc.model.type.Type;
 import edu.kit.typicalc.model.type.TypeVariable;
-import edu.kit.typicalc.model.type.TypeVaribaleKind;
+import edu.kit.typicalc.model.type.TypeVariableKind;
 import nl.jqno.equalsverifier.EqualsVerifier;
 import org.junit.jupiter.api.Test;
 
@@ -10,8 +10,8 @@ import static org.junit.jupiter.api.Assertions.assertEquals;
 
 class SubstitutionTest {
 
-    private static final TypeVariable var = new TypeVariable(TypeVaribaleKind.USER_INPUT, 1);
-    private static final Type type = new TypeVariable(TypeVaribaleKind.TREE, 2);
+    private static final TypeVariable var = new TypeVariable(TypeVariableKind.USER_INPUT, 1);
+    private static final Type type = new TypeVariable(TypeVariableKind.TREE, 2);
 
     @Test
     void equalsTest() {

src/test/java/edu/kit/typicalc/model/TypeVariableFactoryTest.java

@@ -0,0 +1,35 @@
+package edu.kit.typicalc.model;
+
+import edu.kit.typicalc.model.type.TypeVariable;
+import edu.kit.typicalc.model.type.TypeVariableKind;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertNotEquals;
+
+class TypeVariableFactoryTest {
+
+    @Test
+    void createGivenKind() {
+        for (TypeVariableKind kind : TypeVariableKind.values()) {
+            TypeVariableFactory factory = new TypeVariableFactory(kind);
+            assertEquals(kind, factory.nextTypeVariable().getKind());
+        }
+    }
+
+    @Test
+    void createDistinctTypeVariables_100() {
+        TypeVariableFactory factory = new TypeVariableFactory(TypeVariableKind.TREE);
+
+        TypeVariable[] typeVariables = new TypeVariable[100];
+        for (int i = 0; i < 100; i++) {
+            typeVariables[i] = factory.nextTypeVariable();
+        }
+
+        for (int i = 0; i < 100; i++) {
+            for (int j = i + 1; j < 100; j++) {
+                assertNotEquals(typeVariables[i], typeVariables[j]);
+            }
+        }
+    }
+}

src/test/java/edu/kit/typicalc/model/type/FunctionTypeTest.java

@@ -14,9 +14,9 @@ class FunctionTypeTest {
 
     @Test
     void substitute() {
-        TypeVariable typeVariable1 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 1);
-        TypeVariable typeVariable2 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 2);
-        TypeVariable typeVariable3 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 3);
+        TypeVariable typeVariable1 = new TypeVariable(TypeVariableKind.USER_INPUT, 1);
+        TypeVariable typeVariable2 = new TypeVariable(TypeVariableKind.USER_INPUT, 2);
+        TypeVariable typeVariable3 = new TypeVariable(TypeVariableKind.USER_INPUT, 3);
 
         FunctionType functionType1 = new FunctionType(typeVariable1, typeVariable2);
 
@@ -27,10 +27,10 @@ class FunctionTypeTest {
 
     @Test
     void substitute2() {
-        TypeVariable typeVariable1 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 1);
-        TypeVariable typeVariable2 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 2);
-        TypeVariable typeVariable3 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 3);
-        TypeVariable typeVariable4 = new TypeVariable(TypeVaribaleKind.USER_INPUT, 4);
+        TypeVariable typeVariable1 = new TypeVariable(TypeVariableKind.USER_INPUT, 1);
+        TypeVariable typeVariable2 = new TypeVariable(TypeVariableKind.USER_INPUT, 2);
+        TypeVariable typeVariable3 = new TypeVariable(TypeVariableKind.USER_INPUT, 3);
+        TypeVariable typeVariable4 = new TypeVariable(TypeVariableKind.USER_INPUT, 4);
 
         FunctionType functionType1 = new FunctionType(typeVariable1, typeVariable2);
         FunctionType functionType2 = new FunctionType(functionType1, typeVariable3);

src/test/java/edu/kit/typicalc/model/type/UnificationTest.java

@@ -13,9 +13,9 @@ import static org.junit.jupiter.api.Assertions.assertTrue;
 class UnificationTest {
     @Test
     void all() {
-        TypeVariable a1 = new TypeVariable(TypeVaribaleKind.TREE, 1);
-        TypeVariable a2 = new TypeVariable(TypeVaribaleKind.TREE, 2);
-        TypeVariable a3 = new TypeVariable(TypeVaribaleKind.TREE, 3);
+        TypeVariable a1 = new TypeVariable(TypeVariableKind.TREE, 1);
+        TypeVariable a2 = new TypeVariable(TypeVariableKind.TREE, 2);
+        TypeVariable a3 = new TypeVariable(TypeVariableKind.TREE, 3);
         FunctionType id = new FunctionType(a1, a1);
         FunctionType fun = new FunctionType(a2, a3);
         NamedType string = new NamedType("string");