author | wenzelm |
Thu, 13 Nov 2008 21:56:23 +0100 | |
changeset 28770 | 93a372e2dc7a |
parent 28769 | 8fc228f21861 |
child 28771 | 4510201c6aaf |
permissions | -rw-r--r-- |
28762 | 1 |
(* $Id$ *) |
2 |
||
3 |
theory Inner_Syntax |
|
4 |
imports Main |
|
5 |
begin |
|
6 |
||
7 |
chapter {* Inner syntax --- the term language *} |
|
8 |
||
9 |
section {* Printing logical entities *} |
|
10 |
||
11 |
subsection {* Diagnostic commands *} |
|
12 |
||
13 |
text {* |
|
14 |
\begin{matharray}{rcl} |
|
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
15 |
@{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
28762 | 16 |
@{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
17 |
@{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
18 |
@{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
28762 | 19 |
@{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
20 |
@{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
21 |
@{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
28762 | 22 |
\end{matharray} |
23 |
||
24 |
These diagnostic commands assist interactive development by printing |
|
25 |
internal logical entities in a human-readable fashion. |
|
26 |
||
27 |
\begin{rail} |
|
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
28 |
'typ' modes? type |
28762 | 29 |
; |
30 |
'term' modes? term |
|
31 |
; |
|
32 |
'prop' modes? prop |
|
33 |
; |
|
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
34 |
'thm' modes? thmrefs |
28762 | 35 |
; |
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
36 |
( 'prf' | 'full\_prf' ) modes? thmrefs? |
28762 | 37 |
; |
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
38 |
'pr' modes? nat? (',' nat)? |
28762 | 39 |
; |
40 |
||
41 |
modes: '(' (name + ) ')' |
|
42 |
; |
|
43 |
\end{rail} |
|
44 |
||
45 |
\begin{description} |
|
46 |
||
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
47 |
\item @{command "typ"}~@{text \<tau>} reads and prints types of the |
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
48 |
meta-logic according to the current theory or proof context. |
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
49 |
|
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
50 |
\item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>} |
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
51 |
read, type-check and print terms or propositions according to the |
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
52 |
current theory or proof context; the inferred type of @{text t} is |
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
53 |
output as well. Note that these commands are also useful in |
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
54 |
inspecting the current environment of term abbreviations. |
28762 | 55 |
|
56 |
\item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves |
|
57 |
theorems from the current theory or proof context. Note that any |
|
58 |
attributes included in the theorem specifications are applied to a |
|
59 |
temporary context derived from the current theory or proof; the |
|
60 |
result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1, |
|
61 |
\<dots>, a\<^sub>n"} do not have any permanent effect. |
|
62 |
||
63 |
\item @{command "prf"} displays the (compact) proof term of the |
|
64 |
current proof state (if present), or of the given theorems. Note |
|
65 |
that this requires proof terms to be switched on for the current |
|
66 |
object logic (see the ``Proof terms'' section of the Isabelle |
|
67 |
reference manual for information on how to do this). |
|
68 |
||
69 |
\item @{command "full_prf"} is like @{command "prf"}, but displays |
|
70 |
the full proof term, i.e.\ also displays information omitted in the |
|
71 |
compact proof term, which is denoted by ``@{text _}'' placeholders |
|
72 |
there. |
|
73 |
||
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
74 |
\item @{command "pr"}~@{text "goals, prems"} prints the current |
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
75 |
proof state (if present), including the proof context, current facts |
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
76 |
and goals. The optional limit arguments affect the number of goals |
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
77 |
and premises to be displayed, which is initially 10 for both. |
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
78 |
Omitting limit values leaves the current setting unchanged. |
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
79 |
|
28762 | 80 |
\end{description} |
81 |
||
82 |
All of the diagnostic commands above admit a list of @{text modes} |
|
83 |
to be specified, which is appended to the current print mode (see |
|
84 |
also \cite{isabelle-ref}). Thus the output behavior may be modified |
|
85 |
according particular print mode features. For example, @{command |
|
86 |
"pr"}~@{text "(latex xsymbols)"} would print the current proof state |
|
87 |
with mathematical symbols and special characters represented in |
|
88 |
{\LaTeX} source, according to the Isabelle style |
|
89 |
\cite{isabelle-sys}. |
|
90 |
||
91 |
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more |
|
92 |
systematic way to include formal items into the printed text |
|
93 |
document. |
|
94 |
*} |
|
95 |
||
96 |
||
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
97 |
subsection {* Details of printed content *} |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
98 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
99 |
text {* |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
100 |
\begin{mldecls} |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
101 |
@{index_ML show_types: "bool ref"} & default @{ML false} \\ |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
102 |
@{index_ML show_sorts: "bool ref"} & default @{ML false} \\ |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
103 |
@{index_ML show_consts: "bool ref"} & default @{ML false} \\ |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
104 |
@{index_ML long_names: "bool ref"} & default @{ML false} \\ |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
105 |
@{index_ML short_names: "bool ref"} & default @{ML false} \\ |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
106 |
@{index_ML unique_names: "bool ref"} & default @{ML true} \\ |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
107 |
@{index_ML show_brackets: "bool ref"} & default @{ML false} \\ |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
108 |
@{index_ML eta_contract: "bool ref"} & default @{ML true} \\ |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
109 |
@{index_ML goals_limit: "int ref"} & default @{ML 10} \\ |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
110 |
@{index_ML Proof.show_main_goal: "bool ref"} & default @{ML false} \\ |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
111 |
@{index_ML show_hyps: "bool ref"} & default @{ML false} \\ |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
112 |
@{index_ML show_tags: "bool ref"} & default @{ML false} \\ |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
113 |
@{index_ML show_question_marks: "bool ref"} & default @{ML true} \\ |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
114 |
\end{mldecls} |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
115 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
116 |
These global ML variables control the detail of information that is |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
117 |
displayed for types, terms, theorems, goals etc. |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
118 |
|
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
119 |
In interactive sessions, the user interface usually manages these |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
120 |
global parameters of the Isabelle process, even with some concept of |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
121 |
persistence. Nonetheless it is occasionally useful to manipulate ML |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
122 |
variables directly, e.g.\ using @{command "ML_val"} or @{command |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
123 |
"ML_command"}. |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
124 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
125 |
Batch-mode logic sessions may be configured by putting appropriate |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
126 |
ML text directly into the @{verbatim ROOT.ML} file. |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
127 |
|
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
128 |
\begin{description} |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
129 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
130 |
\item @{ML show_types} and @{ML show_sorts} control printing of type |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
131 |
constraints for term variables, and sort constraints for type |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
132 |
variables. By default, neither of these are shown in output. If |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
133 |
@{ML show_sorts} is set to @{ML true}, types are always shown as |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
134 |
well. |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
135 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
136 |
Note that displaying types and sorts may explain why a polymorphic |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
137 |
inference rule fails to resolve with some goal, or why a rewrite |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
138 |
rule does not apply as expected. |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
139 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
140 |
\item @{ML show_consts} controls printing of types of constants when |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
141 |
displaying a goal state. |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
142 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
143 |
Note that the output can be enormous, because polymorphic constants |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
144 |
often occur at several different type instances. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
145 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
146 |
\item @{ML long_names}, @{ML short_names}, and @{ML unique_names} |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
147 |
control the way of printing fully qualified internal names in |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
148 |
external form. See also \secref{sec:antiq} for the document |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
149 |
antiquotation options of the same names. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
150 |
|
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
151 |
\item @{ML show_brackets} controls bracketing in pretty printed |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
152 |
output. If set to @{ML true}, all sub-expressions of the pretty |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
153 |
printing tree will be parenthesized, even if this produces malformed |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
154 |
term syntax! This crude way of showing the internal structure of |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
155 |
pretty printed entities may occasionally help to diagnose problems |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
156 |
with operator priorities, for example. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
157 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
158 |
\item @{ML eta_contract} controls @{text "\<eta>"}-contracted printing of |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
159 |
terms. |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
160 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
161 |
The @{text \<eta>}-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"}, |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
162 |
provided @{text x} is not free in @{text f}. It asserts |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
163 |
\emph{extensionality} of functions: @{prop "f \<equiv> g"} if @{prop "f x \<equiv> |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
164 |
g x"} for all @{text x}. Higher-order unification frequently puts |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
165 |
terms into a fully @{text \<eta>}-expanded form. For example, if @{text |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
166 |
F} has type @{text "(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>"} then its expanded form is @{term |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
167 |
"\<lambda>h. F (\<lambda>x. h x)"}. |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
168 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
169 |
Setting @{ML eta_contract} makes Isabelle perform @{text |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
170 |
\<eta>}-contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"} |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
171 |
appears simply as @{text F}. |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
172 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
173 |
Note that the distinction between a term and its @{text \<eta>}-expanded |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
174 |
form occasionally matters. While higher-order resolution and |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
175 |
rewriting operate modulo @{text "\<alpha>\<beta>\<eta>"}-conversion, some other tools |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
176 |
might look at terms more discretely. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
177 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
178 |
\item @{ML goals_limit} controls the maximum number of subgoals to |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
179 |
be shown in goal output. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
180 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
181 |
\item @{ML Proof.show_main_goal} controls whether the main result to |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
182 |
be proven should be displayed. This information might be relevant |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
183 |
for schematic goals, to inspect the current claim that has been |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
184 |
synthesized so far. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
185 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
186 |
\item @{ML show_hyps} controls printing of implicit hypotheses of |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
187 |
local facts. Normally, only those hypotheses are displayed that are |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
188 |
\emph{not} covered by the assumptions of the current context: this |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
189 |
situation indicates a fault in some tool being used. |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
190 |
|
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
191 |
By setting @{ML show_hyps} to @{ML true}, output of \emph{all} |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
192 |
hypotheses can be enforced, which is occasionally useful for |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
193 |
diagnostic purposes. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
194 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
195 |
\item @{ML show_tags} controls printing of extra annotations within |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
196 |
theorems, such as internal position information, or the case names |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
197 |
being attached by the attribute @{attribute case_names}. |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
198 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
199 |
Note that the @{attribute tagged} and @{attribute untagged} |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
200 |
attributes provide low-level access to the collection of tags |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
201 |
associated with a theorem. |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
202 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
203 |
\item @{ML show_question_marks} controls printing of question marks |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
204 |
for schematic variables, such as @{text ?x}. Only the leading |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
205 |
question mark is affected, the remaining text is unchanged |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
206 |
(including proper markup for schematic variables that might be |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
207 |
relevant for user interfaces). |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
208 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
209 |
\end{description} |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
210 |
*} |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
211 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
212 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
213 |
subsection {* Printing limits *} |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
214 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
215 |
text {* |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
216 |
\begin{mldecls} |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
217 |
@{index_ML Pretty.setdepth: "int -> unit"} \\ |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
218 |
@{index_ML Pretty.setmargin: "int -> unit"} \\ |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
219 |
@{index_ML print_depth: "int -> unit"} \\ |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
220 |
\end{mldecls} |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
221 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
222 |
These ML functions set limits for pretty printed text. |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
223 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
224 |
\begin{description} |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
225 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
226 |
\item @{ML Pretty.setdepth}~@{text d} tells the pretty printer to |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
227 |
limit the printing depth to @{text d}. This affects the display of |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
228 |
types, terms, theorems etc. The default value is 0, which permits |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
229 |
printing to an arbitrary depth. Other useful values for @{text d} |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
230 |
are 10 and 20. |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
231 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
232 |
\item @{ML Pretty.setmargin}~@{text m} tells the pretty printer to |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
233 |
assume a right margin (page width) of @{text m}. The initial margin |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
234 |
is 76, but user interfaces might adapt the margin automatically when |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
235 |
resizing windows. |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
236 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
237 |
\item @{ML print_depth}~@{text n} limits the printing depth of the |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
238 |
ML toplevel pretty printer; the precise effect depends on the ML |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
239 |
compiler and run-time system. Typically @{text n} should be less |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
240 |
than 10. Bigger values such as 100--1000 are useful for debugging. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
241 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
242 |
\end{description} |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
243 |
*} |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
244 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
245 |
|
28762 | 246 |
section {* Mixfix annotations *} |
247 |
||
248 |
text {* Mixfix annotations specify concrete \emph{inner syntax} of |
|
28767 | 249 |
Isabelle types and terms. Some commands such as @{command |
250 |
"typedecl"} admit infixes only, while @{command "definition"} etc.\ |
|
251 |
support the full range of general mixfixes and binders. Fixed |
|
252 |
parameters in toplevel theorem statements, locale specifications |
|
253 |
also admit mixfix annotations. |
|
28762 | 254 |
|
255 |
\indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} |
|
256 |
\begin{rail} |
|
257 |
infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')' |
|
258 |
; |
|
259 |
mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')' |
|
260 |
; |
|
261 |
structmixfix: mixfix | '(' 'structure' ')' |
|
262 |
; |
|
263 |
||
264 |
prios: '[' (nat + ',') ']' |
|
265 |
; |
|
266 |
\end{rail} |
|
267 |
||
268 |
Here the \railtok{string} specifications refer to the actual mixfix |
|
269 |
template, which may include literal text, spacing, blocks, and |
|
270 |
arguments (denoted by ``@{text _}''); the special symbol |
|
271 |
``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index |
|
272 |
argument that specifies an implicit structure reference (see also |
|
273 |
\secref{sec:locale}). Infix and binder declarations provide common |
|
274 |
abbreviations for particular mixfix declarations. So in practice, |
|
275 |
mixfix templates mostly degenerate to literal text for concrete |
|
276 |
syntax, such as ``@{verbatim "++"}'' for an infix symbol. |
|
277 |
||
278 |
\medskip In full generality, mixfix declarations work as follows. |
|
279 |
Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is |
|
280 |
annotated by @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text |
|
281 |
"mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of |
|
282 |
delimiters that surround argument positions as indicated by |
|
283 |
underscores. |
|
284 |
||
285 |
Altogether this determines a production for a context-free priority |
|
286 |
grammar, where for each argument @{text "i"} the syntactic category |
|
287 |
is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and |
|
288 |
the result category is determined from @{text "\<tau>"} (with |
|
289 |
priority @{text "p"}). Priority specifications are optional, with |
|
290 |
default 0 for arguments and 1000 for the result. |
|
291 |
||
292 |
Since @{text "\<tau>"} may be again a function type, the constant |
|
293 |
type scheme may have more argument positions than the mixfix |
|
294 |
pattern. Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for |
|
295 |
@{text "m > n"} works by attaching concrete notation only to the |
|
296 |
innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"} |
|
297 |
instead. If a term has fewer arguments than specified in the mixfix |
|
298 |
template, the concrete syntax is ignored. |
|
299 |
||
300 |
\medskip A mixfix template may also contain additional directives |
|
301 |
for pretty printing, notably spaces, blocks, and breaks. The |
|
302 |
general template format is a sequence over any of the following |
|
303 |
entities. |
|
304 |
||
305 |
\begin{itemize} |
|
306 |
||
307 |
\item @{text "\<^bold>d"} is a delimiter, namely a non-empty |
|
308 |
sequence of characters other than the special characters @{text "'"} |
|
309 |
(single quote), @{text "_"} (underscore), @{text "\<index>"} (index |
|
310 |
symbol), @{text "/"} (slash), @{text "("} and @{text ")"} |
|
311 |
(parentheses). |
|
312 |
||
313 |
A single quote escapes the special meaning of these meta-characters, |
|
314 |
producing a literal version of the following character, unless that |
|
315 |
is a blank. A single quote followed by a blank separates |
|
316 |
delimiters, without affecting printing, but input tokens may have |
|
317 |
additional white space here. |
|
318 |
||
319 |
\item @{text "_"} is an argument position, which stands for a |
|
320 |
certain syntactic category in the underlying grammar. |
|
321 |
||
322 |
\item @{text "\<index>"} is an indexed argument position; this is |
|
323 |
the place where implicit structure arguments can be attached. |
|
324 |
||
325 |
\item @{text "\<^bold>s"} is a non-empty sequence of spaces for |
|
326 |
printing. This and the following specifications do not affect |
|
327 |
parsing at all. |
|
328 |
||
329 |
\item @{text "(\<^bold>n"} opens a pretty printing block. The |
|
330 |
optional number specifies how much indentation to add when a line |
|
331 |
break occurs within the block. If the parenthesis is not followed |
|
332 |
by digits, the indentation defaults to 0. A block specified via |
|
333 |
@{text "(00"} is unbreakable. |
|
334 |
||
335 |
\item @{text ")"} closes a pretty printing block. |
|
336 |
||
337 |
\item @{text "//"} forces a line break. |
|
338 |
||
339 |
\item @{text "/\<^bold>s"} allows a line break. Here @{text |
|
340 |
"\<^bold>s"} stands for the string of spaces (zero or more) right |
|
341 |
after the slash. These spaces are printed if the break is |
|
342 |
\emph{not} taken. |
|
343 |
||
344 |
\end{itemize} |
|
345 |
||
346 |
For example, the template @{text "(_ +/ _)"} specifies an infix |
|
347 |
operator. There are two argument positions; the delimiter @{text |
|
348 |
"+"} is preceded by a space and followed by a space or line break; |
|
349 |
the entire phrase is a pretty printing block. |
|
350 |
||
351 |
The general idea of pretty printing with blocks and breaks is also |
|
352 |
described in \cite{paulson-ml2}. |
|
353 |
*} |
|
354 |
||
355 |
||
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
356 |
section {* Explicit term notation *} |
28762 | 357 |
|
358 |
text {* |
|
359 |
\begin{matharray}{rcll} |
|
360 |
@{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
|
361 |
@{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
|
362 |
\end{matharray} |
|
363 |
||
364 |
\begin{rail} |
|
365 |
('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and') |
|
366 |
; |
|
367 |
\end{rail} |
|
368 |
||
369 |
\begin{description} |
|
370 |
||
371 |
\item @{command "notation"}~@{text "c (mx)"} associates mixfix |
|
372 |
syntax with an existing constant or fixed variable. This is a |
|
373 |
robust interface to the underlying @{command "syntax"} primitive |
|
374 |
(\secref{sec:syn-trans}). Type declaration and internal syntactic |
|
375 |
representation of the given entity is retrieved from the context. |
|
376 |
||
377 |
\item @{command "no_notation"} is similar to @{command "notation"}, |
|
378 |
but removes the specified syntax annotation from the present |
|
379 |
context. |
|
380 |
||
381 |
\end{description} |
|
382 |
*} |
|
383 |
||
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
384 |
section {* The Pure syntax *} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
385 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
386 |
subsection {* Priority grammars *} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
387 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
388 |
text {* A context-free grammar consists of a set of \emph{terminal |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
389 |
symbols}, a set of \emph{nonterminal symbols} and a set of |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
390 |
\emph{productions}. Productions have the form @{text "A = \<gamma>"}, |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
391 |
where @{text A} is a nonterminal and @{text \<gamma>} is a string of |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
392 |
terminals and nonterminals. One designated nonterminal is called |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
393 |
the \emph{root symbol}. The language defined by the grammar |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
394 |
consists of all strings of terminals that can be derived from the |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
395 |
root symbol by applying productions as rewrite rules. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
396 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
397 |
The standard Isabelle parser for inner syntax uses a \emph{priority |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
398 |
grammar}. Each nonterminal is decorated by an integer priority: |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
399 |
@{text "A\<^sup>(\<^sup>p\<^sup>)"}. In a derivation, @{text "A\<^sup>(\<^sup>p\<^sup>)"} may be rewritten |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
400 |
using a production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} only if @{text "p \<le> q"}. Any |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
401 |
priority grammar can be translated into a normal context-free |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
402 |
grammar by introducing new nonterminals and productions. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
403 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
404 |
\medskip Formally, a set of context free productions @{text G} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
405 |
induces a derivation relation @{text "\<longrightarrow>\<^sub>G"} as follows. Let @{text |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
406 |
\<alpha>} and @{text \<beta>} denote strings of terminal or nonterminal symbols. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
407 |
Then |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
408 |
\[ |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
409 |
@{text "\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>"} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
410 |
\] |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
411 |
if and only if @{text G} contains some production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
412 |
for @{text "p \<le> q"}. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
413 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
414 |
\medskip The following grammar for arithmetic expressions |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
415 |
demonstrates how binding power and associativity of operators can be |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
416 |
enforced by priorities. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
417 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
418 |
\begin{center} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
419 |
\begin{tabular}{rclr} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
420 |
@{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim 0} \\ |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
421 |
@{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim "("} @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim ")"} \\ |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
422 |
@{text "A\<^sup>(\<^sup>0\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} \\ |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
423 |
@{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} \\ |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
424 |
@{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "="} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} \\ |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
425 |
\end{tabular} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
426 |
\end{center} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
427 |
The choice of priorities determines that @{verbatim "-"} binds |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
428 |
tighter than @{verbatim "*"}, which binds tighter than @{verbatim |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
429 |
"+"}. Furthermore @{verbatim "+"} associates to the left and |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
430 |
@{verbatim "*"} to the right. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
431 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
432 |
\medskip For clarity, grammars obey these conventions: |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
433 |
\begin{itemize} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
434 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
435 |
\item All priorities must lie between 0 and 1000. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
436 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
437 |
\item Priority 0 on the right-hand side and priority 1000 on the |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
438 |
left-hand side may be omitted. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
439 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
440 |
\item The production @{text "A\<^sup>(\<^sup>p\<^sup>) = \<alpha>"} is written as @{text "A = \<alpha> |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
441 |
(p)"}, i.e.\ the priority of the left-hand side actually appears in |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
442 |
a column on the far right. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
443 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
444 |
\item Alternatives are separated by @{text "|"}. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
445 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
446 |
\item Repetition is indicated by dots @{text "(\<dots>)"} in an informal |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
447 |
but obvious way. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
448 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
449 |
\end{itemize} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
450 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
451 |
Using these conventions, the example grammar specification above |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
452 |
takes the form: |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
453 |
\begin{center} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
454 |
\begin{tabular}{rclc} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
455 |
@{text A} & @{text "="} & @{verbatim 0} & \qquad\qquad \\ |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
456 |
& @{text "|"} & @{verbatim "("} @{text A} @{verbatim ")"} \\ |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
457 |
& @{text "|"} & @{text A} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} & @{text "(0)"} \\ |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
458 |
& @{text "|"} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
459 |
& @{text "|"} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
460 |
\end{tabular} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
461 |
\end{center} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
462 |
*} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
463 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
464 |
|
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
465 |
subsection {* The Pure grammar *} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
466 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
467 |
text {* |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
468 |
\begin{figure}[htb]\small |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
469 |
\begin{center} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
470 |
\begin{tabular}{rclc} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
471 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
472 |
@{text any} & = & @{text "prop | logic"} \\\\ |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
473 |
% FIXME |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
474 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
475 |
\end{tabular} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
476 |
\end{center} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
477 |
\caption{The Pure grammar}\label{fig:pure-grammar} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
478 |
\end{figure} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
479 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
480 |
The priority grammar of the @{text "Pure"} theory is defined in |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
481 |
\figref{fig:pure-grammar}. The following nonterminals are |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
482 |
introduced: |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
483 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
484 |
\begin{description} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
485 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
486 |
\item @{text "any"} denotes any term. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
487 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
488 |
\item @{text "prop"} denotes meta-level propositions, which are |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
489 |
terms of type @{typ prop}. The syntax of such formulae of the |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
490 |
meta-logic is carefully distinguished from usual conventions for |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
491 |
object-logics. In particular, plain @{text "\<lambda>"}-term |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
492 |
notation is \emph{not} recognized as @{text "prop"}. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
493 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
494 |
\item @{text aprop} denotes atomic propositions, which are embedded |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
495 |
into regular @{typ prop} by means of an explicit @{text "PROP"} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
496 |
token. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
497 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
498 |
Terms of type @{typ prop} with non-constant head, e.g.\ a plain |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
499 |
variable, are printed in this form. Constants that yield type @{typ |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
500 |
prop} are expected to provide their own concrete syntax; otherwise |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
501 |
the printed version will appear like @{typ logic} and cannot be |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
502 |
parsed again as @{typ prop}. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
503 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
504 |
\item @{text logic} denotes arbitrary terms of a logical type, |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
505 |
excluding type @{typ prop}. This is the main syntactic category of |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
506 |
object-logic entities, covering plain @{text \<lambda>}-term notation |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
507 |
(variables, abstraction, application), plus anything defined by the |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
508 |
user. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
509 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
510 |
When specifying notation for logical entities, all logical types |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
511 |
(excluding @{typ prop}) are \emph{collapsed} to this single category |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
512 |
of @{typ logic}. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
513 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
514 |
\item @{text idt} denotes identifiers, possibly constrained by |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
515 |
types. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
516 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
517 |
\item @{text idts} denotes a sequence of @{text idt}. This is the |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
518 |
most basic category for variables in iterated binders, such as |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
519 |
@{text "\<lambda>"} or @{text "\<And>"}. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
520 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
521 |
\item @{text pttrn} and @{text pttrns} denote patterns for |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
522 |
abstraction, cases bindings etc. In Pure, these categories start as |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
523 |
a merely copy of @{text idt} and @{text idts}, respectively. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
524 |
Object-logics may add additional productions for binding forms. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
525 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
526 |
\item @{text type} denotes types of the meta-logic. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
527 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
528 |
\item @{text sort} denotes meta-level sorts. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
529 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
530 |
\end{description} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
531 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
532 |
\begin{warn} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
533 |
In @{text idts}, note that @{text "x :: nat y"} is parsed as @{text |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
534 |
"x :: (nat y)"}, treating @{text y} like a type constructor applied |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
535 |
to @{text nat}. To avoid this interpretation, write @{text "(x :: |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
536 |
nat) y"} with explicit parentheses. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
537 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
538 |
Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x :: |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
539 |
(nat y :: nat)"}. The correct form is @{text "(x :: nat) (y :: |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
540 |
nat)"}, or @{text "(x :: nat) y :: nat"} if @{text y} is last in the |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
541 |
sequence of identifiers. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
542 |
\end{warn} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
543 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
544 |
\begin{warn} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
545 |
Type constraints for terms bind very weakly. For example, @{text "x |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
546 |
< y :: nat"} is normally parsed as @{text "(x < y) :: nat"}, unless |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
547 |
@{text "<"} has a very low priority, in which case the input is |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
548 |
likely to be ambiguous. The correct form is @{text "x < (y :: nat)"}. |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
549 |
\end{warn} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
550 |
*} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
551 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
552 |
|
28762 | 553 |
section {* Syntax and translations \label{sec:syn-trans} *} |
554 |
||
555 |
text {* |
|
556 |
\begin{matharray}{rcl} |
|
557 |
@{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
558 |
@{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
559 |
@{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
560 |
@{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
561 |
@{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
562 |
\end{matharray} |
|
563 |
||
564 |
\begin{rail} |
|
565 |
'nonterminals' (name +) |
|
566 |
; |
|
567 |
('syntax' | 'no\_syntax') mode? (constdecl +) |
|
568 |
; |
|
569 |
('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +) |
|
570 |
; |
|
571 |
||
572 |
mode: ('(' ( name | 'output' | name 'output' ) ')') |
|
573 |
; |
|
574 |
transpat: ('(' nameref ')')? string |
|
575 |
; |
|
576 |
\end{rail} |
|
577 |
||
578 |
\begin{description} |
|
579 |
||
580 |
\item @{command "nonterminals"}~@{text c} declares a type |
|
581 |
constructor @{text c} (without arguments) to act as purely syntactic |
|
582 |
type: a nonterminal symbol of the inner syntax. |
|
583 |
||
584 |
\item @{command "syntax"}~@{text "(mode) decls"} is similar to |
|
585 |
@{command "consts"}~@{text decls}, except that the actual logical |
|
586 |
signature extension is omitted. Thus the context free grammar of |
|
587 |
Isabelle's inner syntax may be augmented in arbitrary ways, |
|
588 |
independently of the logic. The @{text mode} argument refers to the |
|
589 |
print mode that the grammar rules belong; unless the @{keyword_ref |
|
590 |
"output"} indicator is given, all productions are added both to the |
|
591 |
input and output grammar. |
|
592 |
||
593 |
\item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar |
|
594 |
declarations (and translations) resulting from @{text decls}, which |
|
595 |
are interpreted in the same manner as for @{command "syntax"} above. |
|
596 |
||
597 |
\item @{command "translations"}~@{text rules} specifies syntactic |
|
598 |
translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}), |
|
599 |
parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}). |
|
600 |
Translation patterns may be prefixed by the syntactic category to be |
|
601 |
used for parsing; the default is @{text logic}. |
|
602 |
||
603 |
\item @{command "no_translations"}~@{text rules} removes syntactic |
|
604 |
translation rules, which are interpreted in the same manner as for |
|
605 |
@{command "translations"} above. |
|
606 |
||
607 |
\end{description} |
|
608 |
*} |
|
609 |
||
610 |
||
611 |
section {* Syntax translation functions *} |
|
612 |
||
613 |
text {* |
|
614 |
\begin{matharray}{rcl} |
|
615 |
@{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
616 |
@{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
617 |
@{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
618 |
@{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
619 |
@{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
620 |
\end{matharray} |
|
621 |
||
622 |
\begin{rail} |
|
623 |
( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | |
|
624 |
'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text |
|
625 |
; |
|
626 |
\end{rail} |
|
627 |
||
628 |
Syntax translation functions written in ML admit almost arbitrary |
|
629 |
manipulations of Isabelle's inner syntax. Any of the above commands |
|
630 |
have a single \railqtok{text} argument that refers to an ML |
|
631 |
expression of appropriate type, which are as follows by default: |
|
632 |
||
633 |
%FIXME proper antiquotations |
|
634 |
\begin{ttbox} |
|
635 |
val parse_ast_translation : (string * (ast list -> ast)) list |
|
636 |
val parse_translation : (string * (term list -> term)) list |
|
637 |
val print_translation : (string * (term list -> term)) list |
|
638 |
val typed_print_translation : |
|
639 |
(string * (bool -> typ -> term list -> term)) list |
|
640 |
val print_ast_translation : (string * (ast list -> ast)) list |
|
641 |
\end{ttbox} |
|
642 |
||
643 |
If the @{text "(advanced)"} option is given, the corresponding |
|
644 |
translation functions may depend on the current theory or proof |
|
645 |
context. This allows to implement advanced syntax mechanisms, as |
|
646 |
translations functions may refer to specific theory declarations or |
|
647 |
auxiliary proof data. |
|
648 |
||
649 |
See also \cite[\S8]{isabelle-ref} for more information on the |
|
650 |
general concept of syntax transformations in Isabelle. |
|
651 |
||
652 |
%FIXME proper antiquotations |
|
653 |
\begin{ttbox} |
|
654 |
val parse_ast_translation: |
|
655 |
(string * (Proof.context -> ast list -> ast)) list |
|
656 |
val parse_translation: |
|
657 |
(string * (Proof.context -> term list -> term)) list |
|
658 |
val print_translation: |
|
659 |
(string * (Proof.context -> term list -> term)) list |
|
660 |
val typed_print_translation: |
|
661 |
(string * (Proof.context -> bool -> typ -> term list -> term)) list |
|
662 |
val print_ast_translation: |
|
663 |
(string * (Proof.context -> ast list -> ast)) list |
|
664 |
\end{ttbox} |
|
665 |
*} |
|
666 |
||
667 |
end |