Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 205) +++ /reasoner/consTranslation.tex (revision 206) @@ -120,8 +120,8 @@ \grayPara{ \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s = deflt\IVML{;\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{s = deflt}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundDefault} - \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; } \constraintWith{c}{s}\IVML{\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}} - \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; eval \{} \constraintWith{c}{s}\IVML{\}\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}} - \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; assign (\ldots) to \{} \constraintWith{c}{s}\IVML{\}\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}} - \patternDerivation{\IVML{compound } C \IVML{\{} T s \IVML{\}; } C\ v \IVML{; } \constraintWith{c}{v.s}\IVML{;}}{\varSubstitution{\constraintWith{c}{v.s}}{\variableMapping}} + \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s\IVML{; } \constraintWith{c}{s}\IVML{\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundSlot} + \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s\IVML{; eval \{} \constraintWith{c}{s}\IVML{\}\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundEval} + \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s\IVML{; assign (\ldots) to \{} \constraintWith{c}{s}\IVML{\}\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundAssign} + \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s \IVML{\}; } C\ v \IVML{; } \constraintWith{c}{v.s}\IVML{;}}{\varSubstitution{\constraintWith{c}{v.s}}{\variableMapping}}{forCompoundAssign} } @@ -132,13 +132,15 @@ \item \emph{Compound slot with default value expression:} The default value is instantiated into a default value assignment constraint as shown in Pattern \ref{forCompoundDefault}. When translating a top-level compound variable $v$, the actual value for \IVMLself{} is determined by $access(v)$ and the accessor for slot $s$ by $access(v.s)$. For nested slots of compound types, Algorithm \ref{algTranslateDeclaration} is called recursively with the respective access expression. - \item \emph{Constraint $\constraintWith{c}{s}$ defined on compound slot $s$:} For a compound variable $v$ of type $C$, contained constraints are instantiated by qualifying all compound-scoped variable occurrences, i.e., by replacing \IVMLself{} 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. 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. - - \item \emph{Eval blocks:} Here nesting becomes transparent and constraints are translated as if they were defined directly in the containing compound type, i.e., according to the second pattern. However, eval blocks require a higher constraint evaluation priority in the compound scope as we will detail below. - - \item \emph{Annotation assignments: } Also here the nesting becomes transparent and constraints are translated as if they were defined directly in the containing compound type, i.e., similar to the second pattern. However, annotation assignments require specific handling of default values to avoid accidental re-assignment of default values as we will discuss in Section \ref{sectAnnotationDefaults}. - - \item \emph{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}. + \item \emph{Constraint $\constraintWith{c}{s}$ defined on compound slot $s$:} For a compound variable $v$ of type $C$, a contained constraint is instantiated by qualifying all compound-scoped variable occurrences. As indicated by Pattern \ref{forCompoundSlot}, we achieve this by substituting \IVMLself{} with the actual compound accessor, i.e., $access(v)$, and slot $s$ with $access(v.s)$. + + \item \emph{Eval blocks:} The containing compound is the evaluation scope of a nested eval block, i.e., constraints in an eval block are translated as if they were defined directly in the containing compound type, i.e., Pattern \ref{forCompoundEval} is rather similar to Pattern \ref{forCompoundSlot}. However, eval blocks require a higher evaluation priority within the compound scope as we will detail below. + + \item \emph{Annotation assignments: } Akin to eval blocks, constraints in a nested assign block are evaluated in the containing compound scope as indicated by Pattern \ref{forCompoundAssign}. However, annotation assignments require specific handling of default values to avoid accidental re-assignment of default values as we will discuss in Section \ref{sectAnnotationDefaults}. + + \item \emph{Top-level constraint defined over a compound variable $v$:} Due to the mandatory use of qualified slot access expressions in top-level constraints, no specific translation is needed. Pattern \ref{forCompoundAssign} is listed here to discuss all possible kinds of compound constraints. Such constraints treated in Algorithm \ref{algTranslateConstraints} line \ref{algTranslateConstraintsTopLevelConstraints}. \end{itemize} + +To handle slot interactions among constraints in the same compound correctly, a respective frame in $\variableMapping$ containing mappings for all slots to their access expressions must be created before any slot is translated. Thereby, $\variableMapping$ implicitly considers containing scopes as well as defined and shadowed variables. Moreover, compounds and, thus, constraints induced by compound types, may be nested in compounds and containers. By following the used types, the respective translation functions will be called recursively, i.e., Algorithm \ref{algTranslateDeclaration} for variables, Algorithm \ref{algTranslateCompoundDeclaration} for compound types as well as the translation of containers in Section \ref{sectContainerDefaults}. We will now focus on the second pattern and discuss the respective translation Algorithm \ref{algTranslateCompoundDeclaration}. The idea is to visit all slots and constraints in the compound type and its refined compound types, first for creating the variable mapping (Algorithm \ref{algRegisterCompoundMapping}), then for translating all constraints (Algorithm \ref{algTranslateCompoundContent}). In some situations, both steps must be carried out individually instead of a fixed sequence, e.g., to perform the translation of potentially inter-dependent compound slot default values between both steps as discussed for Algorithm \ref{algTranslateDeclaration}. As compound slots are nested variable declarations, Algorithm \ref{algTranslateDeclaration} is responsible for translating slots and their annotations. Akin to Algorithm \ref{algTranslateDeclaration}, default values of annotations (here given in terms of annotation assignments) are only turned into assignment constraints if the reasoner is not in incremental mode. Finally, eval blocks (due to evaluation priority) and then directly nested constraints and constraints in assignment blocks of a compound and all refined compound types are translated.