diff -r 6103b0eadbf2 -r f7c97e64cc2a ProgTutorial/Parsing.thy --- 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 \FAIL\ 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 \\\, 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 = \"\ 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 \h\, \e\ and \l\ (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 \q\. 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 @@ \p\, in case it succeeds; otherwise it returns the default value \x\. 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 \option\-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 \foo\ 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 \p\ 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 \p\ and upon successful completion applies the function \f\ 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 \xs\. 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] \Token.explode +@{ML_matchresult_fake [display,gray] \Token.explode (Thy_Header.get_keywords' @{context}) Position.none "hello world"\ \[Token (_,(Ident, "hello"),_), Token (_,(Space, " "),_), @@ -524,7 +524,7 @@ text \ 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 \ 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 \p\, where the items being parsed are separated by the string \s\. 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 \ 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 @@ \\"int \ bool\"\ 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 \ 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. \ @@ -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 \after_qed\ as argument, whose purpose is to store the theorem (once it is proven) under the given name \thm_name\.