mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 10:20:41 +00:00
Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc
This commit is contained in:
commit
75d686d8af
@ -6,6 +6,10 @@ import edu.kit.typicalc.model.type.Type;
|
||||
* Constrains two types to be equal.
|
||||
*/
|
||||
public class Constraint {
|
||||
|
||||
private final Type a;
|
||||
private final Type b;
|
||||
|
||||
/**
|
||||
* Creates a new constraint using the two types.
|
||||
*
|
||||
@ -13,23 +17,23 @@ public class Constraint {
|
||||
* @param b second type
|
||||
*/
|
||||
public Constraint(Type a, Type b) {
|
||||
// TODO
|
||||
// TODO: null checks?
|
||||
this.a = a;
|
||||
this.b = b;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the first type
|
||||
*/
|
||||
public Type getFirstType() {
|
||||
return null;
|
||||
// TODO
|
||||
return a;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the second type
|
||||
*/
|
||||
public Type getSecondType() {
|
||||
return null;
|
||||
// TODO
|
||||
return b;
|
||||
}
|
||||
|
||||
}
|
||||
|
@ -7,6 +7,10 @@ import edu.kit.typicalc.model.type.TypeVariable;
|
||||
* A substitution specifies that some type should be replaced by a different type.
|
||||
*/
|
||||
public class Substitution {
|
||||
|
||||
private final TypeVariable a;
|
||||
private final Type b;
|
||||
|
||||
/**
|
||||
* Creates a new substitution using a type variable a and a type b. When the substitution is applied to a type,
|
||||
* all occurring instances of a should be substituted with b.
|
||||
@ -15,22 +19,22 @@ public class Substitution {
|
||||
* @param b type to insert
|
||||
*/
|
||||
public Substitution(TypeVariable a, Type b) {
|
||||
// TODO
|
||||
// TODO: null checks?
|
||||
this.a = a;
|
||||
this.b = b;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the type variable
|
||||
*/
|
||||
public TypeVariable getVariable() {
|
||||
return null;
|
||||
// TODO
|
||||
return a;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the replacement type
|
||||
*/
|
||||
Type getType() {
|
||||
return null;
|
||||
// TODO
|
||||
return b;
|
||||
}
|
||||
}
|
||||
|
@ -37,9 +37,9 @@ public interface StepVisitor {
|
||||
|
||||
/**
|
||||
* Visits a VarStepWithLet.
|
||||
* @param varD the VarStepWithLet to visit
|
||||
* @param varL the VarStepWithLet to visit
|
||||
*/
|
||||
void visitVarStepWithLet(AbsStepDefault varD);
|
||||
void visitVarStepWithLet(VarStepWithLet varL);
|
||||
|
||||
/**
|
||||
* Visits a LetStepDefault.
|
||||
|
@ -0,0 +1,4 @@
|
||||
package edu.kit.typicalc.model.step;
|
||||
|
||||
public class VarStepWithLet {
|
||||
}
|
@ -1,14 +1,9 @@
|
||||
package edu.kit.typicalc.view.content.typeinferencecontent;
|
||||
|
||||
|
||||
import edu.kit.typicalc.model.Conclusion;
|
||||
import edu.kit.typicalc.model.TypeInfererInterface;
|
||||
import edu.kit.typicalc.model.step.AbsStepDefault;
|
||||
import edu.kit.typicalc.model.step.AbsStepWithLet;
|
||||
import edu.kit.typicalc.model.step.AppStepDefault;
|
||||
import edu.kit.typicalc.model.step.ConstStepDefault;
|
||||
import edu.kit.typicalc.model.step.LetStepDefault;
|
||||
import edu.kit.typicalc.model.step.StepVisitor;
|
||||
import edu.kit.typicalc.model.step.VarStepDefault;
|
||||
import edu.kit.typicalc.model.step.*;
|
||||
import edu.kit.typicalc.model.term.TermVisitor;
|
||||
import edu.kit.typicalc.model.type.TypeVisitor;
|
||||
|
||||
@ -21,12 +16,38 @@ import edu.kit.typicalc.model.type.TypeVisitor;
|
||||
*/
|
||||
public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
|
||||
|
||||
private static final String LABEL_ABS = "\\LeftLabel{ABS}";
|
||||
private static final String LABEL_APP = "\\LeftLabel{APP}";
|
||||
private static final String LABEL_CONST = "\\LeftLabel{CONST}";
|
||||
private static final String LABEL_VAR = "\\LeftLabel{VAR}";
|
||||
private static final String LABEL_LET = "\\LeftLabel{LET}";
|
||||
|
||||
private static final String UIC = "\\UnaryInfC";
|
||||
private static final String BIC = "\\BinaryInfC";
|
||||
private static final String AXC = "\\AxiomC";
|
||||
|
||||
private static final String TREE_BEGIN = "\\begin{prooftree}";
|
||||
private static final String TREE_END = "\\end{prooftree}";
|
||||
|
||||
|
||||
|
||||
|
||||
private final StringBuilder tree;
|
||||
private final boolean stepLabels;
|
||||
|
||||
/**
|
||||
* Generate the pieces of LaTeX-code from the type inferer.
|
||||
*
|
||||
* @param typeInferer theTypeInfererInterface to create the LaTeX-code from
|
||||
*/
|
||||
protected LatexCreator(TypeInfererInterface typeInferer) {
|
||||
this(typeInferer, true);
|
||||
}
|
||||
|
||||
protected LatexCreator(TypeInfererInterface typeInferer, boolean stepLabels) {
|
||||
this.tree = new StringBuilder();
|
||||
this.stepLabels = stepLabels;
|
||||
|
||||
typeInferer.getFirstInferenceStep().accept(this);
|
||||
}
|
||||
|
||||
@ -51,39 +72,63 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
|
||||
return null;
|
||||
}
|
||||
|
||||
private String conclusionToLatex(Conclusion conclusion) {
|
||||
// todo implement
|
||||
return "";
|
||||
}
|
||||
|
||||
private void generateConclusion(InferenceStep step, String label, String command) {
|
||||
StringBuilder conclusion = new StringBuilder();
|
||||
if (stepLabels) {
|
||||
conclusion.append(label);
|
||||
conclusion.append(System.lineSeparator());
|
||||
}
|
||||
conclusion.append(command);
|
||||
conclusion.append(conclusionToLatex(step.getConclusion()));
|
||||
conclusion.append(System.lineSeparator());
|
||||
tree.insert(0, conclusion);
|
||||
}
|
||||
|
||||
@Override
|
||||
public void visitAbsStepDefault(AbsStepDefault absD) {
|
||||
generateConclusion(absD, LABEL_ABS, UIC);
|
||||
|
||||
|
||||
}
|
||||
|
||||
@Override
|
||||
public void visitAbsStepWithLet(AbsStepWithLet absL) {
|
||||
generateConclusion(absL, LABEL_ABS, UIC);
|
||||
|
||||
}
|
||||
|
||||
@Override
|
||||
public void visitAppStepDefault(AppStepDefault appD) {
|
||||
generateConclusion(appD, LABEL_APP, UIC);
|
||||
|
||||
}
|
||||
|
||||
@Override
|
||||
public void visitConstStepDefault(ConstStepDefault constD) {
|
||||
generateConclusion(constD, LABEL_CONST, UIC);
|
||||
|
||||
}
|
||||
|
||||
@Override
|
||||
public void visitVarStepDefault(VarStepDefault varD) {
|
||||
generateConclusion(varD, LABEL_VAR, UIC);
|
||||
|
||||
}
|
||||
|
||||
@Override
|
||||
public void visitVarStepWithLet(AbsStepDefault varD) {
|
||||
public void visitVarStepWithLet(VarStepWithLet varL) {
|
||||
generateConclusion(varL, LABEL_VAR, UIC);
|
||||
|
||||
}
|
||||
|
||||
@Override
|
||||
public void visitLetStepDefault(LetStepDefault letD) {
|
||||
generateConclusion(letD, LABEL_LET, UIC);
|
||||
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user