doc-src/Ref/theories.tex

--- a/doc-src/Ref/theories.tex	Thu Nov 25 11:39:45 1993 +0100
+++ b/doc-src/Ref/theories.tex	Thu Nov 25 11:49:21 1993 +0100
@@ -1,4 +1,5 @@
 %% $Id$
+
 \chapter{Theories, Terms and Types} \label{theories}
 \index{theories|(}\index{signatures|bold}
 \index{reading!axioms|see{{\tt extend_theory} and {\tt assume_ax}}}
@@ -47,7 +48,7 @@
 $theoryDef$ &=& $id$ {\tt=} $name@1$ {\tt+} \dots {\tt+} $name@n$
                             [{\tt+} $extension$]\\\\
 $extension$ &=& [$classes$] [$default$] [$types$] [$arities$] [$consts$]
-                [$rules$] {\tt end} [$ml$]\\\\
+                [$trans$] [$rules$] {\tt end} [$ml$]\\\\
 $classes$ &=& \ttindex{classes} $class$ \dots $class$ \\\\
 $class$ &=& $id$ [{\tt<} $id@1${\tt,} \dots{\tt,} $id@n$] \\\\
 $default$ &=& \ttindex{default} $sort$ \\\\
@@ -67,6 +68,9 @@
              [ [\quad{\tt[} $k@1${\tt,} \dots{\tt,} $k@n$ {\tt]}\quad] $k$]\\
        &$|$& $infix$ \\
        &$|$& \ttindex{binder} $string$ $k$\\\\
+$trans$ &=& \ttindex{translations} $transDecl$ \dots $transDecl$ \\\\
+$transDecl$ &=& [ {\tt(}$string${\tt)} ] $string$ 
+  [ {\tt=>} $|$ {\tt<=} $|$ {\tt==} ] [ ($string$) ] $string$ \\\\
 $rules$ &=& \ttindex{rules} $rule$ \dots $rule$ \\\\
 $rule$ &=& $id$ $string$ \\\\
 $ml$ &=& \ttindex{ML} $text$
@@ -123,13 +127,47 @@
   A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em
     binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated
   like $f(F)$; $p$ is the precedence of the construct.
+\item[$transDecl$] Specifies a syntactic translation rule, that is a parse 
+  rule ({\tt =>}), a print rule ({\tt <=}), or both ({\tt ==}).
 \item[$rule$] A rule consists of a name $id$ and a formula $string$.  Rule
   names must be distinct.
 \item[$ml$] This final part of a theory consists of ML code, 
   typically for parse and print translations.
 \end{description}
-The $mixfix$ and $ml$ sections are explained in more detail in the {\it
-Defining Logics} chapter of the {\it Logics} manual.
+The $mixfix$, $transDecl$ and $ml$ sections are explained in more detail in 
+the {\it Defining Logics} chapter of the {\it Logics} manual.
+
+
+\subsection{Classes and types}
+\index{*arities!context conditions}
+
+Type declarations are subject to the following two well-formedness
+conditions:
+\begin{itemize}
+\item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$
+  with $\vec{r} \neq \vec{s}$.  For example
+\begin{ttbox}
+types ty 1
+arities ty :: ({\ttlbrace}logic{\ttrbrace}) logic
+        ty :: ({\ttlbrace}{\ttrbrace})logic
+\end{ttbox}
+leads to an error message and fails.
+\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
+  (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
+  for $i=1,\dots,n$.  The relationship $\preceq$, defined as
+\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
+expresses that the set of types represented by $s'$ is a subset of the set of
+types represented by $s$.  For example
+\begin{ttbox}
+classes term < logic
+types ty 1
+arities ty :: ({\ttlbrace}logic{\ttrbrace})logic
+        ty :: ({\ttlbrace}{\ttrbrace})term
+\end{ttbox}
+leads to an error message and fails.
+\end{itemize}
+These conditions guarantee principal types~\cite{nipkow-prehofer}.
+
 
 \section{Loading Theories}
 \label{LoadingTheories}