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

implement let in TypeInferers

Browse Source
This commit is contained in:
Johanna Stuber 2021-02-04 11:41:08 +01:00
parent fd00b47928
commit 8dc7fbe725
5 changed files with 50 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -30,6 +30,8 @@ public class Tree implements TermVisitorTree {
private final InferenceStep firstInferenceStep;
private final List<Constraint> constraints;
private boolean failedSubInference;
/**
* 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
@ -62,6 +64,8 @@ public class Tree implements TermVisitorTree {
this.firstTypeVariable = typeVarFactory.nextTypeVariable();
this.firstInferenceStep = lambdaTerm.accept(this, typeAssumptions, firstTypeVariable);
this.failedSubInference = false;
}
/**
@ -94,6 +98,15 @@ public class Tree implements TermVisitorTree {
return constraints;
}
/**
* Indicates whether the tree contains a sub-inference of a let step that failed
*
* @return true, if the tree contains a failed sub-inference, false otherwise
*/
protected boolean hasFailedSubInference() {
return failedSubInference;
}
@Override
public InferenceStep visit(AppTerm appTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
Type leftType = typeVarFactory.nextTypeVariable();
@ -160,6 +173,7 @@ public class Tree implements TermVisitorTree {
constraints.addAll(typeInfererLet.getLetConstraints());
} else {
premise = new EmptyStep();
failedSubInference = true;
}
Conclusion conclusion = new Conclusion(typeAssumptions, letTerm, conclusionType);

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

@ -25,7 +25,7 @@ import java.util.Set;
public class TypeInferer implements TypeInfererInterface {
private final Tree tree;
private final Unification unification;
private final Optional<Unification> unification;
private final Optional<TypeInferenceResult> typeInfResult;
/**
@ -41,17 +41,22 @@ public class TypeInferer implements TypeInfererInterface {
completeTypeAss.putAll(typeAssumptions);
tree = new Tree(completeTypeAss, lambdaTerm);
// TODO: Abbrechen bei fehlgeschlagener let-Teilinferenz, evtl. getUnificationSteps() anpassen
unification = new Unification(new ArrayDeque<>(tree.getConstraints()));
// cancel algorithm if term can't be typified
if (unification.getSubstitutions().isError()) {
// cancel algorithm if a sub-inference failed
if (tree.hasFailedSubInference()) {
unification = Optional.empty();
typeInfResult = Optional.empty();
return;
}
List<Substitution> substitutions = unification.getSubstitutions().unwrap();
unification = Optional.of(new Unification(new ArrayDeque<>(tree.getConstraints())));
// cancel algorithm if term can't be typified
if (unification.get().getSubstitutions().isError()) {
typeInfResult = Optional.empty();
return;
}
List<Substitution> substitutions = unification.get().getSubstitutions().unwrap();
typeInfResult = Optional.of(new TypeInferenceResult(substitutions, tree.getFirstTypeVariable()));
}
@ -74,8 +79,8 @@ public class TypeInferer implements TypeInfererInterface {
}
@Override
public List<UnificationStep> getUnificationSteps() {
return unification.getUnificationSteps();
public Optional<List<UnificationStep>> getUnificationSteps() {
return unification.map(Unification::getUnificationSteps);
}
@Override

6
src/main/java/edu/kit/typicalc/model/TypeInfererInterface.java
View File

@ -24,7 +24,7 @@ public interface TypeInfererInterface {
*
* @return the list of unification steps
*/
List<UnificationStep> getUnificationSteps();
Optional<List<UnificationStep>> getUnificationSteps();
/**
* Returns the most general unifier (mgu) for the lambda term that is type-inferred,
@ -33,7 +33,7 @@ public interface TypeInfererInterface {
*
* @return the most general unifier, empty if there is no valid mgu
*/
Optional<List<Substitution>> getMGU(); // TODO: change of API -> document!
Optional<List<Substitution>> getMGU();
/**
* Returns the type that is the result of the type inference.
@ -41,5 +41,5 @@ public interface TypeInfererInterface {
*
* @return the final type of the lambda term, empty if there is no valid type
*/
Optional<Type> getType(); // TODO: change of API -> document!
Optional<Type> getType();
}

25
src/main/java/edu/kit/typicalc/model/TypeInfererLet.java
View File

@ -19,7 +19,7 @@ import java.util.Optional;
public class TypeInfererLet implements TypeInfererInterface {
private final Tree tree;
private final Unification unification;
private final Optional<Unification> unification;
private final Optional<TypeInferenceResult> typeInfResult;
/**
@ -34,17 +34,22 @@ public class TypeInfererLet implements TypeInfererInterface {
TypeVariableFactory typeVarFactory) {
tree = new Tree(typeAssumptions, lambdaTerm, typeVarFactory);
// TODO: Abbrechen bei fehlgeschlagener let-Teilinferenz, evtl. getUnificationSteps() anpassen
unification = new Unification(new ArrayDeque<>(tree.getConstraints()));
// cancel algorithm if term can't be typified
if (unification.getSubstitutions().isError()) {
// cancel algorithm if a sub-inference failed
if (tree.hasFailedSubInference()) {
unification = Optional.empty();
typeInfResult = Optional.empty();
return;
}
List<Substitution> substitutions = unification.getSubstitutions().unwrap();
unification = Optional.of(new Unification(new ArrayDeque<>(tree.getConstraints())));
// cancel algorithm if term can't be typified
if (unification.get().getSubstitutions().isError()) {
typeInfResult = Optional.empty();
return;
}
List<Substitution> substitutions = unification.get().getSubstitutions().unwrap();
typeInfResult = Optional.of(new TypeInferenceResult(substitutions, tree.getFirstTypeVariable()));
}
@ -74,8 +79,8 @@ public class TypeInfererLet implements TypeInfererInterface {
}
@Override
public List<UnificationStep> getUnificationSteps() {
return unification.getUnificationSteps();
public Optional<List<UnificationStep>> getUnificationSteps() {
return unification.map(Unification::getUnificationSteps);
}
@Override

5
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java
View File

@ -54,11 +54,12 @@ public class LatexCreator implements StepVisitor {
}
/**
* @return the LaTeX-code for constraints nad unification
* @return the LaTeX-code for constraints and unification
*/
protected String[] getUnification() {
List<String> steps = new ArrayList<>();
for (UnificationStep step : typeInferer.getUnificationSteps()) {
// TODO: check if unification is present
for (UnificationStep step : typeInferer.getUnificationSteps().orElseThrow(IllegalStateException::new)) {
Result<List<Substitution>, UnificationError> subs = step.getSubstitutions();
if (subs.isError()) {
continue; // TODO