Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 109)
+++ /reasoner/reasoner.tex	(revision 110)
@@ -225,5 +225,6 @@
 As part of the constraint instantiation, variables must be replaced. Let $c=\createConstraint{\IVML{assign(x, 25)}}$ be a constraint and \IVML{y} be some IVML variable. Then $\varSubstitution{c}{x = y}$ leads to the substitution of all variables named \IVML{x} by \IVML{x}, i.e., for the example effectively to \IVML{y = 25}. If such substitutions are stored in a mapping, i.e., a $\variableMapping=\set{\mapEntry{e_s, e_t}}$ with $e_s$ being the expression to be replaced and $e_t$ the replacing expression, we can apply this mapping to a constraint $c$ using $\varSubstitutionVarMapping{c}$. Moreover, we can combine a specific mapping and already stored mappings using $\varSubstitutionOtherVarMapping{c}{x = y}$. Please note that such substitutions are transitive, i.e., if $\mapEntry{y}{z}\in \variableMapping$, $x$ will be replaced by $z$. If the right side of a substitution is $\undef$, no substitution happens, e.g., in $\varSubstitution{c}{x = \undef}$. As usual in IVML, we denote the creation of collection operations using the arrow and iterator notation. As we use the '$|$' symbol for variable substitutions, using the same symbol in some transformations in IVML quantor expressions would be confusing. Thus, we use in this document the respective syntax parts ':' as introduced for sets in Section \ref{sectGeneralNotation} instead of the syntactically correct '$|$', e.g., \IVML{forall(x:c(x))} instead of the correct IVML notation \IVML{forall(x|c(x))}. Let $c$ be an IVML collection of Integers, then \IVML{c->forall(i:i>20);} requires that all values in $c$ are greater than 20. To create such a constraint with $c$ being an algorithm variable, we denote $\createConstraint{c\IVML{->forall(i:i>20)}}$. 
 
-For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate this information as a `$d$' in the constraint creation notation, e.g., for creating a default constraint, we denote $b \assng \createDefaultConstraint{\IVML{assign}(x, 25)}$ for which $\isDefaultConstraint{b} = true$ holds. Similarly, we denote creating a constraint originating from a constraint variable by `$c$', e.g., $b \assng \createConstraintConstraint{\IVML{assign}(x, 25)}$ for which $\isConstraintConstraint{b} = true$ holds.
+For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate this information as a `$d$' in the constraint creation notation, e.g., for creating a default constraint, we denote $b \assng \createDefaultConstraint{\IVML{assign}(x, 25)}$ for which $\isDefaultConstraint{b} = true$ holds. Further, we allow attaching information to a constraint, e.g., the type it was created for. Let $c = attach(c, t)$ be an operation that attaches $t$ to constraint $c$ (and returns $c$) as well as $t = attached(c)$ return the respective attachment.
+%Similarly, we denote creating a constraint originating from a constraint variable by `$c$', e.g., $b \assng \createConstraintConstraint{\IVML{assign}(x, 25)}$ for which $\isConstraintConstraint{b} = true$ holds.
 
 In some cases, expressions used to build up a constraint are created before the actual constraint and stored in structures for lookup. We denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for calculating the sum of $x$ and 25. A specific type of expression is the constant, which holds an IVML value. The operation $const(e)$ returns the value of $e$ if $e$ is a constant expression or $\undef$ otherwise. When creating expressions, sometimes a temporary (local) variable is needed, e.g., for an IVML let-expression or a container iterator. We state this by $\IVMLMeta{var}(t)$, i.e., create the temporary variable of type $t$ (we don't care for the name of the variable here). For a variable $v=\IVMLMeta{var}(t)$ holds $isLocal(v) = true$. 
@@ -453,6 +454,6 @@
     \item $setTypeExcludes(\variableMapping, s)$ defines a set of types to be marked as excluded from constraint transformations. Excluding types is important for a fast processing of re-scheduled constraints in Section \ref{sectTopLevelConstraintsRescheduling}.
     \item $transferTypeExcludes(\variableMapping, t)$ transfers excluded types into this context and stores the causing type $t$ in the current context. Transferring excluded types binds them to the actual (usual top-most) type rather and avoids applying them some nested type.
-    \item $getCurrentType(\variableMapping)$ returns the type $t$ stored in the current contect by $transferTypeExcludes(\variableMapping, t)$. The result is $\undef$ if no transfer happend on the current context.
-    \item $isTypeExcluded(t)$ returns whether $t$ is excluded in the current context.
+    \item $currentType(\variableMapping)$ returns the type $t$ stored in the current contect by $transferTypeExcludes(\variableMapping, t)$. The result is $\undef$ if no transfer happend on the current context.
+    \item $isTypeExcluded(\variableMapping, t)$ returns whether $t$ is excluded in the current context and $excludedTypes(\variableMapping)$ returns all excluded types for the current context or an empty set.
     \item $size(\variableMapping)$ the number of contexts on the stack. There is at least always one context on the stack representing the containing project.
     \item $clear(\variableMapping)$ clears the stack and cleans up the default context frame dedicated to the IVML project so that $\variableMapping$ is ready for the translation of the next IVML project.
@@ -713,5 +714,5 @@
         $registerMapping(\variableMapping, s, x)$\;
         \ForAll{$a \iterAssng annotations(s)$}{
-          $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t, a), &\text{else}}}$\; \label{algRegisterCompoundMappingAnnotationMapping}
+          $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), a), &\text{else}}}$\; \label{algRegisterCompoundMappingAnnotationMapping}
           $registerMapping(\variableMapping, a, x)$\;
         }
@@ -745,8 +746,8 @@
   }
   \leIf{$ca \neq \undef$}{$f\assng ca$}{$f\assng d$}\label{algTranslateCompoundDeclarationSelf}
-  $eval \assng \setWithFlat{allEvalConstraints(r)}{r\in allRefines^+(t)}$\;\label{algTranslateCompoundDeclarationEvalStart}
-  $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{c}{f}}}{c\in eval}, true)$\;\label{algTranslateCompoundDeclarationEvalEnd}
-  $cmp \assng \setWithFlat{allCompoundConstraints(r)}{r\in allRefines^+(t)}$\;\label{algTranslateCompoundDeclarationAllStart}
-  $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{c}{f}}}{c\in cmp}, true)$\;\label{algTranslateCompoundDeclarationAllEnd}
+  $eval \assng \setWithFlat{allEvalConstraints(r)}{r\in allRefines^+(t) \text{ } \setminus \text{ } excludedTypes(t)}$\;\label{algTranslateCompoundDeclarationEvalStart}
+  $add(\otherConstraints, \setWith{attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{f}}, currentType(\variableMapping))}{c\in eval}, true)$\;\label{algTranslateCompoundDeclarationEvalEnd}
+  $cmp \assng \setWithFlat{allCompoundConstraints(r)}{r\in allRefines^+(t) \text{ } \setminus \text{ } excludedTypes(t)}$\;\label{algTranslateCompoundDeclarationAllStart}
+  $add(\otherConstraints, \setWith{attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{f}}, currentType(\variableMapping))}{c\in cmp}, true)$\;\label{algTranslateCompoundDeclarationAllEnd}
 
  \caption{Translating compound content (\IVML{translateCompoundContent}).}\label{algTranslateCompoundContent}