doc-src/Ref/theory-syntax.tex

removed ML-Systems/smlnj-1.07.ML;

%% $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
        | consts
        | syntax
        | trans
        | defs
        | constdefs
        | rules
        | axclass
        | instance
        | oracle
        ;

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
      ;

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' (id '::' (string | type) string +)
          ;

axclass : 'axclass' classDecl (() | ( id string ) +)
        ;

instance : 'instance' ( name '<' name | name '::' arity) witness
         ;

witness : (() | '(' ((string | longident) + ',') ')') (() | verbatim)
        ;

oracle : 'oracle' name
       ;

ml : 'ML' text
   ;

\end{rail}