diff --git a/src/main/java/edu/kit/typicalc/model/Conclusion.java b/src/main/java/edu/kit/typicalc/model/Conclusion.java new file mode 100644 index 0000000..6006dd8 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/Conclusion.java @@ -0,0 +1,43 @@ +package edu.kit.typicalc.model; + +/** + * Models the conclusion of an inference rule and consists of a list of type assumptions, a lambda term and a type. + * This class is used in inference steps to represent the conclusion of that specific application of the inference rule. + */ +public class Conclusion { + + /** + * Initializes a new Conclusion with the given type assumptions, lambda term and type. + * + * @param typeAssumptions the type assumptions used in the conclusion + * @param lambdaTerm the lambda term in the conclusion + * @param type the type assigned to the lambda term in the conclusion + */ + protected Conclusion(Map typeAssumptions, LambdaTerm lambdaTerm, Type type) { + // TODO + } + + /** + * @return the type assumptions used in the conclusion + */ + public Map getTypeAssumptions() { + return null; + // TODO + } + + /** + * @return the lambda term in the conclusion + */ + public LambdaTerm getLambdaTerm() { + return null; + // TODO + } + + /** + * @return the type assigned to the lambda term in the conclusion + */ + public Type getType() { + return null; + // TODO + } +} diff --git a/src/main/java/edu/kit/typicalc/model/Constraint.java b/src/main/java/edu/kit/typicalc/model/Constraint.java new file mode 100644 index 0000000..226c41a --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/Constraint.java @@ -0,0 +1,33 @@ +package edu.kit.typicalc.model; + +/** + * Constrains two types to be equal. + */ +public class Constraint { + /** + * Creates a new constraint using the two types. + * + * @param a first type + * @param b second type + */ + public Constraint(Type a, Type b) { + // TODO + } + + /** + * @return the first type + */ + public Type getFirstType() { + return null; + // TODO + } + + /** + * @return the second type + */ + public Type getSecondType() { + return null; + // TODO + } + +} diff --git a/src/main/java/edu/kit/typicalc/model/Substitution.java b/src/main/java/edu/kit/typicalc/model/Substitution.java new file mode 100644 index 0000000..e922a3f --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/Substitution.java @@ -0,0 +1,33 @@ +package edu.kit.typicalc.model; + +/** + * A substitution specifies that some type should be replaced by a different type. + */ +public class Substitution { + /** + * Creates a new substitution using a type variable a and a type b. When the substitution is applied to a type, + * all occurring instances of a should be substituted with b. + * + * @param a variable to be replaced + * @param b type to insert + */ + public Substitution(TypeVariable a, Type b) { + // TODO + } + + /** + * @return the type variable + */ + public TypeVariable getVariable() { + return null; + // TODO + } + + /** + * @return the replacement type + */ + Type getType() { + return null; + // TODO + } +} diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java new file mode 100644 index 0000000..b2eb221 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/Tree.java @@ -0,0 +1,63 @@ +package edu.kit.typicalc.model; + +import java.util.List; + +/** + * Models the proof tree formed when the type of a lambda term is inferred. + * A Tree consists of a tree-like structure of inference steps and a list of constraints that + * are part of these steps. It is guaranteed that these members can be accessed right after + * instantiation (no additional initialization is required). + */ +public class Tree implements TermVisitor { + + /** + * Initializes a new Tree representing the proof tree for the type inference of the given + * lambda term considering the given type assumptions. The inference step structure + * and constraint list are generated here. + * + * @param typeAssumptions the type assumptions to consider when generating the tree + * @param lambdaTerm the lambda term to generate the tree for + */ + protected Tree(Map typeAssumptions, LambdaTerm lambdaTerm) { + // TODO + } + + /** + * Initializes a new Tree representing the proof tree for the type inference of the given + * lambda term considering the given type assumptions. This constructor is supposed + * to be used if the lambda term is part of a let term. To generate unique type + * variable names, a type variable factory is provided as a parameter. The inference + * step structure and constraint list are generated here. + * + * @param typeAssumptions the type assumptions to consider when generating the tree + * @param lambdaTerm the lambda term to generate the tree for + * @param typeVariableFactory the type variable factory to use + */ + protected Tree(Map typeAssumptions, LambdaTerm lambdaTerm, + TypeVariableFactory typeVariableFactory) { + // TODO + } + + /** + * Returns the first (on the undermost level) inference step of the proof tree, containing + * the original lambda term that is being type-inferred in this tree and presenting an + * entry point for the tree-like inference step structure. + * + * @return the first inference step of the tree + */ + protected InferenceStep getFirstInferenceStep() { + return null; + // TODO; + } + + /** + * Returns the list of constraints that formed while generating the inference step tree + * structure, needed for the subsequent unification. + * + * @return the constraint list of the tree + */ + protected List getConstraints() { + return null; + // TODO + } +} diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java new file mode 100644 index 0000000..0118a87 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java @@ -0,0 +1,46 @@ +package edu.kit.typicalc.model; + +import java.util.List; + +/** + * Models the final result of the type inference with the most general unifier (mgu) and + * the final inferred type of the lambda term. It is guaranteed that these members can be + * accessed right after instantiation (no additional initialization is required). + */ +public class TypeInferenceResult { + /** + * Initializes a new TypeInferenceResult for the given substitutions (resulting from + * the unification) and the given type variable belonging to the original lambda term + * of the type inference. The final type is obtained by applying the most general unifier + * to this given type variable. The mgu and the final type are generated here. + * + * @param substitutions the substitutions to generate the mgu and the final type + * @param typeVar the type variable belonging to the original lambda term + */ + protected TypeInferenceResult(List substitutions, TypeVariable typeVar) { + // TODO + } + + /** + * Returns the most general unifier (mgu), as a list of substitutions. If no valid type + * (correlating with no valid mgu) can be found for the lambda term to type-infer, null is returned. + * + * @return the most general unifier, null if there is no valid mgu + */ + protected List getMGU() { + return null; + // TODO + } + + /** + * Returns the type that is the result of the type inference. It is obtained by applying + * the mgu to the type variable the type inference result was given in its construstor. + * If no valid type can be found for the lambda term to type-infer, null is returned. + * + * @return the final type of the lambda term, null if there is no valid type + */ + protected Type getType() { + return null; + // TODO + } +} diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferer.java b/src/main/java/edu/kit/typicalc/model/TypeInferer.java new file mode 100644 index 0000000..372a5e2 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/TypeInferer.java @@ -0,0 +1,51 @@ +package edu.kit.typicalc.model; + +import java.util.List; + +/** + * The type inferer is responsible for the whole type inference of a given lambda term, taking + * into account the given type assumptions. It implements the TypeInfererInterface and + * therefore can hand out an inference step structure, a list of unification steps, the most + * general unifier and the final type suiting the type inference of the given lambda term. It is + * guaranteed that this information can be accessed right after instantiation (no additional + * initialization is required). + */ +public class TypeInferer implements TypeInfererInterface { + + /** + * Initializes a new TypeInferer for the given type assumptions and lambda term. + * The inference step structure, unification steps, the most general unifier and the + * final type are generated and calculated here. + * + * @param lambdaTerm the lambda term to generate the tree for + * @param typeAssumptions the type assumptions to consider when generating the tree + */ + protected TypeInferer(LambdaTerm lambdaTerm, Map typeAssumptions) { + // TODO + } + + + @Override + public InferenceStep getFirstInferenceStep() { + return null; + // TODO + } + + @Override + public List getUnificationSteps() { + return null; + // TODO + } + + @Override + public List getMGU() { + return null; + // TODO + } + + @Override + public Type getType() { + return null; + // TODO + } +} diff --git a/src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java b/src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java new file mode 100644 index 0000000..b924d97 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java @@ -0,0 +1,41 @@ +package edu.kit.typicalc.model; + +import java.util.List; + +/** + * Interface for a type inferer with getter methods used to extract the information about + * the type inference that is needed to visualize it step by step. + */ +public interface TypeInfererInterface { + /** + * Returns the first (on the undermost level) inference step of the proof tree of the + * type inference, presenting an entry point for the tree-like inference step structure. + * + * @return the first inference step of the proof tree + */ + InferenceStep getFirstInferenceStep(); + + /** + * Returns the list of unification steps of this type inference. + * + * @return the list of unification steps + */ + List getUnificationSteps(); + + /** + * Returns the most general unifier (mgu) for the lambda term that is type-inferred, + * as a list of substitutions. If no valid type (correlating with no valid mgu) can be + * found for the lambda term to type-infer, null is returned. + * + * @return the most general unifier, null if there is no valid mgu + */ + List getMGU(); + + /** + * Returns the type that is the result of the type inference. + * If no valid type can be found for the lambda term to type-infer, null is returned. + * + * @return the final type of the lambda term, null if there is no valid type + */ + Type getType(); +} diff --git a/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java b/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java new file mode 100644 index 0000000..23eb32e --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java @@ -0,0 +1,36 @@ +package edu.kit.typicalc.model; + +import java.util.List; + +/** + * Instances of this subclass of TypeInferer are used to execute the sub-inference starting in let steps. + * They provide an extended constructor to make sure this sub-inference is consistent with the „outer“ inference. + */ +public class TypeInfererLet extends TypeInferer { + /** + * Initializes a new TypeInfererLet for the given type assumptions, lambda term and type variable factory. + * + * @param lambdaTerm the lambda term to generate the tree for + * @param typeAssumptions the type assumptions to consider when generating the tree + * @param typeVarFactory the type variable factory that should be used in this inference to guarantee consistecy + * with the outer inference + */ + protected TypeInfererLet(LambdaTerm lambdaTerm, Map typeAssumptions, + TypeVariableFactory typeVarFactory) { + super(lambdaTerm, typeAssumptions); + // TODO + } + + /** + * Let σ be the most general unifier resulting from this type inference. + * The following set of constraints is then returned (needed in the outer inference): + * C := { αi = σ(αi) | σ defined for αi } + * + * @return the constraints needed in the outer inference + */ + public List getLetConstraints() { + return null; + // TODO + } + +} diff --git a/src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java b/src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java new file mode 100644 index 0000000..1f746a6 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java @@ -0,0 +1,24 @@ +package edu.kit.typicalc.model; + +/** + * Provides unique type variables on demand. + */ +public class TypeVariableFactory { + + /** + * Initializes a new type variable factory. + */ + protected TypeVariableFactory() { + // TODO + } + + /** + * Creates a new unique type variable. This method will never return the same variable twice. + * + * @return a new unique type variable + */ + public TypeVariable nextTypeVariable() { + return null; + // TODO + } +} diff --git a/src/main/java/edu/kit/typicalc/view/content/type_inference_content/TypeInferenceViewView.java b/src/main/java/edu/kit/typicalc/view/content/type_inference_content/TypeInferenceView.java similarity index 86% rename from src/main/java/edu/kit/typicalc/view/content/type_inference_content/TypeInferenceViewView.java rename to src/main/java/edu/kit/typicalc/view/content/type_inference_content/TypeInferenceView.java index ef77391..c825bc7 100644 --- a/src/main/java/edu/kit/typicalc/view/content/type_inference_content/TypeInferenceViewView.java +++ b/src/main/java/edu/kit/typicalc/view/content/type_inference_content/TypeInferenceView.java @@ -11,14 +11,14 @@ import edu.kit.typicalc.view.main.MainViewImpl; @Route(value = "visualize", layout = MainViewImpl.class) @PageTitle("TypeInferenceView") -@CssImport("./styles/views/typeinferenceview/type-inference-view-view.css") -public class TypeInferenceViewView extends HorizontalLayout { +@CssImport("./styles/views/typeinferenceview/type-inference-view.css") +public class TypeInferenceView extends HorizontalLayout { private TextField name; private Button sayHello; - public TypeInferenceViewView() { - setId("type-inference-view-view"); + public TypeInferenceView() { + setId("type-inference-view"); name = new TextField("Your name"); sayHello = new Button("Say hello"); add(name, sayHello); diff --git a/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java b/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java index 935e873..d41fefd 100644 --- a/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java +++ b/src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java @@ -17,7 +17,7 @@ import com.vaadin.flow.component.tabs.Tabs; import com.vaadin.flow.component.tabs.TabsVariant; import com.vaadin.flow.router.PageTitle; import com.vaadin.flow.router.RouterLink; -import edu.kit.typicalc.view.content.type_inference_content.TypeInferenceViewView; +import edu.kit.typicalc.view.content.type_inference_content.TypeInferenceView; import java.util.Optional; @@ -78,7 +78,7 @@ public class MainViewImpl extends AppLayout { } private Component[] createMenuItems() { - return new Tab[]{createTab("TypeInferenceView", TypeInferenceViewView.class)}; + return new Tab[]{createTab("TypeInferenceView", TypeInferenceView.class)}; } private static Tab createTab(String text, Class navigationTarget) {