arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 10:20:41 +00:00
Code Issues Packages Projects Releases Wiki Activity

Fix tooltips in case of failed let inference

Browse Source
This commit is contained in:
Arne Keller 2021-08-10 11:44:59 +02:00
parent 60ee1583fd
commit 90833c37b5
2 changed files with 21 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java
View File

@ -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())),

15
src/test/java/edu/kit/typicalc/model/step/StepAnnotatorTest.java Normal file
View File

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