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

Instantiate abs step

Browse Source 
see #18
This commit is contained in:
Arne Keller 2021-07-20 15:02:29 +02:00
parent 2e2b39c13b
commit 8c9f2ab67c
3 changed files with 16 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1,7 +1,10 @@
package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.type.FunctionType;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstraints;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorMode;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorType;
import java.util.ArrayList;
import java.util.List;
@ -15,8 +18,15 @@ public class StepAnnotator implements StepVisitor {
@Override
public void visit(AbsStepDefault absD) {
annotations.add("$"
+ LatexCreatorConstraints.createSingleConstraint(absD.getConstraint(), LatexCreatorMode.NORMAL) + "$");
var t1 = ((FunctionType) absD.getConstraint().getSecondType()).getParameter();
var t2 = ((FunctionType) absD.getConstraint().getSecondType()).getOutput();
annotations.add("$$\\begin{align}"
+ "&" + LatexCreatorConstants.RULE_VARIABLE + "_1 := "
+ new LatexCreatorType(t1, LatexCreatorMode.NORMAL).getLatex() + LatexCreatorConstants.LATEX_NEW_LINE + "\n"
+ "&" + LatexCreatorConstants.RULE_VARIABLE + "_2 := "
+ new LatexCreatorType(t2, LatexCreatorMode.NORMAL).getLatex() + LatexCreatorConstants.LATEX_NEW_LINE + "\n"
+ "&" + LatexCreatorConstraints.createSingleConstraint(absD.getConstraint(), LatexCreatorMode.NORMAL)
+ "\\end{align}$$");
absD.getPremise().accept(this);
}

3
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java
View File

@ -55,10 +55,11 @@ public final class LatexCreatorConstants {
protected static final String TREE_VARIABLE = "\\alpha";
protected static final String GENERATED_ASSUMPTION_VARIABLE = "\\beta";
protected static final String USER_VARIABLE = "\\tau";
public static final String RULE_VARIABLE = "\\tau";
protected static final String SIGMA = "\\sigma";
protected static final String GAMMA = "\\Gamma";
protected static final String LATEX_NEW_LINE = "\\\\";
public static final String LATEX_NEW_LINE = "\\\\";
protected static final String CIRC = "\\circ";
protected static final String COLOR_RED = "\\color{Red}";
protected static final String COLOR_HIGHLIGHTED = "\\color{RoyalBlue}";

4
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java
View File

@ -27,7 +27,7 @@ public class LatexCreatorType implements TypeVisitor {
*
* @param type the type
*/
protected LatexCreatorType(Type type, LatexCreatorMode mode) {
public LatexCreatorType(Type type, LatexCreatorMode mode) {
this.type = type;
this.mode = mode;
type.accept(this);
@ -36,7 +36,7 @@ public class LatexCreatorType implements TypeVisitor {
/**
* @return the generated LaTeX code
*/
protected String getLatex() {
public String getLatex() {
return latex.toString();
}