# HG changeset patch # User Christian Urban # Date 1224483731 0 # Node ID b11653b11bd39c387cbb68715b4337dbeaeaab5b # Parent 35e1dff0d9bbb4ba8c8dc0a2fd819bc9616608df further progress on the parsing section and tuning on the antiqu's diff -r 35e1dff0d9bb -r b11653b11bd3 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Fri Oct 17 17:41:34 2008 -0400 +++ b/CookBook/FirstSteps.thy Mon Oct 20 06:22:11 2008 +0000 @@ -133,7 +133,7 @@ For example, one can print out the name of the current theory by typing - @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps : string"} + @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps"} where @{text "@{theory}"} is an antiquotation that is substituted with the current theory (remember that we assumed we are inside the theory CookBook). @@ -338,7 +338,6 @@ *} - section {* Type Checking *} text {* @@ -357,13 +356,11 @@ the @{ML "@{theory}"} antiquotation to get hold of the current theory. For example we can write: - (FIXME ML-response-unchecked needed) - - @{ML [display] "@{term \"(a::nat) + b = c\"}"} + @{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"} and -@{ML [display] +@{ML_response_fake [display] "let val natT = @{typ \"nat\"} val zero = @{term \"0::nat\"} @@ -371,7 +368,7 @@ cterm_of @{theory} (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero) -end"} +end" "0 + 0"} \begin{exercise} Check that the function defined in Exercise~\ref{fun:revsum} returns a @@ -559,60 +556,6 @@ section {* Theorem Attributes *} -ML {* - val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src; - -fun ml_val ys txt = "fn " ^ - (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ - " => (" ^ txt ^ ");"; - -fun ml_val_open (ys, []) txt = ml_val ys txt - | ml_val_open (ys, xs) txt = - ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end"); - -fun ml_pat (rhs, pat) = - let val pat' = implode (map (fn "\" => "_" | s => s) - (Symbol.explode pat)) - in - "val " ^ pat' ^ " = " ^ rhs - end; - -(* modified from original *) -fun ml_val txt = "fn _ => (" ^ txt ^ ");"; -fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"; -fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;"; - -*} - -ML {* ml_pat *} -ML {* K ml_pat *} - -ML {* -fun output_verbatim ml src ctxt (txt, pos) = - let val txt = ml ctxt (txt, pos) - in - (if ! ThyOutput.source then str_of_source src else txt) - |> (if ! ThyOutput.quotes then quote else I) - |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt - end; -*} - -ML {* -fun output_ml ml = output_verbatim - (fn ctxt => fn ((txt, p), pos) => - (ML_Context.eval_in (SOME ctxt) false pos (ml p txt); - txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |> - Chunks.transform_cmts |> implode)); -*} - -ML {* -fun output_ml_checked ml src ctxt (txt, pos) = - (ML_Context.eval_in (SOME ctxt) false pos (ml txt); - (if ! ThyOutput.source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos))) - |> (if ! ThyOutput.quotes then quote else I) - |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt) - -*} diff -r 35e1dff0d9bb -r b11653b11bd3 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Fri Oct 17 17:41:34 2008 -0400 +++ b/CookBook/Parsing.thy Mon Oct 20 06:22:11 2008 +0000 @@ -30,7 +30,6 @@ section {* Building Up Generic Parsers *} - text {* Let us first have a look at parsing strings using generic parsing combinators. @@ -43,22 +42,25 @@ @{ML_response [display] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"} This function will either succeed (as in the two examples above) or raise the exeption - @{ML_text "FAIL"} if no string can be consumed. For example in the next example - try to parse: + @{ML_text "FAIL"} if no string can be consumed. For example trying to parse - @{ML_text [display] "($$ \"x\") (explode \"world\")"} - + @{ML_response_fake [display] "($$ \"x\") (explode \"world\")" + "Exception FAIL raised"} + + will raise the exception @{ML_text "FAIL"}. There are three exceptions used in the parsing combinators: - (FIXME: describe exceptions) - \begin{itemize} - \item @{ML_text "FAIL"} - \item @{ML_text "MORE"} @{ML_text "($$ \"h\") []"} - \item @{ML_text "ABORT"} dead end + \item @{ML_text "FAIL"} is used to indicate that alternative routes of parsing + might be explored. + \item @{ML_text "MORE"} indicates that there is not enough input for the parser. For example + in @{ML_text "($$ \"h\") []"}. + \item @{ML_text "ABORT"} is the exception which is raised when a dead end is reached. + It is used for example in the function @{ML "(op !!)"} (see below). \end{itemize} - Slightly more general than @{ML "(op $$)"} is the function @{ML Scan.one} in that it + + Slightly more general than the parser @{ML "(op $$)"} is the function @{ML Scan.one}, in that it takes a predicate as argument and then parses exactly one item from the input list satisfying this prediate. For example the following parser either consumes an @{ML_text "h"} or a @{ML_text "w"}: @@ -74,7 +76,8 @@ "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"} Two parser can be connected in sequence by using the funtion @{ML "(op --)"}. - For example + For example parsing @{ML_text "h"}, @{ML_text "e"} and @{ML_text "l"} in this + sequence can be achieved by @{ML_response [display] "(($$ \"h\") -- ($$ \"e\") -- ($$ \"l\")) (explode \"hello\")" "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"} @@ -83,7 +86,7 @@ Parsers that explore alternatives can be constructed using the function @{ML "(op ||)"}. For example, the - parser @{ML_open "p || q" for p q} returns the result of @{ML_text "p"}, if it succeeds, + parser @{ML_open "(p || q)" for p q} returns the result of @{ML_text "p"}, if it succeeds, otherwise it returns the result of @{ML_text "q"}. For example @{ML_response [display] @@ -131,15 +134,15 @@ @{ML_open [display] "(p -- q) || r" for p q r} - However, this way is problematic for producing an appropriate error message, in case + However, this parser is problematic for producing an appropriate error message, in case the parsing of @{ML_open "(p -- q)" for p q} fails. Because one loses the information that @{ML_text p} should be followed by @{ML_text q}. To see this consider the case that @{ML_text p} is present in the input, but not @{ML_text q}. So @{ML_open "(p -- q)" for p q} will fail and the - alternative parser @{ML_text r} will be tried. In many circumstances this will be the wrong - parser for the input and therefore probably fail. However, the error message is then caused by the + alternative parser @{ML_text r} will be tried. However in many circumstanes this will be the wrong + parser for the input and therefore will fail. The error message is then caused by the failure of @{ML_text r}, not by the absense of @{ML_text p} in the input. These situations - can be avoided using the funtion @{ML "(op !!)"}, which aborts the whole process of - parsing and invokes an error message. For example if we invoke the parser + can be avoided using the funtion @{ML "(op !!)"}. This function aborts the whole process of + parsing in case of failure and invokes an error message. For example if we invoke the parser @{ML [display] "(!! (fn _ => \"foo\") ($$ \"h\"))"} @@ -149,20 +152,22 @@ "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"} - In contrast if we invoke it on @{ML_text "world"} + but if we invoke it on @{ML_text "world"} - @{ML [display] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")"} + @{ML_response_fake [display] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")" + "Exception ABORT raised"} the parsing aborts and the error message @{ML_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 [display] "Scan.error ((!! (fn _ => \"foo\") ($$ \"h\")))"} + @{ML_response_fake [display] "Scan.error ((!! (fn _ => \"foo\") ($$ \"h\")))" + "Exception Error \"foo\" raised"} This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"} - (FIXME: see below). + (FIXME: give reference to late). - Lets return to our example of parsing @{ML_open "(p -- q) || r" for p q r}. If we want + Returning to our example of parsing @{ML_open "(p -- q) || r" for p q r}. If we want to generate the correct error message for @{ML_text q} not following @{ML_text p}, then we have to write *} @@ -170,39 +175,42 @@ ML {* fun p_followed_by_q p q r = let - val err = (fn _ => p ^ " is not followed by " ^ q) + val err = (fn _ => p ^ " is not followed by " ^ q) in - (($$ p) -- (!! err ($$ q))) || (($$ r) -- ($$ r)) + (($$ p) -- (!! err ($$ q))) || (($$ r) -- ($$ r)) end *} + text {* Running this parser with - @{ML_text [display] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"holle\")"} + @{ML_response_fake [display] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"holle\")" + "Exception ERROR \"h is not followed by e\" raised"} - gives the correct error message and running it with + gives the correct error message. Running it with @{ML_response [display] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"wworld\")" "((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"} yields the expected parsing. - The function @{ML "Scan.repeat"} will apply a parser as often as it succeeds. For examle + The function @{ML_open "Scan.repeat p" for p} will apply a parser @{ML_text p} as + often as it succeeds. For example - @{ML_response "Scan.repeat ($$ \"h\") (explode \"hhhhello\")" + @{ML_response [display] "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 - @{ML "Scan.repeat1"} is similar, but requires that in @{ML_open "Scan.repeat1 p" for p} - the parse @{ML_text "p"} succeeds at least once. + @{ML "Scan.repeat1"} is similar, but requires that the parser @{ML_text "p"} + succeeds at least once. *} text {* - After parsing succeeded, one wants to apply functions on the parsed items. This is - done using the function @{ML_open "(p >> f)" for p f} which applies first the - parser @{ML_text p} upon successful completion applies the function @{ML_text f}. - For example + After parsing succeeded, one nearly always wants to apply a function on the parsed + items. This is done using the function @{ML_open "(p >> f)" for p f} which runs + first the parser @{ML_text p} and upon successful completion applies the + function @{ML_text f} to the result. For example @{ML_response [display] "let @@ -212,6 +220,8 @@ end" "((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"} + doubles the two parsed input strings. + The function @{ML Scan.lift} takes a parser and a pair as arguments. This function applies the given parser to the second component of the pair and leaves the first component untouched. For example @@ -223,17 +233,38 @@ (FIXME: In which situations is this useful?) *} -section {* Parsing Tokens *} +section {* Parsing Theory Syntax *} text {* - Most of the time, however, we will have to deal with tokens that are not just strings. - The parsers for the theory syntax, as well as the parsers for the argument syntax - of proof methods and attributes use the token type @{ML_type OuterParse.token}, - which is identical to @{ML_type OuterLex.token}. + Most of the time, however, Isabelle developers have to deal with parsing tokens, not strings. + This is because the parsers for the theory syntax, as well as the parsers for the + argument syntax of proof methods and attributes, use the type + @{ML_type OuterParse.token} (which is identical to the type @{ML_type OuterLex.token}). The parser functions for the theory syntax are contained in the structure - @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}. + @{ML_struct OuterParse} defined in the file\linebreak @{ML_file "Pure/Isar/outer_parse.ML"}. +*} + +ML {* map OuterLex.mk_text (explode "hello") *} + +text {* + + @{ML_response_fake [display] "map OuterLex.mk_text (explode \"hello\")" + "[Token (\), Token (\), Token (\), Token (\), Token (\)]"} + *} +ML {* + OuterLex.mk_text "hello" +*} + +ML {* + + let val input = [OuterLex.mk_text "hello", OuterLex.mk_text "world"]; + in (Scan.one (fn _ => true)) input end + +*} + + chapter {* Parsing *} diff -r 35e1dff0d9bb -r b11653b11bd3 CookBook/ROOT.ML --- a/CookBook/ROOT.ML Fri Oct 17 17:41:34 2008 -0400 +++ b/CookBook/ROOT.ML Mon Oct 20 06:22:11 2008 +0000 @@ -15,5 +15,6 @@ use_thy "Appendix"; use_thy "Recipes/NamedThms"; use_thy "Recipes/Transformation"; +use_thy "Recipes/Antiquotes"; use_thy "Solutions"; \ No newline at end of file diff -r 35e1dff0d9bb -r b11653b11bd3 CookBook/antiquote_setup_plus.ML --- a/CookBook/antiquote_setup_plus.ML Fri Oct 17 17:41:34 2008 -0400 +++ b/CookBook/antiquote_setup_plus.ML Mon Oct 20 06:22:11 2008 +0000 @@ -36,41 +36,48 @@ |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt end; -fun output_ml ml = output_verbatim +fun output_ml_old ml = output_verbatim (fn ctxt => fn ((txt, p), pos) => (ML_Context.eval_in (SOME ctxt) false pos (ml p txt); txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |> Chunks.transform_cmts |> implode)); -fun output_ml_response ml = output_verbatim - (fn ctxt => fn ((x as (rhs, pat), p), pos) => - (ML_Context.eval_in (SOME ctxt) false pos (ml p x); - rhs ^ "\n" ^ - space_implode "\n" (map (fn s => "> " ^ s) - (space_explode "\n" pat)))); +fun output_ml ml src ctxt txt = + (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt); + ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt) + +fun add_response_indicator txt = + space_implode "\n" (map (fn s => "> " ^ s) (space_explode "\n" txt)) -fun output_ml_checked ml src ctxt (txt, pos) = - (ML_Context.eval_in (SOME ctxt) false pos (ml txt); - (if ! ThyOutput.source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos))) - |> (if ! ThyOutput.quotes then quote else I) - |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt) +fun output_ml_response ml src ctxt (lhs,pat) = + (ML_Context.eval_in (SOME ctxt) false Position.none (ml (lhs,pat)); + let val txt = lhs ^ "\n" ^ (add_response_indicator pat) + in ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt end) + +fun output_ml_response_fake ml src ctxt (lhs,pat) = + (ML_Context.eval_in (SOME ctxt) false Position.none (ml lhs); + let val txt = lhs ^ "\n" ^ (add_response_indicator pat) + in ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt end) fun check_file_exists ctxt name = if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode name)) then () else error ("Source file " ^ quote name ^ " does not exist.") + + val _ = ThyOutput.add_commands [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- - Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml ml_val_open)), - ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position - ((Args.name -- Args.name) >> rpair ()))) (output_ml_response (K ml_pat))), + Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml_old ml_val_open)), ("ML_file", ThyOutput.args (Scan.lift Args.name) - (ThyOutput.output (fn _ => fn name => (check_file_exists name; Pretty.str name)))), + (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))), ("ML_text", ThyOutput.args (Scan.lift Args.name) (ThyOutput.output (fn _ => fn s => Pretty.str s))), - ("ML", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_val)), - ("ML_struct", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_struct)), - ("ML_type", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_type))]; + ("ML", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val)), + ("ML_response", ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response ml_pat)), + ("ML_response_fake", + ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response_fake ml_val)), + ("ML_struct", ThyOutput.args (Scan.lift Args.name) (output_ml ml_struct)), + ("ML_type", ThyOutput.args (Scan.lift Args.name) (output_ml ml_type))]; end; diff -r 35e1dff0d9bb -r b11653b11bd3 CookBook/document/root.tex --- a/CookBook/document/root.tex Fri Oct 17 17:41:34 2008 -0400 +++ b/CookBook/document/root.tex Mon Oct 20 06:22:11 2008 +0000 @@ -23,7 +23,7 @@ \renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text \renewcommand{\isastyleminor}{\tt\slshape}% \renewcommand{\isastyle}{\small\tt\slshape}% -%%\isadroptag{theory} +\isadroptag{theory} % sane default for proof documents \parindent 0pt\parskip 0.6ex diff -r 35e1dff0d9bb -r b11653b11bd3 cookbook.pdf Binary file cookbook.pdf has changed