This commit is contained in:
ucrhh 2021-02-03 11:09:28 +01:00
commit 874b648caf
4 changed files with 80 additions and 9 deletions

View File

@ -1,9 +1,6 @@
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.step.*;
import edu.kit.typicalc.model.term.AbsTerm;
import edu.kit.typicalc.model.term.AppTerm;
import edu.kit.typicalc.model.term.ConstTerm;
@ -133,7 +130,43 @@ public class Tree implements TermVisitorTree {
@Override
public InferenceStep visit(LetTerm letTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
TypeInfererLet typeInfererLet = new TypeInfererLet(
letTerm.getVariableDefinition(), typeAssumptions, typeVarFactory);
Type premiseType = typeVarFactory.nextTypeVariable();
Constraint newConstraint = new Constraint(conclusionType, premiseType);
InferenceStep premise;
if (typeInfererLet.getType().isPresent()) {
Map<VarTerm, TypeAbstraction> extendedTypeAssumptions = new HashMap<>(typeAssumptions);
extendedTypeAssumptions.replaceAll((key, value) -> {
Type newType = value.getInnerType();
for (Substitution substitution : typeInfererLet.getMGU().get()) {
if (value.getQuantifiedVariables().contains(substitution.getVariable())) {
continue;
}
newType = newType.substitute(substitution);
}
return new TypeAbstraction(newType, value.getQuantifiedVariables());
});
List<TypeVariable> variablesToQuantify = new ArrayList<>();
// TODO variablesToQuantify berechnen
TypeAbstraction newTypeAbstraction = new TypeAbstraction(typeInfererLet.getType().get(),
variablesToQuantify);
extendedTypeAssumptions.put(letTerm.getVariable(), newTypeAbstraction);
premise = letTerm.getInner().accept(this, extendedTypeAssumptions, premiseType);
constraints.add(newConstraint);
constraints.addAll(typeInfererLet.getLetConstraints());
} else {
premise = new EmptyStep();
}
Conclusion conclusion = new Conclusion(typeAssumptions, letTerm, conclusionType);
return stepFactory.createLetStep(conclusion, newConstraint, premise, typeInfererLet);
}
@Override

View File

@ -0,0 +1,32 @@
package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint;
/**
* Empty Steps are used if the sub-inference started when creating a let step failed and the second premise of
* this let step therefore cannot be calculated.
*/
public class EmptyStep extends InferenceStep {
/**
* Initializes a new EmptyStep.
*/
public EmptyStep() {
super(null, null); // TODO
}
@Override
public Conclusion getConclusion() {
throw new IllegalStateException("getConclusion() should never be called on an empty step");
}
@Override
public Constraint getConstraint() {
throw new IllegalStateException("getConstraint() should never be called on an empty step");
}
@Override
public void accept(StepVisitor stepVisitor) {
stepVisitor.visit(this);
}
}

View File

@ -47,8 +47,9 @@ public interface StepVisitor {
*/
void visit(LetStepDefault letD);
/**
* Visits an empty step
* @param empty the empty step to visit
*/
void visit(EmptyStep empty);
}

View File

@ -179,6 +179,11 @@ public class LatexCreator implements StepVisitor, TypeVisitor {
// todo implement
}
@Override
public void visit(EmptyStep empty) {
// TODO
}
@Override
public void visit(NamedType named) {
visitorBuffer = TEXTTT + CURLY_LEFT + named.getName() + CURLY_RIGHT;