diff --git a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraintsTest.java b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraintsTest.java index 9ea2401..c3740d9 100644 --- a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraintsTest.java +++ b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraintsTest.java @@ -5,11 +5,13 @@ import edu.kit.typicalc.model.ModelImpl; import edu.kit.typicalc.model.TypeInfererInterface; import org.junit.jupiter.api.Test; +import java.util.ArrayList; import java.util.HashMap; import java.util.List; import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*; import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.fail; class LatexCreatorConstraintsTest { private static final String EMPTY_CONSTRAINT_SET = @@ -98,4 +100,38 @@ class LatexCreatorConstraintsTest { assertEquals(expected.get(i), actual.get(i)); } } + + @Test + void lineBreak() { + typeInferer = model.getTypeInferer("a b c d e f", new HashMap<>()).unwrap(); + List actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything(); + + assertEquals("\\begin{aligned}&\\begin{split}C=\\{&\\alpha_{2}=\\alpha_{3} \\rightarrow \\alpha_{1},\\alpha_{4}=\\alpha_{5} \\rightarrow \\alpha_{2},\\alpha_{6}=\\alpha_{7} \\rightarrow \\alpha_{4},\\alpha_{8}=\\alpha_{9} \\rightarrow \\alpha_{6},\\alpha_{10}=\\alpha_{11} \\rightarrow \\alpha_{8},\\alpha_{10}=\\beta_{1},\\alpha_{11}=\\beta_{2},\\alpha_{9}=\\beta_{3},\\alpha_{7}=\\beta_{4},\\alpha_{5}=\\beta_{5},\\\\&\\alpha_{3}=\\beta_{6}\\}\\end{split}\\end{aligned}", actual.get(11)); + + typeInferer = model.getTypeInferer("let g = a b c d e f in g", new HashMap<>()).unwrap(); + actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything(); + + assertEquals("\\begin{aligned}&\\begin{split}C=\\{&\\alpha_{1}=\\alpha_{13}\\}\\end{split}\\\\\n" + + "&\\begin{split}C_{let}=\\{&\\alpha_{3}=\\alpha_{4} \\rightarrow \\alpha_{2},\\alpha_{5}=\\alpha_{6} \\rightarrow \\alpha_{3},\\alpha_{7}=\\alpha_{8} \\rightarrow \\alpha_{5},\\alpha_{9}=\\alpha_{10} \\rightarrow \\alpha_{7},\\alpha_{11}=\\alpha_{12} \\rightarrow \\alpha_{9},\\alpha_{11}=\\beta_{1},\\alpha_{12}=\\beta_{2},\\alpha_{10}=\\beta_{3},\\alpha_{8}=\\beta_{4},\\alpha_{6}=\\beta_{5},\\\\&\\alpha_{4}=\\beta_{6}\\}\\end{split}\\end{aligned}", actual.get(12)); + } + + @Test + void emptyLetTypeAssumptions() { + typeInferer = model.getTypeInferer("let g = 5 in g", new HashMap<>()).unwrap(); + List actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything(); + assertEquals("\\begin{aligned}&\\begin{split}C=\\{&\\alpha_{1}=\\alpha_{3}\\}\\end{split}\\\\\n" + + "&\\begin{split}C_{let}=\\{&\\alpha_{2}=\\texttt{int}\\}\\end{split}\\\\&\\begin{split}\\sigma_{let}:=\\textit{mgu}(C_{let})=[&\\alpha_{2}\\mathrel{\\unicode{x21E8}}\\texttt{int}]\\end{split}\\\\&\\sigma_{let}(\\alpha_{2})=\\texttt{int}\\\\&\\Gamma'=\\sigma_{let}(\\emptyset),\\ \\texttt{g}:ta(\\sigma_{let}(\\alpha_{2}),\\sigma_{let}(\\emptyset))=\\texttt{g}:\\texttt{int}\\end{aligned}", actual.get(6)); + } + + @Test + void excessiveMemoryUsageAvoided() { + try { + typeInferer = model.getTypeInferer("(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)(λx.x)", new HashMap<>()).unwrap(); + List actual = new LatexCreatorConstraints(typeInferer, Enum::toString).getEverything(); + // should have thrown IllegalStateException by now + fail("did not throw exception"); + } catch (IllegalStateException e) { + assertEquals("type too large!", e.getMessage()); + } + } } diff --git a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTest.java b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTest.java new file mode 100644 index 0000000..9497cde --- /dev/null +++ b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTest.java @@ -0,0 +1,51 @@ +package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator; + +import edu.kit.typicalc.model.Model; +import edu.kit.typicalc.model.ModelImpl; +import edu.kit.typicalc.model.TypeInfererInterface; +import org.junit.jupiter.api.Test; + +import java.util.HashMap; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +class LatexCreatorTest { + private final Model model = new ModelImpl(); + + @Test + void testFailedLet() { + TypeInfererInterface typeInferer = model.getTypeInferer("let fun = 5 5 in fun 42", new HashMap<>()).unwrap(); + String latex = new LatexCreator(typeInferer, Enum::toString).getTree(); + assertEquals("\\begin{prooftree}\n" + + "\\AxiomC{$\\texttt{5} \\in Const$}\n" + + "\\LeftLabel{\\textrm C{\\small ONST}}\n" + + "\\UnaryInfC{$\\vdash\\texttt{5}:\\alpha_{3}$}\n" + + "\\AxiomC{$\\texttt{5} \\in Const$}\n" + + "\\LeftLabel{\\textrm C{\\small ONST}}\n" + + "\\UnaryInfC{$\\vdash\\texttt{5}:\\alpha_{4}$}\n" + + "\\LeftLabel{\\textrm A{\\small PP}}\n" + + "\\BinaryInfC{$\\vdash\\texttt{5}\\ \\texttt{5}:\\alpha_{2}$}\n" + + "\\AxiomC{}\n" + + "\\LeftLabel{\\textrm L{\\small ET}}\n" + + "\\BinaryInfC{$\\vdash\\texttt{\\textbf{let}}\\ \\texttt{fun}=\\texttt{5}\\ \\texttt{5}\\ \\texttt{\\textbf{in}}\\ \\texttt{fun}\\ \\texttt{42}:\\alpha_{1}$}\n" + + "\\end{prooftree}", latex); + typeInferer = model.getTypeInferer("(let fun = 5 5 in fun) 42", new HashMap<>()).unwrap(); + latex = new LatexCreator(typeInferer, Enum::toString).getTree(); + assertEquals("\\begin{prooftree}\n" + + "\\AxiomC{$\\texttt{5} \\in Const$}\n" + + "\\LeftLabel{\\textrm C{\\small ONST}}\n" + + "\\UnaryInfC{$\\vdash\\texttt{5}:\\alpha_{5}$}\n" + + "\\AxiomC{$\\texttt{5} \\in Const$}\n" + + "\\LeftLabel{\\textrm C{\\small ONST}}\n" + + "\\UnaryInfC{$\\vdash\\texttt{5}:\\alpha_{6}$}\n" + + "\\LeftLabel{\\textrm A{\\small PP}}\n" + + "\\BinaryInfC{$\\vdash\\texttt{5}\\ \\texttt{5}:\\alpha_{4}$}\n" + + "\\AxiomC{}\n" + + "\\LeftLabel{\\textrm L{\\small ET}}\n" + + "\\BinaryInfC{$\\vdash\\texttt{\\textbf{let}}\\ \\texttt{fun}=\\texttt{5}\\ \\texttt{5}\\ \\texttt{\\textbf{in}}\\ \\texttt{fun}:\\alpha_{2}$}\n" + + "\\AxiomC{$\\vdash\\texttt{42}:\\alpha_{3}$}\n" + + "\\LeftLabel{\\textrm A{\\small PP}}\n" + + "\\BinaryInfC{$\\vdash(\\texttt{\\textbf{let}}\\ \\texttt{fun}=\\texttt{5}\\ \\texttt{5}\\ \\texttt{\\textbf{in}}\\ \\texttt{fun})\\ \\texttt{42}:\\alpha_{1}$}\n" + + "\\end{prooftree}", latex); + } +}