From eff5e4340ee461f269b07e204dac68b8c206b7e2 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 26 Jul 2021 10:40:40 +0200 Subject: [PATCH] Instantiate types in all tooltips see #18 --- .../typicalc/model/step/StepAnnotator.java | 89 +++++++++++++------ .../latexcreator/AssumptionGeneratorUtil.java | 2 +- 2 files changed, 62 insertions(+), 29 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java b/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java index a7b9aa5..4bc0e84 100644 --- a/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java +++ b/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java @@ -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 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> 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> 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); } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java index ad0a6dd..14e2d20 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java @@ -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);