Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 152) +++ /reasoner/consTranslation.tex (revision 153) @@ -251,13 +251,23 @@ \grayPara{ \begin{gather*} - \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;}}{\bigcup_{t\in usedTypes(v), c\in constraints(t)}f(v, t)\rightarrow \IVML{forall}(w:\varSubstitution{c(x)}{x=w.x, \variableMapping})}\\ - \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;} c(v)\IVML{;}}{\varSubstitution{c(v)}{\variableMapping}} + \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;}}{\\\bigcup_{t~\in~usedTypes(v),~ c~\in~constraints(t)}f(v, t)\rightarrow \IVML{forall(w:}\varSubstitution{c(x)}{x=\IVML{w}, \IVML{self}=\IVML{w}, \variableMapping}\IVML{)}}\\ + \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;}~c(v)\IVML{;}}{\varSubstitution{c(v)}{\variableMapping}} \end{gather*} } -There are two basic translation patterns for containers, 1) constraints induced by used types and 2) top-level constraints for collection variables. We will focus here on the first pattern, as the second pattern comes for free as part of the translation of the top-level constraints. - -As shown for the first pattern, given a container variable $v$, we consider all potential (declared) as well as used types in the actual value and create for each constraint implied by these types an all-quantified constraint over $v$. Please note that individual constraints are needed to provide detailed error messages, but also to keep the re-evaluation effort low. However, if the container is nested, i.e., $T$ is again a container over a certain type, we must take flattening into account to apply the constraints to the individual elements. Moreover, if $\subTypeOf{t}{T)}$, accessing specific properties such as compound slots requires some form of type casting / selection on the elements of the container. These additional container transformations depend on the actual container type and are represented in the schema by $f(v, t)$. For short, $f(v, t)$ turns a sequence into a set to avoid duplicated constraints, flattens a nested container and applies type selects to enable access to slots defined in refined compounds. We will detail $f(v, t)$ below in this section. Finally, the constraint must be substituted adequately, using the quantifier iterator to access the elements, including slot access expressions for compound element types as well as known access expressions to other variables and slots. - +There are two basic translation patterns for containers, the first one for constraints induced by the types used in the container and the second one for top-level constraints over collection variables. We will focus here on the first pattern, as the second pattern comes for free as part of the translation of the top-level constraints in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelEvals}. + +For the first pattern, we consider all declared and used element types in the actual container value of the container variable $v$ and create for each constraint implied by these types an all-quantified constraint over $v$. In more details, let $t$ be a declared or used element type in $v$, then we can quantify all container elements (or at least a subset of type $t$) through a quantor iterator variable $x$ of type $t$ and apply all constraints for $t$ by instantiating the constraints for $x$, i.e., qualifying all used slots with respect to $x$ and replacing \IVML{self}. Although indivdual constraints may appear superfluous, they are needed to provide detailed error messages and also to keep the re-evaluation effort low. However, if the container is nested, i.e., $T$ is again a container over a certain type, in IVML we must flatten the container, i.e., remove all nested containers, to apply the constraints to all individual elements. As mentioned above, if $\subTypeOf{t}{T}$, accessing specific properties such as compound slots requires some form of type casting / selection on the elements of the container. These additional container transformations depend on the actual container type and are represented in the schema by the function $f(v, t)$. + +Basically, $f(v, t)$ turns a sequence into a set to avoid duplicated constraints, flattens a nested container and applies type selects if needed to enable access to slots defined in refined compounds. Therefore, $f(v, t)$ uses the IMVL container operations \IVML{flatten} and \IVML{selectByKind}. Let $e$ be a container access expression, e.g., $e=\createExpression{decl(v)}$. If $e$ is of a nested container type, we apply the \IVML{flatten} operation to extract all element values from all nested containers into one top-level container, i.e., enable access even to deeply nested container elements. We apply the \IVML{selectByKind} operation if $t$ is a subtype of the element type of the container, as otherwise slots defined on the specific type $t$ are not accessible. Finally, as shown in the transformation pattern, we apply an all-quantor over the elements of the (projected) collection using the temporary iterator variable $x$ to the respective constraint $c$ after appropriate variable substitution, in particular to \IVMLself{} by $x$. +% +\begin{displaymath} +e\rightarrow \underbrace{\IVML{flatten()}\rightarrow}_{\text{if isNested(e)}}\underbrace{\IVML{selectByKind(}t\IVML{)}\rightarrow}_{\text{if } \subTypeOf{t}{nested^*(e)}}\IVML{forAll}(x:c(x)) +\end{displaymath} +% +Algorithm \ref{algTranslateContainerDeclaration} translates a container variable declaration. The core idea of this algorithm is to determine the used types for all container elements and for each type to instantiate the constraints as explained above. However, used types are only availabe if a container value has been assigned. If no container value is available, we resort to the static type of the declaration of the container variable. During constraint translation, we distinguish between constraint containers, for which we directly turn the values into constraints, and container types that may imply further constraints such as containers over compounds or containers over derived types. + +Algorithm \ref{algTranslateContainerDeclaration} performs the transformation for a container variable declaration $d$ of variable $v$, if nested with given access expression $ca$ and actual type $t$. First, we create a new variable mapping context in $\variableMapping$ in line \ref{algTranslateContainerDeclarationPushContext} in order to keep marking processed types local to the actual container translation. Then, in line \ref{algTranslateContainerDeclarationInitTypes}, we determine the innermost nested type $t_n$ and its base type $t_b$ (i.e., ignoring intermediate derived types) as well as the relevant value $val$ (cf. Section \ref{sectNotationValues}). If $v$ is a constraint container, i.e., the innermost nested base type is a constraint, we translate all container constraints, i.e., (flattened) element values representing constraints in line \ref{algTranslateContainerDeclarationConstraintContainer}. If $v$ is a compound container, i.e., the innermost nested base type is a compound, we consider the (actual) types used in the container. If there is a compound value, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault}. As the translation algorithm traverses the refinement hierarchy a given type, we prune all general compound types and continue operating only on the most specific types in line \ref{algTranslateContainerDeclarationUsedTypesPrune}. If there is no value, we fall back to the innermost nested base (compound) type $t_b$ as the only used type (line \ref{algTranslateContainerDeclarationUsedTypesFallback}). Then, we iterate over all (pruned) used types and apply Algorithm \ref{algTranslateCompoundContainer}. Independently of constraint or compound container, we finally translate and collect all constraints stemming from derived type definitions in line \ref{algTranslateContainerDeclaration} and pop the initially created context in line \ref{algTranslateContainerDeclarationDerivedTypes}. + \begin{algorithm}[H] \SetAlgoLined @@ -265,10 +275,10 @@ \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, incremental flag $inc$} - $pushContext(\variableMapping, false)$\; - $t_n \assng nested^*(t); t_b \assng base^*(t_n); used\assng\emptySet$\; - $val\assng relevantValue(d, v, inc)$\; + $pushContext(\variableMapping, false)$\;\label{algTranslateContainerDeclarationPushContext} + $t_n \assng nested^*(t); t_b \assng base^*(t_n); val\assng relevantValue(d, v, inc)$\;\label{algTranslateContainerDeclarationInitTypes} \uIf{$isConstraint(t_b)$} { $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{e}{ca}}}{e \in allElements(val)}, true, v)$\; \label{algTranslateContainerDeclarationConstraintContainer} } \ElseIf{$isCompound(t_b)$} {\label{algTranslateContainerDeclarationCompoundContainerStart} + $used\assng\emptySet$\; \uIf{$val \neq \undef$} { $used \assng \setWithFlat{base(u)}{u \in usedTypes(val) \wedge isContainer(base(u))}$\; \label{algTranslateContainerDeclarationUsedTypesDefault} @@ -289,21 +299,11 @@ $translateDerivedDatatypeConstraints(t_n, d)$\; \label{algTranslateContainerDeclarationDerivedTypes} } - $popContext(\variableMapping)$\; + $popContext(\variableMapping)$\;\label{algTranslateContainerDeclarationPopContext} \caption{Translating declaration default value expressions to constraints (\IVML{translateContainerDeclaration}).}\label{algTranslateContainerDeclaration} \end{algorithm} -We detail now the generic translation schema, i.e., the function $f(v, t)$ mentioned above by using the IMVL \IVML{flatten} and the \IVML{selctByKind} operations: Let $d$ denote the variable declaration containing the compound (may alternatively be a compound or container accessor). The \IVML{flatten} resolves all nested containers and implicitly provides access even to deeply nested container entries. \IVML{selectByKind} is needed if we translate for slots of a specific given type $t$ with $\subTypeEqOf{t}{s}$, as otherwise the slots defined on specific types are not accessible. Finally, we apply an all quantor over the elements of the collection using the temporary iterator variable $l$ to the respective constraint $c$ after appropriate variable substitution, in particular replacing \IVMLself{} by $l$. -% -\begin{displaymath} -d\rightarrow \underbrace{\IVML{flatten()}\rightarrow}_{\text{if nested}}\underbrace{\IVML{selectByKind}(t)\rightarrow}_{\text{if } \subTypeOf{t}{nested^*(c)}}\IVML{forAll}(l:c(l)) -\end{displaymath} -% -Thus, the core idea of this algorithm is to consider all elements over all used types. If no value is available, we resort to the static type of the declaration of the containser variable. We create all-quantized constraints for all used types and distinguish between constraint containers, where the values directly turn into constraints, compound containers, where slots, constraints and annotations lead to further constraints, and derived types. - -Algorithm \ref{algTranslateContainerDeclaration} performs the transformation for a container variable declaration $d$ of variable $v$, if nested with given access expression $ca$ and specific type $t$ (due to a known default value). However, if $isCompound(t)$ and $t$ is also recursively used as slot type, Algorithm \ref{algTranslateContainerDeclaration} may cause an endless recursion. Thus, we translate constraints for $t$ only if $t$ was not already processed as flattening of the container elements used below requires considering each used type exactly once. - -For translating constraints, we first determine the innermost nested type $t_n$ and its base type $t_b$ (i.e., ignoring intermediate derived types) as well as the relevant value $val$. If $v$ is a constraint container, i.e., the innermost nested base type is a constraint, we collect and translate all constraints constituted by all (flattened) element values in line \ref{algTranslateContainerDeclarationConstraintContainer}. If $v$ is a compound container, i.e., the innermost nested base type is a compound, we consider the used types. If there is a value, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault} and prune more general refined types in line \ref{algTranslateContainerDeclarationUsedTypesPrune}, as the following algorithm must anyway iterate over the refinement hierarchy. If there is no value, the only used type is the innermost nested base type $t_b$, actually a compound (line \ref{algTranslateContainerDeclarationUsedTypesFallback}). The, we iterate over all (pruned) used types and apply Algorithm \ref{algTranslateCompoundContainer}. Independently of constraint or compound container, we finally translate and collect all constraints stemming from derived type definitions in line \ref{algTranslateContainerDeclaration}. - -Algorithm \ref{algTranslateCompoundContainer} creates constraints for compound values utilized in compounds, e.g., through a container initialize, in IVML like \IVML{seq = \{\{i=1\}, \{i=2\}\}}, assuming that \IVML{seq} is a sequence of compounds, which have an integer slot \IVML{i}. As these compounds are created implicitly within a container initializer, so far no default value constraints, nested constraints, annotation assignments etc. are scheduled to the constraint base, i.e., these compounds would remain uninitialized and their constraints not considered. +\MISSING{No pattern for this!} + +Algorithm \ref{algTranslateCompoundContainer} creates constraints for compound values in containers, e.g., through a container initializer, in IVML like \IVML{setOf(C) s; s = \{\{i=1\}, \{i=2\}\}}, assuming that \IVML{s} is a set of compounds of type \IVML{C} declaring an integer slot \IVML{i}. As these compounds are created implicitly within a container initializer, so far no constraint was added to the constraint base, neither through default value assignments, nested constraints, annotation assignments etc. In consequence, these compounds would remain uninitialized and their implicit constraints would not even be evaluated. \begin{algorithm}[H] @@ -338,4 +338,8 @@ Algorithm \ref{algTranslateCompoundContainer} targets this by creating all-quantized constraints over all elements of the container, mostly be reusing Algorithm \ref{algRegisterCompoundMapping} to create a compound mapping and Algorithm \ref{algTranslateCompoundContent} to translate the compound content. Initially, we a local variable $l$ as later iterator variable for the quantifier expressions. Then, we create a prefix expression $e$ of the quantor constraint expression, i.e., we determine in line \ref{algTranslateDefaultsCompoundContainerInitE} the access expression to the collection either using $ca$ or just holding the variable of the container $d$. If the container is a sequence that may contain duplicates, we first turn it into a set to avoid accidentally duplicated constraints (line \ref{algTranslateDefaultsCompoundContainerFlatten}). If the container is nested, we flatten it in line \ref{algTranslateDefaultsCompoundContainerFlatten} as constraints only need to be created for the elements (no specific constraints can be attached to a container type except for derived values, which are handled by Algorithm \ref{algTranslateDeclaration}). If the actual type $t$ is not the same as the type of the declaration $u)$, we must consider that the slot $s$ only exists for the specific refined type $t$. Then, the instantiation shall apply only to container elements of type $t$ (or of refined types), i.e., we insert in line \ref{algTranslateDefaultsCompoundContainerCast} an element selection by projecting the container to all elements of type $t$ (and refined types). + +%from above +As it is sufficient to process an actually contained type $t$ once per container, we translate constraints for $t$ only if $t$ was not already processed (in \ref{}). This also solves the potential problem that if $t$ is also used as a slot type within a nested compound type and no further measure is taken, Algorithm \ref{algTranslateContainerDeclaration} may run into an endless recursion. + Now we create a context for the container on the stack of $\variableMapping$. In contrast to compound translations, we also register the prefix expression $e$ and the iterator variable $l$. This will be taken up by the $add$ operation, which completes the full constraint from the given information on the stack, i.e., the full creation of the constraint is prepared but not shown in Algorithm \ref{algRegisterCompoundMapping}. As for compounds, we create now the compound mapping using Algorithm \ref{algRegisterCompoundMapping}. Please note that slot access now happens via the iterator variable $l$, while annotation access happens through $ca$. Specifying $t$ also as target type avoids unnecessary type casts here. Then, we call Algorithm \ref{algTranslateCompoundContent} to translate the compound slots, implying translation of annotations as well as recursion over further compounds and containers. Thereby, we replace a given access expression by the iterator variable $l$ or leave the access undefined as it is implicity given in and used from the actual context.