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

LatexCreator for let and const

Browse Source
This commit is contained in:
Johanna Stuber 2021-02-04 13:16:09 +01:00
parent 8dc7fbe725
commit a0e3eb34a2
7 changed files with 71 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java
View File

@ -18,14 +18,22 @@ public class BooleanTerm extends ConstTerm {
this.value = value;
}
/**
* Returns the value of the boolean constant term.
* @return the value of the term
*/
public boolean getValue() {
return value;
}
@Override
public NamedType getType() {
return NamedType.BOOLEAN;
}
@Override
public boolean hasLet() {
return false;
public void accept(TermVisitor termVisitor) {
termVisitor.visit(this);
}
@Override

5
src/main/java/edu/kit/typicalc/model/term/ConstTerm.java
View File

@ -28,11 +28,6 @@ public abstract class ConstTerm extends LambdaTerm {
return false;
}
@Override
public void accept(TermVisitor termVisitor) {
termVisitor.visit(this);
}
@Override
public InferenceStep accept(TermVisitorTree visitor, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
return visitor.visit(this, assumptions, type);

13
src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java
View File

@ -18,11 +18,24 @@ public class IntegerTerm extends ConstTerm {
this.value = value;
}
/**
* Returns the value of the integer constant term.
* @return the value of the term
*/
public int getValue() {
return value;
}
@Override
public NamedType getType() {
return NamedType.INT;
}
@Override
public void accept(TermVisitor termVisitor) {
termVisitor.visit(this);
}
@Override
public String toString() {
return Integer.toString(value);

12
src/main/java/edu/kit/typicalc/model/term/TermVisitor.java
View File

@ -26,8 +26,14 @@ public interface TermVisitor {
void visit(VarTerm varTerm);
/**
* Visit a constant.
* @param constTerm the constant
* Visit an integer constant.
* @param intTerm the integer constant
*/
void visit(ConstTerm constTerm);
void visit(IntegerTerm intTerm);
/**
* Visit a boolean constant.
* @param boolTerm the boolean constant
*/
void visit(BooleanTerm boolTerm);
}

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

@ -214,7 +214,8 @@ public class LatexCreator implements StepVisitor {
public void visit(LetStepDefault letD) {
tree.insert(0, generateConclusion(letD, LABEL_LET, BIC));
letD.getPremise().accept(this);
// todo implement
letD.getTypeInferer().getFirstInferenceStep().accept(this);
// todo correct?
}
@Override

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

@ -5,6 +5,8 @@ public final class LatexCreatorConstants {
}
protected static final String CONST = "Const";
protected static final String LET = "let";
protected static final String IN = "in";
protected static final String NEW_LINE = System.lineSeparator();
protected static final String SPACE = " ";
@ -39,6 +41,7 @@ public final class LatexCreatorConstants {
protected static final String LATEX_SPACE = "\\ ";
protected static final String FOR_ALL = "\\forall";
protected static final String TEXTTT = "\\texttt";
protected static final String TEXTBF = "\\textbf";
protected static final String RIGHT_ARROW = "\\rightarrow";
protected static final String INSTANTIATE_SIGN = "\\succeq";
protected static final String LATEX_IN = "\\in";

45
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreatorTerm.java
View File

@ -1,12 +1,6 @@
package edu.kit.typicalc.view.content.typeinferencecontent;
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.LambdaTerm;
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 static edu.kit.typicalc.view.content.typeinferencecontent.LatexCreatorConstants.*;
@ -68,17 +62,46 @@ public class LatexCreatorTerm implements TermVisitor {
}
@Override
public void visit(ConstTerm constTerm) {
// todo implement correctly (with extended termVisitor)
public void visit(IntegerTerm intTerm) {
latex.append(TEXTTT);
latex.append(CURLY_LEFT);
constTerm.accept(this);
latex.append(intTerm.getValue());
latex.append(CURLY_RIGHT);
needsParentheses = false;
}
@Override
public void visit(BooleanTerm boolTerm) {
latex.append(TEXTTT);
latex.append(CURLY_LEFT);
latex.append(boolTerm.getValue());
latex.append(CURLY_RIGHT);
needsParentheses = false;
}
@Override
public void visit(LetTerm letTerm) {
// todo implement
latex.append(TEXTTT)
.append(CURLY_LEFT)
.append(TEXTBF)
.append(CURLY_LEFT)
.append(LET)
.append(CURLY_RIGHT)
.append(CURLY_RIGHT)
.append(LATEX_SPACE);
letTerm.getVariable().accept(this);
latex.append(EQUALS);
letTerm.getVariableDefinition().accept(this);
latex.append(LATEX_SPACE)
.append(TEXTTT)
.append(CURLY_LEFT)
.append(TEXTBF)
.append(CURLY_LEFT)
.append(IN)
.append(CURLY_RIGHT)
.append(CURLY_RIGHT)
.append(LATEX_SPACE);
letTerm.getInner().accept(this);
needsParentheses = true;
}
}