W3C

XQuery 1.0 and XPath 2.0 Formal Semantics

W3C Working Draft 4 April 2005

This version:
http://www.w3.org/TR/2005/WD-xquery-semantics-20050404/
Latest version:
http://www.w3.org/TR/xquery-semantics/
Previous versions:
http://www.w3.org/TR/2005/WD-xquery-semantics-20050211/ http://www.w3.org/TR/2004/WD-xquery-semantics-20040220/
Editors:
Denise Draper, Microsoft <denised@microsoft.com>
Peter Fankhauser (XML Query WG), Infonyte GmbH <fankhaus@infonyte.com>
Mary Fernández (XML Query WG), AT&T Labs - Research <mff@research.att.com>
Ashok Malhotra (XML Query and XSL WGs), Oracle Corporation <ashok.malhotra@oracle.com>
Kristoffer Rose (XSL WG), IBM T.J. Watson Research Center <krisrose@us.ibm.com>
Michael Rys (XML Query WG), Microsoft <mrys@microsoft.com>
Jérôme Siméon (XML Query WG), IBM T.J. Watson Research Center <simeon@us.ibm.com>
Philip Wadler (XML Query WG), University of Edinburgh <wadler@inf.ed.ac.uk>

Abstract

This document defines formally the semantics of XQuery 1.0 [XQuery 1.0: A Query Language for XML] and XPath 2.0 [XML Path Language (XPath) 2.0].

Status of this Document

This section describes the status of this document at the time of its publication. Other documents may supersede this document. A list of current W3C publications and the latest revision of this technical report can be found in the W3C technical reports index at http://www.w3.org/TR/.

This is a public W3C Working Draft for review by W3C Members and other interested parties. Publication as a Working Draft does not imply endorsement by the W3C Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress.

This version includes a number of changes made in response to comments received during the Last Call period that ended on Feb. 15, 2004. The working group is continuing to process these comments, and additional changes are expected. These decisions are recorded in the Formal Semantics Last Call issues list (http://www.w3.org/2005/04/formal-semantics-issues.html). A list of changes introduced by this draft can be found in [F Revision Log].

XQuery 1.0, XPath 2.0, and their formal semantics has been defined jointly by the XML Query Working Group and the XSL Working Group (both part of the XML Activity).

Public comments on this document and its open issues are invited. Comments should be entered into the last-call issue tracking system for this specification (instructions can be found at http://www.w3.org/XML/2005/04/qt-bugzilla). If access to that system is not feasible, you may send your comments to the W3C mailing list public-qt-comments@w3.org. (archived at http://lists.w3.org/Archives/Public/public-qt-comments/) with “[FS]” at the beginning of the subject field.

The patent policy for this document is the 5 February 2004 W3C Patent Policy. Patent disclosures relevant to this specification may be found on the XML Query Working Group's patent disclosure page and the XSL Working Group's patent disclosure page. An individual who has actual knowledge of a patent which the individual believes contains Essential Claim(s) with respect to this specification should disclose the information in accordance with section 6 of the W3C Patent Policy.

Table of Contents

1 Introduction
    1.1 Normative and Informative Sections
2 Preliminaries
    2.1 Introduction to the Formal Semantics
        2.1.1 Notations from grammar productions
        2.1.2 Notations for judgments
        2.1.3 Notations for inference rules
        2.1.4 Notations for environments
        2.1.5 Putting it together
    2.2 Namespaces and Prefixes
    2.3 XML Values
        2.3.1 Formal values
        2.3.2 Examples of values
    2.4 The [XPath/XQuery] Type System
        2.4.1 XML Schema and the [XPath/XQuery] Type System
        2.4.2 Item types
        2.4.3 Content models
        2.4.4 Top level definitions
        2.4.5 Example of a complete Schema
    2.5 Functions and operators
3 Basics
    3.1 Expression Context
        3.1.1 Static Context
            3.1.1.1 Resolving QNames to Expanded QNames
        3.1.2 Dynamic Context
    3.2 Processing Model
        3.2.1 Processing model
        3.2.2 Normalization judgment
        3.2.3 Static typing judgment
        3.2.4 Dynamic evaluation judgment
    3.3 Error Handling
        3.3.1 Kinds of Errors
        3.3.2 Identifying and Reporting Errors
        3.3.3 Handling Dynamic Errors
        3.3.4 Errors and Optimization
    3.4 Concepts
        3.4.1 Document Order
        3.4.2 Atomization
        3.4.3 Effective Boolean Value
        3.4.4 Input Sources
        3.4.5 URI Literals
    3.5 Types
        3.5.1 Predefined Schema Types
        3.5.2 Typed Value and String Value
        3.5.3 SequenceType Syntax
        3.5.4 SequenceType Matching
    3.6 Comments
4 Expressions
    4.1 Primary Expressions
        4.1.1 Literals
        4.1.2 Variable References
        4.1.3 Parenthesized Expressions
        4.1.4 Context Item Expression
        4.1.5 Function Calls
    4.2 Path Expressions
        4.2.1 Steps
            4.2.1.1 Axes
            4.2.1.2 Node Tests
        4.2.2 Predicates
        4.2.3 Unabbreviated Syntax
        4.2.4 Abbreviated Syntax
    4.3 Sequence Expressions
        4.3.1 Constructing Sequences
        4.3.2 Filter Expressions
        4.3.3 Combining Node Sequences
    4.4 Arithmetic Expressions
    4.5 Comparison Expressions
        4.5.1 Value Comparisons
        4.5.2 General Comparisons
        4.5.3 Node Comparisons
    4.6 Logical Expressions
    4.7 Constructors
        4.7.1 Direct Element Constructors
            4.7.1.1 Attributes
            4.7.1.2 Namespace Declaration Attributes
            4.7.1.3 Content
            4.7.1.4 Whitespace in Element Content
        4.7.2 Other Direct Constructors
        4.7.3 Computed Constructors
            4.7.3.1 Computed Element Constructors
            4.7.3.2 Computed Attribute Constructors
            4.7.3.3 Document Node Constructors
            4.7.3.4 Text Node Constructors
            4.7.3.5 Computed Processing Instruction Constructors
            4.7.3.6 Computed Comment Constructors
        4.7.4 In-scope Namespaces of a Constructed Element
    4.8 [For/FLWR] Expressions
        4.8.1 FLWOR expressions
        4.8.2 For expression
        4.8.3 Let Expression
        4.8.4 Order By and Return Clauses
    4.9 Ordered and Unordered Expressions
    4.10 Conditional Expressions
    4.11 Quantified Expressions
    4.12 Expressions on SequenceTypes
        4.12.1 Instance Of
        4.12.2 Typeswitch
        4.12.3 Cast
        4.12.4 Castable
        4.12.5 Constructor Functions
        4.12.6 Treat
    4.13 Validate Expressions
        4.13.1 Validating an Element Node
        4.13.2 Validating a Document Node
    4.14 Extension Expressions
5 Modules and Prologs
    5.1 Version Declaration
    5.2 Module Declaration
    5.3 Boundary-space Declaration
    5.4 Default Collation Declaration
    5.5 Base URI Declaration
    5.6 Construction Declaration
    5.7 Ordering Mode Declaration
    5.8 Empty Order Declaration
    5.9 Copy-Namespaces Declaration
    5.10 Schema Import
    5.11 Module Import
    5.12 Namespace Declaration
    5.13 Default Namespace Declaration
    5.14 Variable Declaration
    5.15 Function Declaration
    5.16 Option Declaration
6 Conformance
    6.1 Static Typing Feature
        6.1.1 Static Typing Extensions
7 Additional Semantics of Functions
    7.1 Formal Semantics Functions
        7.1.1 The arithmetic operator pseudo-functions: fs:minus, fs:plus, fs:times, fs:idiv, fs:div, and fs:mod
        7.1.2 The comparison pseudo-functions: fs:eq, fs:ne, fs:lt, fs:le, fs:gt, and fs:ge
        7.1.3 The fs:convert-operand function
        7.1.4 The fs:convert-simple-operand function
        7.1.5 The fs:distinct-doc-order function
        7.1.6 The fs:distinct-doc-order-or-atomic-sequence function
        7.1.7 The fs:item-sequence-to-node-sequence function
        7.1.8 The fs:item-sequence-to-untypedAtomic function
        7.1.9 The fs:apply-ordering-mode function
        7.1.10 The fs:to function
    7.2 Standard functions with specific typing rules
        7.2.1 The fn:abs, fn:ceiling, fn:floor, fn:round, and fn:round-half-to-even functions
        7.2.2 The fn:boolean function
        7.2.3 The fn:collection and fn:doc functions
        7.2.4 The fn:data function
        7.2.5 The fn:distinct-values function
        7.2.6 The fn:unordered function
        7.2.7 The fn:error function
        7.2.8 The fn:min, fn:max, fn:avg, and fn:sum functions
        7.2.9 The fn:remove function
        7.2.10 The fn:reverse function
        7.2.11 The fn:subsequence function
        7.2.12 The op:union, op:intersect, and op:except operators
        7.2.13 The fn:zero-or-one, fn:one-or-more, and fn:exactly-one functions
8 Auxiliary Judgments
    8.1 Judgments for accessing types
        8.1.1 Derives from
        8.1.2 Substitutes for
        8.1.3 Element and attribute name lookup (Dynamic)
        8.1.4 Element and attribute type lookup (Static)
        8.1.5 Extension
        8.1.6 Mixed content
        8.1.7 Type adjustment
        8.1.8 Builtin attributes
        8.1.9 Type expansion
        8.1.10 Union interpretation of derived types
    8.2 Judgments for step expressions and filtering
        8.2.1 Principal Node Kind
        8.2.2 Auxiliary judgments for axes
            8.2.2.1 Static semantics of axes
            8.2.2.2 Dynamic semantics of axes
        8.2.3 Auxiliary judgments for node tests
            8.2.3.1 Static semantics of node tests
                8.2.3.1.1 Name Tests
                8.2.3.1.2 Kind Tests
            8.2.3.2 Dynamic semantics of node tests
                8.2.3.2.1 Name Tests
                8.2.3.2.2 Kind Tests
        8.2.4 Attribute filtering
    8.3 Judgments for type matching
        8.3.1 Matches
        8.3.2 Subtype and Type equality
    8.4 Judgments for FLWOR and other expressions on sequences
    8.5 Judgments for function calls
        8.5.1 Type promotion
    8.6 Judgments for validation modes and contexts
        8.6.1 Elements in validation mode

Appendices

A Normalized core grammar
    A.1 Core BNF
B Functions and Operators
    B.1 Functions and Operators used in the Formal Semantics
    B.2 Mapping of Overloaded Internal Functions
C Importing Schemas
    C.1 Introduction
        C.1.1 Features
        C.1.2 Organization
        C.1.3 Main mapping rules
        C.1.4 Special attributes
            C.1.4.1 use, default, and fixed
            C.1.4.2 minOccurs, maxOccurs, minLength, maxLength, and length
            C.1.4.3 mixed
            C.1.4.4 nillable
            C.1.4.5 substitutionGroup
        C.1.5 Anonymous type names
    C.2 Schemas as a whole
        C.2.1 Schema
        C.2.2 Include
        C.2.3 Redefine
        C.2.4 Import
    C.3 Attribute Declarations
        C.3.1 Global attributes declarations
        C.3.2 Local attribute declarations
    C.4 Element Declarations
        C.4.1 Global element declarations
        C.4.2 Local element declarations
    C.5 Complex Type Definitions
        C.5.1 Global complex type
        C.5.2 Local complex type
        C.5.3 Complex type with simple content
        C.5.4 Complex type with complex content
    C.6 Attribute Uses
    C.7 Attribute Group Definitions
        C.7.1 Attribute group definitions
        C.7.2 Attribute group reference
    C.8 Model Group Definitions
    C.9 Model Groups
        C.9.1 All groups
        C.9.2 Choice groups
        C.9.3 Sequence groups
    C.10 Particles
        C.10.1 Element reference
        C.10.2 Group reference
    C.11 Wildcards
        C.11.1 Attribute wildcards
        C.11.2 Element wildcards
    C.12 Identity-constraint Definitions
    C.13 Notation Declarations
    C.14 Annotation
    C.15 Simple Type Definitions
        C.15.1 Global simple type definition
        C.15.2 Local simple type definition
        C.15.3 Simple type content
D References
    D.1 Normative References
    D.2 Non-normative References
    D.3 Background References
E Auxiliary Judgments for Validation (Non-Normative)
    E.1 Judgments for the validate expression
        E.1.1 Type resolution
        E.1.2 Interleaving
        E.1.3 Erasure
            E.1.3.1 Simply erases
            E.1.3.2 Erases
        E.1.4 Annotate
            E.1.4.1 Simply annotate
            E.1.4.2 Nil-annotate
            E.1.4.3 Annotate
F Revision Log (Non-Normative)
    F.1 4 April 2005


1 Introduction

This document defines the formal semantics of XQuery 1.0 and XPath 2.0. The present document is part of a set of documents that together define the XQuery 1.0 and XPath 2.0 languages:

The scope and goals for the [XPath/XQuery] language are discussed in the charter of the W3C [XSL/XML Query] Working Group and in the [XPath/XQuery] requirements [XML Query 1.0 Requirements].

This document defines the semantics of [XPath/XQuery] by giving a precise formal meaning to each of the expressions of the [XPath/XQuery] specification in terms of the [XPath/XQuery] data model. This document assumes that the reader is already familiar with the [XPath/XQuery] language.

Two important design aspects of [XPath/XQuery] are that it is functional and that it is typed. These two aspects play an important role in the [XPath/XQuery] Formal Semantics.

[XPath/XQuery] is a functional language. [XPath/XQuery] is built from expressions, rather than statements. Every construct in the language (except for the XQuery query prolog) is an expression and expressions can be composed arbitrarily. The result of one expression can be used as the input to any other expression, as long as the type of the result of the former expression is compatible with the input type of the latter expression with which it is composed. Another characteristic of a functional language is that variables are always passed by value, and a variable's value cannot be modified through side effects.

[XPath/XQuery] is a typed language. Types can be imported from one or more XML Schemas that describe the input documents and the output document, and the [XPath/XQuery] language can then perform operations based on these types. In addition, [XPath/XQuery] supports static type analysis. Static type analysis infers the output type of an expression based on the type of its input expressions. Static typing allows early detection of type errors, and can be used as the basis for certain forms of optimization. The [XPath/XQuery] type system captures most of the features of [Schema Part 1], including global and local element and attribute declarations, complex and simple type definitions, named and anonymous types, derivation by restriction, extension, list and union, substitution groups, and wildcard types. It does not model uniqueness constraints and facet constraints on simple types.

This document is organized as follows. [2 Preliminaries] introduces the notations used to define the [XPath/XQuery] Formal Semantics. These include the formal notations for values in the [XPath/XQuery] data model and for types in XML Schema. The next three sections: [3 Basics], [4 Expressions], and [5 Modules and Prologs] have the same structure as the corresponding sections in the [XQuery 1.0: A Query Language for XML] and [XML Path Language (XPath) 2.0] documents. This allows the reader to quickly find the formal definition of a particular language construct. [3 Basics] defines the semantics for basic [XPath/XQuery] concepts, and [4 Expressions] defines the dynamic and static semantics of each [XPath/XQuery] expression. [5 Modules and Prologs] defines the semantics of the [XPath/XQuery] prolog. [7 Additional Semantics of Functions] defines the static semantics of several functions in [Functions and Operators] and gives the dynamic and static semantics of several supporting functions used in this document. The remaining sections, [8 Auxiliary Judgments] and [C Importing Schemas], contain material that supports the formal semantics of [XPath/XQuery]. [8 Auxiliary Judgments] defines formal judgments that relate data model values to types, that relate types to types, and that support the formal definition of validation. These judgments are used in the definition of expressions in [4 Expressions]. Lastly, [C Importing Schemas], specifies how XML Schema documents are imported into the [XPath/XQuery] type system and relates XML Schema types to the [XPath/XQuery] type system.

1.1 Normative and Informative Sections

Certain aspects of language processing are described in this specification as implementation-defined or implementation-dependent.

  • [Definition: Implementation-defined indicates an aspect that may differ between implementations, but must be specified by the implementor for each particular implementation.]

  • [Definition: Implementation-dependent indicates an aspect that may differ between implementations, is not specified by this or any W3C specification, and is not required to be specified by the implementor for any particular implementation.]

A language aspect described in this specification as implementation-defined or implementation dependent may be further constrained by the specifications of a host language in which XPath is embedded.

This document contains the normative static semantics of [XPath/XQuery]. The static semantics rules in [3 Basics], [4 Expressions], [5 Modules and Prologs], and [7 Additional Semantics of Functions] are normative. [3.1.1 Static Context] is normative, because it defines the static context used in the static typing rules. [8 Auxiliary Judgments] is normative, because it contains all the judgments necessary for defining SequenceType Matching.

The dynamic semantics of [XPath/XQuery] are normatively defined in [XQuery 1.0: A Query Language for XML] and [XML Path Language (XPath) 2.0]. In this document, the dynamic semantic rules in [3 Basics], [4 Expressions], and [5 Modules and Prologs], the examples and material labeled as "Note" are provided for explanatory purposes and are not normative.

The mapping rules from XML Schema to the XQuery type system provided in [C Importing Schemas], and the formal semantics of XML Schema validation in [E Auxiliary Judgments for Validation] are informative and do not handle every feature of XML Schema.

2 Preliminaries

This section provides the background necessary to understand the Formal Semantics, introduces the notations that are used, and explains its relationship to other documents.

2.1 Introduction to the Formal Semantics

Why a Formal Semantics? The goal of the formal semantics is to complement the [XPath/XQuery] specification ([XQuery 1.0: A Query Language for XML] and [XML Path Language (XPath) 2.0]), by defining the meaning of [XPath/XQuery] expressions with mathematical rigor.

A rigorous formal semantics clarifies the intended meaning of the English specification, ensures that no corner cases are left out, and provides a reference for implementation.

Why use formal notations? Rigor is achieved by the use of formal notations to represent [XPath/XQuery] objects such as expressions, XML values, and XML Schema types, and by the systematic definition of the relationships between those objects to reflect the meaning of the language. In particular, the dynamic semantics relates [XPath/XQuery] expressions to the XML value to which they evaluate, and the static semantics relates [XPath/XQuery] expressions to the XML Schema type that is inferred for that expression.

The Formal Semantics uses several kinds of formal notations to define the relationships between [XPath/XQuery] expressions, XML values, and XML Schema types. This section introduces the notations for judgments, inference rules, and mapping rules as well as the notation for environments, which implement the dynamic and static contexts. The reader already familiar with these notations can skip this section and continue with [2.3 XML Values].

2.1.1 Notations from grammar productions

Grammar productions are used to describe "objects" (values, types, [XPath/XQuery] expressions, etc.) manipulated by the Formal Semantics. The Formal Semantics makes use of several kinds of grammar productions.

XQuery grammar productions describe the XQuery language and expressions. XQuery productions are identified by a number, which corresponds to their number in the [XQuery 1.0: A Query Language for XML] document, and are marked with "(XQuery)". For instance, the following production describes FLWOR expressions in XQuery.

[For/FLWR] Expressions
[33 (XQuery)]    FLWORExpr    ::=    (ForClause | LetClause)+ WhereClause? OrderByClause? "return" ExprSingle

For the purpose of this document, the differences between the XQuery 1.0 and the XPath 2.0 grammars are mostly irrelevant. By default, this document uses XQuery 1.0 grammar productions. Whenever the grammar for XPath 2.0 differs from the one for XQuery 1.0, the corresponding XPath 2.0 productions are also given. XPath productions are identified by a number, which corresponds to their number in [XML Path Language (XPath) 2.0], and are marked with "(XPath)". For instance, the following production describes for expressions in XPath.

[For/FLWR] Expressions
[4 (XPath)]    ForExpr    ::=    SimpleForClause "return" ExprSingle

XQuery Core grammar productions describe the XQuery Core. The Core grammar is given in [A Normalized core grammar]. Core productions are identified by a number, which corresponds to their number in [A Normalized core grammar], and are marked with "(Core)". For instance, the following production describes the simpler form of the "FLWOR" expression in the XQuery Core.

Core FLWOR Expressions
[32 (Core)]    FLWORExpr    ::=    (ForClause | LetClause) "return" ExprSingle

The Formal Semantics manipulates "objects" (values, types, expressions, etc.) for which there is no existing grammar production in the [XQuery 1.0: A Query Language for XML] document. In these cases, specific grammar productions are introduced. Notably, additional productions are used to describe values in the [Data Model], and to describe the [XPath/XQuery] type system. Formal Semantics productions are identified by a number, and are marked by "(Formal)". For instance, the following production describes global type definitions in the [XPath/XQuery] type system.

Type Definitions
[37 (Formal)]    Definition    ::=    ("define" "element" ElementName Substitution? Nillable? TypeReference)
| ("define" "attribute" AttributeName TypeReference)
| ("define" "type" TypeName TypeDerivation)

Note that grammar productions that are specific to the Formal Semantics (i.e., marked with "(Formal)") are not part of [XPath/XQuery]. They are not accessible to the user and are only used in the course of defining the language's semantics.

2.1.2 Notations for judgments

The basic building block of the formal specification is called a judgment. A judgment expresses whether a property holds or not.

For example:

Notation

The judgment

Painting is beautiful

holds if the object Painting is beautiful.

Notation

Here are three judgments that are used extensively in this document.

The judgment

Expr => Value

holds if the expression Expr yields (or evaluates to) the value Value.

The judgment

Expr : Type

holds when the expression Expr has type Type.

The judgment

Expr raises Error

holds when the expression Expr raises the error Error.

A judgment can contain symbols and patterns.

Symbols are purely syntactic and are used to write the judgment itself. In general, symbols in a judgment are chosen to reflect its meaning. For example, 'is beautiful', '=>' and ':' are symbols, the second and third of which should be read "yields", and "has type" respectively.

Patterns are written with italicized words. The name of a pattern is significant: each pattern name corresponds to an "object" (a value, a type, an expression, etc.) that can be substituted legally for the pattern. By convention, all patterns in the Formal Semantics correspond to grammar non-terminals, and are used to represent entities that can be constructed through application of the corresponding grammar production. For example, Expr represents any [XPath/XQuery] expression, and Value represents any value in the [XPath/XQuery] data model.

When applying the judgment, each pattern must be instantiated to an appropriate sort of "object" (value, type, expression, etc). For example, '3 => 3' and '$x+0 => 3' are both instances of the judgment 'Expr => Value'. Note that in the first judgment, '3' corresponds to both the expression '3' (on the left-hand side of the => symbol) and to the the value '3' (on the right-hand side of the => symbol).

Patterns may appear with subscripts (e.g. Expr1, Expr2) to distinguish different instances of the same sort of pattern. Each distinct pattern must be instantiated to a single "object" (value, type, expression, etc.). If the same pattern occurs twice in a judgment description then it should be instantiated with the same "object". For example, '3 => 3' is an instance of the judgment 'Expr1 => Expr1' but '$x+0 => 3' is not since the two expressions '$x+0' and '3' cannot be both instance of the pattern Expr1. The judgment'$x+0 => 3' is an instance of the judgment 'Expr1 => Expr2'.

In a few cases, patterns may have a name that is not exactly the name of a grammar production but is based on it. For instance, a BaseTypeName is a pattern that stands for a type name, as would TypeName, or TypeName2. This usage is limited, and only occurs to improve the readability of some of the inference rules.

2.1.3 Notations for inference rules

Inference rules are used to specify whether a judgment holds or not. Inference rules express the logical relation between judgments and describe how complex judgments can be concluded from simpler premise judgments.

A logical inference rule is written as a collection of premises and a conclusion, written respectively above and below a dividing line:

premise1 ... premisen

conclusion

All premises and the conclusion are judgments. The interpretation of an inference rule is: if all the premise judgments above the line hold, then the conclusion judgment below the line must also hold.

Here is a simple example of inference rule, which uses the example judgment 'Expr => Value' from above:

$x => 0      3 => 3

$x + 3 => 3

This inference rule expresses the following property of the judgment 'Expr => Value': if the variable expression '$x' yields the value '0', and the literal expression '3' yields the value '3', then the expression '$x + 3' yields the value '3'.

An inference rule may have no premises above the line, which means that the expression below the line always holds:


3 => 3

This inference rule expresses the following property of the judgment 'Expr => Value': evaluating the literal expression '3' always yields the value '3'.

The two above rules are expressed in terms of specific variables and values, but usually rules are more abstract. That is, the judgments they relate contain patterns. Here is a rule that says that for any variable Variable that yields the integer value Integer, adding '0' yields the same integer value:

Variable => Integer

Variable + 0 => Integer

As in a judgment, each pattern in a particular inference rule must be instantiated to the same "object" within the entire rule. This means that one can talk about "the value of Variable" instead of the more precise "what Variable is instantiated to in (this particular instantiation of) the inference rule".

Note

In effect, inference rules are just a notation that describes a bottom-up algorithm. In the examples above, the rules describe an evaluation algorithm where the result of an expression depends on the result for its sub-expressions.

2.1.4 Notations for environments

Logical inference rules use environments to record information computed during static type analysis or dynamic evaluation so that this information can be used by other logical inference rules. For example, the type signature of a user-defined function in a [expression/query] prolog can be recorded in an environment and used by subsequent rules. Similarly, the value assigned to a variable within a "let" expression can be captured in an environment and used for further evaluations.

An environment is a dictionary that maps a symbol (e.g., a function name or a variable name) to an "object" (e.g., a function body, a type, a value). One can access information in an environment or update the environment.

If "env" is an environment, then "env(symbol)" denotes the "object" to which symbol is mapped. The notation is intentionally similar to function application, because an environment can be considered a function from the argument symbol to the "object" to which the symbol is mapped.

This document uses environment groups that group related environments. If "env" is an environment group with the member "mem", then that environment is denoted "env.mem" and the value that it maps symbol to is denoted "env.mem(symbol)".

The two main environment groups used in the Formal Semantics are: a dynamic environment (dynEnv), which captures the [XPath/XQuery]'s dynamic context, and a static environment (statEnv), which captures the [XPath/XQuery]'s static context. Both are defined in [3.1 Expression Context].

For example, dynEnv.varValue denotes the dynamic environment that maps variables to values and dynEnv.varValue(Variable) denotes the value of the variable Variable in the dynamic environment.

Updating is only defined on environment groups:

  • "env + mem(symbol => object) " denotes the new environment group that is identical to env except that the mem environment has been updated to map symbol to object. The notation symbol => object indicates that symbol is mapped to object in the new environment.

  • The following shorthand is also allowed: "env + mem( symbol1 => object1 ; ... ; symboln => objectn ) " in which each symbol is mapped to a corresponding object in the new environment.

    This notation is equivalent to nested updates, as in " (env + mem( symbol1 => object1) + ... ) + mem(symboln => objectn)".

  • If the "object" is a type then the following notation relates a symbol to a type: "env + mem(symbol : object) ".

Updating an environment creates a copy of the original environment and overrides any previous binding that might exist for the same name and the same group in that environment. Updating the environment captures the scope of a symbol (e.g., a variable, a namespace prefix, etc). Also, note that there are no operations to remove entries from environments. This is never necessary as updating an environment effectively creates a new extended copy of the original environment, leaving the original environment accessible wherever it is in scope along with the updated copy.

Environments are used in a judgment to capture some of the context in which the judgment is computed, and most judgments are computed assuming that some environment is given. This assumption is denoted by prefixing the judgment with "env |-". The "|-" symbol is called a "turnstile" and is used in almost all inference rules.

For instance, the judgment

dynEnv |- Expr => Value

is read as: Assuming the dynamic environment dynEnv, the expression Expr yields the value Value.

2.1.5 Putting it together

Putting the above notations together, here is an example of an inference rule that occurs later in this document:

statEnv |- Expr1 : Type1      statEnv |- Expr2 : Type2

statEnv |- Expr1 , Expr2 : Type1, Type2

This rule is read as follows: if two expressions Expr1 and Expr2 are known to have the static types types Type1 and Type2 (the two premises above the line), then it is the case that the expression below the line "Expr1 , Expr2" must have the static type "Type1, Type2", which is the sequence of types Type1 and Type2. The above inference rule does not modify the (static) environment.

The following rule defines the static semantics of a "let" expression. The binding of the new variable is captured by an update to the varType component of the original static environment.

statEnv |- VarName of var expands to expanded-QName
statEnv |- Expr1 : Type1      statEnv + varType(expanded-QName : Type1) |- Expr2 : Type2

statEnv |- let $VarName := Expr1 return Expr2 : Type2

This rule is read as follows: First, because the variable is a QName, it is first expanded into an expanded QName. Second, the type Type1 for the "let" input expression Expr1 is computed. Then the "let" variable with expanded name, expanded-QName with type Type1 is added into the varType component of the static environment group statEnv. Finally, the type Type2 of Expr2 is computed in that new environment.

2.2 Namespaces and Prefixes

The Formal Semantics uses the following namespace prefixes.

  • fn: for functions and operators from the [Functions and Operators] document.

  • xs: for XML Schema components and built-in types.

  • xdt: for XQuery built-in types.

All these prefixes are assumed to be bound to the appropriate URIs.

In addition, the Formal Semantics uses the following special prefixes for specification purposes.

These prefixes are always italicized to emphasize that the corresponding functions, variables, and types are abstract: they are not and cannot be made accessible in the host language. None of these special prefixes are given a URI.

2.3 XML Values

The [XPath/XQuery] language is defined over values of the [XPath/XQuery] data model. The [XPath/XQuery] data model is defined normatively in [Data Model]. We define the formal notation that is used in this document to describe and manipulate values in inference rules. Formal values are used for specification purposes only and are not exposed to the [XPath/XQuery] user.

This section gives the grammar for formal values, along with a summary of the corresponding data model properties. In the context of this document, all constraints on values that are specified in [Data Model] are assumed to hold.

2.3.1 Formal values

A value is a sequence of zero or more items. An item is either an atomic value or a node.

An atomic value is a value in the value space of an atomic type, labeled with the name of that atomic type. An atomic type is either a primitive or derived atomic type according to XML Schema [Schema Part 2], xdt:untypedAtomic, or xdt:anyAtomicType.

A node is either an element, an attribute, a document, a text, a comment, or a processing-instruction node.

Element nodes have a type annotationXQ and contain a complex value or a simple value. Attribute nodes have a type annotationXQ and contain a simple value. Text nodes always contain one string value of type xdt:untypedAtomic. Document nodes do not have a type annotation and contain a sequence of element, text, comment, or processing-instruction nodes.

A simple value is a sequence of atomic values.

A complex value is a sequence of attribute nodes followed by a sequence of element, text, comment, or processing-instruction nodes.

A type annotationXQ can be either the QName of a declared type or an anonymous type. An anonymous type corresponds to an XML Schema type for which the schema writer did not provide a name. Anonymous type names are not visible to the user, but are generated during schema validation and used to annotate nodes in the data model. By convention, anonymous type names are written using the fs: Formal Semantics prefix: fs:anon0, fs:anon1, etc.

Formal values are defined by the following grammar.

Values
[7 (Formal)]    Value    ::=    Item
| (Value "," Value)
| ("(" ")")
[18 (Formal)]    Item    ::=    NodeValue
| AtomicValue
[19 (Formal)]    AtomicValue    ::=    AtomicValueContent TypeAnnotation
[1 (Formal)]    AtomicValueContent    ::=    String
| Boolean
| Decimal
| Float
| Double
| Duration
| DateTime
| Time
| Date
| GYearMonth
| GYear
| GMonthDay
| GDay
| GMonth
| HexBinary
| Base64Binary
| AnyURI
| expanded-QName
| NOTATION
[2 (Formal)]    TypeAnnotation    ::=    "of" "type" TypeName
[9 (Formal)]    ElementValue    ::=    "element" ElementName "nilled"? TypeAnnotation "{" Value "}" "{" NamespaceBindings "}"
[10 (Formal)]    AttributeValue    ::=    "attribute" AttributeName TypeAnnotation "{" SimpleValue "}"
[8 (Formal)]    SimpleValue    ::=    AtomicValue
| (SimpleValue "," SimpleValue)
| ("(" ")")
[11 (Formal)]    DocumentValue    ::=    "document" "{" Value "}"
[13 (Formal)]    CommentValue    ::=    "comment" "{" String "}"
[14 (Formal)]    ProcessingInstructionValue    ::=    "processing-instruction" QName "{" String "}"
[12 (Formal)]    TextValue    ::=    "text" "{" String "}"
[17 (Formal)]    NodeValue    ::=    ElementValue
| AttributeValue
| DocumentValue
| TextValue
| CommentValue
| ProcessingInstructionValue
[3 (Formal)]    ElementName    ::=    QName
[6 (Formal)]    AttributeName    ::=    QName
[20 (Formal)]    TypeName    ::=    QName
[15 (Formal)]    NamespaceBindings    ::=    NamespaceBinding ... NamespaceBinding
[16 (Formal)]    NamespaceBinding    ::=    "namespace" NCName "{" String "}"

Notation

In that grammar, "String" indicates the value space of xs:string, "Decimal" indicates the value space of xs:decimal, etc.

Untyped elements (e.g., from well-formed documents) have the type annotationXQ xdt:untyped, untyped attributes have the type annotationXQ xdt:untypedAtomic, and untyped atomic values have the type annotationXQ xdt:untypedAtomic.

An element has an optional "nilled" marker. This marker can only be present if the element has been validated against an element type in the schema which is "nillable", and the element has no content and an attribute xsi:nil set to "true".

An element also has a sequence of namespace bindings, which are the set of in-scope namespaces for that element. Each namespace binding is a prefix, URI pair.

Note:

In [XPath], the in-scope namespaces of an element node are represented by a collection of namespace nodes arranged on a namespace axis, which is optional and deprecated in [XML Path Language (XPath) 2.0]. XQuery does not support the namespace axis and does not represent namespace bindings in the form of nodes.

In examples, we omit the namespace bindings when they are empty. For example, the following two values are the same (note that the xs and xdt prefixes are built-in):

  element weight of type xs:integer { text { "42" } } {}
  element weight of type xs:integer { text { "42" } } 

The same rule about constructing sequences apply to the values described by that grammar. Notably, sequences cannot be nested. For example, the sequence (10, (1, 2), (), (3, 4)) is equivalent to the sequence (10, 1, 2, 3, 4).

When the context is clear, we may omit the type annotationXQ on literal values. For instance:

  "Hello World!"   instead of   "Hello World!" of type xs:string
  10               instead of   10 of type xs:integer

2.3.2 Examples of values

A well-formed document

  <fact>The cat weighs <weight units="lbs">12</weight> pounds.</fact>

In the absence of a Schema, this document is represented as

  element fact of type xdt:untyped {
    text { "The cat weighs " },
    element weight of type xdt:untyped {
      attribute units of type xdt:untypedAtomic {
        "lbs" of type xdt:untypedAtomic
      }
      text { "12" }
    },
    text { " pounds." }
  }

A document before and after validation.

  <weight xsi:type="xs:integer">42</weight>

The formal model for values can represent values before and after validation. Before validation, this element is represented as:

  element weight of type xdt:untyped {
    attribute xsi:type of type xdt:untypedAtomic {
      "xs:integer" of type xdt:untypedAtomic
    },
    text { "42" }
  }

After validation, this element is represented as:

  element weight of type xs:integer {
    attribute xsi:type of type xs:QName {
      "xs:integer" of type xs:QName
    },
    42 of type xs:integer
  }

An element with a list type

  <sizes>1 2 3</sizes>

Before validation, this element is represented as:

  element sizes of type xdt:untyped {
    text { "1 2 3" }
  }

Assume the following Schema.

  <xs:element name="sizes" type="sizesType"/>
  <xs:simpleType name="sizesType">
    <xs:list itemType="sizeType"/>
  </xs:simpleType>
  <xs:simpleType name="sizeType">
    <xs:restriction base="xs:integer"/>
  </xs:simpleType>

After validation against this Schema, the element is represented as:

  element sizes of type sizesType {
    1 of type sizeType,
    2 of type sizeType,
    3 of type sizeType
  }

An element with an anonymous type

  <sizes>1 2 3</sizes>

Before validation, this element is represented as:

  element sizes of type xdt:untyped {
    text { "1 2 3" }
  }

Assume the following Schema.

  <xs:element name="sizes">
    <xs:simpleType>
      <xs:list itemType="xs:integer"/>
    </xs:simpleType>
  </xs:element>

After validation, this element is represented as:

  element sizes of type fs:anon1 {
    1 of type xs:integer,
    2 of type xs:integer,
    3 of type xs:integer
  }

where fs:anon1 stands for the internal anonymous name generated by the system for the sizes element.

An nillable element with xsi:type set to true:

  <sizes xsi:nil="true"/>

Before validation, this element is represented as:

  element sizes of type xdt:untyped {
    attribute xsi:nil of type xdt:untypedAtomic { "true" as xdt:untypedAtomic }
  }

Assume the following Schema.

  <xs:element name="sizes" type="sizesType" nillable="true"/>

After validation against this Schema, the element is represented as:

  element sizes nilled of type sizesType {
    attribute xsi:nil of type xs:boolean { true as xsd:boolean }
  }

An element with a union type

  <sizes>1 two 3 four</sizes>

Before validation, this element is represented as:

  element sizes of type xdt:untyped {
    text { "1 two 3 four" }
  }

Assume the following Schema:

  <xs:element name="sizes" type="sizesType"/>
  <xs:simpleType name="sizesType">
    <xs:list itemType="sizeType"/>
  </xs:simpleType>
  <xs:simpleType name="sizeType">
    <xs:union memberType="xs:integer xs:string"/>
  </xs:simpleType>

After validation against this Schema, the element is represented as:

  element sizes of type sizesType {
    1 of type xs:integer,
    "two" of type xs:string,
    3 of type xs:integer,
    "four" of type xs:string
  }

2.4 The [XPath/XQuery] Type System

The [XPath/XQuery] type system is used in the specification of the dynamic and of the static semantics of [XPath/XQuery]. This section introduces formal notations for describing types.

2.4.1 XML Schema and the [XPath/XQuery] Type System

The [XPath/XQuery] type system is based on [Schema Part 1] and [Schema Part 2]. [Schema Part 1] and [Schema Part 2] specify normatively the type information available in [XPath/XQuery]. We define the formal notation that is used in this document to describe and manipulate types in inference rules. Formal types are used for specification purposes only and are not exposed to the [XPath/XQuery] user.

Representation of content models. For the purpose of static typing, the [XPath/XQuery] type system only describes minOccurs, maxOccurs, and minLength, maxLength on list types for the occurrences that correspond to the DTD operators +, *, and ?. Choices are represented using the DTD operator |. All groups are represented using the interleaving operator (&).

Representation of anonymous types. To clarify the semantics, the [XPath/XQuery] type system makes all anonymous types explicit.

Representation of XML Schema simple type facets and identity constraints. For simplicity, XML Schema simple type facets and identity constraints are not formally represented in the [XPath/XQuery] type system. However, an [XPath/XQuery] implementation supporting XML Schema import and validation must must take simple type facets and identity constraints into account.

The mapping from XML Schema into the [XPath/XQuery] type system is given in [C Importing Schemas]. The rest of this section is organized as follows. [2.4.2 Item types] describes types items, [2.4.3 Content models] describes content models, and [2.4.4 Top level definitions] describe top-level type declarations.

2.4.2 Item types

An item type is either an atomic type, an element type, an attribute type, a document node type, a text node type, a comment node type, or a processing instruction type. We distinguish between document nodes, attribute nodes, and nodes that can occur in element content (elements, comments, processing instructions, and text nodes), as we need to refer to element content nodes later in the formal semantics.

Item Types
[23 (Formal)]    FormalItemType    ::=    AtomicTypeName | NodeType
[26 (Formal)]    AtomicTypeName    ::=    QName
[24 (Formal)]    NodeType    ::=    DocumentType
| AttributeType
| ElementContentType
[25 (Formal)]    ElementContentType    ::=    ElementType
| "comment"
| "processing-instruction"
| "text"
[27 (Formal)]    ElementType    ::=    "element" ElementName? TypeSpecifier?
[28 (Formal)]    TypeSpecifier    ::=    Nillable? TypeReference
[29 (Formal)]    AttributeType    ::=    "attribute" AttributeName? TypeReference?
[30 (Formal)]    Nillable    ::=    "nillable"
[34 (Formal)]    TypeReference    ::=    "of" "type" TypeName
[45 (Formal)]    DocumentType    ::=    "document" ("{" Type? "}")?

An element or attribute type has an optional name and an optional type reference. A name alone corresponds to a reference to a global element or attribute declaration. A name with a type reference corresponds to a local element or attribute declaration. The word "element" or "attribute" alone refers to the wildcard types for any element or any attribute. In addition, an element type has an optional nillable flag that indicates whether the element can be nilled or not.

A document type has an optional content type. If no content type is given, then it refers to the wildcard type describing any document.

Note

Generic node types (e.g., node()), are interpreted in the type system as union types (e.g., element | attribute | text | comment | processing-instruction) and therefore do not appear here. The semantics of sequence types is described in [3.5.4 SequenceType Matching].

Examples

The following is a text node type

  text

The following is a type for all elements

  element

The following is a type for all elements of type string

  element of type xs:string

The following is a type for a nillable element of type string

  element size nillable of type xs:string

The following is a reference to a global attribute declaration

  attribute sizes

The following is a type for elements with anonymous type fs:anon1:

  element sizes of type fs:anon1

2.4.3 Content models

Following XML Schema, types in [XPath/XQuery] are composed from item types by optional, one or more, zero or more, all group, sequence, choice, empty sequence (written empty), or empty choice (written none).

The type empty matches the empty sequence. The type none matches no values. none is the identity for choice, that is (Type | none) = Type)). The type none is the static type for [7.2.7 The fn:error function].

Types
[21 (Formal)]    Type    ::=    FormalItemType
| (Type Occurrence)
| (Type "&" Type)
| (Type "," Type)
| (Type "|" Type)
| "empty"
| "none"
| ("(" Type ")")
[22 (Formal)]    Occurrence    ::=    "*" | "+" | "?"

The [XPath/XQuery] type system includes three binary operators on types: ",", "|" and "&", corresponding respectively to sequence, choice and all groups in Schema. The [XPath/XQuery] type system includes three unary operators on types: "*", "+", and "?", corresponding respectively to zero or more instances of the type, one or more instances of the type, or an optional instance of the type.

The "&" operator builds the "interleaved product" of two types. The type Type1 & Type2 matches any sequence that is an interleaving of a sequence that matches Type1 and a sequence that matches Type2. The interleaved product captures the semantics of all groups in XML Schema, but it more general has it applies to arbitrary types. All groups in XML Schema are restricted to apply only on global or local element declarations with lower bound 0 or 1, and upper bound 1.

Types precedence order. To improve readability when writing types, we assume the following precedence order between operators on types.

# Operator Associativity
1 | (choice) left-to-right
2 & (interleaving) right-to-left
3 , (sequence) left-to-right
4 *, +, ? (occurrence) left-to-right

Parenthesis can be used to enforce precedence. For instance

  xs:string | xs:integer, xs:float*

is equivalent to

  xs:string | (xs:integer, (xs:float*))

and a different precedence can be obtained by writing

  ((xs:string | xs:integer), xs:float)*

Examples

A sequence of elements

The "," operator builds the "sequence" of two types. For example,

  element title of type xs:string, element year of type xs:integer

is a sequence of an element title of type string followed by an element year of type integer.

The union of two element types

The "|" operator builds the "union" of two types. For example,

  element editor of type xs:string | element bib:author

means either an element editor of type string, or a reference to the global element bib:author.

An all group of two elements

The "&" operator builds the "interleaved product" of two types. For example,

  (element a & element b) =
    element a, element b
  | element b, element a

which specifies that the a and b elements can occur in any order.

An empty type

The following type matches the empty sequence.

  empty

A sequence of zero or more elements

The following type matches zero or more elements each of which can be a surgeon or a plumber.

  (element surgeon | element plumber)*

2.4.4 Top level definitions

Top level definitions correspond to global element declarations, global attribute declarations and type definitions in XML Schema.

Type Definitions
[37 (Formal)]    Definition    ::=    ("define" "element" ElementName Substitution? Nillable? TypeReference)
| ("define" "attribute" AttributeName TypeReference)
| ("define" "type" TypeName TypeDerivation)
[38 (Formal)]    Substitution    ::=    "substitutes" "for" ElementName
[31 (Formal)]    TypeDerivation    ::=    ComplexTypeDerivation | AtomicTypeDerivation
[32 (Formal)]    ComplexTypeDerivation    ::=    Derivation? Mixed? "{" Type? "}"
[33 (Formal)]    AtomicTypeDerivation    ::=    "restricts" AtomicTypeName
[35 (Formal)]    Derivation    ::=    ("restricts" TypeName)
| ("extends" TypeName)
[36 (Formal)]    Mixed    ::=    "mixed"

A type definition has a name (possibly anonymous) and a type derivation. In the case of a complex type, or a simple type derived by list or union, derivation indicates if the type is derived by extension or restriction from its base type, gives its content model, and an optional flag indicating if it has mixed content. In the case of an atomic type, it just indicates from which type it is derived. When the type derivation is omitted, the type derives by restriction from xs:anyType, as in:

  define type Bib { element book* } =
  define type Bib restricts xs:anyType { element book* }

Empty content can be indicated with the explicit empty sequence, or omitted, as in:

  define type Bib { } =
  define type Bib { empty }

Global element and attribute declarations always have a name and a reference to a (possibly anonymous) type. A global element declaration also may declare a substitution group for the element and whether the element is nillable.

Examples

A type declaration with complex content

  define type Address {
    element name of type xsd:string,
    element street of type xsd:string*
  }

A type declaration with complex content derived by extension

  define type USAddress extends Address {
    element zip name of type xsd:integer
  }

A type declaration with mixed content

  define type Section mixed {
    (element h1 of type xsd:string |
     element p of type xsd:string |
     element div of type Section)*
  }

A type declaration with simple content derived by restriction

  define type SKU restricts xsd:string

An element declaration

  define element address of type Address

An element declaration with a substitution group

  define element usaddress substitutes for address of type USAddress

An element declaration which is nillable

  define element zip nillable of type xs:integer

2.4.5 Example of a complete Schema

Here is a schema describing purchase orders from [XML Schema Part 0].

  <xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema">
  
   <xsd:annotation>
    <xsd:documentation xml:lang="en">
     Purchase order schema for Example.com.
     Copyright 2000 Example.com. All rights reserved.
    </xsd:documentation>
   </xsd:annotation>
  
   <xsd:element name="purchaseOrder" type="PurchaseOrderType"/>
  
   <xsd:element name="comment" type="xsd:string"/>
  
   <xsd:complexType name="PurchaseOrderType">
    <xsd:sequence>
     <xsd:element name="shipTo" type="USAddress"/>
     <xsd:element name="billTo" type="USAddress"/>
     <xsd:element ref="comment" minOccurs="0"/>
     <xsd:element name="items"  type="Items"/>
    </xsd:sequence>
    <xsd:attribute name="orderDate" type="xsd:date"/>
   </xsd:complexType>
  
   <xsd:complexType name="USAddress">
    <xsd:sequence>
     <xsd:element name="name"   type="xsd:string"/>
     <xsd:element name="street" type="xsd:string"/>
     <xsd:element name="city"   type="xsd:string"/>
     <xsd:element name="state"  type="xsd:string"/>
     <xsd:element name="zip"    type="xsd:decimal"/>
    </xsd:sequence>
    <xsd:attribute name="country" type="xsd:NMTOKEN" fixed="US"/>
   </xsd:complexType>
  
   <xsd:complexType name="Items">
    <xsd:sequence>
     <xsd:element name="item" minOccurs="0" maxOccurs="unbounded">
      <xsd:complexType>
        <xsd:sequence>
         <xsd:element name="productName" type="xsd:string"/>
         <xsd:element name="quantity">
          <xsd:simpleType>
           <xsd:restriction base="xsd:positiveInteger">
            <xsd:maxExclusive value="100"/>
           </xsd:restriction>
          </xsd:simpleType>
         </xsd:element>
         <xsd:element name="USPrice"  type="xsd:decimal"/>
         <xsd:element ref="comment"   minOccurs="0"/>
         <xsd:element name="shipDate" type="xsd:date" minOccurs="0"/>
        </xsd:sequence>
        <xsd:attribute name="partNum" type="SKU" use="required"/>
      </xsd:complexType>
     </xsd:element>
    </xsd:sequence>
   </xsd:complexType>
  
   <!-- Stock Keeping Unit, a code for identifying products -->
   <xsd:simpleType name="SKU">
    <xsd:restriction base="xsd:string">
     <xsd:pattern value="\d{3}-[A-Z]{2}"/>
    </xsd:restriction>
   </xsd:simpleType>
  
  </xsd:schema>

Here is the mapping of the above schema into the [XPath/XQuery] type system.

  namespace xsd = "http://www.w3.org/2001/XMLSchema"

  define element purchaseOrder of type PurchaseOrderType
 
  define element comment of type xsd:string
  
  define type PurchaseOrderType {
    attribute orderDate of type xsd:date?,
    element shipTo of type USAddress,
    element billTo of type USAddress,
    element comment?,
    element items of type Items
  }

  define type USAddress {
    attribute country of type xsd:NMTOKEN,
    element name of type xsd:string,
    element street of type xsd:string,
    element city of type xsd:string,
    element state of type xsd:string,
    element zip of type xsd:decimal
  }

  define type Items {
    attribute partNum of type SKU,
    element item of type fs:anon1*
  }

  define type fs:anon1 {
    element productName of type xsd:string,
    element quantity of type fs:anon2,
    element USPrice of type xsd:decimal,
    element comment?,
    element shipDate of type xsd:date?
  }

  define type fs:anon2 restricts xsd:positiveInteger

  define type SKU restrict xsd:string

Note that the two anonymous types in the item element declarations are mapping to types with names fs:anon1 and fs:anon2.

The following additional definitions illustrate how more advanced XML Schema features (a complex type derived by extension, an anonymous simple type derived by restriction, and substitution groups) are represented in the [XPath/XQuery] type system.

  <complexType name="NYCAddress">
    <complexContent>
     <extension base="USAddress">
      <sequence>
       <element ref="apt"/>
      </sequence>
     </extension>
    </complexContent>
  </complexType>

  <element name="apt">
    <xsd:simpleType>
     <xsd:restriction base="xsd:positiveInteger">
      <xsd:maxExclusive value="10000"/>
     </xsd:restriction>
    </xsd:simpleType>
  </element>

  <element name="usaddress" substitutionGroup="address" type="USAddress"/>
  <element name="nycaddress" substitutionGroup="usaddress" type="NYCAddress"/>

The above definitions are mapped into the [XPath/XQuery] type system as follows:

  define type NYCAddress extends USAddress {
    element apt
  }

  define element apt of type fs:anon3

  define type fs:anon3 restricts xsd:positiveInteger

  define element usaddress  substitutes for address of type USAddress
  define element nycaddress substitutes for usaddress of type NYCAddress

2.5 Functions and operators

The [Functions and Operators] document defines built-in functions available in [XPath/XQuery]. A number of these functions are used to define the [XPath/XQuery] semantics; those functions are listed in [B.1 Functions and Operators used in the Formal Semantics].

Many functions in the [Functions and Operators] document are generic: they perform operations on arbitrary components of the data model, e.g., any kind of node, or any sequence of items. For instance, the fn:distinct-nodes function removes duplicates in any sequence of nodes. As a result, the signature given in the [Functions and Operators] document is also generic. For instance, the signature of the fn:distinct-nodes function is:

  fn:distinct-nodes(node*) as node*

As defined, this signature provides little useful type information. For such functions, better type information can often be obtained by having the output type depend on the type of input parameters. For instance, if the function fn:distinct-nodes is applied on a parameter of type element a*, element b, one can easily deduce that the resulting sequence is a collection of either a or b elements.

In order to provide better static typing for those functions, specific typing rules are given in [7 Additional Semantics of Functions].

3 Basics

The organization of this section parallels the organization of Section 2 BasicsXQ.

3.1 Expression Context

Introduction

The expression context for a given expression consists of all the information that can affect the result of the expression. This information is organized into the static context and the dynamic context. This section specifies the environments that represent the context information used by [XPath/XQuery] expressions.

3.1.1 Static Context

The environment group statEnv denotes the environments that are available during static analysis. Static analysis may extend parts of the static environment. The static environment is also available during dynamic evaluation.

If analysis of an expression relies on some component of the static context that has not been assigned a value, a static error is raised. This constraint is formalized in [3.3 Error Handling].

The following environments are part of the static environment group:

statEnv.xpath1.0_compatibility
The statEnv.xpath1.0_compatibility environment corresponds to the XPath 1.0 compatibility flag in the [XPath/XQuery] static context. It specifies whether the semantic rules for backward compatibility with XPath 1.0 are in effect.
statEnv.namespace
The statEnv.namespace environment corresponds to statically known namespaces in the [XPath/XQuery] static context.
The statEnv.namespace environment maps a namespace prefix (NCName) onto a namespace kind and a namespace URI (URI) or the null namespace (#NULL-NAMESPACE). The namespace kind is either passive or active. The namespace kind determines whether a namespace node is created for an element during element construction.
statEnv.default_elem_namespace
The statEnv.default_elem_namespace environment corresponds to the default element/type namespace in the [XPath/XQuery] static context.
The statEnv.default_elem_namespace environment contains a namespace URI (a URI) or the null namespace (#NULL-NAMESPACE) and is used for any unprefixed QName appearing in a position where an element or type name is expected.
statEnv.default_function_namespace
The statEnv.default_function_namespace environment corresponds to the default function namespace in the [XPath/XQuery] static context.
The statEnv.default_function_namespace environment contains a namespace URI (a URI) or the null namespace (#NULL-NAMESPACE) and is used for any unprefixed QName appearing as the function name in a function call.
statEnv.typeDefn
The statEnv.typeDefn environment corresponds to the in-scope schema types in the [XPath/XQuery] static context.
The statEnv.typeDefn environment maps expanded type names (expanded TypeNames) onto their type definition (Definition). A type name may be globally declared or anonymous.
statEnv.elemDecl
The statEnv.elemDecl environment corresponds to the in-scope element declarations in the [XPath/XQuery] static context.
The statEnv.elemDecl environment maps expanded element names (expanded ElementNames) onto their declaration (Definition).
statEnv.attrDecl
The statEnv.attrDecl environment corresponds to the in-scope attribute declarations in the [XPath/XQuery] static context.
The statEnv.attrDecl environment maps expanded attribute names (expanded AttributeNames) onto their declaration (Definition).
statEnv.varType
The statEnv.varType environment corresponds to the in-scope variables in the [XPath/XQuery] static context.
The statEnv.varType environment maps expanded variable names (expanded Variables) to their static type (Type).
The context item static type in the [XPath/XQuery] static context is represented by the binding of the variable $fs:dot to its corresponding type in statEnv.varType.
statEnv.funcType
The statEnv.funcType environment corresponds to the function signatures part of the [XPath/XQuery] static context.
The statEnv.funcType environment stores the static type signatures of functions. Because [XPath/XQuery] allows multiple functions with the same name differing only in the number and signature of the parameters, this environment maps an expanded QName to the set of all function declaration signatures of the form "define function QName (Type1, ..., Typen) return Type" each corresponding to a declaration of the function.
statEnv.collations
The statEnv.collations environment corresponds to the statically known collations in the [XPath/XQuery] static context.
The statEnv.collations environment maps a unique namespace URI (a URI) to a pair of functions: the first function takes a set of strings and returns a sequence containing those strings in sorted order; and the second function takes two strings, returns true if they are considered equal, and false if not.
statEnv.defaultCollation
The statEnv.defaultCollation environment corresponds to the default collation in the [XPath/XQuery] static context.
The statEnv.defaultCollation environment is a pair of functions as described in statEnv.collations above.
statEnv.constructionMode
The statEnv.constructionMode environment corresponds to the construction mode in the [XPath/XQuery] static context.
The statEnv.constructionMode environment is one of preserve or strip.
statEnv.orderingMode
The statEnv.orderingMode environment corresponds to the ordering mode in the [XPath/XQuery] static context.
The statEnv.orderingMode environment is one of ordered or unordered.
statEnv.defaultEmptySequenceOrder
The statEnv.defaultEmptySequenceOrder environment corresponds to the default order for empty sequences in the [XPath/XQuery] static context.
The statEnv.defaultEmptySequenceOrder environment controls whether an empty sequence is interpreted as the greatest value or as the least value during processing of an order by clause in a FLWOR expression. Its value may be greatest or least.
statEnv.boundarySpace
The statEnv.boundarySpace environment corresponds to the boundary-space policy in the [XPath/XQuery] static context.
The statEnv.boundarySpace environment controls the processing of boundary whitespace by element constructors. Its value may be preserve or strip.
statEnv.copyNamespacesMode
The statEnv.copyNamespacesMode environment corresponds to the copy-namespaces mode in the [XPath/XQuery] static context.
The statEnv.copyNamespacesMode environment controls the namespace bindings that are assigned when an existing element node is copied by an element constructor. Its value consists of two parts: preserve or no-preserve, and inherit or no-inherit.
statEnv.baseUri
The statEnv.baseUri environment corresponds to the base URI in the [XPath/XQuery] static context.
The statEnv.baseUri environment contains a unique namespace URI (a URI).
statEnv.docType
The statEnv.docType environment corresponds to the statically known documents in the [XPath/XQuery] static context. It contains the static type for the input documents, and is used to provide the static type to the fn:doc function.
The statEnv.docType environment contains bindings from input URIs (a URI) to types (a Type).
statEnv.collectionType
The statEnv.collectionType environment corresponds to the statically known collections in the [XPath/XQuery] static context. It contains the static type for the input collections, and is used to provide the static type to the fn:collection function.
The statEnv.collectionType environment contains bindings from input URIs (a URI) to types (a Type).
statEnv.defaultCollectionType
The statEnv.defaultCollectionType environment corresponds to the statically known default collection type in the [XPath/XQuery] static context. It contains the static type for the default collection, and is used to provide the static type to the fn:collection function when called with no arguments.
The statEnv.defaultCollectionType environment contains type (a Type).

Note that the boundary-space behavior is not formally specified in this document.

Environments have an initial state when [expression/query] processing begins, containing, for example, the function signatures of all built-in functions. The initial values for the static context are defined in Section C Context ComponentsXQ and Section C Context ComponentsXP and is denoted by statEnvDefault in the Formal Semantics.

Here is an example that shows how the static environment is modified in response to a namespace definition.

statEnv + namespace(NCName => (passive, URI)) |- Expr*

statEnv |- declare namespace NCName = URI Expr*

This rule reads as follows: "the phrase on the bottom (a namespace declaration in the query prolog followed by a sequence of expressions) is well-typed (accepted by the static type inference rules) within an environment statEnv if the sequence of expressions above the line is well-typed in the environment obtained from statEnv by adding the namespace declaration".

This is a common idiom for adding new information to an environment and passing that environment for use in sub-expressions. If the environment must be updated with a completely new component, the following notation is used:

statEnv [ namespace = (NewEnvironment) ]

The helper function fs:active_ns(statEnv) returns all the active in-scope namespaces in the given static environment.

For each attribute and element node in Value, such that the node has name expanded-QName in the namespace URI, the helper function fs:get_static_ns_from_items(statEnv, Value) returns the in-scope namespace that corresponds to URI. This is a reverse-lookup on statEnv.namespace by URI.

3.1.1.1 Resolving QNames to Expanded QNames

A common use of the static environment is to expand a QName by looking up the URI that corresponds to the QName's namespace prefix in the statEnv.namespace environment and by constructing an expanded-QNameDM, which contains the URI and the QName's local part. Element and type QNames may be in the null namespace, that is, there is no URI associated with their namespace prefix. The null namespace is denoted by the special value #NULL-NAMESPACE.

The auxiliary judgments below expand an element, type, attribute, variable, or function QName by looking up the namespace prefix in statEnv.namespace or, if the QName is unqualified, by using the appropriate default namespace.

Notation

The judgment

holds when the element or type QName expands to the given expanded QName.

The judgment

holds when the attribute QName expands to the given expanded QName.

The judgment

holds when the variable QName expands to the given expanded QName.

The judgment

holds when the function QName expands to the given expanded QName.

Semantics

An element or type QName consisting of a prefix NCName and a local part NCName expands to the URI (or the null namespace) corresponding to that prefix and the local part.

statEnv.namespace(NCName1) = URI-or-#NULL-NAMESPACE

statEnv |- NCName1:NCName2of elem/type expands to (URI-or-#NULL-NAMESPACE,NCName2)

An element or type QName consisting only of a local part NCName expands to the default element/type namespace and the local part.

statEnv.default_elem_namespace = URI-or-#NULL-NAMESPACE

statEnv |- NCName of elem/type expands to (URI-or-#NULL-NAMESPACE,NCName)

An attribute QName consisting of a prefix NCName and a local part NCName expands to the URI (or the null namespace) corresponding to the prefix and the local part.

statEnv.namespace(NCName1) = URI-or-#NULL-NAMESPACE

statEnv |- NCName1:NCName2of attr expands to (URI-or-#NULL-NAMESPACE,NCName2)

An attribute QName consisting only of a local part NCName expands to the null namespace and the local part.


statEnv |- NCName of attr expands to (#NULL-NAMESPACE,NCName)

A variable QName consisting of a prefix NCName and a local part NCName expands to the URI that corresponds to the prefix and the local part.

statEnv.namespace(NCName1) = URI

statEnv |- NCName1:NCName2of var expands to (URI,NCName2)

A variable QName consisting only of a local part NCName expands to the null namespace and the local part.


statEnv |- NCName of var expands to (#NULL-NAMESPACE,NCName)

A function QName consisting of a prefix NCName and a local part NCName expands to the URI that corresponds to the prefix and the local part.

statEnv.namespace(NCName1) = URI

statEnv |- NCName1:NCName2 of func expands to (URI,NCName2)

A function QName consisting only of a local part NCName expands to the default function namespace URI and the local part.

3.1.2 Dynamic Context

The environment group dynEnv denotes the group of environments built and used during dynamic evaluation.

If evaluation of an expression relies on some component of the dynamic context that has not been assigned a value, a dynamic error is raised. This constraint is formalized in [3.3 Error Handling].

The following environments are part of evaluation environment group:

dynEnv.varValue
The dynEnv.varValue environment corresponds to the variable values, the context item, the context position and the context size in the [XPath/XQuery] evaluation context.
The dynamic value environment maps an expanded variable name (expanded Variable) to the variable's value (Value) or to the value #IMPORTED(URI), if the variable is defined in the imported module with namespace URI.
dynEnv.funcDefn
The dynEnv.funcDefn environment corresponds to the function implementations (or definition) part of the in the [XPath/XQuery] dynamic context.
The dynEnv.funcDefn environment maps an expanded function name and parameter signature of the form "expanded-QName (Type1, ..., Typen)" to the remainder of the corresponding function definition, which is either the value #BUILT-IN for functions defined in [Functions and Operators]; the value #EXTERNAL for externally defined functions; the value #IMPORTED(URI), if the function is defined in the imported module with namespace URI; or, if the function is locally declared, the function's body and a list of variables, which are the function's formal parameters, of the form "(Expr, Variable1,..., Variablen)".
The initial function environment (statEnvDefault.funcDefn) maps the signatures of the internal functions defined in [B.2 Mapping of Overloaded Internal Functions] and the signatures of the functions defined in [Functions and Operators] to #BUILT-IN.
dynEnv.dateTime
The dynEnv.dateTime environment corresponds to the current dateTime in the [XPath/XQuery] dynamic context.
dynEnv.timezone
The dynEnv.timezone environment corresponds to the implicit timezone in the [XPath/XQuery] dynamic context and is used by the timezone related functions in [Functions and Operators].
dynEnv.docValue
The dynEnv.docValue environment corresponds to the available documents in the [XPath/XQuery] dynamic context. It contains the document nodes corresponding to input documents, and is used to provide the dynamic value of the fn:doc function.
The dynEnv.docValue environment contains bindings from input URIs (a URI) to documents (a DocumentValue).
dynEnv.collectionValue
The dynEnv.collectionValue environment corresponds to the available collections in the [XPath/XQuery] dynamic context. It contains the root nodes corresponding to the input collections, and is used to provide the dynamic value of the fn:collection function.
The dynEnv.collectionValue environment contains bindings from input URIs (a URI) to a sequence of nodes.
dynEnv.defaultCollectionValue
The dynEnv.defaultCollectionValue environment corresponds to the default collection in the [XPath/XQuery] dynamic context. It contains the sequence of nodes corresponding to the default collection, and is used to provide the dynamic value of the fn:collection function when called with no arguments.
The dynEnv.defaultCollectionValue environment contains a sequence of nodes.

The initial values for the dynamic context are defined in Section C Context ComponentsXQ and Section C Context ComponentsXP and is denoted by dynEnvDefault in the Formal Semantics.

The following Formal Semantics built-in variables represent the context item, context position, and context size properties of the dynamic context:

Built-in Variable   Represents:
$fs:dot context item
$fs:position context position
$fs:last context size

Variables with the "fs" prefix are reserved for use in the definition of the Formal Semantics. Since there is no namespace URI associated to the "fs" prefix, users cannot refer to such variables.

Values of $fs:position and $fs:last can be obtained by invoking the fn:position and fn:last functions, respectively.

3.2 Processing Model

This section reviews the processing model for [XPath/XQuery], and defines the main judgments that are used in this specification. The [XPath/XQuery] processing model is defined normatively in Section 2.2 Processing ModelXQ. This section also explains how the main judgments (normalization rules, static type inference, and dynamic evaluation) relate to the phases in that processing model.

3.2.1 Processing model

The following figure depicts the [XPath/XQuery] processing model

Processing Model Overview

Figure 1: Processing Model Overview

This processing model is not intended to describe an actual implementation, although a naive implementation might be based upon it. It does not prescribe an implementation technique, but any implementation should produce the same results as obtained by following this processing model and applying the rest of the Formal Semantics specification.

Query processing consists of two phases: a static analysis phase and a dynamic evaluation phase. Static analysis is further divided into four sub-phases. Each phase consumes the result of the previous phase and generates output for the next phase. For each processing phase, we point to the relevant notations introduced later in the document.

[Definition: The static analysis phase depends on the expression itself and on the static context. The static analysis phase does not depend on input data (other than schemas).]

The purpose of the static analysis phase is to detect errors, e.g., syntax errors or type errors, at compile time rather than at run-time. If no error occurs, the result of static analysis could be some compiled form of [expression/query], suitable for execution by a compiled-[expression/query] processor. Static analysis consists of the following sub-phases:

  1. Parsing. (Step SQ1 in Figure 1). The grammar for the [XPath/XQuery] syntax is defined in [XQuery 1.0: A Query Language for XML]. Parsing may generate syntax errors. If no error occurs, an internal operation tree of the parsed query is created.

  2. Static Context Processing. (Steps SQ2, SQ3, and SQ4 in Figure 1). The static semantics of [expression/query] depends on the input static context. The input static context needs to be generated before the [expression/query] can be analysed. In XQuery, the input static context may be defined by the processing environment and by declarations in the Query Prolog (See [5 Modules and Prologs]). In XPath, the input static context is defined by the processing environment. The static context is denoted by statEnv.

  3. Normalization. (Step SQ5 in Figure 1). To simplify the semantics specification, some normalization is performed on the [expression/query]. The [XPath/XQuery] language provides many powerful features that make [expression/query]s simpler to write and use, but are also redundant. For instance, a complex for expression might be rewritten as a composition of several simple for expressions. The language composed of these simpler [expression/query] is called the [XPath/XQuery] Core language and is described by a grammar which is a subset of the XQuery grammar. The grammar of the [XPath/XQuery] Core language is given in [A Normalized core grammar].

    During the normalization phase, each [XPath/XQuery] [expression/query] is mapped into its equivalent [expression/query] in the core. (Note that this has nothing to do with Unicode Normalization, which works on character strings.) Normalization works by bottom-up application of normalization rules over expressions, starting with normalization of literal expressions and variables.

    Specifically the normalization phase is defined in terms of the static part of the context (statEnv) and a [expression/query] (Expr) abstract syntax tree. Formal notations for the normalization phase are introduced in [3.2.2 Normalization judgment].

    After normalization, the full semantics is obtained by giving a semantics to the normalized Core [expression/query]. This is done during the last two phases.

  4. Static type analysis. (Step SQ6 in Figure 1). Static type analysis is optional. If this phase is not supported, then normalization is followed directly by dynamic evaluation.

    Static type analysis checks whether each [expression/query] is type safe, and if so, determines its static type. Static type analysis is defined only for Core [expression/query]. Static type analysis works by bottom-up application of type inference rules over expressions, taking the type of literals and of input documents into account.

    If the [expression/query] is not type-safe, static type analysis yields a type error. For instance, a comparison between an integer value and a string value might be detected as an type error during the static type analysis. If static type analysis succeeds, it yields an abstract syntax tree where each sub-expression is associated with its static type.

    More precisely, the static analysis phase is defined in terms of the static context (statEnv) and a core [expression/query] (CoreExpr). Formal notations for the static analysis phase are introduced in [3.2.3 Static typing judgment].

    Static typing does not imply that the content of XML documents must be rigidly fixed or even known in advance. The [XPath/XQuery] type system accommodates "flexible" types, such as elements that can contain any content. Schema-less documents are handled in [XPath/XQuery] by associating a standard type with the document, such that it may include any legal XML content.

If the static analysis phase succeeds, the dynamic evaluation phase (sometimes also called "execution") evaluates a query on input document(s).

  1. Dynamic Context Processing. (Steps DQ2 and DQ3 in Figure 1).The dynamic semantics of [expression/query] depends on the dynamic input context. The dynamic input context needs to be generated before the [expression/query] can be evaluated. The dynamic input context may be defined by the processing environment and by statements in the Query Prolog (See [5 Modules and Prologs]). In XPath, the dynamic input context is defined by the processing environment. The static input context is denoted by dynEnv.

  2. Dynamic Evaluation. (Steps DQ4 and DQ5 in Figure 1). This phase computes the value of an [expression/query]. The semantics of evaluation is defined only for Core [expression/query] terms. Evaluation works by bottom-up application of evaluation rules over expressions, starting with evaluation of literals and variables. Evaluation may result in a value OR a dynamic error, which may be a non-type error or a type error. If static typing of an expression does not raise a type error, then dynamic evaluation of the same expression will not raise a type error (and thus dynamic type checking can be avoided when static typing is enabled). Dynamic evaluation may still raise a non-type error.

    The dynamic evaluation phase is defined in terms of the static context (statEnv) and evaluation context (dynEnv), and a core [expression/query] (CoreExpr). Formal notations for the dynamic evaluation phase are introduced in [3.2.4 Dynamic evaluation judgment].

Static type analysis catches only certain classes of errors. For instance, it can detect a comparison operation applied between incompatible types (e.g., xs:int and xs:date). Some other classes of errors cannot be detected by the static analysis and are only detected at evaluation time. For instance, whether an arithmetic expression on 32 bits integers (xs:int) yields an out-of-bound value can only be detected at run-time by looking at the data.

While implementations are free to implement different processing models, the [XPath/XQuery] static semantics relies on the existence of a static type analysis phase that precedes any access to the input data. Statically typed implementations are required to find and report type errors during static analysis, as specified in this document. Dynamically typed implementations are required to find and report type errors during evaluation, but are permitted to report them during static analysis.

Notice that the separation of logical processing into phases is not meant to imply that implementations must separate the static analysis phase from the dynamic evaluation phase; processors may choose to perform all phases simultaneously at evaluation-time and may even mix the phases in their internal implementations. The processing model simply defines the final result.

The above processing phases are all internal to the [XPath/XQuery] processor. They do not deal with how the [XPath/XQuery] processor interacts with the outside world, notably how it accesses actual documents and types. A typical [expression/query] engine would support at least three other important processing phases:

  1. Schema Import Processing. The [XPath/XQuery] type system is based on XML Schema. In order to perform dynamic or static typing, the [XPath/XQuery] processor needs to build type descriptions that correspond to the schema(s) of the input documents. This phase is achieved by mapping all schemas required by the [expression/query] into the [XPath/XQuery] type system. The XML Schema import phase is described in [C Importing Schemas].

  2. Data Model Generation. Expressions are evaluated on values in the [Data Model]. XML documents must be loaded into the [Data Model] before the evaluation phase. This is described in the [Data Model] and is not discussed further here.

  3. Serialization. Once the [expression/query] is evaluated, processors might want to serialize the result of the [expression/query] as actual XML documents. Serialization of data model instances is described in [Data Model Serialization] and is not discussed further here.

The parsing phase is not specified formally; the formal semantics does not define a formal model for the syntax trees, but uses the [XPath/XQuery] concrete syntax directly. More details about parsing for XQuery 1.0 can be found in the [XQuery 1.0: A Query Language for XML] document and more details about parsing for XPath 2.0 can be found in the [XML Path Language (XPath) 2.0] document. No further discussion of parsing is included here.

3.2.2 Normalization judgment

Normalization is specified using mapping rules, which describe how a [XPath/XQuery] expression is rewritten into an expression in the [XPath/XQuery] Core. Mapping rules are also used in [C Importing Schemas] to specify how XML Schemas are imported into the [XPath/XQuery] type system.

Notation

Mapping rules are written using a square bracket notation, as follows:

 
[Object]Subscript
==
Mapped Object

The original "object" is written above the == sign. The rewritten "object" is written beneath the == sign. The subscript is used to indicate what kind of "object" is mapped, and sometimes to pass some information between mapping rules.

Since normalization is always applied in the presence of a static context, the above rule is a shorthand for:

statEnv |- [Object] Subscript == Mapped Object

The static environment is used in certain normalization rules (e.g. for normalization of function calls). To keep the notation simpler, the static environment is not written in the normalization rules, but it is assumed to be available.

The normalization rule that is used to map "top-level" expressions in the [XPath/XQuery] syntax into expressions in the [XPath/XQuery] Core is:

 
[Expr]Expr
==
CoreExpr

which indicates that the expression Expr is normalized to the expression CoreExpr in the [XPath/XQuery] core (with the implied statEnv).

Example

For instance, the following [expression/query]

    for $i in (1, 2),
        $j in (3, 4)
    return
      element pair { ($i,$j) }

is normalized to the core expression

    for $i in (1, 2) return
      for $j in (3, 4) return
          element pair { ($i,$j) }

in which the "FWLR" expression is mapped into a composition of two simpler "for" expressions.

3.2.3 Static typing judgment

The static semantics is specified using type inference rules, which relate [XPath/XQuery] expressions to types and specify under what conditions an expression is well typed.

Notation

The judgment

statEnv |- Expr : Type

holds when, in the static environment statEnv, the expression Expr has type Type.

Example

The result of static type inference is to associate a static type with every [expression/query], such that any evaluation of that [expression/query] is guaranteed to yield a value that belongs to that type.

For instance, the following expression.

   let $v := 3 return $v+5

has type xs:integer. This can be inferred as follows: the input literals '3' and '5' have type integer, so the variable $v also has type integer. Since the sum of two integers is an integer, the complete expression has type integer.

Note

The type of an expression is computed by inference. Static type inference rules define for each kind of expression how to compute the type of the expression given the types of its sub-expressions. Here is a simple example:

statEnv |- Expr1 : xs:boolean      statEnv |- Expr2 : Type2      statEnv |- Expr3 : Type3

statEnv |- if Expr1 then Expr2 else Expr3 : ( Type2 | Type3 )

This rule states that if the conditional expression of an "if" expression has type boolean, then the type of the entire expression is one of the two types of its "then" and "else" clauses. Note that the resulting type is represented as a union: '(Type2|Type3)'.

The "left half" (the part before the :) of the expression below the line corresponds to some [expression/query], for which a type is computed. If the [expression/query] has been parsed into an internal abstract syntax tree, this usually corresponds to some node in that tree. The expression usually has patterns in it (here Expr1, Expr2, and Expr3) that need to be matched against the children of the node in the abstract syntax tree. The expressions above the line indicate things that need to be computed to use this rule; in this case, the types of the condition expression and the two branches of the if-then-else expression. Once those types are computed (by further applying static inference rules recursively to the expressions on each side), then the type of the expression below the line can be computed. This example illustrates a general feature of the [XPath/XQuery] type system: the type of an expression depends only on the type of its sub-expressions. The overall static type inference algorithm is recursive, following the abstract syntax of the [expression/query]. At each point in the recursion, an appropriate matching inference rule is sought; if at any point there is no applicable rule, then static type inference has failed and the [expression/query] is not type correct.

3.2.4 Dynamic evaluation judgment

The dynamic, or operational, semantics is specified using value inference rules, which relate [XPath/XQuery] expressions to values, and in some cases specify the order in which an [XPath/XQuery] expression is evaluated.

Notation

The judgment

statEnv ; dynEnv |- Expr => Value

holds when, in the static environment statEnv and dynamic environment dynEnv, the expression Expr yields the value Value.

The judgment

statEnv ; dynEnv |- Expr raises Error

holds when, in the static environment statEnv and dynamic environment dynEnv, the expression Expr raises the error Error.

The static environment is used in certain cases (e.g. for type matching) during evaluation. To keep the notation simpler, the static environment is not written in the dynamic inference rules, but it is assumed to be available.

Example

For instance, the following expression.

   let $v := 3 return $v+5

yields the integer value 8. This can be inferred as follows: the input literals '3' and '5' denote the values 3 and 5, respectively, so the variable $v has the value 3. Since the sum of 3 and 5 is 8, the complete expression has the value 8.

Note

As with static type inference, logical inference rules are used to determine the value of each expression, given the dynamic environment and the values of its sub-expressions.

The inference rules used for dynamic evaluation, like those for static type inference, follow a bottom-up recursive structure, computing the value of expressions from the values of their sub-expressions.

3.3 Error Handling

Expressions can raise errors during static analysis or dynamic evaluation. The [Functions and Operators] [XQuery 1.0: A Query Language for XML], and [XML Path Language (XPath) 2.0] specify the conditions under which an expression or operator raises an error. The user may raise an error explicitly by calling the fn:error function, which takes an optional item as an argument.

3.3.1 Kinds of Errors

Notation

The symbol Error denotes any error. We distinguish between a static errorXQ (denoted by statError), a type errorXQ (denoted by typeError), and a generic dynamic errorXQ (denoted by dynError), which represents all dynamic errors. A static error is raised during static analysis. A type error may be raised during static analysis or dynamic evaluation. A dynamic error is raised during dynamic evaluation. Non-type static errors are not formalized in this document.

Note:

We use a generic dynamic error. The [Functions and Operators] and [XQuery 1.0: A Query Language for XML] documents raise specific error conditions, but because these error conditions can be implemented in any way, we do not formalize them here.

3.3.2 Identifying and Reporting Errors

The errors defined in this specification are identified by QNames that have the form err:XXYYnnnn, as described in [XQuery 1.0: A Query Language for XML].

3.3.3 Handling Dynamic Errors

In general, when an error is raised during evaluation of some expression Expr, the error is propogated to the expression Expr1 in which Expr is evaluated. The expression Expr1, in turn, propogates the error to the expression in which Expr1 is evaluated, and so on, until the error is returned to the query environment.

Since most expressions propogate errors as described, we use one inference rule to specify this default behavior. The rule below states that if any sub-expression Expri of expression Expr raises an error dynError then Expr also raises dynError.

dynEnv |- Expri raises dynError      Expri is any subexpression of Expr

dynEnv |- Expr raises dynError

There are several expressions, such as [4.6 Logical Expressions] and [4.11 Quantified Expressions], that do not necessarily propogate an error raised by some sub-expression. For each such expression, we give specific error inference rules.

If analysis (evaluation) of an expression relies on some component of the static (dynamic) context that has not been assigned a value, a static (dynamic) error is raised. The following two rules handle all those cases when a component of an environment is accessed but not defined.

statEnv.component(symbol) undefined

statEnv |- Expr raises statError

dynEnv.component(symbol) undefined

dynEnv |- Expr raises dynError

3.3.4 Errors and Optimization

In [XPath/XQuery], the detection and reporting of dynamic errors is implementation dependent. This permits different implementations to choose to evaluate or optimize an expression in different ways. When an implementation is able to evaluate an expression without evaluating some subexpression, the implementation is never required to evaluate that subexpression solely to determine whether it raises a dynamic error. For example, if a function parameter is never used in the body of the function, an implementation may choose whether to evaluate the expression bound to that parameter in a function call. Similarly, if the variable bound by a let expression is never used in the corresponding return expression, the implementation is not required to evaluate the expression to which the variable is bound.

For simplicity, the dynamic inference rules in Formal Semantics define an eager evaluation semantics for all expressions, i.e., all sub-expressions are evaluated regardless of whether their values are necessary to evaluate the containing expression. For example, every function parameter is evaluated before the body of the function is evaluated, and the expression bound to a let variable is always evaluated. The dynamic semantics rules in the Formal Semantics do not formalize the more flexible evaluation strategy above.

For example, in the following expression, the dynamic semantics rules of the Formal Semantics would raise a dynamic error because a path expression may not be applied to an atomic value. An implementation, however, may not raise an error, because the path expression is not necessary to evaluate the containing let expression.

 let $x := 1/foobar return 1
    

However, the static semantic rules, by definition, are conservative, and therefore a type is computed for every subexpression. In the example above, a static type error would be raised because a path expression may be applied to an atomic value.

3.4 Concepts

[XPath/XQuery] is most generally used to process documents. The representation of a document is normatively defined in [Data Model]. The functions used to access documents and collections are normatively defined in [Functions and Operators].

3.4.1 Document Order

Document order is defined in [Data Model].

3.4.2 Atomization

Atomization converts an item sequence into a sequence of atomic values and is implemented by the fn:data function. Atomization is applied in contexts where an arbitrary sequence of items is used where a sequence of atomic values is expected.

3.4.3 Effective Boolean Value

If a sequence of items is encountered where a boolean value is expected, the item sequence's effective boolean value is used. The fn:boolean function returns the effective boolean value of an item sequence.

3.4.4 Input Sources

[XPath/XQuery] has a set of functions that provide access to input data. These functions are of particular importance because they provide a way in which an expression can reference a document or a collection of documents. The dynamic semantics of these three input functions are described in more detail in [Functions and Operators].

3.4.5 URI Literals

In certain places in the XQuery grammar, a statically known valid absolute URI is required. Those cases are treated as described in [XQuery 1.0: A Query Language for XML]

3.5 Types

3.5.1 Predefined Schema Types

All the built-in types of XML Schema are recognized by [XPath/XQuery]. In addition, [XPath/XQuery] recognizes the predefined types xdt:anyAtomicType, xdt:untypedAtomic and xdt:untyped and the duration subtypes xdt:yearMonthDuration and xdt:dayTimeDuration . The definition of those types in the [XPath/XQuery] type system is given below.

[Definition: The following type definition of xs:anyType reflects the semantics of the Ur type from Schema in the [XPath/XQuery] type system.]

  define type xs:anyType restricts xs:anyType {
    attribute*,
    ( xdt:anyAtomicType* | ( element | text | comment | processing-instruction )* )
  }

[Definition: The following type definition of xs:anySimpleType reflects the semantics of the Ur simple type from Schema in the [XPath/XQuery] type system.]

  define type xs:anySimpleType restricts xs:anyType {
    xdt:anyAtomicType*
  }

The name of the Ur simple type is xs:anySimpleType. It is derived by restriction from xs:anyType, its content is a sequence any atomic types.

[Definition: The following type definition of xdt:anyAtomicType reflects the semantics of xdt:anyAtomicType in the [XPath/XQuery] type system.]

  define type xdt:anyAtomicType restricts xs:anySimpleType {
    ( xs:string
    | xs:boolean
    | xs:decimal
    | xs:float
    | xs:double
    | xs:duration
    | xs:dateTime
    | xs:time
    | xs:date
    | xs:gYearMonth
    | xs:gYear
    | xs:gMonthDay
    | xs:gDay
    | xs:gMonth
    | xs:hexBinary
    | xs:base64Binary
    | xs:anyURI
    | xs:QName
    | xs:NOTATION
    | xdt:untypedAtomic )
  }

[Definition: The following type definitions of the XML Schema primitive types reflects the semantics of the primitive types from Schema in the [XPath/XQuery] type system.]

  define type xs:string       restricts xdt:anyAtomicType
  define type xs:boolean      restricts xdt:anyAtomicType
  define type xs:decimal      restricts xdt:anyAtomicType
  define type xs:float        restricts xdt:anyAtomicType
  define type xs:double       restricts xdt:anyAtomicType
  define type xs:duration     restricts xdt:anyAtomicType
  define type xs:dateTime     restricts xdt:anyAtomicType
  define type xs:time         restricts xdt:anyAtomicType
  define type xs:date         restricts xdt:anyAtomicType
  define type xs:gYearMonth   restricts xdt:anyAtomicType
  define type xs:gYear        restricts xdt:anyAtomicType
  define type xs:gMonthDay    restricts xdt:anyAtomicType
  define type xs:gDay         restricts xdt:anyAtomicType
  define type xs:gMonth       restricts xdt:anyAtomicType
  define type xs:hexBinary    restricts xdt:anyAtomicType
  define type xs:base64Binary restricts xdt:anyAtomicType
  define type xs:anyURI       restricts xdt:anyAtomicType
  define type xs:QName        restricts xdt:anyAtomicType
  define type xs:NOTATION     restricts xdt:anyAtomicType

All of those primitive types derive from xdt:anyAtomicType. Note that the value space of each atomic type (such as xs:string) does not appear. The value space for each type is built-in and is as defined in [Schema Part 2].

[Definition: The type xdt:untypedAtomic is defined as follows.]

  define type xdt:untypedAtomic restricts xdt:anyAtomicType

Note that this rule does not indicate the value space of xdt:untypedAtomic. By definition, xdt:untypedAtomic has the same value space as xs:string.

The following example shows two atomic values. The first one is a value of type string containing "Database". The second one is an untyped atomic value containing "Database".

  "Databases" of type xs:string
  "Databases" of type xdt:untypedAtomic

[Definition: The type xdt:untyped is defined as follows.]

  define type xdt:untyped restricts xs:anyType {
    attribute of type xdt:untypedAtomic*,
    ( element of type xdt:untyped | text | comment | processing-instruction? )*
  }

[Definition: The following type definitions of the XML Schema derived types reflects the semantics of the XML Schema types derived by restriction from another atomic type.]

  define type xs:normalizedString   restricts xs:string
  define type xs:token              restricts xs:normalizedString
  define type xs:language           restricts xs:token
  define type xs:NMTOKEN            restricts xs:token
  define type xs:Name               restricts xs:token
  define type xs:NCName             restricts xs:Name
  define type xs:ID                 restricts xs:Name
  define type xs:IDREF              restricts xs:Name
  define type xs:ENTITY             restricts xs:Name
  define type xs:integer            restricts xs:decimal
  define type xs:nonPositiveInteger restricts xs:integer
  define type xs:negativeInteger    restricts xs:nonPositiveInteger
  define type xs:long               restricts xs:integer
  define type xs:int                restricts xs:long
  define type xs:short              restricts xs:int
  define type xs:byte               restricts xs:short
  define type xs:nonNegativeInteger restricts xs:integer
  define type xs:unsignedLong       restricts xs:nonNegativeInteger
  define type xs:unsignedInt        restricts xs:unsignedLong
  define type xs:unsignedShort      restricts xs:unsignedInt
  define type xs:unsignedByte       restricts xs:unsignedShort
  define type xs:positiveInteger    restricts xs:nonNegativeInteger

Three XML Schema built-in derived types are derived by list, as follows. Note that those derive directly from xs:anySimpleType, since they are derived by list, and that their value space is defined using a "one or more" occurrence indicator.

  define type xs:NMTOKENS restricts xs:anySimpleType { xs:NMTOKEN+ }
  define type xs:IDREFS   restricts xs:anySimpleType { xs:IDREF+ }
  define type xs:ENTITIES restricts xs:anySimpleType { xs:ENTITY+ }

For example, here is an element whose content is of type xs:IDREFS.

  element a of type xs:IDREFS {
    "id1" of type xs:IDREF,
    "id2" of type xs:IDREF,
    "id3" of type xs:IDREF
  }

Note that the type name xs:IDREFS derives from xs:anySimpleType, but not from xs:IDREF. As a consequence, calling the following three XQuery functions with the element a as a parameter succeeds for f1 and f2, but raises a type error for f3.

  define function f1($x as element(*,xs:anySimpleType)) { $x }
  define function f2($x as element(*,xs:IDREFS)) { $x }
  define function f3($x as element(*,xs:IDREF)) { $x }

[Definition: The totally ordered duration types, xdt:yearMonthDuration and xdt:dayTimeDuration , are derived by restriction from xs:duration.]

  define type xdt:yearMonthDuration restricts xs:duration
  define type xdt:dayTimeDuration   restricts xs:duration

[Definition: In addition, the Formal Semantics uses the additional type fs:numeric. This type is necessary for the specification of some of XPath type conversion rules. It is defined as follows.]

  define type fs:numeric restricts xs:anyAtomicType { xs:decimal | xs:float | xs:double }

3.5.2 Typed Value and String Value

The typed value of a node is computed by the fn:data function, and the string value of a node is computed by the fn:string function, defined in [Functions and Operators]. The normative definitions of typed value and string value are defined in [Data Model].

3.5.3 SequenceType Syntax

Introduction

Sequence types can be used in [XPath/XQuery] to refer to an XML Schema type. Sequence types are used to declare the types of function parameters and in several [XPath/XQuery] expressions.

The syntax of sequence types is described by the following grammar productions.

SequenceType
[117 (XQuery)]    SequenceType    ::=    (ItemType OccurrenceIndicator?)
| ("void" "(" ")")
[119 (XQuery)]    ItemType    ::=    AtomicType | KindTest | ("item" "(" ")")
[118 (XQuery)]    OccurrenceIndicator    ::=    "?" | "*" | "+"
[120 (XQuery)]    AtomicType    ::=    QName
[121 (XQuery)]    KindTest    ::=    DocumentTest
| ElementTest
| AttributeTest
| SchemaElementTest
| SchemaAttributeTest
| PITest
| CommentTest
| TextTest
| AnyKindTest
[123 (XQuery)]    DocumentTest    ::=    "document-node" "(" (ElementTest | SchemaElementTest)? ")"
[131 (XQuery)]    ElementTest    ::=    "element" "(" (ElementNameOrWildcard ("," TypeName "?"?)?)? ")"
[133 (XQuery)]    SchemaElementTest    ::=    "schema-element" "(" ElementDeclaration ")"
[134 (XQuery)]    ElementDeclaration    ::=    ElementName
[127 (XQuery)]    AttributeTest    ::=    "attribute" "(" (AttribNameOrWildcard ("," TypeName)?)? ")"
[129 (XQuery)]    SchemaAttributeTest    ::=    "schema-attribute" "(" AttributeDeclaration ")"
[130 (XQuery)]    AttributeDeclaration    ::=    AttributeName
[132 (XQuery)]    ElementNameOrWildcard    ::=    ElementName | "*"
[136 (XQuery)]    ElementName    ::=    QName
[128 (XQuery)]    AttribNameOrWildcard    ::=    AttributeName | "*"
[135 (XQuery)]    AttributeName    ::=    QName
[137 (XQuery)]    TypeName    ::=    QName
[126 (XQuery)]    PITest    ::=    "processing-instruction" "(" (NCName | StringLiteral)? ")"
[125 (XQuery)]    CommentTest    ::=    "comment" "(" ")"
[124 (XQuery)]    TextTest    ::=    "text" "(" ")"
[122 (XQuery)]    AnyKindTest    ::=    "node" "(" ")"

Core Grammar

The Core grammar productions for sequence types are:

[80 (Core)]    SequenceType    ::=    (ItemType OccurrenceIndicator?)
| ("void" "(" ")")
[82 (Core)]    ItemType    ::=    AtomicType | KindTest | ("item" "(" ")")
[81 (Core)]    OccurrenceIndicator    ::=    "?" | "*" | "+"
[83 (Core)]    AtomicType    ::=    QName
[84 (Core)]    KindTest    ::=    DocumentTest
| ElementTest
| AttributeTest
| SchemaElementTest
| SchemaAttributeTest
| PITest
| CommentTest
| TextTest
| AnyKindTest
[86 (Core)]    DocumentTest    ::=    "document-node" "(" (ElementTest | SchemaElementTest)? ")"
[94 (Core)]    ElementTest    ::=    "element" "(" (ElementNameOrWildcard ("," TypeName "?"?)?)? ")"
[96 (Core)]    SchemaElementTest    ::=    "schema-element" "(" ElementDeclaration ")"
[97 (Core)]    ElementDeclaration    ::=    ElementName
[90 (Core)]    AttributeTest    ::=    "attribute" "(" (AttribNameOrWildcard ("," TypeName)?)? ")"
[92 (Core)]    SchemaAttributeTest    ::=    "schema-attribute" "(" AttributeDeclaration ")"
[93 (Core)]    AttributeDeclaration    ::=    AttributeName
[95 (Core)]    ElementNameOrWildcard    ::=    ElementName | "*"
[99 (Core)]    ElementName    ::=    QName
[91 (Core)]    AttribNameOrWildcard    ::=    AttributeName | "*"
[98 (Core)]    AttributeName    ::=    QName
[100 (Core)]    TypeName    ::=    QName
[89 (Core)]    PITest    ::=    "processing-instruction" "(" (NCName | StringLiteral)? ")"
[88 (Core)]    CommentTest    ::=    "comment" "(" ")"
[87 (Core)]    TextTest    ::=    "text" "(" ")"
[85 (Core)]    AnyKindTest    ::=    "node" "(" ")"

The semantics of SequenceTypes is defined by means of normalization rules from SequenceTypes into types in the [XPath/XQuery] type system (See [2.4 The [XPath/XQuery] Type System]).

However, the [XPath/XQuery] type system not being part of the [XPath/XQuery] syntax, the SequenceType syntax is still part of the [XPath/XQuery] core. Normalization from SequenceTypes to types is not applied during the normalization phase but whenever a dynamic or static rule requires it. Normalization of SequenceTypes is the only example of normalization that does not yield an expression in the [XPath/XQuery] core and that occurs on-demand in dynamic or static rules.

3.5.4 SequenceType Matching

Introduction

During processing of a query, it is sometimes necessary to determine whether a given value matches a type that was declared using the SequenceType syntax. This process is known as SequenceType matching, and is formally specified in [8.3 Judgments for type matching].

Notation

To define normalization of SequenceTypes to the [XPath/XQuery] type system, the following auxiliary mapping rule is used.

 
[SequenceType]sequencetype
==
Type

specifies that SequenceType is mapped to a Type, in the [XPath/XQuery] type system.

Normalization

OccurenceIndicators are left unchanged when normalizing SequenceTypes into [XPath/XQuery] types. Each kind of SequenceType component is normalized separately into the [XPath/XQuery] type system.

 
[ItemType OccurrenceIndicator]sequencetype
==
[ItemType]sequencetype OccurrenceIndicator

The "void()" sequence type is mapped to the empty type.

 
[void()]sequencetype
==
empty

An atomic type is normalized to itself in the [XPath/XQuery] type system.

 
[AtomicType]sequencetype
==
AtomicType

An "element" SequenceType without content or with a wildcard and no type name is normalized into a wildcard element type.

 
[element()]sequencetype
==
element
 
[element(*)]sequencetype
==
element

An "element" SequenceType with a wildcard and a type name is normalized into a wildcard element type with a corresponding type name. The presence of a "?" after the type name indicates a nillable element.

 
[element(*,TypeName)]sequencetype
==
element of type TypeName
 
[element(*,TypeName?)]sequencetype
==
element nillable of type TypeName

An "element" SequenceType with a name and a type name is normalized into an element type with a corresponding type name. The presence of a "?" after the type name indicates a nillable element.

 
[element(ElementName,TypeName)]sequencetype
==
element ElementName of type TypeName
 
[element(ElementName,TypeName?)]sequencetype
==
element ElementName nillable of type TypeName

An "element" SequenceType with only a name is normalized into a nillable element type with a corresponding name. The reason for the normalization to allow nillable elements is because the semantics of SequenceTypes in that case allows it to match every possible element with that names, regardless of its type or nilled property.

 
[element(ElementName)]sequencetype
==
element ElementName nillable of type xs:anyType

A "schema-element" SequenceType with an element declaration is normalized into a reference to the corresponding global element declaration.

 
[schema-element(ElementName)]sequencetype
==
element ElementName

An "attribute" SequenceType without content or with a wildcard and no type name is normalized into a wildcard attribute type.

 
[attribute()]sequencetype
==
attribute
 
[attribute(*)]sequencetype
==
attribute

An "attribute" SequenceType with a wildcard and a type name is normalized into a wildcard attribute type with a corresponding type name.

 
[attribute(*,TypeName)]sequencetype
==
attribute of type TypeName

An "attribute" SequenceType with a name and a type name is normalized into an attribute type with a corresponding type name.

 
[attribute(AttributeName,TypeName)]sequencetype
==
attribute AttributeName of type TypeName

A "schema-attribute" SequenceType with an attribute declaration is normalized into a reference to the corresponding global attribute declaration.

 
[schema-attribute(AttributeName)]sequencetype
==
attribute AttributeName

A "document-node()" sequence types is normalized into the corresponding document type.

 
[document-node()]sequencetype
==
document

A "document-node" sequence type with an element test (resp. a schema element test) is normalized into the corresponding document type, whose content is the normalization of the element test (resp. schema element test), interleaved with an arbitrary sequence of processing instruction, comment, and text nodes.

 
[document-node(ElementTest)]sequencetype
==
document { [ElementTest]sequencetype & ( processing-instruction | comment ) *}
 
[document-node(SchemaElementTest)]sequencetype
==
document { [SchemaElementTest]sequencetype & ( processing-instruction | comment ) *}

A "processing-instruction()" SequenceType is normalized into the corresponding processing-instruction type.

 
[processing-instruction()]sequencetype
==
processing-instruction

The [XPath/XQuery] type system does not model the target of a processing-instruction, which is treated as a dynamic property. Therefore a "processing-instruction" SequenceType with a string or NCName parameter is normalized into an optional processing-instruction type.

 
[processing-instruction(String)]sequencetype
==
processing-instruction ?
 
[processing-instruction(NCName)]sequencetype
==
processing-instruction ?

A "comment()" SequenceType is normalized into the corresponding comment type.

 
[comment()]sequencetype
==
comment

A "text()" SequenceType is normalized into the corresponding text type.

 
[text()]sequencetype
==
text

The "node()" SequenceType denotes any node. It is normalized into a choice between the corresponding wildcard types for each kind of node.

 
[node()]sequencetype
==
(element | attribute | text | document | comment | processing-instruction)

The "item()" SequenceType denotes any node or atomic value. It is normalized into a choice between the corresponding wildcard types for each kind of nodes or atomic values.

 
[item()]sequencetype
==
(element | attribute | text | document | comment | processing-instruction | xdt:anyAtomicType )

3.6 Comments

[154 (XQuery)]    Comment    ::=    "(:" (CommentContents | Comment)* ":)"
[155 (XQuery)]    CommentContents    ::=    (Char+ - (Char* ':)' Char*))

Comments are lexical constructs only, and have no effect on the meaning of the query, and therefore do not have any formal semantics.

4 Expressions

This section gives the semantics of all the [XPath/XQuery] expressions. The organization of this section parallels the organization of Section 3 ExpressionsXQ.

[31 (XQuery)]    Expr    ::=    ExprSingle ("," ExprSingle)*
[32 (XQuery)]    ExprSingle    ::=    FLWORExpr
| QuantifiedExpr
| TypeswitchExpr
| IfExpr
| OrExpr
[1 (XPath)]    XPath    ::=    Expr

For each expression, a short description and the relevant grammar productions are given. The semantics of an expression includes the normalization, static analysis, and dynamic evaluation phases. Recall that normalization rules translate [XPath/XQuery] syntax into Core syntax. In the sections that contain normalization rules, the Core grammar productions into which the expression is normalized are also provided. After normalization, sections on static type inference and dynamic evaluation define the static type and dynamic value for the Core expression.

Core Grammar

The Core grammar productions for expressions are:

[30 (Core)]    Expr    ::=    ExprSingle ("," ExprSingle)*
[31 (Core)]    ExprSingle    ::=    FLWORExpr
| TypeswitchExpr
| IfExpr
| OrExpr

Static Type Analysis

It is a static type error for most (but not all) expressions to have the empty type. The exceptions to this rule are the following expressions and functions:

The reason the above expressions and functions are excluded is that they are typically part of the result of normalizing a larger user-level expression and are used to capture the semantics of the user-level expression when applied to the empty sequence.

The rule below enforces the above constraints. The static typing rule for () is in [4.1.3 Parenthesized Expressions].

statEnv |- Expr : Type      not(Expr is empty sequence expression () or fn:data or any fs function applied to empty sequence expression ())     not(Type = empty)

statEnv |- Expr : Type

The rule is written in this way (i.e., in the double negative), because for any expression such that no static type rule applies to the expression, a static type error is raised. That is, the absence of an applicable static rule indicates an error. For example, if an expression is not the empty-sequence expression but has the empty type, the above rule does not apply and therefore a static error is raised.

Example

The above rule can catch common mistakes, such as the misspelling of an element or attribute name or referencing of an element or attribute that does not exist. For instance, the following path expression

  $x/title

raises a static error if the type of variable $x does not include any title children elements.

4.1 Primary Expressions

Primary expressions are the basic primitives of the language.They include literals, variables, function calls, and the parenthesized expressions.

Primary Expressions
[83 (XQuery)]    PrimaryExpr    ::=    Literal | VarRef | ParenthesizedExpr | ContextItemExpr | FunctionCall | Constructor | OrderedExpr | UnorderedExpr

Core Grammar

The Core grammar production for primary expressions is:

Primary Expressions
[62 (Core)]    PrimaryExpr    ::=    Literal | VarRef | ParenthesizedExpr | FunctionCall

4.1.1 Literals

Introduction

A literal is a direct syntactic representation of an atomic value. [XPath/XQuery] supports two kinds of literals: string literals and numeric literals.

Literals
[84 (XQuery)]    Literal    ::=    NumericLiteral | StringLiteral
[85 (XQuery)]    NumericLiteral    ::=    IntegerLiteral | DecimalLiteral | DoubleLiteral
[138 (XQuery)]    IntegerLiteral    ::=    Digits
[139 (XQuery)]    DecimalLiteral    ::=    ("." Digits) | (Digits "." [0-9]*)
[140 (XQuery)]    DoubleLiteral    ::=    (("." Digits) | (Digits ("." [0-9]*)?)) [eE] [+-]? Digits
[142 (XQuery)]    StringLiteral    ::=    ('"' (PredefinedEntityRef | CharRef | ('"' '"') | [^"&])* '"') | ("'" (PredefinedEntityRef | CharRef | ("'" "'") | [^'&])* "'")
[147 (XQuery)]    PredefinedEntityRef    ::=    "&" ("lt" | "gt" | "amp" | "quot" | "apos") ";"
[146 (XQuery)]    Digits    ::=    [0-9]+

Core Grammar

The Core grammar productions for literals are:

Literals
[63 (Core)]    Literal    ::=    NumericLiteral | StringLiteral
[64 (Core)]    NumericLiteral    ::=    IntegerLiteral | DecimalLiteral | DoubleLiteral
[101 (Core)]    IntegerLiteral    ::=    Digits
[102 (Core)]    DecimalLiteral    ::=    ("." Digits) | (Digits "." [0-9]*)
[103 (Core)]    DoubleLiteral    ::=    (("." Digits) | (Digits ("." [0-9]*)?)) [eE] [+-]? Digits
[105 (Core)]    StringLiteral    ::=    ('"' (('"' '"') | [^"])* '"') | ("'" (("'" "'") | [^'])* "'")
[110 (Core)]    PredefinedEntityRef    ::=    "&" ("lt" | "gt" | "amp" | "quot" | "apos") ";"
[109 (Core)]    Digits    ::=    [0-9]+

Normalization

All literals are Core expressions, therefore no normalization rules are required for literals. Predefined entity references and character references in strings are resolved to characters as part of parsing and therefore they do not occur in the Core grammar.

Static Type Analysis

In the static semantics, the type of an integer literal is simply xs:integer:


statEnv |- IntegerLiteral : xs:integer

Dynamic Evaluation

In the dynamic semantics, an integer literal is evaluated by constructing an atomic value in the data model, which consists of the literal value and its type:


dynEnv |- IntegerLiteral => xs:integer (IntegerLiteral)

The formal definitions of decimal, double, and string literals are analogous to those for integer.

Static Type Analysis


statEnv |- DecimalLiteral : xs:decimal

Dynamic Evaluation


dynEnv |- DecimalLiteral => xs:decimal(DecimalLiteral)

Static Type Analysis


statEnv |- DoubleLiteral : xs:double

Dynamic Evaluation


dynEnv |- DoubleLiteral => xs:double(DoubleLiteral)

Static Type Analysis


statEnv |- StringLiteral : xs:string

Dynamic Evaluation


dynEnv |- StringLiteral => xs:string(StringLiteral)

Dynamic Errors

Literal expressions never raise a dynamic error.

4.1.2 Variable References

Introduction

A variable evaluates to the value to which the variable's QName is bound in the dynamic context.

Variable References
[86 (XQuery)]    VarRef    ::=    "$" VarName
[144 (XQuery)]    VarName    ::=    QName

Core Grammar

The Core grammar productions for variable references are:

Primary Expressions
[65 (Core)]    VarRef    ::=    "$" VarName
[107 (Core)]    VarName    ::=    QName

Normalization

A variable is a Core expression, therefore no normalization rule is required for a variable.

Static Type Analysis

In the static semantics, the type of a variable is simply its type in the static type environment statEnv.varType:

statEnv |- VarName of var expands to expanded-QName      statEnv.varType(expanded-QName) = Type

statEnv |- $ VarName : Type

If the variable is not bound in the static environment, a static error is raised.

Dynamic Evaluation

In the dynamic semantics, a locally declared variable is evaluated by "looking up" its value in dynEnv.varValue:

dynEnv |- VarName of var expands to expanded-QName      dynEnv.varValue(expanded-QName) = Value

dynEnv |- $ VarName => Value

In the dynamic semantics, an imported variable is evaluated in the dynamic context of the module in which it is declared:

dynEnv |- VarName of var expands to expanded-QName      dynEnv.varValue(expanded-QName) = #IMPORTED(URI)
URI =>module_dynEnv dynEnv1      dynEnv1 |- $ VarName => Value

dynEnv |- $ VarName => Value

Dynamic Errors

If the variable is not bound in the dynamic environment, a dynamic error is raised; the default rules in [3.3 Error Handling] cover this error.

4.1.3 Parenthesized Expressions

[87 (XQuery)]    ParenthesizedExpr    ::=    "(" Expr? ")"

Core Grammar

The Core grammar production for parenthesized expressions is:

[66 (Core)]    ParenthesizedExpr    ::=    "(" Expr? ")"

The empty-sequence expression () always has type empty. It is a static error for any expression other than () to have the empty type (see [4 Expressions].)

Static Type Analysis


statEnv |- () : empty

statEnv |- Expr : Type

statEnv |- ( Expr ) : Type

Dynamic Evaluation

The empty-sequence expression evaluates to the empty sequence.


dynEnv |- () => ()

dynEnv |- Expr => Value

dynEnv |- ( Expr ) => Value

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to parenthesized expressions.

4.1.4 Context Item Expression

[88 (XQuery)]    ContextItemExpr    ::=    "."

Introduction

A context item expression evaluates to the context item, which may be either a node or an atomic value.

Normalization

A context item expression is normalized to the built-in variable $fs:dot.

 
[.]Expr
==
$fs:dot

4.1.5 Function Calls

Introduction

A function call consists of a QName followed by a parenthesized list of zero or more expressions. In [XPath/XQuery], the actual argument to a function is called an argument and the formal argument of a function is called a parameter. We use the same terminology here.

Function Calls
[91 (XQuery)]    FunctionCall    ::=    QName "(" (ExprSingle ("," ExprSingle)*)? ")"

Because [XPath/XQuery] implicitly converts the values of function arguments, a normalization step is required.

Notation

Normalization of function calls uses an auxiliary mapping []FunctionArgument(SequenceType) used to insert conversions of function arguments that depend only on the expected SequenceType of the corresponding parameters. It is defined as follows:

 
[Expr]FunctionArgument(SequenceType)
==
[[[Expr]AtomizeAtomic(SequenceType)]Extract(SequenceType)]Convert(SequenceType)

where

  • [Expr]AtomizeAtomic(SequenceType) denotes

    fn:data(Expr)    If SequenceType <: xdt:anyAtomic* and Expr : Type and not(Type=empty)
    Expr    Otherwise

    which specifies that if the function expects atomic parameters, then fn:data is called to obtain them.

  • [Expr]Extract(SequenceType) denotes

    fn:subsequence(Expr,1,1)    If statEnv.xpath1.0_compatibility is true and SequenceType <: item?
    Expr    Otherwise

    which specifies that if the backwards compatibility mode is set, then the first node of the sequence passed as an argument is selected.

  • [Expr]Convert(SequenceType) denotes

    fs:convert-simple-operand(Expr,PrototypicalValue) If SequenceType <: xdt:anyAtomicType*
    Expr Otherwise

    where PrototypicalValue has the following values for each possible SequenceType:

    Editorial note  
    Todo: insert dummy prototypical values for each of the 44+4 types...

Note

The fs:convert-simple-operand function takes a PrototypicalValue, which is a value of the target type, to ensure that conversion to base types is possible even though types are not first class objects in [XPath/XQuery].

Core Grammar

The Core grammar production for function calls is:

Function Calls
[69 (Core)]    FunctionCall    ::=    QName "(" (ExprSingle ("," ExprSingle)*)? ")"

Normalization

Each argument expression in a function call is normalized to its corresponding Core expression by applying []FunctionArgument(SequenceType) for each argument with the expected SequenceType for the argument inserted.

 
[ QName (Expr1, ..., Exprn) ]Expr
==
QName ( [Expr1]FunctionArgument(SequenceType1), ..., [Exprn]FunctionArgument(SequenceTypen)) )

Note that this normalization rule depends on the static environment containing function signatures and is the only normalization rule that depends on statEnv. Furthermore notice that the normalization is only well-defined when it is guaranteed that overloading is restricted to atomic types with the same quantifier. This is presently the case.

Static Type Analysis

To typecheck a Core function call we first check in Section [7 Additional Semantics of Functions] if there is a specialized typing rule for the function, and, if so, use it. Otherwise, the function signatures matching the function name and arity are retrieved from the static environment. The type of each argument to the function must be a subtype of a type that is promotable to the corresponding function parameter type of the function; if the inferred type is a union of atomic types then this check is performed separately for each possibility.

The first rule bootstraps type checking of a function call: It expands the function's QName and then applies the function call rule for the expanded function call:

statEnv |- QName of func expands to expanded-QName
statEnv |- Expr1 : Type1 ... Exprn : Typen
statEnv |- expanded-QName(Type1,...,Typen) : Type

statEnv |- QName (Expr1,...,Exprn) : Type

For a function call in which the static type of one of the expressions passed as argument is a union of atomic types, the function call is type checked once separately for each atomic type in that union. The static type of the entire function call expression is then the union of the types computed in each case, as follows:

Typei = (AtomicType1|...|AtomicTypem)
statEnv |- expanded-QName(Type1,..., AtomicType1,..., Typen) : Type1'
...
statEnv |- expanded-QName(Type1,..., AtomicTypem,..., Typen) : Typem'

statEnv |- expanded-QName(Type1, ..., Typen) : (Type1'|...|Typem')

Note

Notice that this semantics makes sense since the type declared for a function parameter, which uses the sequence types syntax, cannot itself be a union.

Finally, the following auxilliary rule type checks a function call in which none of the actual arguments has a type that is a union of atomic types. The rule looks up the function in the static environment and checks that some signature for the function satisfies the following constraint: the type of each actual argument is a subtype of some type that can be promoted to the type of the correponding function parameter. In this case, the function call is well typed and the result type is the return type specified in the function's signature.

not(Type1 = (AtomicType1,1|...|AtomicType1,m1)
...
not(Typen = (AtomicTypen,1|...|AtomicTypen,mn)
statEnv.funcType(expanded-QName) = { FuncDecl1, ..., FuncDeclm }
FuncDecli = define function expanded-QName(Type1'', ..., Typen'') as Type''
Type1 <: Type1'     ...     Typen <: Typen'
Type1' can be promoted to Type1''     ...     Typen' can be promoted to Typen''

statEnv |- expanded-QName(Type1, ..., Typen) : Type''

The function body itself is not analyzed for each invocation: static typing of the function definition itself guarantees that the function body always returns a value of the declared return type.

Notice that the static typing rule checks the function signature in order to determine whether a function exists rather than just the function arity: this is consistent because it will reject function calls with the wrong arity in addition to function calls with the right arity but incompatible parameter types.

Dynamic Evaluation

Based on a function's name and parameter types, the function body is retrieved from the dynamic environment.

If the function is a locally-declared, user-defined function then it is evaluated as follows. First, the rule evaluates each actual function argument expression. Next, a match is searched for among the function's possible declaration signatures, retrieved from statEnv.funcType. If the function is not present in the environment, or there is no matching declaration signature, a type error is raised. Otherwise, the function body and formal variables are obtained from dynEnv.funcDefn for the matching declaration signature. The rule then extends dynEnv.varValue by binding each formal variable to its corresponding value (converted by the normalization as required for the expected type and backwards compatibility flag), and evaluates the body of the function in the new environment. The resulting value is the value of the function call.

statEnv |- QName of func expands to expanded-QName
statEnv.funcType(expanded-QName) = { FuncDecl1, ..., FuncDeclm }
FuncDecli = define function expanded-QName(Type1, ..., Typen) as Type
dynEnv |- Expr1 => Value1 ... dynEnv |- Exprn => Valuen
statEnv |- Value1 against Type1 promotes to Value1'
...
statEnv |- Valuen against Typen promotes to Valuen'
dynEnv.funcDefn(expanded-QName(Type1, ..., Typen)) = (Expr, Variable1, ... , Variablen)
dynEnvDefault = ( Variable1 => Value1'; ...; Variablen => Valuen') ] |- Expr => Value
statEnv |- Value against Type promotes to Value'

dynEnv |- QName ( Expr1, ..., Exprn ) => Value'

Note that the function body is evaluated in the default (top-level) environment extended with just the parameter bindings. Note also that input values and output values are matched against the types declared for the function. If static analysis was performed, all these checks are guaranteed to be true and may be omitted.

The rule for evaluating an imported function is similar to that for evaluating a locally declared function, except that the function call is evaluated in the dynamic context of the module in which it is declared.

statEnv |- QName of func expands to expanded-QName
statEnv.funcType(expanded-QName) = { FuncDecl1, ..., FuncDeclm }
FuncDecli = define function expanded-QName(Type1, ..., Typen) as Type
dynEnv |- Expr1 => Value1 ... dynEnv |- Exprn => Valuen
statEnv |- Value1 against Type1 promotes to Value1'
...
statEnv |- Valuen against Typen promotes to Valuen'
dynEnv.funcDefn(expanded-QName(Type1, ..., Typen)) = #IMPORTED(URI)
URI =>module_dynEnv dynEnv1
dynEnv1 |- QName ( Expr1, ..., Exprn ) => Value'

dynEnv |- QName ( Expr1, ..., Exprn ) => Value'

If the function is a built-in or external function then the rule is somewhat simpler:

statEnv |- QName of func expands to expanded-QName
statEnv.funcType(expanded-QName) = { FuncDecl1, ..., FuncDeclm }
FuncDecli = define function expanded-QName(Type1, ..., Typen) as Type
dynEnv |- Expr1 => Value1 ... dynEnv |- Exprn => Valuen
statEnv |- Value1 against Type1 promotes to Value1'
...
statEnv |- Valuen against Typen promotes to Valuen'
dynEnv.funcDefn(expanded-QName(Type1, ..., Typen)) in { #BUILT-IN, #EXTERNAL }
expanded-QName(Value1', ..., Valuen') => Value
statEnv |- Value against Type promotes to Value'

dynEnv |- QName ( Expr1, ..., Exprn ) => Value'

Calls to built-in or external functions use the following auxiliary judgment to evaluate the built-in or external function:

"The built-in or external function F (from [Data Model], [Functions and Operators], [7 Additional Semantics of Functions], or as defined in dynEnvDefault.funcDefn) applied to the given parameter values yields the specified result value"

F(Value1, ..., Valuen) => Value

Dynamic Errors

If the evaluation of any actual argument raises an error, the function call can raise an error. This rule applies to both user-defined and built-in functions. Note that if more than one expression may raise an error, the function call may raise any one of the errors.

statEnv |- QName of func expands to expanded-QName
statEnv.funcType(expanded-QName) = { FuncDecl1, ..., FuncDeclm }
FuncDecli = define function expanded-QName(Type1, ..., Typen) as Type
dynEnv |- Expri raises Error      1 <= i <= n

dynEnv |- QName ( Expr1, ..., Exprn ) raises Error

If, for all possible function signatures, the evaluation of some actual argument yields a value that cannot be promoted to the corresponding formal type of the parameter, the function call raises a type error. This rule applies to both user-defined and built-in functions.

statEnv |- QName of func expands to expanded-QName
statEnv.funcType(expanded-QName) = { FuncDecl1, ..., FuncDeclm }
FuncDeclj = define function expanded-QName(Type1, ..., Typen) as Type      for all 1 <= j <= m
dynEnv |- Expri => Valuei
statEnv |- not (Valuei against Typei promotes to Valuei')      1 <= i <= n

dynEnv |- QName ( Expr1, ..., Exprn ) raises typeError

If the evaluation of the function call to a user-defined function yields a value that cannot be promoted to the corresponding return type of the function, the function call raises a type error.

statEnv |- QName of func expands to expanded-QName
statEnv.funcType(expanded-QName) = { FuncDecl1, ..., FuncDeclm }
FuncDecli = define function expanded-QName(Type1, ..., Typen) as Type
dynEnv |- Expr1 => Value1 ... dynEnv |- Exprn => Valuen
statEnv |- Value1 against Type1 promotes to Value1'
...
statEnv |- Valuen against Typen promotes to Valuen'
dynEnv.funcDefn(expanded-QName(Type1, ..., Typen)) = (Expr, Variable1, ... , Variablen)
dynEnv [ varValue = ( Variable1 => Value1'; ...; Variablen => Valuen') ] |- Expr => Value
statEnv |- not (Value against Type promotes to Value')

dynEnv |- QName ( Expr1, ..., Exprn ) raises typeError

If the evaluation of the function call to a built-in or external function yields a value that cannot be promoted to the corresponding return type of the function, the built-in or external function call raises a type error.

statEnv |- QName of func expands to expanded-QName
statEnv.funcType(expanded-QName) = { FuncDecl1, ..., FuncDeclm }
FuncDeclj = define function expanded-QName(Type1, ..., Typen) as Type
dynEnv |- Expr1 => Value1 ... dynEnv |- Exprn => Valuen
statEnv |- Value1 against Type1 promotes to Value1'
...
statEnv |- Valuen against Typen promotes to Valuen'
dynEnv.funcDefn(expanded-QName(Type1, ..., Typen)) in { #BUILT-IN, #EXTERNAL }
expanded-QName(Value1', ..., Valuen') => Value
statEnv |- not (Value against Type promotes to Value')

dynEnv |- QName ( Expr1, ..., Exprn ) raises typeError

Built-in function calls use the following auxiliary judgment to evaluate the built-in function call. If the built-in function raises an error, the function call raises an error.

"The built-in function F (from data model, type constructor, or functions and operators) applied to the given parameter raises an error"

F(Value1, ..., Valuen) raises Error

4.2 Path Expressions

Introduction

Path expressions are used to locate nodes within a tree. There are two kinds of path expressions, absolute path expressions and relative path expressions. An absolute path expression is a rooted relative path expression. A relative path expression is composed of a sequence of steps.

Path Expressions
[67 (XQuery)]    PathExpr    ::=    ("/" RelativePathExpr?)
| ("//" RelativePathExpr)
| RelativePathExpr
[68 (XQuery)]    RelativePathExpr    ::=    StepExpr (("/" | "//") StepExpr)*

Core Grammar

PathExpr and RelativePathExpr are fully normalized, therefore they have no corresponding productions in the Core. The grammar for path expressions in the Core starts with the StepExpr production.

Normalization

Absolute path expressions are path expressions starting with the / or // symbols, indicating that the expression must be applied on the root node in the current context. The root node in the current context is the greatest ancestor of the context node. The following two rules normalize absolute path expressions to relative ones. They use the fn:root function, which returns the greatest ancestor of its argument node. The treat expressions guarantee that the value bound to the context variable $fs:dot is a document node.

 
["/"]Expr
==
(fn:root(self::node()) treat as document-node())
 
["/" RelativePathExpr]Expr
==
[((fn:root(self::node())) treat as document-node()) "/" RelativePathExpr]Expr
 
["//" RelativePathExpr]Expr
==
[((fn:root(self::node())) treat as document-node) "/" descendant-or-self::node() "/" RelativePathExpr]Expr
 
[ StepExpr1 // StepExpr2 ]Expr
==
[StepExpr1 / descendant-or-self::node() / StepExpr2]Expr

A composite relative path expression (using /) is normalized into a for expression by concatenating the 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 actualy return atomic values.

 
[StepExpr1 "/" StepExpr2]Expr
==
fs:apply-ordering-mode (
fs:distinct-doc-order-or-atomic-sequence (
  let $fs:sequence as node()* := [StepExpr1]Expr return
  let $fs:last := fn:count($fs:sequence) return
  for $fs:dot at $fs:position in $fs:sequence return
    [StepExpr2]Expr
))

4.2.1 Steps

Note that for this section uses some auxiliary judgments which are defined in [8.2 Judgments for step expressions and filtering].

Introduction

Steps
[69 (XQuery)]    StepExpr    ::=    AxisStep | FilterExpr
[70 (XQuery)]    AxisStep    ::=    (ForwardStep | ReverseStep) PredicateList
[71 (XQuery)]    ForwardStep    ::=    (ForwardAxis NodeTest) | AbbrevForwardStep
[74 (XQuery)]    ReverseStep    ::=    (ReverseAxis NodeTest) | AbbrevReverseStep
[81 (XQuery)]    PredicateList    ::=    Predicate*

Core Grammar

The Core grammar productions for XPath steps are:

Steps
[53 (Core)]    StepExpr    ::=    AxisStep | PrimaryExpr
[54 (Core)]    AxisStep    ::=    ForwardStep | ReverseStep
[55 (Core)]    ForwardStep    ::=    ForwardAxis NodeTest
[57 (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 [4.2.1.1 Axes].

Normalization

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 "[" Numeric "]"]Expr
==
let $fs:sequence := fs:apply-ordering-mode(fs:distinct-doc-order( [ForwardStep PredicateList]Expr )) return
fn:subsequence($fs:sequence,Numeric,1)
 
[ForwardStep PredicateList "[" fn:last() "]"]Expr
==
let $fs:sequence := fs:apply-ordering-mode(fs:distinct-doc-order( [ForwardStep PredicateList]Expr )) return
let $fs:last := fn:count($fs:sequence) return
fn:subsequence($fs:sequence,$fs:last,1)

When predicates are applied on a reverse step, the position variable is bound in reverse document order.

 
[ReverseStep PredicateList "[" Numeric "]"]Expr
==
let $fs:sequence := fs:apply-ordering-mode(fs:distinct-doc-order( [ReverseStep PredicateList]Expr )) return
let $fs:last := fn:count($fs:sequence) return
let $fs:position := $fs:last - Numeric + 1 return
   then fn:subsequence($fs:sequence,$fs:position,1)

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
==
let $fs:sequence := fs:apply-ordering-mode(fs:distinct-doc-order( [ReverseStep PredicateList]Expr )) return
   then fn:subsequence($fs:sequence,1,1)

The normalization rules above all use the function fn:subsequence to select a particular item. The static typing rules for this function are defined in [7.2.11 The fn:subsequence 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
==
let $fs:sequence := fs:apply-ordering-mode(fs:distinct-doc-order( [ForwardStep PredicateList]Expr )) return
let $fs:last := fn:count($fs:sequence) return
for $fs:dot at $fs:position in $fs:sequence return
   if [Expr]Predicates then $fs:dot else ()

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
==
let $fs:sequence := fs:apply-ordering-mode(fs:distinct-doc-order( [ReverseStep PredicateList]Expr )) return
let $fs:last := fn:count($fs:sequence) return
for $fs:dot at $fs:new in $fs:sequence return
let $fs:position := $fs:last - $fs:new + 1 return
  if [Expr]Predicates then $fs:dot else ()

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)

Static Type Analysis

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.varType($fs:dot) = Type1
Type1 <: node
statEnv |- axis Axis of Type1 : Type2
Axis principal PrincipalNodeKind
statEnv |- test NodeTest with PrincipalNodeKind of Type2 : Type3

statEnv |- Axis NodeTest : Type3

Note

Note that the second judgment in the inference rule requires that the context item be a node, guaranteeing that a type error is raised when the context item is an atomic value.

Dynamic Evaluation

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 the filter judgment as follows.

dynEnv.varValue($fs:dot) = Value1
Value1 matches node
dynEnv |- axis Axis of Value1 => Value2
Axis principal PrincipalNodeKind
dynEnv |- test NodeTest with PrincipalNodeKind of Value2 => Value3

dynEnv |- Axis NodeTest => fs:distinct-doc-order(Value3)

Note

Note that the second judgment in the inference rule guarantees that the context item is bound to a node.

Dynamic Errors

If the context item is not a node, the evaluation of an axis node test expression raises a dynamic error.

dynEnv.varValue($fs:dot) = AtomicValue

dynEnv.varValue |- Axis NodeTest raises typeError

4.2.1.1 Axes

Introduction

Axes
[72 (XQuery)]    ForwardAxis    ::=    ("child" "::")
| ("descendant" "::")
| ("attribute" "::")
| ("self" "::")
| ("descendant-or-self" "::")
| ("following-sibling" "::")
| ("following" "::")
[75 (XQuery)]    ReverseAxis    ::=    ("parent" "::")
| ("ancestor" "::")
| ("preceding-sibling" "::")
| ("preceding" "::")
| ("ancestor-or-self" "::")

Core Grammar

The Core grammar productions for XPath axis are:

Axes
[56 (Core)]    ForwardAxis    ::=    ("child" "::")
| ("descendant" "::")
| ("attribute" "::")
| ("self" "::")
| ("descendant-or-self" "::")
| ("following-sibling" "::")
| ("following" "::")
| ("namespace" "::")
[58 (Core)]    ReverseAxis    ::=    ("parent" "::")
| ("ancestor" "::")
| ("preceding-sibling" "::")
| ("preceding" "::")
| ("ancestor-or-self" "::")

Notation

Normalization of axis uses the following auxiliary mapping rule: []Axis.

Normalization

Normalization for all axis 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
==
[let $e := . in parent::node()/child:: NodeTest [.>>$e]]Expr
 
[following:: NodeTest]Axis
==
[ancestor-or-self::node()/following-sibling::node()/descendant-or-self::NodeTest]Expr

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 := . in 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:

 
[parent:: NodeTest]Axis
==
parent:: NodeTest
 
[ancestor:: NodeTest]Axis
==
ancestor:: NodeTest
 
[ancestor-or-self:: NodeTest]Axis
==
ancestor-or-self:: NodeTest
4.2.1.2 Node Tests

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.

Node Tests
[77 (XQuery)]    NodeTest    ::=    KindTest | NameTest
[78 (XQuery)]    NameTest    ::=    QName | Wildcard
[79 (XQuery)]    Wildcard    ::=    "*"
| (NCName ":" "*")
| ("*" ":" NCName)

Core Grammar

The Core grammar productions for node tests are:

Node Tests
[59 (Core)]    NodeTest    ::=    KindTest | NameTest
[60 (Core)]    NameTest    ::=    QName | Wildcard
[61 (Core)]    Wildcard    ::=    "*"
| (NCName ":" "*")
| ("*" ":" NCName)

4.2.2 Predicates

Introduction

A predicate consists of an expression, called a predicate expression, enclosed in square brackets.

[82 (XQuery)]    Predicate    ::=    "[" Expr "]"

Notation

Normalization of predicates uses the following auxiliary mapping rule: []Predicates.

Normalization

Predicates in path expressions are normalized with a special mapping rule:

 
[Expr]Predicates
==
typeswitch (Expr)
  case $v as fs:numeric return op:numeric-equal($v, $fs:position)
  default $v return fn:boolean($v)

Note that the semantics of predicates whose parameter is a numeric value also works for other numeric than integer values, in which case the op:numeric-equal returns false when compared to a position. For example the expression //a[3.4] is allowed and always returns the empty sequence)

4.2.3 Unabbreviated Syntax

The corresponding Section in the [XPath/XQuery] document just contains examples.

4.2.4 Abbreviated Syntax

Abbreviated Syntax
[73 (XQuery)]    AbbrevForwardStep    ::=    "@"? NodeTest
[76 (XQuery)]    AbbrevReverseStep    ::=    ".."

Normalization

Here are normalization rules for the abbreviated syntax.

 
[ .. ]Expr
==
[parent::node()]Axis
 
[ @ NameTest ]Expr
==
attribute :: NameTest
 
[ NodeTest ]Expr
==
[child :: NodeTest]Axis

4.3 Sequence Expressions

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.

4.3.1 Constructing Sequences

Constructing Sequences
[31 (XQuery)]    Expr    ::=    ExprSingle ("," ExprSingle)*
[49 (XQuery)]    RangeExpr    ::=    AdditiveExpr ( "to" AdditiveExpr )?

Core Grammar

The Core grammar production for sequence expressions is:

Core Sequence Expressions
[30 (Core)]    Expr    ::=    ExprSingle ("," ExprSingle)*

Normalization

A sequence expression is normalized into a sequence of normalized single expressions:

 
[Expr1 , Expr2]Expr
==
[Expr1]Expr, [Expr2]Expr

Static Type Analysis

The type of the sequence expression is the sequence over the types of the individual expressions.

statEnv |- Expr1 : Type1      statEnv |- Expr2 : Type2

statEnv |- Expr1 , Expr2 : Type1, Type2

Dynamic Evaluation

Each expression in the sequence is evaluated and the resulting values are concatenated into one sequence.

dynEnv |- Expr1 => Value1     dynEnv |- Expr2 => Value2

dynEnv |- Expr1, Expr2 => Value1, Value2

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to sequence expressions.

Normalization

The range operator is normalized to the fs:to function.

 
[Expr1 to Expr2]Expr
==
fs:to ([Expr1]Expr,[Expr2]Expr)

Static Type Analysis

The static semantics of the fs:to function is defined in [Functions and Operators].

Dynamic Evaluation

The dynamic semantics of the op:to operator is defined in [Functions and Operators].

Dynamic Errors

The error semantics of the op:to operator is defined in [Functions and Operators].

4.3.2 Filter Expressions

Introduction

Filter Expression
[80 (XQuery)]    FilterExpr    ::=    PrimaryExpr PredicateList

Core Grammar

There are no Core grammar productions for filter expressions as they are normalized to other Core expressions.

Normalization

When predicates are applied on a primary expression, the input sequence is processed in sequence order and the context is bound as in the case of forward axes. In that case, the sequence can contain both nodes and atomic values.

 
[PrimaryExpr PredicateList "[" Numeric "]"]Expr
==
let $fs:sequence := [PrimaryExpr PredicateList]Expr return
fn:subsequence($fs:sequence,Numeric,1)

When predicates are applied on a primary expression, the input sequence is processed in sequence order and the context variable is bound to each item in the input sequence, which may contain both nodes and atomic values.

 
[PrimaryExpr PredicateList "[" Expr "]"]Expr
==
let $fs:sequence := [PrimaryExpr PredicateList]Expr return
let $fs:last := fn:count($fs:sequence) return
for $fs:dot at $fs:position in $fs:sequence return
   if [Expr]Predicates then $fs:dot else ()

Static Type Analysis

There are no additional static type rules for filter expressions.

Dynamic Evaluation

There are no additional dynamic evaluation rules for filter expressions.

Dynamic Errors

There are no additional error semantics rules for filter expressions.

4.3.3 Combining Node Sequences

[XPath/XQuery] provides several operators for combining sequences of nodes.

Combining Sequences
[52 (XQuery)]    UnionExpr    ::=    IntersectExceptExpr ( ("union" | "|") IntersectExceptExpr )*
[53 (XQuery)]    IntersectExceptExpr    ::=    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 tables:

SequenceOp [SequenceOp]SequenceOp
"union" op:union
"|" op:union
"intersect" op:intersect
"except" op:except

Normalization

 
[Expr1 SequenceOp Expr2]Expr
==
fs:apply-ordering-mode ([SequenceOp]SequenceOp ( [Expr1]Expr, [Expr2]Expr ))

Static Type Analysis

The static semantics of the functions that operate on sequences are defined in [7 Additional Semantics of Functions].

Dynamic Evaluation

The dynamic semantics for function calls is given in [4.1.5 Function Calls].

Dynamic Errors

The error semantics for function calls is given in [4.1.5 Function Calls].

4.4 Arithmetic Expressions

[XPath/XQuery] provides arithmetic operators for addition, subtraction, multiplication, division, and modulus, in their usual binary and unary forms.

Arithmetic Expressions
[50 (XQuery)]    AdditiveExpr    ::=    MultiplicativeExpr ( ("+" | "-") MultiplicativeExpr )*
[51 (XQuery)]    MultiplicativeExpr    ::=    UnionExpr ( ("*" | "div" | "idiv" | "mod") UnionExpr )*
[58 (XQuery)]    UnaryExpr    ::=    ("-" | "+")* ValueExpr
[59 (XQuery)]    ValueExpr    ::=    ValidateExpr | PathExpr | ExtensionExpr

Core Grammar

The core grammar production for arithmetics expressions is:

[48 (Core)]    ValueExpr    ::=    ValidateExpr | StepExpr | ExtensionExpr

Notation

The mapping functions []ArithOp and UnaryArithOp are defined by the following tables:

ArithOp [ArithOp]ArithOp
"+" fs:plus
"-" fs:minus
"*" fs:times
"div" fs:div
"mod" fs:mod
UnaryArithOp [UnaryArithOp]UnaryArithOp
"+" fs:unary-plus
"-" fs:unary-minus

Core Grammar

There are no Core grammar productions for value comparisons as they are normalized to other Core expressions.

Normalization

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 xdt: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 monomorphic function is given in [B.2 Mapping of Overloaded Internal Functions].

 
[Expr1 ArithOp Expr2]Expr
==
[ArithOp]ArithOp ( fs:convert-operand(fn:data([Expr1]Expr), 1.0E0),
fs:convert-operand(fn:data([Expr2]Expr), 1.0E0))

The normalization rules for the idiv operator are similar, but instead of casting arguments with type xdt:untypedAtomic to xs:double, they are cast to xs:integer.

 
[Expr1 idiv Expr2]Expr
==
fs:idiv ( fs:convert-operand(fn:data([Expr1]Expr), 1),
fs:convert-operand(fn:data([Expr2]Expr), 1))

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(0, fs:convert-operand(fn:data([Expr]Expr), 1.0E0))

Static Type Analysis

The static semantics for function calls is given in [4.1.5 Function Calls].

Dynamic Evaluation

The dynamic semantics for function calls is given in [4.1.5 Function Calls].

Dynamic Errors

The error semantics for function calls is given in [4.1.5 Function Calls].

4.5 Comparison Expressions

Introduction

Comparison expressions allow two values to be compared. [XPath/XQuery] provides four kinds of comparison expressions, called value comparisons, general comparisons, node comparisons, and order comparisons.

Comparison Expressions
[48 (XQuery)]    ComparisonExpr    ::=    RangeExpr ( (ValueComp
| GeneralComp
| NodeComp) RangeExpr )?
[61 (XQuery)]    ValueComp    ::=    "eq" | "ne" | "lt" | "le" | "gt" | "ge"
[60 (XQuery)]    GeneralComp    ::=    "=" | "!=" | "<" | "<=" | ">" | ">="
[62 (XQuery)]    NodeComp    ::=    "is" | "<<" | ">>"

4.5.1 Value Comparisons

Notation

The mapping function []ValueOp is defined by the following table:

ValueOp [ValueOp]ValueOp
"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.

Normalization

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.3 The fs:convert-operand function]. If the first argument to this function has type xdt: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 monomorphic function is given in [B.2 Mapping of Overloaded Internal Functions].

 
[Expr1 ValueOp Expr2]Expr
==
[ValueOp]ValueOp ( fs:convert-operand(fn:data([Expr1]Expr), "string"),
fs:convert-operand(fn:data([Expr2]Expr), "string") )

Static Type Analysis

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 [Functions and Operators].

Dynamic Evaluation

The dynamic semantics for function calls is given in [4.1.5 Function Calls].

Dynamic Errors

The error semantics rules for function calls is given in [4.1.5 Function Calls].

4.5.2 General Comparisons

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

For convenience, GeneralOp denotes the operators "=", "!=", "<", "<=", ">", or ">=".

The function []GeneralOp is defined by the following table:

GeneralOp [GeneralOp]GeneralOp
"=" 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.

Normalization

The normalization rule for a general comparison expression first atomizes each argument by applying fn:data and then applies the existentially quantified some expression to each sequence. The internal function fs:convert-operand is applied to each pair of atomic values. If the first argument to this function has type xdt:untypedAtomic, then the first argument is cast to type of the second argument. If the second argument has type xdt:untypedAtomic, the first argument is cast to a string. The overloaded internal function corresponding to the general comparison operator is then applied to the two converted values.

 
[Expr1 GeneralOp Expr2]Expr
==
some $v1 in fn:data([Expr1]Expr) satisfies
some $v2 in fn:data([Expr2]Expr) satisfies
let $u1 := fs:convert-operand($v1, $v2) return
let $u2 := fs:convert-operand($v2, $v1) return
[GeneralOp]GeneralOp ($u1, $u2)

4.5.3 Node Comparisons

Core Grammar

There are no Core grammar productions for node comparisons as they are normalized to other Core expressions.

Normalization

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 [B.2 Mapping of Overloaded Internal Functions].

 
[Expr1 is Expr2]Expr
==
   fs:is-same-node([Expr1]Expr, [Expr2]Expr)
 
[Expr1 << Expr2]Expr
==
fs:node-before([Expr1]Expr, [Expr2]Expr)
 
[Expr1 >> Expr2]Expr
==
fs:node-after([Expr1]Expr, [Expr2]Expr)

Static Type Analysis

The static semantics for the internal functions are defined in [B.2 Mapping of Overloaded Internal Functions].

Dynamic Evaluation

The dynamic semantics for internal function is defined in [B.2 Mapping of Overloaded Internal Functions].

Dynamic Errors

The error semantics rules for function calls is given in [4.1.5 Function Calls].

4.6 Logical Expressions

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.

Logical Expressions
[46 (XQuery)]    OrExpr    ::=    AndExpr ( "or" AndExpr )*
[47 (XQuery)]    AndExpr    ::=    ComparisonExpr ( "and" ComparisonExpr )*

Core Grammar

The Core grammar productions for logical expressions are:

Core Logical Expressions
[44 (Core)]    OrExpr    ::=    AndExpr ( "or" AndExpr )*
[45 (Core)]    AndExpr    ::=    CastableExpr ( "and" CastableExpr )*

Normalization

The normalization rules for "and" and "or" first get the effective boolean value of each argument, then apply the appropriate Core operator.

 
[Expr1 and Expr2]Expr
==
fn:boolean([Expr1]Expr) and fn:boolean([Expr2]Expr)
 
[Expr1 or Expr2]Expr
==
fn:boolean([Expr1]Expr) or fn:boolean([Expr2]Expr)

Static Type Analysis

The logical expressions require that each subexpression have type xs:boolean. The result type is also xs:boolean.

statEnv |- Expr1 : xs:boolean      statEnv |- Exprn : xs:boolean

statEnv |- Expr1 and Expr2 : xs:boolean

statEnv |- Expr1 : xs:boolean      statEnv |- Exprn : xs:boolean

statEnv |- Expr1 or Expr2 : xs:boolean

Dynamic Evaluation

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.

dynEnv |- Expri => false      1 <= i <= 2

dynEnv |- Expr1 and Expr2 => false

dynEnv |- Expr1 => true      dynEnv |- Expr2 => true

dynEnv |- Expr1 and Expr2 => true

dynEnv |- Expri => true      1 <= i <= 2

dynEnv |- Expr1 or Expr2 => true

dynEnv |- Expr1 => false      dynEnv |- Expr2 => false

dynEnv |- Expr1 or Expr2 => false

Dynamic Errors

dynEnv |- Expri raises Error      1 <= i <= 2

dynEnv |- Expr1 and Expr2 raises Error

dynEnv |- Expri raises Error      1 <= i <= 2

dynEnv |- Expr1 or Expr2 raises Error

4.7 Constructors

[XPath/XQuery] supports two forms of constructors: a direct constructor, which supports literal XML syntax for elements, attributes, and text nodes, and a computed constructor, which can be used to construct element and attribute nodes, possibly with computed names, and also document and text nodes. All direct constructors are normalized into computed constructors, i.e., there are no direct-constructor expressions in the Core.

4.7.1 Direct Element Constructors

Introduction

The static and dynamic semantics of the direct forms of element and attribute constructors are specified on the equivalent computed element and attribute constructors.

Constructors
[92 (XQuery)]    Constructor    ::=    DirectConstructor
| ComputedConstructor
[93 (XQuery)]    DirectConstructor    ::=    DirElemConstructor
| DirCommentConstructor
| DirPIConstructor
[94 (XQuery)]    DirElemConstructor    ::=    "<" QName DirAttributeList ("/>" | (">" DirElemContent* "</" QName S? ">"))
[99 (XQuery)]    DirElemContent    ::=    DirectConstructor
| ElementContentChar
| CDataSection
| CommonContent
[151 (XQuery)]    ElementContentChar    ::=    Char - [{}<&]
[100 (XQuery)]    CommonContent    ::=    PredefinedEntityRef | CharRef | "{{" | "}}" | EnclosedExpr
[105 (XQuery)]    CDataSection    ::=    "<![CDATA[" CDataSectionContents "]]>"
[106 (XQuery)]    CDataSectionContents    ::=    (Char* - (Char* ']]>' Char*))
[95 (XQuery)]    DirAttributeList    ::=    (S (QName S? "=" S? DirAttributeValue)?)*
[96 (XQuery)]    DirAttributeValue    ::=    ('"' (EscapeQuot | QuotAttrValueContent)* '"')
| ("'" (EscapeApos | AposAttrValueContent)* "'")
[97 (XQuery)]    QuotAttrValueContent    ::=    QuotAttrContentChar
| CommonContent
[98 (XQuery)]    AposAttrValueContent    ::=    AposAttrContentChar
| CommonContent
[152 (XQuery)]    QuotAttrContentChar    ::=    Char - ["{}<&]
[153 (XQuery)]    AposAttrContentChar    ::=    Char - ['{}<&]
[149 (XQuery)]    EscapeQuot    ::=    '""'
[150 (XQuery)]    EscapeApos    ::=    "''"
[29 (XQuery)]    EnclosedExpr    ::=    "{" Expr "}"

Notation

The auxiliary mapping rules []ElementContent, and []ElementContent-unit are defined in this section and are used for the normalization of the content of direct element constructors.

Core Grammar

The Core grammar productions for constructors are:

Constructors
[70 (Core)]    ComputedConstructor    ::=    CompDocConstructor
| CompElemConstructor
| CompAttrConstructor
| CompTextConstructor
| CompCommentConstructor
| CompPIConstructor
[28 (Core)]    EnclosedExpr    ::=    "{" Expr "}"

There are no Core grammar productions for direct XML element or attribute constructors as they are normalized to computed constructors.

Normalization

We start with the rules for normalizing a direct element constructor's content. Literal XML character data (CDATA) is assumed to be processed directly at parsing level so it does not require any formal treatment. We distinguish between direct element constructors that contain only one element-content unit and those that contain more than one element-content unit. An element-content unit is a contiguous sequence of literal characters (character references, escaped braces, and predefined entity references), one enclosed expression, one direct element constructor, one XML comment, or one XML processing instruction. Here are three direct element constructors that each contain one element-content unit:

<date>{ xsd:date("2003-03-18") }</date>

<name>Dizzy Gillespe</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.

The next example contains six element-content units:

<address>
  <!-- Dizzy's address -->
  { 123 }-0A <street>Roosevelt Ave.</street> Flushing, NY { 11368 }
</address>

It contains one XML comment, followed by one enclosed expression that contains the integer 123, one contiguous sequence of characters ("-0A "), one direct XML element constructor, one contiguous sequence of characters (" Flushing, NY"), and one enclosed expression that contains the integer 11368. Evaluating this expression yields this element value:

<address>
  <!-- Dizzy's address -->
  123-0A <street>Roosevelt Ave.</street> Flushing, NY 11368
</address>

Adjacent element-content units are convenient because they 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 above, the integer 123 is converted to a string and concatenated with "-0A" and the result is a single text node containing "123-0A".

In general, we do not want to convert all atomic values to text nodes, especially when performing static-type analysis, because we lose useful type information. For example, if we normalize the first example above as follows, we lose the important information that the user constructed a date value, not just a text node containing an arbitrary string:

<date>{ xsd:date("2003-03-18") }</date>
 (normalization that loses type information) == 
element date { text { "2003-03-18" } } 

So to preserve useful type information, we distinguish between direct element constructor's that contain one element-content unit and those that contain more than one (because multiple element-content units commonly denote concatenatation of atomic data and text). Here is the normalization of the first and fourth examples above:

<date>{ xsd:date("2003-03-18") }</date>
 ==
element date { xsd: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
  )
}

Given the distinction between direct element constructors that we made above, we give two normalization rules for a direct element constructor's content. If the direct element constructor contains exactly one element-content unit, we simply normalize that unit by applying the normalization rule for the element content:

 
[ ElementContent1 ]ElementContent-unit
==
[ ElementContent1 ]ElementContent

If the direct element constructor contains more than one element-content unit, we normalize each unit individually and construct a sequence of the normalized results interleaved with empty text nodes. The empty text nodes guarantee that the results of evaluating consecutive element-content units can be distinguished. Then we apply the function fs:item-sequence-to-node-sequence. Section 3.7.1 Direct Element ConstructorsXQ specifies the rules for converting a sequence of atomic values and nodes into a sequence of nodes before element construction. The Formal Semantics function fs:item-sequence-to-node-sequence implements these conversion rules.

 
[ElementContent1 ..., ElementContentn]ElementContent-unit, n > 1
==
fs:item-sequence-to-node-sequence([ ElementContent1 ]ElementContent , text { "" }, ..., text { "" }, [ ElementContentn]ElementContent)

We need to distinguish between multiple element-content units, because the rule for converting sequences of atomic values into strings apply to sequences within distinct enclosed expressions. The empty text nodes are eliminated during evaluation of fs:item-sequence-to-node-sequence when consecutive text nodes are coalesced into a single text node. The text node guarantees that a whitespace character will not be inserted between atomic values computed by distinct enclosed expressions. For example, here is an expression, its normalization, and the resulting XML value:

<example>{ 1 }{ 2 }</example>
 ==
element example { fs:item-sequence-to-node-sequence ((1, text {""}, 2)) }
 ==>
<example>12</example>

In the absence of the empty text node, the expression would evaluate to the following incorrect value:

<example>{ 1 }{ 2 }</example>
 (incorrect normalization) ==
element example { fs:item-sequence-to-node-sequence ((1, 2)) }
 (incorrect value) ==>
<example>1 2</example>

Now that we have explained the normalization rules for direct element content, we give 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 AttributeList > ElementContent* </ QName S? > ]Expr
==
element [QName]Expr{ [ AttributeList ]NamespaceAttrs , [ AttributeList ]Attribute , [ ElementContent* ]ElementContent }
 
[ < QName AttributeList /> ]Expr
==
element [QName]Expr { [ AttributeList ]NamespaceAttrs , [ AttributeList ]Attribute }

Next, we give the normalization rules for each element-content unit. The normalization rule for a contiguous sequence of characters assumes:

  1. that the significant whitespace characters in element constructors have been preserved, as described in [4.7.1.4 Whitespace in Element Content];

  2. that character references have been resolved to individual characters and predefined entity references have been resolved to sequences of characters, and

  3. that the rule is applied to the longest contiguous sequence of characters.

The following normalization rule takes the longest consecutive sequence of individual characters that include literal characters, escaped curly braces, character references, and predefined entity references and normalizes the character sequence as a text node containing the string of characters..

 
[(Char | "{{" | "}}" | CharRef | PredefinedEntityRef)+]ElementContent
==
text { fn:codepoints-to-string((Char | "{{" | "}}" | CharRef | PredefinedEntityRef)+) }

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]ElementContent
==
[DirPIConstructor]Expr
 
[DirCommentConstructor]ElementContent
==
[DirCommentConstructor]Expr

An enclosed expression in element content is normalized by normalizing each individual expression in its expression sequence and then constructing a sequence of the normalized values:

 
[ { Expr1, ..., Exprn } ]ElementContent
==
[ Expr1 ]Expr , ..., [ Exprn]Expr

Static Type Analysis

There are no additional static type rules for direct XML element or attribute constructors.

Dynamic Evaluation

There are no additional dynamic evaluation rules for direct XML element or attribute constructors.

Dynamic Errors

There are no additional error semantics rules for direct XML element or attribute constructors.

4.7.1.1 Attributes

Like literal XML element constructors, literal XML attribute constructors are normalized to computed attribute constructors.

Notation

The auxiliary mapping rules []Attribute, []AttributeContent, and []AttributeContent-unit, are defined in this section and are used for the normalization of the content of direct attribute constructors.

Normalization

Direct attributes may contain namespace-declaration attributes. The normalization rules for attributes ignore namespace-declaration attributes -- they are handled by the normalization rules in [4.7.1.2 Namespace Declaration Attributes].

An AttributeList 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.

 
[
QName1 S? = S? '"' AttributeValue0 '"'
QNamen S? = S? '""' AttributeValuen '"'
]Attribute
==
([QName1 S? = S? '"' AttributeValue0 '"']Attribute
...,
[QNamen S? = S? '"' AttributeValuen '"']Attribute)

Namespace-declaration attributes, i.e., those attributes whose prefix is xmlns are ignored by mapping them to the empty sequence.

 
[Prefix:LocalPart S? = S? '"' AttributeValue '"']Attribute
(Prefix = xmlns)
==
()

All attributes that are not namespace-declaration attributes are mapped to computed attribute constructors.

 
[Prefix:LocalPart S? = S? '"' AttributeValue '"']Attribute
not(Prefix = xmlns)
==
attribute [Prefix:LocalPart ]Expr { [AttributeValue]AttributeContent}

As with literal XML elements, we need to distinguish between direct attribute constructors that contain one attribute-content unit and those that contain multiple attribute-content units, because the rule for converting sequences of atomic values into strings are applied to sequences within distinct enclosed expressions. If the direct attribute constructor contains exactly one attribute-content unit, we simply normalize that unit by applying the normalization rule for the attribute content:

 
[ AttributeValueContent1 ]AttributeContent-unit
==
[AttributeValueContent1]AttributeContent

If the direct attribute constructor contains more than one attribute-content unit, we normalize each unit individually and construct a sequence of the normalized results interleaved with empty text nodes. The empty text nodes guarantee that the results of evaluating consecutive attribute-content units can be distinguished. Then we apply the function fs:item-sequence-to-untypedAtomic, which applies the appropriate conversion rules to the normalized attribute content:

 
[ AttributeValueContent1 ..., AttributeValueContentn ]AttributeContent-unit, n > 1
==
fs:item-sequence-to-untypedAtomic([ AttributeValueContent1 ]AttributeContent , text { "" }, ..., text {""}, [ AttributeValueContentn]AttributeContent)

Literal characters, escaped curly braces, character references, and predefined entity references in attribute content are treated as in element content. In addition, the normalization rule for characters in attributes assumes:

  1. that an escaped single or double quote is converted to an individual single or double quote.

The following normalization rules take the longest consecutive sequence of individual characters that include literal characters, escaped curly braces, escaped quotes, character references, predefined entity references, and escaped single and double quotes and normalizes the character sequence as a string.

 
[( Char | CharRef | EscapeQuot | EscapeApos | PredefinedEntityRef ) +]AttributeContent
==
fn:codepoints-to-string(( Char | CharRef | EscapeQuot | EscapeApos | PredefinedEntityRef )+)

We normalize an enclosed expression in attribute content by normalizing each individual expression in its expression sequence and then construct a sequence of the normalized values:

 
[ { Expr0, ..., Exprn } ]AttributeContent
==
([ Expr0 ]Expr , ..., [ Exprn]Expr)
4.7.1.2 Namespace Declaration Attributes

Notation

The auxiliary mapping rules []NamespaceAttr, and []NamespaceAttrs are defined in this section and are used for the normalization of namespace declaration attributes.

Normalization

Direct attributes may contain namespace-declaration attributes. The normalization rules for namespace-declaration attributes ignore all non-namespace attributes -- they are handled by the normalization rules in [4.7.1.1 Attributes].

An AttributeList 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.

 
[
QName1 S? = S? '"' AttributeValue0 '"'
QNamen S? = S? '""' AttributeValuen '"'
]NamespaceAttrs
==
([QName1 S? = S? '"' AttributeValue0 '"']NamespaceAttr
...,
[QNamen S? = S? '"' AttributeValuen '"']NamespaceAttr)

Attributes whose prefix is not xmlns are ignored by mapping them to the empty sequence.

 
[Prefix:LocalPart S? = S? '"' AttributeValue '"']NamespaceAttr
not (Prefix = xmlns)
==
()

Namespace-declaration attributes are normalized to local namespace declarations (CompElemNamespace).

 
[Prefix:LocalPart S? = S? '"' AttributeValue '"']NamespaceAttr
(Prefix = xmlns)
==
namespace LocalPart { [AttributeValue]AttributeContent}
4.7.1.3 Content

The rules for normalizing element content are given above in [4.7.1 Direct Element Constructors].

4.7.1.4 Whitespace in Element Content

Section 3.7.1.4 Boundary WhitespaceXQ describes how whitespace in element and attribute constructors is processed depending on the value of the xmlspace declaration in the query prolog. the Formal Semantics assumes that the rules for handling whitespace are applied prior to normalization rules, for example, during parsing of a query. Therefore, there are no formal rules for handling whitespace.

4.7.2 Other Direct Constructors

Other Constructors
[103 (XQuery)]    DirPIConstructor    ::=    "<?" PITarget (S DirPIContents)? "?>"
[104 (XQuery)]    DirPIContents    ::=    (Char* - (Char* '?>' Char*))
[101 (XQuery)]    DirCommentConstructor    ::=    "<!--" DirCommentContents "-->"
[102 (XQuery)]    DirCommentContents    ::=    ((Char - '-') | ('-' (Char - '-')))*

Normalization

A literal XML processing instruction is normalized into a computed processing-instruction constructor; its character content is converted to a string as in attribute content.

 
[<? NCName Char* ?>"]Expr
==
processing-instruction NCName { [Char*]AttributeContent }

A literal XML comment is normalized into a computed comment constructor; its character content is converted to a string as in attribute content.

 
[<!-- Char* -->]Expr
==
comment { [Char*]AttributeContent }

Static Type Analysis

There are no additional static type rules for direct processing-instruction or comment constructors.

Dynamic Evaluation

There are no additional dynamic evaluation rules for direct processing-instruction or comment constructors.

Dynamic Errors

There are no additional error semantics rules for direct processing-instruction constructors.

4.7.3 Computed Constructors

Computed Constructors
[107 (XQuery)]    ComputedConstructor    ::=    CompDocConstructor
| CompElemConstructor
| CompAttrConstructor
| CompTextConstructor
| CompCommentConstructor
| CompPIConstructor
4.7.3.1 Computed Element Constructors
[109 (XQuery)]    CompElemConstructor    ::=    (("element" QName "{") | ("element" "{" Expr "}" "{")) ContentExpr? "}"
[110 (XQuery)]    ContentExpr    ::=    Expr

Notation

Local namespace declarations may occur explicitly in a computed element constructor or may be the result of normalizing namespace-declaration attributes contained in direct element constructors. For local element declarations that occur explicitly in a query, the immediately enclosing expression of the local namespace declaration (CompElemNamespace) must be a computed element constructor; otherwise, as specified in [XPath/XQuery], a static error is raised.

Core Grammar

The Core grammar productions for computed element constructors are:

Computed Element Constructors
[72 (Core)]    CompElemConstructor    ::=    (("element" QName "{") | ("element" "{" Expr "}" "{")) ContentExpr "}"
[73 (Core)]    ContentExpr    ::=    Expr

Normalization

If the content expression is missing, the computed element constructor is normalized as if its content expression was the empty sequence.

 
[element QName { }]Expr
==
[element QName { () }]Expr

Computed element constructors 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) }

Static Type Analysis

The normalization rules of direct element and attribute constructors leave us with only the computed forms of constructors. The static semantic 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 xdt: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.

statEnv.constructionMode = preserve
statEnv |- Expr : Type
statEnv |- Type <: attribute *, (element | text | comment | processing-instruction) *

statEnv |- element QName { Expr } : element QName of type xs:anyType

statEnv.constructionMode = strip
statEnv |- Expr : Type
statEnv |- Type <: attribute *, (element | text | comment | processing-instruction) *

statEnv |- element QName { Expr } : element QName of type xdt:untyped

In case the element name is computed as well, the name expression must be of type xs:QName, xs:string, or xdt:untypedAtomic.

statEnv.constructionMode = preserve
statEnv |- Expr1 : Type1
statEnv |- Type1 <: (xs:QName | xs:string | xdt:untypedAtomic)
statEnv |- Expr2 : Type2
statEnv |- Type2 <: attribute *, (element | text | comment | processing-instruction) *

statEnv |- element { Expr1 } { Expr2 } : element of type xs:anyType

statEnv.constructionMode = strip
statEnv |- Expr1 : Type1
statEnv |- Type1 <: (xs:QName | xs:string | xdt:untypedAtomic)
statEnv |- Expr2 : Type2
statEnv |- Type2 <: attribute *, (element | text | comment | processing-instruction) *

statEnv |- element { Expr1 } { Expr2 } : element of type xdt:untyped

Dynamic Evaluation

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 element's content expression is partitioned into the local namespace declarations and all other expressions, and the 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 3.7.1.2 Namespace Declaration AttributesXQ, it is implementation-defined whether undeclaration of namespace prefixes (by setting the namespace prefix to the empty 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 function fs:item-sequence-to-node-sequence is applied to the element's content expression (excluding local namespace declarations); this function call is evaluated in the new static and dynamic environment. Recall from [4.7.1 Direct Element Constructors] that during normalization, we do not convert the content of direct element constructors that contain one element-content unit. This guarantees that useful type information is preserved for static analysis. Since the conversion function fs:item-sequence-to-node-sequence was not applied to all element constructors during normalization, we have to apply it at evaluation time. (Obviously, it is possible to elide the application of fs:item-sequence-to-node-sequence injected during normalization and the application injected during evaluation.) The resulting value Value0 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.

Expr = CompElemNamespace1, ..., CompElemNamespacen, (Expr0)
CompElemNamespace1 = namespace NCName1 { URI1 }
...
CompElemNamespacen = namespace NCNamen { URIn }
statEnv1 = statEnv + namespace(NCName => (active, URI1))
...
statEnvn = statEnvn-1 + namespace(NCName => (active, URIn))
statEnvn, dynEnv |- fs:item-sequence-to-node-sequence (Expr0) => Value0
Value0 matches (attribute*, (element | text | processing-instruction | comment)*)
NamespaceBindings = (CompElemNamespace1, ... CompElemNamespacen, fs:active_ns(statEnv.namespace), fs:get_static_ns_from_items(statEnv, Value0))

statEnv dynEnv |- element QName { Expr } => Value0

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.

dynEnv |- Expr1 => Value0      statEnv |- Value0 matches xs:QName
Expr2 = CompElemNamespace1, ..., CompElemNamespacen, (Expr3)
CompElemNamespace1 = namespace NCName1 { URI1 }
...
CompElemNamespacen = namespace NCNamen { URIn }
statEnv1 = statEnv + namespace(NCName => (active, URI1))
...
statEnvn = statEnvn-1 + namespace(NCName => (active, URIn))
statEnvn, dynEnv |- fs:item-sequence-to-node-sequence (Expr3); => Value1
statEnvn |- Value1 matches (attribute*, (element | text | processing-instruction | comment)*)
NamespaceBindings = (CompElemNamespace1, ... CompElemNamespacen), fs:active_ns(statEnv.namespace), fs:get_static_ns_from_items(statEnv, Value1)

statEnv dynEnv |- element { Expr1 } { Expr2 } => Value1

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to element constructors. In addition, a computed element constructor with a computed name raises a type error if the name value is not a xs:QName.

dynEnv |- Expr1 => Value1      statEnv |- not (Value1 matches xs:QName)

dynEnv |- element { Expr1 } { Expr2 } raises typeError

Both forms of computed element constructors raise a type error if the element's content is not a sequence of attributes followed by a sequence of element, text, comment, and processing-instruction nodes, or a sequence of atomic values.

dynEnv |- Expr2 => Value2
statEnv |- not (Value matches (attribute *, (element | text | comment | processing-instruction | xdt:anyAtomicType )*))

dynEnv |- element { Expr1 } { Expr2 } raises typeError

dynEnv |- Expr2 => Value2
statEnv |- not (Value matches (attribute *, (element | text | comment | processing-instruction | xdt:anyAtomicType)*))

dynEnv |- element QName { Expr2 } raises typeError

4.7.3.2 Computed Attribute Constructors
[111 (XQuery)]    CompAttrConstructor    ::=    (("attribute" QName "{") | ("attribute" "{" Expr "}" "{")) Expr? "}"

Core Grammar

The Core grammar production for computed attribute constructors is:

Computed Attribute Constructors
[74 (Core)]    CompAttrConstructor    ::=    (("attribute" QName "{") | ("attribute" "{" Expr "}" "{")) Expr "}"

Normalization

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-untypedAtomic function.

 
[attribute QName { }]Expr
==
[attribute QName { () }]Expr
 
[attribute QName { Expr }]Expr
==
attribute QName { fs:item-sequence-to-untypedAtomic([Expr]Expr) }
 
[attribute { Expr1 } { Expr2 }]Expr
==
attribute { fn:data([Expr1]Expr) } { fs:item-sequence-to-untypedAtomic([Expr2]Expr) }

Static Type Analysis

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 xdt:untypedAtomic.

statEnv |- Expr : Type
Type <: xdt:untypedAtomic

statEnv |- attribute QName { Expr } : attribute QName of type xdt:untypedAtomic

statEnv |- Expr1 : Type1
statEnv |- Type1 <: (xs:QName | xs:string | xdt:untypedAtomic)
statEnv |- Expr2 : Type2
statEnv |- Type2 <: xdt:untypedAtomic

statEnv |- attribute { Expr1 } { Expr2 } : attribute of type xdt:untypedAtomic

Dynamic Evaluation

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 function fs:item-sequence-to-untypedAtomic is applied to the content expression and this function call is evaluated in the dynamic environment. Recall from [4.7.3.2 Computed Attribute Constructors] that during normalization, we do not convert the content of direct attribute constructors that contain one attribute-content unit. This guarantees that useful type information is preserved for static analysis. Since the conversion function fs:item-sequence-to-untypedAtomic was not applied to all attribute constructors during normalization, we have to apply it at evaluation time. (As before, it is possible to elide the application of fs:item-sequence-to-untypedAtomic injected during normalization and the application injected during evaluation.)

dynEnv |- Expr => Value0      statEnv |- Value0 matches xs:QName
dynEnv |- fs:item-sequence-to-untypedAtomic(Expr) => Value

dynEnv |- attribute { Expr } { Expr } => attribute { Value0 } of type xdt:untypedAtomic { Value }

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to attribute constructors. In addition, an attribute constructor with a computed name raises a type error if the name value is not a xs:QName. the xmlns namespace.

dynEnv |- Expr1 => Value1      statEnv |- not (Value matches xs:QName)

dynEnv |- attribute { Expr1 } { Expr2 } raises typeError

A dynamic error is raised if the namespace URI of the attribute's QName, whether known statically or dynamically, is in the xmlns namespace.

not(Prefix = xmlns)

dynEnv |- attribute Prefix:LocalPart { Expr } raises dynError

dynEnv |- Expr1 => expanded-QName
not (fn:namespace-uri-from-QName(expanded-QName) = statEnv.statEnv.namespace(xmlns))

dynEnv |- attribute { Expr1 } { Expr2 } raises dynError

4.7.3.3 Document Node Constructors
[108 (XQuery)]    CompDocConstructor    ::=    "document" "{" Expr "}"

Core Grammar

The Core grammar production for a computed document constructor is:

Core computed document construtor
[71 (Core)]    CompDocConstructor    ::=    "document" "{" Expr "}"

Normalization

A document node constructor contains an expression, which must evaluate to a sequence of element, text, comment, or processing-instruction nodes. Section 3.7.3.3 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 [7.1.7 The fs:item-sequence-to-node-sequence function] implements this conversion.

 
[document { Expr }]Expr
==
document { fs:item-sequence-to-node-sequence([Expr]Expr) }

Static Type Analysis

The static semantics checks that the type of the argument expression is a sequence of element, text, processing-instruction, and comment nodes. 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 |- Expr : Type
Type <: (element | text | processing-instruction | comment)*

statEnv |- document { Expr } : document

Dynamic Evaluation

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.

statEnv.constructionMode = preserve
dynEnv |- Expr => Value
dynEnv |- Value matches (element | text | processing-instruction | comment)*

dynEnv |- document { Expr } => document { Value }

statEnv.constructionMode = strip
dynEnv |- Expr => Value1
Value1 erases to Value2
dynEnv |- Value2 matches (element | text | processing-instruction | comment)*

dynEnv |- document { Expr } => document { Value2 }

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to document node constructors. In addition, if the argument expression evaluates to a value that is not a sequence of element, text, processing-instruction, or comment nodes, a type error is raised.

dynEnv |- Expr => Value      dynEnv |- not (Value matches (element | text | processing-instruction | comment )*)

dynEnv |- document { Expr } raises typeError

4.7.3.4 Text Node Constructors
[112 (XQuery)]    CompTextConstructor    ::=    "text" "{" Expr "}"

Core Grammar

The Core grammar production for a computed text constructor is:

[75 (Core)]    CompTextConstructor    ::=    "text" "{" Expr "}"

Normalization

A text node constructor contains an expression, which must evaluate to an xs:string value. Section 3.7.3.4 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, [7.1.8 The fs:item-sequence-to-untypedAtomic function] implements this conversion.

 
[text { Expr }]Expr
==
text { (fs:item-sequence-to-untypedAtomic([Expr]Expr)) cast as xs:string? }

Static Type Analysis

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.

statEnv |- Expr : xs:string?

statEnv |- text { Expr } : text?

Dynamic Evaluation

If the argument expression returns the empty sequence, the text node constructor returns the empty sequence.

dynEnv |- Expr => ()

dynEnv |- text { Expr } => ()

If the argument expression returns a value of type xs:string, the text node constructor returns a text node with that string as content.

dynEnv |- Expr => Value      dynEnv |- Value matches xs:string

dynEnv |- text { Expr } => text { Value }

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to text node constructors. In addition, if the argument expression evaluates to a value that is not a string or the empty sequence, a type error is raised.

dynEnv |- Expr => Value      dynEnv |- not (Value matches xs:string?)

dynEnv |- text { Expr } raises typeError

4.7.3.5 Computed Processing Instruction Constructors
[114 (XQuery)]    CompPIConstructor    ::=    (("processing-instruction" NCName "{") | ("processing-instruction" "{" Expr "}" "{")) Expr? "}"

Core Grammar

The Core grammar production for computed processing-instruction constructors is:

[77 (Core)]    CompPIConstructor    ::=    (("processing-instruction" NCName "{") | ("processing-instruction" "{" Expr "}" "{")) Expr? "}"

Normalization

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 QName { Expr }]Expr
==
processing-instruction [QName]Expr { ( fs:item-sequence-to-untypedAtomic ([Expr]Expr )) cast as xs:string }
 
[processing-instruction { Expr1 } { Expr2 }]Expr
==
let $fs:new1 as (xs:QName | xs:string) := fn:data ([Expr1]Expr) return
let $fs:new3 :=
     typeswitch ($fs:new1)
     case $fs:new2 as xs:QName return $fs:new2
     case $fs:new2 as xs:string return xs:QName($fs:new2)
     default return fn:error()
let $fs:new4 := if not(fn:namespace-uri-from-QName($fs:new3) = ()) then $fs:new3 else fn:error()
return processing-instruction { $fs:new4 } { (fs:item-sequence-to-untypedAtomic ([Expr2]Expr)) cast as xs:string }

Static Type Analysis

The static typing rules for processing-instruction constructors are straightforward.

statEnv |- Expr : xs:string

statEnv |- processing-instruction NCName { Expr } : processing-instruction

statEnv |- Expr1 : xs:QName      statEnv |- Expr2 : xs:string

statEnv |- processing-instruction { Expr1 } { Expr2 } : processing-instruction

Dynamic Evaluation

The dynamic evaluation rules for computed processing instructions are straightforward.

dynEnv |- Expr => Value      dynEnv |- Value matches xs:string

dynEnv |- processing-instruction NCName { Expr } => processing-instruction NCName { Value }

dynEnv |- Expr1 => Value1      dynEnv |- Value1 matches xs:QName
dynEnv |- Expr2 => Value2      dynEnv |- Value2 matches xs:string

dynEnv |- processing-instruction { Expr1 } { Expr2 } => processing-instruction Value1 { Value2 }

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to computed processing-instruction constructors. The normalization rules guarantee that a dynamic error is raised if the target expression is not a string or a QName.

4.7.3.6 Computed Comment Constructors
[113 (XQuery)]    CompCommentConstructor    ::=    "comment" "{" Expr "}"

Core Grammar

The Core grammar production for computed comment constructors is:

[76 (Core)]    CompCommentConstructor    ::=    "comment" "{" Expr "}"

Normalization

Computed processing-instruction constructors are normalized by mapping their content expression.

 
[comment { Expr }]Expr
==
comment { (fs:item-sequence-to-untypedAtomic ([Expr]Expr)) cast as xs:string }

Static Type Analysis

The static typing rule for computed comment constructors is straightforward.

statEnv |- Expr : xs:string

statEnv |- comment { Expr } : comment

Dynamic Evaluation

The dynamic evaluation rule for computed comment constructors is straightforward.

dynEnv |- Expr => Value      dynEnv |- Value matches xs:string

dynEnv |- comment { Expr } => comment { Value }

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to computed comment constructors.

4.7.4 In-scope Namespaces of a Constructed Element

The normalization and static semantics of local namespace declarations is defined here. The dynamic semantics of local namespace declarations and their effect on constructed elements in specified in [4.7.1 Direct Element Constructors] and [4.7.3.1 Computed Element Constructors].

Normalization

Local namespace declarations normalized by mapping their name and content expression in the same way as computed processing-instruction constructors.

 
[namespace NCName { Expr }]Expr
==
namespace [NCName]Expr { ( fs:item-sequence-to-untypedAtomic ([Expr]Expr )) cast as xs:string }

Static Type Analysis

A local namespace declaration may only occur within a computed element constructor. The result of evaluating a local namespace declaration is a new namespace binding for the constructed element. Because the local namespace declaration has no effect on the type of the element, its static type is the empty type.

statEnv |- Expr : xs:string

statEnv |- namespace NCName { Expr } : empty

Dynamic Evaluation

The dynamic evaluation rules for a computed element namespace are given in the evaluation rules for computed element constructors in [4.7.3.1 Computed Element Constructors].

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to computed element namespaces.

4.8 [For/FLWR] Expressions

Introduction

[XPath/XQuery] provides [For/FLWR] 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 the , 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. The dynamic semantics is not specified formally as it would require the introduction of tuples, which are not supported in the [XPath/XQuery] data model.

[For/FLWR] Expressions
[33 (XQuery)]    FLWORExpr    ::=    (ForClause | LetClause)+ WhereClause? OrderByClause? "return" ExprSingle
[34 (XQuery)]    ForClause    ::=    "for" "$" VarName TypeDeclaration? PositionalVar? "in" ExprSingle ("," "$" VarName TypeDeclaration? PositionalVar? "in" ExprSingle)*
[36 (XQuery)]    LetClause    ::=    "let" "$" VarName TypeDeclaration? ":=" ExprSingle ("," "$" VarName TypeDeclaration? ":=" ExprSingle)*
[116 (XQuery)]    TypeDeclaration    ::=    "as" SequenceType
[35 (XQuery)]    PositionalVar    ::=    "at" "$" VarName
[37 (XQuery)]    WhereClause    ::=    "where" ExprSingle
[38 (XQuery)]    OrderByClause    ::=    ("order" "by" | "stable" "order" "by") OrderSpecList
[39 (XQuery)]    OrderSpecList    ::=    OrderSpec ("," OrderSpec)*
[40 (XQuery)]    OrderSpec    ::=    ExprSingle OrderModifier
[41 (XQuery)]    OrderModifier    ::=    ("ascending" | "descending")? (("empty" "greatest") | ("empty" "least"))? ("collation" URILiteral)?
[4 (XPath)]    ForExpr    ::=    SimpleForClause "return" ExprSingle
[5 (XPath)]    SimpleForClause    ::=    "for" "$" VarName "in" ExprSingle ("," "$" VarName "in" ExprSingle)*

Core Grammar

The Core grammar productions for FLWOR expressions are:

For Expressions
[32 (Core)]    FLWORExpr    ::=    (ForClause | LetClause) "return" ExprSingle
[33 (Core)]    ForClause    ::=    "for" "$" VarName TypeDeclaration? PositionalVar? "in" ExprSingle
[35 (Core)]    LetClause    ::=    "let" "$" VarName TypeDeclaration? ":=" ExprSingle
[34 (Core)]    PositionalVar    ::=    "at" "$" VarName
[79 (Core)]    TypeDeclaration    ::=    "as" SequenceType
[36 (Core)]    OrderByClause    ::=    ("order" "by" | "stable" "order" "by") OrderSpecList
[37 (Core)]    OrderSpecList    ::=    OrderSpec ("," OrderSpec)*
[38 (Core)]    OrderSpec    ::=    ExprSingle OrderModifier
[39 (Core)]    OrderModifier    ::=    ("ascending" | "descending")? (("empty" "greatest") | ("empty" "least"))? ("collation" URILiteral)?

4.8.1 FLWOR expressions

Notation

Individual [For/FLWR] clauses are normalized by means of the auxiliary normalization rules:

[FLWORClause]FLWOR(Expr)

Where FLWORClause can be any either a ForClause, a LetClause, a WhereClause, or an OrderByClause. The OrderByClause is discussed in [4.8.4 Order By and Return Clauses].

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.

Notation

The auxiliary rule []FLWOR(Expr) normalizes a For, Let, or Where clause in a FLWORExpr expression. Note that the rule takes the remainder of the FLWOR expression (other For, Let, or Where clauses and the Return clause) as a parameter in Expr.

Normalization

The [For/FLWR] expressions include the FLWORExpr of XQuery and the ForExpr of XPath. The normalization rule for ForExpr is simple: It simply unrolls a ForExpr that binds multiple variables into nested ForExprs, each of which bind one variable.

 
[for VarRef0 in Expr0, ..., VarRefn in Exprn return Expr ]Expr
==
for VarRef0 in [Expr0]Expr return
...
for VarRefn in [Exprn]Expr return
[Expr]Expr

Full FLWORExpr expressions are normalized to nested core expressions using two sets of normalization rules. Note that some of the rules also accept ungrammatical FLWORExprs such as "where Expr1 return Expr2". This does not matter, as normalization is always applied on parsed [XPath/XQuery] expressions, and ungrammatical FLWORExprs would be rejected by the parser beforehand.

The first set of rules is applied on a full [For/FLWR] expression, splitting it at the clause level, then applying further normalization on each separate clause.

 
[ (ForClause | LetClause | WhereClause | OrderByClause) FLWORExpr ]Expr
==
[(ForClause | LetClause | WhereClause | OrderByClause)]FLWOR([FLWORExpr]Expr)
 
[ (ForClause | LetClause | WhereClause | OrderByClause) return Expr ]Expr
==
[(ForClause | LetClause | WhereClause | OrderByClause)]FLWOR([Expr]Expr)

Then each [For/FLWR] clause is normalized separately. A ForClause may bind more than one variable, whereas a For expression in the [XPath/XQuery] Core binds and iterates over only one variable. Therefore, a ForClause is normalized to nested for expressions:

 
[
for VarRef1 TypeDeclaration1? PositionalVar1? in Expr1,
···,
VarRefn TypeDeclarationn? PositionalVarn? in Exprn
] FLWOR(Expr)
==
for VarRef1 TypeDeclaration1? PositionalVar1? in [Expr1]Expr return
  ···
     for VarRefn TypeDeclarationn? PositionalVarn? in [ Exprn ]Expr return Expr

Note that the additional Expr parameter of the auxiliary normalization rule is used as the final return expression.

Likewise, a LetClause clause is normalized to nested let expressions, each of which binds one variable:

 
[
let VarRef1 TypeDeclaration1? := Expr1,
···,
VarRefn TypeDeclarationn? := Exprn
]FLWOR(Expr)
==
let VarRef1 TypeDeclaration1? := [Expr1 ]Expr return
  ···
    let VarRefn TypeDeclarationn? := [Exprn]Expr return Expr

A WhereClause is normalized to an IfExpr, with the else-branch returning the empty sequence:

 
[ where Expr1]FLWOR(Expr)
==
if ( [Expr1]Expr ) then Expr else ()

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 binds 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>)

4.8.2 For expression

Static Type Analysis

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 VarRef1 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).

statEnv |- Expr1 : Type1
statEnv + varType(VarRef1 : prime(Type1)) |- Expr2 : Type2

statEnv |- for VarRef1 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 |- Expr1 : Type1
statEnv + varType(VarRef1 : prime(Type1), VarRefpos : xs:integer) |- Expr2 : Type2

statEnv |- for VarRef1 at VarRefpos 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 VarRef1 with type Type0. This semantics is specified by the following typing rule.

statEnv |- Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
prime(Type1) <: Type0
statEnv + varType(VarRef1 : Type0)) |- Expr2 : Type2

statEnv |- for VarRef1 as SequenceType in Expr1 return Expr2 : Type2 · quantifier(Type1)

The last rule contains a For expression that contains 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 |- Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
prime(Type1) <: Type0
statEnv + varType(VarRef1 : Type0, VarRefpos : xs:integer) |- Expr2 : Type2

statEnv |- for VarRef1 as SequenceType at VarRefpos in Expr1 return Expr2 : Type2 · quantifier(Type1)

Example

For example, if $example is bound to the sequence 10.0, 1.0E1, 10 of type xsd:decimal, xsd:float, xsd:integer, then the query

  for $s in $example
  return $s * 2

is typed as follows:

  (1) prime(xsd:decimal, xsd:float, xsd:integer) =
      xsd:decimal | xsd:float | xsd:integer
  (2) quantifier(xsd:decimal, xsd:float, xsd:integer) = +
  (3) $s : xsd:decimal | xsd:float | xsd:integer
  (4) $s * 2 : 
      xsd:decimal | xsd:float | xsd:integer
  (5) result-type :
      ( xsd:decimal | xsd:float | xsd: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: element out {element one {}}, element out {element two {}}, element out {element three {}}. However, inferring such a specific type for arbitrary input types and arbitrary return clauses requires significantly more complex type inference 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.

Dynamic Evaluation

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 VarRef1 TypeDeclaration? 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 environment dynEnv extended with VarRef1 bound to Itemi. This produces values Valuei, ..., Valuen which are concatenated to produce the result sequence.

dynEnv |- Expr1 => Item1 ,..., Itemn
statEnv |- VarRef of var expands to Variable      dynEnv + varValue(Variable => Item1) |- Expr2 => Value1
···
dynEnv + varValue(Variable => Itemn) |- Expr2 => Valuen

dynEnv |- for VarRef in Expr1 return Expr2 => Value1 ,..., Valuen

The following rule is the same as the rule above, but includes the optional positional variable VarRefpos. If present, VarRefpos is bound to the position of the item in the input sequence, i.e., the value i.

dynEnv |- Expr1 => Item1 ,..., Itemn
statEnv |- VarRef of var expands to Variable      statEnv |- VarRefpos of var expands to Variablepos
dynEnv + varValue(Variable => Item1, Variablepos => 1) |- Expr2 => Value1
···
dynEnv + varValue(Variable => Itemn, Variablepos => n) |- Expr2 => Valuen

dynEnv |- for VarRef at VarRefpos 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 rule.

dynEnv |- Expr1 => Item1 ,..., Itemn
Type0 = [ SequenceType ]sequencetype
Item1 matches Type0
statEnv |- VarRef of var expands to Variable      dynEnv + varValue(Variable => Item1) |- Expr2 => Value1
···
Itemn matches Type0
dynEnv + varValue(Variable => Itemn) |- Expr2 => Valuen

dynEnv |- for VarRef as SequenceType in Expr1 return Expr2 => gr_Value1; ,..., Valuen

The last rule covers a For expresstion that contains a type declaration and a positional variable.

dynEnv |- Expr1 => Item1 ,..., Itemn
Type0 = [ SequenceType ]sequencetype
Item1 matches Type0
statEnv |- VarRef of var expands to Variable      statEnv |- VarRefpos of var expands to Variablepos
dynEnv + varValue(Variable => Item1, Variablepos => 1) |- Expr2 => Value1
···
Itemn matches Type0
dynEnv + varValue(Variable => Itemn, Variablepos => n) |- Expr2 => Valuen

dynEnv |- for VarRef as SequenceType at VarRefpos in Expr1 return Expr2 => Value1 ,..., Valuen

Note that this definition allows non-deterministic evaluation of the resulting sequence, since the judgments above the inference rule can be evaluated in any order.

Dynamic Errors

If evaluation of the first expression raises an error, the entire expression raises an error. This rule applies to all forms of a For expression, i.e., those with or without a type declaration or positional variable.

dynEnv |- Expr1 raises Error

dynEnv |- for Variable1 TypeDeclaration1? PositionalVar1? in Expr1 return Expr2 raises Error

If any evaluation of the body of the for expression raises an error, then the entire expression raises an error. This rule applies to for expressions with or without the type declaration.

dynEnv |- Expr1 => Item1 ,..., Itemn
statEnv |- VarRef of var expands to Variable
dynEnv + varValue(Variable => Itemi) |- Expr2 raises Error      1 <= i <= n

dynEnv |- for VarRef TypeDeclaration? in Expr1 return Expr2 raises Error

dynEnv |- Expr1 => Item1 ,..., Itemn
statEnv |- VarRef of var expands to Variable      statEnv |- VarRefpos of var expands to Variablepos
dynEnv + varValue(Variable => ItemiVariablepos => i) |- Expr2 raises Error      1 <= i <= n

dynEnv |- for VarRef TypeDeclaration? at VarRefpos in Expr1 return Expr2 raises Error

When a type declaration is present, a type error is raised if any item in the result of evaluating Expr1 does not match the declared type.

dynEnv |- Expr1 => Item1 ,..., Itemn
Type0 = [ SequenceType ]sequencetype
not (Itemi matches Type0)      1 <= i <= n

dynEnv |- for VarRef as SequenceType PositionalVar1? in Expr1 return Expr2 raises typeError

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>)

4.8.3 Let Expression

Static Type Analysis

A let expression extends the type 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 |- Expr1 : Type1      statEnv |- VarRef of var expands to Variable      statEnv + varType(Variable1 : Type1) |- Expr2 : Type2

statEnv |- let VarRef := 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 rule.

statEnv |- Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
Type1 <: Type0
statEnv |- VarRef of var expands to Variable      statEnv + varType(Variable1 : Type0 ) |- Expr2 : Type2

statEnv |- let VarRef1 as SequenceType := Expr1 return Expr2 : Type2

Dynamic Evaluation

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 |- Expr1 => Value1
statEnv |- VarRef of var expands to Variable      dynEnv + varValue(Variable1 => Value1) |- Expr2 => Value2

dynEnv |- let VarRef1 := 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 rule.

dynEnv |- Expr1 => Value1
Type0 = [ SequenceType ]sequencetype
Value1 matches Type0
statEnv |- VarRef of var expands to Variable      dynEnv + varValue(Variable1 => Value1) |- Expr2 => Value2

dynEnv |- let VarRef1 as SequenceType := Expr1 return Expr2 => Value2

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to let expressions. In addition, in the case that a type declaration is present, a type error is raised if the result of evaluating Expr1 does not match the declared type.

dynEnv |- Expr1 => Value1
Type0 = [ SequenceType ]sequencetype
not (Value1 matches Type0)

dynEnv |- let VarRef1 as SequenceType := Expr1 return Expr2 raises typeError

Example

Note the use of the environment discipline 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.

4.8.4 Order By and Return Clauses

Introduction

The dynamic semantics of the OrderByClause is not specified formally. The dynamic semantics is not specified formally as it 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.

Because an OrderByClause does not effect the type of a FLWORExpr expression, 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 omitted but a gt comparison is applied.

Notation

To define normalization of OrderBy, the following auxiliary mapping rule is used.

 
[OrderSpecList]OrderSpecList
==
[LetClause ... LetClause]

which specify that OrderSpecList is mapped to Expr.

Normalization

An OrderByClause is normalized to a Let clause, nested For expressions, and atomization, which guarantees that the OrderSpecList is well typed. Note that if evaluated dynamically, the normalization of OrderByClause given here does not express the required sorting semantics, but this normalization does provide the correct static type. Notably, the normalization rule uses the gt operation, which implies that the ordering criteria is typed using the same static typing rules, taking into account existential quantification, atomization and type promotion.

 
[ stable? order by OrderSpecList]FLWOR(Expr)
==
[OrderSpecList]OrderSpecList return Expr

Each OrderSpec is normalized the auxiliary atomization normalization rule.

 
[Expr OrderModifier, OrderSpecList]OrderSpecList
==
let $fs:new0 :=
   for $fs:new1 in Expr
   for $fs:new2 in Expr return
     [$fs:new1 gt $fs:new2]Expr
[OrderSpecList]OrderSpecList

4.9 Ordered and Unordered Expressions

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.

[89 (XQuery)]    OrderedExpr    ::=    "ordered" "{" Expr "}"
[90 (XQuery)]    UnorderedExpr    ::=    "unordered" "{" Expr "}"

Core Grammar

The Core grammar productions for ordered/unordered expressions are:

[67 (Core)]    OrderedExpr    ::=    "ordered" "{" Expr "}"
[68 (Core)]    UnorderedExpr    ::=    "unordered" "{" Expr "}"

Normalization

OrderedExpr (resp. UnorderedExpr) expressions are normalized to OrderedExpr (resp. UnorderedExpr) expressions in the [XPath/XQuery] core.

 
[ordered { Expr }]Expr
==
ordered { [Expr]Expr }
 
[unordered { Expr }]Expr
==
unordered { [Expr]Expr }

Dynamic Evaluation

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.

dynEnv |- Expr => Value

dynEnv |- ordered { Expr } => Value

dynEnv |- Expr => Value

dynEnv |- unordered { Expr } => Value

Static Type Analysis

OrderedExpr and UnorderedExpr expressions set the ordering mode in the static context to ordered or unordered.

statEnv1 = statEnv + orderingMode(ordered)
statEnv1 |- Expr : Type

statEnv |- ordered { Expr } : Type

statEnv1 = statEnv + orderingMode(unordered)
statEnv1 |- Expr : Type

statEnv |- unordered { Expr } : Type

4.10 Conditional Expressions

Introduction

A conditional expression supports conditional evaluation of one of two expressions.

Conditional Expression
[45 (XQuery)]    IfExpr    ::=    "if" "(" Expr ")" "then" ExprSingle "else" ExprSingle

Core Grammar

The Core grammar production for the conditional expression is:

Core Conditional Expression
[43 (Core)]    IfExpr    ::=    "if" "(" Expr ")" "then" ExprSingle "else" ExprSingle

Normalization

 
[if (Expr1) then Expr2 else Expr3]Expr
==
  if (fn:boolean([ Expr1 ]Expr)) then [Expr2]Expr else [Expr3]Expr

Static Type Analysis

statEnv |- Expr1 : xs:boolean      statEnv |- Expr2 : Type2      statEnv |- Expr3 : Type3

statEnv |- if (Expr1) then Expr2 else Expr3 : (Type2 | Type3)

Dynamic Evaluation

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 evaluation rules ensures that only one branch of the conditional is evaluated.

dynEnv |- Expr1 => true      dynEnv |- Expr2 => Value2

dynEnv |- if Expr1 then Expr2 else Expr3 => Value2

dynEnv |- Expr1 => false      dynEnv |- Expr3 => Value3

dynEnv |- if Expr1 then Expr2 else Expr3 => Value3

Dynamic Errors

If the conditional's boolean expression raises an error, then the conditional expression raises an error.

dynEnv |- Expr1 raises Error

dynEnv |- if Expr1 then Expr2 else Expr3 raises Error

If the conditional's boolean expression Expr1 evaluates to true, and Expr2 raises an error, then the conditional expression raises an error. Conversely, if the conditional's boolean expression evaluates to false, and Expr3 raises an error, then the conditional raises an error.

dynEnv |- Expr1 => true      dynEnv |- Expr2 raises Error

dynEnv |- if Expr1 then Expr2 else Expr3 raises Error

dynEnv |- Expr1 => false      dynEnv |- Expr3 => Error

dynEnv |- if Expr1 then Expr2 else Expr3 raises Error

4.11 Quantified Expressions

Introduction

[XPath/XQuery] defines two quantification expressions:

Quantified Expression
[42 (XQuery)]    QuantifiedExpr    ::=    (("some" "$") | ("every" "$")) VarName TypeDeclaration? "in" ExprSingle ("," "$" VarName TypeDeclaration? "in" ExprSingle)* "satisfies" ExprSingle
[6 (XPath)]    QuantifiedExpr    ::=    (("some" "$") | ("every" "$")) VarName "in" ExprSingle ("," "$" VarName "in" ExprSingle)* "satisfies" ExprSingle

Core Grammar

The Core grammar production for quantified expressions is:

[40 (Core)]    QuantifiedExpr    ::=    (("some" "$") | ("every" "$")) VarName TypeDeclaration? "in" ExprSingle ("," "$" VarName TypeDeclaration? "in" ExprSingle)* "satisfies" ExprSingle

Normalization

The quantified expressions are normalized into nested Core quantified expressions, each of which binds one variable.

 
[some VarRef1 in Expr1, ..., VarRefn in Exprn satisfies Expr]Expr
==
some VarRef1 in [Expr1]Expr satisfies
   some VarRef2 in [Expr2]Expr satisfies
         ...
     some VarRefn in [Exprn]Expr satisfies
     fn:boolean([Expr]Expr)
 
[every VarRef1 in Expr1, ..., VarRefn in Exprn satisfies Expr]Expr
==
every VarRef1 in [Expr1]Expr satisfies
   every VarRef2 in [Expr2]Expr satisfies
         ...
     every VarRefn in [Exprn]Expr satisfies
     fn:boolean([Expr]Expr)

Static Type Analysis

The static semantics of the quantified expressions uses the prime operator on types, which is explained in [8.4 Judgments for FLWOR and other expressions on sequences]. These rules are similar to those for For expressions in [4.8.2 For expression].

statEnv |- Expr1 : Type1
statEnv |- VarRef1 of var expands to Variable1      statEnv + varType(Variable1 : prime(Type1)) |- Expr2 : xs:boolean

statEnv |- some VarRef1 in Expr1 satisfies Expr2 : xs:boolean

The next rule is for SomeExpr with the optional type declaration.

statEnv |- Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
prime(Type1) <: Type0
statEnv |- VarRef1 of var expands to Variable1      statEnv + varType(Variable1 : Type0) |- Expr2 : xs:boolean

statEnv |- some VarRef1 as SequenceType in Expr1 satisfies Expr2 : xs:boolean

The next rule is for EveryExpr without the optional type declaration.

statEnv |- Expr1 : Type1
statEnv |- VarRef1 of var expands to Variable1      statEnv + varType(Variable1 : prime(Type1)) |- Expr2 : xs:boolean

statEnv |- every VarRef1 in Expr1 satisfies Expr2 : xs:boolean

The next rule is for EveryExpr with the optional type declaration.

statEnv |- Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
prime(Type1) <: Type0
statEnv |- VarRef1 of var expands to Variable1      statEnv + varType(Variable1 : Type0) |- Expr2 : xs:boolean

statEnv |- every VarRef1 as SequenceType in Expr1 satisfies Expr2 : xs:boolean

Dynamic Evaluation

The existentially quantified "some" expression yields true if any evaluation of the satisfies expression yields true. The existentially quantified "some" 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 |- Expr1 => Item1 ... Itemn
1 <= i <= n
statEnv |- VarRef1 of var expands to Variable1      dynEnv(Variable1 => Itemi)) |- Expr2 => true

dynEnv |- some VarRef1 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 |- Expr1 => Item1 ... Itemn
1 <= i <= n
Type0 = [ SequenceType ]sequencetype
Itemi matches Type0
statEnv |- VarRef1 of var expands to Variable1      dynEnv(Variable1 => Itemi)) |- Expr2 => true

dynEnv |- some VarRef1 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 yields false.

dynEnv |- Expr1 => Item1 ... Itemn
statEnv |- VarRef1 of var expands to Variable1      dynEnv(Variable1 => Item1)) |- Expr2 => false
...
dynEnv(VarRef1 => Itemn)) |- Expr2 => false

dynEnv |- some VarRef1 in Expr1 satisfies Expr2 => false

The next rule is for SomeExpr with the optional type declaration, in which all evaluations of the satisfies expression yields false.

dynEnv |- Expr1 => Item1 ... Itemn
Type0 = [ SequenceType ]sequencetype
statEnv |- VarRef1 of var expands to Variable1      dynEnv(Variable1 => Item1)) |- Expr2 => false
Item1 matches Type0
...
statEnv |- VarRef1 of var expands to Variable1      dynEnv(Variable1 => Itemn)) |- Expr2 => false
Itemn matches Type0

dynEnv |- some VarRef1 as SequenceType in Expr1 satisfies Expr2 => false

The universally quantified "every" expression yields false if any evaluation of the satisfies expression yields false. The universally quantified "every" expression yields true if every evaluation of the satisfies expression is true.

dynEnv |- Expr1 => Item1 ... Itemn
1 <= i <= n
statEnv |- VarRef1 of var expands to Variable1      dynEnv(Variable1 => Itemi)) |- Expr2 => false

dynEnv |- every VarRef1 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 |- Expr1 => Item1 ... Itemn
1 <= i <= n
Type0 = [ SequenceType ]sequencetype
Itemi matches Type0
statEnv |- VarRef1 of var expands to Variable1      dynEnv(Variable1 => Itemi)) |- Expr2 => false

dynEnv |- every VarRef1 as SequenceType in Expr1 satisfies Expr2 => false

The next rule is for EveryExpr in which all evaluations of the satisfies expression yields true.

dynEnv |- Expr1 => Item1 ... Itemn
statEnv |- VarRef1 of var expands to Variable1      dynEnv(Variable1 => Item1)) |- Expr2 => true
...
dynEnv(Variable1 => Itemn)) |- Expr2 => true

dynEnv |- every VarRef1 in Expr1 satisfies Expr2 => true

The next rule is for EveryExpr with the optional type declaration in which all evaluations of the satisfies expression yields true.

dynEnv |- Expr1 => Item1 ... Itemn
Type0 = [ SequenceType ]sequencetype
statEnv |- VarRef1 of var expands to Variable1      dynEnv(Variable1 => Item1)) |- Expr2 => true
Item1 matches Type0
...
dynEnv(Variable1 => Itemn)) |- Expr2 => true
Itemn matches Type0

dynEnv |- every VarRef1 as SequenceType in Expr1 satisfies Expr2 => true

Dynamic Errors

An existentially quantified expression raises an error if:

  • evaluation of the first expression raises an error,

  • any evaluation of the satisfies expression raises an error.

dynEnv |- Expr1 raises Error

dynEnv |- some VarRef1 TypeDeclaration ? in Expr1 satisfies Expr2 raises Error

dynEnv |- Expr1 => Item1 ... Itemn
1 <= i <= n
statEnv |- VarRef1 of var expands to Variable1      dynEnv(Variable1 => Itemi)) |- Expr2 raises Error

dynEnv |- some VarRef1 TypeDeclaration? in Expr1 satisfies Expr2 raises Error

dynEnv |- Expr1 raises Error

dynEnv |- every VarRef1 in Expr1 satisfies Expr2 raises Error

dynEnv |- Expr1 => Item1 ... Itemn
1 <= i <= n
statEnv |- VarRef1 of var expands to Variable1      dynEnv(Variable1 => Itemi)) |- Expr2 raises Error

dynEnv |- every VarRef1 in Expr1 satisfies Expr2 raises Error

An existentially quantified expression raises a type error if evaluation of the first expression yields a value, and some item in this value does not match the declared type of the variable.

dynEnv |- Expr1 => Item1 ... Itemn
Type0 = [ SequenceType ]sequencetype
1 <= i <= n
not(Itemi matches Type0)

dynEnv |- some VarRef1 as SequenceType in Expr1 satisfies Expr2 raises typeError

dynEnv |- Expr1 => Item1 ... Itemn
Type0 = [ SequenceType ]sequencetype
1 <= i <= n
not(Itemi matches Type0)

dynEnv |- every VarRef1 as SequenceType in Expr1 satisfies Expr2 raises typeError

4.12 Expressions on SequenceTypes

Introduction

Expressions on SequenceTypes are expressions whose semantics depends on the type of some of the sub-expressions to which they are applied. The syntax of SequenceType expressions is described in [3.5.3 SequenceType Syntax].

4.12.1 Instance Of

SequenceType expressions
[54 (XQuery)]    InstanceofExpr    ::=    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.

Normalization

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.

 
[Expr instance of SequenceType]Expr
==
typeswitch ([ Expr ]Expr)
  case $fs:new as SequenceType return fn:true()
  default $fs:new return fn:false()

4.12.2 Typeswitch

SequenceType expressions
[43 (XQuery)]    TypeswitchExpr    ::=    "typeswitch" "(" Expr ")" CaseClause+ "default" ("$" VarName)? "return" ExprSingle
[44 (XQuery)]    CaseClause    ::=    "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 VarRef, which is bound the value of the input expression. This variable is optional in [XPath/XQuery] but mandatory in the [XPath/XQuery] core. One of the reasons for having this variable is that it is assigned a specific type for the corresponding branch.

Core Grammar

The Core grammar productions for typeswitch are:

[41 (Core)]    TypeswitchExpr    ::=    "typeswitch" "(" Expr ")" CaseClause+ "default" ("$" VarName)? "return" ExprSingle
[42 (Core)]    CaseClause    ::=    "case" ("$" VarName "as")? SequenceType "return" ExprSingle

Notation

To define normalization of case clauses to the [XPath/XQuery] core, the following auxiliary mapping rule is used.

 
[CaseClause]Case
==
CaseClause

specifies that CaseClause is mapped to CaseClause, in the [XPath/XQuery] type system.

Normalization

Normalization of a typeswitch expression guarantees that every branch has an associated VarRef. The following normalization rule adds a newly created variable that does not appear in the rest of the query. Note that $fs:new is a newly generated variable that must not conflict with any variables already in scope and that is not used in any of the sub-expressions.

 
[   case SequenceType return Expr ]Case
==
  case $fs:new1 as SequenceType return [ Expr ]Expr
 
[   case VarRef as SequenceType return Expr ]Case
==
  case VarRef as SequenceType return [ Expr ]Expr
 
[ default return Expr ]Case
==
default $fs:new1 return [ Expr ]Expr
 
[ default VarRef return Expr ]Case
==
default VarRef return [ Expr ]Expr
 
[
typeswitch ( Expr0 )
  CaseClause1
    ···
  CaseClausen
  default (VarRef)? return Exprn+1
]Expr
==
typeswitch ( [ Expr0 ]Expr )
[CaseClause1]Case
    ···
[CaseClausen]Case
[  default (VarRef)? return Exprn+1 ]Case

Notation

The following auxiliary grammar production is used to identify branches of the typeswitch.

CaseRules
[75 (Formal)]    CaseRules    ::=    ("case" "$" VarName "as" SequenceType "return" Expr CaseRules) | ("default" "$" VarName "return" Expr)

The following judgment

statEnv |- Type1 case CaseClause : Type     

is used in the static of typeswitch. It indicates that under the environment statEnv, and with the input type of the typeswitch being Type1, the given case rule yields the type Type.

The following judgment

dynEnv |- Value1 against CaseRules => Value2

is used in the dynamic semantics of typeswitch. It indicates that under the environment dynEnv, with the input value of the typeswitch being Value1, the given case rules yields the value Value2.

Static Type Analysis

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 |- Expr0 : Type0
statEnv |- Type0 case case VarRef1 as SequenceType1 return Expr1 : Type1
    ···
statEnv |- Type0 case case VarRefn as SequenceTypen return Exprn : Typen
statEnv |- Type0 case default VarRefn+1 return Exprn : Typen+1

statEnv |-  
(typeswitch (Expr0)
  case VarRef1 as SequenceType1 return Expr1
    ···
  case VarRefn as SequenceTypen return Exprn
  default VarRefn+1 return Exprn+1)
: (Type1 | ... | Typen+1)

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.

CaseType = [ SequenceType ]sequencetype
statEnv(VarRef : CaseType ) |- Expr : Type

Type0 case case VarRef 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(VarRef : Type0 ) |- Expr : Type

Type0 case default VarRef return Expr : Type

Dynamic Evaluation

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 |- Expr => Value0
dynEnv |- Value0 against CaseRules => Value1

dynEnv |- typeswitch (Expr) CaseRules => Value1

If the value matches the sequence type, the following rule applies: It extends the environment by binding the variable Variable to Value0 and evaluates the body of the return clause.

CaseType = [ SequenceType ]sequencetype
Value0 matches CaseType
statEnv |- VarRef of var expands to Variable      dynEnv + varValue(Variable => Value0) |- Expr => Value1

dynEnv |- Value0 against case VarRef SequenceType return Expr CaseRules => Value1

If the value does not match the sequence type, the current case is not evaluated, and the remaining case rules are evaluated order by applying the inference rule recursively.

CaseType = [ SequenceType ]sequencetype      not(Value0 matches CaseType)      dynEnv |- Value0 against CaseRules => Value1

dynEnv |- Value0 against case SequenceType VarRef return Expr CaseRules => Value1

The last rule states that the default branch of a typeswitch expression always evaluates to the value of its return clause.

statEnv |- VarRef of var expands to Variable      dynEnv + varValue(Variable => Value0) |- Expr => Value1

dynEnv |- Value0 against default VarRef return Expr => Value1

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to the typeswitch expression. In particular, if evaluation of the input expression or evaluation of any case rule raises an error, then the typeswitch expression raises an error.

4.12.3 Cast

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)]    CastExpr    ::=    UnaryExpr ( "cast" "as" SingleType )?
[115 (XQuery)]    SingleType    ::=    AtomicType "?"?

Core Grammar

The Core grammar productions for cast expressions are:

[47 (Core)]    CastExpr    ::=    ValueExpr ( "cast" "as" SingleType )?
[78 (Core)]    SingleType    ::=    AtomicType "?"?

Normalization

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
==
let $v as xdt:anyAtomicType := fn:data([ Expr ]Expr) return
  $v cast as AtomicType
 
[Expr cast as AtomicType? ]Expr
==
let $v as xdt:anyAtomicType ? := fn:data([ Expr ]Expr) return
  typeswitch ($v)
    case void() return ()
    default return $v cast as AtomicType

Static Type Analysis

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

Dynamic Evaluation

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 rules for cast in Section 17 CastingFO are applied. These rules are not specified further here.

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to cast expressions.

4.12.4 Castable

[56 (XQuery)]    CastableExpr    ::=    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:

[46 (Core)]    CastableExpr    ::=    CastExpr ( "castable" "as" SingleType )?

Normalization

The normalization of castable simply maps its expression argument.

 
[Expr castable as AtomicType]Expr
==
let $v as xdt:anyAtomicType := fn:data([ Expr ]Expr) return
$v castable as AtomicType
 
[Expr castable as AtomicType]Expr
==
let $v as xdt:anyAtomicType? := fn:data([ Expr ]Expr) return
$v castable as AtomicType?

Static Type Analysis

The type of a core castable expression is always a boolean.


statEnv |- Expr castable as AtomicType : xs:boolean

Dynamic Evaluation

If casting succeeds, then the castable expression evaluates to true.

dynEnv |- Expr => Value1
( Value1 ) cast as AtomicType=> Value2

dynEnv |- Expr castable as AtomicType => true

If casting raises a dynamic error, 'castable as' evaluates to false.

( Expr1 ) cast as AtomicType2 raises dynError

dynEnv |- Expr1 castable as AtomicType2 => false

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to castable expression.

4.12.5 Constructor Functions

Constructor functions provide an alternative syntax for casting.

Normalization

Constructor functions for atomic types are normalized to explicit cast as expressions.

 
[AtomicType(Expr)]Expr
==
[Expr cast as AtomicType? ]Expr

4.12.6 Treat

[55 (XQuery)]    TreatExpr    ::=    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.

Normalization

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.

 
[Expr treat as SequenceType]Expr
==
typeswitch ([ Expr ]Expr) as $fs:new
  case SequenceType return $fs:new
  default return fn:error()

4.13 Validate Expressions

[63 (XQuery)]    ValidateExpr    ::=    (("validate" "{") | ("validate" ValidationMode "{")) Expr "}"
[145 (XQuery)]    ValidationMode    ::=    "lax" | "strict"

Core Grammar

The Core grammar productions for validate are:

[49 (Core)]    ValidateExpr    ::=    (("validate" "{") | ("validate" ValidationMode "{")) Expr "}"
[108 (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 element or 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.

Normalization

A validate expression with no validation mode is normalized into a validate expression with the validation mode set to strict.

 
validate { Expr }
==
validate strict { [ Expr ]Expr }
 
validate ValidationMode { Expr }
==
validate ValidationMode { [ Expr ]Expr }

Static Type Analysis

Static typing of the validate operation is defined by the following rule. Note the use of a subtyping check to ensure that the type of the expression to validate is either an element or a well-formed document node (i.e., with only one root element and no text nodes). The type of the expression to validate may be a union of more than one element type. We apply the with mode judgment to each element type to determine the meaning of that element type with the given validation mode, which yields a new element type. The result type is the union over all new element types.

statEnv |- Expr : Type
statEnv |- Type <: (element | document { ElementType })
statEnv |- prime(Type) = ElementType1 ... ElementTypen
ElementType1 = element ElementName1? TypeSpecifier1?
···
ElementTypen = element ElementNamen? TypeSpecifiern?
statEnv |- ElementName1 ? with mode ValidationMode resolves to ElementType1
···
statEnv |- ElementNamen ? with mode ValidationMode resolves to ElementTypen
Type1 = ElementName1 | ... | ElementNamen

statEnv |- validate ValidationMode { Expr } : Type1

4.13.1 Validating an Element Node

Dynamic Evaluation

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 [Data Model Serialization], 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 [Data Model].

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 [E 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.

statEnv, dynEnv |- Expr => ElementValue1
ElementValue1 erases to ElementValue2
ElementValue2 = ElementName2 of type TypeName2 { Value };
statEnv |- ElementName2 with mode ValidationMode resolves to ElementType2
annotate as ElementType2 ( ElementValue2) => ElementValue3

dynEnv |- validate ValidationMode { Expr } => ElementValue3

4.13.2 Validating a Document Node

The rule for validating a document node is similar to that for validating an element node.

Dynamic Evaluation

statEnv dynEnv |- Expr => document { ElementValue1 }
document { ElementValue1 } erases to document { ElementValue2 }
ElementValue2 = ElementName2 of type TypeName2 { Value }
statEnv |- ElementName2 with mode ValidationMode resolves to ElementType2
annotate as document { ElementType2 } (document { ElementValue2 }) => document { ElementValue3 }

dynEnv |- validate ValidationMode { Expr } => document { ElementValue3 }

Dynamic Errors

The default rules for propogating errors, described in [3.3 Error Handling] apply to the validate expression.

4.14 Extension Expressions

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.

[64 (XQuery)]    ExtensionExpr    ::=    Pragma+ "{" Expr? "}"
[65 (XQuery)]    Pragma    ::=    "(#" S? QName PragmaContents "#)"
[66 (XQuery)]    PragmaContents    ::=    (Char* - (Char* '#)' Char*))

Core Grammar

The Core grammar productions for ExtensionExpr are:

[50 (Core)]    ExtensionExpr    ::=    Pragma+ "{" Expr? "}"
[51 (Core)]    Pragma    ::=    "(#" S? QName PragmaContents "#)"
[52 (Core)]    PragmaContents    ::=    (Char* - (Char* '#)' Char*))

Normalization

Extension expressions are normalized as extension expressions in the [XPath/XQuery] core.

 
[Pragma+ { Expr }]Expr
==
Pragma+ { [Expr]Expr }

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() }

Dynamic Evaluation

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 |- Some Pragma are recognized, yielding the implementation-defined value Value.

dynEnv |- Pragma+ { Expr } => Value

If none of the pragmas are recognized the dynamic semantics of an ExtensionExpression are the same as evaluating the given expression.

No Pragma is recognized.      dynEnv |- Expr => Value

dynEnv |- Pragma+ { Expr } => Value

Static Type Analysis

If at least one of the pragmas is recognized, the static semantics are implementation-defined.

If none of the pragmas are 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 corresponding static type errors.

statEnv |- Expr : Type1
statEnv |- Some Pragma are recognized, yielding the implementation-defined static type Type2.

statEnv |- Pragma+ { Expr } : Type2

statEnv |- Expr : Type1
statEnv |- No Pragma is recognized.

statEnv |- Pragma+ { Expr } : Type1

5 Modules and Prologs

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 and definitions that affect query processing. The Prolog can be used, for example, to define namespace prefixes, import type definitions from XML Schemas, and define functions and variables. Namespace declarations and schema imports always precede function definitions, as specified by the following grammar productions.

Query Module
[1 (XQuery)]    Module    ::=    VersionDecl? (MainModule | LibraryModule)
[3 (XQuery)]    MainModule    ::=    Prolog QueryBody
[4 (XQuery)]    LibraryModule    ::=    ModuleDecl Prolog
[6 (XQuery)]    Prolog    ::=    ((Setter | Import | NamespaceDecl | DefaultNamespaceDecl) Separator)* ((VarDecl | FunctionDecl | OptionDecl) Separator)*
[7 (XQuery)]    Setter    ::=    BoundarySpaceDecl | DefaultCollationDecl | BaseURIDecl | ConstructionDecl | OrderingModeDecl | EmptyOrderDecl | CopyNamespacesDecl
[8 (XQuery)]    Import    ::=    SchemaImport | ModuleImport
[9 (XQuery)]    Separator    ::=    ";"
[30 (XQuery)]    QueryBody    ::=    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

Core grammar production for the prolog are as follows.

Query Module
[1 (Core)]    Module    ::=    VersionDecl? (MainModule | LibraryModule)
[3 (Core)]    MainModule    ::=    Prolog QueryBody
[4 (Core)]    LibraryModule    ::=    ModuleDecl Prolog
[6 (Core)]    Prolog    ::=    ((Setter | Import | NamespaceDecl | DefaultNamespaceDecl) Separator)* ((VarDecl | FunctionDecl | OptionDecl) Separator)*
[7 (Core)]    Setter    ::=    DefaultCollationDecl | BaseURIDecl | ConstructionDecl | OrderingModeDecl | EmptyOrderDecl | CopyNamespacesDecl
[8 (Core)]    Import    ::=    SchemaImport | ModuleImport
[9 (Core)]    Separator    ::=    ";"
[29 (Core)]    QueryBody    ::=    Expr

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.

Prolog Declarations
[76 (Formal)]    PrologDeclList    ::=    (PrologDecl Separator)*
[77 (Formal)]    PrologDecl    ::=    NamespaceDecl
| DefaultNamespaceDecl
| DefaultCollationDecl
| BaseURIDecl
| SchemaImport
| ModuleImport
| VarDecl

The function []PrologDecl takes a prolog declaration and maps it into its equivalent declaration in the Core grammar.

 
[PrologDecl]PrologDecl
==
PrologDecl

The following auxiliary judgments are applied when 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:

PrologDeclList =>stat statEnv; PrologDeclList1

holds if the sequence of prolog declarations PrologDeclList yields the static environment statEnv and the normalized sequence of prolog declarations in the Core grammar.

The judgment:

statEnv1 |- PrologDecl =>stat statEnv2

holds if under the static environment statEnv1, the single prolog declaration PrologDecl yields the new static environment statEnv2.

Similary, the judgment:

dynEnv |- PrologDecl =>stat dynEnv1

holds if under the dynamic environment dynEnv, the single prolog declaration PrologDecl yields the new dynamic environment dynEnv1.

Normalization

Static Context Processing

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 the default static context.


() =>stat statEnvDefault; ()

The next rule interleaves normalization and static context processing. The result of static context processing and normalization is a static context and the normalized prolog declarations.

PrologDeclList =>stat statEnv1 ; PrologDeclList1
PrologDecl1 = [PrologDecl]PrologDecl
statEnv1 |- PrologDecl1 =>stat statEnv2 ; PrologDecl1

PrologDeclList PrologDecl ; =>stat statEnv2; PrologDeclList1 PrologDecl1 ;

Static Type Analysis

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 =>stat statEnv ; PrologDeclList1
statEnv |- [QueryBody]Expr : Type

PrologDeclList QueryBody : Type

Dynamic Context Processing

The rules for initializing the dynamic context are simpler. The first rule specifies for an empty sequence of prolog declarations, the initial dynamic environment is the default dynamic context.


() =>dyn dynEnvDefault

The second rule simply computes the dynamic environment by processing the prolog declarations in order.

PrologDeclList =>dyn dynEnv
dynEnv |- PrologDecl =>dyn dynEnv1

PrologDeclList PrologDecl ; =>dyn dynEnv1

Dynamic Evaluation

Dynamic evalution 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.

PrologDeclList1 =>dyn dynEnv
dynEnv |- [QueryBody]Expr => Value

PrologDeclList QueryBody => Value

5.1 Version Declaration

[2 (XQuery)]    VersionDecl    ::=    "xquery" "version" StringLiteral ("encoding" StringLiteral)? Separator

Core Grammar

The corresponding core grammar production is:

[2 (Core)]    VersionDecl    ::=    "xquery" "version" StringLiteral ("encoding" StringLiteral)? Separator

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. The Formal Semantics is specified for XQuery 1.0 and does not specify this static error formally.

5.2 Module Declaration

[5 (XQuery)]    ModuleDecl    ::=    "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).

Notation

We define a new judgment that maps a module's URI to the corresponding module's static environment:

URI =>module_statEnv statEnv

We also define a new judgment that maps a module's URI to the corresponding module's dynamic environment:

URI =>module_dynEnv dynEnv

Core Grammar

The corresponding core grammar production is:

[5 (Core)]    ModuleDecl    ::=    "module" "namespace" NCName "=" URILiteral Separator

Static Context Processing

The effect of a module declaration is to apply the static 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 URI, then computes the static context for the complete module.

(declare namespace NCName = String PrologDeclList) =>stat statEnv
module namespace NCName = String PrologDeclList

String =>module_statEnv statEnv

Note that the rule above and the rules for static processing of an "import module" declaration in [5.11 Module Import] are mutually recursive.

Dynamic Context Processing

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 URI, then computes the dynamic context for the complete module.

(declare namespace NCName = String PrologDeclList) =>stat dynEnv
module namespace NCName = String PrologDeclList

String =>module_dynEnv dynEnv

Note that the rule above and the rules for dynamic processing of an "import module" declaration in [5.11 Module Import] are mutually recursive.

5.3 Boundary-space Declaration

[11 (XQuery)]    BoundarySpaceDecl    ::=    "declare" "boundary-space" ("preserve" | "strip")

The xmlspace declaration is not specified formally as the Formal Semantics is defined on the Core language, which is an abstract, not concrete, syntax and is typically the result of parsing phase described in [3.2.1 Processing model].

5.4 Default Collation Declaration

[19 (XQuery)]    DefaultCollationDecl    ::=    "declare" "default" "collation" URILiteral

Core Grammar

The corresponding core grammar production is:

[18 (Core)]    DefaultCollationDecl    ::=    "declare" "default" "collation" URILiteral

Normalization

The default collation declaration is in the Core grammar, so no normalization rules are necessary.

Static Context Processing

The default collation declaration updates the collations environment of the static context. The collations environment is used by several functions in [Functions and Operators], but is otherwise not used in the Formal Semantics.

statEnv1 = statEnv + collations( String)

statEnv |- declare default collation String =>stat statEnv1

Dynamic Context Processing

The default collation declaration does not affect the dynamic context.


dynEnv |- declare default collation String =>dyn dynEnv

5.5 Base URI Declaration

[20 (XQuery)]    BaseURIDecl    ::=    "declare" "base-uri" URILiteral

Core Grammar

The corresponding core grammar production is:

[19 (Core)]    BaseURIDecl    ::=    "declare" "base-uri" URILiteral

Normalization

The base URI declaration is already in the Core grammar, so normalization rule is necessary.

Static Context Processing

A base URI declaration specifies the base URI property of the static context, which is used when resolving relative URIs within a module. A static error is raised if more than one base URI declaration is declared in a query prolog.

statEnv1 = statEnv + baseUri(String)

statEnv |- declare base-uri String =>stat statEnv1

Dynamic Context Processing

The base URI declaration does not affect the dynamic context.


dynEnv |- declare base-uri String =>dyn dynEnv

5.6 Construction Declaration

[25 (XQuery)]    ConstructionDecl    ::=    "declare" "construction" ("preserve" | "strip")

Core Grammar

The corresponding core grammar production is:

[24 (Core)]    ConstructionDecl    ::=    "declare" "construction" ("preserve" | "strip")

Normalization

The construction declaration is in the Core grammar, so no normalization rule is necessary.

Static Context Processing

The construction declaration modifies the construction mode in the static context.

statEnv1 = statEnv + constructionMode( ConstructionMode)

statEnv |- declare construction ConstructionMode =>stat statEnv1

Dynamic Context Processing

The construction declaration does not have any affect on the dynamic context.


dynEnv |- declare construction ConstructionMode =>dyn dynEnv

5.7 Ordering Mode Declaration

[14 (XQuery)]    OrderingModeDecl    ::=    "declare" "ordering" ("ordered" | "unordered")

Core Grammar

The corresponding core grammar production is:

[13 (Core)]    OrderingModeDecl    ::=    "declare" "ordering" ("ordered" | "unordered")

5.8 Empty Order Declaration

[15 (XQuery)]    EmptyOrderDecl    ::=    "declare" "default" "order" ("empty" "greatest" | "empty" "least")

Core Grammar

The corresponding core grammar production is:

[14 (Core)]    EmptyOrderDecl    ::=    "declare" "default" "order" ("empty" "greatest" | "empty" "least")

5.9 Copy-Namespaces Declaration

[16 (XQuery)]    CopyNamespacesDecl    ::=    "declare" "copy-namespaces" PreserveMode "," InheritMode
[17 (XQuery)]    PreserveMode    ::=    "preserve" | "no-preserve"
[18 (XQuery)]    InheritMode    ::=    "inherit" | "no-inherit"

Core Grammar

The corresponding core grammar production is:

[15 (Core)]    CopyNamespacesDecl    ::=    "declare" "copy-namespaces" PreserveMode "," InheritMode
[16 (Core)]    PreserveMode    ::=    "preserve" | "no-preserve"
[17 (Core)]    InheritMode    ::=    "inherit" | "no-inherit"

5.10 Schema Import

Schema Imports
[21 (XQuery)]    SchemaImport    ::=    "import" "schema" SchemaPrefix? URILiteral (("at" URILiteral) ("," URILiteral)*)?
[22 (XQuery)]    SchemaPrefix    ::=    ("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 [C 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 corresponding core grammar productions are.

Schema Imports
[20 (Core)]    SchemaImport    ::=    "import" "schema" SchemaPrefix? URILiteral (("at" URILiteral) ("," URILiteral)*)?
[21 (Core)]    SchemaPrefix    ::=    ("namespace" NCName "=") | ("default" "element" "namespace")

Normalization

Schema import declarations are in the Core grammar, so no normalization rules are necessary.

Notation

The following auxiliary judgments are used when processing schema imports.

The judgment:

statEnv1 |- Definition* =>type statEnv2

holds if under the static environment statEnv1, the sequence of type definitions Definition* yields the new static environment statEnv2.

The judgment:

statEnv1 |- Definition =>type statEnv2

holds if under the static environment statEnv1, the single definition Definition yields the new static environment statEnv2.

Static Context Processing

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 begins in [C.2 Schemas as a whole]. Each type definition in an imported schema is then added to the static environment.

Definition* = [schema String (at String)?]Schema
statEnv |- Definition* =>type statEnv1

statEnv |- import schema String (at String)? =>stat statEnv1

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.

Definition* = [schema String (at String)?]Schema
statEnv |- Definition* =>type statEnv1
statEnv2 = statEnv1 + namespace(NCName => (passive, String))

statEnv |- import schema namespace NCName = String =>stat statEnv2

Definition* = [schema String (at String)?]Schema
statEnv |- Definition* =>type statEnv1
statEnv2 = statEnv1 + default_elem_namespace( String (at String)?)

statEnv |- import schema default element namespace String =>stat statEnv2

An empty sequence of type definitions yields the input environment.


statEnv |- () =>type statEnv

Each type definition is added into the static environment.

statEnv |- Definition* =>type statEnv1
statEnv1 |- Definition1 =>type statEnv2

Definition1 Definition* =>type statEnv2

Each type, element, or attribute declaration is added respectively to the type, element and attribute declarations components of the static environment.

statEnv |- TypeName of elem/type expands to expanded-QName
statEnv1 = statEnv + typeDefn(expanded-QName => define type TypeName TypeDerivation )

statEnv |- define type TypeName TypeDerivation =>type statEnv1

statEnv |- ElementName of elem/type expands to expanded-QName
statEnv1 = statEnv + elemDecl(expanded-QName => define element ElementName Substitution? Nillable? TypeReference)

statEnv |- define element ElementName Substitution? Nillable? TypeReference =>type statEnv1

statEnv |- AttributeName of attr expands to expanded-QName
statEnv1 = statEnv + attrDecl(expanded-QName => define attribute AttributeName TypeReference)

statEnv |- define attribute AttributeName TypeReference =>type statEnv1

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.

Dynamic Context Processing

The schema import declarations do not affect the dynamic context.


dynEnv |- SchemaImport =>dyn dynEnv

5.11 Module Import

[23 (XQuery)]    ModuleImport    ::=    "import" "module" ("namespace" NCName "=")? URILiteral (("at" URILiteral) ("," URILiteral)*)?

Core Grammar

The corresponding core grammar production is:

Module Import
[22 (Core)]    ModuleImport    ::=    "import" "module" ("namespace" NCName "=")? URILiteral (("at" URILiteral) ("," URILiteral)*)?

Notation

The rules below depend on the following auxilliary functions,

The function fs:local-variables(statEnv, URI) 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, URI) returns all the function signatures 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.

Static Context Processing

During static context processing, the effect of an "import module" declaration is to extend the importing module's static context with the global variables (and their types) and the function signatures of the imported module. Module import is not transitive, therefore 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.

The first premise below "looks up" the static context of the imported module, as defined in [5.2 Module Declaration], then extends the input static context with the global variables and function signatures declared in the imported static context.

String =>module_statEnv statEnv2
statEnv3 = statEnv1(fs:local-variables(statEnv2, String1) + fs:local-functions(statEnv2, String1))

statEnv1 |- import module (namespace NCName =)? String1 (at String2)? =>stat statEnv3

Note that the rule above and the rules for processing a library module in [5.2 Module Declaration] above are mutually recursive.

Dynamic Context Processing

During dynamic context processing, the effect of an "import module" declaration is to extend the importing module's dynamic context with the global variables and the function definitions of the imported module. Each variable and function name is mapped to the special value #IMPORTED(URI) to indicate that the variable or function is defined in the imported module with the given URI.

Notation

The rules below depend on the following auxilliary judgments.

This judgment adds each variable explicitly declared in the imported module to the importing module's dynamic variable environment.

String =>module_dynEnv dynEnv2
dynEnv2 = dynEnv1 + varValue(expanded-QName => #IMPORTED(URI))
dynEnv2 ; URI |- (expanded-QName2, Type2) ··· (expanded-QNamen, Typen) =>import_variables dynEnv3

dynEnv1 ; URI |- (expanded-QName1, Type1) ··· (expanded-QNamen, Typen) =>import_variables dynEnv3

This judgment adds each function explicitly declared in the imported module to the importing module's dynamic function environment.

String =>module_dynEnv dynEnv2
dynEnv2 = dynEnv + funcDefn1((expanded-QName1(Type1,1, ..., Type1,n)) => #IMPORTED(URI))
dynEnv2 ; URI |- (expanded-QName2(Type2,1, ..., Type2,n)) ··· (expanded-QNamek(Typek,1, ..., Typek,n)) =>import_functions dynEnv3

dynEnv1 ; URI |- (expanded-QName1(Type1,1, ..., Type1,n)) ··· (expanded-QNamek(Typek,1, ..., Typek,n)) =>import_functions dynEnv3

The first premise below "looks up" the dynamic context of the imported module, as defined in [5.2 Module Declaration]. The auxilliary judgments =>import_variables and =>import_functions add each imported global variable and function name to the input dynamic context.

String =>module_dynEnv dynEnv2
dynEnv1 |- fs:local-variables(statEnv2, String1) =>import_variables dynEnv3
dynEnv3 |- fs:local-functions(statEnv2, String1) =>import_functions dynEnv4

statEnv1 |- import module (namespace NCName =)? String1 (at String2)? =>dyn statEnv4

Note that the rule above and the rules for processing a library module in [5.2 Module Declaration] above are mutually recursive.

5.12 Namespace Declaration

[10 (XQuery)]    NamespaceDecl    ::=    "declare" "namespace" NCName "=" URILiteral

Core Grammar

The corresponding core grammar production is:

[10 (Core)]    NamespaceDecl    ::=    "declare" "namespace" NCName "=" URILiteral

Normalization

The namespace declaration is in the Core grammar, so no normalization rules are necessary.

Static Context Processing

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.

statEnv1 = statEnv + namespace(NCName => (passive, String))

statEnv |- declare namespace NCName = String =>stat statEnv1

Dynamic Context Processing

The namespace declaration does not affect the dynamic context.


dynEnv |- declare namespace NCName =>dyn dynEnv

5.13 Default Namespace Declaration

[12 (XQuery)]    DefaultNamespaceDecl    ::=    (("declare" "default" "element") | ("declare" "default" "function")) "namespace" URILiteral

Core Grammar

The corresponding core grammar production is:

[11 (Core)]    DefaultNamespaceDecl    ::=    (("declare" "default" "element") | ("declare" "default" "function")) "namespace" URILiteral

Normalization

The default namespace declarations are in the Core grammar, so no normalization rules are necessary.

Static Context Processing

A default element namespace declaration changes the default element namespace prefix binding in the namespace component of the static environment. If the string literal is the empty string, the default element namespace is set to the null namespace.

statEnv1 = statEnv + default_elem_namespace(#NULL-NAMESPACE)

statEnv |- declare default element namespace = "" =>stat statEnv1

not(String = "")     statEnv1 = statEnv + default_elem_namespace( String)

statEnv |- declare default element namespace = String =>stat statEnv1

A default function namespace declaration changes the default function namespace prefix binding in the namespace component of the static environment. If the string literal is the empty string, the default function namespace is set to the null namespace.

statEnv1 = statEnv + default_function_namespace(#NULL-NAMESPACE)

statEnv |- declare default function namespace = "" =>stat statEnv1

not(String = "")     statEnv1 = statEnv + default_function_namespace( String)

statEnv |- declare default function namespace = String =>stat statEnv1

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.

Dynamic Context Processing

Default namespace declarations do not affect the dynamic context.


dynEnv |- DefaultNamespaceDecl =>dyn dynEnv

5.14 Variable Declaration

[24 (XQuery)]    VarDecl    ::=    "declare" "variable" "$" VarName TypeDeclaration? ((":=" ExprSingle) | "external")

Core Grammar

The corresponding core grammar production is:

[23 (Core)]    VarDecl    ::=    "declare" "variable" "$" VarName TypeDeclaration? ((":=" ExprSingle) | "external")

Normalization

Normalization of a variable declaration normalizes the variable and its corresponding expression, if it is present.

 
[ declare variable VarRef as SequenceType := Expr ]PrologDecl
==
declare variable VarRef as SequenceType := [Expr]Expr
 
[ declare variable VarRef as SequenceType external ]PrologDecl
==
declare variable VarRef as SequenceType external

Static Context Processing

A variable declaration updates the variable component of the static context by associating the given variable with a static type. If the variable declaration has a type declaration, the static type of the variable is simply the specified type.

statEnv |- VarRef of var expands to Variable
statEnv1 = statEnv + varType( Variable => [SequenceType]sequencetype)

statEnv |- declare variable VarRef as SequenceType (:= Expr | external) =>stat statEnv2

If a variable declaration does not have a type declaration but has an associated expression, then the static type of the variable is the static type of the expression.

statEnv |- Expr : Type
statEnv |- VarRef of var expands to Variable      statEnv1 = statEnv + varType( Variable => Type)

statEnv |- declare variable VarRef := Expr =>stat statEnv1

If an external variable declaration does not have a type declaration it is treated as if the type declaration was item()*.

statEnv |- VarRef of var expands to Variable
Type = [ item()* ]sequencetype
statEnv1 = statEnv + varType( Variable => Type)

statEnv |- declare variable VarRef := Expr =>stat statEnv1

Dynamic Context Processing

To evaluate a variable declaration, its associated expression is evaluated, and the dynamic context is updated with the variable bound to the resulting value.

dynEnv |- Expr => Value
statEnv |- VarRef of var expands to Variable
dynEnv1 = dynEnv + varValue( Variable => Value)

dynEnv |- declare variable VarRef as SequenceType (:= Expr | external) =>stat dynEnv1

Dynamic evaluation does not apply to externally defined variables. The evaluation environment must provide the values of external variables in the initial dynamic context (dynEnvDefault).


dynEnv |- declare variable VarRef as SequenceType external =>stat dynEnv

5.15 Function Declaration

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.

Function Definitions
[26 (XQuery)]    FunctionDecl    ::=    "declare" "function" QName "(" ParamList? (")" | (")" "as" SequenceType)) (EnclosedExpr | "external")
[27 (XQuery)]    ParamList    ::=    Param ("," Param)*
[28 (XQuery)]    Param    ::=    "$" VarName TypeDeclaration?

Core Grammar

The corresponding core grammar productions are.

Function Definitions
[25 (Core)]    FunctionDecl    ::=    "declare" "function" QName "(" ParamList? (")" | (")" "as" SequenceType)) (EnclosedExpr | "external")
[26 (Core)]    ParamList    ::=    Param ("," Param)*
[27 (Core)]    Param    ::=    "$" VarName TypeDeclaration?

Notation

The following auxiliary mapping rule is used for the normalization of parameters in function definitions: []Param.

Parameters without a declared typed are given the item* sequence type.

 
[VarRef]Param
==
VarRef as item*
 
[VarRef as SequenceType ]Param
==
VarRef as SequenceType

Normalization

The parameter list and body of a user-defined function are all normalized into Core expressions.

 
[ define function QName ( ParamList? ) as SequenceType EnclosedExpr ]PrologDecl
==
define function QName ( [ParamList?]Param ) as SequenceType [EnclosedExpr]Expr

If the return type of the function is not provided, it is given the item* sequence type.

 
[define function QName ( ParamList? ) EnclosedExpr ]PrologDecl
==
define function QName( [ParamList?]Param ) as item* [EnclosedExpr]Expr

Externally defined functions are normalized similarly.

 
[ define function QName ( ParamList? ) as SequenceType external]
==
define function QName( [ParamList?]Param ) as SequenceType external
 
[define function QName ( ParamList? ) external ]PrologDecl
==
define function [QName] ( [ParamList?]Param ) as item* external

Static Context Processing

Because functions are mutually referential, all function signatures must be defined in the static environment before static type analysis is applied to the function bodies. This rule also updates the local functions component of the static context to indicate the function is declared withtin the given module.

statEnv |- QName of func expands to expanded-QName
statEnv1 = statEnv + funcType(expanded-QName => ( [SequenceType1]sequencetype, ··· [SequenceTypen]sequencetype , [SequenceTyper]sequencetype))
statEnv2 = statEnv + funcType1(expanded-QName)

define function QName (VarRef1 as SequenceType1, ··· VarRefn as SequenceTypen ) as SequenceTyper ({ Expr } | external) =>stat statEnv2

Static Type Analysis

The static typing rules for function bodies follows normalization and processing of the static context. The typing rules below constructs a new environment in which each variable 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 type checking fails, a static error is raised. Otherwise, static typing of the function has no other effect, as function signatures are already inside the static environment.

statEnv + varType( VarRef1 : [SequenceType1]sequencetype ;...; VarRefn : [SequenceTypen]sequencetype ) |- Expr : Type
Type <: [SequenceTyper]sequencetype

statEnv |- define function QName (VarRef1 as SequenceType1, ··· VarRefn as SequenceTypen) as SequenceTyper { Expr }

The bodies of external functions are not available and therefore cannot by type checked. To ensure type soundness, the evaluation environment must guarantee that the value returned by the external function matches the expected return type.


statEnv |- define function QName ( VarRef1 as SequenceType1 , ··· VarRefn as SequenceTypen ) as SequenceTyper external

Dynamic Context Processing

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.

statEnv |- QName of func expands to expanded-QName
statEnv |- VarRef1 of var expands to Variable1      ···     statEnv |- VarRefn of var expands to Variablen
dynEnv' = dynEnv + funcDefn(expanded-QName => ( Expr , Variable1 , ··· Variablen))

dynEnv |- define function QName ( VarRef1 as SequenceType1 , ··· VarRefn as SequenceTypen ) as SequenceTyper { Expr } =>dyn dynEnv'

An external function declaration does not affect the dynamic environment. The evaluation environment must provide the implementation for externally defined functions.


dynEnv |- define function QName ( Variable1 as SequenceType1 , ··· Variablen as SequenceTypen ) as SequenceTyper external =>dyn dynEnv

The dynamic semantics of a function body are applied when the function is called and is described in [4.1.5 Function Calls].

5.16 Option Declaration

[13 (XQuery)]    OptionDecl    ::=    "declare" "option" QName StringLiteral

Core Grammar

The corresponding core grammar production is:

[12 (Core)]    OptionDecl    ::=    "declare" "option" QName StringLiteral

6 Conformance

The XQuery Formal Semantics is intended primarily as a component that can be used by [XQuery 1.0: A Query Language for XML], or a host language of [XML Path Language (XPath) 2.0]. 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.

6.1 Static Typing Feature

This specification normatively defines the static typing feature which can be used in [XQuery 1.0: A Query Language for XML] or a host language of [XML Path Language (XPath) 2.0]. The static typing feature is specified using the static typing judgment introduced in [3.2.3 Static typing judgment].

6.1.1 Static Typing Extensions

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.

statEnv |- Expr : Type
statEnv |- Type' <: Type

statEnv |- Expr :ext Type'

Note:

It is not recommended for a static typing extension to change the static typing behavior of expressions that specify a type explicitely (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.

7 Additional Semantics of Functions

This section defines a number of auxilliary functions required to define the formal semantics of [XPath/XQuery], and gives special static typing rules for some functions in [Functions and Operators].

7.1 Formal Semantics Functions

Introduction

This section gives the definition and semantics of functions that are used in the formal semantics but are not in [Functions and Operators]. Their dynamic semantics are defined in the same informal style as in the [Functions and Operators] document. The static semantics of some formal-semantics functions require custom typing rules.

7.1.1 The arithmetic operator pseudo-functions: fs:minus, fs:plus, fs:times, fs:idiv, fs:div, and fs:mod

These functions are overloaded placeholders with signatures and semantics as specified in the table in Appendix [B.2 Mapping of Overloaded Internal Functions].

7.1.2 The comparison pseudo-functions: fs:eq, fs:ne, fs:lt, fs:le, fs:gt, and fs:ge

These functions are overloaded placeholders with signatures and semantics as specified in the table of Appendix [B.2 Mapping of Overloaded Internal Functions].

7.1.3 The fs:convert-operand function

fs:convert-operand($actual as item *, $expected as xdt:anyAtomicType) as xdt:anyAtomicType ?

The formal-semantics function fs:convert-operand converts the operands of arithmetic and comparison operators as follows:

  1. If $actual is the empty sequence, returns the empty sequence.

  2. If statEnv.xpath1.0_compatibility is false and $actual is of type xdt:untypedAtomic, then

    1. if $expected is of type xdt:untypedAtomic, returns $actual cast to xs:string;

    2. if $expected is of numeric type, returns $actual cast to xs:double

    3. otherwise returns $actual cast to the type of $expected.

  3. If statEnv.xpath1.0_compatibility is true, and $actual is not of numeric type, then returns the value of the expression fn:number(fn:subsequence($actual,1,1)).

    Editorial note  
    New Issue: According to Michael Kay this converts too much (for example dates) to numbers in backwards compatibility mode. One fix would be to make the test inclusive yet sufficiently general to capture all the actual 1.0 cases, i.e., say something like "$actual : (node* | xdt:untypedAtomic* | xs:string*)". [Kris]
  4. Otherwise, the operand is returned unchanged.

Static Type Analysis

No conversion is needed for numeric (or empty) operands.

statEnv |- Expr1 : Type1
Type1 <: (xs:decimal|xs:float|xs:double)?

statEnv |- fs:convert-operand(Expr1, Expr2) : Type1

In XPath 1.0 backwards compatibility mode, if the static type of the operand is not a single numeric, the static type of the expression is the static type of the expression that extracts the first element of the operand and then converts that item to a double (by applying fn:number).

statEnv.xpath1.0_compatibility = true
statEnv |- Expr1 : Type1
not(Type1 <: (xdt:untypedAtomic|xs:decimal|xs:float|xs:integer)?)
statEnv |- fn:number(fn:subsequence(Expr1,1,1)) : xs:double

statEnv |- fs:convert-operand(Expr1, Expr2) : xs:double

Pairs of untyped atomic operands are converted to strings.

statEnv.xpath1.0_compatibility = false
statEnv |- Expr1 <: Type1      statEnv |- Type1 <: xdt:untypedAtomic ?
statEnv |- Expr2 : xdt:untypedAtomic

statEnv |- fs:convert-operand(Expr1, Expr2) : xs:string · quantifier (Type1)

When an untyped operand is paired with a numeric operand, it is converted to xs:double.

statEnv.xpath1.0_compatibility = false
statEnv |- Expr1 <: Type1      statEnv |- Type1 <: xdt:untypedAtomic ?
statEnv |- Expr2 : Type
statEnv |- Type <: fs:numeric

statEnv |- fs:convert-operand(Expr1, Expr2) : xs:double · quantifier (Type1)

Finally, an untyped atomic operand not dealt with by the above rules is converted to the type of the other operand.

statEnv.xpath1.0_compatibility = false
statEnv |- Expr1 <: Type1      statEnv |- Type1 <: xdt:untypedAtomic ?
statEnv |- Expr2 : Type2      statEnv |- Type2 <: xdt:anyAtomicType
not(Type2 <: (xdt:untypedAtomic|fs:numeric))

statEnv |- fs:convert-operand(Expr1, Expr2) : Type2 · quantifier(Type1)

7.1.4 The fs:convert-simple-operand function

fs:convert-simple-operand($actual as item *, $expected as xdt:anyAtomicType) as xdt:anyAtomicTypeAtomic *

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:

  • If statEnv.xpath1.0_compatibility is true and the $expected argument is of type xs:string, xs:string?, or a type derived from either type, then returns the value of fn:string($actual).

  • If statEnv.xpath1.0_compatibility is true and the $expected argument is xs:double, xs:double? (or a type derived from either type), then returns the value of fn:number($actual).

  • If statEnv.xpath1.0_compatibility is false, then for each item in $actual argument that is of type xdt:untypedAtomic, that item is cast to the type of the $expected argument, and the resulting sequence is returned.

  • Otherwise, return the $actual argument unchanged.

Static Type Analysis

The following static semantics rules correspond to the dynamic semantics rules given above.

statEnv.xpath1.0_compatibility = true
statEnv |- Expr1 : Type1
statEnv |- Expr2 : Type2
statEnv |- Type2 <: xs:string?

statEnv |- fs:convert-simple-operand(Expr1, Expr2) : xs:string

statEnv.xpath1.0_compatibility = true
statEnv |- Expr1 : Type1
statEnv |- Expr2 : Type2
statEnv |- Type2 <: xs:double ?

statEnv |- fs:convert-simple-operand(Expr1, Expr2) : xs:double

statEnv.xpath1.0_compatibility = false
statEnv |- Expr1 : Type1
statEnv |- Expr2 : Type2
statEnv |- Type2 <: xdt:anyAtomicType
Type3 = convert_untypedAtomic(prime(Type1), Type2)

statEnv |- fs:convert-simple-operand(Expr1, Expr2) : Type3 · quantifier(Type1)

7.1.5 The fs:distinct-doc-order function

fs: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.

Static Type Analysis

The fs:distinct-doc-order function expects a sequence of nodes as input and returns a sequence of prime types, which are defined in [8.4 Judgments for FLWOR and other expressions on sequences].

statEnv |- Expr : Type

statEnv |- fs:distinct-doc-order ( Expr ) : prime(Type) · quantifier(Type)

7.1.6 The fs:distinct-doc-order-or-atomic-sequence function

fs:distinct-doc-order-or-atomic-sequence($item as node *) 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.

Static Type Analysis

The fs:distinct-doc-order function expects either a sequence of nodes as input or a sequence of atomic values, and returns a sequence of prime types, which are defined in [8.4 Judgments for FLWOR and other expressions on sequences].

statEnv |- Expr : Type      Type <: node*

statEnv |- fs:distinct-doc-order-or-atomic-sequence ( Expr ) : prime(Type) · quantifier(Type)

statEnv |- Expr : Type      Type <: xdt:anyAtomicType*

statEnv |- fs:distinct-doc-order-or-atomic-sequence ( Expr ) : Type

7.1.7 The fs:item-sequence-to-node-sequence function

fs:item-sequence-to-node-sequence($items as item *) as node *

Th fs:item-sequence-to-node-sequence function converts a sequence of item values to nodes by applying the normative rules in Section 3.7.3.1 Computed Element ConstructorsXQ.

Notation

The type function items_to_nodes(Type) converts all atomic types in a type to the text type. The items_to_nodes function is defined by induction as follows.

items_to_nodes(AtomicTypeName)   =   text
items_to_nodes(NodeType)   =   Type1 & processing-instructions* & comment* if NodeType = document { Type1 }
items_to_nodes(NodeType)   =   NodeType otherwise
items_to_nodes(Type1 , Type2)   =   items_to_nodes(Type1) , items_to_nodes(Type2)
items_to_nodes(Type1 & Type2)   =   items_to_nodes(Type1) & items_to_nodes(Type2)
items_to_nodes(Type1 | Type2)   =   items_to_nodes(Type1) | items_to_nodes(Type2)
items_to_nodes(Type ?)   =   items_to_nodes(Type) ?
items_to_nodes(Type *)   =   items_to_nodes(Type) *
items_to_nodes(Type +)   =   items_to_nodes(Type) +

Static Type Analysis

statEnv |- Expr : Type

statEnv |- fs:item-sequence-to-node-sequence (Expr) : items_to_nodes(Type)

7.1.8 The fs:item-sequence-to-untypedAtomic function

fs:item-sequence-to-untypedAtomic($items as item *) as xdt:untypedAtomic

The fs:item-sequence-to-untypedAtomic function converts a sequence of item values to a string of type xdt:untypedAtomic by applying the normative rules in Section 3.7.3.2 Computed Attribute ConstructorsXQ.

In summary, each node is replaced by its string value. For each adjacent sequence of one or more atomic values returned by an enclosed expression, a string is constructed, containing the canonical lexical representation of all the atomic values, with a single blank character inserted between adjacent values.

Static Type Analysis

There are no special static typing rules for this function.

7.1.9 The fs:apply-ordering-mode function

fs:apply-ordering-mode($items as item()*) as item()*

Dynamic Evaluation

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 = ordered      dynEnv |- fn:unordered(Expr) => Value

dynEnv |- fs:apply-ordering-mode(Expr) => Value

Static Type Analysis

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:apply-ordering-mode(Expr) : 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:apply-ordering-mode(Expr) : prime(Type) · quantifier(Type)

7.1.10 The fs:to function

fs: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.

Dynamic Evaluation

If one of the input paramter 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 function call.

declare function fs:to($firstval as xs:integer?, $lastval as xs:integer?) as xs:integer* {
  if (fn:empty($lastval) or fn:empty($lastval)
  then ()
  else op:to($firstval,$lastval)
};

Static Type Analysis

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.

7.2 Standard functions with specific typing rules

Introduction

This section gives static typing rules for functions in [Functions and Operators] for which the standard typing rule based on the function's signature can be made more precise. All functions that are not mentioned here have static semantics as described by the generic static rule of section [4.1.5 Function Calls]. The rules in this section always give more precise type information than the generic rule.

7.2.1 The fn:abs, fn:ceiling, fn:floor, fn:round, and fn:round-half-to-even functions

Static Type Analysis

The typing rules for the fn:abs, fn:ceiling, fn:floor, fn:round, and fn:round-half-to-even functions promote their input type to the (least) base primitive numeric type from which the input type is derived. Parameters of type xdt:untypedAtomic are always promoted to xs:double. Instead of writing a separate judgment for each function, we write one rule with function variable F, which is one of the fn:abs, fn:ceiling, fn:floor, fn:round, or fn:round-half-to-even functions.

statEnv |- Expr : Type
statEnv |- Type <: xdt:anyAtomicType ?
convert_untypedAtomic(Type, xs:double) can be promoted to Type1
Type1 in { xs:integer xs:decimal, xs:float, xs:double }

statEnv |- F (Expr) : Type1 · quantifier(Type)

7.2.2 The fn:boolean function

Static Type Analysis

The fn:boolean function as described in the [Functions and Operators] document takes an empty sequence, a sequence of one or more nodes, or a singleton value of type xs:string, xdt:untypedAtomic or some numeric type. All other values are illegal.

statEnv |- Expr : Type
statEnv |- Type <: (empty | NodeType+ | xs:boolean | xs:string | xdt:untypedAtomic | fs:numeric)

statEnv |- fn:boolean(Expr) : xs:boolean

7.2.3 The fn:collection and fn:doc functions

Static Type Analysis

The fn:collection function as described in the [Functions and Operators] document, takes a string-valued expression, which denotes a URI, and returns a value.

If the fn:collection function has no parameter, the result type is given by the implementation for the default sequence if it exists.

statEnv |- Implementation-defined default sequence has type Type

statEnv |- fn:collection() : Type

If the argument to fn:collection is a literal String expression and that string is defined in statEnv.collectionType, then the result type is the type corresponding to the String in statEnv.collectionType.

statEnv |- statEnv.collectionType(String) = Type

statEnv |- fn:collection(String) : Type

Otherwise, if the argument is not a literal string or is a string but not defined in statEnv.collectionType, then we don't know anything about the URI, and the static type is node*:

statEnv |- statEnv.collectionType(String) not defined

statEnv |- fn:collection(Expr) : node *

statEnv |- not(Expr = String)

statEnv |- fn:collection(Expr) : node *

The static type of the fn:doc function has similar static rules, but, in addition, requires that the static type of the URI be any document:

statEnv |- statEnv.docType(String) = Type
statEnv |- statEnv.docType(String) = Type
statEnv |- Type <: document

statEnv |- fn:doc(String) : Type

Otherwise, if the argument is not a literal string or is not defined in the domain of statEnv.docType, then we don't know anything about the URI, and the static type is document:

statEnv |- statEnv.docType(String) not defined

statEnv |- fn:doc(Expr) : document

statEnv |- not(Expr = String)

statEnv |- fn:doc(Expr) : document

7.2.4 The fn:data function

Introduction

The fn:data function converts a sequence of items to a sequence of atomic values.

Notation

Infering the type for the fn:data function is done by applying the data on auxiliary judgment, using the same approach as for the XPath steps.

statEnv |- data on Type1 : Type2

Static Type Analysis

The general rule for fn:data is to apply the filter data on to the prime type of its argument type, then apply the quantifier to the result:

statEnv |- Expr : Type
statEnv |- data on prime(Type) : Type1

statEnv |- fn:data(Expr) : Type1 · quantifier(Type)

When applied to none, data on yields none.


statEnv |- data on none : none

When applied to empty, data on yields empty.


statEnv |- data on empty : empty

When applied to the union of two types, data on is applied to each of the two types. The resulting types are combined into a factored type. This rule is necessary because data on may return a sequence of atomic types.

statEnv |- data on Type1 : Type1'
statEnv |- data on Type2 : Type2'

statEnv |- data on (Type1|Type2) : prime(Type1'|Type2') · quantifier(Type1'|Type2')

When applied to an atomic type, data on simply returns the atomic type:

Type <: xdt:anyAtomicType

statEnv |- data on Type : Type

When applied to comment or processing instruction node types, data on returns xs:string

Type <: comment | processing-instruction

statEnv |- data on Type : xs:string

When applied to text, and document node types, data on returns xdt:untypedAtomic

Type <: text | document

statEnv |- data on Type : xdt:untypedAtomic

When applied to element node types with type annotationXQ xdt:untyped, the data on filter returns xdt:untypedAtomic.

statEnv |- ElementType type lookup (of type xdt:untyped)

statEnv |- data on ElementType : xdt:untypedAtomic

When applied to an attribute node type, the data on filter returns the attribute's simple type.

statEnv |- AttributeType type lookup (of type TypeName)
statEnv |- (of type TypeName) expands to Type

statEnv |- data on AttributeType : Type

When applied to an element type whose type annotationXQ denotes a simple type or a complex type of simple content, data on returns the element's simple type.

statEnv |- ElementType type lookup TypeReference
statEnv |- TypeReference expands to Type
Type <: (attribute *, Type1)      Type1 <: xdt:anyAtomicType*

statEnv |- data on ElementType : Type1

When applied to an element type whose type annotationXQ denotes a complex type of mixed content, the data on filter returns xdt:untypedAtomic.

statEnv |- ElementType type lookup (of type TypeName)
statEnv |- TypeName of elem/type expands to expanded-QName      statEnv.typeDefn(expanded-QName) = define type TypeName Derivation? Mixed { Type1? }

statEnv |- data on ElementType : xdt:untypedAtomic

The data on filter is not defined on any element type whose type annotationXQ denotes a complex type of complex content and therefore apply data on to such a node raises a static error.

Example

Consider the following variables and its corresponding static type.

    $x : (element price { attribute currency { xs:string }, xs:decimal }
         | element price_code { xs:integer })

Applying the fn:data function on that variable results in the following type.

    fn:data($x) : (xs:decimal | xs:integer)

Because the input type is a choice, applying the data on filter results in a choice of simple types for the output of the fn:data function.

7.2.5 The fn:distinct-values function

Static Type Analysis

The fn:distinct-values function expects a sequence of atomic values as input and returns a sequence of prime types, which are defined in [8.4 Judgments for FLWOR and other expressions on sequences].

statEnv |- Expr : Type
statEnv |- Type <: xdt:anyAtomicType*

statEnv |- fn:distinct-values(Expr) : prime(Type) · quantifier(Type)

7.2.6 The fn:unordered function

Static Type Analysis

The static semantics for unordered uses the auxiliary type functions prime(Type) and quantifier(Type); which are defined in [8.4 Judgments for FLWOR and other expressions on sequences]. The type of each argument is determined, and then prime(.) and quantifier(.) are applied to the sequence type (Type1, Type2).

statEnv |- Expr1 : Type1

statEnv |- fn:unordered(Expr1) : prime(Type1) · quantifier(Type1)

7.2.7 The fn:error function

Static Type Analysis

The fn:error function always has the none type.


statEnv |- fn:error() : none

statEnv |- Expr : xs:QName

statEnv |- fn:error(Expr) : none

statEnv |- Expr1 : xs:QName?     statEnv |- Expr2 : xs:string

statEnv |- fn:error(Expr1,Expr2) : none

statEnv |- Expr1 : xs:QName?     statEnv |- Expr2 : xs:string

statEnv |- fn:error(Expr1,Expr2,Expr3) : none

7.2.8 The fn:min, fn:max, fn:avg, and fn:sum functions

Static Type Analysis

The dynamic evaluation rules for the fn:min, fn:max, and fn:avg convert any item of type xdt:untypedAtomic in the input sequence to xs:double, then attempt to promote all values in the input sequence to values that are comparable. The static typing rules reflect the dynamic rules.

Semantics

The type function convert_untypedAtomic takes a prime type and converts all occurrences of the type xdt:untypedAtomic to a target type. It is defined by induction as follows.

convert_untypedAtomic(xdt:untypedAtomic, Type)   =   Type
convert_untypedAtomic(FormalItemType, Type)   =   FormalItemType (FormalItemType is not xdt:untypedAtomic)
convert_untypedAtomic(empty, Type)   =   empty
convert_untypedAtomic(none, Type)   =   none
convert_untypedAtomic(Type1 | Type2, Type)   =   convert_untypedAtomic(Type1, Type) | convert_untypedAtomic(Type2, Type)

The function aggregate_quantifier converts the input type quantifier zero-or-more or zero-or-one to the result type quantifier zero-or-one, and converts the input type quantifier one or one-or-more, to the result type quantifier one.

aggregate_quantifier(?)   =   ?
aggregate_quantifier(*)   =   ?
aggregate_quantifier(1)   =   1
aggregate_quantifier(+)   =   1

Now we can define the static typing rules for the aggregate functions. First, the input type is converted to a prime type. Second, the type function convert_untypedAtomic is applied to the prime type, yielding a new prime type, in which occurrences of xdt:untypedAtomic are converted to xs:double. Third, the judgment can be promoted to is applied to the new prime type and a target type T. The result type is T combined with the aggregate quantifier of the input type.

Instead of writing a separate judgment for each function and target type, we write one rule with function variable F and target variable T. When the function variable F is fn:min or fn:max, the target type T must be one of xs:string, xs:integer, xs:decimal, xs:float, xs:double, xdt:yearMonthDuration, or xdt:dayTimeDuration . When the function variable F is fn:avg, the target type T must be one of xs:decimal, xs:float, xs:double, xdt:yearMonthDuration, or xdt:dayTimeDuration .

statEnv |- Expr : Type
Type1 = convert_untypedAtomic(prime(Type), xs:double)
Type1 can be promoted to T

statEnv |- F (Expr) : Type1 · aggregate_quantifier(quantifier(Type))

The static typing rules for fn:sum are similar to those for the aggregate functions above, in which T must be one of xs:integer, xs:decimal, xs:float, xs:double, xdt:yearMonthDuration, or xdt:dayTimeDuration .

The fn:sum function has two forms. The first form takes two arguments: The first argument is the input sequence and the second argument is the value that should be returned if input sequence is empty. In this case, the result type is the union of the target type T and the type of the second argument.

statEnv |- Expr1 : Type1
Type3 = convert_untypedAtomic(prime(Type1), xs:integer)
Type3 can be promoted to T
statEnv |- Expr2 : Type2      statEnv |- Type2 <: xdt:anyAtomicType ?

statEnv |- fn:sum (Expr1, Expr2) : T | Type2

The second form of fn:sum takes one argument, with an implicit second argument of the integer value 0. In this case, the result type is the union of target type T and xs:integer.

statEnv |- Expr1 : Type1
Type3 = convert_untypedAtomic(prime(Type1), xs:integer)
Type3 can be promoted to T

statEnv |- fn:sum (Expr1) : T | xs:integer

7.2.9 The fn:remove function

Static Type Analysis

The typing rules for the fn:remove function returns the factored type of the function's input sequence.

statEnv |- Expr : Type
statEnv |- Expr1 : xs:integer

statEnv |- fn:remove(Expr, Expr1) : : prime(Type) · quantifier(Type)?

7.2.10 The fn:reverse function

Static Type Analysis

The typing rules for the fn:reverse function returns the factored type of the function's input sequence.

statEnv |- Expr : Type

statEnv |- fn:reverse(Expr) : : prime(Type) · quantifier(Type)

7.2.11 The fn:subsequence function

The fn:subsequence function has special typing rules when its second argument is the numeric literal value 1 or the built-in variable $fs:last. These rules provide better typing for path expressions such as Expr[1] and Expr[fn:last()].

Static Type Analysis

If the type of the input expression has exactly one or one-or-more items, then the type inferred for fn:subsequence is the prime type of the input type.

statEnv |- Expr : Type      quantifier(Type) in { 1, + }

statEnv |- fn:subsequence(Expr, 1, 1) : prime(Type)

The same rule applies when the last item in the input sequence is selected.

statEnv |- Expr : Type      quantifier(Type) in { 1, + }

statEnv |- fn:subsequence(Expr, $fs:last, 1) : prime(Type)

If the type of the input expression has zero or more items, then fn:subsequence, when selecting the first item, has zero-or-one of the prime type of the input type.

statEnv |- Expr : Type      quantifier(Type) in { * }

statEnv |- fn:subsequence(Expr, 1, 1) : prime(Type) ?

The same rule applies when the last item in the input sequence is selected.

statEnv |- Expr : Type      quantifier(Type) in { * }

statEnv |- fn:subsequence(Expr, $fs:last, 1) : prime(Type) ?

The last rule applies to all other applications of the fn:subsequence function.

statEnv |- Expr : Type
statEnv |- Expr1 : xs:double      statEnv |- Expr2 : xs:double

statEnv |- fn:subsequence(Expr, Expr1, Expr2) : prime(Type') · quantifier(Type')

7.2.12 The op:union, op:intersect, and op:except operators

Static Type Analysis

The static semantics for op:union uses the auxiliary type functions prime(Type) and quantifier(Type); which are defined in [8.4 Judgments for FLWOR and other expressions on sequences]. The type of each argument is determined, and then prime(.) and quantifier(.) are applied to the sequence type (Type1, Type2).

statEnv |- Expr1 : Type1      statEnv |- Expr2 : Type2

statEnv |- op:union(Expr1, Expr2) : prime(Type1 , Type2) · quantifier(Type1 , Type2)

The static semantics of op:intersect is analogous to that for op:union. Because an intersection may be empty, the result type is optional.

statEnv |- Expr1 : Type1
statEnv |- Expr2 : Type2

statEnv |- op:intersect(Expr1, Expr2) : prime(Type1, Type2); · quantifier(Type1,Type2); · ?

The static semantics of op:except follows. The type of the second argument is ignored as it does not contribute to the result type. As with op:intersect, the result of op:except may be the empty sequence.

statEnv |- Expr1 : Type1

statEnv |- op:except(Expr1, Expr2) : prime(Type1) · quantifier(Type1) · ?

7.2.13 The fn:zero-or-one, fn:one-or-more, and fn:exactly-one functions

The functions fn:zero-or-one, fn:one-or-more, and fn:exactly-one check that the cardinality of a sequence is in the expected range. They are useful to override the static type inferred for a given query. For example, in the following query, the user may know that all ISBN numbers are unique and therefore that the function always return at most one book element. However, the static typing feature cannot infers a precise enough type and will return a static type error at compile time.

  declare function book_with_isbn($isbn as xs:string) as schema-element(book)? {
    //book[@isbn=$isbn]
  }

In that query, the fn:zero-or-one function can be used to tell the type system that the cardinality is known to be zero or one.

  declare function book_with_isbn($isbn as xs:string) as schema-element(book)? {
    fn:zero-or-one(//book[@isbn=$isbn])
  }

Static Type Analysis

The static typing rules for those functions always infer a type with the cardinality indicated by that function.

statEnv |- Expr : Type

statEnv |- fn:zero-or-one(Expr) : prime(Type)?

statEnv |- Expr : Type

statEnv |- fn:one-or-more(Expr) : prime(Type)+

statEnv |- Expr : Type

statEnv |- fn:exactly-one(Expr) : prime(Type)

8 Auxiliary Judgments

This section defines auxiliary judgments used in defining the formal semantics. Many auxiliary judgments are used in both static and dynamic inference rules. Those auxiliary judgments that are used in only the static or dynamic semantics are labeled as such.

8.1 Judgments for accessing types

Introduction

This section defined several auxiliary judgments to access components of the [XPath/XQuery] type system. The first two judgements (derives from and substitutes for) are used to access the type and element name hierarchies in an XML Schema. The other judgments (name lookup, type lookup, extended by, adjusts to and expands to) are used to lookup the meaning of element or attribute types from the schema. These judgments are used in many expressions, notably in the specification of type matching (See [8.3 Judgments for type matching]), validation (See [E.1 Judgments for the validate expression]), and the static semantics of step expressions (See [8.2 Judgments for step expressions and filtering]).

8.1.1 Derives from

Notation

The judgment

statEnv |- TypeName derives from TypeName

holds when the first type name derives from the second type name. This judgment formalizes the definition of the derives-from function in Section 2.5.4 SequenceType MatchingXQ.

Example

For example, assuming the extended XML Schema given in section [2.4.5 Example of a complete Schema], then the following judgments hold.

  USAddress            derives from  xs:anyType
  NYCAddress           derives from  USAddress
  NYCAddress           derives from  xs:anyType
  xsd:positiveInteger  derives from  xsd:integer
  xsd:integer          derives from  xs:anySimpleType
  fs:anon3             derives from  xsd:positiveInteger
  fs:anon3             derives from  xsd:integer
  fs:anon3             derives from  xs:anySimpleType
  fs:anon3             derives from  xs:anyType

Note

Derivation is a partial order. It is reflexive and transitive by the definition below. It is asymmetric because no cycles are allowed in derivation by restriction or extension.

Semantics

This judgment is specified by the following rules.

Some rules have hypotheses that simply list a type, element, or attribute declaration.

Every type name derives from itself.


statEnv |- TypeName derives from TypeName

Every type name derives from the type it is declared to derive from by restriction or extension.

statEnv |- TypeName of elem/type expands to expanded-QName
statEnv.typeDefn(expanded-QName) => define type TypeName extends BaseTypeName Mixed? { Type? }

statEnv |- TypeName derives from BaseTypeName

statEnv |- TypeName of elem/type expands to expanded-QName
statEnv.typeDefn(expanded-QName) => define type TypeName restricts BaseTypeName Mixed? { Type? }

statEnv |- TypeName derives from BaseTypeName

The above rules all require that the type names be defined in the static context, but [XPath/XQuery] permits references to "unknown" type names, i.e., type names that are not defined in the static context. An unknown type name might be encountered, if a module in which the given type name occurs does not import the schema in which the given type name is defined. In this case, an implementation is allowed (but is not required) to provide an implementation-dependent mechanism for determining whether the unknown type name is the same as or derived by restriction from the expected type name. The following rule formalizes this implementation dependent mechanism.

"The implementation is able to determine that TypeName1 is derived by restriction from TypeName2."

statEnv |- TypeName1 derives from TypeName2

The derivation relation is transitive.

statEnv |- TypeName1 derives from TypeName2      statEnv |- TypeName2 derives from TypeName3

statEnv |- TypeName1 derives from TypeName3

8.1.2 Substitutes for

The substitutes judgment is used to know whether an element name is in the substitution group of another element name.

Notation

The judgment

statEnv |- ElementName substitutes for ElementName

holds when the first element name substitutes for the second element name.

Example

For example, assuming the extended XML Schema given in section [2.4.5 Example of a complete Schema], then the following judgments hold.

  usaddress  substitutes for  address
  nyaddress  substitutes for  usaddress
  nyaddress  substitutes for  address

Note

Substitution is a partial order. It is reflexive and transitive by the definition below. It is asymmetric because no cycles are allowed in substitution groups.

Semantics

The substitutes judgment for element names is specified by the following rules.

Every element name substitutes for itself.


statEnv |- ElementName substitutes for ElementName

Every element name substitutes for the element it is declared to substitute for.

statEnv |- ElementName of elem/type expands to expanded-QName
statEnv.elemDecl(expanded-QName) => define element ElementName substitutes for BaseElementName Nillable? TypeReference

statEnv |- ElementName substitutes for BaseElementName

Substitution is transitive.

statEnv |- ElementName1 substitutes for ElementName2      statEnv |- ElementName1 substitutes for ElementName3

statEnv |- ElementName1 substitutes for ElementName3

8.1.3 Element and attribute name lookup (Dynamic)

The name lookup judgment is used in the definition of the matches judgment, which takes a value and a type and determines whether the value matches, or is an instance of, the given type. Both name lookup and matches are used in the dynamic semantics.

The name lookup judgment takes an element(attribute) name (derived from a node value) and an element(attribute) type and if the element(attribute) name matches the corresponding name in the element(attribute) type, the judgment yields the type's corresponding type reference and for elements, its nillable property.

Notation

The judgment

statEnv |- ElementName name lookup ElementType yields Nillable? TypeReference

holds when the given element name matches the given element type and requires that the element be nillable as indicated and have the given type reference.

Example

For example, assuming the extended XML Schema given in section [2.4.5 Example of a complete Schema], then the following judgments hold.

  comment    name lookup element comment                          yields of type xsd:string
  size       name lookup element size nillable of type xs:integer yields nillable of type xsd:string
  apt        name lookup element apt                              yields of type fs:anon3
  nycaddress name lookup element address                          yields of type NYCAddress

Note that when the element name is in a substitution group, the name lookup returns the type name corresponding to the original element name (here the type NYCAddress for the element nycaddress, instead of Address for the element address).

Semantics

This judgment is specified by the following rules.

If the element type is a reference to a global element, then name lookup yields the type reference in the element declaration for the given element name. The given element name must be in the substitution group of the global element.

statEnv |- ElementName1 substitutes for ElementName2
statEnv |- ElementName1 of elem/type expands to expanded-QName1
statEnv.elemDecl(expanded-QName1) => define element ElementName1 Substitution? Nillable? TypeReference

statEnv |- ElementName1 name lookup element ElementName2 yields Nillable? TypeReference

If the given element name matches the element name in the element type, and the element type contains a type reference, then name lookup yields that type reference.


statEnv |- ElementName name lookup element ElementName Nillable? TypeReference yields Nillable? TypeReference

If the element type has no element name but contains a type reference, then name lookup yields the type reference.


statEnv |- ElementName name lookup element TypeReference yields TypeReference

If the element type has no element name and no type reference, then name lookup yields xs:anyType.


statEnv |- ElementName name lookup element yields of type xs:anyType

Notation

The judgment

statEnv |- AttributeName name lookup AttributeType yields TypeReference

holds when matching an attribute with the given attribute name against the given attribute type matches the type reference.

Example

For example, assuming the extended XML Schema given in section [2.4.5 Example of a complete Schema], then the following judgments hold.

  orderDate  name lookup  attribute orderDate of type xsd:date  yields  of type xsd:date?
  orderDate  name lookup  attribute of type xsd:date            yields  of type xsd:date?

Semantics

This judgment is specified by the following rules.

If the attribute type is a reference to a global attribute, then name lookup yields the type reference in the attribute declaration for the given attribute name.

statEnv.attrDecl(AttributeName) => define attribute AttributeName TypeReference

statEnv |- AttributeName name lookup attribute AttributeName yields TypeReference

If the given attribute name matches the attribute name in the attribute type, and the attribute type contains a type reference, then name lookup yields that type reference.


statEnv |- AttributeName name lookup attribute AttributeName TypeReference yields TypeReference

If the attribute type has no attribute name but contains a type reference, then name lookup yields the type reference.


statEnv |- AttributeName name lookup attribute TypeReference yields TypeReference

If the attribute type has no attribute name and no type reference, then name lookup yields xs:anySimpleType.


statEnv |- AttributeName name lookup attribute yields of type xs:anySimpleType

8.1.4 Element and attribute type lookup (Static)

The type lookup judgments are used to obtain the appropriate type reference for an attribute or element.

Notation

The judgment

statEnv |- ElementType type lookup Nillable? TypeReference

holds when the element type is optionally nillable and has the given type reference.

Semantics

The element type lookup judgments are specified by the following rules.

A reference to a global element yields the type reference in the global element declaration with the given element name.

statEnv |- ElementName of elem/type expands to expanded-QName
statEnv.elemDecl(expanded-QName) => define element ElementName Substitution? Nillable? TypeReference

statEnv |- element ElementName type lookup Nillable? TypeReference

If the element name is not defined, i.e., it is not declared in the in-scope schema definitions, then the element's default type is xdt:untyped.

statEnv |- ElementName of elem/type expands to expanded-QName
statEnv.elemDecl(expanded-QName) undefined

statEnv |- element ElementName type lookup Nillable? xdt:untyped

In the case of a local element type, type lookup yields the corresponding type reference.


statEnv |- element ElementName Nillable? TypeReference type lookup Nillable? TypeReference

If the element type has no element name but contains a type reference, then type lookup yields that type reference.