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

implement typeabstraction in LatexCreatorConstraints

Browse Source
This commit is contained in:
ucrhh 2021-02-19 18:37:59 +01:00
parent 0ecb8be4b6
commit 1f68eda42e
2 changed files with 38 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -15,6 +15,7 @@ public final class LatexCreatorConstants {
protected static final String MGU = "mgu";
protected static final String UNIFY = "unify";
protected static final String CONSTRAINT_SET = "C";
protected static final String TYPE_ABSTRACTION = "ta";
protected static final String DOLLAR_SIGN = "$";
protected static final char NEW_LINE = '\n';
@ -58,6 +59,7 @@ public final class LatexCreatorConstants {
protected static final String FOR_ALL = "\\forall";
protected static final String MONO_TEXT = "\\texttt";
protected static final String BOLD_TEXT = "\\textbf";
protected static final String TEXT = "\\text";
protected static final String RIGHT_ARROW = "\\rightarrow";
protected static final String INSTANTIATE_SIGN = "\\succeq";
protected static final String LATEX_IN = "\\in";

44
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java
View File

@ -2,10 +2,15 @@ package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator;
import edu.kit.typicalc.model.*;
import edu.kit.typicalc.model.step.*;
import edu.kit.typicalc.model.term.LetTerm;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.TypeAbstraction;
import edu.kit.typicalc.util.Result;
import java.nio.channels.IllegalSelectorException;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;
import java.util.Optional;
import java.util.function.Function;
@ -26,6 +31,8 @@ public class LatexCreatorConstraints implements StepVisitor {
private final TreeNumberGenerator numberGenerator;
private final String constraintSetIndex;
private final String prefix;
private final Optional<VarTerm> letVariable;
private final Optional<Map<VarTerm, TypeAbstraction>> newTypeAssumption;
private String prevStep;
private final Function<UnificationError, String> translationProvider;
@ -40,15 +47,19 @@ public class LatexCreatorConstraints implements StepVisitor {
Function<UnificationError, String> translationProvider) {
this(typeInferer,
new ConstraintSetIndexFactory(), new TreeNumberGenerator(),
FIRST_PREFIX, translationProvider);
FIRST_PREFIX, Optional.empty(), Optional.empty(), translationProvider);
}
private LatexCreatorConstraints(TypeInfererInterface typeInferer,
ConstraintSetIndexFactory constraintSetIndexFactory,
TreeNumberGenerator numberGenerator,
String prefix,
Optional<VarTerm> letVariable,
Optional<Map<VarTerm, TypeAbstraction>> newTypeAssumption,
Function<UnificationError, String> translationProvider) {
this.prefix = prefix;
this.letVariable = letVariable;
this.newTypeAssumption = newTypeAssumption;
this.prevStep = "";
this.constraintSetIndexFactory = constraintSetIndexFactory;
this.numberGenerator = numberGenerator;
@ -163,10 +174,15 @@ public class LatexCreatorConstraints implements StepVisitor {
@Override
public void visit(LetStepDefault letD) {
addConstraint(letD);
LetTerm term = (LetTerm) letD.getConclusion().getLambdaTerm();
Optional<Map<VarTerm, TypeAbstraction>> newTypeAss = Optional.empty();
if (letD.getTypeInferer().getMGU().isPresent()) {
newTypeAss = Optional.of(letD.getPremise().getConclusion().getTypeAssumptions());
}
LatexCreatorConstraints subCreator = new LatexCreatorConstraints(letD.getTypeInferer(),
constraintSetIndexFactory, numberGenerator,
constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE,
translationProvider);
constraints.get(constraints.size() - 1) + LATEX_NEW_LINE + NEW_LINE, Optional.of(term.getVariable()),
newTypeAss, translationProvider);
constraints.addAll(subCreator.getEverything());
// cancels constraint creation if sub inference failed
@ -311,15 +327,27 @@ public class LatexCreatorConstraints implements StepVisitor {
// generates the TypeAssumptions for the right sub tree of a let step
private String generateNewTypeAssumptions(String subPrefix) {
InferenceStep step = typeInferer.getFirstInferenceStep();
StringBuilder latex = new StringBuilder();
latex.append(subPrefix);
latex.append(LATEX_NEW_LINE + AMPERSAND);
latex.append("Neue Typumgebung:");
latex.append(SIGMA);
latex.append(LATEX_NEW_LINE + AMPERSAND + TEXT + CURLY_LEFT);
latex.append("Neue Typumgebung: ");
latex.append("" + CURLY_RIGHT + SIGMA);
latex.append(constraintSetIndex);
latex.append(PAREN_LEFT);
latex.append(typeAssumptionsToLatex(typeInferer.getFirstInferenceStep().getConclusion().getTypeAssumptions()));
latex.append(PAREN_RIGHT);
latex.append(typeAssumptionsToLatex(step.getConclusion().getTypeAssumptions()));
latex.append("" + PAREN_RIGHT + COMMA + LATEX_SPACE);
latex.append(new LatexCreatorTerm(letVariable.orElseThrow(IllegalStateException::new)).getLatex());
latex.append("" + COLON + TYPE_ABSTRACTION + PAREN_LEFT + SIGMA);
latex.append(constraintSetIndex);
latex.append(PAREN_LEFT);
latex.append(new LatexCreatorType(typeInferer.getFirstInferenceStep().getConclusion().getType()).getLatex());
latex.append("" + PAREN_RIGHT + COMMA + SIGMA);
latex.append(constraintSetIndex);
latex.append(PAREN_LEFT);
latex.append(typeAssumptionsToLatex(step.getConclusion().getTypeAssumptions()));
latex.append("" + PAREN_RIGHT + PAREN_RIGHT + EQUALS);
latex.append(typeAssumptionsToLatex(newTypeAssumption.orElseThrow(IllegalSelectorException::new)));
return latex.toString();
}
}