Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 146) +++ /reasoner/consTranslation.tex (revision 147) @@ -127,10 +127,5 @@ 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. -%As the context with the compound mapping is only valid during Algorithm \ref{algRegisterCompoundMapping}, default value expressions must be translated within the actual context, i.e., if $deflt$ has been passed in, lines \ref{algTranslateCompoundSubstStart}-\ref{algTranslateCompoundSubstEnd} perform the respective substitution, which will be returned as result of Algorithm \ref{algRegisterCompoundMapping}. Finally, Algorithm \ref{algTranslateCompoundDeclaration} removes the actual context frame for this compound from $\variableMapping$. +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, as well as conditional creation and release of variable mapping context frames. We represent the conditional handling of context frames in terms of the compound translation mode already mentioned for Algorithm \ref{algTranslateDeclaration}, i.e., by constants that indicate to $REGISTER$ the variable mapping, to $TRANSLATE$ the constraints and $NONE$ for no operation (type is known or excluded and shall not be mapped or transformed). \begin{algorithm}[H] @@ -141,15 +136,14 @@ $next \assng NONE$\; \If{$\neg alreadyProcessed(\variableMapping, t)$} { - \If{$m = REGISTER \vee m = BOTH$}{ - $recordProcessed(\variableMapping, t)$\;\label{algTranslateCompoundDeclarationRecordProcessed} + \If{$m = REGISTER$}{ $pushContext(\variableMapping, d, v \neq \undef)$\; \label{algTranslateCompoundDeclarationPushContext} $transferTypeExcludes(\variableMapping, t)$\; - $e \assng \createExpression{d}$\; - $registerCompoundMapping(t, ca, v, e)$\; + $registerCompoundMapping(t, ca, \createExpression{d})$\; $next \assng TRANSLATE$\; } - \If{$ m = TRANSLATE \vee m = BOTH$}{ + \If{$ m = TRANSLATE$}{ $translateCompoundContent(d, v, t, ca)$\; - $popContext(\variableMapping)$; + $popContext(\variableMapping)$\; + $recordProcessed(\variableMapping, t)$\;\label{algTranslateCompoundDeclarationRecordProcessed} $next \assng NONE$\; } @@ -159,22 +153,22 @@ \end{algorithm} -Algorithm \ref{algRegisterCompoundMapping} visits all slots and annotations, creates access expressions for them and registers them with the current context frame in the variable mapping $\variableMapping$. The compound type $t_c$ indicates the type to be processed, i.e., where to take slot and annotation definitions from. The access expressions $ca$ is optional as usual and, if given, utilized as prefix to create access expressions for slots and annotations. Finally, a target type $t_t$ is given if the access via $ca_s$ or $ca_t$ requires a type cast so that specific slots of $t_t$ can be accessed. Type casts are required if if the actual value is of a refined type of $t_c$, as otherwise slots defined on the more specific type are not accessible and access is rejected by static type checking of IVML expressions. - -Let -% -$$slots^-(t) = \setWith{s \in slots(t)}{\neg isTypeExcluded(\variableMapping, type(parent(s)))} $$ -% -be the slots of $t$ for which the containing type is not excluded \footnote{Excluded types only occur as an optimization in constraint re-scheduling (cf. Section \ref{sectTopLevelConstraintsRescheduling}} in the actual context of $\variableMapping$. Algorithm \ref{algRegisterCompoundMapping} iterates over all slots accessible for the given compound type $t_c$ and creates for each slot a respective accessor. If a preceding compound access expression for the slots $ca_s$ is not given, it creates a static accessor based on $v$. If an accessor is given, we create an accessor based on $ca_s$ and include a type cast to $t_t$\footnote{The type cast can be omitted if $t=type(value(v))$. This is done by the implementation, but not detailed here as a type cast to the actual type does not have an effect.}. The created accessor is then registered with $\variableMapping$. Similarly, we iterate over all annotations for the current slot, create an accessor expression based on $ca_a$ and register the result with $\variableMapping$. - -\begin{algorithm}[H] - \SetAlgoLined - \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 +Algorithm \ref{algTranslateCompoundDeclaration} integrates the creation of the variable mapping, the constraint translation and the additional functionality for compound value changes controlled by the compound translation mode. Variable mapping and constraint translation are realized by separate algorithms (Algorithms \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent}, respectively) to enable their re-use when translating compound containers (cf. Section \ref{sectCompoundDefaults}). In more details, Algorithm \ref{algTranslateCompoundDeclaration} takes a compound variable $v$ of declaration $d$, an optional compound accessor $ca$, the actual type $t$ as well as the desired compound translation mode $m$ and returns the compound mode for a subsequent call of Algorithm \ref{algTranslateCompoundDeclaration}. A type $t$ is processed only if $t$ was not marked as already processed or, implicitly, recording of processed types is disabled (cf. Section \ref{sectVarMapping}). If a type shall not processed, the next compound mode is $NONE$, indicating that no context frame was created that needs to be popped during $TRANSLATE$. + +If the variable mapping shall be registered for type $t$, Algorithm \ref{algTranslateCompoundDeclaration} pushes a new context frame for the compound type onto the variable mapping stack $\variableMapping$ (line \ref{algTranslateCompoundDeclarationPushContext}) and transfers potentially excluded (global) types (for faster processing of value type changes) into the actual frame. Then it registers all required compound mappings using Algorithm \ref{algRegisterCompoundMapping} (using a joint accessor expression to $d$ in case that $ca=\undef$). The next compound mode after a registration of variable mappings is $TRANSLATE$. + +If constraints shall be translated for type $t$, Algorithm \ref{algTranslateCompoundDeclaration} performs the translation through Algorithm \ref{algTranslateCompoundContent}, pops the previously created context, records $t$ as processed and returns that no further compound translation ($NONE$) is needed for $t$. + +We detail now the variable mapping for compounds. Algorithm \ref{algRegisterCompoundMapping} visits all slots and annotations of a given compound type $t$, creates access expressions for them and registers them with the current context frame in the variable mapping $\variableMapping$. The access expressions $ca$ is optional and, if given, utilized as prefix to create access expressions for slots and annotations. If $ca$ is not given, $e_d$ is used instead, usually containing an expression to the variable declaration using $t$. Algorithm \ref{algRegisterCompoundMapping} iterates over all slots accessible for the given compound type $t$ and creates for each slot a respective accessor. If the compound access expression $ca$ is not given, Algorithm \ref{algRegisterCompoundMapping} creates a static accessor based on $e_d$. The created accessor $x$ is then registered with $\variableMapping$. Similarly, we register accessors for annotations of the current slot $s$ based on the accessor $x$ for $s$. Finally, the algorithm creates accessors for all annotations declared for the underlying compound variable (through $e_d$). + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{compound type $t$, acccess $ca$, declaration expression $e_d$} + \KwData{variable mapping $\variableMapping$} + + \ForAll{$s \iterAssng \setWithFlat{slots(t)}{t\in allRefines^+(t)}$} { \label{algRegisterCompoundMappingVarMappingStart} %actual slots $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)$}{ - $registerMapping(\variableMapping, a, \createExpression{\IVMLMeta{acc}(ca,a)})$\; \label{algRegisterCompoundMappingAnnotationMapping} + $registerMapping(\variableMapping, a, \createExpression{\IVMLMeta{acc}(x,a)})$\; \label{algRegisterCompoundMappingAnnotationMapping} } }\label{algRegisterCompoundMappingVarMappingEnd} @@ -190,4 +184,10 @@ In line \ref{algTranslateCompoundDeclarationSelf}, we determine the actual expression for self, i.e., the access expression $ca$ if given or the declaration $d$. Then, due to their specific priorities, we first translate all eval constraints defined along the type hierarchy for $t$ in lines \ref{algTranslateCompoundDeclarationEvalStart}-\ref{algTranslateCompoundDeclarationEvalEnd}. Afterwards, we include all remaining compound constraints, i.e., type constraints and annotation constraints in lines \ref{algTranslateCompoundDeclarationAllStart}-\ref{algTranslateCompoundDeclarationAllEnd}. + +Let +% +$$slots^-(t) = \setWith{s}{s \in slots(t) \wedge \neg isTypeExcluded(\variableMapping, type(parent(s)))} $$ +% +be the slots of compound type $t$ for which the containing parent type is not excluded in the actual context of $\variableMapping$. \begin{algorithm}[H] @@ -308,5 +308,5 @@ $pushContext(\variableMapping, \undef, e, l, true)$\; - $registerCompoundMapping(t, l, \undef, d)$\; \label{algTranslateDefaultsCompoundContainerMapping} + $registerCompoundMapping(t, l, d)$\; \label{algTranslateDefaultsCompoundContainerMapping} $translateCompoundContent(l, \undef, t, \closedCases{\undef, & \text{if } ca = \undef\\l & \text{else}})$\; \label{algTranslateDefaultsCompoundContainerContent}