Syntax of types:
T ::=
| () Empty sequence
| a[T],T Element
| _[T],T Element with any tag
| T & T Intersection
| T | T Union
| T - T Difference
| T,T Sequence
| T* Repetition
| T+ Non-empty repetition
| Any Universal type (any sequence)
| Empty Empty type
| X Recursion variable (identifier starting with uppercase)
| (T) Syntactical grouping
Loops in types must cross an element constructor. Boolean connectives
& and - cannot appear under regular expression constructors
(sequence, repetition).
Syntax of transducers:
E ::=
| () Empty sequence
| a[E],E Element
| _[E],E Element, copy tag from the input
| /E Move to the sequence of children of the first element
| !E Move to the next element
| if E in T then E else E Conditional
| let B in E Local binding, call by value
| letn B in E Local binding, call by name
| rand(T) Non-deterministic choice in T
| (E;E) Composition
| x Local variable (identifier starting with lowercase)
| X(E1;...;En) Recursive call (identifier starting with uppercase)
| X Recursive call without argument
| Copy Copy the input
| Error Failure
| (E) Syntactical grouping
B ::= x = E and ... and x = E
Loops in transducers must cross a ! or / constructor. There can be no loop
between the left-hand side E2 of composition (E1;E2) and the composition
itself. Moreover, E1 must be closed (no free variables).
The /E, !E and _[E],E transducers fail when the input is the empty sequence.
Values V are defined as the subset of transducers where only the
empty sequence, the element and the concatenation constructors are allowed.
Syntax of phrases:
P ::= type X = T Type definition
| expr X(x1;...;xn) = E Transducer definition
| expr X = E Transducer definition without argument
| check E : T -> T Type-checking
| infer E in T Backward type-inference
| eval E Evaluation (starting from the empty value)
A script is simply a sequence of phrases. All the definitions
are mutually recursive. The commands are evaluated in sequence.
Semantics of transducers:
The evaluation of a transducer E on a value V under an environment G
is defined below as an interpreter. The environment is a mapping from
variables to non empty sets of values. The interpreter is
non-deterministic because of the rand(T) case. The result is either a
value or Error, which behaves as a globally uncaught exception in the
evaluator.
eval(G, (), V) = ()
eval(G, (a[E1],E2), V) = a[eval(G,E1,V)],eval(G,E2,V)
eval(G, (_[E1],E2), V=(a[V1],V2)) = a[eval(G,E1,V)],eval(G,E2,V)
eval(G, (_[E1],E2), ()) = Error
eval(G, /E, (a[V1],V2)) = eval(G,E,V1)
eval(G, /E, ()) = Error
eval(G, !E, (a[V1],V2)) = eval(G,E,V2)
eval(G, !E, ()) = Error
eval(G, if E in T then E1 else E2, V) = eval(G,E1,V) if eval(G,E,V) is in T
= eval(G,E2,V) otherwise
eval(G, let x1 = E1 ... and xn = En in E, V) =
eval(G+(xi |-> {eval(G,Ei,V)}), E, V)
eval(G, let x1 = E1 ... and xn = En in E, V) =
eval(G+(x |-> Eval(G,Ei,V)), E, V)
eval(G, rand(T), V) = a random value in T
eval(G, (E1;E2)), V) = eval(G,E2,eval(G,E1,V))
eval(G, x, V) = a rand value in G(x)
eval(G, Copy, V) = V
eval(G, Error, V) = Error
where Eval(G,E,V) is the set of all possible results for eval(G,E,V).
Recursive call are expanded. If the declaration for X is:
expr X(x1;...;xn) = E
then the expression X(E1;...;En) is equivalent to
let x1 = E1 and ... and xn = n in E