--- a/ProgTutorial/Parsing.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Parsing.thy Fri May 17 10:38:01 2019 +0200
@@ -60,18 +60,18 @@
the rest of the input list. For example:
@{ML_matchresult [display,gray]
- "($$ \"h\") (Symbol.explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
+ \<open>($$ "h") (Symbol.explode "hello")\<close> \<open>("h", ["e", "l", "l", "o"])\<close>}
@{ML_matchresult [display,gray]
- "($$ \"w\") (Symbol.explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
+ \<open>($$ "w") (Symbol.explode "world")\<close> \<open>("w", ["o", "r", "l", "d"])\<close>}
- The function @{ML "$$"} will either succeed (as in the two examples above)
+ The function @{ML \<open>$$\<close>} 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_matchresult_fake [display,gray]
- "($$ \"x\") (Symbol.explode \"world\")"
- "Exception FAIL raised"}
+ \<open>($$ "x") (Symbol.explode "world")\<close>
+ \<open>Exception FAIL raised\<close>}
will raise the exception \<open>FAIL\<close>. The function @{ML_ind "$$" in Scan} will also
fail if you try to consume more than a single character.
@@ -84,7 +84,7 @@
\item \<open>MORE\<close> indicates that there is not enough input for the parser. For example
in \<open>($$ "h") []\<close>.
\item \<open>ABORT\<close> indicates that a dead end is reached.
- It is used for example in the function @{ML "!!"} (see below).
+ It is used for example in the function @{ML \<open>!!\<close>} (see below).
\end{itemize}
However, note that these exceptions are private to the parser and cannot be accessed
@@ -98,15 +98,15 @@
Isabelle. To see the difference consider
@{ML_matchresult_fake [display,gray]
-"let
- val input = \"\<foo> bar\"
+\<open>let
+ val input = "\<foo> bar"
in
(String.explode input, Symbol.explode input)
-end"
-"([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"],
- [\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
+end\<close>
+\<open>(["\\", "<", "f", "o", "o", ">", " ", "b", "a", "r"],
+ ["\<foo>", " ", "b", "a", "r"])\<close>}
- Slightly more general than the parser @{ML "$$"} is the function
+ Slightly more general than the parser @{ML \<open>$$\<close>} is the function
@{ML_ind one in Scan}, in that it takes a predicate as argument and
then parses exactly
one item from the input list satisfying this predicate. For example the
@@ -114,22 +114,22 @@
[quotes] "w"}:
@{ML_matchresult [display,gray]
-"let
- val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")
- val input1 = Symbol.explode \"hello\"
- val input2 = Symbol.explode \"world\"
+\<open>let
+ val hw = Scan.one (fn x => x = "h" orelse x = "w")
+ val input1 = Symbol.explode "hello"
+ val input2 = Symbol.explode "world"
in
(hw input1, hw input2)
-end"
- "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
+end\<close>
+ \<open>(("h", ["e", "l", "l", "o"]),("w", ["o", "r", "l", "d"]))\<close>}
Two parsers can be connected in sequence by using the function @{ML_ind "--" in Scan}.
For example parsing \<open>h\<close>, \<open>e\<close> and \<open>l\<close> (in this
order) you can achieve by:
@{ML_matchresult [display,gray]
- "($$ \"h\" -- $$ \"e\" -- $$ \"l\") (Symbol.explode \"hello\")"
- "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
+ \<open>($$ "h" -- $$ "e" -- $$ "l") (Symbol.explode "hello")\<close>
+ \<open>((("h", "e"), "l"), ["l", "o"])\<close>}
Note how the result of consumed strings builds up on the left as nested pairs.
@@ -137,24 +137,24 @@
then you can use the function @{ML_ind this_string in Scan}.
@{ML_matchresult [display,gray]
- "Scan.this_string \"hell\" (Symbol.explode \"hello\")"
- "(\"hell\", [\"o\"])"}
+ \<open>Scan.this_string "hell" (Symbol.explode "hello")\<close>
+ \<open>("hell", ["o"])\<close>}
Parsers that explore alternatives can be constructed using the function
- @{ML_ind "||" in Scan}. The parser @{ML "(p || q)" for p q} returns the
+ @{ML_ind "||" in Scan}. The parser @{ML \<open>(p || q)\<close> for p q} returns the
result of \<open>p\<close>, in case it succeeds; otherwise it returns the
result of \<open>q\<close>. For example:
@{ML_matchresult [display,gray]
-"let
- val hw = $$ \"h\" || $$ \"w\"
- val input1 = Symbol.explode \"hello\"
- val input2 = Symbol.explode \"world\"
+\<open>let
+ val hw = $$ "h" || $$ "w"
+ val input1 = Symbol.explode "hello"
+ val input2 = Symbol.explode "world"
in
(hw input1, hw input2)
-end"
- "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
+end\<close>
+ \<open>(("h", ["e", "l", "l", "o"]), ("w", ["o", "r", "l", "d"]))\<close>}
The functions @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} work like the sequencing
function for parsers, except that they discard the item being parsed by the
@@ -163,95 +163,95 @@
For example:
@{ML_matchresult [display,gray]
-"let
- val just_e = $$ \"h\" |-- $$ \"e\"
- val just_h = $$ \"h\" --| $$ \"e\"
- val input = Symbol.explode \"hello\"
+\<open>let
+ val just_e = $$ "h" |-- $$ "e"
+ val just_h = $$ "h" --| $$ "e"
+ val input = Symbol.explode "hello"
in
(just_e input, just_h input)
-end"
- "((\"e\", [\"l\", \"l\", \"o\"]), (\"h\", [\"l\", \"l\", \"o\"]))"}
+end\<close>
+ \<open>(("e", ["l", "l", "o"]), ("h", ["l", "l", "o"]))\<close>}
- The parser @{ML "Scan.optional p x" for p x} returns the result of the parser
+ The parser @{ML \<open>Scan.optional p x\<close> for p x} returns the result of the parser
\<open>p\<close>, in case it succeeds; otherwise it returns
the default value \<open>x\<close>. For example:
@{ML_matchresult [display,gray]
-"let
- val p = Scan.optional ($$ \"h\") \"x\"
- val input1 = Symbol.explode \"hello\"
- val input2 = Symbol.explode \"world\"
+\<open>let
+ val p = Scan.optional ($$ "h") "x"
+ val input1 = Symbol.explode "hello"
+ val input2 = Symbol.explode "world"
in
(p input1, p input2)
-end"
- "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
+end\<close>
+ \<open>(("h", ["e", "l", "l", "o"]), ("x", ["w", "o", "r", "l", "d"]))\<close>}
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_matchresult [display,gray]
-"let
- val p = Scan.option ($$ \"h\")
- val input1 = Symbol.explode \"hello\"
- val input2 = Symbol.explode \"world\"
+\<open>let
+ val p = Scan.option ($$ "h")
+ val input1 = Symbol.explode "hello"
+ val input2 = Symbol.explode "world"
in
(p input1, p input2)
-end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
+end\<close> \<open>((SOME "h", ["e", "l", "l", "o"]), (NONE, ["w", "o", "r", "l", "d"]))\<close>}
The function @{ML_ind ahead in Scan} parses some input, but leaves the original
input unchanged. For example:
@{ML_matchresult [display,gray]
- "Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")"
- "(\"foo\", [\"f\", \"o\", \"o\"])"}
+ \<open>Scan.ahead (Scan.this_string "foo") (Symbol.explode "foo")\<close>
+ \<open>("foo", ["f", "o", "o"])\<close>}
The function @{ML_ind "!!" in Scan} helps with producing appropriate error messages
during parsing. For example if you want to parse \<open>p\<close> immediately
followed by \<open>q\<close>, or start a completely different parser \<open>r\<close>,
you might write:
- @{ML [display,gray] "(p -- q) || r" for p q r}
+ @{ML [display,gray] \<open>(p -- q) || r\<close> for p q r}
However, this parser is problematic for producing a useful error
- message, if the parsing of @{ML "(p -- q)" for p q} fails. Because with the
+ message, if the parsing of @{ML \<open>(p -- q)\<close> for p q} fails. Because with the
parser above you lose the information that \<open>p\<close> should be followed by \<open>q\<close>.
To see this assume that \<open>p\<close> is present in the input, but it is not
- followed by \<open>q\<close>. That means @{ML "(p -- q)" for p q} will fail and
+ followed by \<open>q\<close>. That means @{ML \<open>(p -- q)\<close> for p q} will fail and
hence the alternative parser \<open>r\<close> will be tried. However, in many
circumstances this will be the wrong parser for the input ``\<open>p\<close>-followed-by-something''
and therefore will also fail. The error message is then caused by the failure
of \<open>r\<close>, not by the absence of \<open>q\<close> in the input. Such
- situation can be avoided when using the function @{ML "!!"}. This function
+ situation can be avoided when using the function @{ML \<open>!!\<close>}. This function
aborts the whole process of parsing in case of a failure and prints an error
message. For example if you invoke the parser
- @{ML [display,gray] "!! (fn _ => fn _ =>\"foo\") ($$ \"h\")"}
+ @{ML [display,gray] \<open>!! (fn _ => fn _ =>"foo") ($$ "h")\<close>}
on @{text [quotes] "hello"}, the parsing succeeds
@{ML_matchresult [display,gray]
- "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")"
- "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
+ \<open>(!! (fn _ => fn _ => "foo") ($$ "h")) (Symbol.explode "hello")\<close>
+ \<open>("h", ["e", "l", "l", "o"])\<close>}
but if you invoke it on @{text [quotes] "world"}
- @{ML_matchresult_fake [display,gray] "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
- "Exception ABORT raised"}
+ @{ML_matchresult_fake [display,gray] \<open>(!! (fn _ => fn _ => "foo") ($$ "h")) (Symbol.explode "world")\<close>
+ \<open>Exception ABORT raised\<close>}
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_matchresult_fake [display,gray]
- "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
- "Exception Error \"foo\" raised"}
+ \<open>Scan.error (!! (fn _ => fn _ => "foo") ($$ "h")) (Symbol.explode "world")\<close>
+ \<open>Exception Error "foo" raised\<close>}
This kind of ``prefixing'' to see the correct error message is usually done by wrappers
such as @{ML_ind local_theory in Outer_Syntax}
(see Section~\ref{sec:newcommand} which explains this function in more detail).
- Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
+ Let us now return to our example of parsing @{ML \<open>(p -- q) || r\<close> for p q
r}. If you want to generate the correct error message for failure
of parsing \<open>p\<close>-followed-by-\<open>q\<close>, then you have to write:
\<close>
@@ -269,21 +269,21 @@
@{text [quotes] "h"}, @{text [quotes] "e"} and @{text [quotes] "w"}, and
the input @{text [quotes] "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"}
+ @{ML_matchresult_fake [display,gray] \<open>Scan.error (p_followed_by_q "h" "e" "w") (Symbol.explode "holle")\<close>
+ \<open>Exception ERROR "h is not followed by e" raised\<close>}
produces the correct error message. Running it with
- @{ML_matchresult [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"wworld\")"
- "((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
+ @{ML_matchresult [display,gray] \<open>Scan.error (p_followed_by_q "h" "e" "w") (Symbol.explode "wworld")\<close>
+ \<open>(("w", "w"), ["o", "r", "l", "d"])\<close>}
yields the expected parsing.
- The function @{ML "Scan.repeat p" for p} will apply a parser \<open>p\<close> as
+ The function @{ML \<open>Scan.repeat p\<close> for p} will apply a parser \<open>p\<close> as
long as it succeeds. For example:
- @{ML_matchresult [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")"
- "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
+ @{ML_matchresult [display,gray] \<open>Scan.repeat ($$ "h") (Symbol.explode "hhhhello")\<close>
+ \<open>(["h", "h", "h", "h"], ["e", "l", "l", "o"])\<close>}
Note that @{ML_ind repeat in Scan} stores the parsed items in a list. The function
@{ML_ind repeat1 in Scan} is similar, but requires that the parser \<open>p\<close>
@@ -294,8 +294,8 @@
the wrapper @{ML_ind finite in Scan} and the ``stopper-token''
@{ML_ind stopper in Symbol}. With them you can write:
- @{ML_matchresult [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")"
- "([\"h\", \"h\", \"h\", \"h\"], [])"}
+ @{ML_matchresult [display,gray] \<open>Scan.finite Symbol.stopper (Scan.repeat ($$ "h")) (Symbol.explode "hhhh")\<close>
+ \<open>(["h", "h", "h", "h"], [])\<close>}
The function @{ML stopper in Symbol} is the ``end-of-input'' indicator for parsing strings;
other stoppers need to be used when parsing, for example, tokens. However, this kind of
@@ -305,13 +305,13 @@
string as in
@{ML_matchresult [display,gray]
-"let
+\<open>let
val p = Scan.repeat (Scan.one Symbol.not_eof)
- val input = Symbol.explode \"foo bar foo\"
+ val input = Symbol.explode "foo bar foo"
in
Scan.finite Symbol.stopper p input
-end"
-"([\"f\", \"o\", \"o\", \" \", \"b\", \"a\", \"r\", \" \", \"f\", \"o\", \"o\"], [])"}
+end\<close>
+\<open>(["f", "o", "o", " ", "b", "a", "r", " ", "f", "o", "o"], [])\<close>}
where the function @{ML_ind not_eof in Symbol} ensures that we do not read beyond the
end of the input string (i.e.~stopper symbol).
@@ -319,13 +319,13 @@
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_matchresult_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"
- "Exception FAIL raised"}
+ @{ML_matchresult_fake_both [display,gray] \<open>Scan.unless ($$ "h") ($$ "w") (Symbol.explode "hello")\<close>
+ \<open>Exception FAIL raised\<close>}
fails, while
- @{ML_matchresult [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"world\")"
- "(\"w\",[\"o\", \"r\", \"l\", \"d\"])"}
+ @{ML_matchresult [display,gray] \<open>Scan.unless ($$ "h") ($$ "w") (Symbol.explode "world")\<close>
+ \<open>("w",["o", "r", "l", "d"])\<close>}
succeeds.
@@ -334,43 +334,43 @@
example below the marker symbol is a @{text [quotes] "*"}.
@{ML_matchresult [display,gray]
-"let
- val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))
- val input1 = Symbol.explode \"fooooo\"
- val input2 = Symbol.explode \"foo*ooo\"
+\<open>let
+ val p = Scan.repeat (Scan.unless ($$ "*") (Scan.one Symbol.not_eof))
+ val input1 = Symbol.explode "fooooo"
+ val input2 = Symbol.explode "foo*ooo"
in
(Scan.finite Symbol.stopper p input1,
Scan.finite Symbol.stopper p input2)
-end"
-"(([\"f\", \"o\", \"o\", \"o\", \"o\", \"o\"], []),
- ([\"f\", \"o\", \"o\"], [\"*\", \"o\", \"o\", \"o\"]))"}
+end\<close>
+\<open>((["f", "o", "o", "o", "o", "o"], []),
+ (["f", "o", "o"], ["*", "o", "o", "o"]))\<close>}
After parsing is done, you almost always want to apply a function to the parsed
items. One way to do this is the function @{ML_ind ">>" in Scan} where
- @{ML "(p >> f)" for p f} runs
+ @{ML \<open>(p >> f)\<close> for p f} runs
first the parser \<open>p\<close> and upon successful completion applies the
function \<open>f\<close> to the result. For example
@{ML_matchresult [display,gray]
-"let
+\<open>let
fun double (x, y) = (x ^ x, y ^ y)
- val parser = $$ \"h\" -- $$ \"e\"
+ val parser = $$ "h" -- $$ "e"
in
- (parser >> double) (Symbol.explode \"hello\")
-end"
-"((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}
+ (parser >> double) (Symbol.explode "hello")
+end\<close>
+\<open>(("hh", "ee"), ["l", "l", "o"])\<close>}
doubles the two parsed input strings; or
@{ML_matchresult [display,gray]
-"let
+\<open>let
val p = Scan.repeat (Scan.one Symbol.not_eof)
- val input = Symbol.explode \"foo bar foo\"
+ val input = Symbol.explode "foo bar foo"
in
Scan.finite Symbol.stopper (p >> implode) input
-end"
-"(\"foo bar foo\",[])"}
+end\<close>
+\<open>("foo bar foo",[])\<close>}
where the single-character strings in the parsed output are transformed
back into one string.
@@ -380,8 +380,8 @@
untouched. For example
@{ML_matchresult [display,gray]
-"Scan.lift ($$ \"h\" -- $$ \"e\") (1, Symbol.explode \"hello\")"
-"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
+\<open>Scan.lift ($$ "h" -- $$ "e") (1, Symbol.explode "hello")\<close>
+\<open>(("h", "e"), (1, ["l", "l", "o"]))\<close>}
\footnote{\bf FIXME: In which situations is \<open>lift\<close> useful? Give examples.}
@@ -426,8 +426,8 @@
loop, even if it is called without any input. For example
@{ML_matchresult_fake_both [display, gray]
- "parse_tree \"A\""
- "*** Exception- TOPLEVEL_ERROR raised"}
+ \<open>parse_tree "A"\<close>
+ \<open>*** Exception- TOPLEVEL_ERROR raised\<close>}
raises an exception indicating that the stack limit is reached. Such
looping parser are not useful, because of ML's strict evaluation of
@@ -450,20 +450,19 @@
exactly the parser what we wanted. An example is as follows:
@{ML_matchresult [display, gray]
- "let
- val input = Symbol.explode \"(A,((A))),A\"
+ \<open>let
+ val input = Symbol.explode "(A,((A))),A"
in
- Scan.finite Symbol.stopper (parse_tree \"A\") input
-end"
- "(Br (Br (Lf \"A\", Lf \"A\"), Lf \"A\"), [])"}
+ Scan.finite Symbol.stopper (parse_tree "A") input
+end\<close>
+ \<open>(Br (Br (Lf "A", Lf "A"), Lf "A"), [])\<close>}
\begin{exercise}\label{ex:scancmts}
Write a parser that parses an input string so that any comment enclosed
within \<open>(*\<dots>*)\<close> is replaced by the same comment but enclosed within
\<open>(**\<dots>**)\<close> in the output string. To enclose a string, you can use the
- function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML
- "s1 ^ s ^ s2" for s1 s2 s}. Hint: To simplify the task ignore the proper
+ function @{ML \<open>enclose s1 s2 s\<close> for s1 s2 s} which produces the string @{ML \<open>s1 ^ s ^ s2\<close> for s1 s2 s}. Hint: To simplify the task ignore the proper
nesting of comments.
\end{exercise}
\<close>
@@ -497,7 +496,7 @@
token parsers take into account the kind of tokens. The first example shows
how to generate a token list out of a string using the function
@{ML_ind explode in Token}. It is given the argument
- @{ML "Position.none"} since,
+ @{ML \<open>Position.none\<close>} since,
at the moment, we are not interested in generating precise error
messages. The following code
@@ -524,11 +523,11 @@
text \<open>
then lexing @{text [quotes] "hello world"} will produce
- @{ML_matchresult_fake [display,gray] "Token.explode
- (Thy_Header.get_keywords' @{context}) Position.none \"hello world\""
-"[Token (_,(Keyword, \"hello\"),_),
- Token (_,(Space, \" \"),_),
- Token (_,(Ident, \"world\"),_)]"}
+ @{ML_matchresult_fake [display,gray] \<open>Token.explode
+ (Thy_Header.get_keywords' @{context}) Position.none "hello world"\<close>
+\<open>[Token (_,(Keyword, "hello"),_),
+ Token (_,(Space, " "),_),
+ Token (_,(Ident, "world"),_)]\<close>}
Many parsing functions later on will require white space, comments and the like
to have already been filtered out. So from now on we are going to use the
@@ -536,12 +535,12 @@
For example:
@{ML_matchresult_fake [display,gray]
-"let
- val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"hello world\"
+\<open>let
+ val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none "hello world"
in
filter Token.is_proper input
-end"
-"[Token (_,(Ident, \"hello\"), _), Token (_,(Ident, \"world\"), _)]"}
+end\<close>
+\<open>[Token (_,(Ident, "hello"), _), Token (_,(Ident, "world"), _)]\<close>}
For convenience we define the function:
\<close>
@@ -554,10 +553,10 @@
If you now parse
@{ML_matchresult_fake [display,gray]
-"filtered_input \"inductive | for\""
-"[Token (_,(Command, \"inductive\"),_),
- Token (_,(Keyword, \"|\"),_),
- Token (_,(Keyword, \"for\"),_)]"}
+\<open>filtered_input "inductive | for"\<close>
+\<open>[Token (_,(Command, "inductive"),_),
+ Token (_,(Keyword, "|"),_),
+ Token (_,(Keyword, "for"),_)]\<close>}
you obtain a list consisting of only one command and two keyword tokens.
If you want to see which keywords and commands are currently known to Isabelle,
@@ -569,47 +568,47 @@
The parser @{ML_ind "$$$" in Parse} parses a single keyword. For example:
@{ML_matchresult [display,gray]
-"let
- val input1 = filtered_input \"where for\"
- val input2 = filtered_input \"| in\"
+\<open>let
+ val input1 = filtered_input "where for"
+ val input2 = filtered_input "| in"
in
- (Parse.$$$ \"where\" input1, Parse.$$$ \"|\" input2)
-end"
-"((\"where\",_), (\"|\",_))"}
+ (Parse.$$$ "where" input1, Parse.$$$ "|" input2)
+end\<close>
+\<open>(("where",_), ("|",_))\<close>}
Any non-keyword string can be parsed with the function @{ML_ind reserved in Parse}.
For example:
@{ML_matchresult [display,gray]
-"let
- val p = Parse.reserved \"bar\"
- val input = filtered_input \"bar\"
+\<open>let
+ val p = Parse.reserved "bar"
+ val input = filtered_input "bar"
in
p input
-end"
- "(\"bar\",[])"}
+end\<close>
+ \<open>("bar",[])\<close>}
- Like before, you can sequentially connect parsers with @{ML "--"}. For example:
+ Like before, you can sequentially connect parsers with @{ML \<open>--\<close>}. For example:
@{ML_matchresult [display,gray]
-"let
- val input = filtered_input \"| in\"
+\<open>let
+ val input = filtered_input "| in"
in
- (Parse.$$$ \"|\" -- Parse.$$$ \"in\") input
-end"
-"((\"|\", \"in\"), [])"}
+ (Parse.$$$ "|" -- Parse.$$$ "in") input
+end\<close>
+\<open>(("|", "in"), [])\<close>}
- The parser @{ML "Parse.enum s p" for s p} parses a possibly empty
+ The parser @{ML \<open>Parse.enum s p\<close> for s p} parses a possibly empty
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_matchresult [display,gray]
-"let
- val input = filtered_input \"in | in | in foo\"
+\<open>let
+ val input = filtered_input "in | in | in foo"
in
- (Parse.enum \"|\" (Parse.$$$ \"in\")) input
-end"
-"([\"in\", \"in\", \"in\"], [_])"}
+ (Parse.enum "|" (Parse.$$$ "in")) input
+end\<close>
+\<open>(["in", "in", "in"], [_])\<close>}
The function @{ML_ind enum1 in Parse} works similarly, except that the
parsed list must be non-empty. Note that we had to add a string @{text
@@ -619,13 +618,13 @@
``stopper-token'' @{ML Token.stopper}. We can write:
@{ML_matchresult [display,gray]
-"let
- val input = filtered_input \"in | in | in\"
- val p = Parse.enum \"|\" (Parse.$$$ \"in\")
+\<open>let
+ val input = filtered_input "in | in | in"
+ val p = Parse.enum "|" (Parse.$$$ "in")
in
Scan.finite Token.stopper p input
-end"
-"([\"in\", \"in\", \"in\"], [])"}
+end\<close>
+\<open>(["in", "in", "in"], [])\<close>}
The following function will help to run examples.
\<close>
@@ -634,20 +633,19 @@
text \<open>
The function @{ML_ind "!!!" in Parse} can be used to force termination
- of the parser in case of a dead end, just like @{ML "Scan.!!"} (see previous
- section). A difference, however, is that the error message of @{ML
- "Parse.!!!"} is fixed to be @{text [quotes] "Outer syntax error"}
+ of the parser in case of a dead end, just like @{ML \<open>Scan.!!\<close>} (see previous
+ section). A difference, however, is that the error message of @{ML \<open>Parse.!!!\<close>} is fixed to be @{text [quotes] "Outer syntax error"}
together with a relatively precise description of the failure. For example:
@{ML_matchresult_fake [display,gray]
-"let
- val input = filtered_input \"in |\"
- val parse_bar_then_in = Parse.$$$ \"|\" -- Parse.$$$ \"in\"
+\<open>let
+ val input = filtered_input "in |"
+ val parse_bar_then_in = Parse.$$$ "|" -- Parse.$$$ "in"
in
parse (Parse.!!! parse_bar_then_in) input
-end"
-"Exception ERROR \"Outer syntax error: keyword \"|\" expected,
-but keyword in was found\" raised"
+end\<close>
+\<open>Exception ERROR "Outer syntax error: keyword "|" expected,
+but keyword in was found" raised\<close>
}
\begin{exercise} (FIXME)
@@ -672,9 +670,9 @@
where we pretend the parsed string starts on line 7. An example is
@{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\"), _)]"}
+\<open>filtered_input' "foo \\n bar"\<close>
+\<open>[Token (("foo", ({line=7, end_line=7}, {line=7})), (Ident, "foo"), _),
+ Token (("bar", ({line=8, end_line=8}, {line=8})), (Ident, "bar"), _)]\<close>}
in which the @{text [quotes] "\\n"} causes the second token to be in
line 8.
@@ -683,12 +681,12 @@
position and return it as part of the parser result. For example
@{ML_matchresult_fake [display,gray]
-"let
- val input = filtered_input' \"where\"
+\<open>let
+ val input = filtered_input' "where"
in
- parse (Parse.position (Parse.$$$ \"where\")) input
-end"
-"((\"where\", {line=7, end_line=7}), [])"}
+ parse (Parse.position (Parse.$$$ "where")) input
+end\<close>
+\<open>(("where", {line=7, end_line=7}), [])\<close>}
\begin{readmore}
The functions related to positions are implemented in the file
@@ -754,12 +752,12 @@
be parsed using the function @{ML_ind term in Parse}. For example:
@{ML_matchresult_fake [display,gray]
-"let
- val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"foo\"
+\<open>let
+ val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none "foo"
in
Parse.term input
-end"
-"(\"<markup>\", [])"}
+end\<close>
+\<open>("<markup>", [])\<close>}
The function @{ML_ind prop in Parse} is similar, except that it gives a different
@@ -767,15 +765,15 @@
the parsed string, but also some markup information. You can decode the
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:
+ you replace @{ML Position.none} by @{ML \<open>Position.line 42\<close>}, say:
@{ML_matchresult_fake [display,gray]
-"let
- val input = Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 42) \"foo\"
+\<open>let
+ val input = Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 42) "foo"
in
YXML.parse (fst (Parse.term input))
-end"
-"Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
+end\<close>
+\<open>Elem ("token", [("line", "42"), ("end_line", "42")], [XML.Text "foo"])\<close>}
The positional information is stored as part of an XML-tree so that code
called later on will be able to give more precise error messages.
@@ -833,20 +831,20 @@
definition of @{term even} and @{term odd}:
@{ML_matchresult [display,gray]
-"let
+\<open>let
val input = filtered_input
- (\"even and odd \" ^
- \"where \" ^
- \" even0[intro]: \\\"even 0\\\" \" ^
- \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^
- \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
+ ("even and odd " ^
+ "where " ^
+ " even0[intro]: \"even 0\" " ^
+ "| evenS[intro]: \"odd n \<Longrightarrow> even (Suc n)\" " ^
+ "| oddS[intro]: \"even n \<Longrightarrow> odd (Suc n)\"")
in
parse spec_parser input
-end"
-"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
+end\<close>
+\<open>(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
[((even0,_),_),
((evenS,_),_),
- ((oddS,_),_)]), [])"}
+ ((oddS,_),_)]), [])\<close>}
\<close>
ML \<open>let
@@ -865,19 +863,19 @@
\isacommand{and}-separated
list of variables that can include optional type annotations and syntax translations.
For example:\footnote{Note that in the code we need to write
- \<open>\"int \<Rightarrow> bool\"\<close> in order to properly escape the double quotes
+ \<open>"int \<Rightarrow> bool"\<close> in order to properly escape the double quotes
in the compound type.}
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val input = filtered_input
- \"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
+ "foo::\"int \<Rightarrow> bool\" and bar::nat (\"BAR\" 100) and blonk"
in
parse Parse.vars input
-end"
-"([(foo, SOME _, NoSyn),
- (bar, SOME _, Mixfix (Source {text=\"BAR\",...}, [], 100, _)),
- (blonk, NONE, NoSyn)],[])"}
+end\<close>
+\<open>([(foo, SOME _, NoSyn),
+ (bar, SOME _, Mixfix (Source {text="BAR",...}, [], 100, _)),
+ (blonk, NONE, NoSyn)],[])\<close>}
\<close>
text \<open>
@@ -899,12 +897,12 @@
parsed by @{ML_ind prop in Parse}. However, they can include an optional
theorem name plus some attributes. For example
-@{ML_matchresult [display,gray] "let
- val input = filtered_input \"foo_lemma[intro,dest!]:\"
- val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input
+@{ML_matchresult [display,gray] \<open>let
+ val input = filtered_input "foo_lemma[intro,dest!]:"
+ val ((name, attrib), _) = parse (Parse_Spec.thm_name ":") input
in
(name, map Token.name_of_src attrib)
-end" "(foo_lemma, [(\"intro\", _), (\"dest\", _)])"}
+end\<close> \<open>(foo_lemma, [("intro", _), ("dest", _)])\<close>}
The function @{ML_ind opt_thm_name in Parse_Spec} is the ``optional'' variant of
@{ML_ind thm_name in Parse_Spec}. Theorem names can contain attributes. The name
@@ -1019,7 +1017,7 @@
behaviour of the command. In the code above we used a
``do-nothing''-function, which because of the parser @{ML_ind succeed in Scan}
does not parse any argument, but immediately returns the simple
- function @{ML "Local_Theory.background_theory I"}. We can replace
+ function @{ML \<open>Local_Theory.background_theory I\<close>}. We can replace
this code by a function that first parses a proposition (using the
parser @{ML Parse.prop}), then prints out some tracing information
(using the function \<open>trace_prop\<close>) and finally does
@@ -1051,8 +1049,7 @@
``open up'' a proof in order to prove the proposition (for example
\isacommand{lemma}) or prove some other properties (for example
\isacommand{function}). To achieve this kind of behaviour, you have to use
- the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML
- "local_theory_to_proof" in Outer_Syntax} to set up the command.
+ the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML \<open>local_theory_to_proof\<close> in Outer_Syntax} to set up the command.
Below we show the command \isacommand{foobar\_goal} which takes a
proposition as argument and then starts a proof in order to prove
it. Therefore, we need to announce this command in the header
@@ -1084,7 +1081,7 @@
@{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the
proposition. Its argument @{ML NONE} stands for a locale (which we chose to
- omit); the argument @{ML "(K I)"} stands for a function that determines what
+ omit); the argument @{ML \<open>(K I)\<close>} stands for a function that determines what
should be done with the theorem once it is proved (we chose to just forget
about it).