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: |
|