arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 18:30:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

Tree visit(varTerm), dafür Konstruktor von VarStep erweitert

Browse Source
This commit is contained in:
Johanna Stuber 2021-01-28 12:40:49 +01:00
parent 73516eb3b0
commit 3c72a5004c
9 changed files with 85 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/main/java/edu/kit/typicalc/model/Tree.java
View File

@ -150,7 +150,19 @@ public class Tree implements TermVisitorTree {
}
@Override
public InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
public InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType)
throws IllegalStateException {
TypeAbstraction premiseAbs = typeAssumptions.get(varTerm);
if (premiseAbs == null) {
throw new IllegalStateException("Cannot create VarStep for VarTerm '"
+ varTerm.getName() + "' without appropriate type assumption");
}
Type instantiation = premiseAbs.instantiate(typeVarFactory);
Constraint newConstraint = new Constraint(conclusionType, instantiation);
constraints.add(newConstraint);
Conclusion conclusion = new Conclusion(typeAssumptions, varTerm, conclusionType);
return stepFactory.createVarStep(premiseAbs, instantiation, conclusion, newConstraint);
}
}

7
src/main/java/edu/kit/typicalc/model/step/StepFactory.java
View File

@ -2,6 +2,7 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
/**
@ -34,14 +35,16 @@ public interface StepFactory {
* @return the created ConstStep
*/
ConstStep createConstStep(Conclusion conclusion, Constraint constraint);
/**
* Creates a VarStep.
* @param typeAbstraction the type abstraction of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created AbsStep
*/
VarStep createVarStep(TypeAbstraction typeAbstraction, Conclusion conclusion,
Constraint constraint);
VarStep createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs,
Conclusion conclusion, Constraint constraint);
//TODO LetStep
}

15
src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java
View File

@ -2,12 +2,14 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
/**
* A factory to create InferenceStep objects when let polymorphism is not used.
*/
public class StepFactoryDefault implements StepFactory {
/**
* Creates an AbsStepDefault.
* @param premise the premise of this step
@ -15,6 +17,7 @@ public class StepFactoryDefault implements StepFactory {
* @param constraint the constraint that can be derived from this step
* @return the created AbsStepDefault
*/
@Override
public AbsStepDefault createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) {
return new AbsStepDefault(premise, conclusion, constraint);
}
@ -27,28 +30,34 @@ public class StepFactoryDefault implements StepFactory {
* @param constraint the constraint that can be derived from this step
* @return the created AppStepDefault
*/
@Override
public AppStepDefault createAppStep(InferenceStep premise1, InferenceStep premise2,
Conclusion conclusion, Constraint constraint) {
return new AppStepDefault(premise1, premise2, conclusion, constraint);
}
/**
* Creates an ConstStepDefault.
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created ConstStepDefault
*/
@Override
public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint) {
return new ConstStepDefault(conclusion, constraint);
}
/**
* Creates a VarStepDefault.
* @param typeAbstraction the type abstraction of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created AbsStepDefault
*/
public VarStepDefault createVarStep(TypeAbstraction typeAbstraction, Conclusion conclusion,
Constraint constraint) {
return new VarStepDefault(typeAbstraction, conclusion, constraint);
@Override
public VarStepDefault createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs,
Conclusion conclusion, Constraint constraint) {
return new VarStepDefault(typeAbstraction, instantiatedTypeAbs, conclusion, constraint);
}
}

16
src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java
View File

@ -2,12 +2,14 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
/**
* A factory to create InferenceStep objects when let polymorphism is used.
*/
public class StepFactoryWithLet implements StepFactory {
/**
* Creates an AbsStepWithLet.
* @param premise the premise of this step
@ -15,6 +17,7 @@ public class StepFactoryWithLet implements StepFactory {
* @param constraint the constraint that can be derived from this step
* @return the created AbsStepWithLet
*/
@Override
public AbsStepWithLet createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) {
return new AbsStepWithLet(premise, conclusion, constraint);
}
@ -27,28 +30,35 @@ public class StepFactoryWithLet implements StepFactory {
* @param constraint the constraint that can be derived from this step
* @return the created AppStepDefault
*/
@Override
public AppStepDefault createAppStep(InferenceStep premise1, InferenceStep premise2,
Conclusion conclusion, Constraint constraint) {
return new AppStepDefault(premise1, premise2, conclusion, constraint);
}
/**
* Creates an ConstStepDefault.
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created ConstStepDefault
*/
@Override
public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint) {
return new ConstStepDefault(conclusion, constraint);
}
/**
* Creates a VarStepWithLet.
*
* @param typeAbstraction the type abstraction of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created VarStepWithLet
*/
public VarStepWithLet createVarStep(TypeAbstraction typeAbstraction, Conclusion conclusion,
Constraint constraint) {
return new VarStepWithLet(typeAbstraction, conclusion, constraint);
@Override
public VarStepWithLet createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs,
Conclusion conclusion, Constraint constraint) {
return new VarStepWithLet(typeAbstraction, instantiatedTypeAbs, conclusion, constraint);
}
}

23
src/main/java/edu/kit/typicalc/model/step/VarStep.java
View File

@ -2,6 +2,7 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
/**
@ -9,24 +10,40 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
* 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;
private final TypeAbstraction typeAbstractionInPremise;
private final Type instantiatedTypeAbs;
/**
* Initializes a new VarStep with the given values.
*
* @param typeAbstractionInPremise the type abstraction in the premise of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @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(TypeAbstraction typeAbstractionInPremise, Conclusion conclusion, Constraint constraint) {
protected VarStep(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion,
Constraint constraint) {
super(conclusion, constraint);
this.typeAbstractionInPremise = typeAbstractionInPremise;
this.instantiatedTypeAbs = instantiatedTypeAbs;
}
/**
* 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;
}
/**
* Returns the instantiation of the type abstraction.
*
* @return the instantiation of the type abstraction.
*/
public Type getInstantiatedTypeAbs() {
return instantiatedTypeAbs;
}
}

10
src/main/java/edu/kit/typicalc/model/step/VarStepDefault.java
View File

@ -2,17 +2,21 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
public class VarStepDefault extends VarStep {
/**
* Initializes a new VarStep with the given values.
*
* @param typeAbstractionInPremise the type abstraction in the premise of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @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
*/
public VarStepDefault(TypeAbstraction typeAbstractionInPremise, Conclusion conclusion, Constraint constraint) {
super(typeAbstractionInPremise, conclusion, constraint);
public VarStepDefault(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion,
Constraint constraint) {
super(typeAbstractionInPremise, instantiatedTypeAbs, conclusion, constraint);
}
/**

10
src/main/java/edu/kit/typicalc/model/step/VarStepWithLet.java
View File

@ -2,17 +2,21 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
public class VarStepWithLet extends VarStep {
/**
* Initializes a new VarStep with the given values.
*
* @param typeAbstractionInPremise the type abstraction in the premise of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @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
*/
public VarStepWithLet(TypeAbstraction typeAbstractionInPremise, Conclusion conclusion, Constraint constraint) {
super(typeAbstractionInPremise, conclusion, constraint);
public VarStepWithLet(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion,
Constraint constraint) {
super(typeAbstractionInPremise, instantiatedTypeAbs, conclusion, constraint);
}
/**

3
src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java
View File

@ -75,5 +75,6 @@ public interface TermVisitorTree {
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.VarStep}
*/
InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType)
throws IllegalStateException;
}

5
src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java
View File

@ -1,5 +1,7 @@
package edu.kit.typicalc.model.type;
import edu.kit.typicalc.model.TypeVariableFactory;
import java.util.List;
public class TypeAbstraction {
@ -9,4 +11,7 @@ public class TypeAbstraction {
public TypeAbstraction(Type type) {
}
public Type instantiate(TypeVariableFactory typeVarFactory) {
return null;
}
}