diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index f70bec8..f303391 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/src/main/java/edu/kit/typicalc/model/Tree.java @@ -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; } /** diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstraints.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstraints.java index f5d5095..e589fc8 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstraints.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorConstraints.java @@ -48,17 +48,19 @@ public class LatexCreatorConstraints implements StepVisitor { protected List getEverything() { List 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; diff --git a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java index 779d9be..3c9f796 100644 --- a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java +++ b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java @@ -23,7 +23,8 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver { private static final List 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; /**