--- a/ProgTutorial/Parsing.thy Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Parsing.thy Thu May 16 19:56:12 2019 +0200
@@ -38,10 +38,10 @@
\begin{readmore}
The library for writing parser combinators is split up, roughly, into two
parts: The first part consists of a collection of generic parser combinators
- defined in the structure @{ML_struct Scan} in the file @{ML_file
+ defined in the structure @{ML_structure Scan} in the file @{ML_file
"Pure/General/scan.ML"}. The second part of the library consists of
combinators for dealing with specific token types, which are defined in the
- structure @{ML_struct Parse} in the file @{ML_file
+ structure @{ML_structure Parse} in the file @{ML_file
"Pure/Isar/parse.ML"}. In addition specific parsers for packages are
defined in @{ML_file "Pure/Isar/parse_spec.ML"}. Parsers for method arguments
are defined in @{ML_file "Pure/Isar/args.ML"}.
@@ -59,17 +59,17 @@
this context means that it will return a pair consisting of this string and
the rest of the input list. For example:
- @{ML_response [display,gray]
+ @{ML_matchresult [display,gray]
"($$ \"h\") (Symbol.explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
- @{ML_response [display,gray]
+ @{ML_matchresult [display,gray]
"($$ \"w\") (Symbol.explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
The function @{ML "$$"} will either succeed (as in the two examples above)
or raise the exception \<open>FAIL\<close> if no string can be consumed. For
example trying to parse
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"($$ \"x\") (Symbol.explode \"world\")"
"Exception FAIL raised"}
@@ -91,13 +91,13 @@
by the programmer (for example to handle them).
In the examples above we use the function @{ML_ind explode in Symbol} from the
- structure @{ML_struct Symbol}, instead of the more standard library function
+ structure @{ML_structure Symbol}, instead of the more standard library function
@{ML_ind explode in String}, for obtaining an input list for the parser. The reason is
that @{ML explode in Symbol} is aware of character
sequences, for example \<open>\<foo>\<close>, that have a special meaning in
Isabelle. To see the difference consider
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
"let
val input = \"\<foo> bar\"
in
@@ -113,7 +113,7 @@
following parser either consumes an @{text [quotes] "h"} or a @{text
[quotes] "w"}:
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
"let
val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")
val input1 = Symbol.explode \"hello\"
@@ -127,7 +127,7 @@
For example parsing \<open>h\<close>, \<open>e\<close> and \<open>l\<close> (in this
order) you can achieve by:
- @{ML_response [display,gray]
+ @{ML_matchresult [display,gray]
"($$ \"h\" -- $$ \"e\" -- $$ \"l\") (Symbol.explode \"hello\")"
"(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
@@ -136,7 +136,7 @@
If, as in the previous example, you want to parse a particular string,
then you can use the function @{ML_ind this_string in Scan}.
- @{ML_response [display,gray]
+ @{ML_matchresult [display,gray]
"Scan.this_string \"hell\" (Symbol.explode \"hello\")"
"(\"hell\", [\"o\"])"}
@@ -146,7 +146,7 @@
result of \<open>q\<close>. For example:
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
"let
val hw = $$ \"h\" || $$ \"w\"
val input1 = Symbol.explode \"hello\"
@@ -162,7 +162,7 @@
one that @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} ``point'' away.
For example:
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
"let
val just_e = $$ \"h\" |-- $$ \"e\"
val just_h = $$ \"h\" --| $$ \"e\"
@@ -176,7 +176,7 @@
\<open>p\<close>, in case it succeeds; otherwise it returns
the default value \<open>x\<close>. For example:
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
"let
val p = Scan.optional ($$ \"h\") \"x\"
val input1 = Symbol.explode \"hello\"
@@ -189,7 +189,7 @@
The function @{ML_ind option in Scan} works similarly, except no default value can
be given. Instead, the result is wrapped as an \<open>option\<close>-type. For example:
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
"let
val p = Scan.option ($$ \"h\")
val input1 = Symbol.explode \"hello\"
@@ -201,7 +201,7 @@
The function @{ML_ind ahead in Scan} parses some input, but leaves the original
input unchanged. For example:
- @{ML_response [display,gray]
+ @{ML_matchresult [display,gray]
"Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")"
"(\"foo\", [\"f\", \"o\", \"o\"])"}
@@ -230,20 +230,20 @@
on @{text [quotes] "hello"}, the parsing succeeds
- @{ML_response [display,gray]
+ @{ML_matchresult [display,gray]
"(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")"
"(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
but if you invoke it on @{text [quotes] "world"}
- @{ML_response_fake [display,gray] "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
+ @{ML_matchresult_fake [display,gray] "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
"Exception ABORT raised"}
then the parsing aborts and the error message \<open>foo\<close> is printed. In order to
see the error message properly, you need to prefix the parser with the function
@{ML_ind error in Scan}. For example:
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
"Exception Error \"foo\" raised"}
@@ -269,12 +269,12 @@
@{text [quotes] "h"}, @{text [quotes] "e"} and @{text [quotes] "w"}, and
the input @{text [quotes] "holle"}
- @{ML_response_fake [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"holle\")"
+ @{ML_matchresult_fake [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"holle\")"
"Exception ERROR \"h is not followed by e\" raised"}
produces the correct error message. Running it with
- @{ML_response [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"wworld\")"
+ @{ML_matchresult [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"wworld\")"
"((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
yields the expected parsing.
@@ -282,7 +282,7 @@
The function @{ML "Scan.repeat p" for p} will apply a parser \<open>p\<close> as
long as it succeeds. For example:
- @{ML_response [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")"
+ @{ML_matchresult [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")"
"([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
Note that @{ML_ind repeat in Scan} stores the parsed items in a list. The function
@@ -294,7 +294,7 @@
the wrapper @{ML_ind finite in Scan} and the ``stopper-token''
@{ML_ind stopper in Symbol}. With them you can write:
- @{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")"
+ @{ML_matchresult [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")"
"([\"h\", \"h\", \"h\", \"h\"], [])"}
The function @{ML stopper in Symbol} is the ``end-of-input'' indicator for parsing strings;
@@ -304,7 +304,7 @@
The function @{ML_ind repeat in Scan} can be used with @{ML_ind one in Scan} to read any
string as in
- @{ML_response [display,gray]
+ @{ML_matchresult [display,gray]
"let
val p = Scan.repeat (Scan.one Symbol.not_eof)
val input = Symbol.explode \"foo bar foo\"
@@ -319,12 +319,12 @@
The function @{ML_ind unless in Scan} takes two parsers: if the first one can
parse the input, then the whole parser fails; if not, then the second is tried. Therefore
- @{ML_response_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"
+ @{ML_matchresult_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"
"Exception FAIL raised"}
fails, while
- @{ML_response [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"world\")"
+ @{ML_matchresult [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"world\")"
"(\"w\",[\"o\", \"r\", \"l\", \"d\"])"}
succeeds.
@@ -333,7 +333,7 @@
be combined to read any input until a certain marker symbol is reached. In the
example below the marker symbol is a @{text [quotes] "*"}.
- @{ML_response [display,gray]
+ @{ML_matchresult [display,gray]
"let
val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))
val input1 = Symbol.explode \"fooooo\"
@@ -352,7 +352,7 @@
first the parser \<open>p\<close> and upon successful completion applies the
function \<open>f\<close> to the result. For example
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
"let
fun double (x, y) = (x ^ x, y ^ y)
val parser = $$ \"h\" -- $$ \"e\"
@@ -363,7 +363,7 @@
doubles the two parsed input strings; or
- @{ML_response [display,gray]
+ @{ML_matchresult [display,gray]
"let
val p = Scan.repeat (Scan.one Symbol.not_eof)
val input = Symbol.explode \"foo bar foo\"
@@ -379,7 +379,7 @@
the given parser to the second component of the pair and leaves the first component
untouched. For example
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
"Scan.lift ($$ \"h\" -- $$ \"e\") (1, Symbol.explode \"hello\")"
"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
@@ -425,7 +425,7 @@
because of the mutual recursion, this parser will immediately run into a
loop, even if it is called without any input. For example
- @{ML_response_fake_both [display, gray]
+ @{ML_matchresult_fake_both [display, gray]
"parse_tree \"A\""
"*** Exception- TOPLEVEL_ERROR raised"}
@@ -449,7 +449,7 @@
some string is applied for the argument \<open>xs\<close>. This gives us
exactly the parser what we wanted. An example is as follows:
- @{ML_response [display, gray]
+ @{ML_matchresult [display, gray]
"let
val input = Symbol.explode \"(A,((A))),A\"
in
@@ -487,11 +487,11 @@
\begin{readmore}
The parser functions for the theory syntax are contained in the structure
- @{ML_struct Parse} defined in the file @{ML_file "Pure/Isar/parse.ML"}.
+ @{ML_structure Parse} defined in the file @{ML_file "Pure/Isar/parse.ML"}.
The definition for tokens is in the file @{ML_file "Pure/Isar/token.ML"}.
\end{readmore}
- The structure @{ML_struct Token} defines several kinds of tokens (for
+ The structure @{ML_structure Token} defines several kinds of tokens (for
example @{ML_ind Ident in Token} for identifiers, @{ML Keyword in
Token} for keywords and @{ML_ind Command in Token} for commands). Some
token parsers take into account the kind of tokens. The first example shows
@@ -502,7 +502,7 @@
messages. The following code
-@{ML_response_fake [display,gray] \<open>Token.explode
+@{ML_matchresult_fake [display,gray] \<open>Token.explode
(Thy_Header.get_keywords' @{context}) Position.none "hello world"\<close>
\<open>[Token (_,(Ident, "hello"),_),
Token (_,(Space, " "),_),
@@ -524,7 +524,7 @@
text \<open>
then lexing @{text [quotes] "hello world"} will produce
- @{ML_response_fake [display,gray] "Token.explode
+ @{ML_matchresult_fake [display,gray] "Token.explode
(Thy_Header.get_keywords' @{context}) Position.none \"hello world\""
"[Token (_,(Keyword, \"hello\"),_),
Token (_,(Space, \" \"),_),
@@ -535,7 +535,7 @@
functions @{ML filter} and @{ML_ind is_proper in Token} to do this.
For example:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
"let
val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"hello world\"
in
@@ -553,7 +553,7 @@
text \<open>
If you now parse
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
"filtered_input \"inductive | for\""
"[Token (_,(Command, \"inductive\"),_),
Token (_,(Keyword, \"|\"),_),
@@ -568,7 +568,7 @@
The parser @{ML_ind "$$$" in Parse} parses a single keyword. For example:
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
"let
val input1 = filtered_input \"where for\"
val input2 = filtered_input \"| in\"
@@ -580,7 +580,7 @@
Any non-keyword string can be parsed with the function @{ML_ind reserved in Parse}.
For example:
- @{ML_response [display,gray]
+ @{ML_matchresult [display,gray]
"let
val p = Parse.reserved \"bar\"
val input = filtered_input \"bar\"
@@ -591,7 +591,7 @@
Like before, you can sequentially connect parsers with @{ML "--"}. For example:
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
"let
val input = filtered_input \"| in\"
in
@@ -603,7 +603,7 @@
list of items recognised by the parser \<open>p\<close>, where the items being parsed
are separated by the string \<open>s\<close>. For example:
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
"let
val input = filtered_input \"in | in | in foo\"
in
@@ -618,7 +618,7 @@
wrapper @{ML Scan.finite}. This time, however, we have to use the
``stopper-token'' @{ML Token.stopper}. We can write:
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
"let
val input = filtered_input \"in | in | in\"
val p = Parse.enum \"|\" (Parse.$$$ \"in\")
@@ -639,7 +639,7 @@
"Parse.!!!"} is fixed to be @{text [quotes] "Outer syntax error"}
together with a relatively precise description of the failure. For example:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
"let
val input = filtered_input \"in |\"
val parse_bar_then_in = Parse.$$$ \"|\" -- Parse.$$$ \"in\"
@@ -671,7 +671,7 @@
text \<open>
where we pretend the parsed string starts on line 7. An example is
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
"filtered_input' \"foo \\n bar\""
"[Token ((\"foo\", ({line=7, end_line=7}, {line=7})), (Ident, \"foo\"), _),
Token ((\"bar\", ({line=8, end_line=8}, {line=8})), (Ident, \"bar\"), _)]"}
@@ -682,7 +682,7 @@
By using the parser @{ML position in Parse} you can access the token
position and return it as part of the parser result. For example
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
"let
val input = filtered_input' \"where\"
in
@@ -753,7 +753,7 @@
for terms and types: you can just call the predefined parsers. Terms can
be parsed using the function @{ML_ind term in Parse}. For example:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
"let
val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"foo\"
in
@@ -765,11 +765,11 @@
The function @{ML_ind prop in Parse} is similar, except that it gives a different
error message, when parsing fails. As you can see, the parser not just returns
the parsed string, but also some markup information. You can decode the
- information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}.
+ information with the function @{ML_ind parse in YXML} in @{ML_structure YXML}.
The result of the decoding is an XML-tree. You can see better what is going on if
you replace @{ML Position.none} by @{ML "Position.line 42"}, say:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
"let
val input = Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 42) \"foo\"
in
@@ -832,7 +832,7 @@
To see what the parser returns, let us parse the string corresponding to the
definition of @{term even} and @{term odd}:
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
"let
val input = filtered_input
(\"even and odd \" ^
@@ -868,7 +868,7 @@
\<open>\"int \<Rightarrow> bool\"\<close> in order to properly escape the double quotes
in the compound type.}
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
"let
val input = filtered_input
\"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
@@ -899,7 +899,7 @@
parsed by @{ML_ind prop in Parse}. However, they can include an optional
theorem name plus some attributes. For example
-@{ML_response [display,gray] "let
+@{ML_matchresult [display,gray] "let
val input = filtered_input \"foo_lemma[intro,dest!]:\"
val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input
in
@@ -1118,7 +1118,7 @@
The first problem for \isacommand{foobar\_proof} is to parse some
text as ML-source and then interpret it as an Isabelle term using
the ML-runtime. For the parsing part, we can use the function
- @{ML_ind "ML_source" in Parse} in the structure @{ML_struct
+ @{ML_ind "ML_source" in Parse} in the structure @{ML_structure
Parse}. For running the ML-interpreter we need the following
scaffolding code.
\<close>
@@ -1158,7 +1158,7 @@
In Line 12, we implement a parser that first reads in an optional lemma name (terminated
by ``:'') and then some ML-code. The function in Lines 5 to 10 takes the ML-text
and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime}
- in the structure @{ML_struct Code_Runtime}. Once the ML-text has been turned into a term,
+ in the structure @{ML_structure Code_Runtime}. Once the ML-text has been turned into a term,
the function @{ML theorem in Proof} opens a corresponding proof-state. This function takes the
function \<open>after_qed\<close> as argument, whose purpose is to store the theorem
(once it is proven) under the given name \<open>thm_name\<close>.