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

Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

Browse Source
This commit is contained in:
Johanna Stuber 2021-01-30 14:21:35 +01:00
commit badc2d832c
4 changed files with 55 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
.gitlab-ci.yml
View File

@ -1,8 +1,6 @@
build:
script:
- mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp checkstyle:check
- mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp test
- mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp jacoco:prepare-agent test jacoco:report
- mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp checkstyle:check jacoco:prepare-agent test jacoco:report
- python3 /opt/cover2cover.py target/site/jacoco/jacoco.xml src/main/java > target/site/cobertura.xml
- python3 /opt/source2filename.py target/site/cobertura.xml
- /opt/calcCoverage.sh < target/site/cobertura.xml

7
pom.xml
View File

@ -209,13 +209,6 @@
<groupId>org.jacoco</groupId>
<artifactId>jacoco-maven-plugin</artifactId>
<version>0.8.6</version>
<executions>
<execution>
<goals>
<goal>prepare-agent</goal>
</goals>
</execution>
</executions>
</plugin>
<plugin>

65
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java
View File

@ -1,17 +1,12 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
import edu.kit.typicalc.model.type.NamedType;
import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.model.step.*;
import edu.kit.typicalc.model.term.AbsTerm;
import edu.kit.typicalc.model.term.AppTerm;
import edu.kit.typicalc.model.term.ConstTerm;
import edu.kit.typicalc.model.term.LetTerm;
import edu.kit.typicalc.model.term.TermVisitor;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.term.*;
import edu.kit.typicalc.model.type.FunctionType;
import edu.kit.typicalc.model.type.NamedType;
import edu.kit.typicalc.model.type.TypeVariable;
import edu.kit.typicalc.model.type.TypeVisitor;
@ -24,7 +19,13 @@ import edu.kit.typicalc.model.type.TypeVisitor;
*/
public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
private static final String SPACE = " ";
private static final String EQUAL_SIGN = "=";
private static final String CURLY_LEFT = "{";
private static final String CURLY_RIGHT = "}";
private static final String UNDERSCORE = "_";
private static final String PAREN_LEFT = "(";
private static final String PAREN_RIGHT = ")";
private static final String LABEL_ABS = "\\LeftLabel{ABS}";
private static final String LABEL_APP = "\\LeftLabel{APP}";
@ -36,6 +37,12 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
private static final String BIC = "\\BinaryInfC";
private static final String AXC = "\\AxiomC";
private static final String TREE_VARIABLE = "\\alpha";
private static final String GENERATED_ASSUMPTION_VARIABLE = "\\beta";
private static final String USER_VARIABLE = "\\tau";
private static final String TEXTTT = "\\texttt";
private static final String RIGHT_ARROW = "\\rightarrow";
private static final String TREE_BEGIN = "\\begin{prooftree}";
private static final String TREE_END = "\\end{prooftree}";
@ -48,7 +55,8 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
/**
* Needed for typeVisitor methods
*/
private String typeBuffer;
private String visitorBuffer = "";
private boolean needsParentheses;
/**
* Generate the pieces of LaTeX-code from the type inferer.
@ -104,18 +112,12 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
return conclusion;
}
private StringBuilder generateConstraint(InferenceStep step) {
// todo implement maybe rename to addConstraint
StringBuilder constraint = new StringBuilder();
private String generateConstraint(InferenceStep step) {
step.getConstraint().getFirstType().accept(this);
String firstType = typeBuffer;
String firstType = visitorBuffer;
step.getConstraint().getSecondType().accept(this);
String secondType = typeBuffer;
constraint.append(firstType)
.append(EQUAL_SIGN)
.append(secondType)
.append(System.lineSeparator());
return constraint;
String secondType = visitorBuffer;
return firstType + SPACE + EQUAL_SIGN + SPACE + secondType;
}
// todo use generateConstraint
@ -203,16 +205,37 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
@Override
public void visit(NamedType named) {
visitorBuffer = TEXTTT + CURLY_LEFT + named.getName() + CURLY_RIGHT;
needsParentheses = false;
}
@Override
public void visit(TypeVariable variable) {
String name;
switch (variable.getKind()) {
case TREE:
name = TREE_VARIABLE;
break;
case GENERATED_TYPE_ASSUMPTION:
name = GENERATED_ASSUMPTION_VARIABLE;
break;
case USER_INPUT:
name = USER_VARIABLE;
break;
default:
throw new IllegalStateException("unreachable code");
}
visitorBuffer = name + UNDERSCORE + CURLY_LEFT + variable.getIndex() + CURLY_RIGHT;
needsParentheses = false;
}
@Override
public void visit(FunctionType function) {
function.getParameter().accept(this);
String parameter = needsParentheses ? PAREN_LEFT + visitorBuffer + PAREN_RIGHT : visitorBuffer;
function.getOutput().accept(this);
String output = visitorBuffer;
visitorBuffer = parameter + SPACE + RIGHT_ARROW + SPACE + output;
needsParentheses = true;
}
}

9
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/package-info.java Normal file
View File

@ -0,0 +1,9 @@
/**
* This package contains the needed classes for displaying the type inference algorithm step-by-step.
*/
@NonNullFields
@NonNullApi
package edu.kit.typicalc.view.content.typeinferencecontent;
import org.springframework.lang.NonNullApi;
import org.springframework.lang.NonNullFields;