From c2ae5ca10e105e62a0a90eee49697c5df20f4cee Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@student.kit.edu>
Date: Tue, 31 Aug 2021 11:34:25 +0200
Subject: [PATCH] Add new fuzzing target for latex creator

FWIW this didn't find anything, we might need type assumptions..
---
 .../model/parser/LambdaParserFuzzTest.java    | 26 +++++++++++++++++--
 1 file changed, 24 insertions(+), 2 deletions(-)

diff --git a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserFuzzTest.java b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserFuzzTest.java
index 5f26e9b..9b9287c 100644
--- a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserFuzzTest.java
+++ b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserFuzzTest.java
@@ -8,15 +8,17 @@ import edu.kit.typicalc.model.TypeInfererInterface;
 import edu.kit.typicalc.model.step.InferenceStep;
 import edu.kit.typicalc.model.term.LambdaTerm;
 import edu.kit.typicalc.util.Result;
+import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreator;
+import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorMode;
 import org.junit.Ignore;
 import org.junit.runner.RunWith;
 
-import java.io.IOException;
 import java.io.InputStream;
-import java.util.HashMap;
 
 import com.pholser.junit.quickcheck.*;
 
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
 @RunWith(JQF.class)
 public class LambdaParserFuzzTest {
     /**
@@ -32,6 +34,26 @@ public class LambdaParserFuzzTest {
         InferenceStep first = typer.unwrap().getFirstInferenceStep();
     }
 
+    /**
+     * Runs the type inference algorithm and exports the proof tree as latex.
+     * Validates that it ends with `\end{prooftree}`.
+     *
+     * @param term lambda term
+     */
+    @Fuzz
+    public void testInferenceLatex(@From(LambdaTermGenerator.class) String term) {
+        Model model = new ModelImpl();
+        Result<TypeInfererInterface, ParseError> typer = model.getTypeInferer(term, "");
+        if (typer.isError()) {
+            return; // don't care
+        }
+        var lc = new LatexCreator(typer.unwrap(),
+                error -> "root." + error.toString(),
+                LatexCreatorMode.NORMAL);
+        var latexCode = lc.getTree();
+        assertTrue(latexCode.endsWith("\\end{prooftree}"));
+    }
+
     // this is how to rerun a specific fuzz result
     /*
     @Fuzz(repro="target/fuzz-results/edu.kit.typicalc.model.parser.LambdaParserFuzzTest/testInference/corpus/id_000066")