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

Instantiate types in all tooltips

Browse Source 
see #18
This commit is contained in:
Arne Keller 2021-07-26 10:40:40 +02:00
parent 19ec6cbc1a
commit eff5e4340e
2 changed files with 62 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

89
src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java
View File

@ -1,13 +1,14 @@
package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.FunctionType;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstraints;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorMode;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorType;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.*;
import org.apache.commons.lang3.tuple.Pair;
import java.util.ArrayList;
import java.util.List;
import java.util.stream.Collectors;
public class StepAnnotator implements StepVisitor {
private final List<String> annotations = new ArrayList<>();
@ -18,58 +19,90 @@ public class StepAnnotator implements StepVisitor {
@Override
public void visit(AbsStepDefault absD) {
var t1 = ((FunctionType) absD.getConstraint().getSecondType()).getParameter();
var t2 = ((FunctionType) absD.getConstraint().getSecondType()).getOutput();
annotations.add("$$\\begin{align}"
+ "&" + LatexCreatorConstants.RULE_VARIABLE + "_1 := "
+ new LatexCreatorType(t1, LatexCreatorMode.NORMAL).getLatex() + LatexCreatorConstants.LATEX_NEW_LINE
+ "\n"
+ "&" + LatexCreatorConstants.RULE_VARIABLE + "_2 := "
+ new LatexCreatorType(t2, LatexCreatorMode.NORMAL).getLatex() + LatexCreatorConstants.LATEX_NEW_LINE
+ "\n"
+ "&" + LatexCreatorConstraints.createSingleConstraint(absD.getConstraint(), LatexCreatorMode.NORMAL)
+ "\\end{align}$$");
visitAbs(absD);
absD.getPremise().accept(this);
}
@Override
public void visit(AbsStepWithLet absL) {
annotations.add("$"
+ LatexCreatorConstraints.createSingleConstraint(absL.getConstraint(), LatexCreatorMode.NORMAL) + "$");
visitAbs(absL);
absL.getPremise().accept(this);
}
private void visitAbs(AbsStep absStep) {
var t1 = ((FunctionType) absStep.getConstraint().getSecondType()).getParameter();
var t2 = ((FunctionType) absStep.getConstraint().getSecondType()).getOutput();
visitGeneric(t1, t2, absStep.getConstraint());
}
private void visitGeneric(Type t1, Type t2, Constraint c) {
visitGeneric2(List.of(Pair.of("_1", t1), Pair.of("_2", t2)), c);
}
private void visitGeneric2(List<Pair<String, Type>> types, Constraint c) {
visitGeneric3(
types.stream()
.map(pair -> Pair.of(pair.getLeft(),
new LatexCreatorType(pair.getRight(), LatexCreatorMode.NORMAL).getLatex()))
.collect(Collectors.toList()),
c
);
}
private void visitGeneric3(List<Pair<String, String>> types, Constraint c) {
var sb = new StringBuilder("$$\\begin{align}");
for (var pair : types) {
sb.append("&" + LatexCreatorConstants.RULE_VARIABLE)
.append(pair.getLeft())
.append(" := ")
.append(pair.getRight())
.append(LatexCreatorConstants.LATEX_NEW_LINE)
.append("\n");
}
sb.append("&").append(LatexCreatorConstraints.createSingleConstraint(c, LatexCreatorMode.NORMAL));
annotations.add(sb + "\\end{align}$$");
}
@Override
public void visit(AppStepDefault appD) {
annotations.add("$"
+ LatexCreatorConstraints.createSingleConstraint(appD.getConstraint(), LatexCreatorMode.NORMAL) + "$");
visitGeneric(
appD.getPremise2().getConclusion().getType(),
appD.getConclusion().getType(),
appD.getConstraint());
appD.getPremise1().accept(this);
appD.getPremise2().accept(this);
}
@Override
public void visit(ConstStepDefault constD) {
annotations.add("$"
+ LatexCreatorConstraints.createSingleConstraint(constD.getConstraint(), LatexCreatorMode.NORMAL)
+ "$");
visitGeneric2(List.of(Pair.of("_c", constD.getConclusion().getType())), constD.getConstraint());
}
@Override
public void visit(VarStepDefault varD) {
annotations.add("$"
+ LatexCreatorConstraints.createSingleConstraint(varD.getConstraint(), LatexCreatorMode.NORMAL) + "$");
visitGeneric2(List.of(
Pair.of("", varD.getInstantiatedTypeAbs()),
Pair.of("'", varD.getConclusion().getType())),
varD.getConstraint());
}
@Override
public void visit(VarStepWithLet varL) {
annotations.add("$"
+ LatexCreatorConstraints.createSingleConstraint(varL.getConstraint(), LatexCreatorMode.NORMAL) + "$");
visitGeneric3(List.of(
Pair.of("'",
AssumptionGeneratorUtil.generateTypeAbstraction(varL.getTypeAbsInPremise(),
LatexCreatorMode.NORMAL)),
Pair.of("",
new LatexCreatorType(varL.getInstantiatedTypeAbs(), LatexCreatorMode.NORMAL).getLatex())),
varL.getConstraint());
}
@Override
public void visit(LetStepDefault letD) {
annotations.add("$"
+ LatexCreatorConstraints.createSingleConstraint(letD.getConstraint(), LatexCreatorMode.NORMAL) + "$");
visitGeneric2(List.of(
Pair.of("_1", letD.getTypeInferer().getFirstInferenceStep().getConclusion().getType()),
Pair.of("_2", letD.getPremise().getConclusion().getType())),
letD.getConstraint());
letD.getTypeInferer().getFirstInferenceStep().accept(this);
letD.getPremise().accept(this);
}

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

@ -37,7 +37,7 @@ public final class AssumptionGeneratorUtil {
}
}
protected static String generateTypeAbstraction(TypeAbstraction abs, LatexCreatorMode mode) {
public static String generateTypeAbstraction(TypeAbstraction abs, LatexCreatorMode mode) {
StringBuilder abstraction = new StringBuilder();
if (abs.hasQuantifiedVariables()) {
abstraction.append(FOR_ALL);