From 90833c37b5fac16a4bef0a5b598ccfdf8b817ac6 Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@student.kit.edu>
Date: Tue, 10 Aug 2021 11:44:59 +0200
Subject: [PATCH] Fix tooltips in case of failed let inference

---
 .../kit/typicalc/model/step/StepAnnotator.java    |  6 ++++++
 .../typicalc/model/step/StepAnnotatorTest.java    | 15 +++++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 src/test/java/edu/kit/typicalc/model/step/StepAnnotatorTest.java

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());
+    }
+}