% -*- Mode:LaTeX -*-
% CafeOBJ 1.4.0 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]{FreeSerif}
\setsansfont[Scale=MatchLowercase,Mapping=tex-text]{FreeSans}
\setmonofont[Scale=MatchLowercase]{FreeMono}
%** 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.4.8 or later}}
\date{\today}
%\author{}
\author{Toshimi Sawada\thanks{\texttt{sawada@cafeobj.org}} \\
  Kosakusha Inc.
  }
\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}).

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