partly fix issues with failing sub inference

This commit is contained in:
ucrhh 2021-02-09 22:51:54 +01:00
parent 34a727e0c0
commit cadc299791
3 changed files with 21 additions and 14 deletions

View File

@ -63,10 +63,10 @@ public class Tree implements TermVisitorTree {
this.stepFactory = lambdaTerm.hasLet() || partOfLetTerm ? new StepFactoryWithLet() : new StepFactoryDefault();
this.failedSubInference = false;
this.firstTypeVariable = typeVarFactory.nextTypeVariable();
this.firstInferenceStep = lambdaTerm.accept(this, typeAssumptions, firstTypeVariable);
this.failedSubInference = false;
}
/**

View File

@ -48,17 +48,19 @@ public class LatexCreatorConstraints implements StepVisitor {
protected List<String> getEverything() {
List<String> result = new ArrayList<>(constraints);
generateUnification().forEach(step -> {
result.add(step);
numberGenerator.push();
});
typeInferer.getMGU().ifPresent(mgu -> {
result.add(generateMGU());
numberGenerator.push();
result.add(generateMGU() + LATEX_NEW_LINE + new LatexCreatorType(typeInferer.getType().get()).getLatex());
numberGenerator.push();
});
// todo add some helpful text for the user
if (typeInferer.getUnificationSteps().isPresent()) {
generateUnification().forEach(step -> {
result.add(step);
numberGenerator.push();
});
typeInferer.getMGU().ifPresent(mgu -> {
result.add(generateMGU());
numberGenerator.push();
result.add(generateMGU() + LATEX_NEW_LINE + new LatexCreatorType(typeInferer.getType().get()).getLatex());
numberGenerator.push();
});
// todo add some helpful text for the user
}
if (FIRST_PREFIX.equals(prefix)) {
result.replaceAll(content -> ALIGN_BEGIN + content + ALIGN_END);
}
@ -126,6 +128,10 @@ public class LatexCreatorConstraints implements StepVisitor {
constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE);
constraints.addAll(subCreator.getEverything());
// cancels constraint creation if sub inference failed
if (letD.getTypeInferer().getMGU().isEmpty()) {
return;
}
// adds one step in which all let constraints are added to 'outer' constraint set
String letConstraints = createLetConstraints(letD.getTypeInferer().getLetConstraints());
prevStep = prevStep.equals("") ? letConstraints : prevStep + COMMA + letConstraints;

View File

@ -23,7 +23,8 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver {
private static final List<String> EXAMPLES =
List.of("λx.x", "λx.λy.y x", "λx.λy.y (x x)", "let f = λx. g y y in f 3", "(λx.x x) (λx.x x)",
"(λx.λy.y (x y)) (λz. λa. z g a)", "let f = λx. let g = λy. y in g x in f 3");
"(λx.λy.y (x y)) (λz. λa. z g a)", "let f = λx. let g = λy. y in g x in f 3",
"let f = λx. let g = λy.5 5 in g x in f 3");
private final Paragraph instruction;
/**