SPECIF

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