sequences obtained by mapping each node of the left-hand side in
document order to the sequence it generates on the right-hand side.
The call to the fs:distinct-doc-order
function ensures that the result is in document order without
duplicates. The dynamic context is defined by binding the
$
fs:dot
,
$
fs:sequence
,
$
fs:position
and
$
fs:last
variables.
Note that sorting by document order enforces the restriction that input and output sequences contains only nodes, and that the last step in a path expression may actually return atomic values.
| [RelativePathExpr / StepExpr]Expr | |||||||
| == | |||||||
|
Note that this section uses some auxiliary judgments which are defined in [8.2 Judgments for step expressions and filtering].
Introduction
| [70 (XQuery)] | StepExprXQ |
::= | FilterExpr |
AxisStep |
| [71 (XQuery)] | AxisStepXQ |
::= | (ReverseStep |
ForwardStep) PredicateList |
| [72 (XQuery)] | ForwardStepXQ |
::= | (ForwardAxis
NodeTest) | AbbrevForwardStep |
| [75 (XQuery)] | ReverseStepXQ |
::= | (ReverseAxis
NodeTest) | AbbrevReverseStep |
| [82 (XQuery)] | PredicateListXQ |
::= | Predicate* |
Core Grammar
The Core grammar productions for XPath steps are:
| [46 (Core)] | StepExpr |
::= | PrimaryExpr |
AxisStep |
| [47 (Core)] | AxisStep |
::= | ReverseStep |
ForwardStep |
| [48 (Core)] | ForwardStep |
::= | ForwardAxis NodeTest |
| [50 (Core)] | ReverseStep |
::= | ReverseAxis NodeTest |
Note
Step expressions can be followed by predicates. Normalization of predicates uses the following auxiliary mapping rule: []Predicates, which is specified in [4.2.2 Predicates]. Normalization for step expressions also uses the following auxiliary mapping rule: []Axis, which is specified in [<IP_ADDRESS> Axes].
Normalization of predicates need to distinguish between forward steps, reverse steps, and primary expressions.
As explained in the [XPath/XQuery] document, applying a step in
XPath changes the focus (or context). The change of focus is made
explicit by the normalization rule below, which binds the variable
$
fs:dot
to the node currently being processed, and the variable $
fs:position
to the position (i.e., the position within the input sequence) of
that node.
There are two sets of normalization rules for Predicates. The
first set of rules apply when the predicate is a numeric literal or
the expression last()
. The second set of rules apply
to all predicate expressions other than numeric literals and the
expression last()
. In the first case, the
normalization rules provides a more precise static type than if the
general rules were applied.
When the predicate expression is a numeric literal or the
fn:last
function, the following normalization rules
apply.
| [ForwardStep PredicateList [ NumericLiteral ]]Expr | ||
| == | ||
|
[ForwardStep PredicateList [
fn:last () ]]Expr |
|||
| == | |||
|
When predicates are applied on a reverse step, the position variable is bound in reverse document order.
| [ReverseStep PredicateList [ NumericLiteral ]]Expr | ||||
| == | ||||
|
When the step is a reverse axis, then the last item in the context sequence is the first in document order.
[ReverseStep PredicateList [
fn:last () ]]Expr |
||
| == | ||
|
The normalization rules above all use the function fs:item-at
to select a
particular item. The static typing rules for this function are
defined in [7.1.13 The fs:item-at
function].
When predicates are applied on a forward step, the input
sequence is first sorted in document order and duplicates are
removed. The context is changed by binding the $
fs:dot
variable to each node in document order.
| [ForwardStep PredicateList [ Expr ]]Expr | ||||
| == | ||||
|
When predicates are applied on a reverse step, the input
sequence is first sorted in document order and duplicates are
removed. The context is changed by binding the $
fs:dot
variable to each node in document order.
| [ReverseStep PredicateList [ Expr ]]Expr | |||||
| == | |||||
|
Finally, a stand-alone forward or reverse step is normalized by the auxiliary normalization rule for Axis.
| [ForwardStep]Expr |
| == |
fs:apply-ordering-mode ([ForwardStep]Axis) |
| [ReverseStep]Expr |
| == |
fs:apply-ordering-mode ([ReverseStep]Axis) |
The static semantics of an Axis NodeTest pair is obtained by retrieving the type of the context node, and applying the two filters (the Axis, and then the NodeTest with a PrincipalNodeKind) on the result.
|
||||||
|
|
||||||
| statEnv |- Axis NodeTest : Type3 |
Note
Note that the second judgment in the rule requires that the context item be a node, guaranteeing that a type error is raised when the context item is an atomic value.
The dynamic semantics of an Axis NodeTest pair is obtained by retrieving the context node, and applying the two filters (Axis, then NodeTest) on the result. The application of each filter is expressed through several auxiliary judgments (of, has principal, and test), as follows.
|
||||||
|
|
||||||
dynEnv |- Axis
NodeTest => fs:distinct-doc-order (Value3) |
Note
Note that the second judgment in the rule guarantees that the context item is bound to a node.
Introduction
The XQuery grammar for forward and reverse axis is as follows.
| [73 (XQuery)] | ForwardAxisXQ |
::= | ("child" "::") |
| [76 (XQuery)] | ReverseAxisXQ |
::= | ("parent" "::") |
In the case of XPath, forward axis also contain the
namespace::
axis.
| [30 (XPath)] | ForwardAxisXP |
::= | ("child" "::") |
Core Grammar
The Core grammar productions for XPath axis are:
| [49 (Core)] | ForwardAxis |
::= | ("child" "::") |
| [51 (Core)] | ReverseAxis |
::= | ("parent" "::") |
Notation
We introduce the following auxiliary grammar production to describe all axis.
| [90 (Formal)] | Axis |
::= | ForwardAxis |
ReverseAxis |
Notation
The normalization of axes uses the following auxiliary mapping rule: []Axis.
The normalization for all axes is specified as follows.
The semantics of the following(-sibling) and preceding(-sibling) axes are expressed by mapping them to Core expressions. All other axes are part of the Core and therefore are left unchanged through normalization.
[following-sibling::
NodeTest]Axis |
|||
| == | |||
[
|
[following:: NodeTest]Axis |
|||||
| == | |||||
[
|
All other forward axes are part of the Core [XPath/XQuery] and handled by the normalization rules below:
[child:: NodeTest]Axis |
| == |
child::
NodeTest |
[attribute:: NodeTest]Axis |
| == |
attribute:: NodeTest |
[self:: NodeTest]Axis |
| == |
self::
NodeTest |
[descendant:: NodeTest]Axis |
| == |
descendant:: NodeTest |
[descendant-or-self::
NodeTest]Axis |
| == |
descendant-or-self:: NodeTest |
[namespace:: NodeTest]Axis |
| == |
namespace:: NodeTest |
Reverse axes:
[preceding-sibling::
NodeTest]Axis |
| == |
| [let $e := . return $e/parent::node()/child:: NodeTest [.<<$e]]Expr |
[preceding:: NodeTest]Axis |
| == |
[ancestor-or-self::node()/preceding-sibling::node()/descendant-or-self:: NodeTest]Expr |
All other reverse axes are part of the Core [XPath/XQuery] and handled by the normalization rules below:
[parent:: NodeTest]Axis |
| == |
parent::
NodeTest |
[ancestor:: NodeTest]Axis |
| == |
ancestor:: NodeTest |
[ancestor-or-self::
NodeTest]Axis |
| == |
ancestor-or-self:: NodeTest |
Introduction
A node test is a condition applied on the nodes selected by an axis step. Node tests are described by the following grammar productions.
| [78 (XQuery)] | NodeTestXQ |
::= | KindTest | NameTest |
| [79 (XQuery)] | NameTestXQ |
::= | QName | Wildcard |
| [80 (XQuery)] | WildcardXQ |
::= | "*" |
Core Grammar
The Core grammar productions for node tests are:
| [52 (Core)] | NodeTest |
::= | KindTest | NameTest |
| [53 (Core)] | NameTest |
::= | QName | Wildcard |
| [54 (Core)] | Wildcard |
::= | "*" |
Notation
For convenience, we will use the grammar non-terminals Prefix, and LocalPart, both of which are NCNames, in some of the inference rules. They are defined by the following grammar productions.
| [18 (Formal)] | Prefix |
::= | NCName |
| [19 (Formal)] | LocalPart |
::= | NCName |
Introduction
A predicate consists of an expression, called a predicate expression, enclosed in square brackets.
| [83 (XQuery)] | PredicateXQ |
::= | "[" Expr "]" |
Notation
Normalization of predicates uses the following auxiliary mapping rule: []Predicates.
Predicates in path expressions are normalized with a special mapping rule:
| [Expr]Predicates | |||
| == | |||
|
Note that the semantics of predicates whose input expression
returns a numeric value also work if that value is not an integer.
In those cases the op:numeric-equal
returns false when
compared to a position. For example, the expression
//a[3.4]
always returns the empty sequence.
The corresponding Section in the [XPath/XQuery] document just contains examples.
| [74 (XQuery)] | AbbrevForwardStepXQ |
::= | "@"? NodeTest |
| [77 (XQuery)] | AbbrevReverseStepXQ |
::= | ".." |
Here are normalization rules for the abbreviated syntax.
| [..]Axis |
| == |
| parent::node() |
| [@NodeTest]Axis |
| == |
| attribute::NodeTest |
| [NodeTest]Axis |
| == |
| child::NodeTest |
Introduction
[XPath/XQuery] supports operators to construct and combine sequences. A sequence is an ordered collection of zero or more items. An item is either an atomic value or a node.
| [31 (XQuery)] | ExprXQ |
::= | ExprSingle (","
ExprSingle)* |
| [49 (XQuery)] | RangeExprXQ |
::= | AdditiveExpr (
"to" AdditiveExpr
)? |
Core Grammar
The Core grammar production for sequence expressions is:
| [22 (Core)] | Expr |
::= | ExprSingle (","
ExprSingle)* |
A sequence expression is normalized into a sequence of normalized single expressions:
The type of the sequence expression is the sequence over the types of the individual expressions.
Each expression in the sequence is evaluated and the resulting values are concatenated into one sequence.
The range operator is normalized to the
fs:to
function.
The static semantics of the fs:to
function
is defined in [7.1.11 The fs:to
function].
The dynamic semantics of the fs:to
function is defined in [7.1.11 The fs:to
function].
Introduction
| [81 (XQuery)] | FilterExprXQ |
::= | PrimaryExpr
PredicateList |
Core Grammar
There are no Core grammar productions for filter expressions as they are normalized to other Core expressions.
When a predicate with a numeric literal or the
last()
expression is applied on a primary expression,
it is normalized using the fs:item-at
function. This
results in a more precise static type for those cases.
| [PrimaryExpr PredicateList [ NumericLiteral ]]Expr | ||
| == | ||
|
| [PrimaryExpr PredicateList [ fn:last() ]]Expr | |||
| == | |||
|
In the general case, when a predicate is applied on a primary expression, it is normalized to a FLWOR expression as follows. The input sequence is processed in sequence order and the context item is bound to each item in the input sequence.
| [PrimaryExpr PredicateList [ Expr ]]Expr | ||||
| == | ||||
|
There are no additional static typing rules for filter expressions.
There are no additional dynamic evaluation rules for filter expressions.
[XPath/XQuery] provides several operators for combining sequences of nodes.
| [52 (XQuery)] | UnionExprXQ |
::= | IntersectExceptExpr (
("union" | "|") IntersectExceptExpr
)* |
| [53 (XQuery)] | IntersectExceptExprXQ |
::= | InstanceofExpr (
("intersect" | "except") InstanceofExpr )* |
Notation
The union, intersect, and except expressions are normalized into function calls to the appropriate functions. The mapping function []SequenceOp is defined by the following table:
| SequenceOp | [SequenceOp]SequenceOp |
| "union" | op:union |
| "|" | op:union |
| "intersect" | op:intersect |
| "except" | op:except |
Operators for combining node sequences are normalized as follows.
| [Expr1 SequenceOp Expr2]Expr |
| == |
fs:apply-ordering-mode
([SequenceOp]SequenceOp (
[Expr1]Expr,
[Expr2]Expr )) |
The static semantics of the operators that combine sequences are defined in [7.2.14 The op:union, op:intersect, and op:except operators].
The dynamic semantics for function calls is given in [4.1.5 Function Calls].
[XPath/XQuery] provides arithmetic operators for addition, subtraction, multiplication, division, and modulus, in their usual binary and unary forms.
| [50 (XQuery)] | AdditiveExprXQ |
::= | MultiplicativeExpr ( ("+" |
"-") MultiplicativeExpr
)* |
| [51 (XQuery)] | MultiplicativeExprXQ |
::= | UnionExpr ( ("*" |
"div" | "idiv" | "mod") UnionExpr )* |
| [58 (XQuery)] | UnaryExprXQ |
::= | ("-" | "+")* ValueExpr |
| [59 (XQuery)] | ValueExprXQ |
::= | ValidateExpr |
PathExpr | ExtensionExpr |
Core Grammar
The Core grammar production for arithmetic expressions is:
| [40 (Core)] | ValueExpr |
::= | ValidateExpr |
StepExpr | ExtensionExpr |
Notation
The mapping function []ArithOp is defined by the following table:
| ArithOp | [ArithOp]ArithOp |
| "+" | fs:plus |
| "-" | fs:minus |
| "*" | fs:times |
| "div" | fs:div |
| "mod" | fs:mod |
Core Grammar
There are no Core grammar productions for arithmetic expressions as they are normalized to other Core expressions.
The normalization rules for all the arithmetic operators except
idiv
first atomize each argument by applying
fn:data
and then apply the internal function fs:convert-operand
to each argument. If the first argument to this function has type
xs:untypedAtomic
,
then the first argument is cast to a double, otherwise it is
returned unchanged. The overloaded internal function corresponding
to the arithmetic operator is then applied to the two converted
arguments. The table above maps the operators to the corresponding
internal function. The mapping from the overloaded internal
functions to the corresponding non-overloaded function is given in
[C.2 Mapping of Overloaded Internal
Functions].
| [Expr1 ArithOp Expr2]Expr | ||||
| == | ||||
|
The normalization rules for the idiv
operator are
similar, but instead of casting arguments with type xs:untypedAtomic
to
xs:double
, they are cast to
xs:integer
.
[Expr1
idiv Expr2]Expr |
||||
| == | ||||
|
The unary operators are mapped similarly.
[+ Expr]Expr |
| == |
fs:unary-plus (fs:convert-operand (fn:data (([Expr]Expr)),
1.0E0)) |
[- Expr]Expr |
| == |
fs:unary-minus (fs:convert-operand (fn:data (([Expr]Expr)),
1.0E0)) |
The static semantics for function calls is given in [4.1.5 Function Calls]. The mapping from the overloaded internal functions to the corresponding non-overloaded function is given in [C.2 Mapping of Overloaded Internal Functions].
The dynamic semantics for function calls is given in [4.1.5 Function Calls]. The mapping from the overloaded internal functions to the corresponding non-overloaded function is given in [C.2 Mapping of Overloaded Internal Functions].
Introduction
Comparison expressions allow two values to be compared. [XPath/XQuery] provides three kinds of comparison expressions, called value comparisons, general comparisons, and node comparisons.
| [48 (XQuery)] | ComparisonExprXQ |
::= | RangeExpr ( (ValueComp |
| [61 (XQuery)] | ValueCompXQ |
::= | "eq" | "ne" | "lt" | "le" | "gt" | "ge" |
| [60 (XQuery)] | GeneralCompXQ |
::= | "=" | "!=" | "<" | "<=" | ">" |
">=" |
| [62 (XQuery)] | NodeCompXQ |
::= | "is" | "<<" | ">>" |
Notation
The mapping function []ValueComp is defined by the following table:
| ValueComp | [ValueComp]ValueComp |
"eq " |
fs:eq |
"ne " |
fs:ne |
"lt " |
fs:lt |
"le " |
fs:le |
"gt " |
fs:gt |
"ge " |
fs:ge |
Core Grammar
There are no Core grammar productions for value comparisons as they are normalized to other Core expressions.
The normalization rules for the value comparison operators first
atomize each argument by applying fn:data
and then
apply the internal function fs:convert-operand
defined in [7.1.1 The
fs:convert-operand function]. If the first argument to this
function has type xs:untypedAtomic
, then the
first argument is cast to a string, otherwise it is returned
unchanged. The overloaded internal function corresponding to the
value comparison operator is then applied to the two converted
arguments. The table above maps the value operators to the
corresponding internal function. The mapping from the overloaded
internal functions to the corresponding non-overloaded function is
given in [C.2 Mapping of Overloaded
Internal Functions].
| [Expr1 ValueComp Expr2]Expr | ||||
| == | ||||
|
The static semantics for function calls is given in [4.1.5 Function Calls]. The
comparison functions all have return type xs:boolean
,
as specified in [XQuery 1.0 and XPath
2.0 Functions and Operators (Second Edition)].
The dynamic semantics for function calls is given in [4.1.5 Function Calls].
Introduction
General comparisons are defined by adding existential semantics
to value comparisons. The operands of a general comparison may be
sequences of any length. The result of a general comparison is
always true
or false
.
Notation
The function []GeneralComp is defined by the following table:
| GeneralComp | [GeneralComp]GeneralComp |
"= " |
fs:eq |
"!= " |
fs:ne |
"< " |
fs:lt |
"<= " |
fs:le |
"> " |
fs:gt |
">= " |
fs:ge |
Core Grammar
There are no Core grammar productions for general comparisons as they are normalized to existentially quantified Core expressions.
The normalization rule for a general comparison expression first
atomizes each argument by applying fn:data
, resulting
in two sequences of atomic values. Two nested some
expressions then examine (potentially) every pair of values (one
value from each sequence). For each pair, the internal function
fs:convert-operand
is called twice; if either of the two values is of type xs:untypedAtomic
, one of
the calls will cast it to a type determined by the other value. The
overloaded internal function corresponding to the general
comparison operator is then applied to the two converted
values.
| [Expr1 GeneralComp Expr2]Expr | |||||
| == | |||||
|
Core Grammar
There are no Core grammar productions for node comparisons as they are normalized to other Core expressions.
The normalization rules for node comparisons map each argument expression and then apply the internal function corresponding to the node comparison operator. The internal function are defined in [C.2 Mapping of Overloaded Internal Functions].
The static semantics for the internal functions are defined in [C.2 Mapping of Overloaded Internal Functions].
The dynamic semantics for internal function is defined in [C.2 Mapping of Overloaded Internal Functions].
Introduction
A logical expression is either an and-expression
or an or-expression. The value of a logical expression is
always one of the boolean values: true
or
false
.
| [46 (XQuery)] | OrExprXQ |
::= | AndExpr ( "or" AndExpr )* |
| [47 (XQuery)] | AndExprXQ |
::= | ComparisonExpr (
"and" ComparisonExpr
)* |
Core Grammar
The Core grammar productions for logical expressions are:
| [36 (Core)] | OrExpr |
::= | AndExpr ( "or" AndExpr )* |
| [37 (Core)] | AndExpr |
::= | CastableExpr ( "and"
CastableExpr )* |
The normalization rules for "and
" and
"or
" first get the effective boolean value of each
argument, then apply the appropriate Core operator.
The logical expressions require that each subexpression have
type xs:boolean
. The result type is also
xs:boolean
.
The dynamic semantics of logical expressions is
non-deterministic. This non-determinism permits implementations to
use short-circuit evaluation strategies when evaluating logical
expressions. In the expression, Expr1 and
Expr2, if either expression raises an error or
evaluates to false, the entire expression may raise an error or
evaluate to false. In the expression, Expr1 or
Expr2, if either expression raises an error or
evaluates to true, the entire expression may raise an error or
evaluate to true.
[XPath/XQuery] supports two forms of constructors. Direct constructors support literal XML syntax for elements, attributes, text nodes, processing-instructions and comments. Computed constructors can be used to construct elements, attributes, text nodes, processing-instructions, comments, and document nodes. All direct constructors are normalized into computed constructors, i.e., there are no direct-constructor expressions in the Core.
Core Grammar
The Core grammar productions for constructors are:
| [64 (Core)] | Constructor |
::= | ComputedConstructor |
| [65 (Core)] | ComputedConstructor |
::= | CompDocConstructor |
| [21 (Core)] | EnclosedExpr |
::= | "{" Expr "}" |
There are no Core grammar productions for direct XML element or attribute constructors as they are normalized to computed constructors.
Introduction
The static and dynamic semantics of the direct forms of element and attribute constructors are specified in terms of the equivalent computed element and attribute constructors.
Notation
The auxiliary mapping rules []ElementContent, []ElementContentUnit, []PartitionIntoUnits, and []DirCharsUnit are defined in this section and are used for the normalization of the content of direct element constructors.
Notation
An element-content unit is either a DirCharsUnit ( a maximal contiguous sequence of literal characters , CDataSections, character references, escaped braces, and predefined entity references), an enclosed expression, a direct element constructor, an XML comment, or an XML processing instruction. We use the following auxiliary grammar productions to describe element-content units.
| [83 (Formal)] | ElementContentUnit |
::= | DirectConstructor | EnclosedExpr | DirCharsUnit |
| [84 (Formal)] | DirCharsUnit |
::= | (CDataSection |
PredefinedEntityRef |
CharRef | "{{" | "}}" | ElementContentChar)+ |
We use the auxiliary normalization rule [ DirElemContent* ]PartitionIntoUnits to restructure the original element content, DirElemContent*, into the appropriate sequence of element-content units. This normalization rule is not specified formally.
Here are three direct element constructors, each of which contains one element-content unit:
<date>{ xs:date("2003-03-18") }</date> <name>Dizzy Gillespie</name> <comment><!-- Just a comment --></comment>
The first contains one enclosed expression, the second contains one contiguous sequence of characters, and the third contains one XML comment.
After boundary whitespace is stripped, the next example contains six element-content units:
<address> <!-- Dizzy's address --> { 123 }-0A <street>Roosevelt Ave.</street> Flushing, NY { 11368 } </address>
It contains an XML comment, followed by an enclosed expression that contains the integer 123, a contiguous sequence of characters ("-0A "), a direct XML element constructor, a contiguous sequence of characters (" Flushing, NY "), and an enclosed expression that contains the integer 11368. Evaluation of that constructor will result in the following element.
<address><!-- Dizzy's address -->123-0A <street>Roosevelt Ave.</street> Flushing, NY 11368</address>
We start by giving the rules for the two forms of direct XML element constructors. Note that the direct attribute constructors are normalized twice: the []NamespaceAttrs normalizes the namespace-declaration attributes and []Attribute normalizes all other attributes that are not namespace-declaration attributes.
| [ < QName DirAttributeList > DirElemContent* </ QName S? > ]Expr |
| == |
| element QName { [ DirAttributeList ]Attribute , [ [ DirElemContent* ]PartitionIntoUnits ]ElementContent } { [ DirAttributeList ]NamespaceAttrs } |
| [ < QName DirAttributeList /> ]Expr |
| == |
| element QName { [ DirAttributeList ]Attribute } { [ DirAttributeList ]NamespaceAttrs } |
We can now give the rules for normalizing a direct element constructor's content.
Adjacent element-content units permit arbitrary interleaving of text and atomic data. During evaluation, atomic values are converted to text nodes containing the string representations of the atomic values, and then adjacent text nodes are concatenated together. In the example at the beginning of this section, the integer 123 is converted to a string and concatenated with "-0A" and the result is a single text node containing "123-0A".
Below are two examples of normalization for element constructors.
<date>{ xs:date("2003-03-18") }</date> = element date { fs:item-sequence-to-node-sequence( xs:date("2003-03-18") ) } {} <address> <!-- Dizzy's address --> { 123 }-0A <street>Roosevelt Ave.</street> Flushing, NY { 11368 } </address> = element address { fs:item-sequence-to-node-sequence( comment { " Dizzy's address "}, 123, text { "-0A "}, element street {"Roosevelt Ave."} {}, text { " Flushing, NY " }, 11368 ) } {}
We normalize each unit individually and construct a sequence of the normalized results.
| [ElementContentUnit1, ..., ElementContentUnitn]ElementContent |
| == |
| [ ElementContentUnit1 ]ElementContentUnit , ..., [ ElementContentUnitn]ElementContentUnit |
(Note that this rule should be understood to cover the degenerate cases of n=0 and n=1, where the element constructor's content consists of zero or one element-content units.)
Next, we give the normalization rules for each element-content unit. The normalization rule for a contiguous sequence of characters assumes that the significant whitespace characters in element constructors have been preserved, as described in [<IP_ADDRESS> Boundary Whitespace].
The following normalization rule takes a maximal contiguous sequence of individual characters that include literal characters, CDataSections, escaped curly braces, character references, and predefined entity references and normalizes the character sequence as a text node containing the string of characters.
| [DirCharsUnit]ElementContentUnit |
| == |
| text { [ DirCharsUnit ]DirCharsUnit } |
The application of []DirCharsUnit to DirCharsUnit is defined informally. It produces a string literal corresponding to the content of the DirCharsUnit, in which boundary whitespace is processed as specified in Section <IP_ADDRESS> Boundary WhitespaceXQ, and non-literal characters (CharRefs, PredefinedEntityRefs, CDataSections, and escaped-braces) are resolved according to the rules in Section <IP_ADDRESS> ContentXQ.
XML processing instructions and comments in element content are normalized by applying the standard normalization rules for expressions, which appear in [4.7.2 Other Direct Constructors].
| [DirPIConstructor]ElementContentUnit |
| == |
| [DirPIConstructor]Expr |
| [DirCommentConstructor]ElementContentUnit |
| == |
| [DirCommentConstructor]Expr |
A direct element constructor is normalized using the normalization rule for expressions.
| [DirElemConstructor]ElementContentUnit |
| == |
| [DirElemConstructor]Expr |
An enclosed expression in element content is normalized into a
call to the function fs:item-sequence-to-node-sequence
,
which implements various rules for converting a sequence of atomic
values and nodes into a sequence of nodes before element
construction.
| [ { Expr } ]ElementContentUnit |
| == |
fs:item-sequence-to-node-sequence ((
[Expr]Expr )) |
There are no additional static typing rules for direct XML element or attribute constructors.
There are no additional dynamic evaluation rules for direct XML element or attribute constructors.
Like direct element constructors, direct attribute constructors are normalized to computed attribute constructors.
Notation
The auxiliary mapping rules []Attribute, []DirAttributeValue, []AttributeContent, []AttributeContentUnit, and []AttributeCharsUnit, are defined in this section and are used for the normalization of direct attribute constructors.
We use the following grammar productions to represent AttributeContentUnits, i.e., the expressions used to compute the content of an attribute.
| [87 (Formal)] | AttributeContentUnits |
::= | AttributeContentUnit* |
| [88 (Formal)] | AttributeContentUnit |
::= | AttributeCharsUnit | EnclosedExpr |
| [91 (Formal)] | AttributeCharsUnit |
::= | (QuotAttrContentChar |
AposAttrContentChar |
EscapeQuot | EscapeApos | PredefinedEntityRef |
CharRef | "{{" |
"}}")+ |
An AttributeCharsUnit is required to be maximal, i.e., it must extend as far as possible in both directions. In other words, an AttributeContentUnits must not contain two adjacent AttributeCharsUnits.
Direct attributes may contain namespace-declaration attributes. The normalization rules in this section ignore namespace-declaration attributes -- they are handled by the normalization rules in [<IP_ADDRESS> Namespace Declaration Attributes].
A DirAttributeList is normalized by the following rule, which maps each of the individual attribute-value expressions in the attribute list and constructs a sequence of the normalized values.
[
|
|||
| == | |||
|
Namespace-declaration attributes, i.e.,
those attributes whose prefix is xmlns
are ignored by
mapping them to the empty sequence.
|
||
| == | ||
| () |
All attributes that are not namespace-declaration attributes are mapped to computed attribute constructors.
|
||
| == | ||
| attribute Prefix:LocalPart { [ [DirAttributeValue]DirAttributeValue ]AttributeContent } |
The effect of [DirAttributeValue]DirAttributeValue is not specified formally; informally, it partitions the content of DirAttributeValue into a sequence of AttributeContentUnits, each of which is either an enclosed expression (EnclosedExpr) or a maximal run of character content (AttributeCharsUnit). These content units are then normalized via []AttributeContent, which is defined below.
To apply []AttributeContent to zero or more
attribute-content units, we normalize each unit individually and
construct a sequence of the normalized results. Then we apply the
function fn:string-join
, which will concatenate the
values of the normalized units.
| [ AttributeContentUnit1 ... AttributeContentUnitn ]AttributeContent |
| == |
| fn:string-join (([ AttributeContentUnit1 ]AttributeContentUnit , ..., [ AttributeContentUnitn]AttributeContentUnit) , '' ) |
(Note that this rule should be understood to cover the degenerate cases of n=0 and n=1, where the attribute constructor's content consists of zero or one attribute-content units.)
The next two rules specify the normalization of each attribute-content unit via []AttributeContentUnit.
We normalize an AttributeCharsUnit (i.e., a maximal run of attribute-content characters, including literal characters, character references, predefined entity references, escaped curly braces, and escaped single and double quotes) by converting it into a string literal.
| [ AttributeCharsUnit ]AttributeContentUnit |
| == |
| [ AttributeCharsUnit ]AttributeCharsUnit |
The effect of [AttributeCharsUnit]AttributeCharsUnit is not specified formally; informally, it unescapes any escaped braces or quotes, performs attribute value normalization as specified in Section <IP_ADDRESS> AttributesXQ, and then represents the resulting string value as a string literal.
We normalize an enclosed expression into a call to the function
fs:item-sequence-to-string
,
which implements various rules for converting a sequence of atomic
values and nodes into a string.
| [ { Expr } ]AttributeContentUnit |
| == |
fs:item-sequence-to-string ((
[ Expr ]Expr )) |
Notation
The auxiliary mapping rules []NamespaceAttr, and []NamespaceAttrs are defined in this section and are used for the normalization of namespace declaration attributes.
Some direct attributes may be namespace-declaration attributes. The normalization rules for namespace-declaration attributes ignore all non-namespace attributes -- they are handled by the normalization rules in [<IP_ADDRESS> Attributes].
A DirAttributeList containing namespace-declaration attributes is normalized by the following rule, which maps each of the individual namespace-declaration attributes in the attribute list and constructs a sequence of the normalized namespace attribute values.
[
|
|||
| == | |||
|
Attributes whose prefix is not xmlns
are ignored by
mapping them to the empty sequence.
|
||
| == | ||
| () |
Namespace-declaration attributes are normalized to local namespace declarations (LocalNamespaceDecl). The content of such attributes must be defined with a URI literal.
|
||
| == | ||
| namespace LocalPart { URILiteral } |
The rules for normalizing element content are given above in [4.7.1 Direct Element Constructors].
Section
<IP_ADDRESS> Boundary WhitespaceXQ
describes how whitespace is processed in element constructors
depending on the value of the boundary-space
declaration in the query prolog. The Formal Semantics assumes that
the rules for handling whitespace are applied by the (informally
defined) auxiliary rule []DirCharsUnit.
| [105 (XQuery)] | DirPIConstructorXQ |
::= | "<?" PITarget
(S DirPIContents)? "?>" |
| [106 (XQuery)] | DirPIContentsXQ |
::= | (Char* - (Char* '?>'
Char*)) |
| [103 (XQuery)] | DirCommentConstructorXQ |
::= | "<!--" DirCommentContents
"-->" |
| [104 (XQuery)] | DirCommentContentsXQ |
::= | ((Char - '-') | ('-'
(Char - '-')))* |
Notation
The auxiliary mapping rule []Characters is defined in this section and used for the normalization of direct PI and comment constructors.
[Char*]Characters takes the character content of a PI or comment constructor and yields a corresponding StringLiteral.
A literal XML processing instruction is normalized into a computed processing-instruction constructor; its character content is converted to a string using the auxiliary mapping rule []Characters.
| [<? NCName DirPIContents ?>]Expr |
| == |
| [processing-instruction NCName { [DirPIContents]Characters }]Expr |
A literal XML comment is normalized into a computed comment constructor; its character content is converted to a string using the auxiliary mapping rule []Characters.
| [<!-- DirCommentContents -->]Expr |
| == |
| [comment { [DirCommentContents]Characters }]Expr |
There are no additional static typing rules for direct processing-instruction or comment constructors.
There are no additional dynamic evaluation rules for direct processing-instruction or comment constructors.
| [109 (XQuery)] | ComputedConstructorXQ |
::= | CompDocConstructor |
Introduction
This section describes the semantics of computed element constructors. Remember that direct element constructors are normalized into computed element constructors. This document does not formally specify how namespaces are copied. The semantics of namespaces copying in element constructors can be found in [XQuery 1.0: An XML Query Language (Second Edition)].
| [111 (XQuery)] | CompElemConstructorXQ |
::= | "element" (QName | ("{"
Expr "}")) "{" ContentExpr? "}" |
| [112 (XQuery)] | ContentExprXQ |
::= | Expr |
Core Grammar
The Core grammar productions for computed element constructors are:
| [67 (Core)] | CompElemConstructor |
::= | "element" (QName | ("{"
Expr "}")) "{" ContentExpr "}" "{" LocalNamespaceDecls
"}" |
| [69 (Core)] | ContentExpr |
::= | Expr |
| [98 (Core)] | LocalNamespaceDecls |
::= | LocalNamespaceDecl* |
| [68 (Core)] | LocalNamespaceDecl |
::= | "namespace" NCName "{"
URILiteral "}" |
If the content expression is missing, the computed element constructor is normalized as if its content expression was the empty sequence.
Computed element constructors are normalized using the fs:item-sequence-to-node-sequence
function over their content expression.
| [element QName { Expr }]Expr |
| == |
element QName
{ fs:item-sequence-to-node-sequence (([Expr]Expr)) }
{} |
When the name of the element is also computed, the normalization rule applies atomization to the name expression.
| [element { Expr1 } { Expr2 }]Expr |
| == |
element {
fn:data (([Expr1]Expr)) }{
fs:item-sequence-to-node-sequence (([Expr2]Expr)) }
{} |
Notation
The following auxiliary judgment adds a sequence of namespace bindings to the static context.
This judgment is defined as follows.
|
||||||||||
|
|
||||||||||
|
The normalization rules of direct element and attribute constructors leave us with only the computed forms of constructors. The static semantics for constructors is defined on all the computed forms. The computed element constructor itself has two forms: one in which the element name is a literal QName, and the other in which the element name is a computed expression.
A computed element constructor creates a new element with either
the type
annotationXQ xs:untyped
(in strip construction
mode), or with the type
annotationXQ xs:anyType
(in preserve construction mode). The content expression must return
a sequence of nodes with attribute nodes at the beginning.
|
|||||
|
|
|||||
statEnv1 |- element QName {
Expr } { LocalNamespaceDecls }
: element
QName of type xs:anyType |
|
|||||
|
|
|||||
statEnv1 |- element QName {
Expr } { LocalNamespaceDecls }
: element
QName of type xs:untyped |
In case the element name is computed as well, the name
expression must be of type xs:QName
,
xs:string
, or xs:untypedAtomic
.
|
|||||||
|
|
|||||||
statEnv1 |- element {
Expr1 } {
Expr2 } { LocalNamespaceDecls }
: element * of
type xs:anyType |
|
|||||||
|
|
|||||||
statEnv1 |- element {
Expr1 } {
Expr2 } { LocalNamespaceDecls }
: element * of
type xs:untyped |
Notation
The following auxiliary judgment is used in the dynamic semantics of node constructors.
This judgment is informally defined to hold when Value1 is obtained by applying the following modifications to Value0:
Adjacent text nodes in Value0 are merged into a single text node by concatenating their contents, with no intervening blanks.
After concatenation, any text node whose content is a zero-length string is deleted from the sequence.
The following rules take a computed element constructor expression and construct an element node. The dynamic semantics for computed element constructors is the most complex of all expressions in XQuery. Here is how to read the rule below.
First, the constructor's local namespace declarations are evaluated, yielding a sequence of namespace bindings. The static environment is extended to include the new namespace bindings, which are all active. In Section <IP_ADDRESS> Namespace Declaration AttributesXQ, it is implementation-defined whether undeclaration of namespace prefixes (by setting the namespace prefix to the zero-length string) in an element constructor is supported. In the dynamic semantics below, we assume all local namespace declarations declare a binding of a prefix to a URI.
Second, the expression is evaluated, and its value's text nodes are processed. The resulting sequence must match zero-or-more attributes followed by zero-or-more element, text, processing-instruction or comment nodes.
Third, the namespace bindings are concatenated with the list of active namespaces in the namespace environment statEnv.namespace and the namespaces corresponding to the element's name and all attributes names. The resulting sequence is the sequence of namespace bindings for the element.
|
|||||
|
|
|||||
statEnv; dynEnv |-
element QName { Expr } {} => element QName of type
xs:anyType { Value1 } { } |
|
|||||||||||||||||||
|
|
|||||||||||||||||||
statEnv; dynEnv |-
element QName { Expr } { LocalNamespaceDecls }
=> element
QName of type xs:anyType { Value1 } { NamespaceBindings } |
The dynamic evaluation of an element constructor with a computed
name is similar. There is one additional rule that checks that the
value of the element's name expression matches
xs:QName
.
| [113 (XQuery)] | CompAttrConstructorXQ |
::= | "attribute" (QName |
("{" Expr "}")) "{" Expr? "}" |
Core Grammar
The Core grammar production for computed attribute constructors is:
| [70 (Core)] | CompAttrConstructor |
::= | "attribute" (QName | ("{"
Expr "}")) "{" Expr "}" |
Computed attribute constructors are normalized by mapping their
name and content expression in a similar way as computed element
constructors. The normalization rule uses the fs:item-sequence-to-string
function.
| [attribute QName { Expr }]Expr |
| == |
attribute
QName { fs:item-sequence-to-string
(([Expr]Expr)) } |
| [attribute { Expr1 } { Expr2 }]Expr |
| == |
attribute {
fn:data (([Expr1]Expr)) } {
fs:item-sequence-to-string
(([Expr2]Expr)) } |
The normalization rules for direct attribute constructors leave us with only the computed form of the attribute constructors. Like in a computed element constructor, a computed attribute constructor has two forms: one in which the attribute name is a literal QName, and the other in which the attribute name is a computed expression.
In the case of attribute constructors, the type
annotationXQ is always xs:untypedAtomic
.
|
|||
|
|
|||
statEnv |- attribute QName {
Expr } : attribute QName of type xs:untypedAtomic |
|
|||||
|
|
|||||
statEnv |- attribute {
Expr1 } {
Expr2 } : attribute * of type
xs:untypedAtomic |
The following rules take a computed attribute constructor expression and construct an attribute node. The rules are similar to those rules for element constructors. First, the attribute's name is expanded into a qualified name. Second, the content expression is evaluated in the dynamic environment.
|
||
|
|
||
dynEnv |- attribute QName {
Expr } => attribute QName of type
xs:untypedAtomic {
AtomicValue } |
|
|||||
|
|
|||||
dynEnv |- attribute {
Expr1 } {
Expr2 } => attribute
QName1 of type xs:untypedAtomic { AtomicValue2 } |
| [110 (XQuery)] | CompDocConstructorXQ |
::= | "document" "{" Expr
"}" |
Core Grammar
The Core grammar production for a computed document constructor is:
| [66 (Core)] | CompDocConstructor |
::= | "document" "{" Expr
"}" |
A document node constructor contains an expression, which must
evaluate to a sequence of element, text, comment, or
processing-instruction nodes. Section
<IP_ADDRESS> Document Node ConstructorsXQ
specifies the rules for converting a sequence of atomic values and
nodes into a sequence of nodes before document construction. The
built-in function fs:item-sequence-to-node-sequence
implements most of this conversion.
| [document { Expr }]Expr |
| == |
document { fs:item-sequence-to-node-sequence
(([Expr]Expr)) } |
The type of the entire expression is the most general
document
type, because the document constructor erases
all type
annotationXQ on its content
nodes.
|
|||
|
|
|||
| statEnv |- document { Expr } : document { Type } |
The dynamic semantics checks that the argument expression
evaluates to a value that is a sequence of element, text,
processing-instruction, or comment nodes. The entire expression
evaluates to a new document node value. If the construction mode is
set to strip
, the type
annotationXQ for all the nodes in
content of a document node are erased.
| [114 (XQuery)] | CompTextConstructorXQ |
::= | "text" "{" Expr
"}" |
Core Grammar
The Core grammar production for a computed text constructor is:
| [71 (Core)] | CompTextConstructor |
::= | "text" "{" Expr
"}" |
A text node constructor contains an expression, which must
evaluate to an xs:string
value. Section <IP_ADDRESS>
Text Node ConstructorsXQ specifies
the rules for converting a sequence of atomic values into a string
prior to construction of a text node. Each node is replaced by its
string value. For each adjacent sequence of one or more atomic
values returned by an enclosed expression, a untyped atomic value
is constructed, containing the canonical lexical representation of
all the atomic values, with a single blank character inserted
between adjacent values. As formal specification of these
conversion rules is not instructive, the fs:item-sequence-to-untypedAtomic-text
function implements this conversion.
| [text { Expr }]Expr |
| == |
text { (fs:item-sequence-to-untypedAtomic-text (fn:data (([Expr]Expr)))) cast
as xs:string ? } |
The static semantics checks that the argument expression has
type xs:string
or empty
. The type of the
entire expression is an optional text node type, as the text node
constructor returns the empty sequence if its argument is the empty
sequence.
If the argument expression returns the empty sequence, the text node constructor returns the empty sequence.
If the argument expression returns a value of type
xs:string
, the text node constructor returns a text
node with that string as content.
| [116 (XQuery)] | CompPIConstructorXQ |
::= | "processing-instruction" (NCName | ("{" Expr "}")) "{" Expr? "}" |
Core Grammar
The Core grammar production for computed processing-instruction constructors is:
| [73 (Core)] | CompPIConstructor |
::= | "processing-instruction" (NCName | ("{" Expr "}")) "{" Expr? "}" |
Computed processing-instruction constructors are normalized by mapping their name and content expression in the same way that computed element and attribute constructors are normalized.
| [processing-instruction NCName { Expr }]Expr |
| == |
processing-instruction
NCName { fs:item-sequence-to-untypedAtomic-PI (([Expr]Expr)) } |
| [processing-instruction { Expr1 } { Expr2 }]Expr |
| == |
processing-instruction
{ fn:data (([Expr1]Expr)) } {
fs:item-sequence-to-untypedAtomic-PI (([Expr2]Expr)) } |
The static typing rules for processing-instruction constructors are straightforward.
statEnv |- Expr : xs:untypedAtomic |
|
|
| statEnv |- processing-instruction NCName { Expr } : processing-instruction NCName |
statEnv |-
Expr1 :
(xs:NCName | xs:string | xs:untypedAtomic )
statEnv |-
Expr2 : xs:untypedAtomic |
|
|
| statEnv |- processing-instruction { Expr1 } { Expr2 } : processing-instruction * |
The dynamic evaluation rules for computed processing-instructions are straightforward.
| [115 (XQuery)] | CompCommentConstructorXQ |
::= | "comment" "{" Expr
"}" |
Core Grammar
The Core grammar production for computed comment constructors is:
| [72 (Core)] | CompCommentConstructor |
::= | "comment" "{" Expr
"}" |
Computed comment constructors are normalized by mapping their content expression.
| [comment { Expr }]Expr |
| == |
comment { (fs:item-sequence-to-untypedAtomic-comment (([Expr]Expr))) cast
as xs:string } |
The static typing rule for computed comment constructors is straightforward.
The dynamic evaluation rule for computed comment constructors is straightforward.
The effect of in-scope namespaces on constructed elements is specified in [4.7.1 Direct Element Constructors] and [<IP_ADDRESS> Computed Element Constructors].
Introduction
[XPath/XQuery] provides [For/FLWOR] expressions for iteration, for binding variables to intermediate results, and filtering bound variables according to a predicate.
A FLWORExpr in XQuery 1.0 consists of a sequence of ForClauses and LetClauses, followed by an optional WhereClause, followed by an optional OrderByClause, as described by the following grammar productions. Each variable binding is preceded by an optional type declaration which specify the type expected for the variable.
The dynamic semantics of the ordering mode in FLWOR expressions is not specified formally, as it would require the introduction of tuples, which are not supported in the [XPath/XQuery] data model.
| [33 (XQuery)] | FLWORExprXQ |
::= | (ForClause | LetClause)+ WhereClause? OrderByClause? "return" ExprSingle |
| [34 (XQuery)] | ForClauseXQ |
::= | "for" "$" VarName
TypeDeclaration? PositionalVar? "in" ExprSingle ("," "$" VarName TypeDeclaration? PositionalVar? "in" ExprSingle)* |
| [36 (XQuery)] | LetClauseXQ |
::= | "let" "$" VarName
TypeDeclaration? ":="
ExprSingle ("," "$" VarName TypeDeclaration? ":=" ExprSingle)* |
| [118 (XQuery)] | TypeDeclarationXQ |
::= | "as" SequenceType |
| [35 (XQuery)] | PositionalVarXQ |
::= | "at" "$" VarName |
| [37 (XQuery)] | WhereClauseXQ |
::= | "where" ExprSingle |
| [38 (XQuery)] | OrderByClauseXQ |
::= | (("order" "by") | ("stable" "order" "by")) OrderSpecList |
| [39 (XQuery)] | OrderSpecListXQ |
::= | OrderSpec (","
OrderSpec)* |
| [40 (XQuery)] | OrderSpecXQ |
::= | ExprSingle OrderModifier |
| [41 (XQuery)] | OrderModifierXQ |
::= | ("ascending" | "descending")? ("empty" ("greatest" |
"least"))? ("collation" URILiteral)? |
| [4 (XPath)] | ForExprXP |
::= | SimpleForClause
"return" ExprSingle |
| [5 (XPath)] | SimpleForClauseXP |
::= | "for" "$" VarName "in" ExprSingle ("," "$" VarName "in"
ExprSingle)* |
Core Grammar
The Core grammar productions for FLWOR expressions are:
| [24 (Core)] | FLWORExpr |
::= | (ForClause | LetClause) "return" ExprSingle |
| [25 (Core)] | ForClause |
::= | "for" "$" VarName
TypeDeclaration? PositionalVar? "in" ExprSingle |
| [27 (Core)] | LetClause |
::= | "let" "$" VarName
TypeDeclaration? ":="
ExprSingle |
| [26 (Core)] | PositionalVar |
::= | "at" "$" VarName |
| [75 (Core)] | TypeDeclaration |
::= | "as" SequenceType |
| [28 (Core)] | OrderByClause |
::= | (("order" "by") | ("stable" "order" "by")) OrderSpecList |
| [29 (Core)] | OrderSpecList |
::= | OrderSpec ("," OrderSpec)* |
| [30 (Core)] | OrderSpec |
::= | ExprSingle OrderModifier |
| [31 (Core)] | OrderModifier |
::= | ("ascending" | "descending")? ("empty" ("greatest" |
"least"))? ("collation" URILiteral)? |
Notation
For convenience, we introduce the following auxiliary grammar productions to represent optional type declarations and positional variables in For and Let clauses.
| [79 (Formal)] | OptTypeDeclaration |
::= | TypeDeclaration? |
| [80 (Formal)] | OptPositionalVar |
::= | PositionalVar? |
Notation
To facilitate the specification of normalization, we also introduce the following auxiliary grammar productions as an alternative grammar for FLWOR expressions.
| [65 (Formal)] | FormalFLWORClause |
::= | ForClause | LetClause | WhereClause | OrderByClause |
| [66 (Formal)] | FormalReturnClause |
::= | FormalFLWORExpr |
("return" Expr) |
| [67 (Formal)] | FormalFLWORExpr |
::= | FormalFLWORClause
FormalReturnClause |
Full FLWOR expressions are normalized to nested Core FLWOR expressions with a single for or let clause. Note that some of the normalization rules below accept ungrammatical FLWOR expressions such as "where Expr1 return Expr2". This does not matter, as normalization is always applied on parsed [XPath/XQuery] expressions, and such ungrammatical FLWOR expressions would be rejected by the parser beforehand.
Normalized FLWOR expressions restrict a For and Let clause to bind only one variable. Otherwise, the Core FLWOR expression is the same as the XQuery FLWOR expression. The first normalization rule is applied on a full [For/FLWOR] expression, splitting it at the clause level, then applying further normalization on each separate clause.
[
|
||||
| == | ||||
|
Likewise, a LetClause clause is normalized to nested let expressions, each of which binds one variable:
[
|
||||
| == | ||||
|
A WhereClause is normalized to an IfExpr, with the else-branch returning the empty sequence:
| [ where Expr1 FormalReturnClause]Expr |
| == |
| if ( fn:boolean(( [Expr1]Expr )) ) then [FormalReturnClause]Expr else () |
The order by clause is normalized using the auxiliary mapping rule []OrderSpecList which is defined in [4.8.4 Order By and Return Clauses].
| [ stable? order by OrderSpecList FormalReturnClause]Expr |
| == |
| [OrderSpecList]OrderSpecList return [FormalReturnClause]Expr |
Finally, a stand-alone return clause is normalized into the
corresponding expression. Recall that return
keywords
are introduced in the previous rule after the normalization of each
clause.
Example
The following simple example illustrates how a
FLWORExpr is normalized. The for
expression
in the example below is used to iterate over two collections,
binding variables $i
and $j
to items in
these collections. It uses a let
clause to bind the
local variable $k
to the sum of both numbers, and a
where
clause to select only those numbers that have a
sum equal to or greater than the integer 5
.
for $i as xs:integer in (1, 2), $j in (3, 4) let $k := $i + $j where $k >= 5 return <tuple> <i> { $i } </i> <j> { $j } </j> </tuple>
By the first set of rules, this is normalized to (except for the operators and element constructor which are not treated here):
for $i as xs:integer in (1, 2) return for $j in (3, 4) return let $k := $i + $j return if ($k >= 5) then <tuple> <i> { $i } </i> <j> { $j } </j> </tuple> else ()
For each binding of $i
to an item in the sequence
(1 , 2)
the inner for
expression iterates
over the sequence (3 , 4)
to produce tuples ordered by
the ordering of the outer sequence and then by the ordering of the
inner sequence. This Core expression eventually results in the
following document fragment:
(<tuple> <i>1</i> <j>4</j> </tuple>, <tuple> <i>2</i> <j>3</j> </tuple>, <tuple> <i>2</i> <j>4</j> </tuple>)
A single for
expression is typed as follows: First
Type1 of the iteration expression
Expr1 is inferred. Then
the prime type of
Type1, prime(Type1), is computed. This is a union over all item
types in Type1 (See [8.4 Judgments for
FLWOR and other expressions on sequences]). With the
variable component of the static environment statEnv extended with
$VarName1 as type
prime(Type1), the type Type2
of Expr2 is inferred.
Because the for
expression iterates over the result of
Expr1, the final type of
the iteration is Type2
multiplied with the possible number of items in Type1
(one, ?
, *
, or +
). This
number is determined by the auxiliary type-function quantifier(Type1). Operations between quantifiers and types, such
as Type2 ·
quantifier(Type1), used in the following rule, are defined in
[8.4 Judgments for FLWOR and other
expressions on sequences].
|
||||
|
|
||||
| statEnv |- for $VarName1 in Expr1 return Expr2 : Type2 · quantifier(Type1) |
When a positional variable Variablepos is present, the static environment is also
extended with the positional variable typed as an
xs:integer
.
|
|||||
|
|
|||||
| statEnv |- for $VarName1 at $VarNamepos in Expr1 return Expr2 : Type2 · quantifier(Type1) |
When a type declaration is present, the static semantics also checks that the type of the input expression is a subtype of the declared type and extends the static environment by typing $VarName1 with type Type0. This semantics is specified by the following static typing rule.
|
||||||
|
|
||||||
| statEnv |- for $VarName1 as SequenceType in Expr1 return Expr2 : Type2 · quantifier(Type1) |
The last rule handles For expressions that contain a type declaration and a positional variable. When the positional variable is present, the static environment is also extended with the positional variable typed as an integer.
|
|||||||
|
|
|||||||
| statEnv |- for $VarName1 as SequenceType at $VarNamepos in Expr1 return Expr2 : Type2 · quantifier(Type1) |
Example
For example, if $example
is bound to the sequence
10.0, 1.0E1, 10
of type xs:decimal, xs:float,
xs:integer
, then the query
for $s in $example return $s * 2
is typed as follows:
(1) prime(xs:decimal, xs:float, xs:integer) = xs:decimal | xs:float | xs:integer (2) quantifier(xs:decimal, xs:float, xs:integer) = + (3) $s : xs:decimal | xs:float | xs:integer (4) $s * 2 : xs:decimal | xs:float | xs:integer (5) result-type : ( xs:decimal | xs:float | xs:integer ) +
This result-type is not the most specific type possible. It does
not take into account the order of elements in the input type, and
it ignores the individual and overall number of elements in the
input type. The most specific type possible is: xs:decimal,
xs:float, xs:integer
. However, inferring such a specific
type for arbitrary input types and arbitrary return clauses
requires significantly more complex static typing rules. In
addition, if put into the context of an element, the specific type
violates the "unique particle attribution" restriction of XML
schema, which requires that an element must have a unique content
model within a particular context.
The evaluation of a for
expression distinguishes
two cases: If the iteration expression
Expr1 evaluates to the
empty sequence, then the entire expression evaluates to the empty
sequence:
| dynEnv |- Expr1 => () |
|
|
| dynEnv |- for $VarName1 OptTypeDeclaration OptPositionalVar in Expr1 return Expr2 => () |
Otherwise, the iteration expression
Expr1 is evaluated to
produce the sequence Item1,
..., Itemn. For each item Itemi
in this sequence, the body of the for
expression
Expr2 is evaluated in the
dynamic environment dynEnv extended with $VarName1 bound to Itemi.
This produces values Valuei, ..., Valuen which are concatenated to produce the result
sequence.
|
||||||
|
|
||||||
| dynEnv |- for $VarName in Expr1 return Expr2 => Value1 ,..., Valuen |
The following rule is the same as the rule above, but includes the optional positional variable $VarNamepos. If present, $VarNamepos is bound to the position of the item in the input sequence, i.e., the value i.
|
||||||
|
|
||||||
| dynEnv |- for $VarName at $VarNamepos in Expr1 return Expr2 => Value1 ,..., Valuen |
When a type declaration is present, the dynamic semantics also checks that each item in the result of evaluating Expr1 matches the declared type. This semantics is specified by the following dynamic evaluation rule.
|
||||||||||
|
|
||||||||||
| dynEnv |- for $VarName as SequenceType in Expr1 return Expr2 => Value1 ,..., Valuen |
The last rule covers a for
expression that contains
a type declaration and a positional variable.
|
|||||||||||
|
|
|||||||||||
| dynEnv |- for $VarName as SequenceType at $VarNamepos in Expr1 return Expr2 => Value1 ,..., Valuen |
Note that this definition allows non-deterministic evaluation of the resulting sequence, since the preconditions in the above rule can be evaluated in any order.
Example
Note that if the expression in the return
clause
results in a sequence, sequences are never nested in the
[XPath/XQuery] data model. For instance, in the following for
expression:
for $i in (1,2) return (<i> {$i} </i>, <negi> {-$i} </negi>)
each iteration in the for
results in a sequence of
two elements, which are then concatenated and flattened in the
resulting sequence:
(<i>1</i>, <negi>-1</negi>, <i>2</i>, <negi>-2</negi>)
A let
expression extends the static environment
statEnv with
Variable1 of type
Type1 inferred from Expr1, and infers the type of
Expr2 in the extended
environment to produce the result type Type2.
|
||
|
|
||
| statEnv |- let $VarName := Expr1 return Expr2 : Type2 |
When a type declaration is present, the static semantics also checks that the type of the input expression is a subtype of the declared type and extends the static environment by typing Variable1 with type Type0. This semantics is specified by the following static typing rule.
|
|||||
|
|
|||||
| statEnv |- let $VarName1 as SequenceType := Expr1 return Expr2 : Type2 |
A let
expression extends the dynamic environment
dynEnv with
Variable bound to Value1 returned by Expr1, and evaluates Expr2 in the extended environment to produce Value2.
|
|||
|
|
|||
| dynEnv |- let $VarName1 := Expr1 return Expr2 => Value2 |
When a type declaration is present, the dynamic semantics also checks that the result of evaluating Expr1 matches the declared type. This semantics is specified as the following dynamic evaluation rule.
|
|||||
|
|
|||||
| dynEnv |- let $VarName1 as SequenceType := Expr1 return Expr2 => Value2 |
Example
Note the use of the environments to define the scope of each
variable. For instance, in the following nested let
expression:
let $k := 5 return let $k := $k + 1 return $k+1
the outermost let
expression binds variable
$k
to the integer 5
in the environment,
then the expression $k+1
is computed, yielding value
6
, to which the second variable $k
is
bound. The expression then results in the final integer
7
.
Introduction
The dynamic semantics of the OrderByClause is not specified formally, as doing so would require the introduction of tuples, which are not supported in the [XPath/XQuery] data model. The dynamic semantics of the order-by clause can be found in Section 3.8.3 Order By and Return ClausesXQ.
Although an OrderByClause does not affect the type of a
FLWORExpr expression, it must still undergo static
analysis, in case this raises a static error. The static semantics
of a FLWORExpr expression with an OrderByClause
is equivalent to the static semantics of an equivalent
FLWORExpr in which the OrderByClause is replaced
by a call to the gt
comparison over the corresponding
OrderSpec expression(s).
Notation
To define normalization of OrderBy, the following auxiliary mapping rule is used.
| [OrderSpecList]OrderSpecList |
| == |
| LetClause ... LetClause |
This rules specifies that OrderSpecList is mapped to a sequence of LetClauses.
Proper static typing for FLWOR expressions with an
OrderByClause is obtained by normalizing the
OrderByClause to a Let clause, nested For expressions, and
atomization, then by applying the standard static typing rules for
those expressions. Note that if evaluated dynamically, the
normalization of OrderByClause given here does not express
the required sorting semantics. Notably, the normalization rule
introduces the gt
operation which is used implicitely
in the semantics of order by.
Each OrderSpec is normalized by the following rules.
| [OrderSpec1 ... OrderSpecn]OrderSpecList |
| == |
| [OrderSpec1]OrderSpecList, ... [OrderSpecn]OrderSpecList |
| [Expr OrderModifier]OrderSpecList | ||||||
| == | ||||||
|
Introduction
The purpose of ordered
and unordered
expressions is to set the ordering mode in the static context to
ordered
or unordered
for a certain region
in a query. The specified ordering mode applies to the expression
nested inside the curly braces.
| [91 (XQuery)] | OrderedExprXQ |
::= | "ordered" "{" Expr
"}" |
| [92 (XQuery)] | UnorderedExprXQ |
::= | "unordered" "{" Expr
"}" |
Core Grammar
The Core grammar productions for ordered/unordered expressions are:
| [61 (Core)] | OrderedExpr |
::= | "ordered" "{" Expr
"}" |
| [62 (Core)] | UnorderedExpr |
::= | "unordered" "{" Expr
"}" |
OrderedExpr (resp. UnorderedExpr) expressions are normalized to OrderedExpr (resp. UnorderedExpr) expressions in the [XPath/XQuery] Core.
OrderedExpr and UnorderedExpr expressions set
the ordering mode in the static context to ordered
or
unordered
.
|
|||
|
|
|||
| statEnv |- ordered { Expr } : Type |
|
|||
|
|
|||
| statEnv |- unordered { Expr } : Type |
OrderedExpr and UnorderedExpr expressions only
have an effect on the static context. The effect on the evaluation
of its subexpression(s) is captured using the fs:apply-ordering-mode
function, which introduced during normalization of axis steps,
union
, intersect
, and except
expressions, and FLWOR expressions that have no order
by
clause.
Introduction
A conditional expression supports conditional evaluation of one of two expressions.
| [45 (XQuery)] | IfExprXQ |
::= | "if" "(" Expr ")" "then"
ExprSingle "else" ExprSingle |
Core Grammar
The Core grammar production for the conditional expression is:
| [35 (Core)] | IfExpr |
::= | "if" "(" Expr ")" "then"
ExprSingle "else" ExprSingle |
Conditional expressions are normalized as follows.
| [if (Expr1) then Expr2 else Expr3]Expr | |
| == | |
|
statEnv |- Expr1 : xs:boolean
statEnv |- Expr2 : Type2
statEnv |- Expr3 : Type3 |
|
|
statEnv |- if
(Expr1) then
Expr2 else
Expr3 : (Type2
| Type3) |
If the conditional's boolean expression Expr1 evaluates to true, Expr2 is evaluated and its value is produced. If the conditional's boolean expression evaluates to false, Expr3 is evaluated and its value is produced. Note that the existence of two separate dynamic evaluation rules ensures that only one branch of the conditional is evaluated.
Introduction
[XPath/XQuery] defines two quantification expressions:
| [42 (XQuery)] | QuantifiedExprXQ |
::= | ("some" | "every") "$" VarName TypeDeclaration? "in" ExprSingle ("," "$" VarName TypeDeclaration? "in" ExprSingle)* "satisfies" ExprSingle |
| [6 (XPath)] | QuantifiedExprXP |
::= | ("some" | "every") "$" VarName "in" ExprSingle ("," "$"
VarName "in" ExprSingle)* "satisfies" ExprSingle |
Core Grammar
The Core grammar production for quantified expressions is:
| [32 (Core)] | QuantifiedExpr |
::= | ("some" | "every") "$" VarName TypeDeclaration? "in" ExprSingle ("," "$" VarName TypeDeclaration? "in" ExprSingle)* "satisfies" ExprSingle |
The quantified expressions are normalized into nested Core quantified expressions, each of which binds one variable.
| [some $VarName1 in Expr1, ..., $VarNamen in Exprn satisfies Expr]Expr | |||||
| == | |||||
|
| [every $VarName1 in Expr1, ..., $VarNamen in Exprn satisfies Expr]Expr | |||||
| == | |||||
|
The static semantics of the quantified expressions uses the
notion of prime
type. These rules are similar to those for for
expressions in [4.8.2 For
expression].
|
||||
|
|
||||
statEnv |- some
$VarName1 in
Expr1 satisfies
Expr2 :
xs:boolean |
The next rule is for SomeExpr with the optional type declaration.
|
||||||
|
|
||||||
statEnv |- some
$VarName1 as
SequenceType in Expr1 satisfies Expr2 : xs:boolean |
The next rule is for EveryExpr without the optional type declaration.
|
||||
|
|
||||
statEnv |- every
$VarName1 in
Expr1 satisfies
Expr2 :
xs:boolean |
The next rule is for EveryExpr with the optional type declaration.
|
||||||
|
|
||||||
statEnv |- every
$VarName1 as
SequenceType in Expr1 satisfies Expr2 : xs:boolean |
If its input expression returns the empty sequence, the SomeExpr expression returns false.
The SomeExpr expression yields true if any evaluation of the satisfies expression yields true. The SomeExpr expression yields false if every evaluation of the satisfies expression is false. A quantified expression may raise an error if any evaluation of the satisfies expression raises an error. The dynamic semantics of quantified expressions is non-deterministic. This non-determinism permits implementations to use short-circuit evaluation strategies when evaluating quantified expressions.
|
|||||
|
|
|||||
| dynEnv |- some $VarName1 in Expr1 satisfies Expr2 => true |
The next rule is for SomeExpr with the optional type declaration, in which some evaluation of the satisfies expression yields true.
|
|||||||
|
|
|||||||
| dynEnv |- some $VarName1 as SequenceType in Expr1 satisfies Expr2 => true |
The next rule is for SomeExpr without the optional type declaration, in which all evaluations of the satisfies expression yield false.
|
||||||
|
|
||||||
| dynEnv |- some $VarName1 in Expr1 satisfies Expr2 => false |
The next rule is for SomeExpr with the optional type declaration, in which all evaluations of the satisfies expression yield false.
|
|||||||||
|
|
|||||||||
| dynEnv |- some $VarName1 as SequenceType in Expr1 satisfies Expr2 => false |
If its input expression returns the empty sequence, the EveryExpr expression returns true.
The EveryExpr expression yields false if any evaluation of the satisfies expression yields false. The EveryExpr expression yields true if every evaluation of the satisfies expression is true.
|
|||||
|
|
|||||
| dynEnv |- every $VarName1 in Expr1 satisfies Expr2 => false |
The next rule is for EveryExpr with the optional type declaration, in which some evaluation of the satisfies expression yields false.
|
|||||||
|
|
|||||||
| dynEnv |- every $VarName1 as SequenceType in Expr1 satisfies Expr2 => false |
The next rule is for EveryExpr in which all evaluations of the satisfies expression yield true.
|
||||||
|
|
||||||
| dynEnv |- every $VarName1 in Expr1 satisfies Expr2 => true |
The next rule is for EveryExpr with the optional type declaration in which all evaluations of the satisfies expression yield true.
|
|||||||||
|
|
|||||||||
| dynEnv |- every $VarName1 as SequenceType in Expr1 satisfies Expr2 => true |
Introduction
Some of the expressions relying on the SequenceTypes syntax are called expressions on SequenceTypes. The syntax of SequenceTypes is described in [3.5.3 SequenceType Syntax].
| [54 (XQuery)] | InstanceofExprXQ |
::= | TreatExpr (
"instance" "of" SequenceType
)? |
Introduction
The SequenceType expression "Expr instance of SequenceType" is true if and only if the result of evaluating expression Expr is an instance of the type referred to by SequenceType.
An InstanceofExpr expression is normalized into a TypeswitchExpr expression. Note that the following normalization rule uses a variable $fs:new, which is a newly created variable which must not conflict with any variables already in scope. This variable is necessary to comply with the syntax of typeswitch expressions in the Core [XPath/XQuery], but is never used.
| [43 (XQuery)] | TypeswitchExprXQ |
::= | "typeswitch" "(" Expr ")"
CaseClause+ "default" ("$"
VarName)? "return" ExprSingle |
| [44 (XQuery)] | CaseClauseXQ |
::= | "case" ("$" VarName
"as")? SequenceType "return"
ExprSingle |
Introduction
The typeswitch expression chooses one of several expressions to evaluate based on the dynamic type of an input value.
Each branch of a typeswitch expression may have an optional $VarName, which is bound to the value of the input expression. One reason for using a variable on one of the branches is that it is assigned a type specific for that branch. This variable is optional in [XPath/XQuery] but made mandatory in the [XPath/XQuery] Core.
Core Grammar
The Core grammar productions for typeswitch
are:
| [33 (Core)] | TypeswitchExpr |
::= | "typeswitch" "(" Expr ")"
CaseClause+ "default" "$"
VarName "return" ExprSingle |
| [34 (Core)] | CaseClause |
::= | "case" "$" VarName "as"
SequenceType "return" ExprSingle |
Notation
For convenience, we introduce the following auxiliary grammar production.
| [81 (Formal)] | OptVarName |
::= | ("$" VarName)? |
Notation
To define normalization of case clauses to the [XPath/XQuery] Core, the following auxiliary mapping rules are used.
| [CaseClause]Case |
| == |
| CaseClause |
specifies that CaseClause is mapped to CaseClause, in the [XPath/XQuery] Core.
Normalization of a typeswitch expression guarantees that every branch has an associated $VarName. The following normalization rules add newly created variables that must not conflict with any variables already in scope.
| [ case $VarName as SequenceType return Expr ]Case |
| == |
| case $VarName as SequenceType return [ Expr ]Expr |
[
|
|||||
| == | |||||
|
Notation
For convenience, we use the following auxiliary grammar productions to denote case clauses in a typeswitch.
| [68 (Formal)] | FormalCaseClauses |
::= | (FormalCaseClause
FormalCaseClauses) |
FormalDefaultCaseClause |
| [69 (Formal)] | FormalCaseClause |
::= | "case" "$" VarName "as"
SequenceType "return" Expr |
| [70 (Formal)] | FormalDefaultCaseClause |
::= | "default" "$" VarName
"return" Expr |
The following judgments
is used in the static semantics of typeswitch. It indicates that under the static environment statEnv, and with the input type of the typeswitch being Type1, the given case clause yields the type Type.
The following judgment
is used in the dynamic semantics of typeswitch. It indicates that under the dynamic environment dynEnv, with the input value of the typeswitch being Value1, the given case clauses yield the value Value2.
The static typing rules for the typeswitch expression are simple. Each case clause and the default clause of the typeswitch is typed independently. The type of the entire typeswitch expression is the union of the types of all the clauses.
|
||||||
|
|
||||||
statEnv |-
|
To type one case clause, the case variable is assigned the type of the case clause CaseType and the body of the clause is typed in the extended environment. Thus, the type of a case clause is independent of the type of the input expression.
|
||||
|
|
||||
| statEnv |- Type0 case case $VarName as SequenceType return Expr : Type |
To type the default clause, the variable is assigned the type of the input expression and the body of the default clause is typed in the extended environment.
|
|||
|
|
|||
| statEnv |- Type0 case default $VarName return Expr : Type |
The evaluation of a typeswitch proceeds as follows. First, the
input expression is evaluated, yielding an input value. The
effective case is the first case
clause such
that the input value matches the SequenceType in the
case
clause. The return
clause of the
effective case is evaluated and the value of the
return
expression is the value of the typeswitch
expression.
|
|||
|
|
|||
| dynEnv |- typeswitch (Expr) FormalCaseClauses => Value1 |
If the value matches the sequence type, the following rule
applies: It extends the dynamic environment by binding the variable
Variable to Value0 and evaluates the body of the
return
clause.
|
|||||
|
|
|||||
| dynEnv |- Value0 against case $VarName as SequenceType return Expr FormalCaseClauses => Value1 |
If the value does not match the sequence type, the current case is not evaluated, and the remaining case clauses are evaluated in order by applying the inference rule recursively.
|
||
|
|
||
| dynEnv |- Value0 against case $VarName as SequenceType return Expr FormalCaseClauses => Value1 |
The last rule states that the default
branch of a
typeswitch expression always evaluates to the value of its
return
clause.
Introduction
The cast
expression can be used to convert a value
to a specific datatype. It changes both the type and value of the
result of an expression, and can only be applied to an atomic
value.
| [57 (XQuery)] | CastExprXQ |
::= | UnaryExpr ( "cast"
"as" SingleType )? |
| [117 (XQuery)] | SingleTypeXQ |
::= | AtomicType
"?"? |
Core Grammar
The Core grammar productions for cast
expressions
are:
| [39 (Core)] | CastExpr |
::= | ValueExpr ( "cast" "as"
SingleType )? |
| [74 (Core)] | SingleType |
::= | AtomicType
"?"? |
The normalization of cast applies atomization to its argument. The type declaration asserts that the result is a single atomic value. The second normalization rule applies when the target type is optional.
| [Expr cast as AtomicType ]Expr | ||
| == | ||
|
| [Expr cast as AtomicType? ]Expr | ||||
| == | ||||
|
The static typing rule of cast
expression is as
follows. The type of a Core cast
expression is always
the target type. Note that a cast
expression can fail
at run-time if the given value cannot be cast to the target
type.
|
|
| statEnv |- Expr cast as AtomicType : AtomicType |
Notation
The dynamic semantics of cast
expressions is
defined in Section 17
CastingFO. The semantics of cast
expressions depends on the type of the input value and on the
target type. For any source and target primitive types, the
casting table in Section 17
CastingFO indicates whether the cast
from the source type to the target type is permitted. When a cast
is permitted, the detailed dynamic evaluation rules for cast in
Section 17
CastingFO are applied. We refer to
those rules using an auxiliary judgment defined as follows.
The judgment
holds if AtomicValue1 can be cast to type AtomicType, resulting in the new value AtomicValue2 according to the rules in Section 17 CastingFO.
|
|||
|
|
|||
| dynEnv |- Expr cast as AtomicType => AtomicValue2 |
| [56 (XQuery)] | CastableExprXQ |
::= | CastExpr ( "castable"
"as" SingleType )? |
Castable expressions check whether a value can be cast to a given type.
Core Grammar
The Core grammar production for castable is:
| [38 (Core)] | CastableExpr |
::= | CastExpr ( "castable"
"as" SingleType )? |
The normalization of castable simply maps its expression argument.
The type of a Core castable
expression is always a
boolean.
|
|
statEnv |- Expr castable as
AtomicType :
xs:boolean |
Notation
The auxiliary judgment:
holds when Value can be atomized and cast to SingleType. Its definition depends on the cast value to type judgment.
|
|||
|
|
|||
|
If the value of the operand expression can be cast to the given
type, then the castable
expression evaluates to
true.
|
|||
|
|
|||
|
Otherwise, 'castable as' evaluates to false.
Constructor functions provide an alternative syntax for casting.
Notation
Calls to constructor functions are normalized differently from other function calls, so we introduce an auxiliary judgment to detect whether the function being called is a constructor function.
This judgment holds when the expanded function name maps to an atomic type in the in-scope schema types.
|
||
|
|
||
| statEnv |- expanded-QName denotes a constructor function |
Constructor functions for atomic types are normalized to
explicit cast as
expressions. Note that the following
normalization rule requires to resolve the name of the function
call and confirm that it denotes a constructor function in the
static context.
|
|||
|
|
|||
| statEnv |- [QName(ExprSingle1)]Expr = [ExprSingle1 cast as QName?]Expr |
| [55 (XQuery)] | TreatExprXQ |
::= | CastableExpr (
"treat" "as" SequenceType
)? |
Introduction
The expression "Expr treat as SequenceType", can be used to change the static type of the result of an expression without changing its value. The treat-as expression raises a dynamic error if the dynamic type of the input value does not match the specified type.
Treat as expressions are normalized to typeswitch expressions. Note that the following normalization rule uses a variable $fs:new, which is a newly created variable that does not conflict with any variables already in scope.
| [63 (XQuery)] | ValidateExprXQ |
::= | "validate" ValidationMode? "{" Expr "}" |
| [64 (XQuery)] | ValidationModeXQ |
::= | "lax" | "strict" |
Core Grammar
The Core grammar productions for validate are:
| [41 (Core)] | ValidateExpr |
::= | "validate" ValidationMode? "{" Expr "}" |
| [42 (Core)] | ValidationMode |
::= | "lax" | "strict" |
A validate
expression validates its argument with
respect to the in-scope schema definitions, using the schema
validation process described in [Schema Part
1]. The argument to a validate expression must be either an
element or a document node. Validation replaces all nodes with new
nodes that have their own identity, the type
annotationXQ, and default values
created during the validation process.
A validate expression with no validation mode is normalized into a validate expression with the validation mode set to strict.
Static typing of the validate operation begins with the following rule. We infer the type of the argument expression, and ensure that it is consistent with a run-time argument that is either an element or a well-formed document node (i.e., with only one root element and no text nodes). Then we hand off the type and the validation mode to the validate judgment.
|
||||
|
|
||||
|
Because the type of the argument expression may be a union of multiple element and document types, the judgment:
extracts the prime type of the argument type, applies the validate item type judgment to each type in the union, and yields the union of the results.
|
||||||
|
|
||||||
|
The judgement
does a case analysis on the different item types that it can encounter.
|
|||
|
|
|||
|
|
|||
|
|
|||
|
|
|
||
|
The normative dynamic semantics of validation is specified in Section 3.13 Validate ExpressionsXQ. The effect of validation of a data model value is equivalent to:
serialization of the data model, as described in [XSLT 2.0 and XQuery 1.0 Serialization (Second Edition)], followed by
validation of the serialized value into a Post-Schema Validated Infoset, as described in [Schema Part 1], followed by
construction of a new data model value, as described in [XQuery 1.0 and XPath 2.0 Data Model (Second Edition)].
The above steps are expressed formally by the "erasure" and
"annotation" judgments. Formally, validation removes existing type
annotations from nodes ("erasure"), and it re-validates the
corresponding data model instance, possibly adding new type
annotations to nodes ("annotation"). Both erasure and annotation
are described formally in [F
Auxiliary Judgments for Validation]. Indeed, the
conjunction of erasure and annotation provides a formal model for a
large part of actual schema validation. The semantics of the
validate
expression is specified as follows.
In the first premise below, the expression to validate is evaluated. The resulting value must be an element or document node. The second premise constructs a new value in which all existing type annotations have been erased. The third premise determines the element type that corresponds to the element node's name in the given validation mode. The last premise validates erased element node with the type against which it is validated, using the annotate as judgment, yielding the final validated element.
|
||||||
|
|
||||||
| dynEnv |- validate ValidationMode { Expr } => ElementValue3 |
The rule for validating a document node is similar to that for validating an element node.
|
||||||
|
|
||||||
| dynEnv |- validate ValidationMode { Expr } => document { ElementValue3 } |
Introduction
An extension expression is an expression whose semantics are implementation-defined. An extension expression consists of one or more pragmas, followed by an expression enclosed in curly braces.
| [65 (XQuery)] | ExtensionExprXQ |
::= | Pragma+ "{" Expr? "}" |
| [66 (XQuery)] | PragmaXQ |
::= | "(#" S? QName (S
PragmaContents)?
"#)" |
| [67 (XQuery)] | PragmaContentsXQ |
::= | (Char* - (Char* '#)'
Char*)) |
Core Grammar
The Core grammar productions for ExtensionExpr are:
| [43 (Core)] | ExtensionExpr |
::= | Pragma+ "{" Expr? "}" |
| [44 (Core)] | Pragma |
::= | "(#" S? QName (S PragmaContents)? "#)" |
| [45 (Core)] | PragmaContents |
::= | (Char* - (Char* '#)'
Char*)) |
Extension expressions are normalized as extension expressions in the [XPath/XQuery] Core.
If the extension expression does not contain any expression,
this is normalized into an extension expression with a call to the
fn:error
function.
| [Pragma+ { }]Expr |
| == |
Pragma+ {
fn:error () } |
If at least one of the pragmas is recognized, the static semantics are implementation-defined.
If none of the pragmas is recognized, the static semantics are the same as for the input expression. In both cases, the static typing must be applied on the input expression, possibly raising the corresponding type errors.
|
|||
|
|
|||
| statEnv |- Pragma+ { Expr } : Type2 |
The QName of a pragma must resolve to a namespace URI and local name, using the statically known namespaces. If at least one of the pragmas is recognized, the dynamic semantics is implementation-defined.
|
||
|
|
||
| dynEnv |- Pragma+ { Expr } => Value |
If none of the pragmas is recognized, the dynamic semantics of an ExtensionExpr are the same as evaluating the given expression.
The organization of this section parallels the organization of Section 4 Modules and PrologsXQ.
Introduction
XQuery supports modules as defined in Section 4 Modules and PrologsXQ. A main moduleXQ contains a PrologXQ followed by a query bodyXQ. A query has exactly one main module. In a main module, the query bodyXQ can be evaluated, and its value is the result of the query. A library moduleXQ contains a module declaration followed by a PrologXQ.
The Prolog is a sequence of declarations that affect query processing. The Prolog can be used, for example, to declare namespace prefixes, import types from XML Schemas, and declare functions and variables. Namespace declarations and schema imports always precede function and variable declarations, as specified by the following grammar productions.
| [1 (XQuery)] | ModuleXQ |
::= | VersionDecl?
(LibraryModule | MainModule) |
| [3 (XQuery)] | MainModuleXQ |
::= | Prolog QueryBody |
| [4 (XQuery)] | LibraryModuleXQ |
::= | ModuleDecl Prolog |
| [6 (XQuery)] | PrologXQ |
::= | ((DefaultNamespaceDecl |
Setter | NamespaceDecl | Import) Separator)* ((VarDecl | FunctionDecl | OptionDecl) Separator)* |
| [7 (XQuery)] | SetterXQ |
::= | BoundarySpaceDecl | DefaultCollationDecl |
BaseURIDecl | ConstructionDecl | OrderingModeDecl | EmptyOrderDecl | CopyNamespacesDecl |
| [8 (XQuery)] | ImportXQ |
::= | SchemaImport |
ModuleImport |
| [9 (XQuery)] | SeparatorXQ |
::= | ";" |
| [30 (XQuery)] | QueryBodyXQ |
::= | Expr |
Function declarations are globally scoped, that is, the use of a function name in a function call may precede declaration of the function. Variable declarations are lexically scoped, i.e., variable declarations must precede variable uses.
Core Grammar
The module declarations and prolog are processed as part of the static and dynamic context processing. In addition, normalization of prolog declarations is performed into a simplified formal grammar given below. As a result, the XQuery core does not need to include the prolog and module declarations. The entry point for the core grammar is the Expr non-terminal, as given in [4 Expressions].
Notation
Modules are identified and can be imported using a target namespace (a URI). In [XPath/XQuery], the process by which a module is obtained from a given target namespace is implementation defined. In this specification, we use the following auxiliary judgment to model that implementation defined process.
The judgment:
holds if Module1 ... Modulen are the modules associated to the target namespace AnyURI, and such as Modulei does not depend directly, or transitively on any module after it. (See [XQuery 1.0: An XML Query Language (Second Edition)] for the formal definition of whether a module directly depends on another)
Notation
The XQuery Prolog requires that declarations appear in a particular order. In the Formal Semantics, it is simpler to assume the declarations can appear in any order, as it does not change their semantics -- we simply assume that an XQuery parser has enforced the required order.
The Prolog contains a variety of declarations that specify the initial static and dynamic context of the query. The following formal grammar productions represent any Prolog declaration.
| [71 (Formal)] | PrologDeclList |
::= | (PrologDecl Separator PrologDeclList)? |
| [72 (Formal)] | PrologDecl |
::= | DefaultCollationDecl |
The function []PrologDecl takes a prolog declaration and maps it into its equivalent declaration in the Core grammar.
| [PrologDecl1]PrologDecl |
| == |
| PrologDecl2 |
The following auxiliary judgments are applied when statically processing the declarations in the prolog. The effect of the judgment is to process each prolog declaration in order, constructing a new static environment from the static environment constructed from previous prolog declarations.
The judgment:
holds if for the given module with namespace AnyURI, and under the static environment statEnv1, the sequence of prolog declarations PrologDeclList yields the static environment statEnv2 and the normalized sequence of prolog declarations in the Core grammar.
The judgment:
holds if under the static environment statEnv1, the single prolog declaration PrologDecl yields the new static environment statEnv2.
Notation
Because functions can be mutually referential, function signatures must be defined in the static environment before static type analysis is applied to the function bodies. The following judgment is used to extend the static environment with the appropriate function signatures. That judgment is used when computing the static context for a given module before applying static context processing.
The judgment:
holds if extending the static environment statEnv1 with the function signatures declared in PrologDeclList yields the new static environment statEnv2.
This judgment is defined as follows. In case there is no declaration, the static environment is returned unchanged.
If the case of a namespace declaration, the static context is extended with the corresponding namespace binding.
|
||||
|
|
||||
| statEnv |- PrologDecl ; PrologDeclList =>sigs statEnv2 |
If the case of a function declaration, the static context is extended with the corresponding signature.
|
||||
|
|
||||
| statEnv |- PrologDecl ; PrologDeclList =>sigs statEnv2 |
|
|||||||||
|
|
|||||||||
| statEnv |- FunctionDecl =>sigs statEnv1 |
For all other kinds of declarations, the static context is left unchanged.
|
||
|
|
||
| statEnv |- PrologDecl ; PrologDeclList =>sigs statEnv |
In case of a function declaration, the static context is extended with the corresponding function signature.
Prolog declarations are processed in the order they are encountered. The normalization of a prolog declaration PrologDecl depends on the static context processing of all previous prolog declarations. In turn, static context processing of PrologDecl depends on the normalization of the PrologDecl. For example, because variables are lexically scoped, the normalization and static context processing of a variable declaration depends on the normalization and static context processing of all previous variable declarations. Therefore, the normalization phase and static context processing are interleaved, with normalization preceding static context processing for each prolog declaration.
The following inference rules express this dependency. The first rule specifies that for an empty sequence of prolog declarations, the initial static environment is left unchanged.
The next two rules interleaves normalization and static context processing. The result of static context processing and normalization is a static context and the normalized prolog declarations. In case the declaration is a module import, the URI for the current module is passed to the static context processing rule. This allows to avoid self-import, which is handled globally (See rules for building the context for module declarations in [5.2 Module Declaration]).
|
|||||
|
|
|||||
| AnyURI ; statEnv |- PrologDecl ; PrologDeclList =>stat statEnv2 with PrologDecl1 ; PrologDeclList1 |
|
|||||
|
|
|||||
| AnyURI ; statEnv |- PrologDecl ; PrologDeclList =>stat statEnv2 with PrologDecl1 ; PrologDeclList1 |
Static typing of a main module follows context processing and normalization. Context processing and normalization of a main module applies the rules above to the prolog, then using the resulting static environment statEnv, the query body is normalized into a Core expression, and the static typing rules are applied to this Core expression.
|
||||
|
|
||||
| PrologDeclList QueryBody : Type |
Notation
Similarly, the judgment:
holds if under the dynamic environment dynEnv1, the sequence of prolog declarations PrologDeclList yields the dynamic environment dynEnv2.
The judgment:
holds if under the dynamic environment dynEnv, the single prolog declaration PrologDecl yields the new dynamic environment dynEnv1.
The rules for initializing the dynamic context are as follows. The first rule specifies that for an empty sequence of prolog declarations, the dynamic environment is left unchanged.
The second rule simply computes the dynamic environment by processing the prolog declarations in order.
|
|||
|
|
|||
| dynEnv |- PrologDecl ; PrologDeclList =>dyn dynEnv2 |
Dynamic evaluation of a main module applies the rules for dynamic-context processing to the prolog declarations, then using the resulting dynamic environment dynEnv, the dynamic evaluation rules are applied to the normalized query body.
|
|||||
|
|
|||||
|
Notation
We define a new judgment that maps a module's target namespace (or a main module) to the corresponding module's static environment:
We also define a new judgment that maps a module's target namespace (or a main module) to the corresponding module's dynamic environment:
For a main module, those judgments are defined as follows.
|
||
|
|
||
|
|
||
|
|
||
|
For a library module, those judgments are defined in [5.11 Module Import].
| [2 (XQuery)] | VersionDeclXQ |
::= | "xquery" "version" StringLiteral ("encoding" StringLiteral)? Separator |
Introduction
A version declaration specifies the applicable XQuery syntax and semantics for a module. An XQuery implementation must raise a static error when processing a query labeled with a version that the implementation does not support. This document applies to XQuery 1.0 only and does not specify this static error formally. Verifying whether the proper version declaration is used is not formally specified.
Introduction
| [5 (XQuery)] | ModuleDeclXQ |
::= | "module" "namespace" NCName "=" URILiteral Separator |
We assume that the static-context processing and dynamic-context processing described in [5 Modules and Prologs] are applied to all library modules before the normalization, static context processing, and dynamic context processing of the main module. That is, at the time an "import module" declaration is processed, we assume that the static and dynamic context of the imported module is already available. This assumption does not require or assume separate compilation of modules. An implementation might process all or some imported modules statically (i.e., before the importing module is identified) or dynamically (i.e., when the importing module is identified and processed).
Core Grammar
The core grammar production for module declarations is:
| [1 (Core)] | ModuleDecl |
::= | "module" "namespace" NCName "=" URILiteral Separator |
| [2 (Core)] | Separator |
::= | ";" |
Module declarations are left unchanged through normalization.
| [ModuleDecl]PrologDecl |
| == |
| ModuleDecl |
The effect of a module declaration is to apply the static context processing rules defined in [5 Modules and Prologs] to the module's prolog. The resulting static context is then available to any importing module.
The module declaration extends the prolog with a namespace declaration that binds the module's prefix to its target namespace (a URI), then computes the static context for the complete module.
|
||||||||||
|
|
||||||||||
|
Note that the rule above and the rules for static context processing of an "import module" declaration in [5.11 Module Import] are mutually recursive.
The dynamic context processing of a module declaration is similar to that of static processing. The module declaration extends the prolog with a namespace declaration that binds the module's prefix to its target namespace (a URI), then computes the dynamic context for the complete module.
|
|||||||||
|
|
|||||||||
|
Note that the rule above and the rules for dynamic context processing of an "import module" declaration in [5.11 Module Import] are mutually recursive.
| [11 (XQuery)] | BoundarySpaceDeclXQ |
::= | "declare" "boundary-space" ("preserve" |
"strip") |
The semantics of a boundary-space declaration is not specified formally.
| [19 (XQuery)] | DefaultCollationDeclXQ |
::= | "declare" "default" "collation" URILiteral |
Core Grammar
The core grammar production for default collation declarations is:
| [11 (Core)] | DefaultCollationDecl |
::= | "declare" "default" "collation" URILiteral |
Default collation declarations are left unchanged through normalization.
| [DefaultCollationDecl]PrologDecl |
| == |
| DefaultCollationDecl |
The default collation declaration updates the collations environment component within the static environment. The collations environment component is used by several functions in [XQuery 1.0 and XPath 2.0 Functions and Operators (Second Edition)], but is not used in the Formal Semantics.
|
||||
|
|
||||
|
The default collation declaration does not affect the dynamic context.
| [20 (XQuery)] | BaseURIDeclXQ |
::= | "declare" "base-uri" URILiteral |
Core Grammar
The core grammar production for base uri declarations is:
| [12 (Core)] | BaseURIDecl |
::= | "declare" "base-uri" URILiteral |
Base URI declarations are left unchanged through normalization.
| [BaseURIDecl]PrologDecl |
| == |
| BaseURIDecl |
A base URI declaration specifies the base URI property of the static context, which is used when resolving relative URIs within a module.
|
|||
|
|
|||
|
The base URI declaration does not affect the dynamic context.
| [25 (XQuery)] | ConstructionDeclXQ |
::= | "declare" "construction" ("strip" |
"preserve") |
Core Grammar
The core grammar production for construction declarations is:
| [17 (Core)] | ConstructionDecl |
::= | "declare" "construction" ("strip" |
"preserve") |
Notation
For convenience, we introduce the following auxiliary grammar production.
| [89 (Formal)] | ConstructionMode |
::= | "preserve" | "strip" |
Construction declarations are left unchanged through normalization.
| [ConstructionDecl]PrologDecl |
| == |
| ConstructionDecl |
The construction declaration modifies the construction mode in the static context.
| statEnv1 = statEnv + constructionMode( ConstructionMode) | ||
|
|
||
|
The construction declaration does not have any effect on the dynamic context.
| [14 (XQuery)] | OrderingModeDeclXQ |
::= | "declare" "ordering" ("ordered" |
"unordered") |
Core Grammar
The core grammar production for ordering mode declarations is:
| [6 (Core)] | OrderingModeDecl |
::= | "declare" "ordering" ("ordered" |
"unordered") |
Ordering mode declarations are left unchanged through normalization.
| [OrderingModeDecl]PrologDecl |
| == |
| OrderingModeDecl |
The ordering mode declaration does not have any effect on the static context.
The ordering mode declaration does not have any effect on the dynamic context.
| [15 (XQuery)] | EmptyOrderDeclXQ |
::= | "declare" "default" "order" "empty" ("greatest" |
"least") |
Core Grammar
The core grammar production for empty order declarations is:
| [7 (Core)] | EmptyOrderDecl |
::= | "declare" "default" "order" "empty" ("greatest" |
"least") |
Empty order declarations are left unchanged through normalization.
| [EmptyOrderDecl]PrologDecl |
| == |
| EmptyOrderDecl |
The empty order declaration does not have any effect on the static context.
The empty order declaration does not have any effect on the dynamic context.
| [16 (XQuery)] | CopyNamespacesDeclXQ |
::= | "declare" "copy-namespaces" PreserveMode "," InheritMode |
| [17 (XQuery)] | PreserveModeXQ |
::= | "preserve" | "no-preserve" |
| [18 (XQuery)] | InheritModeXQ |
::= | "inherit" | "no-inherit" |
Core Grammar
The core grammar productions for copy-namespaces declarations are:
| [8 (Core)] | CopyNamespacesDecl |
::= | "declare" "copy-namespaces" PreserveMode "," InheritMode |
| [9 (Core)] | PreserveMode |
::= | "preserve" | "no-preserve" |
| [10 (Core)] | InheritMode |
::= | "inherit" | "no-inherit" |
Copy-namespace declarations are left unchanged through normalization.
| [CopyNamespacesDecl]PrologDecl |
| == |
| CopyNamespacesDecl |
The copy-namespace declaration does not have any effect on the static context.
The copy-namespace declaration does not have any effect on the dynamic context.
| [21 (XQuery)] | SchemaImportXQ |
::= | "import" "schema" SchemaPrefix? URILiteral ("at" URILiteral ("," URILiteral)*)? |
| [22 (XQuery)] | SchemaPrefixXQ |
::= | ("namespace" NCName
"=") | ("default" "element" "namespace") |
The semantics of Schema Import is described in terms of the [XPath/XQuery] type system. The process of converting an XML Schema into a sequence of type declarations is described in Section [D Importing Schemas]. This section describes how the resulting sequence of type declarations is added into the static context when the Prolog is processed.
Core Grammar
The Core grammar productions for schema imports are:
| [13 (Core)] | SchemaImport |
::= | "import" "schema" SchemaPrefix? URILiteral ("at" URILiteral ("," URILiteral)*)? |
| [14 (Core)] | SchemaPrefix |
::= | ("namespace" NCName "=")
| ("default" "element" "namespace") |
Schema imports are left unchanged through normalization.
| [SchemaImport]PrologDecl |
| == |
| SchemaImport |
Notation
For convenience, we introduce the following auxiliary grammar productions.
| [16 (Formal)] | LocationHints |
::= | "at" URILiteral (","
URILiteral)* |
| [82 (Formal)] | OptLocationHints |
::= | LocationHints? |
Notation
The following auxiliary judgments are used when processing schema imports.
The judgment:
holds if under the static environment statEnv1, the sequence of type definitions Definitions yields the new static environment statEnv2.
The judgment:
holds if under the static environment statEnv1, the single definition Definition yields the new static environment statEnv2.
A schema imported into a query is first mapped into the [XPath/XQuery] type system, which yields a sequence of XQuery type definitions. The rules for mapping the imported schema begin in [D.2 Schemas as a whole]. Each type definition in an imported schema is then added to the static environment.
|
|||
|
|
|||
|
The schema import declaration may also assign an element/type namespace prefix to the URI of the imported schema, or assign the default element namespace to the URI of the imported schema.
|
|||||
|
|
|||||
|
|
|||||
|
|
|||||
|
An empty sequence of type definitions yields the input environment.
Each type definition is added into the static environment.
|
|||
|
|
|||
|
Each type, element, or attribute declaration is added respectively to the type, element and attribute declarations components of the static environment.
|
|||
|
|
|||
|
|
|||
|
|
|||
|
|
|||
|
|
|||
|
Note that it is a static error to import two schemas that both define the same name in the same symbol space and in the same scope. That is multiple top-level definitions of the same type, element, or attribute name raises a static error. For instance, a query may not import two schemas that include top-level element declarations for two elements with the same expanded name.
The schema import declarations do not affect the dynamic context.
| [23 (XQuery)] | ModuleImportXQ |
::= | "import" "module" ("namespace" NCName "=")? URILiteral ("at" URILiteral ("," URILiteral)*)? |
Introduction
The effect of an "import module" declaration is to extend the importing module's dynamic (and static) context with the global variables (and their types) and the functions (and their signatures) of the imported module. Module import is not transitive, only the global variables and functions declared explicitly in the imported module are available in the importing module. Also, module import does not import schemas, therefore the importing module must explicitly import any schemas on which the imported global variables or functions depend.
Core Grammar
The core grammar production for module imports is:
| [15 (Core)] | ModuleImport |
::= | "import" "module" ("namespace" NCName "=")? URILiteral ("at" URILiteral ("," URILiteral)*)? |
Module imports are left unchanged through normalization.
| [ModuleImport]PrologDecl |
| == |
| ModuleImport |
Notation
The rules below depend on the following auxiliary functions which are used to import the proper fragment of the static context.
The function fs:local-variables
(statEnv, AnyURI) returns all the (expanded-QName, Type) pairs in statEnv.varType such that the URI part of the variable's
expanded-QName equals the given URI, that is, the variables that
are declared locally in the module with the given namespace
URI.
The function fs:local-functions
(statEnv, AnyURI) returns all the
(FunctionKey, FunctionSig) pairs in statEnv.funcType such that the URI part of the function's
expanded-QName equals the given URI, that is, the function
signatures that are declared locally in the module with the given
namespace URI.
Notation
The following auxiliary judgments is used to extend a given static environment with the static environment from an imported module.
The judgment
holds if extending the environment statEnv1 with the environment statEnv2 yields the environment statEnv3 under the given namespace uri AnyURI.
This judgment is defined as follows.
|
|||||
|
|
|||||
|
Notation
The rules below depend on the following auxiliary judgments.
The following rules add each variable explicitly declared in the imported module to the importing module's dynamic variable environment.
|
|
||
|
|
|||
|
|
|||
|
The following rules add each function explicitly declared in the imported module to the importing module's dynamic function environment.
|
|
||
|
|
|||
|
|
|||
|
Notation
The following auxiliary judgments is used to extend a given dynamic environment with the dynamic environment from an imported module.
The judgment
holds if extending the dynamic environment dynEnv1 with the dynamic environment dynEnv2 yields the dynamic environment dynEnv3 under the given namespace uri AnyURI.
This judgment is defined as follows.
|
||||
|
|
||||
|
The first set of premises below "look up" the static contexts of all the imported modules, as defined in [5.2 Module Declaration]. The second set of premises extend the input static context with the global variables and function signatures declared in the imported static contexts.
|
||||
|
|
||||
|
|
||||||
|
|
||||||
|
|
||||
|
|
||||
|
Note that the rules above and the rules for processing a library module in [5.2 Module Declaration] above are mutually recursive. It is possible to define the semantics in that way, since XQuery forbids the use of recursive modules.
During dynamic context processing, each variable and function
name is mapped to the special value
#IMPORTED
(AnyURI) to indicate that the
variable or function is defined in the imported module with the
given URI.
The first set of premises below "look up" the dynamic contexts of all the imported modules, as defined in [5.2 Module Declaration]. The second set of premises extend the input dynamic context with the global variables and functions declared in the imported dynamic contexts.
|
||||||||
|
|
||||||||
|
Note that the rule above and the rules for processing a library module in [5.2 Module Declaration] above are mutually recursive. It is possible to define the semantics in that way, since XQuery forbids the use of recursive modules.
| [10 (XQuery)] | NamespaceDeclXQ |
::= | "declare" "namespace" NCName "=" URILiteral |
Core Grammar
The core grammar production for namespace declarations is:
| [3 (Core)] | NamespaceDecl |
::= | "declare" "namespace" NCName "=" URILiteral |
Namespace declarations are left unchanged through normalization.
| [NamespaceDecl]PrologDecl |
| == |
| NamespaceDecl |
A namespace declaration adds a new (prefix,uri) binding in the namespace component of the static environment. All namespace declarations in the prolog are passive declarations. Namespace declaration attributes of element constructors are active declarations.
|
|||
|
|
|||
|
In case the URILiteral part of a namespace declaration is a zero-length string, the namespace prefix is marked as #UNDECLARED in the static context.
|
||
|
|
||
|
The namespace declaration does not affect the dynamic context.
| [12 (XQuery)] | DefaultNamespaceDeclXQ |
::= | "declare" "default" ("element" | "function") "namespace"
URILiteral |
Core Grammar
The core grammar production for default namespace declarations is:
| [4 (Core)] | DefaultNamespaceDecl |
::= | "declare" "default" ("element" | "function") "namespace"
URILiteral |
Default namespace declarations are left unchanged through normalization.
| [DefaultNamespaceDecl]PrologDecl |
| == |
| DefaultNamespaceDecl |
A default element namespace declaration changes the default element namespace component of the static environment. If the URI literal is the zero-length string, the default element namespace is set to the null namespace.
| statEnv1 = statEnv + default_elem_namespace(#NULL-NAMESPACE) | ||
|
|
||
|
|
||||
|
|
||||
|
A default function namespace declaration changes the default function namespace component of the static environment. If the URI literal is the zero-length string, the default function namespace is set to the null namespace.
| statEnv1 = statEnv + default_function_namespace(#NULL-NAMESPACE) | ||
|
|
||
|
|
||||
|
|
||||
|
Note that multiple declarations of the same namespace prefix in the Prolog result in a static error. However, a declaration of a namespace in the Prolog can override a prefix that has been predeclared in the static context.
Default namespace declarations do not affect the dynamic context.
| [24 (XQuery)] | VarDeclXQ |
::= | "declare" "variable" "$" QName TypeDeclaration? ((":=" ExprSingle) | "external") |
Core Grammar
The core grammar production for variable declarations is:
| [16 (Core)] | VarDecl |
::= | "declare" "variable" "$" QName TypeDeclaration? ((":=" ExprSingle) | "external") |
Normalization of a variable declaration normalizes its initializing expression, if it is present.
| [ declare variable $VarName as SequenceType := Expr ]PrologDecl |
| == |
| declare variable $VarName as SequenceType := [Expr]Expr |
| [ declare variable $VarName := Expr ]PrologDecl |
| == |
| declare variable $VarName := [Expr]Expr |
If an external variable declaration does not have a type
declaration it is treated as if the type declaration was
item()*
.
| [ declare variable $VarName external ]PrologDecl |
| == |
| declare variable $VarName as item()* external |
| [ declare variable $VarName as SequenceType external ]PrologDecl |
| == |
| declare variable $VarName as SequenceType external |
A variable declaration updates the variable component of the static context by associating the given variable with a static type.
If a variable declaration has an associated expression but does not have a type declaration, the static type of the variable is the static type of the expression.
|
||||
|
|
||||
|
If the variable declaration has an associated expression and has a type declaration, the static type of the variable is the specified type. The type of the expression must be a subtype of the declared type.
|
||||||
|
|
||||||
|
If the variable declaration is external and has a type declaration, the static type of the variable is the specified type.
|
||||
|
|
||||
|
To evaluate a variable declaration, its associated expression is evaluated, and the dynamic context is updated with the variable bound to the resulting value.
|
||||
|
|
||||
|
|
||||||
|
|
||||||
|
Dynamic evaluation does not apply to externally defined variables. The dynamic environment must provide the values of external variables in the initial dynamic context (dynEnvDefault).
Introduction
User-defined functions specify the name of the function, the names and types of the parameters, and the type of the result. The function body defines how the result of the function is computed from its parameters.
| [26 (XQuery)] | FunctionDeclXQ |
::= | "declare" "function" QName "(" ParamList? ")" ("as" SequenceType)? (EnclosedExpr |
"external") |
| [27 (XQuery)] | ParamListXQ |
::= | Param ("," Param)* |
| [28 (XQuery)] | ParamXQ |
::= | "$" QName TypeDeclaration? |
Core Grammar
The core grammar productions for function declarations are:
| [18 (Core)] | FunctionDecl |
::= | "declare" "function" QName
"(" ParamList? ")" ("as" SequenceType)? (EnclosedExpr | "external") |
| [19 (Core)] | ParamList |
::= | Param ("," Param)* |
| [20 (Core)] | Param |
::= | "$" QName TypeDeclaration? |
Notation
The following auxiliary mapping rule is used for the normalization of parameters in function declarations: []Param.
Parameters without a declared type are given the item()* sequence type.
| [$VarName]Param |
| == |
| $VarName as item()* |
| [$VarName as SequenceType ]Param |
| == |
| $VarName as SequenceType |
An empty parameter list is left unchanged.
| []Param |
| == |
A parameter list is normalized by applying the normalization rule to each parameter.
The parameter list and body of a user-defined function are all normalized into Core expressions.
|
|||
|
|
|||
| statEnv |- [ declare function QName ( ParamList? ) as SequenceType { Expr } ]PrologDecl = declare function QName ( [ParamList?]Param ) as SequenceType { [Expr]FunctionArgument(Type) } |
If the return type of the function is not provided, it is given
the item()*
sequence type.
| [declare function QName ( ParamList? ) { Expr }]PrologDecl |
| == |
| [declare function QName ( ParamList? ) as item()* { Expr }]PrologDecl |
Externally defined functions are normalized similarly.
| [ declare function QName ( ParamList? ) as SequenceType external]PrologDecl |
| == |
| declare function QName( [ParamList?]Param ) as SequenceType external |
| [declare function QName ( ParamList? ) external ]PrologDecl |
| == |
| [declare function QName ( ParamList? ) as item()* external ]PrologDecl |
Notation
We use the following auxiliary judgment during static context processing and static type analysis of function declarations.
The judgment:
holds if the function declaration FunctionDecl with the signature FunctionSig has the type Type.
Static context processing accesses the function signature from the static context, and checks that the function declaration corresponds to the declared type.
|
|||
|
|
|||
| statEnv |- FunctionDecl =>stat statEnv1 |
Note that the static context processing is performing type checking of the function, as defined below. Note also that the type checking is done in the new environment in which the function declaration has been added which ensures that recursive calls are type-checked properly.
The static typing rules for function bodies follow normalization and processing of the static context. The static typing rules below construct a new environment in which each parameter has the given expected type, then the static type of the function's body is computed under the new environment. The function body's type must be a subtype of the expected return type. If static typing fails, a static type error is raised. Otherwise, static typing of the function has no other effect, as function signatures are already inside the static environment.
|
|||
|
|
|||
| statEnv |- function declaration declare function QName () as SequenceTyper { Expr } with signature declare function expanded-QName() as Typer : Typer |
|
||||||
|
|
||||||
| statEnv |- function declaration declare function QName ($VarName1 as SequenceType1, ···, $VarNamen as SequenceTypen) as SequenceTyper { Expr } with signature declare function expanded-QName(Type1, ..., Typen) as Typer : Typer |
The bodies of external functions are not available and therefore cannot by type checked. To ensure type soundness, the implementation must guarantee that the value returned by the external function matches the expected return type.
|
|
| statEnv |- function declaration declare function QName () as SequenceTyper external with signature declare function expanded-QName() as Typer : Typer |
|
||||
|
|
||||
| statEnv |- function declaration declare function QName ( $VarName1 as SequenceType1, ···, $VarNamen as SequenceTypen ) as SequenceTyper external with signature declare function expanded-QName(Type1, ..., Typen) as Typer : Typer |
A function declaration updates the dynamic context. The function name with arity N is associated with the given function body. The number of arguments is required, because XQuery permits overloading of function names as long as each function signature has a different number of arguments.
|
|||
|
|
|||
| dynEnv |- declare function QName () as SequenceTyper { Expr } =>dyn dynEnv1 |
|
||||||
|
|
||||||
| dynEnv |- declare function QName ( $VarName1 as SequenceType1, ···, $VarNamen as SequenceTypen ) as SequenceTyper { Expr } =>dyn dynEnv1 |
An external function declaration does not affect the dynamic environment. The implementation must support the declared external functions.
|
|
| dynEnv |- declare function QName ( $VarName1 as SequenceType1, ···, $VarNamen as SequenceTypen ) as SequenceTyper external =>dyn dynEnv |
The dynamic semantics of a function body are applied when the function is called, as described in [4.1.5 Function Calls].
| [13 (XQuery)] | OptionDeclXQ |
::= | "declare" "option" QName
StringLiteral |
Core Grammar
The core grammar production for option declarations is:
| [5 (Core)] | OptionDecl |
::= | "declare" "option" QName
StringLiteral |
Option declarations are left unchanged through normalization.
| [OptionDecl]PrologDecl |
| == |
| OptionDecl |
An option declaration does not have any effect on the static context.
An option declaration does not have any effect on the dynamic context.
The XQuery Formal Semantics is intended primarily as a component that can be used by [XQuery 1.0: An XML Query Language (Second Edition)], or a host language of [XML Path Language (XPath) 2.0 (Second Edition)]. Therefore, the XQuery Formal Semantics relies on specifications that use it (such as [XPath 2.0], [XSLT 2.0], and [XQuery]) to specify conformance criteria in their respective environments. Specifications that set conformance criteria for their use of the formal semantics must not relax the constraints expressed in this specification.
This specification normatively defines the static typing feature which can be used in [XQuery 1.0: An XML Query Language (Second Edition)] or a host language of [XML Path Language (XPath) 2.0 (Second Edition)]. The static typing feature is specified using the static typing judgment introduced in [3.2.3 Static typing judgment].
In some cases, the static typing rules are not very precise
(see, for example, the type inference rules for the ancestor
axes—parent, ancestor, and ancestor-or-self—and for the function
fn:root
). If an implementation supports a static
typing extension, it must always provide a more precise type than
the one defined in this specification.
This constraint is formally expressed as follows. A static typing extension Expr :ext Type must be such that for every expression Expr the following holds.
Note:
It is not recommended for a static typing extension to change
the static typing behavior of expressions that specify a type
explicitly (treat as
, cast as
,
typeswitch
, function parameters, and type declarations
in variable bindings), since the purpose of those expressions is to
impose a specific type.
This section defines the auxiliary functions required to define the formal semantics of [XPath/XQuery], and gives special normalization and static typing rules for some functions in [XQuery 1.0 and XPath 2.0 Functions and Operators (Second Edition)].
Remember from [4.1.5 Function Calls] that the following rules operate after namespace resolution for the function name, and directly over the input type of the parameters. In the rest of the section, we will use the following shortcuts notations for specific relevant URIs:
FN-URI
for functions from the [XQuery 1.0 and XPath 2.0 Functions and
Operators (Second Edition)] document.
OP-URI
for operators from the [XQuery 1.0 and XPath 2.0 Functions and
Operators (Second Edition)] document.
FS-URI
for formal semantics functions.
Introduction
This section gives the definition and semantics of functions that are used in the formal semantics but are not in [XQuery 1.0 and XPath 2.0 Functions and Operators (Second Edition)]. Their dynamic semantics are defined in the same informal style as in the [XQuery 1.0 and XPath 2.0 Functions and Operators (Second Edition)] document. The static semantics of some formal-semantics functions require custom static typing rules.
convert-operand
functionfs:convert-operand
($actual
as
xs:anyAtomicType?
, $expected
as
xs:anyAtomicType
) as
xs:anyAtomicType ?
The formal-semantics function fs:convert-operand
converts the operands of arithmetic and comparison operators as
follows:
If $actual
is the empty sequence, returns the empty
sequence.
If $actual
is an instance of type xs:untypedAtomic
, then
if $expected
is an instance of type xs:untypedAtomic
or
xs:string
, returns $actual
cast to
xs:string
;
if $expected
is of numeric type, returns
$actual
cast to xs:double
otherwise returns $actual
cast to the type of
$expected
.
Otherwise, returns $actual
.
To analyze a call to fs:convert-operand
,
we extract the prime type of the static type of each of the two
arguments. (Each prime type will be a union of atomic types.) We
consider all possible pairs formed by taking one atomic type from
each prime type, apply the convert_operand judgment to each pair, form
the union of the results, and adjust that by the quantifier of the
first argument's type.
|
|||||||||||||
|
|
|||||||||||||
|
The auxiliary judgment:
is the static analog of the fs:convert-operand
function. It is defined by the following rules.
No conversion is needed if the first argument isn't an instance
of type xs:untypedAtomic
.
|
||
|
|
||
|
The remaining rules cover the cases when the first argument
is an instance of type xs:untypedAtomic
. The
outcome depends on the type of the second argument.
If the second argument is of type xs:untypedAtomic
or
xs:string
, the first is converted to a string.
|
|||
|
|
|||
|
If the second argument is numeric, the first is converted to
xs:double
.
|
|||
|
|
|||
|
Otherwise, the first argument is converted to the type of the second argument.
|
|||
|
|
|||
|
convert-simple-operand
functionfs:convert-simple-operand
($actual
as
xs:anyAtomicType
*
, $expected
as
xs:anyAtomicType
) as
xs:anyAtomicType *
The formal-semantics function fs:convert-simple-operand
is used to convert the value of the $actual
argument
such that it matches the type of the $expected
argument (or matches a sequence of that type).
The dynamic semantics of this function are as follows:
For each item in $actual
argument that is of type
xs:untypedAtomic, that item is cast to the type of the
$expected
argument, and the resulting sequence is
returned.
The following static typing rules correspond to the dynamic semantics rules given above.
|
|||
|
|
|||
statEnv |- (FS-URI ,"convert-simple-operand ")(Type1,
Type2) : Type3
· quantifier(Type1) |
distinct-doc-order
functionfs:distinct-doc-order
($nodes
as
node
*
) as
node *
The fs:distinct-doc-order
function sorts its input sequence of nodes by document order and
removes duplicates.
The fs:distinct-doc-order
function expects a sequence of nodes as input. The resulting type
is computed using prime
and quantifier, which
are defined in [8.4 Judgments for FLWOR
and other expressions on sequences].
distinct-doc-order-or-atomic-sequence
functionfs:distinct-doc-order-or-atomic-sequence
($item
as
item()*
) as
item()*
The fs:distinct-doc-order-or-atomic-sequence
function operates on either an homogeneous sequence of nodes or an
homogeneous sequence of atomic values. If the input is a sequence
of nodes, is sorts those nodes by document order and removes
duplicates, using the fs:distinct-doc-order function. If it is a
sequence of atomic values, it returns it unchanged.
The fs:distinct-doc-order
function expects either a sequence of nodes as input or a sequence
of atomic values. The resulting type is computed using prime and quantifier, which are defined in [8.4 Judgments for FLWOR and other expressions on
sequences].
|
||
|
|
||
|
item-sequence-to-node-sequence
functionfs:item-sequence-to-node-sequence
($items
as
item()*
) as
node()*
The fs:item-sequence-to-node-sequence
function converts a sequence of item values to nodes by applying
the normative rules numbered 1e
and 2
in
Section <IP_ADDRESS>
ContentXQ (with the value bound to
$items
playing the role of "the value of an enclosed
expression").
If the input sequence contains any attribute nodes, they must precede any other items.
|
||
|
|
||
|
|
||
|
|
||
|
|
||
|
|
||
|
item-sequence-to-string
functionIntroduction
fs:item-sequence-to-string
($items
as
item()*
) as
xs:string
The fs:item-sequence-to-string
function converts a sequence of item values to a string by applying
the normative rules in Section
<IP_ADDRESS> Computed Attribute
ConstructorsXQ for processing the
content expression.
If the input of the fs:item-sequence-to-string
function is an empty sequence, it returns a zero-length string.
Otherwise, each atomic value in the input sequence is cast into a
string. The individual strings resulting from the previous step are
merged into a single string by concatenating them with a single
space character between each pair.
There are no special static typing rules for this function. Static type analysis for this function should be performed as for a built-in function declared with the given signature.
item-sequence-to-untypedAtomic-PI
functionIntroduction
fs:item-sequence-to-untypedAtomic-PI
($items
as
item()*
) as
xs:untypedAtomic
The fs:item-sequence-to-untypedAtomic-PI
function converts a sequence of item values to a string of type
xs:untypedAtomic
by
applying the normative rules in Section <IP_ADDRESS>
Computed Processing Instruction
ConstructorsXQ for processing the
content expression.
If the input is an empty sequence, the fs:item-sequence-to-untypedAtomic-PI
function returns a zero-length string. Otherwise, each atomic value
in the input sequence is cast into a string. If any of the
resulting strings contains the string "?>", a dynamic error is
raised. The individual strings resulting from the previous step are
merged into a single string by concatenating them with a single
space character between each pair. Leading whitespace is removed
from the resulting string.
There are no special static typing rules for this function. Static type analysis for this function should be performed as for a built-in function declared with the given signature.
item-sequence-to-untypedAtomic-text
functionIntroduction
fs:item-sequence-to-untypedAtomic-text
($items
as
item()*
) as
xs:untypedAtomic?
The fs:item-sequence-to-untypedAtomic-text
function converts a sequence of item values to a string of type
xs:untypedAtomic
,
or empty, by applying the rules in Section <IP_ADDRESS>
Text Node ConstructorsXQ for
processing the content expression.
If the input is the empty sequence, the fs:item-sequence-to-untypedAtomic-text
function returns the empty sequence. Otherwise, each atomic value
in the input sequence is cast into a string. The individual strings
resulting from the previous step are merged into a single string by
concatenating them with a single space character between each
pair.
There are no special static typing rules for this function. Static type analysis for this function should be performed as for a built-in function declared with the given signature.
item-sequence-to-untypedAtomic-comment
functionIntroduction
fs:item-sequence-to-untypedAtomic-comment
($items
as
item()*
) as
xs:untypedAtomic
The fs:item-sequence-to-untypedAtomic-comment
function converts a sequence of item values to a string of type
xs:untypedAtomic
by
applying the normative rules in Section <IP_ADDRESS>
Computed Comment ConstructorsXQ for
processing the content expression.
If the input is the empty sequence, the fs:item-sequence-to-untypedAtomic-comment
function returns a zero-length string. Otherwise, each atomic value
in the input sequence is cast into a string. The individual strings
resulting from the previous step are merged into a single string by
concatenating them with a single space character between each pair.
It is a dynamic error if the result of the content expression of a
computed comment constructor contains two adjacent hyphens or ends
with a hyphen.
There are no special static typing rules for this function. Static type analysis for this function should be performed as for a built-in function declared with the given signature.
apply-ordering-mode
functionfs:apply-ordering-mode
($items
as
item()*
) as
item()*
If the statEnv.orderingMode is set to ordered, the fs:apply-ordering-mode
function is the identity function, returning its input sequence in
its original order.
statEnv.orderingMode =
ordered dynEnv
|- Expr => Value |
|
|
dynEnv
|- fs:apply-ordering-mode (Expr)
=> Value |
If the statEnv.orderingMode is set to unordered, the fs:apply-ordering-mode
is equivalent to the fn:unordered
function, returning
the items from its input sequence in arbitrary order.
statEnv.orderingMode =
unordered dynEnv
|- fn:unordered (Expr)
=> Value |
|
|
dynEnv
|- fs:apply-ordering-mode (Expr)
=> Value |
If the ordering context is set to ordered
, the
static type of the input expression of the fs:apply-ordering-mode
function is left unchanged.
statEnv.orderingMode =
ordered |
|
|
statEnv
|- (FS-URI ,"apply-ordering-mode ")(Type)
: Type |
If the ordering context is set to unordered
, the
static type of the input expression of the fs:apply-ordering-mode
function is computed using the prime and quantifier judgments, as for the
fn:unordered
function.
statEnv.orderingMode =
unordered |
|
|
statEnv
|- (FS-URI ,"apply-ordering-mode ")(Type)
: prime(Type) · quantifier(Type) |
to
functionfs:to
($firstval
as
xs:integer?
,
$lastval
as
xs:integer?
) as
xs:integer*
The formal semantics function fs:to
is a
wrapper function for the op:to
operator, taking the
semantics of the range expression over empty sequences into
account.
If one of the input parameters for fs:to
is the empty sequence, the function returns the empty sequence,
otherwise it returns the result of calling the op:to
operator. This semantics is equivalent to the following
user-defined function.
declare function fs:to($firstval as xs:integer?, $lastval as xs:integer?) as xs:integer* { if (fn:empty($firstval) or fn:empty($lastval) then () else op:to($firstval,$lastval) };
The static type of fs:to
does not require
any additional static typing rule, and is typed as a function call
based on the above signature.
node-sequence
functionfs:node-sequence
($nodes
as
node()*
) as
node()*