diff --git a/src/main/java/edu/kit/typicalc/model/type/FunctionType.java b/src/main/java/edu/kit/typicalc/model/type/FunctionType.java index 55bf2d7..78af02e 100644 --- a/src/main/java/edu/kit/typicalc/model/type/FunctionType.java +++ b/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 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 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 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 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; + } } diff --git a/src/main/java/edu/kit/typicalc/model/type/NamedType.java b/src/main/java/edu/kit/typicalc/model/type/NamedType.java index 66f4099..4b3ddc0 100644 --- a/src/main/java/edu/kit/typicalc/model/type/NamedType.java +++ b/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 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 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 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 constrainEqualToVariable(TypeVariable type) { + //TODO + return null; } } diff --git a/src/main/java/edu/kit/typicalc/model/type/Type.java b/src/main/java/edu/kit/typicalc/model/type/Type.java index f321ac8..0586fc2 100644 --- a/src/main/java/edu/kit/typicalc/model/type/Type.java +++ b/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 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 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 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 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; + } } diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java b/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java index 60343ee..ac2ef98 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java +++ b/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 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 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 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; + } + + } diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java index 2e88734..31d4bcd 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java +++ b/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 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 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 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 constrainEqualToVariable(TypeVariable type) { + //TODO + return null; } } diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java b/src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java index 6755bc4..d5baaef 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java +++ b/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); } diff --git a/src/main/java/edu/kit/typicalc/model/type/UnificationActions.java b/src/main/java/edu/kit/typicalc/model/type/UnificationActions.java new file mode 100644 index 0000000..3872256 --- /dev/null +++ b/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 constraints; + private Optional 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 constraints, Optional substitution) { + this.constraints = constraints; + this.substitution = substitution; + } + + /** + * Getter for constraints + * @return the constraints stored in this object + */ + public Collection getConstraints() { + return constraints; + } + + public Optional getSubstitution() { + return substitution; + } +} diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java index 1e9ab05..65a46cb 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java +++ b/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.*; diff --git a/src/main/java/edu/kit/typicalc/view/main/MainView.java b/src/main/java/edu/kit/typicalc/view/main/MainView.java index b32d4f0..6e71a4c 100644 --- a/src/main/java/edu/kit/typicalc/view/main/MainView.java +++ b/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 typeAssumptions); } }