
%\documentstyle{csart}

%\begin{document}

\section{\label{interface}The Procedure Interface: Pattern-matching.}

     Following the {\em occam} model, procedure call semantics are 
defined in terms of abbreviation and textual substitution.  
Informally speaking (with some provisos about name-clashes), the code-fragment
\begin{linear}
\begin{verbatim}

    PROC eg ([] INDEX x, {x} INT a)

      ...  body of 'eg'
    :

    [n] INDEX y :
    {y} INT b :
    SEQ
      ...  preamble
      eg (y, b)

\end{verbatim}
\end{linear}
is ``semantically equivalent'' to the fragment
\begin{linear}
\begin{verbatim}

    [n] INDEX y :
    {y} INT b :
    SEQ
      ...  preamble

      [] INDEX x IS y :
      {x} INT  a IS b :
      ...  body of 'eg'

\end{verbatim}
\end{linear}
With this understanding it suffices to give a meaning to type and
rank matching in abbreviations, in order to define their behaviour
in the procedure interface.

     Three generic forms of abbreviation are
\begin{linear}
\begin{verbatim}

     abbreviation  ::=  name IS expression :

     abbreviation  ::=  type_pattern name IS expression :

     abbreviation  ::=  rank_pattern type_pattern name IS expression :

\end{verbatim}
\end{linear}
(\verb$VAL$ forms would also be available).
In the first form the type (and rank, if there is a non-trivial one)
of $name$ are inherited from $expression$ (this is a normal {\em occam}
convention).  In the second form rank is inherited from
$expression$---$type\_pattern$ must match the type of $expression$.
Section \ref{type} describes treatment of this form.
Section \ref{rank} describes treatment of the third form.
First we introduce a couple of operators involving types and ranks.

\subsection{Some Type and Rank Operators}

     The operator \verb$TYPEOF$ applied to an expression returns to
type of an operator.  Similarly the operator \verb$RANKOF$ returns an
expression's rank.

     Two primitive ``arithmetic'' operators on ranks are defined.
The ``union'' operator \verb$\/$ can be used to combine several ranks,
returning the rank containing all the indicies from the component
ranks.
\begin{linear}
\begin{verbatim}

    {x, y} \/ {z} = {x, y, z}

\end{verbatim}
\end{linear}
Note however that it is erroneous to try and combine
ranks with common indicies using \verb$\/$.  The union operator
is commutative.

    The ``subtraction''
operator \verb$-$ can be used to combine two ranks, returning
the rank containing those indicies in its left-hand operand which
are not in its right-hand operand.
\begin{linear}
\begin{verbatim}

    {x, y, z} - {z} = {x, y}

\end{verbatim}
\end{linear}
It is erroneous to try to
combine ranks for which the right-hand operand is not a subset of
the left-hand operand using \verb$-$.  Below we take the subtraction operator
to have lower precedence than the union operator.

\subsection{\label{type}Type Matching}

     The syntax for a type pattern is simply
\begin{linear}
\begin{verbatim}

    type_pattern   ::=  type_constant | type_variable

    type_variable  ::=  TYPE name 

\end{verbatim}
\end{linear}
and $type\_constant$ is either the name of a previously defined type,
or a literal type (such as \verb$[3] INT$).

      Type patterns are reduced rather straightforwardly.  In the
case where the pattern is a type-constant, no reduction is necessary.
In the case where it is a type-variable, the reduction is
\begin{linear}
\begin{verbatim}

     TYPE name_1 name_2 IS expression :

\end{verbatim}
\end{linear}
is equivalent to
\begin{linear}
\begin{verbatim}

     TYPE name_1 IS TYPEOF expression :
     name_2      IS expression :

\end{verbatim}
\end{linear}

     We can now give a full (if fairly trivial) example of a
type-polymorphic procedure:
\begin{linear}
\begin{verbatim}

    PROC copy (TYPE t out, VAL t in)

      out := in
    :

    REAL32 a, b :
    SEQ
      ...
      copy (a, b)

\end{verbatim}
\end{linear}
is first reduced to
\begin{linear}
\begin{verbatim}

    REAL32 a, b :
    SEQ
      ...
      TYPE t out IS a :
      VAL  t  in IS b :
      out := in

\end{verbatim}
\end{linear}
by the procedure expansion rules.  The second abbreviation needs no
reduction.  The first is reduced according to the above rules to
\begin{linear}
\begin{verbatim}

    REAL32 a, b :
    SEQ
      ...
      TYPE t   IS TYPEOF a :
      out      IS a :
      VAL t in IS b :
      out := in

\end{verbatim}
\end{linear}
In other words, the type variable $t$ is bound to the value \verb$REAL32$,
and the types of the $a$ and $b$ abbreviations match correctly.

\subsection{\label{rank}Rank Matching}

     The syntax of a rank pattern is more elaborate.  Introduce
\begin{linear}
\begin{verbatim}

    index_constant ::=  name

    index_variable ::=  [] INDEX name | [expression] INDEX name

    rank_element   ::=  rank_constant | rank_variable

    rank_constant  ::=  name | { index_constant_list }

    rank_variable  ::=  RANK name | { index_variable_list }

\end{verbatim}
\end{linear}
where $index\_constant\_list$ and $index\_variable\_list$ are comma-separated
lists.  The syntax of a rank pattern is then
\begin{linear}
\begin{verbatim}

    rank_pattern   ::=  rank_element | rank_element \/ rank_pattern

\end{verbatim}
\end{linear}
In other words, a rank pattern is a union of rank constants and
rank variables.
To disambiguate pattern-matching, we assume
that there is at most one {\em rank variable} in a particular
rank pattern.  For example
\begin{linear}
\begin{verbatim}

    r \/ s \/ {[] INDEX x, [] INDEX y}

    {x} \/ RANK r

\end{verbatim}
\end{linear}
are legal rank patterns, with the last term of the union being the
rank variable in both cases.  But
\begin{linear}
\begin{verbatim}

    RANK s \/ {[] INDEX x}
   
\end{verbatim}
\end{linear}
is illegal, because it includes two rank variables.

     In the case where the rank pattern has no variable part, the
abbreviation reduces immediately to the case of the previous section
\begin{linear}
\begin{verbatim}

     rank_pattern type_pattern name IS expression :

\end{verbatim}
\end{linear}
is equivalent to
\begin{linear}
\begin{verbatim}

     type_pattern name IS expression :

\end{verbatim}
\end{linear}
provided the constant $rank\_pattern$ matches the rank of $expression$.
Otherwise a rank-checking error has occured.  In the case where
the rank pattern includes a variable part and a constant part,
denote the variable part by $var$ and the constant part by $const$,
and the reduction is to
\begin{linear}
\begin{verbatim}

     var               IS RANKOF expression - const :
     type_pattern name IS expression :

\end{verbatim}
\end{linear}

     Since the latter manipulation is slightly intricate we
give two examples.  In
\begin{linear}
\begin{verbatim}

    r \/ s \/ {[] INDEX x, [] INDEX y} INT a IS expr :

\end{verbatim}
\end{linear}
$var$ is identified as \verb${[] INDEX x, [] INDEX y}$ and $const$ as
\verb$r \/ s$, with the resulting reduction 
\begin{linear}
\begin{verbatim}

    {[] INDEX x, [] INDEX y} IS RANKOF expr - r \/ s :
    INT a IS expr :

\end{verbatim}
\end{linear}
and in
\begin{linear}
\begin{verbatim}

    {x} \/ RANK r TYPE t a IS expr :

\end{verbatim}
\end{linear}
$var$ is identified as \verb$RANK r$ and $const$ as
\verb${x}$, leading to
\begin{linear}
\begin{verbatim}

    RANK r   IS RANKOF expr - {x} :
    TYPE t a IS expr :

\end{verbatim}
\end{linear}

     Finally we have to give a meaning to abbreviations of the
form
\begin{linear}
\begin{verbatim}

    { index_variable_list } IS rank_expression :

\end{verbatim}
\end{linear}
such as that appearing in the first example above.  If the number of
index variables in the list doesn't correspond to the size of the
rank expression on the left hand side, a rank-checking error occurs.
Otherwise, if there is only one index variable in the list the meaning
is fairly clear.  If there are several, an ambiguity exists.  
To give a meaning to this case we assume that all indicies
in existence have a precedence defined amongst them.  For example
the index defined first---with the largest scope---could be
the highest precedence, and so on.  This gives a natural ordering
to the indicies in the $rank\_expression$ set.  After evaluating
this expression and ordering it thus, the substitution takes the form
\begin{linear}
\begin{verbatim}

    {[e_1] INDEX v_1, ..., [e_n] INDEX v_n} IS {c_1, ..., c_n} :

\end{verbatim}
\end{linear}
is equivalent to
\begin{linear}
\begin{verbatim}

    [e_1] INDEX v_1 IS c_1 :
    ...
    [e_n] INDEX v_n IS c_n :

\end{verbatim}
\end{linear}

%\end{document}
