From 7abfd66aa82b9ea51903fe54756a2a96402cf93b Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 16 Aug 2021 09:50:43 +0200 Subject: [PATCH] Fix some bugs of the unification explanation see #20 --- frontend/styles/view/type-inference.css | 1 + .../edu/kit/typicalc/model/Unification.java | 8 ++-- .../kit/typicalc/model/UnificationStep.java | 18 +++++++- .../typicalc/view/TypicalcI18NProvider.java | 4 +- .../ExplanationCreatorUnification.java | 42 +++++++++---------- .../ExplanationTranslationProvider.java | 28 +++++++++++++ .../language/translation_de.properties | 15 +++---- .../language/translation_en.properties | 4 +- .../kit/typicalc/model/UnificationTest.java | 35 +++++++--------- .../latexcreator/ExplanationCreatorTest.java | 16 +++++++ 10 files changed, 111 insertions(+), 60 deletions(-) create mode 100644 src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationTranslationProvider.java create mode 100644 src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorTest.java diff --git a/frontend/styles/view/type-inference.css b/frontend/styles/view/type-inference.css index 2191daa..29ee42d 100644 --- a/frontend/styles/view/type-inference.css +++ b/frontend/styles/view/type-inference.css @@ -43,6 +43,7 @@ tc-explanation { max-width: 40em; padding-left: 1em; padding-right: 1em; + overflow-y: auto; } #rules-button { diff --git a/src/main/java/edu/kit/typicalc/model/Unification.java b/src/main/java/edu/kit/typicalc/model/Unification.java index 35f45f3..d738458 100644 --- a/src/main/java/edu/kit/typicalc/model/Unification.java +++ b/src/main/java/edu/kit/typicalc/model/Unification.java @@ -24,7 +24,8 @@ public class Unification { steps = new ArrayList<>(); List substitutions = new ArrayList<>(); - steps.add(new UnificationStep(new Result<>(Collections.emptyList()), new ArrayList<>(constraints))); + steps.add(new UnificationStep( + new Result<>(Collections.emptyList()), new ArrayList<>(constraints), Optional.empty())); while (!constraints.isEmpty()) { Constraint c = constraints.removeFirst(); // calculate the result of this constraint @@ -32,7 +33,7 @@ public class Unification { Type b = c.getSecondType(); Result actions = a.constrainEqualTo(b); if (actions.isError()) { - steps.add(new UnificationStep(new Result<>(actions), new ArrayList<>(constraints))); + steps.add(new UnificationStep(new Result<>(actions), new ArrayList<>(constraints), Optional.of(c))); substitutionsResult = new Result<>(actions); return; } @@ -56,7 +57,8 @@ public class Unification { for (Constraint constraint : thisStep.getConstraints()) { constraints.addFirst(constraint); } - steps.add(new UnificationStep(new Result<>(new ArrayList<>(substitutions)), new ArrayList<>(constraints))); + steps.add(new UnificationStep( + new Result<>(new ArrayList<>(substitutions)), new ArrayList<>(constraints), Optional.of(c))); } substitutionsResult = new Result<>(substitutions); diff --git a/src/main/java/edu/kit/typicalc/model/UnificationStep.java b/src/main/java/edu/kit/typicalc/model/UnificationStep.java index 998927c..ac0616f 100644 --- a/src/main/java/edu/kit/typicalc/model/UnificationStep.java +++ b/src/main/java/edu/kit/typicalc/model/UnificationStep.java @@ -5,6 +5,7 @@ import edu.kit.typicalc.util.Result; import java.util.Arrays; import java.util.List; import java.util.Objects; +import java.util.Optional; /** * Models one step of the unification algorithm with a list of constraints and a list of substitutions. @@ -15,6 +16,7 @@ import java.util.Objects; public class UnificationStep { private final Result, UnificationError> substitutions; private final List constraints; + private final Optional processedConstraint; /** * Initializes a new {@link UnificationStep} with the given lists of constraints and substitutions. @@ -23,11 +25,14 @@ public class UnificationStep { * * @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) + * @param processedConstraint the constraint processed in this step, if any */ protected UnificationStep(Result, UnificationError> substitutions, - List constraints) { + List constraints, + Optional processedConstraint) { this.substitutions = substitutions; this.constraints = constraints; + this.processedConstraint = processedConstraint; } /** @@ -50,11 +55,19 @@ public class UnificationStep { return constraints; } + /** + * @return the constraint processed in this step + */ + public Optional getProcessedConstraint() { + return processedConstraint; + } + @Override public String toString() { return "UnificationStep{" + "substitutions=" + substitutions + ", constraints=" + Arrays.toString(constraints.toArray()) + + ", processed=" + processedConstraint + '}'; } @@ -67,7 +80,8 @@ public class UnificationStep { return false; } UnificationStep that = (UnificationStep) o; - return substitutions.equals(that.substitutions) && constraints.equals(that.constraints); + return substitutions.equals(that.substitutions) && constraints.equals(that.constraints) + && processedConstraint.equals(that.processedConstraint); } @Override diff --git a/src/main/java/edu/kit/typicalc/view/TypicalcI18NProvider.java b/src/main/java/edu/kit/typicalc/view/TypicalcI18NProvider.java index 98b36ef..15dc6a8 100644 --- a/src/main/java/edu/kit/typicalc/view/TypicalcI18NProvider.java +++ b/src/main/java/edu/kit/typicalc/view/TypicalcI18NProvider.java @@ -52,9 +52,9 @@ public class TypicalcI18NProvider implements I18NProvider { return "?[" + key + "]?"; } } - // replace placeholders {0} ... + // replace placeholders %0% ... for (int i = 0; i < params.length; i++) { - result = result.replace(String.format("{%d}", i), params[i].toString()); + result = result.replace(String.format("%%%d%%", i), params[i].toString()); } return result; } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java index 8ae53ca..c6c469b 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java @@ -40,8 +40,8 @@ import edu.kit.typicalc.util.Result; public class ExplanationCreatorUnification { private static final String KEY_PREFIX = "expUnification."; - private static final String LET_KEY_PREFIX = "expLetUnification."; - + private static final String LET_KEY_PREFIX = "expLetUnification."; + private final TypeArgumentVisitor typeDeterminer = new TypeArgumentVisitor(); private final TypeInfererInterface typeInferer; private final Locale locale; @@ -88,6 +88,7 @@ public class ExplanationCreatorUnification { typeAssumptionsToLatex(typeInferer.getFirstInferenceStep().getConclusion().getTypeAssumptions(), mode); String letVariableLatex = new LatexCreatorTerm(this.letVariable.get(), mode).getLatex(); + // TODO: replace with parametrized translation text (see createVariableText) StringBuilder latex = new StringBuilder(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss1")). append(toLatex(GAMMA)). append(getDefaultTextLatex(LET_KEY_PREFIX + "typeAss2")). @@ -128,6 +129,7 @@ public class ExplanationCreatorUnification { private void createFinalType(boolean isLetUnification) { String keyPrefix = isLetUnification ? LET_KEY_PREFIX : KEY_PREFIX; + // TODO: replace with parametrized translation text (see createVariableText) StringBuilder latex = new StringBuilder(getDefaultTextLatex(keyPrefix + "finalType1")). append(toLatex(letCounterToLatex(SIGMA))). append(getDefaultTextLatex(keyPrefix + "finalType2")). @@ -183,11 +185,10 @@ public class ExplanationCreatorUnification { List unificationSteps = typeInferer.getUnificationSteps() .orElseThrow(IllegalStateException::new); - List initialConstraints = unificationSteps.get(0).getConstraints(); // skip first step since the substitutions list is still empty (unification introduction is shown) - Constraint currentConstraint = initialConstraints.get(initialConstraints.size() - 1); - for (int stepNum = 1; stepNum < unificationSteps.size() - 1; stepNum++) { + for (int stepNum = 1; stepNum < unificationSteps.size(); stepNum++) { UnificationStep step = unificationSteps.get(stepNum); + Constraint currentConstraint = step.getProcessedConstraint().get(); // works because only step 0 has no constraint Result, UnificationError> subs = step.getSubstitutions(); if (subs.isError()) { @@ -195,6 +196,7 @@ public class ExplanationCreatorUnification { errorOccurred = true; break; } + List substitutions = subs.unwrap(); List constraints = step.getConstraints(); if (currentConstraint.getFirstType().equals(currentConstraint.getSecondType())) { @@ -203,23 +205,22 @@ public class ExplanationCreatorUnification { } else if (typeDeterminer.getArguments(currentConstraint.getFirstType()).isEmpty()) { // left side is a variable createVariableText(currentConstraint.getFirstType(), currentConstraint.getSecondType(), - currentConstraint, subs.unwrap().get(0)); + currentConstraint, substitutions.get(substitutions.size() - 1)); } else if (typeDeterminer.getArguments(currentConstraint.getSecondType()).isEmpty()) { // right side is a variable createVariableText(currentConstraint.getSecondType(), currentConstraint.getFirstType(), - currentConstraint, subs.unwrap().get(0)); + currentConstraint, substitutions.get(substitutions.size() - 1)); } else { // both sides are functions createFunctionText(currentConstraint, constraints.get(constraints.size() - 1), constraints.get(constraints.size() - 2)); } - - currentConstraint = constraints.get(constraints.size() - 1); } } - + private void createTrivialConstraintText(Constraint currentConstraint) { StringBuilder latex = new StringBuilder(); + // TODO: replace with parametrized translation text (see createVariableText) latex.append(getDefaultTextLatex(KEY_PREFIX + "trivial1")). append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))). append(getDefaultTextLatex(KEY_PREFIX + "trivial2")); @@ -228,6 +229,7 @@ public class ExplanationCreatorUnification { private void createFunctionText(Constraint currentConstraint, Constraint newConstraint1, Constraint newConstraint2) { StringBuilder latex = new StringBuilder(); + // TODO: replace with parametrized translation text (see createVariableText) latex.append(getDefaultTextLatex(KEY_PREFIX + "function1")). append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))). append(getDefaultTextLatex(KEY_PREFIX + "function2")). @@ -246,19 +248,13 @@ public class ExplanationCreatorUnification { private void createVariableText(Type variable, Type anyType, Constraint currentConstraint, Substitution newSubstitution) { - StringBuilder latex = new StringBuilder(); - latex.append(getDefaultTextLatex(KEY_PREFIX + "variable1")). - append(toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode))). - append(getDefaultTextLatex(KEY_PREFIX + "variable2")). - append(toLatex(new LatexCreatorType(variable, mode).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "variable3")). - append(toLatex(new LatexCreatorType(variable, mode).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "variable4")). - append(toLatex(new LatexCreatorType(anyType, mode).getLatex())). - append(getDefaultTextLatex(KEY_PREFIX + "variable5")). - append(toLatex(getSubstitutionLatex(newSubstitution))). - append(getDefaultTextLatex(KEY_PREFIX + "variable6")); - unificationTexts.add(latex.toString()); + String constraintLatex = toLatex(LatexCreatorConstraints.createSingleConstraint(currentConstraint, mode)); + String variableType = toLatex(new LatexCreatorType(variable, mode).getLatex()); + String otherType = toLatex(new LatexCreatorType(anyType, mode).getLatex()); + String substitutionLatex = toLatex(getSubstitutionLatex(newSubstitution)); + String finalText = provider.getTranslation(KEY_PREFIX + "variable", locale, + constraintLatex, variableType, otherType, substitutionLatex); + unificationTexts.add(finalText); } private void createErrorText(UnificationError errorType) { diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationTranslationProvider.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationTranslationProvider.java new file mode 100644 index 0000000..48aa5ba --- /dev/null +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationTranslationProvider.java @@ -0,0 +1,28 @@ +package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator; + +import com.vaadin.flow.i18n.I18NProvider; + +import java.util.List; +import java.util.Locale; + +public class ExplanationTranslationProvider implements I18NProvider { + private final I18NProvider innerProvider; + + public ExplanationTranslationProvider(I18NProvider provider) { + this.innerProvider = provider; + } + + @Override + public List getProvidedLocales() { + return innerProvider.getProvidedLocales(); + } + + @Override + public String getTranslation(String key, Locale locale, Object... params) { + return innerProvider.getTranslation(key, locale, params); + } + + public String getTranslationInstantiated(String key, Locale locale, Object... params) { + return ""; + } +} diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties index bb588a5..eb34b66 100644 --- a/src/main/resources/language/translation_de.properties +++ b/src/main/resources/language/translation_de.properties @@ -109,8 +109,8 @@ error.heading=Syntaktisch falsche Eingabe! error.termForError=Term:\u0020 error.typeAssumptionForError=Typannahme:\u0020 error.wrongCharacter=Falsches Zeichen:\u0020 -error.expectedToken=Erwartet: {0} -error.additionalInformation = Information: {0} +error.expectedToken=Erwartet: %0% +error.additionalInformation = Information: %0% error.hint=Die Grammatiken, die die korrekte Syntax eines Terms und der Typannahmen beschreiben, \ sind auch über das Info-Symbol zu erreichen. tokentype.UNIVERSAL_QUANTIFIER=Allquantor @@ -252,13 +252,10 @@ ausgeführt, um den Typen der let-Variable zu finden und damit die neue Typumgeb expUnification.trivial1=In diesem Schritt wurde der Constraint expUnification.trivial2=entfernt. Da linke und rechte Seite identisch sind, ist der Constraint immer erfüllt und \ wird somit nicht benötigt. -expUnification.variable1=In diesem Schritt wurde der Constraint -expUnification.variable2=ersetzt. Da t ein Variablentyp ist und nicht in -expUnification.variable3=vorkommt, können alle Vorkommen von -expUnification.variable4=durch -expUnification.variable5=ersetzt werden. In der Folge wird die Substitution -expUnification.variable6=erstellt und auf die übrige Constraintmenge angewandt. Die daraus resultierenden Veräderungen \ -sind blau markiert. +expUnification.variable=In diesem Schritt wurde der Constraint %0% ersetzt.\ + Da %1% ein Variablentyp ist und nicht in %2% vorkommt, können alle Vorkommen von %1% durch %2% ersetzt werden.\ + In der Folge wird die Substitution %3% erstellt und auf die übrige Constraintmenge angewandt.\ + Die daraus resultierenden Veränderungen sind blau markiert. expUnification.function1=In diesem Schritt wurde der Constraint expUnification.function2=ersetzt. Da sowohl expUnification.function3=als auch diff --git a/src/main/resources/language/translation_en.properties b/src/main/resources/language/translation_en.properties index 904a8e2..63efb42 100644 --- a/src/main/resources/language/translation_en.properties +++ b/src/main/resources/language/translation_en.properties @@ -101,8 +101,8 @@ error.heading=Input is syntactically wrong! error.wrongCharacter=Wrong character:\u0020 error.termForError=Term:\u0020 error.typeAssumptionForError=Type assumption:\u0020 -error.expectedToken=Expected: {0} -error.additionalInformation = Information: {0} +error.expectedToken=Expected: %0% +error.additionalInformation = Information: %0% error.hint=The grammars describing the correct syntax of a term or a type assumption can also be reached \ via the info icon. tokentype.UNIVERSAL_QUANTIFIER=universal quantifier diff --git a/src/test/java/edu/kit/typicalc/model/UnificationTest.java b/src/test/java/edu/kit/typicalc/model/UnificationTest.java index de06a61..43b7e1a 100644 --- a/src/test/java/edu/kit/typicalc/model/UnificationTest.java +++ b/src/test/java/edu/kit/typicalc/model/UnificationTest.java @@ -7,10 +7,7 @@ import edu.kit.typicalc.util.Result; import nl.jqno.equalsverifier.EqualsVerifier; import org.junit.jupiter.api.Test; -import java.util.ArrayDeque; -import java.util.ArrayList; -import java.util.Deque; -import java.util.List; +import java.util.*; import static org.junit.jupiter.api.Assertions.assertEquals; @@ -32,11 +29,11 @@ class UnificationTest { List steps = u.getUnificationSteps(); assertEquals(2, steps.size()); assertEquals(new UnificationStep(new Result<>(new ArrayList<>()), - new ArrayList<>(initialConstraints)), steps.get(0)); + new ArrayList<>(initialConstraints), Optional.empty()), steps.get(0)); List substitutions = new ArrayList<>(List.of(new Substitution(a, new FunctionType(b, c)))); assertEquals(new UnificationStep(new Result<>( substitutions - ), new ArrayList<>()), steps.get(1)); + ), new ArrayList<>(), Optional.of(constraints.getFirst())), steps.get(1)); assertEquals(substitutions, u.getSubstitutions().unwrap()); } @@ -54,39 +51,39 @@ class UnificationTest { List steps = u.getUnificationSteps(); assertEquals(6, steps.size()); assertEquals(new UnificationStep(new Result<>(new ArrayList<>()), - new ArrayList<>(initialConstraints)), steps.get(0)); + new ArrayList<>(initialConstraints), Optional.empty()), steps.get(0)); - initialConstraints.removeFirst(); + var constraint = initialConstraints.removeFirst(); List substitutions = new ArrayList<>(List.of(new Substitution(a, new FunctionType(b, c)))); assertEquals(new UnificationStep(new Result<>( substitutions - ), new ArrayList<>(initialConstraints)), steps.get(1)); + ), new ArrayList<>(initialConstraints), Optional.of(constraint)), steps.get(1)); - initialConstraints.removeFirst(); + constraint = initialConstraints.removeFirst(); substitutions.add(new Substitution(c, new FunctionType(a4, a5))); assertEquals(new UnificationStep(new Result<>( substitutions - ), new ArrayList<>(initialConstraints)), steps.get(2)); + ), new ArrayList<>(initialConstraints), Optional.of(constraint)), steps.get(2)); - initialConstraints.removeFirst(); + constraint = initialConstraints.removeFirst(); initialConstraints.removeFirst(); initialConstraints.addFirst(new Constraint(new FunctionType(a7, a5), a4)); substitutions.add(new Substitution(a6, new FunctionType(a7, a5))); assertEquals(new UnificationStep(new Result<>( substitutions - ), new ArrayList<>(initialConstraints)), steps.get(3)); + ), new ArrayList<>(initialConstraints), Optional.of(constraint)), steps.get(3)); - initialConstraints.removeFirst(); + constraint = initialConstraints.removeFirst(); substitutions.add(new Substitution(a4, new FunctionType(a7, a5))); assertEquals(new UnificationStep(new Result<>( substitutions - ), new ArrayList<>(initialConstraints)), steps.get(4)); + ), new ArrayList<>(initialConstraints), Optional.of(constraint)), steps.get(4)); - initialConstraints.removeFirst(); + constraint = initialConstraints.removeFirst(); substitutions.add(new Substitution(a7, b)); assertEquals(new UnificationStep(new Result<>( substitutions - ), new ArrayList<>(initialConstraints)), steps.get(5)); + ), new ArrayList<>(initialConstraints), Optional.of(constraint)), steps.get(5)); assertEquals(substitutions, u.getSubstitutions().unwrap()); } @@ -100,10 +97,10 @@ class UnificationTest { List steps = u.getUnificationSteps(); assertEquals(2, steps.size()); assertEquals(new UnificationStep(new Result<>(new ArrayList<>()), - new ArrayList<>(initialConstraints)), steps.get(0)); + new ArrayList<>(initialConstraints), Optional.empty()), steps.get(0)); assertEquals(new UnificationStep(new Result<>(null, UnificationError.INFINITE_TYPE - ), new ArrayList<>()), steps.get(1)); + ), new ArrayList<>(), Optional.of(initialConstraints.getFirst())), steps.get(1)); } @Test diff --git a/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorTest.java b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorTest.java new file mode 100644 index 0000000..b5925f2 --- /dev/null +++ b/src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorTest.java @@ -0,0 +1,16 @@ +package edu.kit.typicalc.view.content.typeinferencecontent.latexcreator; + +import edu.kit.typicalc.model.Model; +import edu.kit.typicalc.model.ModelImpl; +import edu.kit.typicalc.model.TypeInfererInterface; +import org.junit.jupiter.api.Test; + +import java.util.Locale; + +public class ExplanationCreatorTest { + @Test + void itWorks() { + TypeInfererInterface model = new ModelImpl().getTypeInferer("λx.x", "").unwrap(); + new ExplanationCreator(model, Locale.GERMAN).getExplanationTexts(); + } +}