diff --git a/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java b/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java index 6ee6c7f..8c263ce 100644 --- a/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java +++ b/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java @@ -98,6 +98,12 @@ public class StepAnnotator implements StepVisitor { @Override public void visit(LetStepDefault letD) { + // account for failed sub-inference + if (letD.getPremise() instanceof EmptyStep) { // TODO: there must be a better way to solve this! + annotations.add(""); + letD.getTypeInferer().getFirstInferenceStep().accept(this); + return; + } visitGeneric2(List.of( Pair.of("_1", letD.getTypeInferer().getFirstInferenceStep().getConclusion().getType()), Pair.of("_2", letD.getPremise().getConclusion().getType())), diff --git a/src/test/java/edu/kit/typicalc/model/step/StepAnnotatorTest.java b/src/test/java/edu/kit/typicalc/model/step/StepAnnotatorTest.java new file mode 100644 index 0000000..f37e179 --- /dev/null +++ b/src/test/java/edu/kit/typicalc/model/step/StepAnnotatorTest.java @@ -0,0 +1,15 @@ +package edu.kit.typicalc.model.step; + +import edu.kit.typicalc.model.Model; +import edu.kit.typicalc.model.ModelImpl; +import edu.kit.typicalc.model.TypeInfererInterface; +import org.junit.jupiter.api.Test; + +public class StepAnnotatorTest { + @Test + void canAnnotateFailedLetTerm() { + Model model = new ModelImpl(); + TypeInfererInterface typer = model.getTypeInferer("let f = (λx.y x) (y 5) in λg.f 3", "y: int->(int->boolean)").unwrap(); + typer.getFirstInferenceStep().accept(new StepAnnotator()); + } +}