%% $Id$
\appendix
\newlinechar=-1 %mathsing.sty sets \newlinechar=`\|, which would cause mayhem
\chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
Below we present the full syntax of theory definition files as
provided by {\Pure} Isabelle --- object-logics may add their own
sections. \S\ref{sec:ref-defining-theories} explains the meanings of
these constructs. The syntax obeys the following conventions:
\begin{itemize}
\item {\tt Typewriter font} denotes terminal symbols.
\item $id$, $tid$, $nat$, $string$ and $longident$ are the lexical
classes of identifiers, type identifiers, natural numbers, quoted
strings (without the need for \verb$\$\dots\verb$\$ between lines)
and long qualified \ML{} identifiers.
The categories $id$, $tid$, $nat$ are fully defined in \iflabelundefined{Defining-Logics}%
{{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%
{\S\ref{Defining-Logics}}.
\item $text$ is all text from the current position to the end of file,
$verbatim$ is any text enclosed in \verb.{|.\dots\verb.|}.
\item Comments in theories take the form {\tt (*}\dots{\tt*)} and may
be nested, just as in \ML.
\end{itemize}
\begin{rail}
theoryDef : id '=' (name + '+') ('+' extension | ())
;
name : id | string
;
extension : (section +) 'end' ( () | ml )
;
section : classes
| default
| types
| arities
| nonterminals
| consts
| syntax
| trans
| defs
| constdefs
| rules
| axclass
| instance
| oracle
| locale
| local
| global
| setup
;
classes : 'classes' ( classDecl + )
;
classDecl : (id (() | '<' (id + ',')))
;
default : 'default' sort
;
sort : id
| lbrace (id * ',') rbrace
;
types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
;
infix : ( 'infixr' | 'infixl' ) (() | string) nat
;
typeDecl : typevarlist name
( () | '=' ( string | type ) );
typevarlist : () | tid | '(' ( tid + ',' ) ')';
type : simpleType | '(' type ')' | type '=>' type |
'[' ( type + "," ) ']' '=>' type;
simpleType: id | ( tid ( () | '::' id ) ) |
'(' ( type + "," ) ')' id | simpleType id
;
arities : 'arities' ((name + ',') '::' arity +)
;
arity : ( () | '(' (sort + ',') ')' ) sort
;
nonterminals : 'nonterminals' (name+)
;
consts : 'consts' ( mixfixConstDecl + )
;
syntax : 'syntax' (() | mode) ( mixfixConstDecl + );
mode : '(' name (() | 'output') ')'
;
mixfixConstDecl : constDecl (() | ( '(' mixfix ')' ))
;
constDecl : ( name + ',') '::' (string | type);
mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat )
| infix
| 'binder' string nat ;
trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
;
pat : ( () | ( '(' id ')' ) ) string;
rules : 'rules' (( id string ) + )
;
defs : 'defs' (( id string ) + )
;
constdefs : 'constdefs' (name '::' (string | type) (() | mixfix) string +)
;
axclass : 'axclass' classDecl (() | ( id string ) +)
;
instance : 'instance' ( name '<' name | name '::' arity) witness
;
witness : (() | '(' ((string | id | longident) + ',') ')') (() | verbatim)
;
locale : 'locale' name '=' ( () | name '+' ) localeBody
;
localeBody : localeConsts ( () | localeAsms ) ( () | localeDefs )
;
localeConsts: ( 'fixes' ( ( (name '::' ( string | type )) ( () | '(' mixfix ')' ) ) + ) )
;
localeAsms: ( 'assumes' ( ( id string ) + ) )
;
localeDefs: ( 'defines' ( ( id string ) +) )
;
oracle : 'oracle' name '=' name
;
local : 'local'
;
global : 'global'
;
setup : 'setup' (id | longident)
;
ml : 'ML' text
;
\end{rail}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"
%%% End: