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

TypeAssumption entfernen, Konstruktoren und getter von Tree

Browse Source
This commit is contained in:
Johanna Stuber 2021-01-28 00:37:48 +01:00
parent ad0d059f24
commit 8a7497fada
6 changed files with 47 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1,6 +1,9 @@
package edu.kit.typicalc.model;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.step.StepFactory;
import edu.kit.typicalc.model.step.StepFactoryDefault;
import edu.kit.typicalc.model.step.StepFactoryWithLet;
import edu.kit.typicalc.model.term.AbsTerm;
import edu.kit.typicalc.model.term.AppTerm;
import edu.kit.typicalc.model.term.ConstTerm;
@ -10,9 +13,9 @@ import edu.kit.typicalc.model.term.TermVisitorTree;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import edu.kit.typicalc.model.type.TypeAssumption;
import edu.kit.typicalc.model.type.TypeVariable;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;
@ -24,6 +27,13 @@ import java.util.Map;
*/
public class Tree implements TermVisitorTree {
private final TypeVariableFactory typeVarFactory;
private final StepFactory stepFactory;
private final TypeVariable firstTypeVariable;
private final InferenceStep firstInferenceStep;
private final List<Constraint> constraints;
/**
* 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
@ -33,7 +43,7 @@ public class Tree implements TermVisitorTree {
* @param lambdaTerm the lambda term to generate the tree for
*/
protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm) {
// TODO
this(typeAssumptions, lambdaTerm, new TypeVariableFactory());
}
/**
@ -49,7 +59,14 @@ public class Tree implements TermVisitorTree {
*/
protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm,
TypeVariableFactory typeVariableFactory) {
// TODO
// TODO: null checks
this.typeVarFactory = typeVariableFactory;
this.constraints = new ArrayList<>();
this.stepFactory = lambdaTerm.hasLet() ? new StepFactoryWithLet() : new StepFactoryDefault();
this.firstTypeVariable = typeVarFactory.nextTypeVariable();
this.firstInferenceStep = lambdaTerm.accept(this, typeAssumptions, firstTypeVariable);
}
/**
@ -60,8 +77,7 @@ public class Tree implements TermVisitorTree {
* @return the first inference step of the tree
*/
protected InferenceStep getFirstInferenceStep() {
return null;
// TODO;
return firstInferenceStep;
}
/**
@ -70,8 +86,7 @@ public class Tree implements TermVisitorTree {
* @return the first type variable
*/
protected TypeVariable getFirstTypeVariable() {
return null;
// TODO;
return firstTypeVariable;
}
/**
@ -81,32 +96,31 @@ public class Tree implements TermVisitorTree {
* @return the constraint list of the tree
*/
protected List<Constraint> getConstraints() {
return null;
// TODO
return constraints;
}
@Override
public InferenceStep visit(AppTerm appTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
public InferenceStep visit(AppTerm appTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
}
@Override
public InferenceStep visit(AbsTerm absTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
public InferenceStep visit(AbsTerm absTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
}
@Override
public InferenceStep visit(LetTerm letTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
public InferenceStep visit(LetTerm letTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
}
@Override
public InferenceStep visit(ConstTerm constTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
public InferenceStep visit(ConstTerm constTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
}
@Override
public InferenceStep visit(VarTerm varTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
public InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
}
}

1
src/main/java/edu/kit/typicalc/model/TypeInferer.java
View File

@ -32,6 +32,7 @@ public class TypeInferer implements TypeInfererInterface {
* @param typeAssumptions the type assumptions to consider when generating the tree
*/
protected TypeInferer(LambdaTerm lambdaTerm, Map<VarTerm, TypeAbstraction> typeAssumptions) {
// TODO: null checks
tree = new Tree(typeAssumptions, lambdaTerm);
// TODO: Abbrechen bei fehlgeschlagener let-Teilinferenz, evtl. getUnificationSteps() anpassen

10
src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java
View File

@ -1,5 +1,11 @@
package edu.kit.typicalc.model.term;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.Map;
public abstract class LambdaTerm {
/**
* @return whether the lambda term contains a let expression
@ -11,4 +17,8 @@ public abstract class LambdaTerm {
* @param termVisitor a visitor
*/
public abstract void accept(TermVisitor termVisitor);
public abstract InferenceStep accept(TermVisitorTree termVisitorTree,
Map<VarTerm, TypeAbstraction> assumptions, Type type);
}

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

@ -2,9 +2,9 @@ package edu.kit.typicalc.model.term;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAssumption;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.List;
import java.util.Map;
public interface TermVisitorTree {
/**
@ -19,7 +19,7 @@ public interface TermVisitorTree {
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.AppStep}
*/
InferenceStep visit(AppTerm appTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
InferenceStep visit(AppTerm appTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
/**
* Returns an {@link edu.kit.typicalc.model.step.AbsStep} suiting the given abstraction (lambda term)
@ -33,7 +33,7 @@ public interface TermVisitorTree {
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.AbsStep}
*/
InferenceStep visit(AbsTerm absTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
InferenceStep visit(AbsTerm absTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
/**
* Returns an {@link edu.kit.typicalc.model.step.LetStep} suiting the given let expression (lambda term)
@ -47,7 +47,7 @@ public interface TermVisitorTree {
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.LetStep}
*/
InferenceStep visit(LetTerm letTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
InferenceStep visit(LetTerm letTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
/**
* Returns an {@link edu.kit.typicalc.model.step.ConstStep} suiting the given constant
@ -61,7 +61,7 @@ public interface TermVisitorTree {
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.ConstStep}
*/
InferenceStep visit(ConstTerm constTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
InferenceStep visit(ConstTerm constTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
/**
* Returns an {@link edu.kit.typicalc.model.step.VarStep} suiting the given variable (lambda term)
@ -75,5 +75,5 @@ public interface TermVisitorTree {
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.VarStep}
*/
InferenceStep visit(VarTerm varTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
}

4
src/main/java/edu/kit/typicalc/model/type/TypeAssumption.java
View File

@ -1,4 +0,0 @@
package edu.kit.typicalc.model.type;
public class TypeAssumption {
}

2
src/main/java/edu/kit/typicalc/model/type/TypeVariable.java
View File

@ -1,6 +1,6 @@
package edu.kit.typicalc.model.type;
public class TypeVariable {
public class TypeVariable extends Type {
public TypeVariable(int index) {
}