Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 69) +++ /reasoner/reasoner.tex (revision 70) @@ -494,5 +494,55 @@ \subsection{Compound constraints}\label{sectCompoundDefaults} -Translating a compound into all its constraints requires considering all slots, all constraints defined within a compound, as well as all supported nested structures, such as eval blocks or attribute value assignment blocks. In particular, if the IVML keyword \IVMLself{} is used, it must be replaced by the actual variable of the respective compound type. First, we define some helper functions, then the translation algorithms. +Translating a compound into all its constraints requires considering all slots including inherited slots, all constraints defined within a compound including inherited ones, as well as all nested structures, such as eval blocks or attribute value assignment blocks. In particular, if the IVML keyword \IVMLself{} is used, it must be replaced 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} consists of three parts: +\begin{enumerate} +\item Creation and registration of access expressions to all slots and attributes so that cross references can be implicitly resolved during variable substitution applied to all default value expressions and constraints. +\item Translating all slot declarations and attributes using Algorithm \ref{algTranslateDeclaration}. +\item Special treatment of (constraint) container default values to $\otherConstraints$ as these constraints can be treated as usual constraints. +\item Translating all nested eval blocks to $\otherConstraints$ before further constraints to take their priority into account. +\item Translating all nested annotation assignment blocks $\otherConstraints$ as assignment and contained constraints represent usual constraints. +\item Translating all compound constraints to $\otherConstraints$ as these constraints can be treated as usual constraints. +\end{enumerate} + +In lines \ref{algTranslateCompoundDeclarationVarMappingStart}-\ref{algTranslateCompoundDeclarationVarMappingEnd}, Algorithm \ref{algTranslateCompoundDeclaration} creates accessors for all slots of the compound and registers them in the variable mapping $\variableMapping$. The first case creates a static accessor based on the declared type. The second case handles values of sub-types of $type(d)=type(v)$. Therefore, it creates a compound accessor for the most specific type given by $type(value(v))$. However, due to static type checking of the expression, we need a type cast to $type(value(v))$ as otherwise slots defined on the more specific type are not accessible. In fact, as an optimization, the type cast can be omitted if $t=type(value(v))$, but this is not shown in Algorithm \ref{algTranslateCompoundDeclaration}. Now, as the mapping is completed for $v$, the algorithm performs a transitive / recursive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclaration} in line \ref{algTranslateCompoundDeclarationTranslateSlots}. Please note that $slots(v)$ also includes the actual annotations for $v$, i.e., at this point the variable mapping contains also accessors to annotations and processing their declarations through Algorithm \ref{algTranslateDeclaration} anyway considers annotations. + +Now, we can translate further nested values / structures or contained constraints involving the mapping. First, Algorithm \ref{algTranslateCompoundDeclaration} inspects all slots / attributes. If one slot is a container of constraints, it translates all (constraint) values into instantiated constraints by substituting \IVMLself{} with the actual declaration (including matching mappings in $\variableMapping$) adding the translated constraint to the set of other constraints $\otherConstraints$. +If the slot is a compound container, it translates all contained compound variables, calling constraints using Algorithm \ref{algTranslateCompoundContainer}. Then the algorithm adds all + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{declaration $d$, variable $v$, compound access $ca$, default value type $t$} + \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$} + + \ForAll{$s \iterAssng slots(v)$} { \label{algTranslateCompoundDeclarationVarMappingStart} %actual slots + $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(d,s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, type(value(v))), s), &\text{else}}}$\; + $\variableMapping \assng \variableMapping \addMap \set{\mapEntry{s}{x}}$\; + }\label{algTranslateCompoundDeclarationVarMappingEnd} + \ForAll{$s \iterAssng slots(v)$ } { %actual slots + $translateDeclaration(s, decision(v, s), c)$\; \label{algTranslateCompoundDeclarationTranslateSlots} + } + \ForAll{$s \iterAssng slots(v)$} { %actual slots + \uIf{$isConstraintContainer(type(s))$} { + $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{value(e)}{d}}}{e \in elements(value(s))}, true)$\; + }\ElseIf{$isContainer(type(s))$} { + $add(\otherConstraints, translateCompoundContainer(s, v, \variableMapping[s]), true)$\; + } + } + \leIf{$ca \neq \undef$}{$f\assng ca$}{$f\assng d$} + $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{f}{c}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}, true)$\; + \If{$\neg inc$} { + \ForAll{$a \iterAssng assignments(t)$}{ + $translateAnnotationAssignments(a, v, \undef, ca)$\; \label{algTranslateCompoundDeclarationCompoundAssignments} + } + } + $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{c}{f}}}{c\in allCompoundConstraints(t, false)}, true)$\; + + \caption{Translating compound declarations (\IVML{translateCompoundDeclaration}).}\label{algTranslateCompoundDeclaration} +\end{algorithm} + +Finally, the algorithm translates all attribute assignments using Algorithm \ref{algTranslateAnnotationAssignments}, all direct compound constraints (substituting \IVMLself{} and registered variables), and translates and collects all eval constraints (\TBD{no self??}). + +We define now the specific helper functions used in Algorithm \ref{algTranslateCompoundDeclaration}. %Expressions may be simple variables, calculations or operation calls, in compounds also using the predefined variable \texttt{self} indicating the actual instance of the respective compound. These constraints must be evaluated upon each variable instance, i.e., for top-level basic variables, top-level compound variables, compound values within compounds as well as compound values within container initialiers, each potentially with a different access expression to make the variable unique. @@ -529,43 +579,4 @@ Algorithm \ref{algTranslateCompoundDeclaration} translates the default 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$). The types are related by $type(d) = type(v) \in allRefines^+(t)$. -First, Algorithm \ref{algTranslateCompoundDeclaration} creates all accessors for all slots of the compound and registers them in the variable mapping $\variableMapping$. While the first case creates a static accessor based on the declared type, the second case mitigates the problem that on slots known for specific value types may not be accessed through simple accessor expression as the compound access may be created for a refined type. Therefore, it creates a compound accessor for the most specific type obtained from an IVML type cast of the compound accessor to the actual value type (can be omitted if $t=type(value(v))$, not shown here). Then, it performs a transitive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclaration}. - -Second, Algorithm \ref{algTranslateCompoundDeclaration} considers all slots, in particular if one slot is a container of constraints, it translates all (constraint) values into instantiated constraints by substituting \IVMLself{} with the actual declaration (including matching mappings in $\variableMapping$) adding the translated constraint to the set of constraint variables ($\otherConstraints$). -%If the slot directly represents a constraint (variable), the algorithm performs a similar translation on the respective default value expression. -If the slot is a compound container, it translates all (\TBD{defaults?}) the contained constraints using Algorithm \ref{algTranslateContainerCompoundConstraints}. - -Finally, the algorithm translates all attribute assignments using Algorithm \ref{algTranslateAnnotationAssignments}, all direct compound constraints (substituting \IVMLself{} and registered variables), and translates and collects all eval constraints (\TBD{no self??}). - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{declaration $d$, variable $v$, compound access $ca$, default value type $t$} - \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$} - - \ForAll{s \iterAssng slots(v)} { \label{algTranslateCompoundDeclarationVarMappingStart} %actual slots - $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(d,s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, type(value(v))), s), &\text{else}}}$\; - $\variableMapping \assng \variableMapping \addMap \set{\mapEntry{s}{x}}$\; - }\label{algTranslateCompoundDeclarationVarMappingEnd} - \ForAll{s \iterAssng slots(v) \TBD{hint: contains vars from assignment block defs!}} { %actual slots - $translateDeclaration(s, decision(v, s), c)$\; \label{algTranslateCompoundDeclarationTranslateSlots} - } - \ForAll{s \iterAssng slots(v)} { %actual slots - \If{$isConstraintContainer(type(s))$} { - $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{value(e)}{d}}}{e \in elements(value(s))}, true)$\; - } - \If{$isContainer(type(s))$} { - $add(\otherConstraints, translateContainerCompoundConstraints(s, v, \variableMapping[s]), true)$\; - } - } - \If{$\neg inc$} { - \ForAll{$a \iterAssng assignments(t)$}{ - $translateAnnotationAssignments(a, v, \undef, ca)$\; \label{algTranslateCompoundDeclarationCompoundAssignments} - } - } - $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{c}{d}}}{c\in allCompoundConstraints(t, false)}, true)$\; - $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionVarMapping{c}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}, true)$\; - - \caption{Translating compound declarations (\IVML{translateCompoundDeclaration}).}\label{algTranslateCompoundDeclaration} -\end{algorithm} - \subsection{Container default constraints}\label{sectContainerDefaults} @@ -583,5 +594,5 @@ } } - $add(\otherConstraints, translateContainerCompoundConstraints(d, v, \undef), true)$\; + $add(\otherConstraints, translateCompoundContainer(d, v, \undef), true)$\; \If{$isContainer(t) \wedge isDerived(contained(t))$}{ $translateDerivedDatatypeConstraints(contained(t), d)$\; @@ -602,6 +613,6 @@ \end{algorithm} -If $d$ is a container, we must translate and apply all constraints of compounds within that container \TBD{nested containers follow?} to $d$. As Algorithm \ref{algTranslateContainerCompoundConstraints} is used within different algorithms, we return the collected constraints here. -The relevant types to be considered includes the contained type of $d$ and the types of all elements. If the respective type is a compound, we perform the actual translation (cf. Algorithm \ref{algTranslateContainerCompoundConstraints2}). +If $d$ is a container, we must translate and apply all constraints of compounds within that container \TBD{nested containers follow?} to $d$. As Algorithm \ref{algTranslateCompoundContainer} is used within different algorithms, we return the collected constraints here. +The relevant types to be considered includes the contained type of $d$ and the types of all elements. If the respective type is a compound, we perform the actual translation (cf. Algorithm \ref{algTranslateCompoundContainer2}). \begin{algorithm}[H] @@ -614,8 +625,8 @@ \ForAll{$t \iterAssng \set{tc} \cup \setWith{type(value(e))}{e\in elements(v)}$}{ \If{$isCompound(t)$}{ - $c \assng c \cup translateContainerCompoundConstraints(t, tc, d, ca)$\; + $c \assng c \cup translateCompoundContainer(t, tc, d, ca)$\; } } - \caption{Translating compound constraints from a container (\IVML{translateContainerCompoundConstraints}).}\label{algTranslateContainerCompoundConstraints} + \caption{Translating compound constraints from a container (\IVML{translateCompoundContainer}).}\label{algTranslateCompoundContainer} \end{algorithm} @@ -638,5 +649,5 @@ } - \caption{Translating compound constraints from a container (\IVML{translateContainerCompoundConstraints}).}\label{algTranslateContainerCompoundConstraints2} + \caption{Translating compound constraints from a container (\IVML{translateCompoundContainer}).}\label{algTranslateCompoundContainer2} \end{algorithm}