From c72df7ff03966cdcd16b3a7ad37e52a56163d407 Mon Sep 17 00:00:00 2001 From: uogau Date: Wed, 27 Jan 2021 21:03:11 +0100 Subject: [PATCH] Abstrakte Steps auch commited --- .../edu/kit/typicalc/model/step/AbsStep.java | 32 ++++++++++++ .../edu/kit/typicalc/model/step/AppStep.java | 36 ++++++++++++++ .../kit/typicalc/model/step/ConstStep.java | 18 +++++++ .../edu/kit/typicalc/model/step/LetStep.java | 49 +++++++++++++++++++ .../edu/kit/typicalc/model/step/VarStep.java | 32 ++++++++++++ 5 files changed, 167 insertions(+) create mode 100644 src/main/java/edu/kit/typicalc/model/step/AbsStep.java create mode 100644 src/main/java/edu/kit/typicalc/model/step/AppStep.java create mode 100644 src/main/java/edu/kit/typicalc/model/step/ConstStep.java create mode 100644 src/main/java/edu/kit/typicalc/model/step/LetStep.java create mode 100644 src/main/java/edu/kit/typicalc/model/step/VarStep.java diff --git a/src/main/java/edu/kit/typicalc/model/step/AbsStep.java b/src/main/java/edu/kit/typicalc/model/step/AbsStep.java new file mode 100644 index 0000000..3cfb558 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/step/AbsStep.java @@ -0,0 +1,32 @@ +package edu.kit.typicalc.model.step; + +import edu.kit.typicalc.model.Conclusion; +import edu.kit.typicalc.model.Constraint; + +/** + * Models one step of the inference tree where the abstraction rule is applied. + */ +public abstract class AbsStep extends InferenceStep { + + private InferenceStep premise; + + /** + * Initializes a new AbsStep with the given values. + * @param premise the premise of this step + * @param conclusion the conclusion of this step + * @param constraint the constraint added in this step + */ + protected AbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) { + super(conclusion, constraint); + this.premise = premise; + } + + /** + * Getter for the premise of this step. + * @return premise the premise of this step + */ + public InferenceStep getPremise() { + return this.premise; + } + +} diff --git a/src/main/java/edu/kit/typicalc/model/step/AppStep.java b/src/main/java/edu/kit/typicalc/model/step/AppStep.java new file mode 100644 index 0000000..d9578cf --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/step/AppStep.java @@ -0,0 +1,36 @@ +package edu.kit.typicalc.model.step; + +import edu.kit.typicalc.model.Conclusion; +import edu.kit.typicalc.model.Constraint; + +/** + * Models one step of the inference tree where the application rule is applied. The first + * premise contains the sub-tree of inference steps for the function of the application term. + * The second premise contains the sub-tree of inference steps for the input of the application + * term. + */ +public abstract class AppStep extends InferenceStep { + private InferenceStep premise1; + private InferenceStep premise2; + + protected AppStep(InferenceStep premise1, InferenceStep premise2, Conclusion conclusion, Constraint constraint) { + super(conclusion, constraint); + this.premise1 = premise1; + this.premise2 = premise2; + } + + /** + * Getter for the first premise of this Step. + * @return premise1 the first premise of this Step. + */ + public InferenceStep getPremise1() { + return premise1; + } + /** + * Getter for the second premise of this Step. + * @return premise2 the second premise of this Step. + */ + public InferenceStep getPremise2() { + return premise2; + } +} diff --git a/src/main/java/edu/kit/typicalc/model/step/ConstStep.java b/src/main/java/edu/kit/typicalc/model/step/ConstStep.java new file mode 100644 index 0000000..dccf9be --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/step/ConstStep.java @@ -0,0 +1,18 @@ +package edu.kit.typicalc.model.step; + +import edu.kit.typicalc.model.Conclusion; +import edu.kit.typicalc.model.Constraint; + +/** + * Models one step of the inference tree where the constant rule is applied. + */ +public abstract class ConstStep extends InferenceStep { + /** + * Initializes a new ConstStep with the given values. + * @param conclusion the conclusion of this step + * @param constraint the constraint added in this step + */ + protected ConstStep(Conclusion conclusion, Constraint constraint) { + super(conclusion, constraint); + } +} diff --git a/src/main/java/edu/kit/typicalc/model/step/LetStep.java b/src/main/java/edu/kit/typicalc/model/step/LetStep.java new file mode 100644 index 0000000..30312e4 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/step/LetStep.java @@ -0,0 +1,49 @@ +package edu.kit.typicalc.model.step; + +import edu.kit.typicalc.model.Conclusion; +import edu.kit.typicalc.model.Constraint; +import edu.kit.typicalc.model.TypeInfererLet; + +/** + * Models one step of the inference tree where the let rule is applied. A let step contains an + * additional instance of a type inferer that is responisble for the „sub-inference“ that takes + * place when applying the let rule. This type inferer grants access to all the information + * needed to visualize this sub-inference. + * If the sub-inference fails due to a contradiction or an infinite type forming in its unification, + * the inference step representing the second premise of the let step should not be created + * and the „outer“ inference should be interrupted + */ +public abstract class LetStep extends InferenceStep { + private InferenceStep premise; + private TypeInfererLet typeInferer; + + /** + * Initializes a new LetStep with the given values. + * @param conclusion the conclusion of this step + * @param constraint the constraint added in this step + * @param premise the right premise of this step + * @param typeInferer the typeInferer that performs the Type Inference for the premise + * that needs its own type Inference. + */ + protected LetStep(Conclusion conclusion, Constraint constraint, InferenceStep premise, TypeInfererLet typeInferer) { + super(conclusion, constraint); + this.premise = premise; + this.typeInferer = typeInferer; + } + /** + * Returns the premise of the let step that doesn’t have its own sub-inference (the + * one usually placed right in the proof tree). + * @return premise the right premise of this step + */ + public InferenceStep getPremise() { + return premise; + } + + /** + * Returns the TypeInferer for the premise which needs its own type Inference. + * @return typeInferer the type inferer of the sub-inference + */ + public TypeInfererLet getTypeInferer() { + return typeInferer; + } +} diff --git a/src/main/java/edu/kit/typicalc/model/step/VarStep.java b/src/main/java/edu/kit/typicalc/model/step/VarStep.java new file mode 100644 index 0000000..b18740e --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/step/VarStep.java @@ -0,0 +1,32 @@ +package edu.kit.typicalc.model.step; + +import edu.kit.typicalc.model.Conclusion; +import edu.kit.typicalc.model.Constraint; +import edu.kit.typicalc.model.type.TypeAbstraction; + +/** + * Models one step of the inference tree where the variable rule is applied. It contains a type + * abstraction that is identified as the type of the variable in the premise of the step. + */ +public abstract class VarStep extends InferenceStep { + private TypeAbstraction typeAbstractionInPremise; + + /** + * Initializes a new VarStep with the given values. + * @param conclusion the conclusion of this step + * @param constraint the constraint added in this step + * @param typeAbstractionInPremise the type abstraction in the premise of this step + */ + protected VarStep(Conclusion conclusion, Constraint constraint, TypeAbstraction typeAbstractionInPremise) { + super(conclusion, constraint); + this.typeAbstractionInPremise = typeAbstractionInPremise; + } + /** + * Returns the type abstraction in the premise of the step, that is identified as the + * variable’s type. + * @return the type abstraction in the premise of this step + */ + public TypeAbstraction getTypeAbsInPremise() { + return typeAbstractionInPremise; + } +}