Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 145) +++ /reasoner/consTranslation.tex (revision 146) @@ -125,7 +125,9 @@ 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. +We will now focus on the first 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. + +If the value of a compound variable changes during reasoning, the value type may also change along the compound refinement hierarchy. Although constraint re-scheduling will be discussed in Section \ref{sectTopLevelConstraintsRescheduling}, we consider this topic already here to present a complete translation algorithm for compund types instead of refining the algorithm later in Section \ref{sectTopLevelConstraintsRescheduling}. Changing value types require adjusting the constraint base, i.e., more or less constraints must be considered dynamically while reasoning. However, when the actual type of a compound variable changes, executing the full constraint transformation for the new type is possible, but inefficent as already known constraints are added again to the constraint base. Moreover, constraints that are still in the constraint base, as they were not evaluated or not fulfilled so far, are duplicated and may cause multiple error messages for the same violation. Thus, it is desirable to transform just the differences between the involved types, i.e., to translate the constraints for all types in the refinement hierarchy between old and new value type. This requires knowledge about already processed types, type exclusion, conditional creation and release of variable mapping context frames. + +Algorithm \ref{algTranslateCompoundDeclaration}, integrates the creation of the variable mapping, the translation and the additional functionality for compound value changes, the latter via the compound translation mode already mentioned for Algorithm \ref{algTranslateDeclaration}. In more details, Algorithm \ref{algTranslateCompoundDeclaration} translates the constraints for a compound variable $v$ of declaration $d$, compound accessor $ca$, actual type $t$ and compound translation mode $m$ (may be $REGISTER$, $TRANSLATE$). No variable mapping or translation happens if type $t$ was already processed, e.g., in case of recursive compound types. If the type shall be processed, and the variable mapping shall be registered, Algorithm \ref{algTranslateCompoundDeclaration} records $t$ as processed (line \ref{algTranslateCompoundDeclarationRecordProcessed}) and pushes a new context frame for the compound type onto the variable mapping stack $\variableMapping$ (line \ref{algTranslateCompoundDeclarationPushContext})\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. The main two steps are detailed in Algorithm \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent} as both Algorithms are reused with different arguments during the translation of compounds in Section \ref{sectCompoundDefaults}. Algorithm \ref{algRegisterCompoundMapping} registers all compound slots and annotations in the variable mapping, using $ca$ or $d$ as basis for access expressions for slots and annotations and casts to the type of the actual value in $v$ if available (else $\undef$ is passed in as argument). Now Algorithm \ref{algTranslateCompoundContent} can translate the entire compound content including slots, annotations, constraints, annotation-blocks and eval-blocks. @@ -139,13 +141,13 @@ $next \assng NONE$\; \If{$\neg alreadyProcessed(\variableMapping, t)$} { - \If{$m = ANYWAY \vee m = REGISTER$}{ - $recordProcessed(\variableMapping, t)$\; - $pushContext(\variableMapping, d, v \neq \undef)$\; + \If{$m = REGISTER \vee m = BOTH$}{ + $recordProcessed(\variableMapping, t)$\;\label{algTranslateCompoundDeclarationRecordProcessed} + $pushContext(\variableMapping, d, v \neq \undef)$\; \label{algTranslateCompoundDeclarationPushContext} $transferTypeExcludes(\variableMapping, t)$\; $e \assng \createExpression{d}$\; - $registerCompoundMapping(t, ca, v, e, type(value(v)))$\; + $registerCompoundMapping(t, ca, v, e)$\; $next \assng TRANSLATE$\; } - \If{$m = ANYWAY \vee m = TRANSLATE$}{ + \If{$ m = TRANSLATE \vee m = BOTH$}{ $translateCompoundContent(d, v, t, ca)$\; $popContext(\variableMapping)$; @@ -167,9 +169,9 @@ \begin{algorithm}[H] \SetAlgoLined - \KwIn{compound type $t_c$, acccess $ca$, variable $v$, declaration expression $e_d$ target type $t_t$} + \KwIn{compound type $t_c$, acccess $ca$, variable $v$, declaration expression $e_d$} \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$} \ForAll{$s \iterAssng \setWithFlat{slots(t)}{t\in allRefines^+(t_c)}$} { \label{algRegisterCompoundMappingVarMappingStart} %actual slots - $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(e_d, s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), s), &\text{else}}}$\; \label{algRegisterCompoundMappingVarMapping} + $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(e_d, s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca, s), &\text{else}}}$\; \label{algRegisterCompoundMappingVarMapping} $registerMapping(\variableMapping, s, x)$\; \ForAll{$a \iterAssng annotations(s)$}{ @@ -178,5 +180,5 @@ }\label{algRegisterCompoundMappingVarMappingEnd} \ForAll{$a \iterAssng annotations^+(decl(e_d))$}{ - $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(e_d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), a), &\text{else}}}$\; \label{algRegisterCompoundMappingCreateExpression} + $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(e_d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca, a), &\text{else}}}$\; \label{algRegisterCompoundMappingCreateExpression} $registerMapping(\variableMapping, a, x)$\; % left out origins } @@ -306,5 +308,5 @@ $pushContext(\variableMapping, \undef, e, l, true)$\; - $registerCompoundMapping(t, l, \undef, d, t)$\; \label{algTranslateDefaultsCompoundContainerMapping} + $registerCompoundMapping(t, l, \undef, d)$\; \label{algTranslateDefaultsCompoundContainerMapping} $translateCompoundContent(l, \undef, t, \closedCases{\undef, & \text{if } ca = \undef\\l & \text{else}})$\; \label{algTranslateDefaultsCompoundContainerContent}