doc-src/Ref/theory-syntax.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 6669 5f1ce866c497
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
     1 %% $Id$
     2 
     3 \appendix
     4 \newlinechar=-1  %mathsing.sty sets \newlinechar=`\|, which would cause mayhem
     5 
     6 \chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
     7 
     8 Below we present the full syntax of theory definition files as provided by
     9 Pure Isabelle --- object-logics may add their own sections.
    10 \S\ref{sec:ref-defining-theories} explains the meanings of these constructs.
    11 The syntax obeys the following conventions:
    12 \begin{itemize}
    13 \item {\tt Typewriter font} denotes terminal symbols.
    14   
    15 \item $id$, $tid$, $nat$, $string$ and $longident$ are the lexical
    16   classes of identifiers, type identifiers, natural numbers, quoted
    17   strings (without the need for \verb$\$\dots\verb$\$ between lines)
    18   and long qualified \ML{} identifiers.
    19   The categories $id$, $tid$, $nat$ are fully defined in \iflabelundefined{Defining-Logics}%
    20   {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%
    21   {\S\ref{Defining-Logics}}.
    22   
    23 \item $text$ is all text from the current position to the end of file,
    24   $verbatim$ is any text enclosed in \verb.{|.\dots\verb.|}.
    25   
    26 \item Comments in theories take the form {\tt (*}\dots{\tt*)} and may
    27   be nested, just as in \ML.
    28 \end{itemize}
    29 
    30 \begin{rail}
    31 
    32 theoryDef : id '=' (name + '+') ('+' extension | ())
    33           ;
    34 
    35 name : id | string
    36      ;
    37 
    38 extension : (section +) 'end' ( () | ml )
    39           ;
    40 
    41 section : classes
    42         | default
    43         | types
    44         | arities
    45         | nonterminals
    46         | consts
    47         | syntax
    48         | trans
    49         | defs
    50         | constdefs
    51         | rules
    52         | axclass
    53         | instance
    54         | oracle
    55         | locale
    56         | local
    57         | global
    58         | setup
    59         ;
    60 
    61 classes : 'classes' ( classDecl + )
    62         ;
    63 
    64 classDecl : (id (() | '<' (id + ',')))
    65           ;
    66 
    67 default : 'default' sort 
    68         ;
    69 
    70 sort :  id
    71      | lbrace (id * ',') rbrace
    72      ;
    73 
    74 types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
    75       ;
    76 
    77 infix : ( 'infixr' | 'infixl' ) (() | string) nat
    78       ;
    79 
    80 typeDecl : typevarlist name
    81            ( () | '=' ( string | type ) );
    82 
    83 typevarlist : () | tid | '(' ( tid + ',' ) ')';
    84 
    85 type : simpleType | '(' type ')' | type '=>' type |
    86        '[' ( type + "," ) ']' '=>' type;
    87 
    88 simpleType: id | ( tid ( () | '::' id ) ) |
    89             '(' ( type + "," ) ')' id | simpleType id
    90           ;
    91 
    92 arities : 'arities' ((name + ',') '::' arity +)
    93         ;
    94 
    95 arity : ( () | '(' (sort + ',') ')' ) sort
    96       ;
    97 
    98 nonterminals : 'nonterminals' (name+)
    99              ;
   100 
   101 consts : 'consts' ( mixfixConstDecl + )
   102        ;
   103 
   104 syntax : 'syntax' (() | mode) ( mixfixConstDecl + );
   105 
   106 mode : '(' name (() | 'output') ')'
   107      ;
   108 
   109 mixfixConstDecl : constDecl (() | ( '(' mixfix ')' ))
   110                 ;
   111 
   112 constDecl : ( name + ',') '::' (string | type);
   113 
   114 mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
   115        |  infix
   116        | 'binder' string nat ;
   117 
   118 trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
   119       ;
   120 
   121 pat : ( () | ( '(' id ')' ) ) string;
   122 
   123 rules : 'rules' (( id string ) + )
   124       ;
   125 
   126 defs : 'defs' (( id string ) + )
   127      ;
   128 
   129 constdefs : 'constdefs' (name '::' (string | type) (() | mixfix) string +)
   130           ;
   131 
   132 axclass : 'axclass' classDecl (() | ( id string ) +)
   133         ;
   134 
   135 instance : 'instance' ( name '<' name | name '::' arity) witness
   136          ;
   137 
   138 witness : (() | '(' ((string | id | longident) + ',') ')') (() | verbatim)
   139         ;
   140 
   141 locale : 'locale' name '=' ( () | name '+' ) localeBody
   142        ;
   143 
   144 localeBody : localeConsts ( () | localeAsms ) ( () | localeDefs )
   145        ;
   146 
   147 localeConsts: ( 'fixes' ( ( (name '::' ( string | type )) ( () | '(' mixfix ')' ) ) + ) )
   148        ;
   149 
   150 
   151 localeAsms:    ( 'assumes' ( ( id string ) + ) )
   152        ;
   153 
   154 localeDefs:   ( 'defines' ( ( id string ) +) )
   155        ;
   156 
   157 oracle : 'oracle' name '=' name
   158        ;
   159 
   160 local : 'local'
   161       ;
   162 
   163 global : 'global'
   164        ;
   165 
   166 setup : 'setup' (id | longident)
   167       ;
   168 
   169 ml : 'ML' text
   170    ;
   171 
   172 \end{rail}
   173 
   174 
   175 %%% Local Variables: 
   176 %%% mode: latex
   177 %%% TeX-master: "ref"
   178 %%% End: