This commit is contained in:
Johanna Stuber 2021-01-31 12:18:39 +01:00
commit b09b52e5df
10 changed files with 165 additions and 70 deletions

View File

@ -1,4 +1,45 @@
package edu.kit.typicalc.model;
import edu.kit.typicalc.util.Result;
import java.util.List;
/**
* Models one step of the unification algorithm with a list of constraints and a list of substitutions.
* These lists contain all the constraints or substitutions that are present in the unification after this step.
* When detected that this unification step leads to a contradiction or an infinite type,
* it contains a {@link UnificationError} instead of a list of substitutions.
*/
public class UnificationStep {
private final Result<List<Substitution>, UnificationError> substitutions;
private final List<Constraint> constraints;
/**
* Initializes a new {@link UnificationStep} with the given lists of constraints and substitutions.
* When detected that this unification step leads to a contradiction or an infinite type,
* it should be passed a {@link UnificationError} instead of a list of substitutions.
* @param substitutions list of substitutions, or an error
* @param constraints the list of all constraints of the unification (in the state resulting from this step)
*/
protected UnificationStep(Result<List<Substitution>, UnificationError> substitutions,
List<Constraint> constraints) {
this.substitutions = substitutions;
this.constraints = constraints;
}
/**
* Returns as a {@link Result} either the list of all substitutions
* of the unification (in the state resulting from this step).
* Or, in case of a detected contradiction or infinite type, a {@link UnificationError}.
*/
public Result<List<Substitution>, UnificationError> getSubstitutions() {
return substitutions;
}
/**
* @return a list of all resulting constraints
*/
public List<Constraint> getConstraints() {
return constraints;
}
}

View File

@ -28,10 +28,6 @@ public class LambdaLexer {
*/
public LambdaLexer(String term) {
this.term = term;
tokenize();
}
private void tokenize() {
Deque<Token> tokens = new ArrayDeque<>();
while (true) {
Result<Token, ParseError> token = parseNextToken();

View File

@ -17,7 +17,7 @@ public enum ParseError {
*/
UNEXPECTED_CHARACTER;
private Token cause;
private Token cause = new Token(Token.TokenType.EOF, "", -1);
public ParseError withToken(Token cause) {
this.cause = cause;

View File

@ -15,8 +15,8 @@ import java.util.Objects;
* The subclasses vary in the premise(s) they contain.
*/
public abstract class InferenceStep {
private Conclusion conclusion;
private Constraint constraint;
private final Conclusion conclusion;
private final Constraint constraint;
/**
* Initializes a new InferenceStep with the given values.

View File

@ -4,6 +4,8 @@ import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.TypeInfererLet;
import java.util.Objects;
/**
* Models one step of the inference tree where the let rule is applied. A let step contains an
* additional instance of a type inferer that is responisble for the sub-inference that takes
@ -46,4 +48,24 @@ public abstract class LetStep extends InferenceStep {
public TypeInfererLet getTypeInferer() {
return typeInferer;
}
@Override
public boolean equals(Object o) {
if (this == o) {
return true;
}
if (o == null || getClass() != o.getClass()) {
return false;
}
if (!super.equals(o)) {
return false;
}
LetStep letStep = (LetStep) o;
return premise.equals(letStep.premise) && typeInferer.equals(letStep.typeInferer);
}
@Override
public int hashCode() {
return Objects.hash(super.hashCode(), premise, typeInferer);
}
}

View File

@ -13,10 +13,7 @@ import java.util.Optional;
* Utility class to avoid unification logic duplication in type methods.
*/
final class UnificationUtil {
// TODO: document class? implementation detail?
private UnificationUtil() {
}
private UnificationUtil() { }
static Result<UnificationActions, UnificationError> functionFunction(FunctionType a, FunctionType b) {
return new Result<>(new UnificationActions(List.of(

View File

@ -16,7 +16,7 @@ import java.util.Map;
* only use packages and commands that MathJax supports. The LaTeX code is also usable
* outside of MathJax, in a normal .tex document.
*/
public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
public class LatexCreator implements StepVisitor, TypeVisitor {
private static final String CONST = "Const";
@ -45,6 +45,7 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
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 GAMMA = "\\Gamma";
private static final String LAMBDA = "\\lambda";
private static final String LATEX_SPACE = "\\ ";
@ -52,12 +53,13 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
private static final String RIGHT_ARROW = "\\rightarrow";
private static final String INSTANTIATE_SIGN = "\\succeq";
private static final String LATEX_IN = "\\in";
private static final String VDASH = "\\vdash";
private static final String TREE_BEGIN = "\\begin{prooftree}";
private static final String TREE_END = "\\end{prooftree}";
private final TypeInfererInterface typeInferer;
private final StringBuilder tree;
private final boolean stepLabels;
@ -81,18 +83,18 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
}
protected LatexCreator(TypeInfererInterface typeInferer, boolean stepLabels) {
this.typeInferer = typeInferer;
this.tree = new StringBuilder();
this.stepLabels = stepLabels;
// typeInferer.getFirstInferenceStep().accept(this);
}
/**
* @return the LaTeX-code for the proof tree
*/
protected String getTree() {
return "the $\\LaTeX$ inference tree should be here ";
} // todo implement
typeInferer.getFirstInferenceStep().accept(this);
return TREE_BEGIN + tree.toString() + TREE_END;
}
/**
* @return the LaTeX-code for constraints nad unification
@ -120,7 +122,9 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
private String conclusionToLatex(Conclusion conclusion) {
String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions());
return "{$some text$}";
String term = new LatexCreatorTerm(conclusion.getLambdaTerm()).getLatex();
String type = " \\tau_{42}";
return DOLLAR_SIGN + GAMMA + VDASH + term + COLON + type + DOLLAR_SIGN;
}
private StringBuilder generateConclusion(InferenceStep step, String label, String command) {
@ -129,7 +133,9 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
conclusion.append(label).append(NEW_LINE);
}
conclusion.append(command)
.append(CURLY_LEFT)
.append(conclusionToLatex(step.getConclusion()))
.append(CURLY_RIGHT)
.append(NEW_LINE);
return conclusion;
}
@ -144,8 +150,7 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
private String generateVarStepPremise(VarStep var) {
String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions());
var.getConclusion().getLambdaTerm().accept(this);
String term = visitorBuffer;
String term = new LatexCreatorTerm(var.getConclusion().getLambdaTerm()).getLatex();
String type = generateTypeAbstraction(var.getTypeAbsInPremise());
return AXC + CURLY_LEFT + DOLLAR_SIGN + PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term
+ PAREN_RIGHT + EQUAL_SIGN + type + DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
@ -180,7 +185,7 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
@Override
public void visit(ConstStepDefault constD) {
tree.insert(0, generateConclusion(constD, LABEL_CONST, UIC));
constD.getConclusion().getLambdaTerm().accept(this);
visitorBuffer = new LatexCreatorTerm(constD.getConclusion().getLambdaTerm()).getLatex();
String step = AXC + CURLY_LEFT + DOLLAR_SIGN + visitorBuffer + SPACE + LATEX_IN + SPACE + CONST
+ DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
tree.insert(0, step);
@ -212,49 +217,6 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
// todo implement
}
@Override
public void visit(AppTerm appTerm) {
appTerm.getFunction().accept(this);
String function = visitorBuffer;
appTerm.getParameter().accept(this);
String parameter = needsParentheses ? PAREN_LEFT + visitorBuffer + PAREN_RIGHT : visitorBuffer;
needsParentheses = true;
visitorBuffer = function + LATEX_SPACE + parameter;
}
@Override
public void visit(AbsTerm absTerm) {
absTerm.getVariable().accept(this);
String variable = visitorBuffer;
absTerm.getInner().accept(this);
String inner = visitorBuffer;
needsParentheses = false;
visitorBuffer = LAMBDA + SPACE + variable + DOT_SIGN + LATEX_SPACE + inner;
}
@Override
public void visit(VarTerm varTerm) {
needsParentheses = false;
visitorBuffer = TEXTTT + CURLY_LEFT + varTerm.getName() + CURLY_RIGHT;
}
@Override
public void visit(ConstTerm constTerm) {
// todo implement correctly (with extended termVisitor)
String constant = visitorBuffer;
needsParentheses = false;
visitorBuffer = TEXTTT + CURLY_LEFT + constant + CURLY_RIGHT;
}
@Override
public void visit(LetTerm letTerm) {
// todo implement
}
@Override
public void visit(NamedType named) {
visitorBuffer = TEXTTT + CURLY_LEFT + named.getName() + CURLY_RIGHT;

View File

@ -0,0 +1,79 @@
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;
public class LatexCreatorTerm implements TermVisitor {
// TODO: document
private static final String PAREN_LEFT = "(";
private static final String PAREN_RIGHT = ")";
private static final String LATEX_SPACE = "\\ ";
private static final String LAMBDA = "\\lambda";
private static final String CURLY_LEFT = "{";
private static final String CURLY_RIGHT = "}";
private static final String TEXTTT = "\\texttt";
private final StringBuilder latex;
private boolean needsParentheses = false;
protected LatexCreatorTerm(LambdaTerm lambdaTerm) {
this.latex = new StringBuilder();
lambdaTerm.accept(this);
}
public String getLatex() {
return latex.toString();
}
@Override
public void visit(AppTerm appTerm) {
appTerm.getFunction().accept(this);
latex.append(LATEX_SPACE);
appTerm.getParameter().accept(this);
if (needsParentheses) {
latex.insert(0, PAREN_LEFT);
latex.append(PAREN_RIGHT);
}
needsParentheses = true;
}
@Override
public void visit(AbsTerm absTerm) {
latex.append(LAMBDA);
latex.append(' ');
absTerm.getVariable().accept(this);
latex.append('.');
latex.append(LATEX_SPACE);
absTerm.getInner().accept(this);
needsParentheses = false;
}
@Override
public void visit(VarTerm varTerm) {
needsParentheses = false;
latex.append(TEXTTT);
latex.append(CURLY_LEFT);
latex.append(varTerm.getName());
latex.append(CURLY_RIGHT);
}
@Override
public void visit(ConstTerm constTerm) {
// todo implement correctly (with extended termVisitor)
latex.append(TEXTTT);
latex.append(CURLY_LEFT);
constTerm.accept(this);
latex.append(CURLY_RIGHT);
needsParentheses = false;
}
@Override
public void visit(LetTerm letTerm) {
// todo implement
}
}

View File

@ -21,9 +21,9 @@ public class TypeInferenceView extends VerticalLayout
private MathjaxUnification unification;
private MathjaxProofTree tree;
private TypeInfererInterface typeInferer;
private Div content;
private ControlPanel controlPanel;
private final transient TypeInfererInterface typeInferer;
private final Div content;
private final ControlPanel controlPanel;
public TypeInferenceView() {
typeInferer = ComponentUtil.getData(UI.getCurrent(), TypeInfererInterface.class);

View File

@ -1,9 +1,7 @@
/**
* 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;
import org.springframework.lang.NonNullApi;