Index: /reasoner/consTranslation.tex
===================================================================
--- /reasoner/consTranslation.tex	(revision 144)
+++ /reasoner/consTranslation.tex	(revision 145)
@@ -119,7 +119,11 @@
 }
 
-The first pattern indicates that an IVML compound type $C$ with declared slot $s$ and contained constraint $c(s)$ over slot $s$. The translation is applied if a variable $v$ of type $T$, i.e., a concrete instance of a compound type is declared and, however, receives a value. In this case, each contained constraint is instantiated by qualifying all relevant variable occurrences, i.e., replacing \IVML{self} with the actual variable $v$, the slot $s$ with the respective qualified access $v.s$ as well as all other known variable mappings, in particular including qualified access expression known for other slots in $C$. More complex access expressions also allow for translating nested compounds. The second case indicates a top-level constraint defined over the compound variable $v$. In contrast, this translation can happen as part of translating all top-level constraints, as due to the use of only qualified slot access expressions, just the (top-level) variable mapping is relevant for the substitution. The patterns show, that in both cases, the respective variable mapping including top-level and type-level cross-reference accesses must be created before the respective translation (including annotations, to handle constraints on annotations similarly). However, compounds may contain assignment and eval blocks. Assignment blocks are discussed in Section \ref{sectAnnotationDefaults}, but mainly differ in the treatment of the default value assignments rather than the contained constraints. Constraints in eval blocks can be transformed as shown by the patterns, but require different constraint evaluation priority. Moreover, compound instances may occur in containers, which we will discuss in more detail in Section \ref{sectContainerDefaults}. We will now focus on the first pattern and discuss the respective translation Algorithm \ref{algTranslateCompoundDeclaration}.
-
-For slots and annotations we can resort to Algorithm \ref{algTranslateDeclaration}, i.e., compound types, derived types, constraint variables and collections, while for the remaining constraints, we must visit these structures, instantiate and collect the respective constraints. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. In particular, if the IVML keyword \IVMLself{} is used within a constraint, it must be substituted by the actual variable of the respective compound type. Moreover, it is important to recall that a variable $v$ of type $type(v)$ can contain instances of any refined type $allRefines^+(t)$, and in this case the translation must consider the default values of the potentially larger slot, additional constraints and nested structures.
+The first pattern requires an IVML compound type $C$ with declared slot $s$ and contained constraint $c(s)$ over slot $s$. The translation is applied if a variable $v$ of type $C$, i.e., a concrete instance of a compound type is declared. A contained constraint is instantiated by qualifying all compound-scoped variable occurrences, i.e., by replacing \IVML{self} with the actual variable $v$, the slot $s$ with the respective qualified access $v.s$ as well as all other known variable mappings including remaining slots. Thus, the variable mapping for a compound must be created before any slot is translated. 
+
+Annotation assignments are translated similarly, but require specific handling of default values as we will discuss in Section \ref{sectAnnotationDefaults}. Eval blocks are also translated similarly, but the resulting constraints require a higher constraint evaluation priority in the actual scope as we will detail below. Nested compounds are implicitly considered through the $access$ function, i.e., by respective access prefix expressions. Moreover, compound instances and, thus, constraints induced by compound types, may occur in containers. In Section \ref{sectContainerDefaults}, we will discuss the translations of containers, which recursively utilizes the translation of variables, i.e., Algorithm \ref{algTranslateDeclaration} and, thus, of compound types.
+
+The second pattern transforms a top-level constraint defined over a compound variable $v$. Due to the mandatory use of only qualified slot access expressions in IVML, no translation is needed and such constraints are handled through line \ref{algTranslateConstraintsTopLevelConstraints} in Algorithm \ref{algTranslateConstraints}. 
+
+We will now focus on the first pattern and discuss the respective translation Algorithm \ref{algTranslateCompoundDeclaration}. For slots and annotations we can resort to Algorithm \ref{algTranslateDeclaration}, i.e., compound types, derived types, constraint variables and collections, while for the remaining constraints, we must visit these structures, instantiate and collect the respective constraints. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. In particular, if the IVML keyword \IVMLself{} is used within a constraint, it must be substituted by the actual variable of the respective compound type. Moreover, it is important to recall that a variable $v$ of type $type(v)$ can contain instances of any refined type $allRefines^+(t)$, and in this case the translation must consider the default values of the potentially larger slot, additional constraints and nested structures.
 
 Algorithm \ref{algTranslateCompoundDeclaration} collects and translates the constraints for a compound variable $v$ with declaration $d$, potential compound accessor $ca$ and (default value) type (or $type(d)$ if no default expression is defined for $d$). No translation happens if type $t$ was already processed, e.g., in case of recursive compound types. The types are related by $type(d) = type(v) \in allRefines^+(t)$. Algorithm \ref{algTranslateCompoundDeclaration} creates a context frame and pushes it onto the variable mapping stack $\variableMapping$\footnote{For optimizing constraint rescheduling (see Section \ref{sectTopLevelConstraintsRescheduling}), the algorithm applies type exclusions to the actual context by transferring them and storing the causing type $t$ in the current context}. Used types are registered only if there is no variable $v$ given, e.g., we process constraints according to a potentially recursive type structure. If a variable $v$ is given, the nested variables are initialized correctly, in particular recursively nested variables terminate correctly based on configured values, i.e., we do not have to take care of recursion in this case.