mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
erste Implementierung für TypeInferer
This commit is contained in:
parent
aadddee628
commit
c823f710cc
@ -11,6 +11,7 @@ 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.List;
|
||||
import java.util.Map;
|
||||
@ -63,6 +64,16 @@ public class Tree implements TermVisitorTree {
|
||||
// TODO;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the first type variable the original lambda term was assigned in the first inference step.
|
||||
*
|
||||
* @return the first type variable
|
||||
*/
|
||||
protected TypeVariable getFirstTypeVariable() {
|
||||
return null;
|
||||
// TODO;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the list of constraints that formed while generating the inference step tree
|
||||
* structure, needed for the subsequent unification.
|
||||
|
@ -19,6 +19,10 @@ import java.util.Map;
|
||||
*/
|
||||
public class TypeInferer implements TypeInfererInterface {
|
||||
|
||||
private final Tree tree;
|
||||
private final Unification unification;
|
||||
private final TypeInferenceResult typeInfResult;
|
||||
|
||||
/**
|
||||
* Initializes a new TypeInferer for the given type assumptions and lambda term.
|
||||
* The inference step structure, unification steps, the most general unifier and the
|
||||
@ -28,31 +32,41 @@ 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
|
||||
tree = new Tree(typeAssumptions, lambdaTerm);
|
||||
// TODO: Abbrechen bei fehlgeschlagener let-Teilinferenz, evtl. getUnificationSteps() anpassen
|
||||
|
||||
unification = new Unification(tree.getConstraints());
|
||||
|
||||
// cancel algorithm if term can't be typified
|
||||
if (!unification.getSubstitutions().isOk()) {
|
||||
typeInfResult = null;
|
||||
// TODO: schönere Methode, mit nicht typisierbar umzugehen?
|
||||
// getter unten anpassen!
|
||||
return;
|
||||
}
|
||||
|
||||
List<Substitution> substitutions = unification.getSubstitutions().getValue();
|
||||
typeInfResult = new TypeInferenceResult(substitutions, tree.getFirstTypeVariable());
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
public InferenceStep getFirstInferenceStep() {
|
||||
return null;
|
||||
// TODO
|
||||
return tree.getFirstInferenceStep();
|
||||
}
|
||||
|
||||
@Override
|
||||
public List<UnificationStep> getUnificationSteps() {
|
||||
return null;
|
||||
// TODO
|
||||
return unification.getUnificationSteps();
|
||||
}
|
||||
|
||||
@Override
|
||||
public List<Substitution> getMGU() {
|
||||
return null;
|
||||
// TODO
|
||||
return typeInfResult.getMGU();
|
||||
}
|
||||
|
||||
@Override
|
||||
public Type getType() {
|
||||
return null;
|
||||
// TODO
|
||||
return typeInfResult.getType();
|
||||
}
|
||||
}
|
||||
|
20
src/main/java/edu/kit/typicalc/model/Unification.java
Normal file
20
src/main/java/edu/kit/typicalc/model/Unification.java
Normal file
@ -0,0 +1,20 @@
|
||||
package edu.kit.typicalc.model;
|
||||
|
||||
import edu.kit.typicalc.util.Result;
|
||||
|
||||
import java.util.List;
|
||||
|
||||
public class Unification {
|
||||
protected Unification(List<Constraint> constraints) {
|
||||
|
||||
}
|
||||
|
||||
protected List<UnificationStep> getUnificationSteps() {
|
||||
return null;
|
||||
}
|
||||
|
||||
protected Result<List<Substitution>, UnificationError> getSubstitutions() {
|
||||
return null;
|
||||
}
|
||||
|
||||
}
|
@ -0,0 +1,4 @@
|
||||
package edu.kit.typicalc.model;
|
||||
|
||||
public enum UnificationError {
|
||||
}
|
Loading…
Reference in New Issue
Block a user