Explanation texts english

src/main/resources/language/translation_de.properties

@@ -214,9 +214,8 @@ explanationTree.constStep=Der aktuelle Term %0% ist eine Konstante. Daher wird i
 die Konstante %0% vom Typ %1% angewendet. Da %0% ein %2%-Wert ist, wird die Bedingung %3% der Constraintmenge hinzugefügt.
 explanationTree.letStep=Da der aktuelle Term %0% ein Let-Ausdruck vom Typ %1% mit Variable %2%, Definition %3% \
 und innerem Term %4% ist, wird in diesem Schritt die Let-Regel angewendet. Dafür wird im linken Teilbaum eine neue \
-Typinferenz mit dem Term %3% gestartet. Mit dem Ergebnis der Let-Teilinferenz lässt sich anschließend der Typ der Variable \
+Typinferenz mit dem Term %3% gestartet. Da der Let-Ausdruck und der innere Term vom gleichen Typ sein müssen, wird außerdem \
-%2% bestimmen. Da der Let-Ausdruck und der innere Term vom gleichen Typ sind, muss außerdem die \
+die Bedingung %5% der Constraintmenge hinzugefügt werden.
-Bedingung %5% der Constraintmenge hinzugefügt werden.
 expUnification.initial=In den folgenden Schritten wird der Unifikationsalgorithmus auf der Constraintmenge %0% ausgeführt, \
  um den Typen des eingegebenen Terms zu bestimmen.
 expLetUnification.initial=In den folgenden Schritten wird der Unifikationsalgorithmus auf der Constraintmenge %0% \
@@ -244,7 +243,6 @@ expLetUnification.typeAss=In diesem Schritt werden die Typannahmen %0% für die
  berechnet. Im ersten Schritt wird dafür %1% auf die aktuelle Menge von Typannahmen angewandt. Die dadurch entstandenen \
  Typannahmen werden anschließend der Menge %0% hinzugefügt. Im zweiten Schritt wird der Typ der let-Variable %2% berechnet\
  . Dafür wird die Typabstraktion %3% zuerst instanziiert und dann gemeinsam mit der Variable %2% als Typannahme der Menge \
- %0% hinzugefügt. Bei der Instanziierung werden alle Typvariablen, die frei in %4% aber nicht frei in %5% vorkommen \
+ %0% hinzugefügt.
- allquantifiziert.
 expLetUnification.letStep=Die Let-Teilinferenz ist jetzt abgeschlossen. Der Typinferenz-Algorithmus wird mit der um %0% \
  erweiterten Constraintmenge und den neu berechneten Typannahmen fortgeführt.

src/main/resources/language/translation_en.properties

@@ -185,3 +185,49 @@ share.packagesTree.label=Packages (inference tree)
 share.latexTree.label=LaTeX code (whole inference tree)
 share.packagesUnification.label=Packages (unification/MGU)
 share.latexUnification.label=LaTeX code (current step in unifcation/MGU)
+
+explanationTree.initial=At the beginning of the algorithm the type variable %1% is assigned to the input %0%. \
+ In the following steps the type of %1% will be determined gradually.
+explanationTree.varStep=The current expression %0% is a variable. Therefore the var rule is applied to the variable \
+ %0% of type %1%. Since %0% is of type %2% under the given type assumptions, the constraint %3% is added to the set \
+ of constraints.
+explanationTree.absStep=Since the current expression %0% is an abstraction of type %1% with parameter %2% and result %3%, \
+ the abs rule is applied in this step. To do this, the parameter is assigned type %4% and the result is assigned type %5%. \
+ Therefore the abstraction is of type %6% and the constraint %7% has to be added to the set of constraints.
+explanationTree.appStep=Since the current expression %0% is an application of type %1% with function %2% and argument %3% \
+ the app rule is applied in this step. To do this, the function is assigned type %4% and the argument is assigned type \
+ %5%. Therefore the function is of the type %6% and the constraint %7% has to be added to the set of constraints.
+explanationTree.constStep=The current expression %0% is a constant. Therefore the const rule is applied to the constant \
+ %0% of type %1%. Since the value of %0% is %2%, the constraint %3% is added to the set of constraints.
+explanationTree.letStep=Since the current expression %0% is a let-expression of type %1% with variable %2%, definition %3% \
+ and inner term %4%, the let rule is applied in this step. To do this, a new type inference with expression %3% is started \
+ in the left subtree. As the let-expression and the inner term have to be of the same type, the constraint %5% is added to \
+ the set of constraints.
+expUnification.initial=In the following steps the unfication algorithm will be executed on the set of constraints %0% to \
+ determine the type of the initial input.
+expLetUnification.initial=In the following steps the unfication algorithm will be executed on the set of constraints %0% \
+ to determine the type of the let-variable %1%.
+expUnification.trivial=In this step the constraint %0% has been removed. Since the left and right side of the constraint \
+ are identical, the constraint is always fulfilled and hence is of no use.
+expUnification.variable=In this step the constraint %0% has been replaced. Since %1% is a variable type and does not appear \
+ in %2%, all other appearances of %1% can be replaced by %2%. To do this, the substitution %3% is created and is applied to \
+ the remaining set of constraints. All changes of the set are highlighted in blue.
+expUnification.function=In this step the constraint %0% has been replaced. Since %1% as well as %2% are function types, \
+ the constraints %3% and %4% have to be added to the set of constraints. The original constraint %0% has been removed from \
+ the set.
+expUnification.mgu=In this step the most general unifier %0% for the set of constraints %1% is calculated. Therefore the \
+ whole set of substitutions is applied to every single substitution of the set.
+expUnification.finalType=In this step the most general unifier %0% is applied to the type %1% of the input. The result %2% \
+ is the final type of the input.
+expUnification.infiniteType=The same type variable appears on both sides of the constraint. Since this would cause an \
+ infinite type, the execution of the unification is stopped.
+expUnification.differentTypes=Since the types on both sides of the constraint are incompatible, the execution of the \
+ unification is stopped.
+expLetUnification.finalType=In this step the most general unifier %0% is applied to the type %1% of the let-definition. \
+ The result %2% is the final type of the let-definition.
+expLetUnification.typeAss=In this step the type assumptions %0% for the further execution of the algorithm are \
+ calculated. To do this, %1% is applied to the current set of type assumptions. The resulting new type assumptions are \
+ added to the set %0%. Afterwards the type of the let-variable %2% is calculated. Therefore the type assumption is \
+ instantiated and then added to the set %0% as a type assumption with variable %2%.
+expLetUnification.letStep=The let-inference is now finished. The execution of the algorithm continues with the newly \
+ calculated type assumptions and the old set of constraints extended by the set %0%.