author | clasohm |
Thu, 30 Nov 1995 12:58:44 +0100 | |
changeset 1375 | d04af07266e8 |
parent 1373 | f061d2435d63 |
child 1379 | 8f693d2ffb59 |
permissions | -rw-r--r-- |
285 | 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} |
|
325 | 7 |
Chapter~\ref{sec:ref-defining-theories} explains the meanings of these |
8 |
constructs. The syntax obeys the following conventions: |
|
285 | 9 |
\begin{itemize} |
10 |
\item {\tt Typewriter font} denotes terminal symbols. |
|
11 |
\item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of |
|
12 |
identifiers, type identifiers, natural numbers, \ML\ strings (with their |
|
1148 | 13 |
quotation marks, but without the need for \verb$\$ at the end of a line and |
14 |
the beginning of the next line) and arbitrary \ML\ text. The first three |
|
15 |
are fully defined in \iflabelundefined{Defining-Logics}% |
|
325 | 16 |
{{\it The Isabelle Reference Manual}, chapter `Defining Logics'}% |
17 |
{Chap.\ts\ref{Defining-Logics}}. |
|
285 | 18 |
\end{itemize} |
325 | 19 |
Comments in theories take the form {\tt (*} {\it text\/} {\tt*)}, where |
20 |
{\it text\/} should not contain the character sequence {\tt*)}. |
|
285 | 21 |
|
22 |
\begin{rail} |
|
23 |
||
24 |
theoryDef : id '=' (name + '+') ('+' extension | ()); |
|
25 |
||
26 |
name: id | string; |
|
27 |
||
1082 | 28 |
extension : (section +) 'end' ( () | ml ); |
285 | 29 |
|
1080 | 30 |
section : classes |
31 |
| default |
|
32 |
| types |
|
33 |
| arities |
|
34 |
| consts |
|
35 |
| trans |
|
36 |
| defs |
|
37 |
| rules |
|
38 |
; |
|
39 |
||
40 |
classes : 'classes' ( ( id ( () |
|
285 | 41 |
| '<' (id + ',') |
42 |
) |
|
43 |
) + ) |
|
44 |
; |
|
45 |
||
1080 | 46 |
default : 'default' sort |
285 | 47 |
; |
48 |
||
49 |
sort : id |
|
50 |
| '\{' (id * ',') '\}' |
|
51 |
; |
|
52 |
||
1080 | 53 |
types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) |
285 | 54 |
; |
55 |
||
325 | 56 |
typeDecl : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '=' string ); |
285 | 57 |
|
58 |
infix : ( 'infixr' | 'infixl' ) nat; |
|
59 |
||
60 |
||
1080 | 61 |
arities : 'arities' ((( name + ',' ) '::' arity ) + ) |
285 | 62 |
; |
63 |
||
64 |
arity : ( () |
|
65 |
| '(' (sort + ',') ')' |
|
66 |
) id |
|
67 |
; |
|
68 |
||
69 |
||
1080 | 70 |
consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + ) |
285 | 71 |
; |
72 |
||
1375 | 73 |
constDecl : ( name + ',') '::' (string | constType); |
285 | 74 |
|
1375 | 75 |
constType : simpleType | '(' constType ')' | '[' ( constType + "," ) ']' |
76 |
'=>' constType | constType '=>' constType; |
|
1373
f061d2435d63
changed syntax diagrams according to quote-less consts and syntax section
clasohm
parents:
1148
diff
changeset
|
77 |
|
1375 | 78 |
simpleType: id | ( tid ( () | '::' id ) ) | |
79 |
'(' ( constType + "," ) ')' id | simpleType id; |
|
285 | 80 |
|
81 |
mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) |
|
82 |
| infix |
|
83 |
| 'binder' string nat ; |
|
84 |
||
1080 | 85 |
trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) |
285 | 86 |
; |
87 |
||
88 |
pat : ( () | ( '(' id ')' ) ) string; |
|
89 |
||
1080 | 90 |
rules : 'rules' (( id string ) + ) |
285 | 91 |
; |
92 |
||
1080 | 93 |
defs : 'defs' (( id string ) + ) |
94 |
; |
|
95 |
||
1082 | 96 |
ml : 'ML' text |
285 | 97 |
; |
98 |
||
99 |
\end{rail} |