arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-09-18 17:55:14 +00:00
Code Issues Packages Projects Releases Wiki Activity

Fix some bugs of the unification explanation

Browse Source 
see #20
This commit is contained in:
Arne Keller 2021-08-16 09:50:43 +02:00
parent 208c21277b
commit 7abfd66aa8
10 changed files with 111 additions and 60 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
frontend/styles/view/type-inference.css
View File

@ -43,6 +43,7 @@ tc-explanation {
max-width: 40em;
padding-left: 1em;
padding-right: 1em;
overflow-y: auto;
}
#rules-button {

8
src/main/java/edu/kit/typicalc/model/Unification.java
View File

@ -24,7 +24,8 @@ public class Unification {
steps = new ArrayList<>();
List<Substitution> 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<UnificationActions, UnificationError> 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);

18
src/main/java/edu/kit/typicalc/model/UnificationStep.java
View File

@ -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<List<Substitution>, UnificationError> substitutions;
private final List<Constraint> constraints;
private final Optional<Constraint> 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<List<Substitution>, UnificationError> substitutions,
List<Constraint> constraints) {
List<Constraint> constraints,
Optional<Constraint> 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<Constraint> 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

4
src/main/java/edu/kit/typicalc/view/TypicalcI18NProvider.java
View File

@ -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;
}

42
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorUnification.java
View File

@ -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<UnificationStep> unificationSteps = typeInferer.getUnificationSteps()
.orElseThrow(IllegalStateException::new);
List<Constraint> 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<List<Substitution>, UnificationError> subs = step.getSubstitutions();
if (subs.isError()) {
@ -195,6 +196,7 @@ public class ExplanationCreatorUnification {
errorOccurred = true;
break;
}
List<Substitution> substitutions = subs.unwrap();
List<Constraint> 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) {

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

@ -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<Locale> 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 "";
}
}

15
src/main/resources/language/translation_de.properties
View File

@ -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

4
src/main/resources/language/translation_en.properties
View File

@ -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

35
src/test/java/edu/kit/typicalc/model/UnificationTest.java
View File

@ -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<UnificationStep> 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<Substitution> 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<UnificationStep> 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<Substitution> 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<UnificationStep> 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

16
src/test/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ExplanationCreatorTest.java Normal file
View File

@ -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();
}
}