% -*- Mode:LaTeX -*-
% CafeOBJ 1.5.X syntax reference card.
% comment out the following 2 lines if you use old latex209
% \documentclass[a4paper]{article}
\documentclass[a4paper]{article}
\usepackage[scale=0.76]{geometry}
% \usepackage[dvipdfm]{hyperref} 
\usepackage{hyperref} 
%%%% box
\usepackage{fancybox}
\newenvironment{fminipage}%
{\begin{Sbox}\begin{minipage}}%
{\end{minipage}\end{Sbox}\fbox{\TheSbox}}
\newcommand{\vsep}{\vskip\fboxsep}
\newcommand{\nvsep}{\vskip\fboxsep\noindent}
%%%%% xlatex specific
\usepackage{fontspec,xltxtra,xunicode}
\defaultfontfeatures{Mapping=tex-text}
\setromanfont[Mapping=tex-text]{Times New Roman}
\setsansfont[Scale=MatchLowercase,Mapping=tex-text]{Gill Sans}
\setmonofont[Scale=MatchLowercase]{Andale Mono}
%** begin header
\makeatletter
\def\cafeobj{\textsf{CafeOBJ}}
% kbd - argument is characters typed literally.
\def\kbd#1{{\texttt{#1}\null}}
% beginexample...endexample - surrounds literal text, such a code example.
% typeset in a typewriter font with line breaks preserved.
\def\example{\leavevmode\begingroup
  \obeylines\obeyspaces\parskip0pt\texttt}
{\obeyspaces\global\let =\ }
\def\endexample{\endgroup}
% terminal - used for terminal symbols, argument is characters appear in sf.
\def\sym#1{\textsf{#1}\null}
% nonterm - used for non terminal symbols, argument is characters typed with
%           italic face.
\def\nonterm#1{\textit{#1}\null}
% syntax ... endsyntax
\def\xstrut{\relax\ifmmode\copy\strutbox\else\unhcopy\strutbox\fi}
\def\syntax{\syntaxoutnonbox\halign\bgroup
    \xstrut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil
    &$\@lign##$\hfil &\qquad\@lign-- ##\hfil\cr}
\def\endsyntax{\crcr\egroup$$
  \global\@ignoretrue
}
\def\syntaxoutnonbox{\xleavevmode$$
    \parskip=0pt\lineskip=0pt
    \def\\{\crcr}% Must have \def and not \let for nested alignments.
    \everycr={\noalign{\penalty10000}}
    \tabskip=0pt}
\def\xleavevmode{\ifvmode\if@inlabel\indent\else\if@noskipsec\indent\else
    \if@nobreak\global\@nobreakfalse\everypar={}\fi
    {\parskip=0pt\noindent}\fi\fi\fi}
\def\@but{\noalign{\nointerlineskip}}
\def\alt{{\;|\;}}
\def\seqof#1{\mbox{\textbf{\{}}\;{#1}\;\mbox{\textbf{\}}}}
\def\optn#1{\textbf{[}\;{#1}\;\textbf{]}}
\def\synindent{\;\;\;}
\makeatother
%** end of header

\title{\cafeobj\ Syntax Quick Reference \\
  {\small for Interpreter version 1.5.0 or later}}
\date{\today}
%\author{}
\author{Toshimi Sawada\thanks{\texttt{sawada@cafeobj.org}}
  }
\begin{document}
\maketitle
\tableofcontents
%
\setlength{\parindent}{0pt}
\setlength{\parskip}{1.4ex}
\section{Syntax}
\label{sec:cafeobj-syntax}

We use an extended BNF grammar to define the syntax. The general form
of a production is
\begin{syntax}
\synindent\synindent  nonterminal &::=& alternative \alt alternative \alt \cdots \alt alternative
\end{syntax}

The following extensions are used:
\begin{center}
\begin{fminipage}{0.7\textwidth}
  \begin{tabular}{ll}
    a $\cdots$ & a list of one or more \textit{a}s. \\
    a, $\cdots$ & a list of one or more \textit{a}s separated by commas: \\
    & ``a'' or ``a, a'' or ``a, a, a'', etc. \\
    $\seqof{\textrm{a}}$ & \textbf{\{} and \textbf{\}} are meta-syntactical
    brackets \\ 
    & treating \textit{a} as one syntactic category. \\
    $\optn{\textrm{a}}$ & an optional \textit{a}: `` '' or ``a''.
  \end{tabular}
\end{fminipage}
\end{center}
Nonterminal symbols appear in \textit{italic face}. Terminal symbols
appear in the face like this: ``\sym{terminal}'', and may be
surrounded by `` and '' for emphasis or to avoid confusion
with meta characters used in the extended BNF. We will refer terminal
symbols other than self-terminating characters (see section
~\ref{sec:selfterminating}) as \textit{keyword}s in this document.

%\subsection{CafeOBJ program}
\subsection{CafeOBJ Spec}
\label{sec:cafeobjprogram}
\begin{syntax}
  \synindent\synindent spec &::=& \seqof{module \alt view \alt eval} \cdots
\end{syntax}
A \cafeobj\ spec is a sequence of \nonterm{module} (module declaration
-- section ~\ref{sec:module-decl}), \nonterm{view} (view declaration -- 
section ~\ref{sec:view-decl}) or \nonterm{eval} (\textit{reduce} or
\textit{execute} term -- section ~\ref{sec:eval}).

\subsection{Module Declaration}
\label{sec:module-decl}
\begin{syntax}
  module &::=& module\_type\; module\_name \;
  \optn{parameters} \;
  \optn{principal\_sort} \\
  && \sym{``\{''}\; module\_elt\cdots \; \sym{``\}''} \\
  \synindent module\_type &::=& \sym{module} \alt \sym{module!} \alt
  \sym{module*}\\ 
  \synindent module\_name &::=& ident  &
  \footnote{The nonterminal \textit{ident} is for identifiers and 
    will be defined in the section ~\ref{sec:identifier}.} \\
  parameters &::=& \sym{``(''}\; parameter, \cdots \sym{``)''}\\
  \synindent parameter &::=&
  \optn{\sym{protecting}\alt\sym{extending}\alt\sym{including}}\; 
  paramter\_name \; 
  \sym{::}\; module\_expr  &\footnote{\textit{module\_expr} is defined in 
    the section ~\ref{sec:modexpr}.}\footnote{If optional
    $\optn{\sym{protecting}\alt\sym{extending}\alt\sym{including}}$ is omitted, it is
    defaulted to \sym{protecting}.}
 \\
  \synindent parameter\_name &::=& ident \\
  principal\_sort &::=& \sym{principal-sort}\; sort\_name \\
%  module\_elt &::=& import \alt sort \alt record \alt operator \alt
  module\_elt &::=& import \alt sort  \alt operator \alt
  variable \alt axiom \alt macro \alt comment &\footnote{\nonterm{comment} is
    descussed in section ~\ref{sec:comments}.}\\  
  import &::=& \seqof{\sym{protecting}\alt\sym{extending}\alt\sym{including}\alt\sym{using}}
  \sym{``(''}\;module\_expr\;\sym{``)''}\\
  sort & ::= & visible\_sort \alt hidden\_sort \\
  \synindent visible\_sort & ::=& \sym{``[''}\; sort\_decl, \cdots \; \sym{``]''} \\
  \synindent hidden\_sort & ::=& \sym{``*[''}\; sort\_decl, \cdots \; \sym{``]*''} \\
  \synindent sort\_decl &::=& sort\_name\; \cdots\; \optn{supersorts\; \cdots} \\
  \synindent supersorts &::=& <\; sort\_name\; \cdots \\
  \synindent sort\_name &::=& sort\_symbol\optn{qualifier} 
  &\footnote{There must not be any separators (see section
    ~\ref{sec:lex}) between \nonterm{ident} and \nonterm{qualifier}.}
  \\ 
  \synindent sort\_symbol &::=& ident \\
  \synindent qualifier &::=& \sym{``.''}module\_name\\
  % record &::=& \sym{record}\; sort\_name\; \optn{super\;\cdots}\;
  % \sym{``\{''}\; \seqof{slot \alt comment}\cdots \; \sym{``\}''} \\
  % \synindent super &::=&
  % \sym{``[''}\;sort\_name\;\optn{\sym{``(''}\; slot\_rename,\cdots
  %   \sym{``)''}}\;\sym{``]''} \\
  % \synindent slot &::=& slot\_name : sort\_name \alt
  % slot\_name\;\sym{=}\;\sym{``(''}term\sym{``)''}\;:\; sort\_name \\
  % \synindent slot\_name &::=& ident \\
  % \synindent slot\_rename &::=& slot\_name\; \verb|->|\; slot\_name\\
  operator &::=& \seqof{\sym{op}\alt\sym{bop}}
               \; operator\_symbol\; : \; \optn{arity}\; \verb|->|\;
  coarity \; \optn{op\_attrs}
  &\footnote{\nonterm{operator\_symbol} is defined in section
    ~\ref{sec:opsymbol}.}\\ 
  \synindent arity &::=& sort\_name \cdots \\
  \synindent coarity &::=& sort\_name \\
  \synindent op\_attrs &::=& \sym{``\{''}\;op\_attr\cdots\;\sym{``\}''} \\
  \synindent op\_attr &::=& \sym{constr} \alt 
  \sym{associative} \alt \sym{commutative}
  \alt\sym{idempotent}
  \alt \seqof{\sym{id:} \alt \sym{idr:}} \sym{``(''} \; term\; \sym{``)''}
  %&\footnote{The general syntax of \nonterm{term} is defined in section
  %  ~\ref{sec:term}.}
  \\
  &\alt & \sym{strat: ``(''}\; natural \cdots\; \sym{``)''}
  \alt\sym{prec:}\; natural 
  \alt \sym{l-assoc} \alt \sym{r-assoc} \alt \sym{coherent} \alt \sym{demod}
  &\footnote{\nonterm{natural} is a natural number written in ordinal
    arabic notation.} \\
  variable &::=& \sym{var}\; var\_name\; :\; sort\_name \alt
  \sym{vars} \; var\_name\cdots\; :\; sort\_name \\
  \synindent var\_name &::=& ident \\
  axiom &::=& equation \alt cequation\alt transition \alt ctransition \alt fol\\
  \synindent equation &::=& \seqof{\sym{eq} \alt \sym{beq}}\;
  \optn{label}\; term \; \sym{=} \; term\; \sym{``.''}\\
  \synindent cequation &::=& \seqof{\sym{ceq} \alt \sym{bceq}}\;
  \optn{label}\; term \; \sym{=} 
  \; term\; \sym{if}\; term\;\sym{``.''} \\
  \synindent transition &::=& \seqof{\sym{trans} \alt \sym{btrans}}\;
  \optn{label}\; term \; \verb|=>| \; term \;\sym{``.''}\\
  \synindent ctransition &::=& \seqof{\sym{ctrans} \alt \sym{bctrans}}\;
  \optn{label}\; term \; \verb|=>| \; term\; \sym{if}\; term\;\sym{``.''}\\
  \synindent fol & ::= & \sym{ax} \optn{label}\; term \; \sym{``.''}\\
  \synindent label &::=& \sym{``[''}\; ident\cdots\; \sym{``]:''}\\
  macro &::=& \sym{\#define}\; term\; \sym{::=}\; term\; \sym{``.''}
\end{syntax}

\subsection{Module Expression}
\label{sec:modexpr}
\begin{syntax}
  module\_expr &::=& module\_name \alt sum \alt rename \alt instantiation 
  \alt \sym{``(''} module\_expr \sym{``)''} \\
  sum &::=& module\_expr\; \seqof{+\;\; module\_expr} \cdots \\
  rename &::=& module\_expr\;\sym{*}\;\sym{``\{''} rename\_map,\cdots
               \sym{``\}''} \\ 
%  instantiation &::=&  module\_expr\;\sym{``(''}
%  \seqof{ident \optn{qualifier}\;\verb|<=|\;aview},\cdots
%  \sym{``)''}
  instantiation &::=& module\_expr\;\sym{``(''}\textbf{\{}\;ident 
  [ qualifier ]\; \verb|<=|\; aview\textbf{\}},\;\cdots\;\sym{``)''}
  \\ 
  rename\_map &::=& sort\_map \alt op\_map \\
  sort\_map &::=& \seqof{\sym{sort} \alt \sym{hsort}}\; 
  sort\_name \; \verb|->|\; ident \\
  op\_map &::=& \seqof{\sym{op} \alt \sym{bop}}\;
                op\_name\;\verb|->|\;operaotr\_symbol \\
  op\_name &::=& operator\_symbol\alt 
  \sym{``(''}operator\_symbol\sym{``)''}qualifier\\
  aview &::=& view\_name\alt module\_expr\\
  & \alt & 
  \sym{view to}\; module\_expr\;\sym{``\{''} view\_elt,\cdots \sym{``\}''} \\
  view\_name &::=& ident \\
  view\_elt &::=& sort\_map \alt op\_view \alt variable \\
  op\_view &::=& op\_map \alt term\; \verb|->|\; term
\end{syntax}

When a module expression is not fully parenthesized, the proper
nesting of subexpressions may be ambiguous. The following precedence rule
is used to resolve such ambiguity:
\[ \nonterm{sum} < \nonterm{rename} < \nonterm{instantiation} \]

\subsection{View Declaration}
\label{sec:view-decl}
\begin{syntax}
  view &::=& \sym{view}\; view\_name\; \sym{from}\; module\_expr\; \sym{to}
  \; module\_expr \\
  && \sym{``\{''}\; view\_elt, \cdots \; \sym{``\}''} \\
\end{syntax}

%\subsection{Term}
%\label{sec:term}

\subsection{Evaluation}
\label{sec:eval}
\begin{syntax}
  eval & ::= & \seqof{\sym{reduce}\alt\sym{behavioural-reduce}
    \alt\sym{execute}}\; context\;
  term\; \sym{``.''} \\
  context & ::=& \sym{in}\; module\_expr\;\sym{:} 
\end{syntax}
The interpreter has a notion of \textit{current module} which
is specified by a \nonterm{module\_expr} and establishes a context.
If it is set, \nonterm{context} can be omitted.

\subsection{Sugars and Abbriviations}
\label{sec:sugar}
\paragraph{Module type}
There are following abbreviations for \nonterm{module\_type}.
\begin{center}
  \begin{tabular}{ll}\hline
    Keyword & Abbriviation \\\hline
    \sym{module} & \sym{mod}\\
    \sym{module!} & \sym{mod!} \\
    \sym{module*} & \sym{mod*}\\\hline
  \end{tabular}
\end{center}

\paragraph{Module Declaration}
\begin{syntax}
  make &::=& \sym{make}\;module\_name\;\sym{``(''}\; module\_expr\;\sym{``)''}
\end{syntax}
\nonterm{make} is a short hand for declaring module of
name \nonterm{module\_name} which imports \nonterm{module\_expr} with 
protecting mode. 
\begin{example}
  make FOO (BAR * \{sort Bar -> Foo\})
\end{example}
is equivalent to
\begin{example}
  module FOO \{ protecting (BAR * \{sort Bar -> Foo\}) \}
\end{example}

\paragraph{Principal Sort}
\sym{principal-sort} can be abbriviated to \sym{psort}.

\paragraph{Import Mode}
For import modes, the following abbriviations can be used:
\begin{center}
  \begin{tabular}{ll}\hline
    Keyword & Abbriviation \\\hline
    \sym{protecting} & \sym{pr} \\
    \sym{extending} & \sym{ex} \\
    \sym{including} & \sym{inc} \\
    \sym{using} & \sym{us} \\\hline
  \end{tabular}
\end{center}

\paragraph{Simultaneous Operator Declaration}
Several operators with the same arity, coarity and operator attributes 
can be declared at once by \sym{ops}.
The form
\begin{syntax}
  \sym{ops}\; operator\_symbol_1 \cdots operator\_symbol_n\;
  :\; arity\; \verb|->|\; coarity\; op\_attrs
\end{syntax}
is just equivalent to the following multiple operator declarations:
\begin{syntax}
\sym{op}\; & operator\_symbol_1\;:\;arity\;\verb|->|\;coarity\;op\_attrs 
\\
&\vdots\\
\sym{op}\; & operator\_symbol_n\;:\;arity\;\verb|->|\;coarity\;op\_attrs 
\end{syntax}

\sym{bops} is the counterpart of \sym{ops} for behavioural operators.
\begin{syntax}
  \sym{bops}\; operator\_symbol\;\cdots\; : \; arity\;\verb|->|\;
  coarity \; op\_attrs
\end{syntax}

In simultaneous declarations, parentheses are sometimes necessary
to separate operator symbols. This is always required if an operator
symbol contains dots, blank characters or underscores.
  
\paragraph{Predicate}
Predicate declaration (\nonterm{predicate}) is a syntactic sugar for
declaring \sym{Bool} valued operators, and has the syntax:
\begin{syntax}
  predicate &::=&
  \sym{pred}\;operator\_symbol\;:\;arity\;\optn{op\_attrs}
  &\footnote{You cannot use \nonterm{sort\_name} of the same
    character sequence as that of any keywords, i.e., \sym{module}, 
    \sym{op}, \sym{vars}, etc. in \nonterm{arity}.}
\end{syntax}
The form
\begin{syntax}
 \sym{pred}\;operator\_symbol\;:\;arity\;op\_attrs 
\end{syntax}
is equivalent to:
\begin{syntax}
\sym{op}\;operator\_symbol\;:\;arity\;\verb|->|\; \sym{Bool} \;op\_attrs
\end{syntax}

\paragraph{Operator Attributes}
The following abbriviations are available:
\begin{center}
  \begin{tabular}{ll}\hline
    Keyword & Abbriviation \\\hline
    \sym{associative} & \sym{assoc} \\
    \sym{commutative} & \sym{comm} \\
    \sym{idempotent} & \sym{idem} \\\hline
  \end{tabular}
\end{center}

\paragraph{Axioms}
For the keywords introducing axioms, the following
abbriviations can be used:
\begin{center}
  \begin{tabular}{ll|ll}\hline
    Keyword & Abbriviation & Keyword & Abbriviation \\\hline
    \sym{ceq} & \sym{cq} & 
    \sym{bceq} & \sym{bcq} \\
    \sym{trans} & \sym{trns} &
    \sym{ctrans} & \sym{ctrns} \\
    \sym{btrans} & \sym{btrns} &
    \sym{bctrans} & \sym{bctrns} \\\hline
  \end{tabular}
\end{center}

\paragraph{Blocks of Declarations}
References to (importations of) other modules, signature definitions and
axioms can be clusterd in blocked declarations:
\begin{syntax}
  imports &::=&
  \sym{imports}\;\sym{``\{''}\\
  &&\synindent\seqof{import \alt comment}\cdots\\
  &&\sym{``\}''}\\
  signature &::=& \sym{signature}\;\sym{``\{''}\\
  &&\synindent\seqof{sort \alt record \alt operator \alt
    comment}\cdots\\
  &&\sym{``\}''}\\
  axioms &::=&  \sym{axioms}\;\sym{``\{''}\\
  &&\synindent\seqof{variable \alt axiom\alt comment}\cdots\\
  &&\sym{``\}''}
\end{syntax}

\paragraph{Views}
To reduce the complexity of views appearing in module instantiation, 
some sugars are provided. 

First, it is possible to identify parameters by positions, not by names. 
For example, if a parameterized module is declared like
\begin{example}
  \sym{module!} FOO (A1 :: TH1, A2 :: TH2) \sym{\{} ... \sym{\}}
\end{example}
the form
\begin{example}
  FOO(V1, V2)
\end{example}
is equivalent to 
\begin{example}
  FOO(A1 <= V1, A2 <= V2)
\end{example}

Secondly, \sym{view to} construct in arguments of module
instantiations can always be omitted. That is,
\begin{example}
  FOO(A1 <= \sym{view to} \nonterm{module\_expr}\{...\})
\end{example}
can be written as
\begin{example}
  FOO(A1 <= \nonterm{module\_expr}\{...\})
\end{example}

\paragraph{Evaluation}
\begin{center}
\begin{tabular}{ll}\hline
Keyword & Abbriviation \\\hline
\sym{reduce} & \sym{red} \\
\sym{bereduce} & \sym{bred} \\
\sym{execute} & \sym{exec} \\\hline
\end{tabular}
\end{center}

\section{Lexical Considerations}
\label{sec:lex}
A \cafeobj\ spec is written as a sequence of tokens and separators.
A \textit{token} is a sequence of ``printing'' ASCII characters (octal
40 through 176).\footnote{The current interpreter accepts Unicode characters also, but this is beyond the definition of
  CafeOBJ language.}
A \textit{separator} is a ``blank'' character (space, vertical
tab, horizontal tab, carriage return, newline, form feed).
In general, any mumber of separators may appear between tokens. 

\subsection{Reserved Word}
\label{sec:keywords}
There are \textit{no\/} reserved word in \cafeobj.
One can use keywords such as \sym{module}, \sym{op}, \sym{var},
or \sym{signature}, etc. for identifiers or operator symbols.

\subsection{Self-terminating Characters}
\label{sec:selfterminating}
The following eight characters are always treated as \textit{self-terminating},
i.e., the character itself construct a token.
\begin{center}
\begin{tabular}{llllllll}
  \sym{(} & \sym{)} & \sym{,} & \sym{[} & \sym{]}
  & \sym{\{} & \sym{\}} & \sym{;}
\end{tabular}
\end{center}

\subsection{Identifier}
\label{sec:identifier}
Nonterminal \nonterm{ident} is for \emph{identifier}
which is a sequnce of any printing ASCII characters except
the followings:
\begin{center}
  \begin{tabular}{l}
    self-terminating characters (see section ~\ref{sec:selfterminating})\\
    \sym{.} (dot)\\
    \sym{"} (double quote)\\
  \end{tabular}
\end{center}
Upper- and lowercase are distinguished in identifiers.
\nonterm{ident}s are used for module names (\nonterm{module\_name}),
view names (\nonterm{view\_name}), 
parameter names (\nonterm{parameter\_name}), 
sort symbols (\nonterm{sort\_symbol}), variables(\nonterm{var\_name}), 
slot names (\nonterm{slot\_name}) and labels (\nonterm{label}).

\subsection{Operator Symbol}
\label{sec:opsymbol}
The nonterminal \nonterm{operator\_symbol} is used for naming operators 
(\nonterm{operator}) and is a sequence of any ASCII characters
(self-terminating characters or non-printing characters can be an
element of operator names.)\footnote{The current implementation does
  not allow EOT character (control-D) to be an element of operator
  symbol. } 

Underscores are specially treated when they apper as a part of
operator names; they reserve the places where arguments of the
operator are inserted. Thus the single underscore cannot be a
name of an operator. 

\subsection{Comments and Separators}
\label{sec:comments}
A \nonterm{comment} is a sequence of characters that begins with one
of the following four character sequences
\begin{center}
  \begin{tabular}{ll}
    \verb|--| &
    \verb|-->|\\
    \verb|**| &
    \verb|**>| \\
  \end{tabular}
\end{center}
which ends with a newline character, and contains only printing ASCII
characters and horizontal tabs in between.

A \nonterm{separator} is a blank character (space, vertical tab,
horizontal tab, carriage return, newline, from feed).
One or more separators must appear between any two adjuacent
non-self-terminating tokens.\footnote{The same rule is applied to 
  \nonterm{term}.
  Further, if an \nonterm{operator\_symbol} contains blanks or
  self-terminating characters, it is sometimes neccessary to enclose a
  term with such operator as top by parentheses for disambiguation.}

Comments also act as separators, but their apperance is limited to
some specific places (see section ~\ref{sec:cafeobj-syntax}).

\paragraph{Multiline comments}
A multiple lines which starts with \verb+#|+ and ends with \verb+|#+
is treated as multiline comment.
\begin{center}
\begin{verbatim}
#|---------------------------------------------------
  This is an example of multiline comment.
  Multiline comments are used for large text descriptions of
  code or to comment out chunks of code while developping
  your specification. 
  Multiline comments are ignored by the system.
 ---------------------------------------------------|#
\end{verbatim}
\end{center}


\end{document}

% Local variables:
% compile-command: "latex qref"
% TeX-master: t
% End:
