Go up to 5 Syntax Extensions
Go forward to 5.2 Extended Syntax for Numbers
5.1 Extended Syntax for Functions on Argument Lists
In a datatype for lists one would like to write a list consisting of
four items i_{1}, i_{2}, i_{3}, and i_{4}
i_1 :: i_2 :: i_3 :: i_4 :: nil
(which is a possible notation in our specification of lists in
[RM99]) by a shorter construct like
[i_1, i_2, i_3, i_4].
For this purpose we propose an extension of the CASLsyntax which the
parser can easily translate into standard CASL. We demonstrate this
extension first on our datatype for lists of [RM99]:
 spec
 GenerateList
[Elem with sort Elem] =
 free
 types
List[Elem]  ::=  nil  sort NonEmptyList[Elem];

NonEmptyList[Elem]  ::= 
__ :: __ (first : Elem; rest : List[Elem])

 op
 __ :: __: Elem × List[Elem] > List[Elem] %right
assoc
 end
In this setting we suggest to declare the metafunction [ __ ]:
Elem^{*} > List[Elem] as follows:
 spec
 List[Elem] =
 GenerateList[Elem]
 then

 type
 List[Elem]::=
nil  __::__(Elem; List[Elem]),

brackets [ __ ] 
 end
Thus this notation is a special datatype declaration^{7} for a sort s, which consists of two
alternatives: the first is a constant const of this type, while the
second is a constructor f with exactly two components which both are
sorts (i.e. we do not care about the definition of selectors at this
point). The first component is an arbitrary sort t, the second sort
has to be s. After the keyword brackets the syntax of the
function is declared. For simplicity we suggest that the function name
is a pair of brackets combined with any character c, which is not a
bracket,
i.e. {c __ c}, or
[c __ c].
The syntax translation [ [ ] ] of the operation
t_{1} __ t_{2} : t^{*} ~> s,
where ~> = > if f is a total constructor and
~> = >? if f is a partial constructor,
and t_{1} and t_{2} are tokens,
is defined inductively as
 [ [ t_{1} t_{2} ] ]:= const and
 [ [ t_{1} i_{1}, i_{2}, ..., i_{n} t_{2} ] ] :=
f( i_{1}, [ [ t_{1} i_{2}, ..., i_{n} t_{2} ] ] ).
Thus if the constructor is not associative one should note that the
list i_{1}, i_{2}, ..., i_{n} is parsed right associative. For example
in the specification
 spec
 Nat=
 ...
 %% define the sort Nat and the operation +
 type
 Nat::=
0  __ + __ (Nat; Nat),

brackets [+ __ +] 
the term
[+ n_1, n_2, n_3, n_4 +].
is translated to n_{1} + (n_{2} + (n_{3} + (n_{4} + 0))).
CoFI
Note: L11  Version: 0.1  11 March 1999.
Comments to roba@informatik.unibremen.de