Type-Paket

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

@@ -1,7 +1,130 @@
 package edu.kit.typicalc.model.type;
 
+import edu.kit.typicalc.model.UnificationError;
+import edu.kit.typicalc.util.Result;
+
+/**
+ * Models the type of an abstraction/function.
+ */
 public class FunctionType extends Type {
+
+    private Type parameter;
+    private Type output;
+    /**
+     * Initializes a new FunctionType with the given parameter and output types.
+     * @param parameter the type of this function’s parameter
+     * @param output the type of this function’s output
+     */
     public FunctionType(Type parameter, Type output) {
+        this.parameter = parameter;
+        this.output = output;
     }
 
+    /**
+     * Checks whether some type occurs in the parameter or output of this function.
+     * @param x the type to look for
+     * @return whether the specified type occurs in this type
+     */
+    @Override
+    public boolean contains(Type x) {
+        return (contains(parameter) || contains(output));
+    }
+
+    /**
+     * Substitutes a type variable for a different type.
+     * @param a  the type variable to replace
+     * @param b the type to insert
+     * @return a new FunctionType that is created by substituting a and b in the parameter
+     * and output type
+     */
+    @Override
+    public FunctionType substitute(TypeVariable a, Type b) {
+        boolean first = false;
+        boolean second = false;
+        if (this.parameter.equals(a)) {
+            first = true;
+        }
+        if (this.output.equals(a)) {
+             second = true;
+        }
+        if (first && second) {
+            return new FunctionType(b, b);
+        } else if (first) {
+            return new FunctionType(b, output);
+        } else if (second) {
+            return new FunctionType(parameter, b);
+        } else {
+            return this;
+        }
+    }
+
+    /**
+     * Accepts a visitor.
+     * @param typeVisitor the visitor that wants to visit this
+     */
+    @Override
+    public void accept(TypeVisitor typeVisitor) {
+        typeVisitor.visit(this);
+    }
+
+    /**
+     * Computes the neccessary constraints (and substitution) to unify this type with
+     * another. This method uses the constrainEqualToFunction method on the other
+     * type.
+     * @param type  the other type
+     * @return unification steps neccessary, or an error if that is impossible
+     */
+    public Result<UnificationActions, UnificationError> constrainEqualTo(Type type) {
+        //TODO
+        return null;
+    }
+
+    /**
+     * Computes the neccessary constraints (and substitution) to unify this type with a
+     * function type.
+     * @param type the function type
+     * @return unification steps neccessary, or an error if that is impossible
+     */
+    public Result<UnificationActions, UnificationError> constrainEqualToFunction(Type type) {
+        //TODO
+        return null;
+    }
+
+    /**
+     * Computes the neccessary constraints (and substitution) to unify this type with a
+     * named type.
+     * @param type the named type
+     * @return unification steps neccessary, or an error if that is impossible
+     */
+    public Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type) {
+        //TODO
+        return null;
+    }
+
+    /**
+     * Computes the neccessary constraints (and substitution) to unify this type with a
+     * type variable.
+     * @param type the type variable
+     * @return the unification steps neccessary, or an error if that is impossible
+     */
+    public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) {
+        //TODO
+        return null;
+    }
+
+    /**
+     * Getter for output
+     * @return output
+     */
+    public Type getOutput() {
+        return output;
+    }
+
+    /**
+     * Getter for parameter
+     * @return parameter
+     */
+    public Type getParameter() {
+        return parameter;
+    }
 }

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

@@ -1,10 +1,111 @@
 package edu.kit.typicalc.model.type;
 
+import edu.kit.typicalc.model.UnificationError;
+import edu.kit.typicalc.util.Result;
+
+/**
+ * Models a simple named type.
+ */
 public class NamedType extends Type {
+	/**
+	 * boolean type
+	 */
 	public static final NamedType BOOLEAN = new NamedType("boolean");
+	/**
+	 * int type
+	 */
 	public static final NamedType INT = new NamedType("int");
 
+	private String name;
+
+	/**
+	 * Initializes a new NamedType with the given name.
+	 * @param name the name of this type
+	 */
 	public NamedType(String name) {
-		// TODO
+		this.name = name;
+	}
+
+	/**
+	 * Returns the name of the named type.
+	 * @return the name of this type
+	 */
+	public String getName() {
+		return name;
+	}
+
+	/**
+	 * Checks whether some type occurs in this type.
+	 * @param x the type to look for
+	 * @return whether the specified type is equal to this type
+	 */
+	public boolean contains(Type x) {
+		return this.equals(x);
+	}
+
+	/**
+	 * Substitutes a type variable for a different type.
+	 * @param a the type to replace
+	 * @param b the type to insert
+	 * @return itself, or b if a is equal to this object
+	 */
+	@Override
+	public Type substitute(TypeVariable a, Type b) {
+		//TODO: Methode überhaupt sinnvoll?
+		return null;
+	}
+
+	/**
+	 * Accepts a visitor.
+	 * @param typeVisitor the visitor that wants to visit this
+	 */
+	@Override
+	public void accept(TypeVisitor typeVisitor) {
+		typeVisitor.visit(this);
+	}
+
+	/**
+	 * Computes the neccessary constraints (and substitution) to unify this type with
+	 * another. This method uses the constrainEqualToNamedType method on the other
+	 * type.
+	 * @param type  the other type
+	 * @return unification steps neccessary, or an error if that is impossible
+	 */
+	public Result<UnificationActions, UnificationError> constrainEqualTo(Type type) {
+		//TODO
+		return null;
+	}
+
+	/**
+	 * Computes the neccessary constraints (and substitution) to unify this type with a
+	 * function type.
+	 * @param type the function type
+	 * @return unification steps neccessary, or an error if that is impossible
+	 */
+	public Result<UnificationActions, UnificationError> constrainEqualToFunction(Type type) {
+		//TODO
+		return null;
+	}
+
+	/**
+	 * Computes the neccessary constraints (and substitution) to unify this type with a
+	 * named type.
+	 * @param type the named type
+	 * @return unification steps neccessary, or an error if that is impossible
+	 */
+	public Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type) {
+		//TODO
+		return null;
+	}
+
+	/**
+	 * Computes the neccessary constraints (and substitution) to unify this type with a
+	 * type variable.
+	 * @param type the type variable
+	 * @return the unification steps neccessary, or an error if that is impossible
+	 */
+	public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) {
+		//TODO
+		return null;
 	}
 }

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

@@ -1,4 +1,82 @@
 package edu.kit.typicalc.model.type;
 
+import edu.kit.typicalc.model.UnificationError;
+import edu.kit.typicalc.util.Result;
+
+/**
+ * Models the type of a lambda term.
+ */
 public abstract class Type {
+    /**
+     * Checks whether some type occurs in this type.
+     * @param x the type to look for
+     * @return whether the specified type occurs in this type
+     */
+    public abstract boolean contains(Type x);
+
+    /**
+     * Substitutes a type Variable for a different type
+     * @param a the type to replace
+     * @param b the type to insert
+     * @return a Type that is created by replacing a with b
+     */
+    public abstract Type substitute(TypeVariable a, Type b);
+
+    /**
+     * Accepts a visitor
+     * @param typeVisitor the visitor that wants to visit this
+     */
+    public abstract void accept(TypeVisitor typeVisitor);
+
+    /**
+     * Computes the neccessary constraints (and substitution) to unify this type with
+     * another type.
+     * @param type  the other type
+     * @return unification steps neccessary, or an error if that is impossible
+     */
+    public abstract Result<UnificationActions, UnificationError> constrainEqualTo(Type type);
+
+    /**
+     * Computes the neccessary constraints (and substitution) to unify this type with a
+     * function type.
+     * @param type the function type
+     * @return unification steps neccessary, or an error if that is impossible
+     */
+    public abstract Result<UnificationActions, UnificationError> constrainEqualToFunction(Type type);
+
+    /**
+     * Computes the neccessary constraints (and substitution) to unify this type with a
+     * named type.
+     * @param type the named type
+     * @return unification steps neccessary, or an error if that is impossible
+     */
+    public abstract Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type);
+
+    /**
+     * Computes the neccessary constraints (and substitution) to unify this type with a
+     * type variable.
+     * @param type the type variable
+     * @return the unification steps neccessary, or an error if that is impossible
+     */
+    public abstract Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type);
+
+    /**
+     * Checks whether this is equal to another Type
+     * @param o the other Type
+     * @return whether this is equal to the other Type or not.
+     */
+    @Override
+    public boolean equals(Object o) {
+        if (this instanceof NamedType && o instanceof NamedType) {
+            return ((NamedType) o).getName().equals(((NamedType) this).getName());
+        }
+        if (this instanceof TypeVariable && o instanceof TypeVariable) {
+            return ((TypeVariable) o).getIndex() == ((TypeVariable) this).getIndex();
+        }
+        if (this instanceof FunctionType && o instanceof FunctionType) {
+            return (((FunctionType) o).getOutput().equals(((FunctionType) this).getOutput())
+                    && ((FunctionType) o).getParameter().equals(((FunctionType) this).getParameter()));
+        }
+        return false;
+    }
 }

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

@@ -4,14 +4,71 @@ import edu.kit.typicalc.model.TypeVariableFactory;
 
 import java.util.List;
 
+/**
+ * Models a type abstraction with its type and the type variables bound by the for-all
+ * quantifier.
+ */
 public class TypeAbstraction {
+
+    private Type type;
+    private List<TypeVariable> quantifiedVariables;
+    /**
+     * Initializes a new type abstraction with its type and the type variables bound by
+     * the for-all quantifier.
+     * @param type  the type of the type abstraction
+     * @param quantifiedVariables the type variables bound by the for-all quantifier
+     */
     public TypeAbstraction(Type type, List<TypeVariable> quantifiedVariables) {
-
+        this.type = type;
+        this.quantifiedVariables = quantifiedVariables;
     }
+
+    /**
+     * Initializes a new type abstraction with its type and no type variables bound by the
+     * for-all quantifier.
+     * @param type the type of the type abstraction
+     */
     public TypeAbstraction(Type type) {
-
+        this.type = type;
+        this.quantifiedVariables = null;
     }
+
+    /**
+     * Instantiates the type abstraction with a new type and returns it. The new type
+     * contains new type variables generated by the given type variable factory.
+     * @param typeVarFactory  the type variable factory used to generate the new type
+     * variables
+     * @return the new type resulting from the instantiation of the type abstraction
+     */
     public Type instantiate(TypeVariableFactory typeVarFactory) {
+        //TODO
         return null;
     }
+
+    /**
+     * Indicates whether any type variables are quantified in the type abstraction.
+     * @return true if one or more type variables are quantified, false otherwise
+     */
+    public boolean hasQuantifiedVariables() {
+        return !quantifiedVariables.isEmpty();
+    }
+
+    /**
+     * Returns a list of all type variables that are bound by an for-all quantifier in the
+     * type abstraction.
+     * @return a list of all quantified type variables
+     */
+    public List<TypeVariable> getQuantifiedVariables() {
+        return quantifiedVariables;
+    }
+
+    /**
+     * Getter for the inner type of the type abstraction
+     * @return the inner type of the type abstraction
+     */
+    public Type getInnerType() {
+        return type;
+    }
+
+
 }

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

@@ -1,7 +1,99 @@
 package edu.kit.typicalc.model.type;
 
-public class TypeVariable extends Type {
-    public TypeVariable(int index) {
+import edu.kit.typicalc.model.UnificationError;
+import edu.kit.typicalc.util.Result;
 
+/**
+ * Models a type variable
+ */
+public class TypeVariable extends Type {
+    private int index;
+    /**
+     * Initializes a new TypeVariable with the given index.
+     * @param index the index of this variable
+     */
+    public TypeVariable(int index) {
+        this.index = index;
+    }
+
+    /**
+     * the index of the type variable as an integer
+     * @return index
+     */
+    public int getIndex() {
+        return index;
+    }
+
+    /**
+     * Checks whether some type occurs in this type.
+     * @param x the type to look for
+     * @return whether the specified type is equal to this type
+     */
+    @Override
+    public boolean contains(Type x) {
+        return this.equals(x);
+    }
+
+    /**
+     * Substitutes a type variable for a different type.
+     * @param a the type to replace
+     * @param b the type to insert
+     * @return itself, or b if a is equal to this object
+     */
+    public Type substitute(TypeVariable a, Type b) {
+        if (this.equals(a)) {
+        return b;
+        } else {
+            return this;
+        }
+    }
+
+    public void accept(TypeVisitor typeVisitor) {
+        typeVisitor.visit(this);
+    }
+
+    /**
+     * Computes the neccessary constraints (and substitution) to unify this type with
+     * another. This method uses the constrainEqualToVariable method on the other
+     * type.
+     * @param type  the other type
+     * @return unification steps neccessary, or an error if that is impossible
+     */
+    public Result<UnificationActions, UnificationError> constrainEqualTo(Type type) {
+        //TODO
+        return null;
+    }
+
+    /**
+     * Computes the neccessary constraints (and substitution) to unify this type with a
+     * function type.
+     * @param type the function type
+     * @return unification steps neccessary, or an error if that is impossible
+     */
+    public Result<UnificationActions, UnificationError> constrainEqualToFunction(Type type) {
+        //TODO
+        return null;
+    }
+
+    /**
+     * Computes the neccessary constraints (and substitution) to unify this type with a
+     * named type.
+     * @param type the named type
+     * @return unification steps neccessary, or an error if that is impossible
+     */
+    public Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type) {
+        //TODO
+        return null;
+    }
+
+    /**
+     * Computes the neccessary constraints (and substitution) to unify this type with a
+     * type variable.
+     * @param type the type variable
+     * @return the unification steps neccessary, or an error if that is impossible
+     */
+    public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) {
+        //TODO
+        return null;
     }
 }

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

@@ -1,23 +1,24 @@
 package edu.kit.typicalc.model.type;
 
-import com.fasterxml.jackson.databind.jsontype.NamedType;
-
+/**
+ * Can be implemented to process Type objects.
+ */
 public interface TypeVisitor {
 	/**
 	 * Visit a named type.
-	 * @param named the type
+	 * @param named the type to be visited
 	 */
 	void visit(NamedType named);
 
 	/**
 	 * Visit a type variable
-	 * @param variable the variable
+	 * @param variable the variable to be visited
 	 */
 	void visit(TypeVariable variable);
 
 	/**
 	 * Visit a function.
-	 * @param function the function
+	 * @param function the function to be visited
 	 */
 	void visit(FunctionType function);
 }

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

@@ -0,0 +1,37 @@
+package edu.kit.typicalc.model.type;
+
+import edu.kit.typicalc.model.Constraint;
+import edu.kit.typicalc.model.Substitution;
+
+import java.util.Collection;
+import java.util.Optional;
+
+/**
+ * Models the neccessary actions to process a constraint.
+ */
+public class UnificationActions {
+    private Collection<Constraint> constraints;
+    private Optional<Substitution> substitution;
+
+    /**
+     * Initializes this object using the provided constraints and substitution.
+     * @param constraints added constraints, if any
+     * @param substitution neccessary substitution, if any
+     */
+    protected UnificationActions(Collection<Constraint> constraints, Optional<Substitution> substitution) {
+        this.constraints = constraints;
+        this.substitution = substitution;
+    }
+
+    /**
+     * Getter for constraints
+     * @return the constraints stored in this object
+     */
+    public Collection<Constraint> getConstraints() {
+        return constraints;
+    }
+
+    public Optional<Substitution> getSubstitution() {
+        return substitution;
+    }
+}

src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java

@@ -1,7 +1,7 @@
 package edu.kit.typicalc.view.content.typeinferencecontent;
 
 
-import com.fasterxml.jackson.databind.jsontype.NamedType;
+import edu.kit.typicalc.model.type.NamedType;
 import edu.kit.typicalc.model.Conclusion;
 import edu.kit.typicalc.model.TypeInfererInterface;
 import edu.kit.typicalc.model.step.*;

src/main/java/edu/kit/typicalc/view/main/MainView.java

@@ -25,8 +25,7 @@ public interface MainView {
      */
     void displayError(ParseError error);
     
-     interface MainViewListener {
-        
+    interface MainViewListener {
         void typeInferLambdaString(String lambdaTerm, Map<String, String> typeAssumptions);
     }
 }