%> do tex %F -l -l -d"-t a4"
%> do tex %F -l -l -d"-D" -p2

% $Id: glad-def.cia,v 1.3 1994/10/14 11:41:20 lotos Exp lotos $
















\documentstyle[12pt,times]{article}
\input{psfig}



\textwidth=16cm
\oddsidemargin=1cm
\evensidemargin=1cm
\textheight=22cm
\topmargin=0cm
\parindent=0mm
\parskip=4mm

\title{GLAD: General Language to Annotate Data  \\
       Using TOPO --- version 3R6
      }

\author{Marcelino Veiga                         \\
                                                \\
        Dpt. Ingenier{\'\i}a Telem{\'a}tica             \\
        E.T.S.I. de Telecomunicaci{\'o}n                \\
        Univ. Polit{\'e}cnica de Madrid         \\
        E-28040 Madrid, SPAIN                   \\
                                                \\
        {\tt <topo@dit.upm.es>}
        }

\date{10 October, 1994}

\begin{document}

\pagestyle{myheadings}
\markright{A General Language to Annotate Data}

\maketitle

\begin{abstract}
It is a language, with its associated tool,
that permits {\em external} annotation of LOTOS data.
Rather than modifying the specification text,
the required annotations are introduced by TOPO after semantics
analysis, following an external description of user desires.
\end{abstract}

\newpage
\tableofcontents

\newpage

\section{Introduction}
TOPO is able to compile abstract data types following the user
equations by means of generating a rewrite system
specifically tailored to the specification subject to implementation.
This may be valid for early prototypes,
but is usually inadequate for real applications.

Then, TOPO permits to annotate the data.
It is a mechanism to associate LOTOS names to external
(user provided) objects that may be implemented much more efficiently.

Sometimes,
describing a type by means of providing a set of equations is a boring
activity that users wish to skip.
Then,
rather than specifying equations,
the sort and/or operation(s) are said to be external,
and the behavioral part will link to that externally provided data.

Other annotations permit user packages to refer to LOTOS data by
providing name handles.
It would be nice if LOTOS identifiers could be mapped to external
identifiers preserving the lexical value;
but it is usually infeasible due to both the rich set of characters
that LOTOS accepts to build operation identifiers,
and to the facilities provided for overloading names.

TOPO has also a data interpreter, useful for symbolic evaluation of data
expressions, mainly for debugging purposes. In any case (compiler or
interpreter), thinking in rewrite rules it is very useful to provide
information about what are constructors. It allows to debug large
specification much easier. So, TOPO also permit to annotation data for
this purpose.

\section{Why is GLAD needed?}
The primitive mechanism to annotate LOTOS data consist on modifying the
textual specification and write special comments syntactically linked
to sort and/or operation identifiers.

Several problems are a consequence of this:
\begin{enumerate}
\item
  The specification has to be edited,
  and it is frequently impossible to keep the new text concentrated in
  a clearly distinguishable section.
  The annotations are poured all about the user specification.
\item
  It is not possible to annotate data types brought from the library.
  The implementer is forced provide those types needed in its
  specification, rather then bringing them from the standard library.
  Alternatively,
  but equally uneasy,
  a private copy of the \verb/stdlib/ may be edited by the user to
  annotate it.
\item
  Data operations as renaming and actualization manipulate sort and
  operation names.
  As a side effect, annotations are {\em propagated} with no change,
  but there is no way to annotate the resulting objects coming out from them,
  because it is unclear and perhaps too tricky.
\item
  It is cumbersome to do incremental annotations as the specification
  grows up.
  What does it mean?
\end{enumerate}

Owed to these problems it was necessary to invent an alternative
mechanism to annotate data: an annotation language.

\section{Syntax}
The syntax has been chosen deliberately close to LOTOS,
to avoid the users have to pass long time learning a new language.

The language allows to the user to write templates compound with several
sets of rules.
\begin{quote}
\begin{verbatim}
rule
  module ::= _template

rule
  _template ::= [ rule_set * ]
\end{verbatim}
\end{quote}

These sets of rules are divided in four classes. The first and second
ones represent the beginning and the end of the LOTOS specification, and
both ones consist on only one rule.
\begin{quote}
\begin{verbatim}
rule
  rule_set ::= _initial_rule

rule
  rule_set ::= _final_rule
\end{verbatim}
\end{quote}

And third and fourth classes correspond to sort and operation
declarations, both of them compound of one or more rules.
\begin{quote}
\begin{verbatim}
rule
  rule_set ::= "sorts" _sort_rule_list

rule
  _sort_rule_list ::= [ _sort_rule + ]

rule
  rule_set ::= "opns" _operation_rule_list

rule
  _operation_rule_list ::= [ _operation_rule + ]
\end{verbatim}
\end{quote}

Every rule consists of two parts: a pattern and an annotation list.
\begin{quote}
\begin{verbatim}
rule
  _initial_rule ::= _initial_pattern
                    [ "=>" _initial_annotation_list ]
                    ';'

rule
  _final_rule ::= _final_pattern
                  [ "=>" _final_annotation_list ]
                  ';'

rule
  _sort_rule ::= _sort_pattern
                 [ "=>" _sort_annotation_list ]
                 ';'

rule
  _operation_rule ::= _operation_pattern
                      [ "=>" _operation_annotation_list ]
                      ';'
\end{verbatim}
\end{quote}

Both for initial an final rules, the pattern is simple enough.
\begin{quote}
\begin{verbatim}
rule
  _initial_pattern ::= "specification"

rule
  _final_pattern ::= "endspec"
\end{verbatim}
\end{quote}

For sorts, the pattern is like a LOTOS sort declaration. Only one
remark, there is a special sort name, {\em any}, to represent any sort.
\begin{quote}
\begin{verbatim}
rule
  _sort_pattern ::= _sort_descriptor

rule
  _sort_descriptor ::= _any_sort

rule
  _sort_descriptor ::= _sort_identifier

rule
  _any_sort ::= "any"

rule
  _sort_identifier ::= IDENTIFIER
\end{verbatim}
\end{quote}

And for operations, the pattern is also like a LOTOS operation
declaration, with some extensions: a special operation name,
{\em any}, represents any operation; for arguments and result, the
sort name {\em any} is allowed too; and only for arguments the key word
{\em forall} represents any kind and any number of arguments.
\begin{quote}
\begin{verbatim}
rule
  _operation_pattern ::= _operation_descriptor
                         ':' [ _argument_descriptor ]
                         "->" _result_descriptor

rule
  _operation_descriptor ::= _any_operation

rule
  _operation_descriptor ::= _operation_identifier

rule
  _operation_descriptor ::= '_' _operation_identifier '_'

rule
  _any_operation ::= "any"

rule
  _operation_identifier ::= IDENTIFIER

rule
  _operation_identifier ::= SPECIAL

rule
  _argument_descriptor ::= _any_argument_list

rule
  _argument_descriptor ::= _argument_list

rule
  _any_argument_list ::= "forall"

rule
  _argument_list ::= [ argument + ',' ]

rule
  argument ::= _any_sort

rule
  argument ::= _sort_identifier

rule
  _result_descriptor ::= _any_sort

rule
  _result_descriptor ::= _sort_identifier
\end{verbatim}
\end{quote}

And here they are the annotations. For initial rules,
\begin{quote}
\begin{verbatim}
rule
  _initial_annotation_list ::= [ initial_annotation + ]

rule
  initial_annotation ::= _ldc_annotation

rule
  initial_annotation ::= _ldcinit_annotation
\end{verbatim}
\end{quote}

For final rules,
\begin{quote}
\begin{verbatim}
rule
  _final_annotation_list ::= [ final_annotation + ]

rule
  final_annotation ::= _ldc_annotation
\end{verbatim}
\end{quote}

For sort rules,
\begin{quote}
\begin{verbatim}
rule
  _sort_annotation_list ::= [ sort_annotation + ]

rule
  sort_annotation ::= _name_annotation

rule
  sort_annotation ::= _lexical_annotation

rule
  sort_annotation ::= _extern_annotation

rule
  sort_annotation ::= _free_annotation

rule
  sort_annotation ::= _nofree_annotation

rule
  sort_annotation ::= _equal_annotation

rule
  sort_annotation ::= _draw_annotation

rule
  sort_annotation ::= _nodraw_annotation

rule
  sort_annotation ::= _parse_annotation

rule
  sort_annotation ::= _noparse_annotation
\end{verbatim}
\end{quote}

And for operation rules,
\begin{quote}
\begin{verbatim}
rule
  _operation_annotation_list ::= [ operation_annotation + ]

rule
  operation_annotation ::= _using_annotation

rule
  operation_annotation ::= _usingsort_annotation

rule
  operation_annotation ::= _name_annotation

rule
  operation_annotation ::= _lexical_annotation

rule
  operation_annotation ::= _lexicalifpossible_annotation

rule
  operation_annotation ::= _internal_annotation

rule
  operation_annotation ::= _extern_annotation

rule
  operation_annotation ::= _call_annotation

rule
  operation_annotation ::= _partial_annotation

rule
  operation_annotation ::= _constructor_annotation

rule
  operation_annotation ::= _nonconstructor_annotation
\end{verbatim}
\end{quote}

The format of all annotations is the same as in LOTOS specifications.
\begin{quote}
\begin{verbatim}
rule
  _annotation ::= "(*|" annot_name annot_size "|*)"
\end{verbatim}
\end{quote}

And even their size, of course.







\begin{center}
\begin{minipage}[t]{5.5cm}
\begin{tabular}{l | l |}
Name & Size \\
\hline
ldc & {\em text} \\
ldcinit & {\em text} \\
using & {\em word} \\
usingsort & -- \\
name & {\em word} \\
lexical & -- \\
lexicalifpossible & -- \\
internal & -- \\
extern & -- \\
free & {\em word} \\
\hline
\end{tabular}
\end{minipage}
\begin{minipage}[t]{5.5cm}
\begin{tabular}{l | l |}
Name & Size \\
\hline
nofree & -- \\
equal & {\em word} \\
draw & {\em word} \\
nodraw & -- \\
parse & {\em word} \\
noparse & -- \\
call & {\em text} \\
partial & {\em text} \\
constructor & -- \\
nonconstructor & -- \\
\hline
\end{tabular}
\end{minipage}
\end{center}

Besides, there are comments like in LOTOS, than can be nested.
\begin{quote}
\begin{verbatim}
rule
  comment ::= "(*" comm_text "*)"
\end{verbatim}
\end{quote}

\section{Semantics}
\subsection{Annotations}
At the beginning of the specification:
\begin{description}
\item[ldc.-]
  It is a piece of code to be included verbatim in the generated code,
  and is devoted to insert links to external provisions.

\item[ldcinit.-]
  It is also a piece of code, and is to be invoked during start up
  of data run-time support. It is typically used to initialize some
  structures of hand coded data.
\end{description}

At the end of the specification:
\begin{description}
\item[ldc.-]
  It is like the same one at the very beginning, but is devoted to
  insert some definitions to be used in data part of the specification.
\end{description}

For sorts we have the following annotations:
\begin{description}
\item[name.-]
  Use the given name rather than a name generated by TOPO.

\item[lexical.-]
  Use the lexical value to refer to the sort.

  It is the default option to generate sort names.

\item[extern.-]
  This sort is externally implemented.

\item[free.-]
  The user provides a function to deallocate memory.

\item[nofree.-]
  The user does not provide a function to deallocate memory, so
  data of such a sort do not need to deallocate memory.

  It is the default, but it avoids a warning.

\item[equal.-]
  The user provides a function to decide equality,
  overtaking the one provided by the initial model of the algebra.

\item[draw.-]
  The user provides a function to draw values of this sort,
  rather than using system provided pretty--printing.

\item[nodraw.-]
  The user does not provide a function to draw values of this sort, so
  data of such a sort are not printable.

  It is the default, but it avoids a warning.

\item[parse.-]
  The user provides a parsing function a string to get a value of this
  sort. It is used instead of the internal one.

\item[noparse.-]
  The user does not provide any parsing function, so
  this sort is not parseable.

  It is the default, but it avoids a warning.
\end{description}

And for operations:
\begin{description}
\item[using.-]
  The user provides a prefix for the operation name.
  Provided that \verb/operation/ is the name decided for the operation,
  the full name of the operation will be \verb/prefix_operation/.

  This is very handy when there is plenty of overloading,
  either explicit or implied by renaming and/or actualizing.

\item[usingsort.-]
  Similar to previous one, but the prefix is the name decided for the
  sort.

\item[name.-]
  Use the given name rather than a name generated by TOPO.

\item[lexical.-]
  Use the lexical value to refer to the operation.

\item[lexicalifpossible.-]
  The lexical value is used if the target language accepts it,
  otherwise the internal value is used.

\item[internal.-]
  Use an internal name to refer to the operation.

  It is the default option to generate names.

\item[extern.-]
  This operation is externally provided.

\item[call.-]
  It is like a macro to be called instead of generating code for the
  operation.

\item[partial.-]
  A predicate is applied to function arguments in run-time, every time
  the operation is instantiated.
  It raises an exception if the predicate does not hold.

\item[constructor.-]
  This operation may be a constructor,
  and if every pattern for rewriting fails,
  it is legal to build a term using this operation.

  This is the default option.

\item[nonconstructor.-]
  This operation cannot be a constructor:
  the patterns for rewriting should consider every case,
  and provide adequate rewriting.
  If all those fail,
  an exception is raised in run-time.
\end{description}

Everyone of these annotations will be available both via GLAD,
or via direct association to operations in the source text.

\subsection{Relationships}
The next table an initial classification of annotations.



\begin{center}
\begin{minipage}[t]{7.5cm}
\begin{tabular}{l | l | l |}
Name & Class & Group \\
\hline
ldc & {\em external} & -- \\
ldcinit & {\em external} & -- \\
using & {\em external} & {\em using} \\
usingsort & {\em external} & {\em using} \\
name & {\em external} & {\em name} \\
lexical & {\em external} & {\em name} \\
lexicalifpossible & {\em external} & {\em name} \\
internal & {\em external} & {\em name} \\
extern & {\em external} & {\em extern} \\
free & {\em external} & {\em free} \\
\hline
\end{tabular}
\end{minipage}
\begin{minipage}[t]{7.5cm}
\begin{tabular}{l | l | l |}
Name & Class & Group \\
\hline
nofree & {\em external} & {\em free} \\
equal & {\em external} & {\em equal} \\
draw & {\em external} & {\em draw} \\
nodraw & {\em external} & {\em draw} \\
parse & {\em external} & {\em parse} \\
noparse & {\em external} & {\em parse} \\
call & {\em external} & {\em call} \\
partial & {\em external} & {\em partial} \\
constructor & {\em symbolic} & {\em constructor} \\
nonconstructor & {\em symbolic} & {\em constructor} \\
\hline
\end{tabular}
\end{minipage}
\end{center}

As you can see, there are two classes of annotations: {\em symbolic} and
{\em external} ones. First class correspond specially (but not only) to
annotations for symbolic tools, i.e., there is nothing out of LOTOS
(e.g. a data interpreter); and second class, {\em only} to annotations
for non-symbolic tools, i.e., LOTOS specification can be enriched with
some code in another language (e.g. a code generator). In other words,
symbolic tools only can use {\em symbolic} annotation, but non-symbolic
tools can use both {\em symbolic} and {\em external} annotations.

Besides, the annotations are divided in several groups. All the
annotations in the same group have a similar function, so they are
mutually exclusive. And even more, an annotation that belong to any
group cannot be repeated. Only annotation belonging to no group are
compatible to any other one, even itself.

Apart of this relationships, there are several ones more:
\begin{enumerate}
\item
  If a sort is {\em extern},
  it is mandatory to provide an {\em equal} annotation, otherwise an
  error is issued.
  And it is convenient to provide {\em free}, {\em draw} and {\em parse}
  annotations (or their counterpart {\em nofree}, {\em nodraw} and
  {\em noparse}), otherwise a warning is issued.
  Moreover, if a {\em parse} is provided, a {\em draw} annotation
  is also needed.

\item
  If a sort is not {\em extern},
  it is unusual to provide {\em free}, {\em nofree}, {\em equal}, {\em
  draw}, {\em nodraw}, {\em parse} and {\em noparse} annotations.
  A warning is issued if any of them is present.

\item
  If a sort is {\em extern},
  every {\em constructor} operation returning a value of that sort is
  expected to be {\em extern} too.
  An error is issued otherwise.

\item
  If a sort is not {\em extern},
  every {\em constructor} operation returning a value of that sort is
  expected to be not {\em extern} too.
  An error is issued otherwise.

\item
  If a sort is {\em extern} and there one or more operations of such
  sort, one of them must be {\em extern} at least.

\item
  If a sort is not {\em extern} and there one or more operations of such
  sort, one of them must be a {\em constructor} at least.

\item
  Pattern matching may fail on values of external sorts.
  In general, the rewrite system may not make any assumption on the
  structure of values of external sorts.
  In these cases, an error will be issued in a later phase.

\item
  For {\em extern} operations, it is needed either a known {\em name}
  or a {\em call} annotation.

\item
  For {\em extern} operations, the {\em partial} annotation does not
  make sense.

\item
  For not {\em extern} operations, the {\em call} annotation does not
  make sense.
\end{enumerate}

\subsection{Rules}
GLAD applies on the output of the semantics analysis,
where overloading has been sorted out,
and there is a unique (and flat) canonical data type.

The rules of a GLAD specification are applied sequentially.
The system tries to apply rule $N$ to every object in the canonical
data type;
and it is applied as many times as the pattern applies;
when no other application is possible,
rule $N+1$ gets its opportunity.

This mechanism permits to provide general rules
(with generic patterns)
at the beginning,
and later on, more specific ones to refine the annotations.

But there is one exception to this mechanism:
the annotations in LOTOS specifications have priority.
In other words, no annotation in a GLAD specification can override
another one in the LOTOS specification.
It avoids surprises to the users,
and allows to use GLAD only to change default annotations.

\section{Examples}
Let's show a few examples of GLAD use.

\begin{enumerate}
\item
  Default generation of operation names corresponds to
  a simple specification:       \\
  \begin{center}
  \begin{verbatim}
  opns
    any: forall -> any => (*| internal |*) ;
  \end{verbatim}
  \end{center}

\item
  It is useful to generate lexical names for debugging: \\
  \begin{center}
  \begin{verbatim}
  opns
    any: forall -> any => (*| lexical |*) ;
  \end{verbatim}
  \end{center}

\item
  But LOTOS names for operations are not always identifiers in the
  target language, so it is better to generate lexical names only when
  possible:      \\
  \begin{center}
  \begin{verbatim}
  opns
    any: forall -> any => (*| lexicalifpossible |*) ;
  \end{verbatim}
  \end{center}

\item
  It is very usual that a check for constructors is required.
  The following specification provides a means of annotating
  NaturalNumbers:
  \begin{center}
  \begin{verbatim}
  opns
    any: forall -> nat => (*| nonconstructor |*) ;
    0  :        -> nat => (*| constructor |*) ;
    s  : nat    -> nat => (*| constructor |*) ;
  \end{verbatim}
  \end{center}

\item
  And even more general, all the operations can be marked as
  non-constructors, to specify the constructors later on: \\
  \begin{center}
  \begin{verbatim}
    any: forall -> any => (*| nonconstructor |*) ;
  \end{verbatim}
  \end{center}

\item
  When an data is renamed,
  plenty of overloading is usually introduced.
  It may be completely dealt with by qualifying every object of the
  resulting sort:
  \begin{center}
  \begin{verbatim}
    any: forall -> SetOfNats => (*| usingsort |*)
                                (*| lexicalifpossible |*) ;
  \end{verbatim}
  \end{center}

\end{enumerate}

\section{Limitations}
Although the approach proposed above is much more powerful than the
current approach,
still it has some limits.

The most notorious one is that it works on the canonical data type,
what means that no scope information is available to distinguish data
specified in different contexts.

This limitation seems to be rarely applicable in actual practice:
most specifiers concentrate all the data in a single scope,
the outmost one.
This seems to be a good specification style,
although resource oriented specifications might be more interested on
local definitions of data.

\bibliographystyle{abbrv}
\bibliography{lotos}

\end{document}


% Local Variables:
% eval: (if (not (fboundp 'texdate)) (load "texdate" t t nil))
% eval: (if (fboundp 'texdate) (setq texdate-active t))
% End:
