From 8700a83390ee182842b2f2e9204628ab3adc43ad Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 27 Jan 2021 09:15:29 +0100 Subject: [PATCH] =?UTF-8?q?Klassenger=C3=BCst?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/main/java/edu/kit/typicalc/model/Conclusion.java | 7 +++++++ src/main/java/edu/kit/typicalc/model/Constraint.java | 2 ++ src/main/java/edu/kit/typicalc/model/Substitution.java | 3 +++ src/main/java/edu/kit/typicalc/model/Tree.java | 7 +++++++ .../java/edu/kit/typicalc/model/TypeInferenceResult.java | 3 +++ src/main/java/edu/kit/typicalc/model/TypeInferer.java | 7 +++++++ .../java/edu/kit/typicalc/model/TypeInfererInterface.java | 3 +++ src/main/java/edu/kit/typicalc/model/TypeInfererLet.java | 5 +++++ .../java/edu/kit/typicalc/model/TypeVariableFactory.java | 2 ++ src/main/java/edu/kit/typicalc/model/UnificationStep.java | 4 ++++ .../java/edu/kit/typicalc/model/step/InferenceStep.java | 4 ++++ src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java | 4 ++++ src/main/java/edu/kit/typicalc/model/term/TermVisitor.java | 4 ++++ src/main/java/edu/kit/typicalc/model/term/VarTerm.java | 4 ++++ src/main/java/edu/kit/typicalc/model/type/Type.java | 4 ++++ .../java/edu/kit/typicalc/model/type/TypeAbstraction.java | 4 ++++ .../java/edu/kit/typicalc/model/type/TypeVariable.java | 4 ++++ 17 files changed, 71 insertions(+) create mode 100644 src/main/java/edu/kit/typicalc/model/UnificationStep.java create mode 100644 src/main/java/edu/kit/typicalc/model/step/InferenceStep.java create mode 100644 src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java create mode 100644 src/main/java/edu/kit/typicalc/model/term/TermVisitor.java create mode 100644 src/main/java/edu/kit/typicalc/model/term/VarTerm.java create mode 100644 src/main/java/edu/kit/typicalc/model/type/Type.java create mode 100644 src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java create mode 100644 src/main/java/edu/kit/typicalc/model/type/TypeVariable.java diff --git a/src/main/java/edu/kit/typicalc/model/Conclusion.java b/src/main/java/edu/kit/typicalc/model/Conclusion.java index 6006dd8..763667d 100644 --- a/src/main/java/edu/kit/typicalc/model/Conclusion.java +++ b/src/main/java/edu/kit/typicalc/model/Conclusion.java @@ -1,5 +1,12 @@ 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.Type; +import edu.kit.typicalc.model.type.TypeAbstraction; + +import java.util.Map; + /** * 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. diff --git a/src/main/java/edu/kit/typicalc/model/Constraint.java b/src/main/java/edu/kit/typicalc/model/Constraint.java index 226c41a..34c9a49 100644 --- a/src/main/java/edu/kit/typicalc/model/Constraint.java +++ b/src/main/java/edu/kit/typicalc/model/Constraint.java @@ -1,5 +1,7 @@ package edu.kit.typicalc.model; +import edu.kit.typicalc.model.type.Type; + /** * Constrains two types to be equal. */ diff --git a/src/main/java/edu/kit/typicalc/model/Substitution.java b/src/main/java/edu/kit/typicalc/model/Substitution.java index e922a3f..65f6713 100644 --- a/src/main/java/edu/kit/typicalc/model/Substitution.java +++ b/src/main/java/edu/kit/typicalc/model/Substitution.java @@ -1,5 +1,8 @@ package edu.kit.typicalc.model; +import edu.kit.typicalc.model.type.Type; +import edu.kit.typicalc.model.type.TypeVariable; + /** * A substitution specifies that some type should be replaced by a different type. */ diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index b2eb221..6c7eb80 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/src/main/java/edu/kit/typicalc/model/Tree.java @@ -1,6 +1,13 @@ package edu.kit.typicalc.model; +import edu.kit.typicalc.model.step.InferenceStep; +import edu.kit.typicalc.model.term.LambdaTerm; +import edu.kit.typicalc.model.term.TermVisitor; +import edu.kit.typicalc.model.term.VarTerm; +import edu.kit.typicalc.model.type.TypeAbstraction; + import java.util.List; +import java.util.Map; /** * Models the proof tree formed when the type of a lambda term is inferred. diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java index 0118a87..87878fd 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java @@ -1,5 +1,8 @@ package edu.kit.typicalc.model; +import edu.kit.typicalc.model.type.Type; +import edu.kit.typicalc.model.type.TypeVariable; + import java.util.List; /** diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferer.java b/src/main/java/edu/kit/typicalc/model/TypeInferer.java index 372a5e2..67de596 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferer.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInferer.java @@ -1,6 +1,13 @@ package edu.kit.typicalc.model; +import edu.kit.typicalc.model.step.InferenceStep; +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 java.util.List; +import java.util.Map; /** * The type inferer is responsible for the whole type inference of a given lambda term, taking diff --git a/src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java b/src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java index b924d97..2f78826 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java @@ -1,5 +1,8 @@ package edu.kit.typicalc.model; +import edu.kit.typicalc.model.step.InferenceStep; +import edu.kit.typicalc.model.type.Type; + import java.util.List; /** diff --git a/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java b/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java index 23eb32e..eb359be 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java +++ b/src/main/java/edu/kit/typicalc/model/TypeInfererLet.java @@ -1,6 +1,11 @@ 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.TypeAbstraction; + import java.util.List; +import java.util.Map; /** * Instances of this subclass of TypeInferer are used to execute the sub-inference starting in let steps. diff --git a/src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java b/src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java index 1f746a6..3a9669e 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java +++ b/src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java @@ -1,5 +1,7 @@ package edu.kit.typicalc.model; +import edu.kit.typicalc.model.type.TypeVariable; + /** * Provides unique type variables on demand. */ diff --git a/src/main/java/edu/kit/typicalc/model/UnificationStep.java b/src/main/java/edu/kit/typicalc/model/UnificationStep.java new file mode 100644 index 0000000..f2b40be --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/UnificationStep.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model; + +public class UnificationStep { +} diff --git a/src/main/java/edu/kit/typicalc/model/step/InferenceStep.java b/src/main/java/edu/kit/typicalc/model/step/InferenceStep.java new file mode 100644 index 0000000..1f995bc --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/step/InferenceStep.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model.step; + +public class InferenceStep { +} diff --git a/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java b/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java new file mode 100644 index 0000000..6945106 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model.term; + +public class LambdaTerm { +} diff --git a/src/main/java/edu/kit/typicalc/model/term/TermVisitor.java b/src/main/java/edu/kit/typicalc/model/term/TermVisitor.java new file mode 100644 index 0000000..c35bec0 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/term/TermVisitor.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model.term; + +public interface TermVisitor { +} diff --git a/src/main/java/edu/kit/typicalc/model/term/VarTerm.java b/src/main/java/edu/kit/typicalc/model/term/VarTerm.java new file mode 100644 index 0000000..d00ef06 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/term/VarTerm.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model.term; + +public class VarTerm { +} diff --git a/src/main/java/edu/kit/typicalc/model/type/Type.java b/src/main/java/edu/kit/typicalc/model/type/Type.java new file mode 100644 index 0000000..f321ac8 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/type/Type.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model.type; + +public abstract class Type { +} diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java b/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java new file mode 100644 index 0000000..681f18c --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model.type; + +public class TypeAbstraction { +} diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java new file mode 100644 index 0000000..3c394fe --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/type/TypeVariable.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model.type; + +public class TypeVariable { +}