--- a/CookBook/Parsing.thy Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/Parsing.thy Wed Jan 14 23:44:14 2009 +0000
@@ -42,13 +42,14 @@
return a pair consisting of this string and the rest of the input list.
For example:
- @{ML_response [display] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
- @{ML_response [display] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
+ @{ML_response [display,gray] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
+
+ @{ML_response [display,gray] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
This function will either succeed (as in the two examples above) or raise the exception
@{text "FAIL"} if no string can be consumed. For example trying to parse
- @{ML_response_fake [display] "($$ \"x\") (explode \"world\")"
+ @{ML_response_fake [display,gray] "($$ \"x\") (explode \"world\")"
"Exception FAIL raised"}
will raise the exception @{text "FAIL"}.
@@ -73,7 +74,7 @@
[quotes] "w"}:
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")
val input1 = (explode \"hello\")
@@ -87,7 +88,7 @@
For example parsing @{text "h"}, @{text "e"} and @{text "l"} in this
sequence can be achieved by
- @{ML_response [display] "(($$ \"h\") -- ($$ \"e\") -- ($$ \"l\")) (explode \"hello\")"
+ @{ML_response [display,gray] "(($$ \"h\") -- ($$ \"e\") -- ($$ \"l\")) (explode \"hello\")"
"(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
Note how the result of consumed strings builds up on the left as nested pairs.
@@ -95,7 +96,7 @@
If, as in the previous example, one wants to parse a particular string,
then one should use the function @{ML Scan.this_string}:
- @{ML_response [display] "Scan.this_string \"hell\" (explode \"hello\")"
+ @{ML_response [display,gray] "Scan.this_string \"hell\" (explode \"hello\")"
"(\"hell\", [\"o\"])"}
Parsers that explore alternatives can be constructed using the function @{ML
@@ -104,7 +105,7 @@
result of @{text "q"}. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val hw = ($$ \"h\") || ($$ \"w\")
val input1 = (explode \"hello\")
@@ -118,7 +119,7 @@
for parsers, except that they discard the item being parsed by the first (respectively second)
parser. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val just_e = ($$ \"h\") |-- ($$ \"e\")
val just_h = ($$ \"h\") --| ($$ \"e\")
@@ -132,7 +133,7 @@
@{text "p"}, if it succeeds; otherwise it returns
the default value @{text "x"}. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val p = Scan.optional ($$ \"h\") \"x\"
val input1 = (explode \"hello\")
@@ -145,7 +146,7 @@
The function @{ML Scan.option} works similarly, except no default value can
be given. Instead, the result is wrapped as an @{text "option"}-type. For example:
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val p = Scan.option ($$ \"h\")
val input1 = (explode \"hello\")
@@ -159,7 +160,7 @@
followed by @{text q}, or start a completely different parser @{text r},
one might write
- @{ML [display] "(p -- q) || r" for p q r}
+ @{ML [display,gray] "(p -- q) || r" for p q r}
However, this parser is problematic for producing an appropriate error message, in case
the parsing of @{ML "(p -- q)" for p q} fails. Because in that case one loses the information
@@ -174,24 +175,24 @@
can be avoided when using the function @{ML "(op !!)"}. This function aborts the whole process of
parsing in case of a failure and prints an error message. For example if we invoke the parser
- @{ML [display] "(!! (fn _ => \"foo\") ($$ \"h\"))"}
+ @{ML [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\"))"}
on @{text [quotes] "hello"}, the parsing succeeds
- @{ML_response [display]
+ @{ML_response [display,gray]
"(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"hello\")"
"(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
but if we invoke it on @{text [quotes] "world"}
- @{ML_response_fake [display] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")"
+ @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")"
"Exception ABORT raised"}
then the parsing aborts and the error message @{text "foo"} is printed out. In order to
see the error message properly, we need to prefix the parser with the function
@{ML "Scan.error"}. For example
- @{ML_response_fake [display] "Scan.error ((!! (fn _ => \"foo\") ($$ \"h\")))"
+ @{ML_response_fake [display,gray] "Scan.error ((!! (fn _ => \"foo\") ($$ \"h\")))"
"Exception Error \"foo\" raised"}
This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"}
@@ -214,12 +215,12 @@
Running this parser with the @{text [quotes] "h"} and @{text [quotes] "e"}, and
the input @{text [quotes] "holle"}
- @{ML_response_fake [display] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"holle\")"
+ @{ML_response_fake [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"holle\")"
"Exception ERROR \"h is not followed by e\" raised"}
produces the correct error message. Running it with
- @{ML_response [display] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"wworld\")"
+ @{ML_response [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"wworld\")"
"((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
yields the expected parsing.
@@ -227,7 +228,7 @@
The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as
often as it succeeds. For example
- @{ML_response [display] "Scan.repeat ($$ \"h\") (explode \"hhhhello\")"
+ @{ML_response [display,gray] "Scan.repeat ($$ \"h\") (explode \"hhhhello\")"
"([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
Note that @{ML "Scan.repeat"} stores the parsed items in a list. The function
@@ -239,7 +240,7 @@
the wrapper @{ML Scan.finite} and the ``stopper-token'' @{ML Symbol.stopper}. With
them we can write
- @{ML_response [display] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (explode \"hhhh\")"
+ @{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (explode \"hhhh\")"
"([\"h\", \"h\", \"h\", \"h\"], [])"}
@{ML Symbol.stopper} is the ``end-of-input'' indicator for parsing strings;
@@ -249,7 +250,7 @@
The function @{ML Scan.repeat} can be used with @{ML Scan.one} to read any
string as in
- @{ML_response [display]
+ @{ML_response [display,gray]
"let
val p = Scan.repeat (Scan.one Symbol.not_eof)
val input = (explode \"foo bar foo\")
@@ -264,12 +265,12 @@
The function @{ML "Scan.unless p q" for p q} 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] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"hello\")"
+ @{ML_response_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"hello\")"
"Exception FAIL raised"}
fails, while
- @{ML_response [display] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"world\")"
+ @{ML_response [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"world\")"
"(\"w\",[\"o\", \"r\", \"l\", \"d\"])"}
succeeds.
@@ -278,7 +279,7 @@
input until a certain marker symbol is reached. In the example below the marker
symbol is a @{text [quotes] "*"}.
- @{ML_response [display]
+ @{ML_response [display,gray]
"let
val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))
val input1 = (explode \"fooooo\")
@@ -295,7 +296,7 @@
first the parser @{text p} and upon successful completion applies the
function @{text f} to the result. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
fun double (x,y) = (x^x,y^y)
in
@@ -305,7 +306,7 @@
doubles the two parsed input strings. Or
- @{ML_response [display]
+ @{ML_response [display,gray]
"let
val p = Scan.repeat (Scan.one Symbol.not_eof) >> implode
val input = (explode \"foo bar foo\")
@@ -330,7 +331,7 @@
the given parser to the second component of the pair and leaves the first component
untouched. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"Scan.lift (($$ \"h\") -- ($$ \"e\")) (1,(explode \"hello\"))"
"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
@@ -365,7 +366,7 @@
generating precise error messages. The following
-@{ML_response_fake [display] "OuterSyntax.scan Position.none \"hello world\""
+@{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\""
"[Token (\<dots>,(Ident, \"hello\"),\<dots>),
Token (\<dots>,(Space, \" \"),\<dots>),
Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
@@ -381,7 +382,7 @@
functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example
-@{ML_response_fake [display]
+@{ML_response_fake [display,gray]
"let
val input = OuterSyntax.scan Position.none \"hello world\"
in
@@ -400,7 +401,7 @@
If we parse
-@{ML_response_fake [display]
+@{ML_response_fake [display,gray]
"filtered_input \"inductive | for\""
"[Token (\<dots>,(Command, \"inductive\"),\<dots>),
Token (\<dots>,(Keyword, \"|\"),\<dots>),
@@ -411,7 +412,7 @@
the following (you might have to adjust the @{ML print_depth} in order to
see the complete list):
-@{ML_response_fake [display]
+@{ML_response_fake [display,gray]
"let
val (keywords, commands) = OuterKeyword.get_lexicons ()
in
@@ -421,7 +422,7 @@
Now the parser @{ML "OuterParse.$$$"} parses a single keyword. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val input1 = filtered_input \"where for\"
val input2 = filtered_input \"| in\"
@@ -432,7 +433,7 @@
Like before, we can sequentially connect parsers with @{ML "(op --)"}. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val input = filtered_input \"| in\"
in
@@ -444,7 +445,7 @@
list of items recognised by the parser @{text p}, where the items being parsed
are separated by the string @{text s}. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val input = filtered_input \"in | in | in foo\"
in
@@ -460,7 +461,7 @@
Scan.finite}. This time, however, we have to use the ``stopper-token'' @{ML
OuterLex.stopper}. We can write
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val input = filtered_input \"in | in | in\"
in
@@ -482,7 +483,7 @@
except that the error message is fixed to be @{text [quotes] "Outer syntax error"}
with a relatively precise description of the failure. For example:
-@{ML_response_fake [display]
+@{ML_response_fake [display,gray]
"let
val input = filtered_input \"in |\"
val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\"
@@ -728,7 +729,7 @@
text {*
Now we can type for example
- @{ML_response_fake_both [display] "foobar \"True \<and> False\"" "True \<and> False"}
+ @{ML_response_fake_both [display,gray] "foobar \"True \<and> False\"" "True \<and> False"}
and see the proposition in the tracing buffer.
@@ -774,13 +775,13 @@
If we now type @{text "foobar \"True \<and> True\""}, we obtain the following
proof state:
- @{ML_response_fake_both [display] "foobar \"True \<and> True\""
+ @{ML_response_fake_both [display,gray] "foobar \"True \<and> True\""
"goal (1 subgoal):
1. True \<and> True"}
and we can build the proof
- @{text [display] "foobar \"True \<and> True\"
+ @{text [display,gray] "foobar \"True \<and> True\"
apply(rule conjI)
apply(rule TrueI)+
done"}