4
+ − 1
theory Parsing
321
+ − 2
imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package"
4
+ − 3
begin
+ − 4
346
+ − 5
(*<*)
+ − 6
setup {*
+ − 7
open_file_with_prelude
+ − 8
"Parsing_Code.thy"
+ − 9
["theory Parsing",
+ − 10
"imports Base \"Package/Simple_Inductive_Package\"",
+ − 11
"begin"]
+ − 12
*}
+ − 13
(*>*)
+ − 14
414
+ − 15
chapter {* Parsing\label{chp:parsing} *}
4
+ − 16
+ − 17
text {*
421
+ − 18
\begin{flushright}
+ − 19
{\em An important principle underlying the success and popularity of Unix\\ is
+ − 20
the philosophy of building on the work of others.} \\[1ex]
+ − 21
Linus Torwalds in the email exchange\\ with Andrew S.~Tannenbaum
+ − 22
\end{flushright}
+ − 23
+ − 24
321
+ − 25
Isabelle distinguishes between \emph{outer} and \emph{inner}
+ − 26
syntax. Commands, such as \isacommand{definition}, \isacommand{inductive}
+ − 27
and so on, belong to the outer syntax, whereas terms, types and so on belong
+ − 28
to the inner syntax. For parsing inner syntax, Isabelle uses a rather
+ − 29
general and sophisticated algorithm, which is driven by priority
+ − 30
grammars. Parsers for outer syntax are built up by functional parsing
+ − 31
combinators. These combinators are a well-established technique for parsing,
+ − 32
which has, for example, been described in Paulson's classic ML-book
+ − 33
\cite{paulson-ml2}. Isabelle developers are usually concerned with writing
+ − 34
these outer syntax parsers, either for new definitional packages or for
+ − 35
calling methods with specific arguments.
42
+ − 36
+ − 37
\begin{readmore}
236
+ − 38
The library for writing parser combinators is split up, roughly, into two
326
+ − 39
parts: The first part consists of a collection of generic parser combinators
236
+ − 40
defined in the structure @{ML_struct Scan} in the file @{ML_file
+ − 41
"Pure/General/scan.ML"}. The second part of the library consists of
+ − 42
combinators for dealing with specific token types, which are defined in the
426
+ − 43
structure @{ML_struct Parse} in the file @{ML_file
424
+ − 44
"Pure/Isar/parse.ML"}. In addition specific parsers for packages are
+ − 45
defined in @{ML_file "Pure/Isar/parse_spec.ML"}. Parsers for method arguments
326
+ − 46
are defined in @{ML_file "Pure/Isar/args.ML"}.
42
+ − 47
\end{readmore}
38
+ − 48
+ − 49
*}
+ − 50
49
+ − 51
section {* Building Generic Parsers *}
38
+ − 52
+ − 53
text {*
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 54
240
+ − 55
Let us first have a look at parsing strings using generic parsing
344
+ − 56
combinators. The function @{ML_ind "$$" in Scan} takes a string as argument and will
240
+ − 57
``consume'' this string from a given input list of strings. ``Consume'' in
+ − 58
this context means that it will return a pair consisting of this string and
+ − 59
the rest of the input list. For example:
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 60
240
+ − 61
@{ML_response [display,gray]
+ − 62
"($$ \"h\") (Symbol.explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 63
240
+ − 64
@{ML_response [display,gray]
+ − 65
"($$ \"w\") (Symbol.explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 66
240
+ − 67
The function @{ML "$$"} will either succeed (as in the two examples above)
+ − 68
or raise the exception @{text "FAIL"} if no string can be consumed. For
+ − 69
example trying to parse
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 70
240
+ − 71
@{ML_response_fake [display,gray]
+ − 72
"($$ \"x\") (Symbol.explode \"world\")"
+ − 73
"Exception FAIL raised"}
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 74
240
+ − 75
will raise the exception @{text "FAIL"}. There are three exceptions used in
+ − 76
the parsing combinators:
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 77
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 78
\begin{itemize}
58
+ − 79
\item @{text "FAIL"} is used to indicate that alternative routes of parsing
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 80
might be explored.
58
+ − 81
\item @{text "MORE"} indicates that there is not enough input for the parser. For example
+ − 82
in @{text "($$ \"h\") []"}.
60
5b9c6010897b
doem tuning and made the cookbook work again with recent changes (CookBook/Package/Ind_Interface.thy needs to be looked at to see what the problem with the new parser type is)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 83
\item @{text "ABORT"} is the exception that is raised when a dead end is reached.
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 84
It is used for example in the function @{ML "!!"} (see below).
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 85
\end{itemize}
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 86
50
+ − 87
However, note that these exceptions are private to the parser and cannot be accessed
49
+ − 88
by the programmer (for example to handle them).
240
+ − 89
357
+ − 90
In the examples above we use the function @{ML_ind explode in Symbol} from the
344
+ − 91
structure @{ML_struct Symbol}, instead of the more standard library function
369
+ − 92
@{ML_ind explode in String}, for obtaining an input list for the parser. The reason is
+ − 93
that @{ML explode} in @{ML_struct Symbol} is aware of character
344
+ − 94
sequences, for example @{text "\<foo>"}, that have a special meaning in
+ − 95
Isabelle. To see the difference consider
240
+ − 96
+ − 97
@{ML_response_fake [display,gray]
+ − 98
"let
261
+ − 99
val input = \"\<foo> bar\"
240
+ − 100
in
+ − 101
(explode input, Symbol.explode input)
+ − 102
end"
+ − 103
"([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"],
261
+ − 104
[\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
240
+ − 105
256
+ − 106
Slightly more general than the parser @{ML "$$"} is the function
344
+ − 107
@{ML_ind one in Scan}, in that it takes a predicate as argument and
256
+ − 108
then parses exactly
52
+ − 109
one item from the input list satisfying this predicate. For example the
58
+ − 110
following parser either consumes an @{text [quotes] "h"} or a @{text
49
+ − 111
[quotes] "w"}:
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 112
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 113
@{ML_response [display,gray]
40
+ − 114
"let
+ − 115
val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")
240
+ − 116
val input1 = Symbol.explode \"hello\"
+ − 117
val input2 = Symbol.explode \"world\"
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 118
in
236
+ − 119
(hw input1, hw input2)
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 120
end"
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 121
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 122
344
+ − 123
Two parsers can be connected in sequence by using the function @{ML_ind "--" in Scan}.
220
+ − 124
For example parsing @{text "h"}, @{text "e"} and @{text "l"} (in this
+ − 125
order) you can achieve by:
38
+ − 126
236
+ − 127
@{ML_response [display,gray]
240
+ − 128
"($$ \"h\" -- $$ \"e\" -- $$ \"l\") (Symbol.explode \"hello\")"
236
+ − 129
"(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 130
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 131
Note how the result of consumed strings builds up on the left as nested pairs.
38
+ − 132
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 133
If, as in the previous example, you want to parse a particular string,
326
+ − 134
then you can use the function @{ML_ind this_string in Scan}.
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 135
236
+ − 136
@{ML_response [display,gray]
240
+ − 137
"Scan.this_string \"hell\" (Symbol.explode \"hello\")"
236
+ − 138
"(\"hell\", [\"o\"])"}
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 139
256
+ − 140
Parsers that explore alternatives can be constructed using the function
344
+ − 141
@{ML_ind "||" in Scan}. The parser @{ML "(p || q)" for p q} returns the
58
+ − 142
result of @{text "p"}, in case it succeeds, otherwise it returns the
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 143
result of @{text "q"}. For example:
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 144
38
+ − 145
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 146
@{ML_response [display,gray]
40
+ − 147
"let
236
+ − 148
val hw = $$ \"h\" || $$ \"w\"
240
+ − 149
val input1 = Symbol.explode \"hello\"
+ − 150
val input2 = Symbol.explode \"world\"
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 151
in
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 152
(hw input1, hw input2)
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 153
end"
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 154
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
38
+ − 155
344
+ − 156
The functions @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} work like the sequencing
321
+ − 157
function for parsers, except that they discard the item being parsed by the
357
+ − 158
first (respectively second) parser. That means the item being dropped is the
+ − 159
one that @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} ``point'' away.
+ − 160
For example:
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 161
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 162
@{ML_response [display,gray]
40
+ − 163
"let
236
+ − 164
val just_e = $$ \"h\" |-- $$ \"e\"
+ − 165
val just_h = $$ \"h\" --| $$ \"e\"
240
+ − 166
val input = Symbol.explode \"hello\"
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 167
in
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 168
(just_e input, just_h input)
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 169
end"
241
+ − 170
"((\"e\", [\"l\", \"l\", \"o\"]), (\"h\", [\"l\", \"l\", \"o\"]))"}
38
+ − 171
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 172
The parser @{ML "Scan.optional p x" for p x} returns the result of the parser
58
+ − 173
@{text "p"}, if it succeeds; otherwise it returns
104
+ − 174
the default value @{text "x"}. For example:
38
+ − 175
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 176
@{ML_response [display,gray]
40
+ − 177
"let
+ − 178
val p = Scan.optional ($$ \"h\") \"x\"
240
+ − 179
val input1 = Symbol.explode \"hello\"
+ − 180
val input2 = Symbol.explode \"world\"
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 181
in
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 182
(p input1, p input2)
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 183
end"
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 184
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 185
344
+ − 186
The function @{ML_ind option in Scan} works similarly, except no default value can
50
+ − 187
be given. Instead, the result is wrapped as an @{text "option"}-type. For example:
+ − 188
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 189
@{ML_response [display,gray]
50
+ − 190
"let
+ − 191
val p = Scan.option ($$ \"h\")
240
+ − 192
val input1 = Symbol.explode \"hello\"
+ − 193
val input2 = Symbol.explode \"world\"
50
+ − 194
in
+ − 195
(p input1, p input2)
+ − 196
end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
49
+ − 197
344
+ − 198
The function @{ML_ind ahead in Scan} parses some input, but leaves the original
326
+ − 199
input unchanged. For example:
+ − 200
+ − 201
@{ML_response [display,gray]
+ − 202
"Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")"
+ − 203
"(\"foo\", [\"f\", \"o\", \"o\"])"}
+ − 204
344
+ − 205
The function @{ML_ind "!!" in Scan} helps with producing appropriate error messages
326
+ − 206
during parsing. For example if you want to parse @{text p} immediately
58
+ − 207
followed by @{text q}, or start a completely different parser @{text r},
104
+ − 208
you might write:
40
+ − 209
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 210
@{ML [display,gray] "(p -- q) || r" for p q r}
40
+ − 211
326
+ − 212
However, this parser is problematic for producing a useful error
+ − 213
message, if the parsing of @{ML "(p -- q)" for p q} fails. Because with the
+ − 214
parser above you lose the information that @{text p} should be followed by @{text q}.
220
+ − 215
To see this assume that @{text p} is present in the input, but it is not
+ − 216
followed by @{text q}. That means @{ML "(p -- q)" for p q} will fail and
+ − 217
hence the alternative parser @{text r} will be tried. However, in many
236
+ − 218
circumstances this will be the wrong parser for the input ``@{text "p"}-followed-by-something''
220
+ − 219
and therefore will also fail. The error message is then caused by the failure
+ − 220
of @{text r}, not by the absence of @{text q} in the input. This kind of
+ − 221
situation can be avoided when using the function @{ML "!!"}. This function
+ − 222
aborts the whole process of parsing in case of a failure and prints an error
+ − 223
message. For example if you invoke the parser
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 224
40
+ − 225
236
+ − 226
@{ML [display,gray] "!! (fn _ => \"foo\") ($$ \"h\")"}
40
+ − 227
58
+ − 228
on @{text [quotes] "hello"}, the parsing succeeds
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 229
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 230
@{ML_response [display,gray]
240
+ − 231
"(!! (fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")"
236
+ − 232
"(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
40
+ − 233
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 234
but if you invoke it on @{text [quotes] "world"}
40
+ − 235
240
+ − 236
@{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 237
"Exception ABORT raised"}
40
+ − 238
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 239
then the parsing aborts and the error message @{text "foo"} is printed. In order to
120
+ − 240
see the error message properly, you need to prefix the parser with the function
344
+ − 241
@{ML_ind error in Scan}. For example:
40
+ − 242
236
+ − 243
@{ML_response_fake [display,gray]
+ − 244
"Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
+ − 245
"Exception Error \"foo\" raised"}
40
+ − 246
426
+ − 247
This ``prefixing'' is usually done by wrappers such as @{ML_ind local_theory in Outer_Syntax}
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 248
(see Section~\ref{sec:newcommand} which explains this function in more detail).
40
+ − 249
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 250
Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
326
+ − 251
r}. If you want to generate the correct error message for failure
+ − 252
of parsing @{text "p"}-followed-by-@{text "q"}, then you have to write:
38
+ − 253
*}
+ − 254
69
+ − 255
ML{*fun p_followed_by_q p q r =
133
+ − 256
let
236
+ − 257
val err_msg = fn _ => p ^ " is not followed by " ^ q
133
+ − 258
in
+ − 259
($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
+ − 260
end *}
38
+ − 261
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 262
40
+ − 263
text {*
220
+ − 264
Running this parser with the arguments
+ − 265
@{text [quotes] "h"}, @{text [quotes] "e"} and @{text [quotes] "w"}, and
65
+ − 266
the input @{text [quotes] "holle"}
40
+ − 267
240
+ − 268
@{ML_response_fake [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"holle\")"
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 269
"Exception ERROR \"h is not followed by e\" raised"}
40
+ − 270
65
+ − 271
produces the correct error message. Running it with
40
+ − 272
240
+ − 273
@{ML_response [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"wworld\")"
40
+ − 274
"((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
+ − 275
+ − 276
yields the expected parsing.
38
+ − 277
58
+ − 278
The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 279
often as it succeeds. For example:
40
+ − 280
240
+ − 281
@{ML_response [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")"
40
+ − 282
"([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
+ − 283
344
+ − 284
Note that @{ML_ind repeat in Scan} stores the parsed items in a list. The function
+ − 285
@{ML_ind repeat1 in Scan} is similar, but requires that the parser @{text "p"}
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 286
succeeds at least once.
48
+ − 287
58
+ − 288
Also note that the parser would have aborted with the exception @{text MORE}, if
326
+ − 289
you had it run with the string @{text [quotes] "hhhh"}. This can be avoided by using
344
+ − 290
the wrapper @{ML_ind finite in Scan} and the ``stopper-token''
+ − 291
@{ML_ind stopper in Symbol}. With them you can write:
49
+ − 292
240
+ − 293
@{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")"
49
+ − 294
"([\"h\", \"h\", \"h\", \"h\"], [])"}
+ − 295
326
+ − 296
The function @{ML stopper in Symbol} is the ``end-of-input'' indicator for parsing strings;
128
+ − 297
other stoppers need to be used when parsing, for example, tokens. However, this kind of
65
+ − 298
manually wrapping is often already done by the surrounding infrastructure.
49
+ − 299
344
+ − 300
The function @{ML_ind repeat in Scan} can be used with @{ML_ind one in Scan} to read any
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 301
string as in
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 302
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 303
@{ML_response [display,gray]
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 304
"let
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 305
val p = Scan.repeat (Scan.one Symbol.not_eof)
240
+ − 306
val input = Symbol.explode \"foo bar foo\"
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 307
in
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 308
Scan.finite Symbol.stopper p input
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 309
end"
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 310
"([\"f\", \"o\", \"o\", \" \", \"b\", \"a\", \"r\", \" \", \"f\", \"o\", \"o\"], [])"}
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 311
344
+ − 312
where the function @{ML_ind not_eof in Symbol} ensures that we do not read beyond the
65
+ − 313
end of the input string (i.e.~stopper symbol).
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 314
344
+ − 315
The function @{ML_ind unless in Scan} takes two parsers: if the first one can
60
5b9c6010897b
doem tuning and made the cookbook work again with recent changes (CookBook/Package/Ind_Interface.thy needs to be looked at to see what the problem with the new parser type is)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 316
parse the input, then the whole parser fails; if not, then the second is tried. Therefore
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 317
240
+ − 318
@{ML_response_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 319
"Exception FAIL raised"}
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 320
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 321
fails, while
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 322
240
+ − 323
@{ML_response [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"world\")"
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 324
"(\"w\",[\"o\", \"r\", \"l\", \"d\"])"}
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 325
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 326
succeeds.
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 327
344
+ − 328
The functions @{ML_ind repeat in Scan} and @{ML_ind unless in Scan} can
256
+ − 329
be combined to read any input until a certain marker symbol is reached. In the
+ − 330
example below the marker symbol is a @{text [quotes] "*"}.
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 331
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 332
@{ML_response [display,gray]
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 333
"let
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 334
val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))
240
+ − 335
val input1 = Symbol.explode \"fooooo\"
+ − 336
val input2 = Symbol.explode \"foo*ooo\"
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 337
in
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 338
(Scan.finite Symbol.stopper p input1,
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 339
Scan.finite Symbol.stopper p input2)
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 340
end"
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 341
"(([\"f\", \"o\", \"o\", \"o\", \"o\", \"o\"], []),
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 342
([\"f\", \"o\", \"o\"], [\"*\", \"o\", \"o\", \"o\"]))"}
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 343
256
+ − 344
220
+ − 345
After parsing is done, you almost always want to apply a function to the parsed
344
+ − 346
items. One way to do this is the function @{ML_ind ">>" in Scan} where
256
+ − 347
@{ML "(p >> f)" for p f} runs
58
+ − 348
first the parser @{text p} and upon successful completion applies the
+ − 349
function @{text f} to the result. For example
38
+ − 350
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 351
@{ML_response [display,gray]
40
+ − 352
"let
193
+ − 353
fun double (x, y) = (x ^ x, y ^ y)
326
+ − 354
val parser = $$ \"h\" -- $$ \"e\"
40
+ − 355
in
326
+ − 356
(parser >> double) (Symbol.explode \"hello\")
40
+ − 357
end"
+ − 358
"((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}
+ − 359
104
+ − 360
doubles the two parsed input strings; or
59
+ − 361
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 362
@{ML_response [display,gray]
59
+ − 363
"let
104
+ − 364
val p = Scan.repeat (Scan.one Symbol.not_eof)
240
+ − 365
val input = Symbol.explode \"foo bar foo\"
59
+ − 366
in
104
+ − 367
Scan.finite Symbol.stopper (p >> implode) input
59
+ − 368
end"
+ − 369
"(\"foo bar foo\",[])"}
+ − 370
60
5b9c6010897b
doem tuning and made the cookbook work again with recent changes (CookBook/Package/Ind_Interface.thy needs to be looked at to see what the problem with the new parser type is)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 371
where the single-character strings in the parsed output are transformed
59
+ − 372
back into one string.
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 373
344
+ − 374
The function @{ML_ind lift in Scan} takes a parser and a pair as arguments. This function applies
40
+ − 375
the given parser to the second component of the pair and leaves the first component
+ − 376
untouched. For example
38
+ − 377
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 378
@{ML_response [display,gray]
240
+ − 379
"Scan.lift ($$ \"h\" -- $$ \"e\") (1, Symbol.explode \"hello\")"
40
+ − 380
"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
+ − 381
390
+ − 382
\footnote{\bf FIXME: In which situations is @{text "lift"} useful? Give examples.}
+ − 383
397
+ − 384
Be aware of recursive parsers. Suppose you want to read strings separated by
+ − 385
commas and by parentheses into a tree datastructure; for example, generating
+ − 386
the tree corresponding to the string @{text [quotes] "(A, A), (A, A)"} where
+ − 387
the @{text "A"}s will be the leaves. We assume the trees are represented by the
+ − 388
datatype:
390
+ − 389
*}
+ − 390
+ − 391
ML{*datatype tree =
+ − 392
Lf of string
+ − 393
| Br of tree * tree*}
+ − 394
+ − 395
text {*
+ − 396
Since nested parentheses should be treated in a meaningful way---for example
+ − 397
the string @{text [quotes] "((A))"} should be read into a single
+ − 398
leaf---you might implement the following parser.
+ − 399
*}
+ − 400
+ − 401
ML{*fun parse_basic s =
397
+ − 402
$$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")"
+ − 403
390
+ − 404
and parse_tree s =
397
+ − 405
parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s*}
390
+ − 406
+ − 407
text {*
397
+ − 408
This parser corrsponds to the grammar:
+ − 409
+ − 410
\begin{center}
+ − 411
\begin{tabular}{lcl}
+ − 412
@{text "<Basic>"} & @{text "::="} & @{text "<String> | (<Tree>)"}\\
+ − 413
@{text "<Tree>"} & @{text "::="} & @{text "<Basic>, <Tree> | <Basic>"}\\
+ − 414
\end{tabular}
+ − 415
\end{center}
+ − 416
390
+ − 417
The parameter @{text "s"} is the string over which the tree is parsed. The
+ − 418
parser @{ML parse_basic} reads either a leaf or a tree enclosed in
+ − 419
parentheses. The parser @{ML parse_tree} reads either a pair of trees
+ − 420
separated by a comma, or acts like @{ML parse_basic}. Unfortunately,
+ − 421
because of the mutual recursion, this parser will immediately run into a
+ − 422
loop, even if it is called without any input. For example
+ − 423
+ − 424
@{ML_response_fake_both [display, gray]
+ − 425
"parse_tree \"A\""
+ − 426
"*** Exception- TOPLEVEL_ERROR raised"}
+ − 427
+ − 428
raises an exception indicating that the stack limit is reached. Such
392
+ − 429
looping parser are not useful, because of ML's strict evaluation of
390
+ − 430
arguments. Therefore we need to delay the execution of the
+ − 431
parser until an input is given. This can be done by adding the parsed
397
+ − 432
string as an explicit argument. So the parser above should be implemented
+ − 433
as follows.
390
+ − 434
*}
+ − 435
+ − 436
ML{*fun parse_basic s xs =
397
+ − 437
($$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")") xs
+ − 438
390
+ − 439
and parse_tree s xs =
397
+ − 440
(parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s) xs*}
390
+ − 441
+ − 442
text {*
+ − 443
While the type of the parser is unchanged by the addition, its behaviour
+ − 444
changed: with this version of the parser the execution is delayed until
+ − 445
some string is applied for the argument @{text "xs"}. This gives us
+ − 446
exactly the parser what we wanted. An example is as follows:
+ − 447
+ − 448
@{ML_response [display, gray]
+ − 449
"let
+ − 450
val input = Symbol.explode \"(A,((A))),A\"
+ − 451
in
+ − 452
Scan.finite Symbol.stopper (parse_tree \"A\") input
+ − 453
end"
+ − 454
"(Br (Br (Lf \"A\", Lf \"A\"), Lf \"A\"), [])"}
+ − 455
149
+ − 456
+ − 457
\begin{exercise}\label{ex:scancmts}
+ − 458
Write a parser that parses an input string so that any comment enclosed
220
+ − 459
within @{text "(*\<dots>*)"} is replaced by the same comment but enclosed within
149
+ − 460
@{text "(**\<dots>**)"} in the output string. To enclose a string, you can use the
+ − 461
function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML
236
+ − 462
"s1 ^ s ^ s2" for s1 s2 s}. Hint: To simplify the task ignore the proper
+ − 463
nesting of comments.
149
+ − 464
\end{exercise}
40
+ − 465
*}
+ − 466
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 467
section {* Parsing Theory Syntax *}
38
+ − 468
40
+ − 469
text {*
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 470
Most of the time, however, Isabelle developers have to deal with parsing
156
+ − 471
tokens, not strings. These token parsers have the type:
128
+ − 472
*}
+ − 473
426
+ − 474
ML{*type 'a parser = Token.T list -> 'a * Token.T list*}
128
+ − 475
+ − 476
text {*
149
+ − 477
The reason for using token parsers is that theory syntax, as well as the
128
+ − 478
parsers for the arguments of proof methods, use the type @{ML_type
426
+ − 479
Token.T}.
42
+ − 480
+ − 481
\begin{readmore}
40
+ − 482
The parser functions for the theory syntax are contained in the structure
426
+ − 483
@{ML_struct Parse} defined in the file @{ML_file "Pure/Isar/parse.ML"}.
+ − 484
The definition for tokens is in the file @{ML_file "Pure/Isar/token.ML"}.
42
+ − 485
\end{readmore}
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 486
426
+ − 487
The structure @{ML_struct Token} defines several kinds of tokens (for
+ − 488
example @{ML_ind Ident in Token} for identifiers, @{ML Keyword in
+ − 489
Token} for keywords and @{ML_ind Command in Token} for commands). Some
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 490
token parsers take into account the kind of tokens. The first example shows
256
+ − 491
how to generate a token list out of a string using the function
426
+ − 492
@{ML_ind scan in Outer_Syntax}. It is given the argument
256
+ − 493
@{ML "Position.none"} since,
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 494
at the moment, we are not interested in generating precise error
376
+ − 495
messages. The following code
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 496
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 497
426
+ − 498
@{ML_response_fake [display,gray] "Outer_Syntax.scan Position.none \"hello world\""
50
+ − 499
"[Token (\<dots>,(Ident, \"hello\"),\<dots>),
+ − 500
Token (\<dots>,(Space, \" \"),\<dots>),
+ − 501
Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
+ − 502
+ − 503
produces three tokens where the first and the last are identifiers, since
58
+ − 504
@{text [quotes] "hello"} and @{text [quotes] "world"} do not match any
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 505
other syntactic category. The second indicates a space.
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 506
326
+ − 507
We can easily change what is recognised as a keyword with the function
426
+ − 508
@{ML_ind keyword in Keyword}. For example calling it with
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 509
*}
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 510
426
+ − 511
ML{*val _ = Keyword.keyword "hello"*}
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 512
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 513
text {*
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 514
then lexing @{text [quotes] "hello world"} will produce
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 515
426
+ − 516
@{ML_response_fake [display,gray] "Outer_Syntax.scan Position.none \"hello world\""
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 517
"[Token (\<dots>,(Keyword, \"hello\"),\<dots>),
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 518
Token (\<dots>,(Space, \" \"),\<dots>),
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 519
Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
50
+ − 520
241
+ − 521
Many parsing functions later on will require white space, comments and the like
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 522
to have already been filtered out. So from now on we are going to use the
426
+ − 523
functions @{ML filter} and @{ML_ind is_proper in Token} to do this.
256
+ − 524
For example:
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 525
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 526
@{ML_response_fake [display,gray]
50
+ − 527
"let
426
+ − 528
val input = Outer_Syntax.scan Position.none \"hello world\"
50
+ − 529
in
426
+ − 530
filter Token.is_proper input
50
+ − 531
end"
+ − 532
"[Token (\<dots>,(Ident, \"hello\"), \<dots>), Token (\<dots>,(Ident, \"world\"), \<dots>)]"}
+ − 533
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 534
For convenience we define the function:
50
+ − 535
*}
+ − 536
69
+ − 537
ML{*fun filtered_input str =
426
+ − 538
filter Token.is_proper (Outer_Syntax.scan Position.none str) *}
50
+ − 539
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 540
text {*
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 541
If you now parse
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 542
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 543
@{ML_response_fake [display,gray]
50
+ − 544
"filtered_input \"inductive | for\""
+ − 545
"[Token (\<dots>,(Command, \"inductive\"),\<dots>),
+ − 546
Token (\<dots>,(Keyword, \"|\"),\<dots>),
+ − 547
Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 548
221
+ − 549
you obtain a list consisting of only one command and two keyword tokens.
241
+ − 550
If you want to see which keywords and commands are currently known to Isabelle,
+ − 551
type:
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 552
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 553
@{ML_response_fake [display,gray]
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 554
"let
426
+ − 555
val (keywords, commands) = Keyword.get_lexicons ()
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 556
in
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 557
(Scan.dest_lexicon commands, Scan.dest_lexicon keywords)
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 558
end"
132
+ − 559
"([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
42
+ − 560
344
+ − 561
You might have to adjust the @{ML_ind print_depth} in order to
241
+ − 562
see the complete list.
+ − 563
426
+ − 564
The parser @{ML_ind "$$$" in Parse} parses a single keyword. For example:
50
+ − 565
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 566
@{ML_response [display,gray]
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 567
"let
50
+ − 568
val input1 = filtered_input \"where for\"
+ − 569
val input2 = filtered_input \"| in\"
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 570
in
426
+ − 571
(Parse.$$$ \"where\" input1, Parse.$$$ \"|\" input2)
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 572
end"
128
+ − 573
"((\"where\",\<dots>), (\"|\",\<dots>))"}
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 574
426
+ − 575
Any non-keyword string can be parsed with the function @{ML_ind reserved in Parse}.
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 576
For example:
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 577
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 578
@{ML_response [display,gray]
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 579
"let
426
+ − 580
val p = Parse.reserved \"bar\"
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 581
val input = filtered_input \"bar\"
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 582
in
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 583
p input
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 584
end"
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 585
"(\"bar\",[])"}
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 586
344
+ − 587
Like before, you can sequentially connect parsers with @{ML "--"}. For example:
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 588
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 589
@{ML_response [display,gray]
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 590
"let
50
+ − 591
val input = filtered_input \"| in\"
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 592
in
426
+ − 593
(Parse.$$$ \"|\" -- Parse.$$$ \"in\") input
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 594
end"
183
+ − 595
"((\"|\", \"in\"), [])"}
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 596
426
+ − 597
The parser @{ML "Parse.enum s p" for s p} parses a possibly empty
58
+ − 598
list of items recognised by the parser @{text p}, where the items being parsed
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 599
are separated by the string @{text s}. For example:
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 600
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 601
@{ML_response [display,gray]
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 602
"let
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 603
val input = filtered_input \"in | in | in foo\"
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 604
in
426
+ − 605
(Parse.enum \"|\" (Parse.$$$ \"in\")) input
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 606
end"
183
+ − 607
"([\"in\", \"in\", \"in\"], [\<dots>])"}
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 608
426
+ − 609
The function @{ML_ind enum1 in Parse} works similarly, except that the
326
+ − 610
parsed list must be non-empty. Note that we had to add a string @{text
+ − 611
[quotes] "foo"} at the end of the parsed string, otherwise the parser would
+ − 612
have consumed all tokens and then failed with the exception @{text
+ − 613
"MORE"}. Like in the previous section, we can avoid this exception using the
+ − 614
wrapper @{ML Scan.finite}. This time, however, we have to use the
426
+ − 615
``stopper-token'' @{ML Token.stopper}. We can write:
49
+ − 616
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 617
@{ML_response [display,gray]
49
+ − 618
"let
50
+ − 619
val input = filtered_input \"in | in | in\"
426
+ − 620
val p = Parse.enum \"|\" (Parse.$$$ \"in\")
49
+ − 621
in
426
+ − 622
Scan.finite Token.stopper p input
49
+ − 623
end"
183
+ − 624
"([\"in\", \"in\", \"in\"], [])"}
49
+ − 625
75
+ − 626
The following function will help to run examples.
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 627
*}
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 628
426
+ − 629
ML{*fun parse p input = Scan.finite Token.stopper (Scan.error p) input *}
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 630
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 631
text {*
426
+ − 632
The function @{ML_ind "!!!" in Parse} can be used to force termination
326
+ − 633
of the parser in case of a dead end, just like @{ML "Scan.!!"} (see previous
+ − 634
section). A difference, however, is that the error message of @{ML
426
+ − 635
"Parse.!!!"} is fixed to be @{text [quotes] "Outer syntax error"}
221
+ − 636
together with a relatively precise description of the failure. For example:
49
+ − 637
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 638
@{ML_response_fake [display,gray]
49
+ − 639
"let
50
+ − 640
val input = filtered_input \"in |\"
426
+ − 641
val parse_bar_then_in = Parse.$$$ \"|\" -- Parse.$$$ \"in\"
49
+ − 642
in
426
+ − 643
parse (Parse.!!! parse_bar_then_in) input
49
+ − 644
end"
+ − 645
"Exception ERROR \"Outer syntax error: keyword \"|\" expected,
+ − 646
but keyword in was found\" raised"
+ − 647
}
42
+ − 648
65
+ − 649
\begin{exercise} (FIXME)
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 650
A type-identifier, for example @{typ "'a"}, is a token of
426
+ − 651
kind @{ML_ind Keyword in Token}. It can be parsed using
+ − 652
the function @{ML type_ident in Parse}.
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 653
\end{exercise}
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 654
104
+ − 655
(FIXME: or give parser for numbers)
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 656
125
+ − 657
Whenever there is a possibility that the processing of user input can fail,
221
+ − 658
it is a good idea to give all available information about where the error
220
+ − 659
occurred. For this Isabelle can attach positional information to tokens
326
+ − 660
and then thread this information up the ``processing chain''. To see this,
+ − 661
modify the function @{ML filtered_input}, described earlier, as follows
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 662
*}
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 663
125
+ − 664
ML{*fun filtered_input' str =
426
+ − 665
filter Token.is_proper (Outer_Syntax.scan (Position.line 7) str) *}
49
+ − 666
+ − 667
text {*
125
+ − 668
where we pretend the parsed string starts on line 7. An example is
49
+ − 669
125
+ − 670
@{ML_response_fake [display,gray]
+ − 671
"filtered_input' \"foo \\n bar\""
+ − 672
"[Token ((\"foo\", ({line=7, end_line=7}, {line=7})), (Ident, \"foo\"), \<dots>),
+ − 673
Token ((\"bar\", ({line=8, end_line=8}, {line=8})), (Ident, \"bar\"), \<dots>)]"}
+ − 674
+ − 675
in which the @{text [quotes] "\\n"} causes the second token to be in
+ − 676
line 8.
+ − 677
426
+ − 678
By using the parser @{ML position in Parse} you can access the token
326
+ − 679
position and return it as part of the parser result. For example
125
+ − 680
+ − 681
@{ML_response_fake [display,gray]
+ − 682
"let
241
+ − 683
val input = filtered_input' \"where\"
125
+ − 684
in
426
+ − 685
parse (Parse.position (Parse.$$$ \"where\")) input
125
+ − 686
end"
+ − 687
"((\"where\", {line=7, end_line=7}), [])"}
+ − 688
+ − 689
\begin{readmore}
+ − 690
The functions related to positions are implemented in the file
+ − 691
@{ML_file "Pure/General/position.ML"}.
+ − 692
\end{readmore}
49
+ − 693
391
+ − 694
\begin{exercise}\label{ex:contextfree}
+ − 695
Write a parser for the context-free grammar representing arithmetic
+ − 696
expressions with addition and multiplication. As usual, multiplication
+ − 697
binds stronger than addition, and both of them nest to the right.
+ − 698
The context-free grammar is defined as:
+ − 699
+ − 700
\begin{center}
+ − 701
\begin{tabular}{lcl}
+ − 702
@{text "<Basic>"} & @{text "::="} & @{text "<Number> | (<Expr>)"}\\
+ − 703
@{text "<Factor>"} & @{text "::="} & @{text "<Basic> * <Factor> | <Basic>"}\\
+ − 704
@{text "<Expr>"} & @{text "::="} & @{text "<Factor> + <Expr> | <Factor>"}\\
+ − 705
\end{tabular}
+ − 706
\end{center}
+ − 707
+ − 708
Hint: Be careful with recursive parsers.
+ − 709
\end{exercise}
49
+ − 710
*}
+ − 711
326
+ − 712
section {* Parsers for ML-Code (TBD) *}
+ − 713
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 714
text {*
426
+ − 715
@{ML_ind ML_source in Parse}
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 716
*}
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 717
193
+ − 718
section {* Context Parser (TBD) *}
+ − 719
+ − 720
text {*
326
+ − 721
@{ML_ind Args.context}
+ − 722
*}
+ − 723
(*
+ − 724
ML {*
+ − 725
let
+ − 726
val parser = Args.context -- Scan.lift Args.name_source
+ − 727
+ − 728
fun term_pat (ctxt, str) =
+ − 729
str |> Syntax.read_prop ctxt
+ − 730
in
+ − 731
(parser >> term_pat) (Context.Proof @{context}, filtered_input "f (a::nat)")
+ − 732
|> fst
+ − 733
end
+ − 734
*}
+ − 735
*)
+ − 736
+ − 737
text {*
+ − 738
@{ML_ind Args.context}
+ − 739
193
+ − 740
Used for example in \isacommand{attribute\_setup} and \isacommand{method\_setup}.
+ − 741
*}
+ − 742
207
+ − 743
section {* Argument and Attribute Parsers (TBD) *}
+ − 744
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 745
section {* Parsing Inner Syntax *}
42
+ − 746
125
+ − 747
text {*
+ − 748
There is usually no need to write your own parser for parsing inner syntax, that is
285
+ − 749
for terms and types: you can just call the predefined parsers. Terms can
426
+ − 750
be parsed using the function @{ML_ind term in Parse}. For example:
125
+ − 751
+ − 752
@{ML_response [display,gray]
+ − 753
"let
426
+ − 754
val input = Outer_Syntax.scan Position.none \"foo\"
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 755
in
426
+ − 756
Parse.term input
125
+ − 757
end"
+ − 758
"(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"}
+ − 759
426
+ − 760
The function @{ML_ind prop in Parse} is similar, except that it gives a different
127
+ − 761
error message, when parsing fails. As you can see, the parser not just returns
+ − 762
the parsed string, but also some encoded information. You can decode the
326
+ − 763
information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}. For example
127
+ − 764
+ − 765
@{ML_response [display,gray]
+ − 766
"YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
+ − 767
"XML.Elem (\"token\", [], [XML.Text \"foo\"])"}
+ − 768
149
+ − 769
The result of the decoding is an XML-tree. You can see better what is going on if
131
+ − 770
you replace @{ML Position.none} by @{ML "Position.line 42"}, say:
101
+ − 771
125
+ − 772
@{ML_response [display,gray]
+ − 773
"let
426
+ − 774
val input = Outer_Syntax.scan (Position.line 42) \"foo\"
125
+ − 775
in
426
+ − 776
YXML.parse (fst (Parse.term input))
125
+ − 777
end"
127
+ − 778
"XML.Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
125
+ − 779
149
+ − 780
The positional information is stored as part of an XML-tree so that code
+ − 781
called later on will be able to give more precise error messages.
125
+ − 782
127
+ − 783
\begin{readmore}
128
+ − 784
The functions to do with input and output of XML and YXML are defined
127
+ − 785
in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}.
+ − 786
\end{readmore}
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 787
361
+ − 788
FIXME:
+ − 789
@{ML_ind parse_term in Syntax} @{ML_ind check_term in Syntax}
+ − 790
@{ML_ind parse_typ in Syntax} @{ML_ind check_typ in Syntax}
374
+ − 791
@{ML_ind read_term in Syntax} @{ML_ind read_term in Syntax}
+ − 792
361
+ − 793
125
+ − 794
*}
101
+ − 795
116
+ − 796
section {* Parsing Specifications\label{sec:parsingspecs} *}
101
+ − 797
+ − 798
text {*
121
+ − 799
There are a number of special purpose parsers that help with parsing
156
+ − 800
specifications of function definitions, inductive predicates and so on. In
220
+ − 801
Chapter~\ref{chp:package}, for example, we will need to parse specifications
121
+ − 802
for inductive predicates of the form:
+ − 803
*}
101
+ − 804
121
+ − 805
simple_inductive
+ − 806
even and odd
+ − 807
where
+ − 808
even0: "even 0"
+ − 809
| evenS: "odd n \<Longrightarrow> even (Suc n)"
+ − 810
| oddS: "even n \<Longrightarrow> odd (Suc n)"
101
+ − 811
327
+ − 812
101
+ − 813
text {*
121
+ − 814
For this we are going to use the parser:
101
+ − 815
*}
+ − 816
121
+ − 817
ML %linenosgray{*val spec_parser =
426
+ − 818
Parse.fixes --
126
+ − 819
Scan.optional
426
+ − 820
(Parse.$$$ "where" |--
+ − 821
Parse.!!!
+ − 822
(Parse.enum1 "|"
+ − 823
(Parse_Spec.opt_thm_name ":" -- Parse.prop))) []*}
120
+ − 824
101
+ − 825
text {*
241
+ − 826
Note that the parser must not parse the keyword \simpleinductive, even if it is
126
+ − 827
meant to process definitions as shown above. The parser of the keyword
128
+ − 828
will be given by the infrastructure that will eventually call @{ML spec_parser}.
126
+ − 829
+ − 830
124
+ − 831
To see what the parser returns, let us parse the string corresponding to the
121
+ − 832
definition of @{term even} and @{term odd}:
+ − 833
101
+ − 834
@{ML_response [display,gray]
+ − 835
"let
+ − 836
val input = filtered_input
+ − 837
(\"even and odd \" ^
+ − 838
\"where \" ^
+ − 839
\" even0[intro]: \\\"even 0\\\" \" ^
+ − 840
\"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^
+ − 841
\"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
+ − 842
in
120
+ − 843
parse spec_parser input
101
+ − 844
end"
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 845
"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
101
+ − 846
[((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
+ − 847
((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
+ − 848
((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
121
+ − 849
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 850
As you see, the result is a pair consisting of a list of
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 851
variables with optional type-annotation and syntax-annotation, and a list of
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 852
rules where every rule has optionally a name and an attribute.
121
+ − 853
426
+ − 854
The function @{ML_ind "fixes" in Parse} in Line 2 of the parser reads an
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 855
\isacommand{and}-separated
124
+ − 856
list of variables that can include optional type annotations and syntax translations.
121
+ − 857
For example:\footnote{Note that in the code we need to write
+ − 858
@{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes
+ − 859
in the compound type.}
+ − 860
+ − 861
@{ML_response [display,gray]
+ − 862
"let
+ − 863
val input = filtered_input
+ − 864
\"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
+ − 865
in
426
+ − 866
parse Parse.fixes input
121
+ − 867
end"
+ − 868
"([(foo, SOME \"\\^E\\^Ftoken\\^Eint \<Rightarrow> bool\\^E\\^F\\^E\", NoSyn),
+ − 869
(bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)),
+ − 870
(blonk, NONE, NoSyn)],[])"}
50
+ − 871
*}
+ − 872
121
+ − 873
text {*
156
+ − 874
Whenever types are given, they are stored in the @{ML SOME}s. The types are
+ − 875
not yet used to type the variables: this must be done by type-inference later
149
+ − 876
on. Since types are part of the inner syntax they are strings with some
241
+ − 877
encoded information (see previous section). If a mixfix-syntax is
369
+ − 878
present for a variable, then it is stored in the
371
+ − 879
@{ML Mixfix} data structure; no syntax translation is indicated by @{ML_ind NoSyn in Syntax}.
121
+ − 880
+ − 881
\begin{readmore}
371
+ − 882
The data structure for mixfix annotations are implemented in
+ − 883
@{ML_file "Pure/Syntax/mixfix.ML"} and @{ML_file "Pure/Syntax/syntax.ML"}.
121
+ − 884
\end{readmore}
+ − 885
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 886
Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
219
+ − 887
list of introduction rules, that is propositions with theorem annotations
+ − 888
such as rule names and attributes. The introduction rules are propositions
426
+ − 889
parsed by @{ML_ind prop in Parse}. However, they can include an optional
219
+ − 890
theorem name plus some attributes. For example
121
+ − 891
+ − 892
@{ML_response [display,gray] "let
+ − 893
val input = filtered_input \"foo_lemma[intro,dest!]:\"
426
+ − 894
val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input
121
+ − 895
in
+ − 896
(name, map Args.dest_src attrib)
+ − 897
end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
+ − 898
426
+ − 899
The function @{ML_ind opt_thm_name in Parse_Spec} is the ``optional'' variant of
+ − 900
@{ML_ind thm_name in Parse_Spec}. Theorem names can contain attributes. The name
131
+ − 901
has to end with @{text [quotes] ":"}---see the argument of
426
+ − 902
the function @{ML Parse_Spec.opt_thm_name} in Line 7.
121
+ − 903
+ − 904
\begin{readmore}
+ − 905
Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"}
+ − 906
and @{ML_file "Pure/Isar/args.ML"}.
+ − 907
\end{readmore}
101
+ − 908
*}
65
+ − 909
193
+ − 910
text_raw {*
+ − 911
\begin{exercise}
426
+ − 912
Have a look at how the parser @{ML Parse_Spec.where_alt_specs} is implemented
424
+ − 913
in file @{ML_file "Pure/Isar/parse_spec.ML"}. This parser corresponds
207
+ − 914
to the ``where-part'' of the introduction rules given above. Below
426
+ − 915
we paraphrase the code of @{ML_ind where_alt_specs in Parse_Spec} adapted to our
207
+ − 916
purposes.
193
+ − 917
\begin{isabelle}
+ − 918
*}
+ − 919
ML %linenosgray{*val spec_parser' =
426
+ − 920
Parse.fixes --
193
+ − 921
Scan.optional
426
+ − 922
(Parse.$$$ "where" |--
+ − 923
Parse.!!!
+ − 924
(Parse.enum1 "|"
+ − 925
((Parse_Spec.opt_thm_name ":" -- Parse.prop) --|
+ − 926
Scan.option (Scan.ahead (Parse.name ||
+ − 927
Parse.$$$ "[") --
+ − 928
Parse.!!! (Parse.$$$ "|"))))) [] *}
193
+ − 929
text_raw {*
+ − 930
\end{isabelle}
284
+ − 931
Both parsers accept the same input% that's not true:
+ − 932
% spec_parser accepts input that is refuted by spec_parser'
+ − 933
, but if you look closely, you can notice
207
+ − 934
an additional ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of
+ − 935
this additional ``tail''?
193
+ − 936
\end{exercise}
+ − 937
*}
+ − 938
229
+ − 939
text {*
426
+ − 940
(FIXME: @{ML Parse.type_args}, @{ML Parse.typ}, @{ML Parse.opt_mixfix})
229
+ − 941
*}
+ − 942
+ − 943
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 944
section {* New Commands and Keyword Files\label{sec:newcommand} *}
65
+ − 945
+ − 946
text {*
68
+ − 947
Often new commands, for example for providing new definitional principles,
+ − 948
need to be implemented. While this is not difficult on the ML-level,
66
+ − 949
new commands, in order to be useful, need to be recognised by
65
+ − 950
ProofGeneral. This results in some subtle configuration issues, which we
+ − 951
will explain in this section.
+ − 952
74
+ − 953
To keep things simple, let us start with a ``silly'' command that does nothing
+ − 954
at all. We shall name this command \isacommand{foobar}. On the ML-level it can be
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 955
defined as:
68
+ − 956
*}
65
+ − 957
69
+ − 958
ML{*let
394
+ − 959
val do_nothing = Scan.succeed (Local_Theory.theory I)
426
+ − 960
val kind = Keyword.thy_decl
65
+ − 961
in
426
+ − 962
Outer_Syntax.local_theory "foobar" "description of foobar" kind do_nothing
69
+ − 963
end *}
65
+ − 964
68
+ − 965
text {*
426
+ − 966
The crucial function @{ML_ind local_theory in Outer_Syntax} expects a name for the command, a
219
+ − 967
short description, a kind indicator (which we will explain later more thoroughly) and a
+ − 968
parser producing a local theory transition (its purpose will also explained
66
+ − 969
later).
65
+ − 970
101
+ − 971
While this is everything you have to do on the ML-level, you need a keyword
68
+ − 972
file that can be loaded by ProofGeneral. This is to enable ProofGeneral to
+ − 973
recognise \isacommand{foobar} as a command. Such a keyword file can be
74
+ − 974
generated with the command-line:
68
+ − 975
74
+ − 976
@{text [display] "$ isabelle keywords -k foobar some_log_files"}
65
+ − 977
74
+ − 978
The option @{text "-k foobar"} indicates which postfix the name of the keyword file
80
+ − 979
will be assigned. In the case above the file will be named @{text
86
+ − 980
"isar-keywords-foobar.el"}. This command requires log files to be
68
+ − 981
present (in order to extract the keywords from them). To generate these log
101
+ − 982
files, you first need to package the code above into a separate theory file named
68
+ − 983
@{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the
+ − 984
complete code.
65
+ − 985
66
+ − 986
+ − 987
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 988
\begin{figure}[t]
69
+ − 989
\begin{graybox}\small
66
+ − 990
\isacommand{theory}~@{text Command}\\
+ − 991
\isacommand{imports}~@{text Main}\\
+ − 992
\isacommand{begin}\\
85
+ − 993
\isacommand{ML}~@{text "\<verbopen>"}\\
66
+ − 994
@{ML
+ − 995
"let
394
+ − 996
val do_nothing = Scan.succeed (Local_Theory.theory I)
426
+ − 997
val kind = Keyword.thy_decl
66
+ − 998
in
426
+ − 999
Outer_Syntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing
66
+ − 1000
end"}\\
85
+ − 1001
@{text "\<verbclose>"}\\
66
+ − 1002
\isacommand{end}
80
+ − 1003
\end{graybox}
241
+ − 1004
\caption{This file can be used to generate a log file. This log file in turn can
+ − 1005
be used to generate a keyword file containing the command \isacommand{foobar}.
+ − 1006
\label{fig:commandtheory}}
66
+ − 1007
\end{figure}
+ − 1008
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1009
75
+ − 1010
For our purposes it is sufficient to use the log files of the theories
68
+ − 1011
@{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as
75
+ − 1012
the log file for the theory @{text "Command.thy"}, which contains the new
+ − 1013
\isacommand{foobar}-command. If you target other logics besides HOL, such
74
+ − 1014
as Nominal or ZF, then you need to adapt the log files appropriately.
104
+ − 1015
74
+ − 1016
@{text Pure} and @{text HOL} are usually compiled during the installation of
+ − 1017
Isabelle. So log files for them should be already available. If not, then
75
+ − 1018
they can be conveniently compiled with the help of the build-script from the Isabelle
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1019
distribution.
65
+ − 1020
+ − 1021
@{text [display]
+ − 1022
"$ ./build -m \"Pure\"
+ − 1023
$ ./build -m \"HOL\""}
+ − 1024
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1025
The @{text "Pure-ProofGeneral"} theory needs to be compiled with:
65
+ − 1026
+ − 1027
@{text [display] "$ ./build -m \"Pure-ProofGeneral\" \"Pure\""}
+ − 1028
101
+ − 1029
For the theory @{text "Command.thy"}, you first need to create a ``managed'' subdirectory
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1030
with:
66
+ − 1031
68
+ − 1032
@{text [display] "$ isabelle mkdir FoobarCommand"}
66
+ − 1033
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1034
This generates a directory containing the files:
66
+ − 1035
+ − 1036
@{text [display]
+ − 1037
"./IsaMakefile
68
+ − 1038
./FoobarCommand/ROOT.ML
+ − 1039
./FoobarCommand/document
+ − 1040
./FoobarCommand/document/root.tex"}
65
+ − 1041
+ − 1042
101
+ − 1043
You need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
66
+ − 1044
and add the line
+ − 1045
207
+ − 1046
@{text [display] "no_document use_thy \"Command\";"}
66
+ − 1047
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1048
to the file @{text "./FoobarCommand/ROOT.ML"}. You can now compile the theory by just typing:
65
+ − 1049
+ − 1050
@{text [display] "$ isabelle make"}
+ − 1051
101
+ − 1052
If the compilation succeeds, you have finally created all the necessary log files.
+ − 1053
They are stored in the directory
65
+ − 1054
241
+ − 1055
@{text [display] "~/.isabelle/heaps/Isabelle2009/polyml-5.2.1_x86-linux/log"}
65
+ − 1056
74
+ − 1057
or something similar depending on your Isabelle distribution and architecture.
+ − 1058
One quick way to assign a shell variable to this directory is by typing
66
+ − 1059
+ − 1060
@{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
+ − 1061
156
+ − 1062
on the Unix prompt. If you now type @{text "ls $ISABELLE_LOGS"}, then the
128
+ − 1063
directory should include the files:
65
+ − 1064
+ − 1065
@{text [display]
+ − 1066
"Pure.gz
+ − 1067
HOL.gz
+ − 1068
Pure-ProofGeneral.gz
68
+ − 1069
HOL-FoobarCommand.gz"}
65
+ − 1070
101
+ − 1071
From them you can create the keyword files. Assuming the name
75
+ − 1072
of the directory is in @{text "$ISABELLE_LOGS"},
74
+ − 1073
then the Unix command for creating the keyword file is:
65
+ − 1074
+ − 1075
@{text [display]
68
+ − 1076
"$ isabelle keywords -k foobar
80
+ − 1077
$ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
65
+ − 1078
80
+ − 1079
The result is the file @{text "isar-keywords-foobar.el"}. It should contain
321
+ − 1080
the string @{text "foobar"} twice.\footnote{To see whether things are fine,
+ − 1081
check that @{text "grep foobar"} on this file returns something non-empty.}
+ − 1082
This keyword file needs to be copied into the directory @{text
+ − 1083
"~/.isabelle/etc"}. To make ProofGeneral aware of it, you have to start
+ − 1084
Isabelle with the option @{text "-k foobar"}, that is:
65
+ − 1085
80
+ − 1086
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1087
@{text [display] "$ isabelle emacs -k foobar a_theory_file"}
65
+ − 1088
101
+ − 1089
If you now build a theory on top of @{text "Command.thy"},
326
+ − 1090
then you can use the command \isacommand{foobar}. You can just write
321
+ − 1091
*}
+ − 1092
+ − 1093
foobar
+ − 1094
+ − 1095
text {*
+ − 1096
but you will not see any action as we chose to implement this command to do
327
+ − 1097
nothing. The point of this command is only to show the procedure of how
326
+ − 1098
to interact with ProofGeneral. A similar procedure has to be done with any
+ − 1099
other new command, and also any new keyword that is introduced with
426
+ − 1100
the function @{ML_ind keyword in Keyword}. For example:
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1101
*}
65
+ − 1102
426
+ − 1103
ML{*val _ = Keyword.keyword "blink" *}
65
+ − 1104
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1105
text {*
321
+ − 1106
At the moment the command \isacommand{foobar} is not very useful. Let us
+ − 1107
refine it a bit next by letting it take a proposition as argument and
+ − 1108
printing this proposition inside the tracing buffer.
68
+ − 1109
75
+ − 1110
The crucial part of a command is the function that determines the behaviour
+ − 1111
of the command. In the code above we used a ``do-nothing''-function, which
344
+ − 1112
because of @{ML_ind succeed in Scan} does not parse any argument, but immediately
394
+ − 1113
returns the simple function @{ML "Local_Theory.theory I"}. We can
75
+ − 1114
replace this code by a function that first parses a proposition (using the
426
+ − 1115
parser @{ML Parse.prop}), then prints out the tracing
219
+ − 1116
information (using a new function @{text trace_prop}) and
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1117
finally does nothing. For this you can write:
68
+ − 1118
*}
+ − 1119
69
+ − 1120
ML{*let
219
+ − 1121
fun trace_prop str =
394
+ − 1122
Local_Theory.theory (fn ctxt => (tracing str; ctxt))
75
+ − 1123
426
+ − 1124
val kind = Keyword.thy_decl
68
+ − 1125
in
426
+ − 1126
Outer_Syntax.local_theory "foobar_trace" "traces a proposition"
+ − 1127
kind (Parse.prop >> trace_prop)
69
+ − 1128
end *}
68
+ − 1129
321
+ − 1130
text {*
+ − 1131
The command is now \isacommand{foobar\_trace} and can be used to
+ − 1132
see the proposition in the tracing buffer.
+ − 1133
*}
+ − 1134
+ − 1135
foobar_trace "True \<and> False"
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1136
68
+ − 1137
text {*
426
+ − 1138
Note that so far we used @{ML_ind thy_decl in Keyword} as the kind
219
+ − 1139
indicator for the command. This means that the command finishes as soon as
+ − 1140
the arguments are processed. Examples of this kind of commands are
+ − 1141
\isacommand{definition} and \isacommand{declare}. In other cases, commands
+ − 1142
are expected to parse some arguments, for example a proposition, and then
+ − 1143
``open up'' a proof in order to prove the proposition (for example
86
+ − 1144
\isacommand{lemma}) or prove some other properties (for example
219
+ − 1145
\isacommand{function}). To achieve this kind of behaviour, you have to use
426
+ − 1146
the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML
+ − 1147
"local_theory_to_proof" in Outer_Syntax} to set up the command. Note,
219
+ − 1148
however, once you change the ``kind'' of a command from @{ML thy_decl in
426
+ − 1149
Keyword} to @{ML thy_goal in Keyword} then the keyword file needs
219
+ − 1150
to be re-created!
68
+ − 1151
327
+ − 1152
Below we show the command \isacommand{foobar\_goal} which takes a
+ − 1153
proposition as argument and then starts a proof in order to prove
+ − 1154
it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in
426
+ − 1155
Keyword}.
68
+ − 1156
*}
+ − 1157
114
+ − 1158
ML%linenosgray{*let
327
+ − 1159
fun goal_prop str lthy =
68
+ − 1160
let
241
+ − 1161
val prop = Syntax.read_prop lthy str
68
+ − 1162
in
422
+ − 1163
Proof.theorem NONE (K I) [[(prop, [])]] lthy
327
+ − 1164
end
68
+ − 1165
426
+ − 1166
val kind = Keyword.thy_goal
68
+ − 1167
in
426
+ − 1168
Outer_Syntax.local_theory_to_proof "foobar_goal" "proves a proposition"
+ − 1169
kind (Parse.prop >> goal_prop)
69
+ − 1170
end *}
68
+ − 1171
+ − 1172
text {*
327
+ − 1173
The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1174
proved) and a context as argument. The context is necessary in order to be able to use
344
+ − 1175
@{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
422
+ − 1176
In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the
75
+ − 1177
proposition. Its argument @{ML NONE} stands for a locale (which we chose to
+ − 1178
omit); the argument @{ML "(K I)"} stands for a function that determines what
+ − 1179
should be done with the theorem once it is proved (we chose to just forget
219
+ − 1180
about it). Line 9 contains the parser for the proposition.
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1181
321
+ − 1182
If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \<and> True"},
+ − 1183
you obtain the following proof state
+ − 1184
*}
68
+ − 1185
321
+ − 1186
foobar_goal "True \<and> True"
+ − 1187
txt {*
+ − 1188
\begin{minipage}{\textwidth}
+ − 1189
@{subgoals [display]}
+ − 1190
\end{minipage}\medskip
68
+ − 1191
321
+ − 1192
and can prove the proposition as follows.
+ − 1193
*}
+ − 1194
apply(rule conjI)
+ − 1195
apply(rule TrueI)+
+ − 1196
done
+ − 1197
+ − 1198
text {*
327
+ − 1199
{\bf TBD below}
74
+ − 1200
394
+ − 1201
(FIXME: read a name and show how to store theorems; see @{ML_ind note in Local_Theory})
241
+ − 1202
65
+ − 1203
*}
+ − 1204
328
+ − 1205
ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*}
321
+ − 1206
ML{*let
324
+ − 1207
fun after_qed thm_name thms lthy =
394
+ − 1208
Local_Theory.note (thm_name, (flat thms)) lthy |> snd
324
+ − 1209
+ − 1210
fun setup_proof (thm_name, (txt, pos)) lthy =
321
+ − 1211
let
+ − 1212
val trm = ML_Context.evaluate lthy true ("r", r) txt
+ − 1213
in
422
+ − 1214
Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
324
+ − 1215
end
321
+ − 1216
426
+ − 1217
val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
321
+ − 1218
in
426
+ − 1219
Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition"
+ − 1220
Keyword.thy_goal (parser >> setup_proof)
321
+ − 1221
end*}
+ − 1222
324
+ − 1223
foobar_prove test: {* @{prop "True"} *}
321
+ − 1224
apply(rule TrueI)
+ − 1225
done
+ − 1226
322
+ − 1227
(*
+ − 1228
ML {*
+ − 1229
structure TacticData = ProofDataFun
+ − 1230
(
+ − 1231
type T = thm list -> tactic;
+ − 1232
fun init _ = undefined;
366
+ − 1233
)
322
+ − 1234
+ − 1235
val set_tactic = TacticData.put;
+ − 1236
*}
+ − 1237
+ − 1238
ML {*
+ − 1239
TacticData.get @{context}
+ − 1240
*}
+ − 1241
+ − 1242
ML {* Method.set_tactic *}
+ − 1243
ML {* fun tactic (facts: thm list) : tactic = (atac 1) *}
+ − 1244
ML {* Context.map_proof *}
+ − 1245
ML {* ML_Context.expression *}
+ − 1246
ML {* METHOD *}
+ − 1247
+ − 1248
+ − 1249
ML {*
+ − 1250
fun myexpression pos bind body txt =
+ − 1251
let
+ − 1252
val _ = tracing ("bind)" ^ bind)
+ − 1253
val _ = tracing ("body)" ^ body)
+ − 1254
val _ = tracing ("txt)" ^ txt)
+ − 1255
val _ = tracing ("result) " ^ "Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
+ − 1256
" end (ML_Context.the_generic_context ())));")
+ − 1257
in
+ − 1258
ML_Context.exec (fn () => ML_Context.eval false pos
+ − 1259
("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
+ − 1260
" end (ML_Context.the_generic_context ())));"))
+ − 1261
end
+ − 1262
*}
319
+ − 1263
+ − 1264
322
+ − 1265
ML {*
+ − 1266
fun ml_tactic (txt, pos) ctxt =
+ − 1267
let
+ − 1268
val ctxt' = ctxt |> Context.proof_map
+ − 1269
(myexpression pos
+ − 1270
"fun tactic (facts: thm list) : tactic"
+ − 1271
"Context.map_proof (Method.set_tactic tactic)" txt);
+ − 1272
in
+ − 1273
Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt')
+ − 1274
end;
+ − 1275
*}
+ − 1276
+ − 1277
ML {*
+ − 1278
fun tactic3 (txt, pos) ctxt =
+ − 1279
let
+ − 1280
val _ = tracing ("1) " ^ txt )
+ − 1281
in
+ − 1282
METHOD (ml_tactic (txt, pos) ctxt; K (atac 1))
+ − 1283
end
+ − 1284
*}
+ − 1285
+ − 1286
setup {*
426
+ − 1287
Method.setup (Binding.name "tactic3") (Scan.lift (Parse.position Args.name)
322
+ − 1288
>> tactic3)
+ − 1289
"ML tactic as proof method"
+ − 1290
*}
+ − 1291
+ − 1292
lemma "A \<Longrightarrow> A"
+ − 1293
apply(tactic3 {* (atac 1) *})
+ − 1294
done
+ − 1295
+ − 1296
ML {*
+ − 1297
(ML_Context.the_generic_context ())
+ − 1298
*}
+ − 1299
+ − 1300
ML {*
+ − 1301
Context.set_thread_data;
+ − 1302
ML_Context.the_generic_context
+ − 1303
*}
+ − 1304
+ − 1305
lemma "A \<Longrightarrow> A"
+ − 1306
ML_prf {*
+ − 1307
Context.set_thread_data (SOME (let fun tactic (facts: thm list) : tactic = (atac 1) in Context.map_proof (Method.set_tactic tactic) end (ML_Context.the_generic_context ())));
+ − 1308
*}
+ − 1309
+ − 1310
ML {*
+ − 1311
Context.set_thread_data (SOME ((let fun tactic (facts: thm list) : tactic = (atac 1) in 3 end) (ML_Context.the_generic_context ())));
+ − 1312
*}
+ − 1313
+ − 1314
ML {*
+ − 1315
Context.set_thread_data (SOME (let
+ − 1316
fun tactic (facts: thm list) : tactic = (atac 1)
+ − 1317
in
+ − 1318
Context.map_proof (Method.set_tactic tactic)
+ − 1319
end
+ − 1320
(ML_Context.the_generic_context ())));
+ − 1321
*}
+ − 1322
+ − 1323
+ − 1324
ML {*
+ − 1325
let
+ − 1326
fun tactic (facts: thm list) : tactic = atac
+ − 1327
in
+ − 1328
Context.map_proof (Method.set_tactic tactic)
+ − 1329
end *}
+ − 1330
+ − 1331
end *}
+ − 1332
+ − 1333
ML {* Toplevel.program (fn () =>
+ − 1334
(ML_Context.expression Position.none "val plus : int" "3 + 4" "1" (Context.Proof @{context})))*}
+ − 1335
+ − 1336
+ − 1337
ML {*
+ − 1338
fun ml_tactic (txt, pos) ctxt =
+ − 1339
let
+ − 1340
val ctxt' = ctxt |> Context.proof_map
+ − 1341
(ML_Context.expression pos
+ − 1342
"fun tactic (facts: thm list) : tactic"
+ − 1343
"Context.map_proof (Method.set_tactic tactic)" txt);
+ − 1344
in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt') end;
+ − 1345
+ − 1346
*}
+ − 1347
+ − 1348
ML {*
+ − 1349
Context.set_thread_data (SOME (let fun tactic (facts: thm list) : tactic = (atac 1) in Context.map_proof (Method.set_tactic tactic) end (ML_Context.the_generic_context ())));
+ − 1350
*}
+ − 1351
*)
319
+ − 1352
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1353
section {* Methods (TBD) *}
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1354
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1355
text {*
207
+ − 1356
(FIXME: maybe move to after the tactic section)
+ − 1357
221
+ − 1358
Methods are central to Isabelle. They are the ones you use for example
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1359
in \isacommand{apply}. To print out all currently known methods you can use the
192
+ − 1360
Isabelle command:
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1361
207
+ − 1362
\begin{isabelle}
+ − 1363
\isacommand{print\_methods}\\
+ − 1364
@{text "> methods:"}\\
+ − 1365
@{text "> -: do nothing (insert current facts only)"}\\
+ − 1366
@{text "> HOL.default: apply some intro/elim rule (potentially classical)"}\\
+ − 1367
@{text "> ..."}
+ − 1368
\end{isabelle}
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1369
193
+ − 1370
An example of a very simple method is:
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1371
*}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1372
244
+ − 1373
method_setup %gray foo =
181
+ − 1374
{* Scan.succeed
+ − 1375
(K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *}
244
+ − 1376
"foo method for conjE and conjI"
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1377
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1378
text {*
286
+ − 1379
It defines the method @{text foo}, which takes no arguments (therefore the
207
+ − 1380
parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which
256
+ − 1381
applies @{thm [source] conjE} and then @{thm [source] conjI}. The function
344
+ − 1382
@{ML_ind SIMPLE_METHOD in Method}
287
+ − 1383
turns such a tactic into a method. The method @{text "foo"} can be used as follows
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1384
*}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1385
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1386
lemma shows "A \<and> B \<Longrightarrow> C \<and> D"
244
+ − 1387
apply(foo)
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1388
txt {*
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1389
where it results in the goal state
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1390
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1391
\begin{minipage}{\textwidth}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1392
@{subgoals}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1393
\end{minipage} *}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1394
(*<*)oops(*>*)
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1395
421
+ − 1396
method_setup test = {* Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *}
+ − 1397
+ − 1398
lemma "True"
+ − 1399
apply(test)
+ − 1400
oops
+ − 1401
+ − 1402
method_setup joker = {* Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *}
+ − 1403
+ − 1404
lemma "False"
+ − 1405
apply(joker)
+ − 1406
oops
+ − 1407
+ − 1408
text {* if true is set then always works *}
+ − 1409
+ − 1410
ML {* atac *}
+ − 1411
+ − 1412
method_setup first_atac = {* Scan.lift (Scan.succeed (K (SIMPLE_METHOD (atac 1)))) *} {* bla *}
+ − 1413
+ − 1414
ML {* HEADGOAL *}
+ − 1415
+ − 1416
lemma "A \<Longrightarrow> A"
+ − 1417
apply(first_atac)
+ − 1418
oops
+ − 1419
+ − 1420
method_setup my_atac = {* Scan.lift (Scan.succeed (K (SIMPLE_METHOD' atac))) *} {* bla *}
+ − 1421
+ − 1422
lemma "A \<Longrightarrow> A"
+ − 1423
apply(my_atac)
+ − 1424
oops
+ − 1425
+ − 1426
193
+ − 1427
319
+ − 1428
+ − 1429
+ − 1430
+ − 1431
193
+ − 1432
(*
+ − 1433
ML {* SIMPLE_METHOD *}
+ − 1434
ML {* METHOD *}
+ − 1435
ML {* K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *}
+ − 1436
ML {* Scan.succeed *}
+ − 1437
*)
+ − 1438
421
+ − 1439
ML {* resolve_tac *}
+ − 1440
+ − 1441
method_setup myrule =
+ − 1442
{* Scan.lift (Scan.succeed (K (METHOD (fn thms => resolve_tac thms 1)))) *}
+ − 1443
{* bla *}
+ − 1444
+ − 1445
lemma
+ − 1446
assumes a: "A \<Longrightarrow> B \<Longrightarrow> C"
+ − 1447
shows "C"
+ − 1448
using a
+ − 1449
apply(myrule)
+ − 1450
oops
+ − 1451
+ − 1452
+ − 1453
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1454
text {*
421
+ − 1455
(********************************************************)
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1456
(FIXME: explain a version of rule-tac)
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1457
*}
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1458
220
+ − 1459
end