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

partially implement let type assumptions

Browse Source
This commit is contained in:
ucrhh 2021-02-19 14:55:02 +01:00
parent 70f8e64423
commit 0ecb8be4b6
3 changed files with 70 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java Normal file
View File

@ -0,0 +1,46 @@
package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.Map;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.DOT_SIGN;
public final class AssumptionGeneratorUtil {
private AssumptionGeneratorUtil() { }
protected static String typeAssumptionsToLatex(Map<VarTerm, TypeAbstraction> typeAssumptions) {
if (typeAssumptions.isEmpty()) {
return "";
} else {
StringBuilder assumptions = new StringBuilder();
typeAssumptions.forEach(((varTerm, typeAbstraction) -> {
String termLatex = new LatexCreatorTerm(varTerm).getLatex();
String abstraction = generateTypeAbstraction(typeAbstraction);
assumptions.append(termLatex)
.append(COLON)
.append(abstraction)
.append(COMMA);
}));
assumptions.deleteCharAt(assumptions.length() - 1);
return assumptions.toString();
}
}
protected static String generateTypeAbstraction(TypeAbstraction abs) {
StringBuilder abstraction = new StringBuilder();
if (abs.hasQuantifiedVariables()) {
abstraction.append(FOR_ALL);
abs.getQuantifiedVariables().forEach(typeVariable -> {
String variableTex = new LatexCreatorType(typeVariable).getLatex();
abstraction.append(variableTex).append(COMMA);
});
abstraction.deleteCharAt(abstraction.length() - 1);
abstraction.append(DOT_SIGN);
}
abstraction.append(new LatexCreatorType(abs.getInnerType()).getLatex());
return abstraction.toString();
}
}

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

@ -4,13 +4,12 @@ import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.model.UnificationError;
import edu.kit.typicalc.model.step.*;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.List;
import java.util.Map;
import java.util.function.Function;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.AssumptionGeneratorUtil.generateTypeAbstraction;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.AssumptionGeneratorUtil.typeAssumptionsToLatex;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*;
/**
@ -88,26 +87,6 @@ public class LatexCreator implements StepVisitor {
}
private String typeAssumptionsToLatex(Map<VarTerm, TypeAbstraction> typeAssumptions) {
if (typeAssumptions.isEmpty()) {
return "";
} else {
StringBuilder assumptions = new StringBuilder();
typeAssumptions.forEach(((varTerm, typeAbstraction) -> {
String termLatex = new LatexCreatorTerm(varTerm).getLatex();
String abstraction = generateTypeAbstraction(typeAbstraction);
assumptions.append(termLatex)
.append(COLON)
.append(abstraction)
.append(COMMA);
}));
assumptions.deleteCharAt(assumptions.length() - 1);
return assumptions.toString();
}
}
private String conclusionToLatex(Conclusion conclusion) {
String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions());
String term = new LatexCreatorTerm(conclusion.getLambdaTerm()).getLatex();
@ -136,21 +115,6 @@ public class LatexCreator implements StepVisitor {
+ PAREN_RIGHT + EQUALS + type + DOLLAR_SIGN;
}
private String generateTypeAbstraction(TypeAbstraction abs) {
StringBuilder abstraction = new StringBuilder();
if (abs.hasQuantifiedVariables()) {
abstraction.append(FOR_ALL);
abs.getQuantifiedVariables().forEach(typeVariable -> {
String variableTex = new LatexCreatorType(typeVariable).getLatex();
abstraction.append(variableTex).append(COMMA);
});
abstraction.deleteCharAt(abstraction.length() - 1);
abstraction.append(DOT_SIGN);
}
abstraction.append(new LatexCreatorType(abs.getInnerType()).getLatex());
return abstraction.toString();
}
@Override
public void visit(AbsStepDefault absD) {

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

@ -9,6 +9,7 @@ import java.util.List;
import java.util.Optional;
import java.util.function.Function;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.AssumptionGeneratorUtil.typeAssumptionsToLatex;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*;
/**
@ -87,6 +88,13 @@ public class LatexCreatorConstraints implements StepVisitor {
}
if (FIRST_PREFIX.equals(prefix)) {
result.replaceAll(content -> ALIGN_BEGIN + content + ALIGN_END);
} else {
// add the new type assumptions only during a let sub inference where
// the unification was successful
typeInferer.getMGU().ifPresent(mgu -> {
result.add(generateNewTypeAssumptions(result.get(result.size() - 1)));
numberGenerator.push();
});
}
return result;
}
@ -300,4 +308,18 @@ public class LatexCreatorConstraints implements StepVisitor {
latex.append(new LatexCreatorType(typeInferer.getType().get()).getLatex());
return latex.toString();
}
// generates the TypeAssumptions for the right sub tree of a let step
private String generateNewTypeAssumptions(String subPrefix) {
StringBuilder latex = new StringBuilder();
latex.append(subPrefix);
latex.append(LATEX_NEW_LINE + AMPERSAND);
latex.append("Neue Typumgebung:");
latex.append(SIGMA);
latex.append(constraintSetIndex);
latex.append(PAREN_LEFT);
latex.append(typeAssumptionsToLatex(typeInferer.getFirstInferenceStep().getConclusion().getTypeAssumptions()));
latex.append(PAREN_RIGHT);
return latex.toString();
}
}