4
+ − 1
theory Parsing
321
+ − 2
imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package"
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 3
uses "Parsing.ML"
4
+ − 4
begin
+ − 5
+ − 6
chapter {* Parsing *}
+ − 7
+ − 8
text {*
321
+ − 9
Isabelle distinguishes between \emph{outer} and \emph{inner}
+ − 10
syntax. Commands, such as \isacommand{definition}, \isacommand{inductive}
+ − 11
and so on, belong to the outer syntax, whereas terms, types and so on belong
+ − 12
to the inner syntax. For parsing inner syntax, Isabelle uses a rather
+ − 13
general and sophisticated algorithm, which is driven by priority
+ − 14
grammars. Parsers for outer syntax are built up by functional parsing
+ − 15
combinators. These combinators are a well-established technique for parsing,
+ − 16
which has, for example, been described in Paulson's classic ML-book
+ − 17
\cite{paulson-ml2}. Isabelle developers are usually concerned with writing
+ − 18
these outer syntax parsers, either for new definitional packages or for
+ − 19
calling methods with specific arguments.
42
+ − 20
+ − 21
\begin{readmore}
236
+ − 22
The library for writing parser combinators is split up, roughly, into two
326
+ − 23
parts: The first part consists of a collection of generic parser combinators
236
+ − 24
defined in the structure @{ML_struct Scan} in the file @{ML_file
+ − 25
"Pure/General/scan.ML"}. The second part of the library consists of
+ − 26
combinators for dealing with specific token types, which are defined in the
+ − 27
structure @{ML_struct OuterParse} in the file @{ML_file
326
+ − 28
"Pure/Isar/outer_parse.ML"}. In addition specific parsers for packages are
+ − 29
defined in @{ML_file "Pure/Isar/spec_parse.ML"}. Parsers for method arguments
+ − 30
are defined in @{ML_file "Pure/Isar/args.ML"}.
42
+ − 31
\end{readmore}
38
+ − 32
+ − 33
*}
+ − 34
49
+ − 35
section {* Building Generic Parsers *}
38
+ − 36
+ − 37
text {*
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 38
240
+ − 39
Let us first have a look at parsing strings using generic parsing
316
+ − 40
combinators. The function @{ML_ind "$$"} takes a string as argument and will
240
+ − 41
``consume'' this string from a given input list of strings. ``Consume'' in
+ − 42
this context means that it will return a pair consisting of this string and
+ − 43
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
+ − 44
240
+ − 45
@{ML_response [display,gray]
+ − 46
"($$ \"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
+ − 47
240
+ − 48
@{ML_response [display,gray]
+ − 49
"($$ \"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
+ − 50
240
+ − 51
The function @{ML "$$"} will either succeed (as in the two examples above)
+ − 52
or raise the exception @{text "FAIL"} if no string can be consumed. For
+ − 53
example trying to parse
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 54
240
+ − 55
@{ML_response_fake [display,gray]
+ − 56
"($$ \"x\") (Symbol.explode \"world\")"
+ − 57
"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
+ − 58
240
+ − 59
will raise the exception @{text "FAIL"}. There are three exceptions used in
+ − 60
the parsing combinators:
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 61
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 62
\begin{itemize}
58
+ − 63
\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
+ − 64
might be explored.
58
+ − 65
\item @{text "MORE"} indicates that there is not enough input for the parser. For example
+ − 66
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
+ − 67
\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
+ − 68
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
+ − 69
\end{itemize}
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 70
50
+ − 71
However, note that these exceptions are private to the parser and cannot be accessed
49
+ − 72
by the programmer (for example to handle them).
240
+ − 73
316
+ − 74
In the examples above we use the function @{ML_ind Symbol.explode}, instead of the
+ − 75
more standard library function @{ML_ind explode}, for obtaining an input list for
326
+ − 76
the parser. The reason is that @{ML_ind Symbol.explode} is aware of character sequences,
261
+ − 77
for example @{text "\<foo>"}, that have a special meaning in Isabelle. To see
240
+ − 78
the difference consider
+ − 79
+ − 80
@{ML_response_fake [display,gray]
+ − 81
"let
261
+ − 82
val input = \"\<foo> bar\"
240
+ − 83
in
+ − 84
(explode input, Symbol.explode input)
+ − 85
end"
+ − 86
"([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"],
261
+ − 87
[\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
240
+ − 88
256
+ − 89
Slightly more general than the parser @{ML "$$"} is the function
316
+ − 90
@{ML_ind one in Scan}, in that it takes a predicate as argument and
256
+ − 91
then parses exactly
52
+ − 92
one item from the input list satisfying this predicate. For example the
58
+ − 93
following parser either consumes an @{text [quotes] "h"} or a @{text
49
+ − 94
[quotes] "w"}:
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 95
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 96
@{ML_response [display,gray]
40
+ − 97
"let
+ − 98
val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")
240
+ − 99
val input1 = Symbol.explode \"hello\"
+ − 100
val input2 = Symbol.explode \"world\"
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 101
in
236
+ − 102
(hw input1, hw input2)
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 103
end"
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 104
"((\"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
+ − 105
316
+ − 106
Two parsers can be connected in sequence by using the function @{ML_ind "--"}.
220
+ − 107
For example parsing @{text "h"}, @{text "e"} and @{text "l"} (in this
+ − 108
order) you can achieve by:
38
+ − 109
236
+ − 110
@{ML_response [display,gray]
240
+ − 111
"($$ \"h\" -- $$ \"e\" -- $$ \"l\") (Symbol.explode \"hello\")"
236
+ − 112
"(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 113
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 114
Note how the result of consumed strings builds up on the left as nested pairs.
38
+ − 115
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
+ − 116
If, as in the previous example, you want to parse a particular string,
326
+ − 117
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
+ − 118
236
+ − 119
@{ML_response [display,gray]
240
+ − 120
"Scan.this_string \"hell\" (Symbol.explode \"hello\")"
236
+ − 121
"(\"hell\", [\"o\"])"}
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 122
256
+ − 123
Parsers that explore alternatives can be constructed using the function
316
+ − 124
@{ML_ind "||"}. The parser @{ML "(p || q)" for p q} returns the
58
+ − 125
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
+ − 126
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
+ − 127
38
+ − 128
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 129
@{ML_response [display,gray]
40
+ − 130
"let
236
+ − 131
val hw = $$ \"h\" || $$ \"w\"
240
+ − 132
val input1 = Symbol.explode \"hello\"
+ − 133
val input2 = Symbol.explode \"world\"
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 134
in
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 135
(hw input1, hw input2)
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 136
end"
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 137
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
38
+ − 138
321
+ − 139
The functions @{ML_ind "|--"} and @{ML_ind "--|"} work like the sequencing
+ − 140
function for parsers, except that they discard the item being parsed by the
+ − 141
first (respectively second) parser. For example:
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 142
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 143
@{ML_response [display,gray]
40
+ − 144
"let
236
+ − 145
val just_e = $$ \"h\" |-- $$ \"e\"
+ − 146
val just_h = $$ \"h\" --| $$ \"e\"
240
+ − 147
val input = Symbol.explode \"hello\"
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 148
in
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 149
(just_e input, just_h input)
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 150
end"
241
+ − 151
"((\"e\", [\"l\", \"l\", \"o\"]), (\"h\", [\"l\", \"l\", \"o\"]))"}
38
+ − 152
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 153
The parser @{ML "Scan.optional p x" for p x} returns the result of the parser
58
+ − 154
@{text "p"}, if it succeeds; otherwise it returns
104
+ − 155
the default value @{text "x"}. For example:
38
+ − 156
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 157
@{ML_response [display,gray]
40
+ − 158
"let
+ − 159
val p = Scan.optional ($$ \"h\") \"x\"
240
+ − 160
val input1 = Symbol.explode \"hello\"
+ − 161
val input2 = Symbol.explode \"world\"
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 162
in
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 163
(p input1, p input2)
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 164
end"
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 165
"((\"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
+ − 166
316
+ − 167
The function @{ML_ind option in Scan} works similarly, except no default value can
50
+ − 168
be given. Instead, the result is wrapped as an @{text "option"}-type. For example:
+ − 169
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 170
@{ML_response [display,gray]
50
+ − 171
"let
+ − 172
val p = Scan.option ($$ \"h\")
240
+ − 173
val input1 = Symbol.explode \"hello\"
+ − 174
val input2 = Symbol.explode \"world\"
50
+ − 175
in
+ − 176
(p input1, p input2)
+ − 177
end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
49
+ − 178
326
+ − 179
The function @{ML_ind ahead in Scan} parses some input, but leaves the original
+ − 180
input unchanged. For example:
+ − 181
+ − 182
@{ML_response [display,gray]
+ − 183
"Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")"
+ − 184
"(\"foo\", [\"f\", \"o\", \"o\"])"}
+ − 185
+ − 186
The function @{ML_ind "!!"} helps with producing appropriate error messages
+ − 187
during parsing. For example if you want to parse @{text p} immediately
58
+ − 188
followed by @{text q}, or start a completely different parser @{text r},
104
+ − 189
you might write:
40
+ − 190
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 191
@{ML [display,gray] "(p -- q) || r" for p q r}
40
+ − 192
326
+ − 193
However, this parser is problematic for producing a useful error
+ − 194
message, if the parsing of @{ML "(p -- q)" for p q} fails. Because with the
+ − 195
parser above you lose the information that @{text p} should be followed by @{text q}.
220
+ − 196
To see this assume that @{text p} is present in the input, but it is not
+ − 197
followed by @{text q}. That means @{ML "(p -- q)" for p q} will fail and
+ − 198
hence the alternative parser @{text r} will be tried. However, in many
236
+ − 199
circumstances this will be the wrong parser for the input ``@{text "p"}-followed-by-something''
220
+ − 200
and therefore will also fail. The error message is then caused by the failure
+ − 201
of @{text r}, not by the absence of @{text q} in the input. This kind of
+ − 202
situation can be avoided when using the function @{ML "!!"}. This function
+ − 203
aborts the whole process of parsing in case of a failure and prints an error
+ − 204
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
+ − 205
40
+ − 206
236
+ − 207
@{ML [display,gray] "!! (fn _ => \"foo\") ($$ \"h\")"}
40
+ − 208
58
+ − 209
on @{text [quotes] "hello"}, the parsing succeeds
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 210
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 211
@{ML_response [display,gray]
240
+ − 212
"(!! (fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")"
236
+ − 213
"(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
40
+ − 214
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
+ − 215
but if you invoke it on @{text [quotes] "world"}
40
+ − 216
240
+ − 217
@{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
+ − 218
"Exception ABORT raised"}
40
+ − 219
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 220
then the parsing aborts and the error message @{text "foo"} is printed. In order to
120
+ − 221
see the error message properly, you need to prefix the parser with the function
316
+ − 222
@{ML_ind error in Scan}. For example:
40
+ − 223
236
+ − 224
@{ML_response_fake [display,gray]
+ − 225
"Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
+ − 226
"Exception Error \"foo\" raised"}
40
+ − 227
316
+ − 228
This ``prefixing'' is usually done by wrappers such as @{ML_ind local_theory in OuterSyntax}
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
+ − 229
(see Section~\ref{sec:newcommand} which explains this function in more detail).
40
+ − 230
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
+ − 231
Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
326
+ − 232
r}. If you want to generate the correct error message for failure
+ − 233
of parsing @{text "p"}-followed-by-@{text "q"}, then you have to write:
38
+ − 234
*}
+ − 235
69
+ − 236
ML{*fun p_followed_by_q p q r =
133
+ − 237
let
236
+ − 238
val err_msg = fn _ => p ^ " is not followed by " ^ q
133
+ − 239
in
+ − 240
($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
+ − 241
end *}
38
+ − 242
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 243
40
+ − 244
text {*
220
+ − 245
Running this parser with the arguments
+ − 246
@{text [quotes] "h"}, @{text [quotes] "e"} and @{text [quotes] "w"}, and
65
+ − 247
the input @{text [quotes] "holle"}
40
+ − 248
240
+ − 249
@{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
+ − 250
"Exception ERROR \"h is not followed by e\" raised"}
40
+ − 251
65
+ − 252
produces the correct error message. Running it with
40
+ − 253
240
+ − 254
@{ML_response [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"wworld\")"
40
+ − 255
"((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
+ − 256
+ − 257
yields the expected parsing.
38
+ − 258
58
+ − 259
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
+ − 260
often as it succeeds. For example:
40
+ − 261
240
+ − 262
@{ML_response [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")"
40
+ − 263
"([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
+ − 264
316
+ − 265
Note that @{ML_ind repeat in Scan} stores the parsed items in a list. The function
+ − 266
@{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
+ − 267
succeeds at least once.
48
+ − 268
58
+ − 269
Also note that the parser would have aborted with the exception @{text MORE}, if
326
+ − 270
you had it run with the string @{text [quotes] "hhhh"}. This can be avoided by using
316
+ − 271
the wrapper @{ML_ind finite in Scan} and the ``stopper-token''
+ − 272
@{ML_ind stopper in Symbol}. With them you can write:
49
+ − 273
240
+ − 274
@{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")"
49
+ − 275
"([\"h\", \"h\", \"h\", \"h\"], [])"}
+ − 276
326
+ − 277
The function @{ML stopper in Symbol} is the ``end-of-input'' indicator for parsing strings;
128
+ − 278
other stoppers need to be used when parsing, for example, tokens. However, this kind of
65
+ − 279
manually wrapping is often already done by the surrounding infrastructure.
49
+ − 280
316
+ − 281
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
+ − 282
string as in
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 283
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 284
@{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
+ − 285
"let
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 286
val p = Scan.repeat (Scan.one Symbol.not_eof)
240
+ − 287
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
+ − 288
in
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 289
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
+ − 290
end"
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 291
"([\"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
+ − 292
316
+ − 293
where the function @{ML_ind not_eof in Symbol} ensures that we do not read beyond the
65
+ − 294
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
+ − 295
316
+ − 296
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
+ − 297
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
+ − 298
240
+ − 299
@{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
+ − 300
"Exception FAIL raised"}
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 301
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 302
fails, while
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 303
240
+ − 304
@{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
+ − 305
"(\"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
+ − 306
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 307
succeeds.
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 308
316
+ − 309
The functions @{ML_ind repeat in Scan} and @{ML_ind unless in Scan} can
256
+ − 310
be combined to read any input until a certain marker symbol is reached. In the
+ − 311
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
+ − 312
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 313
@{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
+ − 314
"let
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 315
val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))
240
+ − 316
val input1 = Symbol.explode \"fooooo\"
+ − 317
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
+ − 318
in
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 319
(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
+ − 320
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
+ − 321
end"
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 322
"(([\"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
+ − 323
([\"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
+ − 324
256
+ − 325
220
+ − 326
After parsing is done, you almost always want to apply a function to the parsed
316
+ − 327
items. One way to do this is the function @{ML_ind ">>"} where
256
+ − 328
@{ML "(p >> f)" for p f} runs
58
+ − 329
first the parser @{text p} and upon successful completion applies the
+ − 330
function @{text f} to the result. For example
38
+ − 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]
40
+ − 333
"let
193
+ − 334
fun double (x, y) = (x ^ x, y ^ y)
326
+ − 335
val parser = $$ \"h\" -- $$ \"e\"
40
+ − 336
in
326
+ − 337
(parser >> double) (Symbol.explode \"hello\")
40
+ − 338
end"
+ − 339
"((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}
+ − 340
104
+ − 341
doubles the two parsed input strings; or
59
+ − 342
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 343
@{ML_response [display,gray]
59
+ − 344
"let
104
+ − 345
val p = Scan.repeat (Scan.one Symbol.not_eof)
240
+ − 346
val input = Symbol.explode \"foo bar foo\"
59
+ − 347
in
104
+ − 348
Scan.finite Symbol.stopper (p >> implode) input
59
+ − 349
end"
+ − 350
"(\"foo bar foo\",[])"}
+ − 351
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
+ − 352
where the single-character strings in the parsed output are transformed
59
+ − 353
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
+ − 354
316
+ − 355
The function @{ML_ind lift in Scan} takes a parser and a pair as arguments. This function applies
40
+ − 356
the given parser to the second component of the pair and leaves the first component
+ − 357
untouched. For example
38
+ − 358
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 359
@{ML_response [display,gray]
240
+ − 360
"Scan.lift ($$ \"h\" -- $$ \"e\") (1, Symbol.explode \"hello\")"
40
+ − 361
"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
+ − 362
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 363
(FIXME: In which situations is this useful? Give examples.)
149
+ − 364
+ − 365
\begin{exercise}\label{ex:scancmts}
+ − 366
Write a parser that parses an input string so that any comment enclosed
220
+ − 367
within @{text "(*\<dots>*)"} is replaced by the same comment but enclosed within
149
+ − 368
@{text "(**\<dots>**)"} in the output string. To enclose a string, you can use the
+ − 369
function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML
236
+ − 370
"s1 ^ s ^ s2" for s1 s2 s}. Hint: To simplify the task ignore the proper
+ − 371
nesting of comments.
149
+ − 372
\end{exercise}
40
+ − 373
*}
+ − 374
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 375
section {* Parsing Theory Syntax *}
38
+ − 376
40
+ − 377
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
+ − 378
Most of the time, however, Isabelle developers have to deal with parsing
156
+ − 379
tokens, not strings. These token parsers have the type:
128
+ − 380
*}
+ − 381
+ − 382
ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}
+ − 383
+ − 384
text {*
149
+ − 385
The reason for using token parsers is that theory syntax, as well as the
128
+ − 386
parsers for the arguments of proof methods, use the type @{ML_type
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 387
OuterLex.token}.
42
+ − 388
+ − 389
\begin{readmore}
40
+ − 390
The parser functions for the theory syntax are contained in the structure
42
+ − 391
@{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}.
+ − 392
The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}.
+ − 393
\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
+ − 394
316
+ − 395
The structure @{ML_struct OuterLex} defines several kinds of tokens (for
+ − 396
example @{ML_ind Ident in OuterLex} for identifiers, @{ML Keyword in
+ − 397
OuterLex} for keywords and @{ML_ind Command in OuterLex} for commands). Some
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 398
token parsers take into account the kind of tokens. The first example shows
256
+ − 399
how to generate a token list out of a string using the function
316
+ − 400
@{ML_ind scan in OuterSyntax}. It is given the argument
256
+ − 401
@{ML "Position.none"} since,
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 402
at the moment, we are not interested in generating precise error
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 403
messages. The following code\footnote{Note that because of a possible bug in
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 404
the PolyML runtime system, the result is printed as @{text [quotes] "?"},
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 405
instead of the tokens.}
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 406
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
+ − 407
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 408
@{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\""
50
+ − 409
"[Token (\<dots>,(Ident, \"hello\"),\<dots>),
+ − 410
Token (\<dots>,(Space, \" \"),\<dots>),
+ − 411
Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
+ − 412
+ − 413
produces three tokens where the first and the last are identifiers, since
58
+ − 414
@{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
+ − 415
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
+ − 416
326
+ − 417
We can easily change what is recognised as a keyword with the function
+ − 418
@{ML_ind keyword in OuterKeyword}. For example calling it with
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 419
*}
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 420
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 421
ML{*val _ = OuterKeyword.keyword "hello"*}
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 422
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 423
text {*
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 424
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
+ − 425
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 426
@{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\""
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 427
"[Token (\<dots>,(Keyword, \"hello\"),\<dots>),
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 428
Token (\<dots>,(Space, \" \"),\<dots>),
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 429
Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
50
+ − 430
241
+ − 431
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
+ − 432
to have already been filtered out. So from now on we are going to use the
316
+ − 433
functions @{ML filter} and @{ML_ind is_proper in OuterLex} to do this.
256
+ − 434
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
+ − 435
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 436
@{ML_response_fake [display,gray]
50
+ − 437
"let
+ − 438
val input = OuterSyntax.scan Position.none \"hello world\"
+ − 439
in
+ − 440
filter OuterLex.is_proper input
+ − 441
end"
+ − 442
"[Token (\<dots>,(Ident, \"hello\"), \<dots>), Token (\<dots>,(Ident, \"world\"), \<dots>)]"}
+ − 443
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
+ − 444
For convenience we define the function:
50
+ − 445
*}
+ − 446
69
+ − 447
ML{*fun filtered_input str =
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 448
filter OuterLex.is_proper (OuterSyntax.scan Position.none str) *}
50
+ − 449
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 450
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
+ − 451
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
+ − 452
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 453
@{ML_response_fake [display,gray]
50
+ − 454
"filtered_input \"inductive | for\""
+ − 455
"[Token (\<dots>,(Command, \"inductive\"),\<dots>),
+ − 456
Token (\<dots>,(Keyword, \"|\"),\<dots>),
+ − 457
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
+ − 458
221
+ − 459
you obtain a list consisting of only one command and two keyword tokens.
241
+ − 460
If you want to see which keywords and commands are currently known to Isabelle,
+ − 461
type:
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 462
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 463
@{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
+ − 464
"let
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 465
val (keywords, commands) = OuterKeyword.get_lexicons ()
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 466
in
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 467
(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
+ − 468
end"
132
+ − 469
"([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
42
+ − 470
316
+ − 471
You might have to adjust the @{ML_ind print_depth} in order to
241
+ − 472
see the complete list.
+ − 473
316
+ − 474
The parser @{ML_ind "$$$" in OuterParse} parses a single keyword. For example:
50
+ − 475
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 476
@{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
+ − 477
"let
50
+ − 478
val input1 = filtered_input \"where for\"
+ − 479
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
+ − 480
in
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
+ − 481
(OuterParse.$$$ \"where\" input1, OuterParse.$$$ \"|\" input2)
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
+ − 482
end"
128
+ − 483
"((\"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
+ − 484
316
+ − 485
Any non-keyword string can be parsed with the function @{ML_ind reserved in OuterParse}.
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 486
For example:
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 487
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 488
@{ML_response [display,gray]
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 489
"let
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 490
val p = OuterParse.reserved \"bar\"
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 491
val input = filtered_input \"bar\"
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 492
in
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 493
p input
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 494
end"
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 495
"(\"bar\",[])"}
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 496
316
+ − 497
Like before, you can sequentially connect parsers with @{ML_ind "--"}. 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
+ − 498
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 499
@{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
+ − 500
"let
50
+ − 501
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
+ − 502
in
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
+ − 503
(OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\") input
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
+ − 504
end"
183
+ − 505
"((\"|\", \"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
+ − 506
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 507
The parser @{ML "OuterParse.enum s p" for s p} parses a possibly empty
58
+ − 508
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
+ − 509
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
+ − 510
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 511
@{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
+ − 512
"let
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 513
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
+ − 514
in
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
+ − 515
(OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
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
+ − 516
end"
183
+ − 517
"([\"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
+ − 518
326
+ − 519
The function @{ML_ind enum1 in OuterParse} works similarly, except that the
+ − 520
parsed list must be non-empty. Note that we had to add a string @{text
+ − 521
[quotes] "foo"} at the end of the parsed string, otherwise the parser would
+ − 522
have consumed all tokens and then failed with the exception @{text
+ − 523
"MORE"}. Like in the previous section, we can avoid this exception using the
+ − 524
wrapper @{ML Scan.finite}. This time, however, we have to use the
+ − 525
``stopper-token'' @{ML OuterLex.stopper}. We can write:
49
+ − 526
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 527
@{ML_response [display,gray]
49
+ − 528
"let
50
+ − 529
val input = filtered_input \"in | in | in\"
326
+ − 530
val p = OuterParse.enum \"|\" (OuterParse.$$$ \"in\")
49
+ − 531
in
326
+ − 532
Scan.finite OuterLex.stopper p input
49
+ − 533
end"
183
+ − 534
"([\"in\", \"in\", \"in\"], [])"}
49
+ − 535
75
+ − 536
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
+ − 537
*}
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 538
69
+ − 539
ML{*fun parse p input = Scan.finite OuterLex.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
+ − 540
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 541
text {*
326
+ − 542
The function @{ML_ind "!!!" in OuterParse} can be used to force termination
+ − 543
of the parser in case of a dead end, just like @{ML "Scan.!!"} (see previous
+ − 544
section). A difference, however, is that the error message of @{ML
+ − 545
"OuterParse.!!!"} is fixed to be @{text [quotes] "Outer syntax error"}
221
+ − 546
together with a relatively precise description of the failure. For example:
49
+ − 547
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 548
@{ML_response_fake [display,gray]
49
+ − 549
"let
50
+ − 550
val input = filtered_input \"in |\"
49
+ − 551
val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\"
+ − 552
in
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 553
parse (OuterParse.!!! parse_bar_then_in) input
49
+ − 554
end"
+ − 555
"Exception ERROR \"Outer syntax error: keyword \"|\" expected,
+ − 556
but keyword in was found\" raised"
+ − 557
}
42
+ − 558
65
+ − 559
\begin{exercise} (FIXME)
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 560
A type-identifier, for example @{typ "'a"}, is a token of
316
+ − 561
kind @{ML_ind Keyword in OuterLex}. It can be parsed using
256
+ − 562
the function @{ML type_ident in OuterParse}.
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 563
\end{exercise}
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 564
104
+ − 565
(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
+ − 566
125
+ − 567
Whenever there is a possibility that the processing of user input can fail,
221
+ − 568
it is a good idea to give all available information about where the error
220
+ − 569
occurred. For this Isabelle can attach positional information to tokens
326
+ − 570
and then thread this information up the ``processing chain''. To see this,
+ − 571
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
+ − 572
*}
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 573
125
+ − 574
ML{*fun filtered_input' str =
+ − 575
filter OuterLex.is_proper (OuterSyntax.scan (Position.line 7) str) *}
49
+ − 576
+ − 577
text {*
125
+ − 578
where we pretend the parsed string starts on line 7. An example is
49
+ − 579
125
+ − 580
@{ML_response_fake [display,gray]
+ − 581
"filtered_input' \"foo \\n bar\""
+ − 582
"[Token ((\"foo\", ({line=7, end_line=7}, {line=7})), (Ident, \"foo\"), \<dots>),
+ − 583
Token ((\"bar\", ({line=8, end_line=8}, {line=8})), (Ident, \"bar\"), \<dots>)]"}
+ − 584
+ − 585
in which the @{text [quotes] "\\n"} causes the second token to be in
+ − 586
line 8.
+ − 587
326
+ − 588
By using the parser @{ML position in OuterParse} you can access the token
+ − 589
position and return it as part of the parser result. For example
125
+ − 590
+ − 591
@{ML_response_fake [display,gray]
+ − 592
"let
241
+ − 593
val input = filtered_input' \"where\"
125
+ − 594
in
+ − 595
parse (OuterParse.position (OuterParse.$$$ \"where\")) input
+ − 596
end"
+ − 597
"((\"where\", {line=7, end_line=7}), [])"}
+ − 598
+ − 599
\begin{readmore}
+ − 600
The functions related to positions are implemented in the file
+ − 601
@{ML_file "Pure/General/position.ML"}.
+ − 602
\end{readmore}
49
+ − 603
+ − 604
*}
+ − 605
326
+ − 606
section {* Parsers for ML-Code (TBD) *}
+ − 607
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 608
text {*
326
+ − 609
@{ML_ind ML_source in OuterParse}
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 610
*}
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 611
193
+ − 612
section {* Context Parser (TBD) *}
+ − 613
+ − 614
text {*
326
+ − 615
@{ML_ind Args.context}
+ − 616
*}
+ − 617
(*
+ − 618
ML {*
+ − 619
let
+ − 620
val parser = Args.context -- Scan.lift Args.name_source
+ − 621
+ − 622
fun term_pat (ctxt, str) =
+ − 623
str |> Syntax.read_prop ctxt
+ − 624
in
+ − 625
(parser >> term_pat) (Context.Proof @{context}, filtered_input "f (a::nat)")
+ − 626
|> fst
+ − 627
end
+ − 628
*}
+ − 629
*)
+ − 630
+ − 631
text {*
+ − 632
@{ML_ind Args.context}
+ − 633
193
+ − 634
Used for example in \isacommand{attribute\_setup} and \isacommand{method\_setup}.
+ − 635
*}
+ − 636
207
+ − 637
section {* Argument and Attribute Parsers (TBD) *}
+ − 638
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
+ − 639
section {* Parsing Inner Syntax *}
42
+ − 640
125
+ − 641
text {*
+ − 642
There is usually no need to write your own parser for parsing inner syntax, that is
285
+ − 643
for terms and types: you can just call the predefined parsers. Terms can
326
+ − 644
be parsed using the function @{ML_ind term in OuterParse}. For example:
125
+ − 645
+ − 646
@{ML_response [display,gray]
+ − 647
"let
+ − 648
val input = OuterSyntax.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
+ − 649
in
125
+ − 650
OuterParse.term input
+ − 651
end"
+ − 652
"(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"}
+ − 653
326
+ − 654
The function @{ML_ind prop in OuterParse} is similar, except that it gives a different
127
+ − 655
error message, when parsing fails. As you can see, the parser not just returns
+ − 656
the parsed string, but also some encoded information. You can decode the
326
+ − 657
information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}. For example
127
+ − 658
+ − 659
@{ML_response [display,gray]
+ − 660
"YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
+ − 661
"XML.Elem (\"token\", [], [XML.Text \"foo\"])"}
+ − 662
149
+ − 663
The result of the decoding is an XML-tree. You can see better what is going on if
131
+ − 664
you replace @{ML Position.none} by @{ML "Position.line 42"}, say:
101
+ − 665
125
+ − 666
@{ML_response [display,gray]
+ − 667
"let
+ − 668
val input = OuterSyntax.scan (Position.line 42) \"foo\"
+ − 669
in
127
+ − 670
YXML.parse (fst (OuterParse.term input))
125
+ − 671
end"
127
+ − 672
"XML.Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
125
+ − 673
149
+ − 674
The positional information is stored as part of an XML-tree so that code
+ − 675
called later on will be able to give more precise error messages.
125
+ − 676
127
+ − 677
\begin{readmore}
128
+ − 678
The functions to do with input and output of XML and YXML are defined
127
+ − 679
in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}.
+ − 680
\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
+ − 681
125
+ − 682
*}
101
+ − 683
116
+ − 684
section {* Parsing Specifications\label{sec:parsingspecs} *}
101
+ − 685
+ − 686
text {*
121
+ − 687
There are a number of special purpose parsers that help with parsing
156
+ − 688
specifications of function definitions, inductive predicates and so on. In
220
+ − 689
Chapter~\ref{chp:package}, for example, we will need to parse specifications
121
+ − 690
for inductive predicates of the form:
+ − 691
*}
101
+ − 692
121
+ − 693
simple_inductive
+ − 694
even and odd
+ − 695
where
+ − 696
even0: "even 0"
+ − 697
| evenS: "odd n \<Longrightarrow> even (Suc n)"
+ − 698
| oddS: "even n \<Longrightarrow> odd (Suc n)"
101
+ − 699
327
+ − 700
101
+ − 701
text {*
121
+ − 702
For this we are going to use the parser:
101
+ − 703
*}
+ − 704
121
+ − 705
ML %linenosgray{*val spec_parser =
126
+ − 706
OuterParse.fixes --
+ − 707
Scan.optional
+ − 708
(OuterParse.$$$ "where" |--
+ − 709
OuterParse.!!!
+ − 710
(OuterParse.enum1 "|"
+ − 711
(SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
120
+ − 712
101
+ − 713
text {*
241
+ − 714
Note that the parser must not parse the keyword \simpleinductive, even if it is
126
+ − 715
meant to process definitions as shown above. The parser of the keyword
128
+ − 716
will be given by the infrastructure that will eventually call @{ML spec_parser}.
126
+ − 717
+ − 718
124
+ − 719
To see what the parser returns, let us parse the string corresponding to the
121
+ − 720
definition of @{term even} and @{term odd}:
+ − 721
101
+ − 722
@{ML_response [display,gray]
+ − 723
"let
+ − 724
val input = filtered_input
+ − 725
(\"even and odd \" ^
+ − 726
\"where \" ^
+ − 727
\" even0[intro]: \\\"even 0\\\" \" ^
+ − 728
\"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^
+ − 729
\"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
+ − 730
in
120
+ − 731
parse spec_parser input
101
+ − 732
end"
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 733
"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
101
+ − 734
[((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
+ − 735
((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
+ − 736
((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
121
+ − 737
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 738
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
+ − 739
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
+ − 740
rules where every rule has optionally a name and an attribute.
121
+ − 741
316
+ − 742
The function @{ML_ind "fixes" in OuterParse} 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
+ − 743
\isacommand{and}-separated
124
+ − 744
list of variables that can include optional type annotations and syntax translations.
121
+ − 745
For example:\footnote{Note that in the code we need to write
+ − 746
@{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes
+ − 747
in the compound type.}
+ − 748
+ − 749
@{ML_response [display,gray]
+ − 750
"let
+ − 751
val input = filtered_input
+ − 752
\"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
+ − 753
in
219
+ − 754
parse OuterParse.fixes input
121
+ − 755
end"
+ − 756
"([(foo, SOME \"\\^E\\^Ftoken\\^Eint \<Rightarrow> bool\\^E\\^F\\^E\", NoSyn),
+ − 757
(bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)),
+ − 758
(blonk, NONE, NoSyn)],[])"}
50
+ − 759
*}
+ − 760
121
+ − 761
text {*
156
+ − 762
Whenever types are given, they are stored in the @{ML SOME}s. The types are
+ − 763
not yet used to type the variables: this must be done by type-inference later
149
+ − 764
on. Since types are part of the inner syntax they are strings with some
241
+ − 765
encoded information (see previous section). If a mixfix-syntax is
316
+ − 766
present for a variable, then it is stored in the @{ML_ind Mixfix} data structure;
+ − 767
no syntax translation is indicated by @{ML_ind NoSyn}.
121
+ − 768
+ − 769
\begin{readmore}
241
+ − 770
The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
121
+ − 771
\end{readmore}
+ − 772
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 773
Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
219
+ − 774
list of introduction rules, that is propositions with theorem annotations
+ − 775
such as rule names and attributes. The introduction rules are propositions
316
+ − 776
parsed by @{ML_ind prop in OuterParse}. However, they can include an optional
219
+ − 777
theorem name plus some attributes. For example
121
+ − 778
+ − 779
@{ML_response [display,gray] "let
+ − 780
val input = filtered_input \"foo_lemma[intro,dest!]:\"
+ − 781
val ((name, attrib), _) = parse (SpecParse.thm_name \":\") input
+ − 782
in
+ − 783
(name, map Args.dest_src attrib)
+ − 784
end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
+ − 785
316
+ − 786
The function @{ML_ind opt_thm_name in SpecParse} is the ``optional'' variant of
+ − 787
@{ML_ind thm_name in SpecParse}. Theorem names can contain attributes. The name
131
+ − 788
has to end with @{text [quotes] ":"}---see the argument of
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 789
the function @{ML SpecParse.opt_thm_name} in Line 7.
121
+ − 790
+ − 791
\begin{readmore}
+ − 792
Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"}
+ − 793
and @{ML_file "Pure/Isar/args.ML"}.
+ − 794
\end{readmore}
101
+ − 795
*}
65
+ − 796
193
+ − 797
text_raw {*
+ − 798
\begin{exercise}
207
+ − 799
Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented
+ − 800
in file @{ML_file "Pure/Isar/spec_parse.ML"}. This parser corresponds
+ − 801
to the ``where-part'' of the introduction rules given above. Below
316
+ − 802
we paraphrase the code of @{ML_ind where_alt_specs in SpecParse} adapted to our
207
+ − 803
purposes.
193
+ − 804
\begin{isabelle}
+ − 805
*}
+ − 806
ML %linenosgray{*val spec_parser' =
+ − 807
OuterParse.fixes --
+ − 808
Scan.optional
+ − 809
(OuterParse.$$$ "where" |--
+ − 810
OuterParse.!!!
+ − 811
(OuterParse.enum1 "|"
+ − 812
((SpecParse.opt_thm_name ":" -- OuterParse.prop) --|
+ − 813
Scan.option (Scan.ahead (OuterParse.name ||
+ − 814
OuterParse.$$$ "[") --
+ − 815
OuterParse.!!! (OuterParse.$$$ "|"))))) [] *}
+ − 816
text_raw {*
+ − 817
\end{isabelle}
284
+ − 818
Both parsers accept the same input% that's not true:
+ − 819
% spec_parser accepts input that is refuted by spec_parser'
+ − 820
, but if you look closely, you can notice
207
+ − 821
an additional ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of
+ − 822
this additional ``tail''?
193
+ − 823
\end{exercise}
+ − 824
*}
+ − 825
229
+ − 826
text {*
+ − 827
(FIXME: @{ML OuterParse.type_args}, @{ML OuterParse.typ}, @{ML OuterParse.opt_mixfix})
+ − 828
*}
+ − 829
+ − 830
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
+ − 831
section {* New Commands and Keyword Files\label{sec:newcommand} *}
65
+ − 832
+ − 833
text {*
68
+ − 834
Often new commands, for example for providing new definitional principles,
+ − 835
need to be implemented. While this is not difficult on the ML-level,
66
+ − 836
new commands, in order to be useful, need to be recognised by
65
+ − 837
ProofGeneral. This results in some subtle configuration issues, which we
+ − 838
will explain in this section.
+ − 839
74
+ − 840
To keep things simple, let us start with a ``silly'' command that does nothing
+ − 841
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
+ − 842
defined as:
68
+ − 843
*}
65
+ − 844
69
+ − 845
ML{*let
219
+ − 846
val do_nothing = Scan.succeed (LocalTheory.theory I)
68
+ − 847
val kind = OuterKeyword.thy_decl
65
+ − 848
in
219
+ − 849
OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
69
+ − 850
end *}
65
+ − 851
68
+ − 852
text {*
316
+ − 853
The crucial function @{ML_ind local_theory in OuterSyntax} expects a name for the command, a
219
+ − 854
short description, a kind indicator (which we will explain later more thoroughly) and a
+ − 855
parser producing a local theory transition (its purpose will also explained
66
+ − 856
later).
65
+ − 857
101
+ − 858
While this is everything you have to do on the ML-level, you need a keyword
68
+ − 859
file that can be loaded by ProofGeneral. This is to enable ProofGeneral to
+ − 860
recognise \isacommand{foobar} as a command. Such a keyword file can be
74
+ − 861
generated with the command-line:
68
+ − 862
74
+ − 863
@{text [display] "$ isabelle keywords -k foobar some_log_files"}
65
+ − 864
74
+ − 865
The option @{text "-k foobar"} indicates which postfix the name of the keyword file
80
+ − 866
will be assigned. In the case above the file will be named @{text
86
+ − 867
"isar-keywords-foobar.el"}. This command requires log files to be
68
+ − 868
present (in order to extract the keywords from them). To generate these log
101
+ − 869
files, you first need to package the code above into a separate theory file named
68
+ − 870
@{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the
+ − 871
complete code.
65
+ − 872
66
+ − 873
+ − 874
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 875
\begin{figure}[t]
69
+ − 876
\begin{graybox}\small
66
+ − 877
\isacommand{theory}~@{text Command}\\
+ − 878
\isacommand{imports}~@{text Main}\\
+ − 879
\isacommand{begin}\\
85
+ − 880
\isacommand{ML}~@{text "\<verbopen>"}\\
66
+ − 881
@{ML
+ − 882
"let
219
+ − 883
val do_nothing = Scan.succeed (LocalTheory.theory I)
68
+ − 884
val kind = OuterKeyword.thy_decl
66
+ − 885
in
219
+ − 886
OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing
66
+ − 887
end"}\\
85
+ − 888
@{text "\<verbclose>"}\\
66
+ − 889
\isacommand{end}
80
+ − 890
\end{graybox}
241
+ − 891
\caption{This file can be used to generate a log file. This log file in turn can
+ − 892
be used to generate a keyword file containing the command \isacommand{foobar}.
+ − 893
\label{fig:commandtheory}}
66
+ − 894
\end{figure}
+ − 895
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 896
75
+ − 897
For our purposes it is sufficient to use the log files of the theories
68
+ − 898
@{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as
75
+ − 899
the log file for the theory @{text "Command.thy"}, which contains the new
+ − 900
\isacommand{foobar}-command. If you target other logics besides HOL, such
74
+ − 901
as Nominal or ZF, then you need to adapt the log files appropriately.
104
+ − 902
74
+ − 903
@{text Pure} and @{text HOL} are usually compiled during the installation of
+ − 904
Isabelle. So log files for them should be already available. If not, then
75
+ − 905
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
+ − 906
distribution.
65
+ − 907
+ − 908
@{text [display]
+ − 909
"$ ./build -m \"Pure\"
+ − 910
$ ./build -m \"HOL\""}
+ − 911
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
+ − 912
The @{text "Pure-ProofGeneral"} theory needs to be compiled with:
65
+ − 913
+ − 914
@{text [display] "$ ./build -m \"Pure-ProofGeneral\" \"Pure\""}
+ − 915
101
+ − 916
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
+ − 917
with:
66
+ − 918
68
+ − 919
@{text [display] "$ isabelle mkdir FoobarCommand"}
66
+ − 920
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
+ − 921
This generates a directory containing the files:
66
+ − 922
+ − 923
@{text [display]
+ − 924
"./IsaMakefile
68
+ − 925
./FoobarCommand/ROOT.ML
+ − 926
./FoobarCommand/document
+ − 927
./FoobarCommand/document/root.tex"}
65
+ − 928
+ − 929
101
+ − 930
You need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
66
+ − 931
and add the line
+ − 932
207
+ − 933
@{text [display] "no_document use_thy \"Command\";"}
66
+ − 934
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
+ − 935
to the file @{text "./FoobarCommand/ROOT.ML"}. You can now compile the theory by just typing:
65
+ − 936
+ − 937
@{text [display] "$ isabelle make"}
+ − 938
101
+ − 939
If the compilation succeeds, you have finally created all the necessary log files.
+ − 940
They are stored in the directory
65
+ − 941
241
+ − 942
@{text [display] "~/.isabelle/heaps/Isabelle2009/polyml-5.2.1_x86-linux/log"}
65
+ − 943
74
+ − 944
or something similar depending on your Isabelle distribution and architecture.
+ − 945
One quick way to assign a shell variable to this directory is by typing
66
+ − 946
+ − 947
@{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
+ − 948
156
+ − 949
on the Unix prompt. If you now type @{text "ls $ISABELLE_LOGS"}, then the
128
+ − 950
directory should include the files:
65
+ − 951
+ − 952
@{text [display]
+ − 953
"Pure.gz
+ − 954
HOL.gz
+ − 955
Pure-ProofGeneral.gz
68
+ − 956
HOL-FoobarCommand.gz"}
65
+ − 957
101
+ − 958
From them you can create the keyword files. Assuming the name
75
+ − 959
of the directory is in @{text "$ISABELLE_LOGS"},
74
+ − 960
then the Unix command for creating the keyword file is:
65
+ − 961
+ − 962
@{text [display]
68
+ − 963
"$ isabelle keywords -k foobar
80
+ − 964
$ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
65
+ − 965
80
+ − 966
The result is the file @{text "isar-keywords-foobar.el"}. It should contain
321
+ − 967
the string @{text "foobar"} twice.\footnote{To see whether things are fine,
+ − 968
check that @{text "grep foobar"} on this file returns something non-empty.}
+ − 969
This keyword file needs to be copied into the directory @{text
+ − 970
"~/.isabelle/etc"}. To make ProofGeneral aware of it, you have to start
+ − 971
Isabelle with the option @{text "-k foobar"}, that is:
65
+ − 972
80
+ − 973
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
+ − 974
@{text [display] "$ isabelle emacs -k foobar a_theory_file"}
65
+ − 975
101
+ − 976
If you now build a theory on top of @{text "Command.thy"},
326
+ − 977
then you can use the command \isacommand{foobar}. You can just write
321
+ − 978
*}
+ − 979
+ − 980
foobar
+ − 981
+ − 982
text {*
+ − 983
but you will not see any action as we chose to implement this command to do
327
+ − 984
nothing. The point of this command is only to show the procedure of how
326
+ − 985
to interact with ProofGeneral. A similar procedure has to be done with any
+ − 986
other new command, and also any new keyword that is introduced with
327
+ − 987
the function @{ML_ind keyword in OuterKeyword}. For example:
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 988
*}
65
+ − 989
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 990
ML{*val _ = OuterKeyword.keyword "blink" *}
65
+ − 991
230
8def50824320
added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 992
text {*
321
+ − 993
At the moment the command \isacommand{foobar} is not very useful. Let us
+ − 994
refine it a bit next by letting it take a proposition as argument and
+ − 995
printing this proposition inside the tracing buffer.
68
+ − 996
75
+ − 997
The crucial part of a command is the function that determines the behaviour
+ − 998
of the command. In the code above we used a ``do-nothing''-function, which
316
+ − 999
because of @{ML_ind succeed in Scan} does not parse any argument, but immediately
219
+ − 1000
returns the simple function @{ML "LocalTheory.theory I"}. We can
75
+ − 1001
replace this code by a function that first parses a proposition (using the
+ − 1002
parser @{ML OuterParse.prop}), then prints out the tracing
219
+ − 1003
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
+ − 1004
finally does nothing. For this you can write:
68
+ − 1005
*}
+ − 1006
69
+ − 1007
ML{*let
219
+ − 1008
fun trace_prop str =
327
+ − 1009
LocalTheory.theory (fn ctxt => (tracing str; ctxt))
75
+ − 1010
68
+ − 1011
val kind = OuterKeyword.thy_decl
+ − 1012
in
321
+ − 1013
OuterSyntax.local_theory "foobar_trace" "traces a proposition"
327
+ − 1014
kind (OuterParse.prop >> trace_prop)
69
+ − 1015
end *}
68
+ − 1016
321
+ − 1017
text {*
+ − 1018
The command is now \isacommand{foobar\_trace} and can be used to
+ − 1019
see the proposition in the tracing buffer.
+ − 1020
*}
+ − 1021
+ − 1022
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
+ − 1023
68
+ − 1024
text {*
316
+ − 1025
Note that so far we used @{ML_ind thy_decl in OuterKeyword} as the kind
219
+ − 1026
indicator for the command. This means that the command finishes as soon as
+ − 1027
the arguments are processed. Examples of this kind of commands are
+ − 1028
\isacommand{definition} and \isacommand{declare}. In other cases, commands
+ − 1029
are expected to parse some arguments, for example a proposition, and then
+ − 1030
``open up'' a proof in order to prove the proposition (for example
86
+ − 1031
\isacommand{lemma}) or prove some other properties (for example
219
+ − 1032
\isacommand{function}). To achieve this kind of behaviour, you have to use
316
+ − 1033
the kind indicator @{ML_ind thy_goal in OuterKeyword} and the function @{ML
219
+ − 1034
"local_theory_to_proof" in OuterSyntax} to set up the command. Note,
+ − 1035
however, once you change the ``kind'' of a command from @{ML thy_decl in
+ − 1036
OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs
+ − 1037
to be re-created!
68
+ − 1038
327
+ − 1039
Below we show the command \isacommand{foobar\_goal} which takes a
+ − 1040
proposition as argument and then starts a proof in order to prove
+ − 1041
it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in
+ − 1042
OuterKeyword}.
68
+ − 1043
*}
+ − 1044
114
+ − 1045
ML%linenosgray{*let
327
+ − 1046
fun goal_prop str lthy =
68
+ − 1047
let
241
+ − 1048
val prop = Syntax.read_prop lthy str
68
+ − 1049
in
241
+ − 1050
Proof.theorem_i NONE (K I) [[(prop,[])]] lthy
327
+ − 1051
end
68
+ − 1052
+ − 1053
val kind = OuterKeyword.thy_goal
+ − 1054
in
327
+ − 1055
OuterSyntax.local_theory_to_proof "foobar_goal" "proves a proposition"
+ − 1056
kind (OuterParse.prop >> goal_prop)
69
+ − 1057
end *}
68
+ − 1058
+ − 1059
text {*
327
+ − 1060
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
+ − 1061
proved) and a context as argument. The context is necessary in order to be able to use
316
+ − 1062
@{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
+ − 1063
In Line 6 the function @{ML_ind theorem_i in Proof} starts the proof for the
75
+ − 1064
proposition. Its argument @{ML NONE} stands for a locale (which we chose to
+ − 1065
omit); the argument @{ML "(K I)"} stands for a function that determines what
+ − 1066
should be done with the theorem once it is proved (we chose to just forget
219
+ − 1067
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
+ − 1068
321
+ − 1069
If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \<and> True"},
+ − 1070
you obtain the following proof state
+ − 1071
*}
68
+ − 1072
321
+ − 1073
foobar_goal "True \<and> True"
+ − 1074
txt {*
+ − 1075
\begin{minipage}{\textwidth}
+ − 1076
@{subgoals [display]}
+ − 1077
\end{minipage}\medskip
68
+ − 1078
321
+ − 1079
and can prove the proposition as follows.
+ − 1080
*}
+ − 1081
apply(rule conjI)
+ − 1082
apply(rule TrueI)+
+ − 1083
done
+ − 1084
+ − 1085
text {*
327
+ − 1086
{\bf TBD below}
74
+ − 1087
316
+ − 1088
(FIXME: read a name and show how to store theorems; see @{ML_ind note in LocalTheory})
241
+ − 1089
65
+ − 1090
*}
+ − 1091
328
+ − 1092
ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*}
321
+ − 1093
ML{*let
324
+ − 1094
fun after_qed thm_name thms lthy =
+ − 1095
LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd
+ − 1096
+ − 1097
fun setup_proof (thm_name, (txt, pos)) lthy =
321
+ − 1098
let
+ − 1099
val trm = ML_Context.evaluate lthy true ("r", r) txt
+ − 1100
in
324
+ − 1101
Proof.theorem_i NONE (after_qed thm_name) [[(trm,[])]] lthy
+ − 1102
end
321
+ − 1103
324
+ − 1104
val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
321
+ − 1105
in
+ − 1106
OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition"
324
+ − 1107
OuterKeyword.thy_goal (parser >> setup_proof)
321
+ − 1108
end*}
+ − 1109
324
+ − 1110
foobar_prove test: {* @{prop "True"} *}
321
+ − 1111
apply(rule TrueI)
+ − 1112
done
+ − 1113
322
+ − 1114
(*
+ − 1115
ML {*
+ − 1116
structure TacticData = ProofDataFun
+ − 1117
(
+ − 1118
type T = thm list -> tactic;
+ − 1119
fun init _ = undefined;
+ − 1120
);
+ − 1121
+ − 1122
val set_tactic = TacticData.put;
+ − 1123
*}
+ − 1124
+ − 1125
ML {*
+ − 1126
TacticData.get @{context}
+ − 1127
*}
+ − 1128
+ − 1129
ML {* Method.set_tactic *}
+ − 1130
ML {* fun tactic (facts: thm list) : tactic = (atac 1) *}
+ − 1131
ML {* Context.map_proof *}
+ − 1132
ML {* ML_Context.expression *}
+ − 1133
ML {* METHOD *}
+ − 1134
+ − 1135
+ − 1136
ML {*
+ − 1137
fun myexpression pos bind body txt =
+ − 1138
let
+ − 1139
val _ = tracing ("bind)" ^ bind)
+ − 1140
val _ = tracing ("body)" ^ body)
+ − 1141
val _ = tracing ("txt)" ^ txt)
+ − 1142
val _ = tracing ("result) " ^ "Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
+ − 1143
" end (ML_Context.the_generic_context ())));")
+ − 1144
in
+ − 1145
ML_Context.exec (fn () => ML_Context.eval false pos
+ − 1146
("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
+ − 1147
" end (ML_Context.the_generic_context ())));"))
+ − 1148
end
+ − 1149
*}
319
+ − 1150
+ − 1151
322
+ − 1152
ML {*
+ − 1153
fun ml_tactic (txt, pos) ctxt =
+ − 1154
let
+ − 1155
val ctxt' = ctxt |> Context.proof_map
+ − 1156
(myexpression pos
+ − 1157
"fun tactic (facts: thm list) : tactic"
+ − 1158
"Context.map_proof (Method.set_tactic tactic)" txt);
+ − 1159
in
+ − 1160
Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt')
+ − 1161
end;
+ − 1162
*}
+ − 1163
+ − 1164
ML {*
+ − 1165
fun tactic3 (txt, pos) ctxt =
+ − 1166
let
+ − 1167
val _ = tracing ("1) " ^ txt )
+ − 1168
in
+ − 1169
METHOD (ml_tactic (txt, pos) ctxt; K (atac 1))
+ − 1170
end
+ − 1171
*}
+ − 1172
+ − 1173
setup {*
+ − 1174
Method.setup (Binding.name "tactic3") (Scan.lift (OuterParse.position Args.name)
+ − 1175
>> tactic3)
+ − 1176
"ML tactic as proof method"
+ − 1177
*}
+ − 1178
+ − 1179
lemma "A \<Longrightarrow> A"
+ − 1180
apply(tactic3 {* (atac 1) *})
+ − 1181
done
+ − 1182
+ − 1183
ML {*
+ − 1184
(ML_Context.the_generic_context ())
+ − 1185
*}
+ − 1186
+ − 1187
ML {*
+ − 1188
Context.set_thread_data;
+ − 1189
ML_Context.the_generic_context
+ − 1190
*}
+ − 1191
+ − 1192
lemma "A \<Longrightarrow> A"
+ − 1193
ML_prf {*
+ − 1194
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 ())));
+ − 1195
*}
+ − 1196
+ − 1197
ML {*
+ − 1198
Context.set_thread_data (SOME ((let fun tactic (facts: thm list) : tactic = (atac 1) in 3 end) (ML_Context.the_generic_context ())));
+ − 1199
*}
+ − 1200
+ − 1201
ML {*
+ − 1202
Context.set_thread_data (SOME (let
+ − 1203
fun tactic (facts: thm list) : tactic = (atac 1)
+ − 1204
in
+ − 1205
Context.map_proof (Method.set_tactic tactic)
+ − 1206
end
+ − 1207
(ML_Context.the_generic_context ())));
+ − 1208
*}
+ − 1209
+ − 1210
+ − 1211
ML {*
+ − 1212
let
+ − 1213
fun tactic (facts: thm list) : tactic = atac
+ − 1214
in
+ − 1215
Context.map_proof (Method.set_tactic tactic)
+ − 1216
end *}
+ − 1217
+ − 1218
end *}
+ − 1219
+ − 1220
ML {* Toplevel.program (fn () =>
+ − 1221
(ML_Context.expression Position.none "val plus : int" "3 + 4" "1" (Context.Proof @{context})))*}
+ − 1222
+ − 1223
+ − 1224
ML {*
+ − 1225
fun ml_tactic (txt, pos) ctxt =
+ − 1226
let
+ − 1227
val ctxt' = ctxt |> Context.proof_map
+ − 1228
(ML_Context.expression pos
+ − 1229
"fun tactic (facts: thm list) : tactic"
+ − 1230
"Context.map_proof (Method.set_tactic tactic)" txt);
+ − 1231
in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt') end;
+ − 1232
+ − 1233
*}
+ − 1234
+ − 1235
ML {*
+ − 1236
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 ())));
+ − 1237
*}
+ − 1238
*)
319
+ − 1239
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
+ − 1240
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
+ − 1241
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1242
text {*
207
+ − 1243
(FIXME: maybe move to after the tactic section)
+ − 1244
221
+ − 1245
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
+ − 1246
in \isacommand{apply}. To print out all currently known methods you can use the
192
+ − 1247
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
+ − 1248
207
+ − 1249
\begin{isabelle}
+ − 1250
\isacommand{print\_methods}\\
+ − 1251
@{text "> methods:"}\\
+ − 1252
@{text "> -: do nothing (insert current facts only)"}\\
+ − 1253
@{text "> HOL.default: apply some intro/elim rule (potentially classical)"}\\
+ − 1254
@{text "> ..."}
+ − 1255
\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
+ − 1256
193
+ − 1257
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
+ − 1258
*}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1259
244
+ − 1260
method_setup %gray foo =
181
+ − 1261
{* Scan.succeed
+ − 1262
(K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *}
244
+ − 1263
"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
+ − 1264
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1265
text {*
286
+ − 1266
It defines the method @{text foo}, which takes no arguments (therefore the
207
+ − 1267
parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which
256
+ − 1268
applies @{thm [source] conjE} and then @{thm [source] conjI}. The function
316
+ − 1269
@{ML_ind SIMPLE_METHOD}
287
+ − 1270
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
+ − 1271
*}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1272
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1273
lemma shows "A \<and> B \<Longrightarrow> C \<and> D"
244
+ − 1274
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
+ − 1275
txt {*
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1276
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
+ − 1277
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1278
\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
+ − 1279
@{subgoals}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1280
\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
+ − 1281
(*<*)oops(*>*)
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1282
193
+ − 1283
319
+ − 1284
+ − 1285
+ − 1286
+ − 1287
193
+ − 1288
(*
+ − 1289
ML {* SIMPLE_METHOD *}
+ − 1290
ML {* METHOD *}
+ − 1291
ML {* K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *}
+ − 1292
ML {* Scan.succeed *}
+ − 1293
*)
+ − 1294
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1295
text {*
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1296
(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
+ − 1297
*}
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1298
75
+ − 1299
(*<*)
194
+ − 1300
(* THIS IS AN OLD VERSION OF THE PARSING CHAPTER BY JEREMY DAWSON *)
38
+ − 1301
chapter {* Parsing *}
+ − 1302
+ − 1303
text {*
+ − 1304
4
+ − 1305
Lots of Standard ML code is given in this document, for various reasons,
+ − 1306
including:
+ − 1307
\begin{itemize}
+ − 1308
\item direct quotation of code found in the Isabelle source files,
+ − 1309
or simplified versions of such code
+ − 1310
\item identifiers found in the Isabelle source code, with their types
+ − 1311
(or specialisations of their types)
+ − 1312
\item code examples, which can be run by the reader, to help illustrate the
+ − 1313
behaviour of functions found in the Isabelle source code
+ − 1314
\item ancillary functions, not from the Isabelle source code,
+ − 1315
which enable the reader to run relevant code examples
+ − 1316
\item type abbreviations, which help explain the uses of certain functions
+ − 1317
\end{itemize}
+ − 1318
+ − 1319
*}
+ − 1320
+ − 1321
section {* Parsing Isar input *}
+ − 1322
+ − 1323
text {*
+ − 1324
+ − 1325
The typical parsing function has the type
+ − 1326
\texttt{'src -> 'res * 'src}, with input
+ − 1327
of type \texttt{'src}, returning a result
+ − 1328
of type \texttt{'res}, which is (or is derived from) the first part of the
+ − 1329
input, and also returning the remainder of the input.
+ − 1330
(In the common case, when it is clear what the ``remainder of the input''
+ − 1331
means, we will just say that the functions ``returns'' the
+ − 1332
value of type \texttt{'res}).
+ − 1333
An exception is raised if an appropriate value
+ − 1334
cannot be produced from the input.
+ − 1335
A range of exceptions can be used to identify different reasons
+ − 1336
for the failure of a parse.
+ − 1337
+ − 1338
This contrasts the standard parsing function in Standard ML,
+ − 1339
which is of type
+ − 1340
\texttt{type ('res, 'src) reader = 'src -> ('res * 'src) option};
+ − 1341
(for example, \texttt{List.getItem} and \texttt{Substring.getc}).
+ − 1342
However, much of the discussion at
+ − 1343
FIX file:/home/jeremy/html/ml/SMLBasis/string-cvt.html
+ − 1344
is relevant.
+ − 1345
+ − 1346
Naturally one may convert between the two different sorts of parsing functions
+ − 1347
as follows:
+ − 1348
\begin{verbatim}
+ − 1349
open StringCvt ;
+ − 1350
type ('res, 'src) ex_reader = 'src -> 'res * 'src
75
+ − 1351
ex_reader : ('res, 'src) reader -> ('res, 'src) ex_reader
4
+ − 1352
fun ex_reader rdr src = Option.valOf (rdr src) ;
75
+ − 1353
reader : ('res, 'src) ex_reader -> ('res, 'src) reader
4
+ − 1354
fun reader exrdr src = SOME (exrdr src) handle _ => NONE ;
+ − 1355
\end{verbatim}
+ − 1356
+ − 1357
*}
+ − 1358
+ − 1359
section{* The \texttt{Scan} structure *}
+ − 1360
+ − 1361
text {*
+ − 1362
The source file is \texttt{src/General/scan.ML}.
+ − 1363
This structure provides functions for using and combining parsing functions
+ − 1364
of the type \texttt{'src -> 'res * 'src}.
+ − 1365
Three exceptions are used:
+ − 1366
\begin{verbatim}
+ − 1367
exception MORE of string option; (*need more input (prompt)*)
+ − 1368
exception FAIL of string option; (*try alternatives (reason of failure)*)
+ − 1369
exception ABORT of string; (*dead end*)
+ − 1370
\end{verbatim}
+ − 1371
Many functions in this structure (generally those with names composed of
+ − 1372
symbols) are declared as infix.
+ − 1373
+ − 1374
Some functions from that structure are
+ − 1375
\begin{verbatim}
+ − 1376
|-- : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->
+ − 1377
'src -> 'res2 * 'src''
+ − 1378
--| : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->
+ − 1379
'src -> 'res1 * 'src''
+ − 1380
-- : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->
+ − 1381
'src -> ('res1 * 'res2) * 'src''
+ − 1382
^^ : ('src -> string * 'src') * ('src' -> string * 'src'') ->
+ − 1383
'src -> string * 'src''
+ − 1384
\end{verbatim}
+ − 1385
These functions parse a result off the input source twice.
+ − 1386
+ − 1387
\texttt{|--} and \texttt{--|}
+ − 1388
return the first result and the second result, respectively.
+ − 1389
+ − 1390
\texttt{--} returns both.
+ − 1391
+ − 1392
\verb|^^| returns the result of concatenating the two results
+ − 1393
(which must be strings).
+ − 1394
+ − 1395
Note how, although the types
+ − 1396
\texttt{'src}, \texttt{'src'} and \texttt{'src''} will normally be the same,
+ − 1397
the types as shown help suggest the behaviour of the functions.
+ − 1398
\begin{verbatim}
+ − 1399
:-- : ('src -> 'res1 * 'src') * ('res1 -> 'src' -> 'res2 * 'src'') ->
+ − 1400
'src -> ('res1 * 'res2) * 'src''
+ − 1401
:|-- : ('src -> 'res1 * 'src') * ('res1 -> 'src' -> 'res2 * 'src'') ->
+ − 1402
'src -> 'res2 * 'src''
+ − 1403
\end{verbatim}
+ − 1404
These are similar to \texttt{|--} and \texttt{--|},
+ − 1405
except that the second parsing function can depend on the result of the first.
+ − 1406
\begin{verbatim}
+ − 1407
>> : ('src -> 'res1 * 'src') * ('res1 -> 'res2) -> 'src -> 'res2 * 'src'
+ − 1408
|| : ('src -> 'res_src) * ('src -> 'res_src) -> 'src -> 'res_src
+ − 1409
\end{verbatim}
+ − 1410
\texttt{p >> f} applies a function \texttt{f} to the result of a parse.
+ − 1411
+ − 1412
\texttt{||} tries a second parsing function if the first one
+ − 1413
fails by raising an exception of the form \texttt{FAIL \_}.
+ − 1414
+ − 1415
\begin{verbatim}
+ − 1416
succeed : 'res -> ('src -> 'res * 'src) ;
+ − 1417
fail : ('src -> 'res_src) ;
+ − 1418
!! : ('src * string option -> string) ->
+ − 1419
('src -> 'res_src) -> ('src -> 'res_src) ;
+ − 1420
\end{verbatim}
+ − 1421
\texttt{succeed r} returns \texttt{r}, with the input unchanged.
+ − 1422
\texttt{fail} always fails, raising exception \texttt{FAIL NONE}.
+ − 1423
\texttt{!! f} only affects the failure mode, turning a failure that
+ − 1424
raises \texttt{FAIL \_} into a failure that raises \texttt{ABORT ...}.
+ − 1425
This is used to prevent recovery from the failure ---
+ − 1426
thus, in \texttt{!! parse1 || parse2}, if \texttt{parse1} fails,
+ − 1427
it won't recover by trying \texttt{parse2}.
+ − 1428
+ − 1429
\begin{verbatim}
+ − 1430
one : ('si -> bool) -> ('si list -> 'si * 'si list) ;
+ − 1431
some : ('si -> 'res option) -> ('si list -> 'res * 'si list) ;
+ − 1432
\end{verbatim}
+ − 1433
These require the input to be a list of items:
+ − 1434
they fail, raising \texttt{MORE NONE} if the list is empty.
+ − 1435
On other failures they raise \texttt{FAIL NONE}
+ − 1436
+ − 1437
\texttt{one p} takes the first
+ − 1438
item from the list if it satisfies \texttt{p}, otherwise fails.
+ − 1439
+ − 1440
\texttt{some f} takes the first
+ − 1441
item from the list and applies \texttt{f} to it, failing if this returns
+ − 1442
\texttt{NONE}.
+ − 1443
+ − 1444
\begin{verbatim}
+ − 1445
many : ('si -> bool) -> 'si list -> 'si list * 'si list ;
+ − 1446
\end{verbatim}
+ − 1447
\texttt{many p} takes items from the input until it encounters one
+ − 1448
which does not satisfy \texttt{p}. If it reaches the end of the input
+ − 1449
it fails, raising \texttt{MORE NONE}.
+ − 1450
+ − 1451
\texttt{many1} (with the same type) fails if the first item
+ − 1452
does not satisfy \texttt{p}.
+ − 1453
+ − 1454
\begin{verbatim}
+ − 1455
option : ('src -> 'res * 'src) -> ('src -> 'res option * 'src)
+ − 1456
optional : ('src -> 'res * 'src) -> 'res -> ('src -> 'res * 'src)
+ − 1457
\end{verbatim}
+ − 1458
\texttt{option}:
+ − 1459
where the parser \texttt{f} succeeds with result \texttt{r}
+ − 1460
or raises \texttt{FAIL \_},
+ − 1461
\texttt{option f} gives the result \texttt{SOME r} or \texttt{NONE}.
+ − 1462
+ − 1463
\texttt{optional}: if parser \texttt{f} fails by raising \texttt{FAIL \_},
+ − 1464
\texttt{optional f default} provides the result \texttt{default}.
+ − 1465
+ − 1466
\begin{verbatim}
+ − 1467
repeat : ('src -> 'res * 'src) -> 'src -> 'res list * 'src
+ − 1468
repeat1 : ('src -> 'res * 'src) -> 'src -> 'res list * 'src
+ − 1469
bulk : ('src -> 'res * 'src) -> 'src -> 'res list * 'src
+ − 1470
\end{verbatim}
+ − 1471
\texttt{repeat f} repeatedly parses an item off the remaining input until
+ − 1472
\texttt{f} fails with \texttt{FAIL \_}
+ − 1473
+ − 1474
\texttt{repeat1} is as for \texttt{repeat}, but requires at least one
+ − 1475
successful parse.
+ − 1476
+ − 1477
\begin{verbatim}
+ − 1478
lift : ('src -> 'res * 'src) -> ('ex * 'src -> 'res * ('ex * 'src))
+ − 1479
\end{verbatim}
+ − 1480
\texttt{lift} changes the source type of a parser by putting in an extra
+ − 1481
component \texttt{'ex}, which is ignored in the parsing.
+ − 1482
+ − 1483
The \texttt{Scan} structure also provides the type \texttt{lexicon},
+ − 1484
HOW DO THEY WORK ?? TO BE COMPLETED
+ − 1485
\begin{verbatim}
+ − 1486
dest_lexicon: lexicon -> string list ;
+ − 1487
make_lexicon: string list list -> lexicon ;
+ − 1488
empty_lexicon: lexicon ;
+ − 1489
extend_lexicon: string list list -> lexicon -> lexicon ;
+ − 1490
merge_lexicons: lexicon -> lexicon -> lexicon ;
+ − 1491
is_literal: lexicon -> string list -> bool ;
+ − 1492
literal: lexicon -> string list -> string list * string list ;
+ − 1493
\end{verbatim}
+ − 1494
Two lexicons, for the commands and keywords, are stored and can be retrieved
+ − 1495
by:
+ − 1496
\begin{verbatim}
+ − 1497
val (command_lexicon, keyword_lexicon) = OuterSyntax.get_lexicons () ;
+ − 1498
val commands = Scan.dest_lexicon command_lexicon ;
+ − 1499
val keywords = Scan.dest_lexicon keyword_lexicon ;
+ − 1500
\end{verbatim}
+ − 1501
*}
+ − 1502
+ − 1503
section{* The \texttt{OuterLex} structure *}
+ − 1504
+ − 1505
text {*
+ − 1506
The source file is @{text "src/Pure/Isar/outer_lex.ML"}.
+ − 1507
In some other source files its name is abbreviated:
+ − 1508
\begin{verbatim}
+ − 1509
structure T = OuterLex;
+ − 1510
\end{verbatim}
+ − 1511
This structure defines the type \texttt{token}.
+ − 1512
(The types
+ − 1513
\texttt{OuterLex.token},
+ − 1514
\texttt{OuterParse.token} and
+ − 1515
\texttt{SpecParse.token} are all the same).
+ − 1516
+ − 1517
Input text is split up into tokens, and the input source type for many parsing
+ − 1518
functions is \texttt{token list}.
+ − 1519
250
ab9e09076462
some polishing; added together with Jasmin more examples to the pretty printing section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1520
The datatype definition (which is not published in the signature) is
4
+ − 1521
\begin{verbatim}
+ − 1522
datatype token = Token of Position.T * (token_kind * string);
+ − 1523
\end{verbatim}
+ − 1524
but here are some runnable examples for viewing tokens:
+ − 1525
+ − 1526
*}
+ − 1527
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1528
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1529
4
+ − 1530
69
+ − 1531
ML{*
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1532
val toks = OuterSyntax.scan Position.none
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1533
"theory,imports;begin x.y.z apply ?v1 ?'a 'a -- || 44 simp (* xx *) { * fff * }" ;
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1534
*}
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1535
69
+ − 1536
ML{*
4
+ − 1537
print_depth 20 ;
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1538
*}
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1539
69
+ − 1540
ML{*
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1541
map OuterLex.text_of toks ;
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1542
*}
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1543
69
+ − 1544
ML{*
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1545
val proper_toks = filter OuterLex.is_proper toks ;
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1546
*}
4
+ − 1547
69
+ − 1548
ML{*
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1549
map OuterLex.kind_of proper_toks
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1550
*}
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1551
69
+ − 1552
ML{*
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1553
map OuterLex.unparse proper_toks ;
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1554
*}
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1555
69
+ − 1556
ML{*
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1557
OuterLex.stopper
4
+ − 1558
*}
+ − 1559
+ − 1560
text {*
+ − 1561
+ − 1562
The function \texttt{is\_proper : token -> bool} identifies tokens which are
+ − 1563
not white space or comments: many parsing functions assume require spaces or
+ − 1564
comments to have been filtered out.
+ − 1565
+ − 1566
There is a special end-of-file token:
+ − 1567
\begin{verbatim}
+ − 1568
val (tok_eof : token, is_eof : token -> bool) = T.stopper ;
+ − 1569
(* end of file token *)
+ − 1570
\end{verbatim}
+ − 1571
+ − 1572
*}
+ − 1573
+ − 1574
section {* The \texttt{OuterParse} structure *}
+ − 1575
+ − 1576
text {*
+ − 1577
The source file is \texttt{src/Pure/Isar/outer\_parse.ML}.
+ − 1578
In some other source files its name is abbreviated:
+ − 1579
\begin{verbatim}
+ − 1580
structure P = OuterParse;
+ − 1581
\end{verbatim}
+ − 1582
Here the parsers use \texttt{token list} as the input source type.
+ − 1583
+ − 1584
Some of the parsers simply select the first token, provided that it is of the
+ − 1585
right kind (as returned by \texttt{T.kind\_of}): these are
+ − 1586
\texttt{ command, keyword, short\_ident, long\_ident, sym\_ident, term\_var,
+ − 1587
type\_ident, type\_var, number, string, alt\_string, verbatim, sync, eof}
+ − 1588
Others select the first token, provided that it is one of several kinds,
+ − 1589
(eg, \texttt{name, xname, text, typ}).
+ − 1590
+ − 1591
\begin{verbatim}
+ − 1592
type 'a tlp = token list -> 'a * token list ; (* token list parser *)
+ − 1593
$$$ : string -> string tlp
+ − 1594
nat : int tlp ;
+ − 1595
maybe : 'a tlp -> 'a option tlp ;
+ − 1596
\end{verbatim}
+ − 1597
+ − 1598
\texttt{\$\$\$ s} returns the first token,
+ − 1599
if it equals \texttt{s} \emph{and} \texttt{s} is a keyword.
+ − 1600
+ − 1601
\texttt{nat} returns the first token, if it is a number, and evaluates it.
+ − 1602
+ − 1603
\texttt{maybe}: if \texttt{p} returns \texttt{r},
+ − 1604
then \texttt{maybe p} returns \texttt{SOME r} ;
+ − 1605
if the first token is an underscore, it returns \texttt{NONE}.
+ − 1606
+ − 1607
A few examples:
+ − 1608
\begin{verbatim}
+ − 1609
P.list : 'a tlp -> 'a list tlp ; (* likewise P.list1 *)
+ − 1610
P.and_list : 'a tlp -> 'a list tlp ; (* likewise P.and_list1 *)
+ − 1611
val toks : token list = OuterSyntax.scan "44 ,_, 66,77" ;
+ − 1612
val proper_toks = List.filter T.is_proper toks ;
+ − 1613
P.list P.nat toks ; (* OK, doesn't recognize white space *)
+ − 1614
P.list P.nat proper_toks ; (* fails, doesn't recognize what follows ',' *)
+ − 1615
P.list (P.maybe P.nat) proper_toks ; (* fails, end of input *)
+ − 1616
P.list (P.maybe P.nat) (proper_toks @ [tok_eof]) ; (* OK *)
+ − 1617
val toks : token list = OuterSyntax.scan "44 and 55 and 66 and 77" ;
+ − 1618
P.and_list P.nat (List.filter T.is_proper toks @ [tok_eof]) ; (* ??? *)
+ − 1619
\end{verbatim}
+ − 1620
+ − 1621
The following code helps run examples:
+ − 1622
\begin{verbatim}
+ − 1623
fun parse_str tlp str =
+ − 1624
let val toks : token list = OuterSyntax.scan str ;
+ − 1625
val proper_toks = List.filter T.is_proper toks @ [tok_eof] ;
+ − 1626
val (res, rem_toks) = tlp proper_toks ;
+ − 1627
val rem_str = String.concat
+ − 1628
(Library.separate " " (List.map T.unparse rem_toks)) ;
+ − 1629
in (res, rem_str) end ;
+ − 1630
\end{verbatim}
+ − 1631
+ − 1632
Some examples from \texttt{src/Pure/Isar/outer\_parse.ML}
+ − 1633
\begin{verbatim}
+ − 1634
val type_args =
+ − 1635
type_ident >> Library.single ||
+ − 1636
$$$ "(" |-- !!! (list1 type_ident --| $$$ ")") ||
+ − 1637
Scan.succeed [];
+ − 1638
\end{verbatim}
+ − 1639
There are three ways parsing a list of type arguments can succeed.
+ − 1640
The first line reads a single type argument, and turns it into a singleton
+ − 1641
list.
+ − 1642
The second line reads "(", and then the remainder, ignoring the "(" ;
+ − 1643
the remainder consists of a list of type identifiers (at least one),
+ − 1644
and then a ")" which is also ignored.
+ − 1645
The \texttt{!!!} ensures that if the parsing proceeds this far and then fails,
+ − 1646
it won't try the third line (see the description of \texttt{Scan.!!}).
+ − 1647
The third line consumes no input and returns the empty list.
+ − 1648
+ − 1649
\begin{verbatim}
+ − 1650
fun triple2 (x, (y, z)) = (x, y, z);
+ − 1651
val arity = xname -- ($$$ "::" |-- !!! (
+ − 1652
Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) []
+ − 1653
-- sort)) >> triple2;
+ − 1654
\end{verbatim}
+ − 1655
The parser \texttt{arity} reads a typename $t$, then ``\texttt{::}'' (which is
+ − 1656
ignored), then optionally a list $ss$ of sorts and then another sort $s$.
+ − 1657
The result $(t, (ss, s))$ is transformed by \texttt{triple2} to $(t, ss, s)$.
+ − 1658
The second line reads the optional list of sorts:
+ − 1659
it reads first ``\texttt{(}'' and last ``\texttt{)}'', which are both ignored,
+ − 1660
and between them a comma-separated list of sorts.
+ − 1661
If this list is absent, the default \texttt{[]} provides the list of sorts.
+ − 1662
+ − 1663
\begin{verbatim}
+ − 1664
parse_str P.type_args "('a, 'b) ntyp" ;
+ − 1665
parse_str P.type_args "'a ntyp" ;
+ − 1666
parse_str P.type_args "ntyp" ;
+ − 1667
parse_str P.arity "ty :: tycl" ;
+ − 1668
parse_str P.arity "ty :: (tycl1, tycl2) tycl" ;
+ − 1669
\end{verbatim}
+ − 1670
+ − 1671
*}
+ − 1672
+ − 1673
section {* The \texttt{SpecParse} structure *}
+ − 1674
+ − 1675
text {*
+ − 1676
The source file is \texttt{src/Pure/Isar/spec\_parse.ML}.
+ − 1677
This structure contains token list parsers for more complicated values.
+ − 1678
For example,
+ − 1679
\begin{verbatim}
+ − 1680
open SpecParse ;
+ − 1681
attrib : Attrib.src tok_rdr ;
+ − 1682
attribs : Attrib.src list tok_rdr ;
+ − 1683
opt_attribs : Attrib.src list tok_rdr ;
+ − 1684
xthm : (thmref * Attrib.src list) tok_rdr ;
+ − 1685
xthms1 : (thmref * Attrib.src list) list tok_rdr ;
+ − 1686
+ − 1687
parse_str attrib "simp" ;
+ − 1688
parse_str opt_attribs "hello" ;
+ − 1689
val (ass, "") = parse_str attribs "[standard, xxxx, simp, intro, OF sym]" ;
+ − 1690
map Args.dest_src ass ;
+ − 1691
val (asrc, "") = parse_str attrib "THEN trans [THEN sym]" ;
+ − 1692
+ − 1693
parse_str xthm "mythm [attr]" ;
+ − 1694
parse_str xthms1 "thm1 [attr] thms2" ;
+ − 1695
\end{verbatim}
+ − 1696
+ − 1697
As you can see, attributes are described using types of the \texttt{Args}
+ − 1698
structure, described below.
+ − 1699
*}
+ − 1700
+ − 1701
section{* The \texttt{Args} structure *}
+ − 1702
+ − 1703
text {*
+ − 1704
The source file is \texttt{src/Pure/Isar/args.ML}.
250
ab9e09076462
some polishing; added together with Jasmin more examples to the pretty printing section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1705
The primary type of this structure is the \texttt{src} datatype;
4
+ − 1706
the single constructors not published in the signature, but
+ − 1707
\texttt{Args.src} and \texttt{Args.dest\_src}
+ − 1708
are in fact the constructor and destructor functions.
+ − 1709
Note that the types \texttt{Attrib.src} and \texttt{Method.src}
+ − 1710
are in fact \texttt{Args.src}.
+ − 1711
+ − 1712
\begin{verbatim}
+ − 1713
src : (string * Args.T list) * Position.T -> Args.src ;
+ − 1714
dest_src : Args.src -> (string * Args.T list) * Position.T ;
+ − 1715
Args.pretty_src : Proof.context -> Args.src -> Pretty.T ;
+ − 1716
fun pr_src ctxt src = Pretty.string_of (Args.pretty_src ctxt src) ;
+ − 1717
+ − 1718
val thy = ML_Context.the_context () ;
+ − 1719
val ctxt = ProofContext.init thy ;
+ − 1720
map (pr_src ctxt) ass ;
+ − 1721
\end{verbatim}
+ − 1722
+ − 1723
So an \texttt{Args.src} consists of the first word, then a list of further
+ − 1724
``arguments'', of type \texttt{Args.T}, with information about position in the
+ − 1725
input.
+ − 1726
\begin{verbatim}
+ − 1727
(* how an Args.src is parsed *)
+ − 1728
P.position : 'a tlp -> ('a * Position.T) tlp ;
+ − 1729
P.arguments : Args.T list tlp ;
+ − 1730
+ − 1731
val parse_src : Args.src tlp =
+ − 1732
P.position (P.xname -- P.arguments) >> Args.src ;
+ − 1733
\end{verbatim}
+ − 1734
+ − 1735
\begin{verbatim}
+ − 1736
val ((first_word, args), pos) = Args.dest_src asrc ;
+ − 1737
map Args.string_of args ;
+ − 1738
\end{verbatim}
+ − 1739
+ − 1740
The \texttt{Args} structure contains more parsers and parser transformers
+ − 1741
for which the input source type is \texttt{Args.T list}. For example,
+ − 1742
\begin{verbatim}
+ − 1743
type 'a atlp = Args.T list -> 'a * Args.T list ;
+ − 1744
open Args ;
+ − 1745
nat : int atlp ; (* also Args.int *)
+ − 1746
thm_sel : PureThy.interval list atlp ;
+ − 1747
list : 'a atlp -> 'a list atlp ;
+ − 1748
attribs : (string -> string) -> Args.src list atlp ;
+ − 1749
opt_attribs : (string -> string) -> Args.src list atlp ;
+ − 1750
+ − 1751
(* parse_atl_str : 'a atlp -> (string -> 'a * string) ;
+ − 1752
given an Args.T list parser, to get a string parser *)
+ − 1753
fun parse_atl_str atlp str =
+ − 1754
let val (ats, rem_str) = parse_str P.arguments str ;
+ − 1755
val (res, rem_ats) = atlp ats ;
+ − 1756
in (res, String.concat (Library.separate " "
+ − 1757
(List.map Args.string_of rem_ats @ [rem_str]))) end ;
+ − 1758
+ − 1759
parse_atl_str Args.int "-1-," ;
+ − 1760
parse_atl_str (Scan.option Args.int) "x1-," ;
+ − 1761
parse_atl_str Args.thm_sel "(1-,4,13-22)" ;
+ − 1762
+ − 1763
val (ats as atsrc :: _, "") = parse_atl_str (Args.attribs I)
+ − 1764
"[THEN trans [THEN sym], simp, OF sym]" ;
+ − 1765
\end{verbatim}
+ − 1766
+ − 1767
From here, an attribute is interpreted using \texttt{Attrib.attribute}.
+ − 1768
+ − 1769
\texttt{Args} has a large number of functions which parse an \texttt{Args.src}
+ − 1770
and also refer to a generic context.
+ − 1771
Note the use of \texttt{Scan.lift} for this.
+ − 1772
(as does \texttt{Attrib} - RETHINK THIS)
+ − 1773
+ − 1774
(\texttt{Args.syntax} shown below has type specialised)
+ − 1775
+ − 1776
\begin{verbatim}
+ − 1777
type ('res, 'src) parse_fn = 'src -> 'res * 'src ;
+ − 1778
type 'a cgatlp = ('a, Context.generic * Args.T list) parse_fn ;
+ − 1779
Scan.lift : 'a atlp -> 'a cgatlp ;
+ − 1780
term : term cgatlp ;
+ − 1781
typ : typ cgatlp ;
+ − 1782
+ − 1783
Args.syntax : string -> 'res cgatlp -> src -> ('res, Context.generic) parse_fn ;
+ − 1784
Attrib.thm : thm cgatlp ;
+ − 1785
Attrib.thms : thm list cgatlp ;
+ − 1786
Attrib.multi_thm : thm list cgatlp ;
+ − 1787
+ − 1788
(* parse_cgatl_str : 'a cgatlp -> (string -> 'a * string) ;
+ − 1789
given a (Context.generic * Args.T list) parser, to get a string parser *)
+ − 1790
fun parse_cgatl_str cgatlp str =
+ − 1791
let
+ − 1792
(* use the current generic context *)
+ − 1793
val generic = Context.Theory thy ;
+ − 1794
val (ats, rem_str) = parse_str P.arguments str ;
+ − 1795
(* ignore any change to the generic context *)
+ − 1796
val (res, (_, rem_ats)) = cgatlp (generic, ats) ;
+ − 1797
in (res, String.concat (Library.separate " "
+ − 1798
(List.map Args.string_of rem_ats @ [rem_str]))) end ;
+ − 1799
\end{verbatim}
+ − 1800
*}
+ − 1801
+ − 1802
section{* Attributes, and the \texttt{Attrib} structure *}
+ − 1803
+ − 1804
text {*
+ − 1805
The type \texttt{attribute} is declared in \texttt{src/Pure/thm.ML}.
+ − 1806
The source file for the \texttt{Attrib} structure is
+ − 1807
\texttt{src/Pure/Isar/attrib.ML}.
+ − 1808
Most attributes use a theorem to change a generic context (for example,
+ − 1809
by declaring that the theorem should be used, by default, in simplification),
+ − 1810
or change a theorem (which most often involves referring to the current
+ − 1811
theory).
+ − 1812
The functions \texttt{Thm.rule\_attribute} and
+ − 1813
\texttt{Thm.declaration\_attribute} create attributes of these kinds.
+ − 1814
+ − 1815
\begin{verbatim}
+ − 1816
type attribute = Context.generic * thm -> Context.generic * thm;
+ − 1817
type 'a trf = 'a -> 'a ; (* transformer of a given type *)
+ − 1818
Thm.rule_attribute : (Context.generic -> thm -> thm) -> attribute ;
+ − 1819
Thm.declaration_attribute : (thm -> Context.generic trf) -> attribute ;
+ − 1820
+ − 1821
Attrib.print_attributes : theory -> unit ;
+ − 1822
Attrib.pretty_attribs : Proof.context -> src list -> Pretty.T list ;
+ − 1823
+ − 1824
List.app Pretty.writeln (Attrib.pretty_attribs ctxt ass) ;
+ − 1825
\end{verbatim}
+ − 1826
+ − 1827
An attribute is stored in a theory as indicated by:
+ − 1828
\begin{verbatim}
+ − 1829
Attrib.add_attributes :
+ − 1830
(bstring * (src -> attribute) * string) list -> theory trf ;
+ − 1831
(*
+ − 1832
Attrib.add_attributes [("THEN", THEN_att, "resolution with rule")] ;
+ − 1833
*)
+ − 1834
\end{verbatim}
+ − 1835
where the first and third arguments are name and description of the attribute,
+ − 1836
and the second is a function which parses the attribute input text
+ − 1837
(including the attribute name, which has necessarily already been parsed).
+ − 1838
Here, \texttt{THEN\_att} is a function declared in the code for the
+ − 1839
structure \texttt{Attrib}, but not published in its signature.
+ − 1840
The source file \texttt{src/Pure/Isar/attrib.ML} shows the use of
+ − 1841
\texttt{Attrib.add\_attributes} to add a number of attributes.
+ − 1842
+ − 1843
\begin{verbatim}
+ − 1844
FullAttrib.THEN_att : src -> attribute ;
+ − 1845
FullAttrib.THEN_att atsrc (generic, ML_Context.thm "sym") ;
+ − 1846
FullAttrib.THEN_att atsrc (generic, ML_Context.thm "all_comm") ;
+ − 1847
\end{verbatim}
+ − 1848
+ − 1849
\begin{verbatim}
+ − 1850
Attrib.syntax : attribute cgatlp -> src -> attribute ;
+ − 1851
Attrib.no_args : attribute -> src -> attribute ;
+ − 1852
\end{verbatim}
+ − 1853
When this is called as \texttt{syntax scan src (gc, th)}
+ − 1854
the generic context \texttt{gc} is used
+ − 1855
(and potentially changed to \texttt{gc'})
+ − 1856
by \texttt{scan} in parsing to obtain an attribute \texttt{attr} which would
+ − 1857
then be applied to \texttt{(gc', th)}.
+ − 1858
The source for parsing the attribute is the arguments part of \texttt{src},
+ − 1859
which must all be consumed by the parse.
+ − 1860
+ − 1861
For example, for \texttt{Attrib.no\_args attr src}, the attribute parser
+ − 1862
simply returns \texttt{attr}, requiring that the arguments part of
+ − 1863
\texttt{src} must be empty.
+ − 1864
+ − 1865
Some examples from \texttt{src/Pure/Isar/attrib.ML}, modified:
+ − 1866
\begin{verbatim}
+ − 1867
fun rot_att_n n (gc, th) = (gc, rotate_prems n th) ;
+ − 1868
rot_att_n : int -> attribute ;
+ − 1869
val rot_arg = Scan.lift (Scan.optional Args.int 1 : int atlp) : int cgatlp ;
+ − 1870
val rotated_att : src -> attribute =
+ − 1871
Attrib.syntax (rot_arg >> rot_att_n : attribute cgatlp) ;
+ − 1872
+ − 1873
val THEN_arg : int cgatlp = Scan.lift
+ − 1874
(Scan.optional (Args.bracks Args.nat : int atlp) 1 : int atlp) ;
+ − 1875
+ − 1876
Attrib.thm : thm cgatlp ;
+ − 1877
+ − 1878
THEN_arg -- Attrib.thm : (int * thm) cgatlp ;
+ − 1879
+ − 1880
fun THEN_att_n (n, tht) (gc, th) = (gc, th RSN (n, tht)) ;
+ − 1881
THEN_att_n : int * thm -> attribute ;
+ − 1882
+ − 1883
val THEN_att : src -> attribute = Attrib.syntax
+ − 1884
(THEN_arg -- Attrib.thm >> THEN_att_n : attribute cgatlp);
+ − 1885
\end{verbatim}
+ − 1886
The functions I've called \texttt{rot\_arg} and \texttt{THEN\_arg}
+ − 1887
read an optional argument, which for \texttt{rotated} is an integer,
+ − 1888
and for \texttt{THEN} is a natural enclosed in square brackets;
+ − 1889
the default, if the argument is absent, is 1 in each case.
+ − 1890
Functions \texttt{rot\_att\_n} and \texttt{THEN\_att\_n} turn these into
+ − 1891
attributes, where \texttt{THEN\_att\_n} also requires a theorem, which is
+ − 1892
parsed by \texttt{Attrib.thm}.
+ − 1893
Infix operators \texttt{--} and \texttt{>>} are in the structure \texttt{Scan}.
+ − 1894
+ − 1895
*}
+ − 1896
+ − 1897
section{* Methods, and the \texttt{Method} structure *}
+ − 1898
+ − 1899
text {*
+ − 1900
The source file is \texttt{src/Pure/Isar/method.ML}.
+ − 1901
The type \texttt{method} is defined by the datatype declaration
+ − 1902
\begin{verbatim}
+ − 1903
(* datatype method = Meth of thm list -> cases_tactic; *)
+ − 1904
RuleCases.NO_CASES : tactic -> cases_tactic ;
+ − 1905
\end{verbatim}
+ − 1906
In fact \texttt{RAW\_METHOD\_CASES} (below) is exactly the constructor
+ − 1907
\texttt{Meth}.
+ − 1908
A \texttt{cases\_tactic} is an elaborated version of a tactic.
+ − 1909
\texttt{NO\_CASES tac} is a \texttt{cases\_tactic} which consists of a
+ − 1910
\texttt{cases\_tactic} without any further case information.
+ − 1911
For further details see the description of structure \texttt{RuleCases} below.
+ − 1912
The list of theorems to be passed to a method consists of the current
+ − 1913
\emph{facts} in the proof.
+ − 1914
+ − 1915
\begin{verbatim}
+ − 1916
RAW_METHOD : (thm list -> tactic) -> method ;
+ − 1917
METHOD : (thm list -> tactic) -> method ;
+ − 1918
+ − 1919
SIMPLE_METHOD : tactic -> method ;
+ − 1920
SIMPLE_METHOD' : (int -> tactic) -> method ;
+ − 1921
SIMPLE_METHOD'' : ((int -> tactic) -> tactic) -> (int -> tactic) -> method ;
+ − 1922
+ − 1923
RAW_METHOD_CASES : (thm list -> cases_tactic) -> method ;
+ − 1924
METHOD_CASES : (thm list -> cases_tactic) -> method ;
+ − 1925
\end{verbatim}
+ − 1926
A method is, in its simplest form, a tactic; applying the method is to apply
+ − 1927
the tactic to the current goal state.
+ − 1928
+ − 1929
Applying \texttt{RAW\_METHOD tacf} creates a tactic by applying
+ − 1930
\texttt{tacf} to the current {facts}, and applying that tactic to the
+ − 1931
goal state.
+ − 1932
+ − 1933
\texttt{METHOD} is similar but also first applies
+ − 1934
\texttt{Goal.conjunction\_tac} to all subgoals.
+ − 1935
+ − 1936
\texttt{SIMPLE\_METHOD tac} inserts the facts into all subgoals and then
+ − 1937
applies \texttt{tacf}.
+ − 1938
+ − 1939
\texttt{SIMPLE\_METHOD' tacf} inserts the facts and then
+ − 1940
applies \texttt{tacf} to subgoal 1.
+ − 1941
+ − 1942
\texttt{SIMPLE\_METHOD'' quant tacf} does this for subgoal(s) selected by
+ − 1943
\texttt{quant}, which may be, for example,
+ − 1944
\texttt{ALLGOALS} (all subgoals),
+ − 1945
\texttt{TRYALL} (try all subgoals, failure is OK),
+ − 1946
\texttt{FIRSTGOAL} (try subgoals until it succeeds once),
+ − 1947
\texttt{(fn tacf => tacf 4)} (subgoal 4), etc
16
+ − 1948
(see the \texttt{Tactical} structure, FIXME) %%\cite[Chapter 4]{ref}).
4
+ − 1949
+ − 1950
A method is stored in a theory as indicated by:
+ − 1951
\begin{verbatim}
+ − 1952
Method.add_method :
+ − 1953
(bstring * (src -> Proof.context -> method) * string) -> theory trf ;
+ − 1954
( *
+ − 1955
* )
+ − 1956
\end{verbatim}
+ − 1957
where the first and third arguments are name and description of the method,
+ − 1958
and the second is a function which parses the method input text
+ − 1959
(including the method name, which has necessarily already been parsed).
+ − 1960
+ − 1961
Here, \texttt{xxx} is a function declared in the code for the
+ − 1962
structure \texttt{Method}, but not published in its signature.
+ − 1963
The source file \texttt{src/Pure/Isar/method.ML} shows the use of
+ − 1964
\texttt{Method.add\_method} to add a number of methods.
240
+ − 1965
*}
4
+ − 1966
75
+ − 1967
(*>*)
220
+ − 1968
end