Up Next
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 i1, i2, i3, and i4 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 CASL-syntax 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 meta-function [| __ |]: 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 declaration7 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 t1 __ t2 : t* ~> s, where ~> = -> if f is a total constructor and ~> = ->? if f is a partial constructor, and t1 and t2 are tokens, is defined inductively as Thus if the constructor is not associative one should note that the list i1, i2, ..., in 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 n1 + (n2 + (n3 + (n4 + 0))).
CoFI Note: L-11 -- Version: 0.1 -- 11 March 1999.
Comments to roba@informatik.uni-bremen.de

Up Next