Syntax
-----

t :=                    TERMS
     (t)                Disambiguation parentheses
     ()                 Empty sequence
     t,t                Concatenation
     s[t]               Element
     t|t                Alternation
     t*                 Repetition
     t+                 Non-empty repetition
     t?                 Optional
     /t                 Children
     <t : t : t>        Test
     X                  Variable

s :=                    TAG SPECIFICATIONS
     a                  This tag
     _                  Any tag
     {a|...|a}          One of these tags
     {^a|...|a}         Any other tag    


p :=                    PROGRAM
     s ... s            Phrases

s :=                    PHRASES
     X = t              Definition
     #check E:T->T      Type-checking
     #run E(V)          Evaluation


a, X : Identifiers

Comments: /* ... */

All the variables that appear in terms must be defined in the
program. Multiple definitions for the same variable are not allowed.

The categories V (values), T (types) and E (expressions) are
subcategories of terms, defined below.


Values
------

Values represent fragments of XML documents, that is, sequences of elements.
They are a subcategorie of terms, where only the following constructions
are allowed:

V :=                    VALUES
     (V)                Disambiguation parentheses
     ()                 Empty sequence
     V,V                Concatenation
     N                  Element
     X                  Variable

N :=                    ELEMENTS
     a[V]               Element (with a fixed tag)
   

where variables must resolve to values. Moreover, values are finite trees
(a variable cannot appear in the unfolding of its own definition).

We identify values modulo the following equations:

V1,(V2,V3) = (V1,V2),V3
V,() = (),V = V


Types
-----

Types represent sets of values.
They are a subcategorie of terms, where only the following constructions
are allowed:

T :=                    TYPES
     (T)                Disambiguation parentheses
     ()                 Empty sequence
     T,T                Concatenation
     s[T]               Element
     T|T                Alternation
     T*                 Repetition
     T+                 Non-empty repetition
     T?                 Optional
     X                  Variable

where variables must resolve to types. Moreover, recursion must be
guarded: a variable must be separated from its use (in the unfolding
of its definition) by at least one Element constructor. E.g.
"X = a[],X" is not allowed, but "X = a[X,X]" is.

Note that any value is also a type.


Expressions
-----------

Expressions represent total and determinisic transformations from
values to values.  Types represent sets of values.  They are a
subcategorie of terms, where only the following constructions are
allowed:

E :=                    EXPRESSIONS
     (E)                Disambiguation parentheses
     ()                 Empty sequence
     E,E                Concatenation
     a[E]               Element
     _[E]               Copy element
     E*                 Repetition
     /E                 Children
     !E                 Next
     <T : E : E>        Test
     X                  Variable

where variables must resolve to expressions. Moreover, recursion must be
guarded: a variable must be separated from its use (in the unfolding
of its definition) by at least one Children or Next constructor. E.g.
"X = a[X]" is not allowed, but "X = /X" is.

Note that any value is also an expression.


Semantics of types
------------------

The following equations define the intepretation of types as sets
of values:

<(T)>         = <T>
<()>          = { () }
<T1,T2>       = { V1,V2  |  V1 in <T1> and V2 in <T2> }
<s[T]>        = { s[V] | V in <T> }
<T1|T2>       = { V  |  V in <T1> or  V <T2> }
<T?>          = <T> union { () }
<T*>          = { V1,...,Vn | n >= 0 and forall i. Vi in <T> }
<T+>          = { V1,...,Vn | n >= 1 and forall i. Vi in <T> }
<X>           = <T> where T is the definition for X


Semantics of expressions
------------------------

The following equations define the semantics of expressions. We
write E(V) for the result of applying E to V.

(E)(V)        = E(V)
()(V)         = ()
E1,E2(V)      = E1(V),E2(V)
a[E](V)       = a[E(V)]
_[E](V)       = a[E(V)] if V=a[V1],V2
              = ()      if V=()
E*(V)         = E(V),!E(V)
/E(V)         = E(V1)   if V=a[V1],V2
              = ()      if V=()
!E(V)         = E(V2)   if V=a[V1],V2
              = ()      if V=()
<T:E1:E2>(V)  = E1(V)   if N in T
                E2(V)   otherwise
X(V)          = E(V) where E is the definition for X

As a consequence, a value V can be seen as an expression which transform any
value to V:

V1(V2)        = V1


Note that E* is equivalent to a fresh variable X where X is defined by
X=E,!X.

Definitions
-----------

All the definitions for variables are parsed before other phrases.
They are all mutually recursive, and the same variable can be used in
different contexts with several kinds (as a value, a type, or an
expression).


Type-checking
-------------

The phrase " #check E:T1->T2" checks whether the expression E maps
all the values of type T1 to values of type T2. If this is the case,
the program prints "Ok!". Otherwise, it displays an input value
(in T1) and the corresponding output (not in T2) that exhibits the problem.


Evaluation
----------

The phrase "#run E(V)" computes and displays the result E(V).