mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Add unit tests for new changes
- failed let in sub-tree (both cases) - empty type assumptions of let - constraint line breaking - DoS protection
This commit is contained in:
parent
f95ff0721a
commit
dc60c58011
@ -5,11 +5,13 @@ import edu.kit.typicalc.model.ModelImpl;
|
|||||||
import edu.kit.typicalc.model.TypeInfererInterface;
|
import edu.kit.typicalc.model.TypeInfererInterface;
|
||||||
import org.junit.jupiter.api.Test;
|
import org.junit.jupiter.api.Test;
|
||||||
|
|
||||||
|
import java.util.ArrayList;
|
||||||
import java.util.HashMap;
|
import java.util.HashMap;
|
||||||
import java.util.List;
|
import java.util.List;
|
||||||
|
|
||||||
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*;
|
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.assertEquals;
|
||||||
|
import static org.junit.jupiter.api.Assertions.fail;
|
||||||
|
|
||||||
class LatexCreatorConstraintsTest {
|
class LatexCreatorConstraintsTest {
|
||||||
private static final String EMPTY_CONSTRAINT_SET =
|
private static final String EMPTY_CONSTRAINT_SET =
|
||||||
@ -98,4 +100,38 @@ class LatexCreatorConstraintsTest {
|
|||||||
assertEquals(expected.get(i), actual.get(i));
|
assertEquals(expected.get(i), actual.get(i));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@Test
|
||||||
|
void lineBreak() {
|
||||||
|
typeInferer = model.getTypeInferer("a b c d e f", new HashMap<>()).unwrap();
|
||||||
|
List<String> 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<String> 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<String> 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());
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -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);
|
||||||
|
}
|
||||||
|
}
|
Loading…
Reference in New Issue
Block a user