diff -r a9eb69749c93 -r 1dc03eaa7cb9 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Mon Mar 30 17:40:20 2009 +0200 +++ b/ProgTutorial/Parsing.thy Wed Apr 01 12:28:14 2009 +0100 @@ -195,7 +195,7 @@ @{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"} + This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.local_theory"} (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 @@ -350,8 +350,6 @@ section {* Parsing Theory Syntax *} text {* - (FIXME: context parser) - Most of the time, however, Isabelle developers have to deal with parsing tokens, not strings. These token parsers have the type: *} @@ -620,12 +618,14 @@ for inductive predicates of the form: *} +(* simple_inductive even and odd where even0: "even 0" | evenS: "odd n \ even (Suc n)" | oddS: "even n \ odd (Suc n)" +*) text {* For this we are going to use the parser: @@ -680,7 +680,7 @@ val input = filtered_input \"foo::\\\"int \ bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\" in - parse OuterParse.fixes input + parse OuterParse.fixes input end" "([(foo, SOME \"\\^E\\^Ftoken\\^Eint \ bool\\^E\\^F\\^E\", NoSyn), (bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)), @@ -700,10 +700,10 @@ \end{readmore} Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a - list of introduction rules, that is propositions with theorem - annotations. The introduction rules are propositions parsed by @{ML - OuterParse.prop}. However, they can include an optional theorem name plus - some attributes. For example + list of introduction rules, that is propositions with theorem annotations + such as rule names and attributes. The introduction rules are propositions + parsed by @{ML OuterParse.prop}. However, they can include an optional + theorem name plus some attributes. For example @{ML_response [display,gray] "let val input = filtered_input \"foo_lemma[intro,dest!]:\" @@ -753,8 +753,6 @@ section {* New Commands and Keyword Files\label{sec:newcommand} *} text {* - (FIXME: update to the right command setup --- is this still needed?) - Often new commands, for example for providing new definitional principles, need to be implemented. While this is not difficult on the ML-level, new commands, in order to be useful, need to be recognised by @@ -767,16 +765,16 @@ *} ML{*let - val do_nothing = Scan.succeed (Toplevel.theory I) + val do_nothing = Scan.succeed (LocalTheory.theory I) val kind = OuterKeyword.thy_decl in - OuterSyntax.command "foobar" "description of foobar" kind do_nothing + OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing end *} text {* - The crucial function @{ML OuterSyntax.command} expects a name for the command, a - short description, a kind indicator (which we will explain later on more thoroughly) and a - parser producing a top-level transition function (its purpose will also explained + The crucial function @{ML OuterSyntax.local_theory} expects a name for the command, a + short description, a kind indicator (which we will explain later more thoroughly) and a + parser producing a local theory transition (its purpose will also explained later). While this is everything you have to do on the ML-level, you need a keyword @@ -804,15 +802,15 @@ \isacommand{ML}~@{text "\"}\\ @{ML "let - val do_nothing = Scan.succeed (Toplevel.theory I) + val do_nothing = Scan.succeed (LocalTheory.theory I) val kind = OuterKeyword.thy_decl in - OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing + OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing end"}\\ @{text "\"}\\ \isacommand{end} \end{graybox} - \caption{\small The file @{text "Command.thy"} is necessary for generating a log + \caption{The file @{text "Command.thy"} is necessary for generating a log file. This log file enables Isabelle to generate a keyword file containing the command \isacommand{foobar}.\label{fig:commandtheory}} \end{figure} @@ -910,22 +908,22 @@ The crucial part of a command is the function that determines the behaviour of the command. In the code above we used a ``do-nothing''-function, which because of @{ML Scan.succeed} does not parse any argument, but immediately - returns the simple toplevel function @{ML "Toplevel.theory I"}. We can + returns the simple function @{ML "LocalTheory.theory I"}. We can replace this code by a function that first parses a proposition (using the parser @{ML OuterParse.prop}), then prints out the tracing - information (using a new top-level function @{text trace_top_lvl}) and + information (using a new function @{text trace_prop}) and finally does nothing. For this you can write: *} ML{*let - fun trace_top_lvl str = - Toplevel.theory (fn thy => (tracing str; thy)) + fun trace_prop str = + LocalTheory.theory (fn lthy => (tracing str; lthy)) - val trace_prop = OuterParse.prop >> trace_top_lvl - + val trace_prop_parser = OuterParse.prop >> trace_prop val kind = OuterKeyword.thy_decl in - OuterSyntax.command "foobar" "traces a proposition" kind trace_prop + OuterSyntax.local_theory "foobar" "traces a proposition" + kind trace_prop_parser end *} text {* @@ -938,17 +936,19 @@ and see the proposition in the tracing buffer. - Note that so far we used @{ML thy_decl in OuterKeyword} as the kind indicator - for the command. This means that the command finishes as soon as the - arguments are processed. Examples of this kind of commands are - \isacommand{definition} and \isacommand{declare}. In other cases, - commands are expected to parse some arguments, for example a proposition, - and then ``open up'' a proof in order to prove the proposition (for example + Note that so far we used @{ML thy_decl in OuterKeyword} as the kind + indicator for the command. This means that the command finishes as soon as + the arguments are processed. Examples of this kind of commands are + \isacommand{definition} and \isacommand{declare}. In other cases, commands + are expected to parse some arguments, for example a proposition, and then + ``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 thy_goal in OuterKeyword}. Note, however, once you change the - ``kind'' of a command from @{ML thy_decl in OuterKeyword} to @{ML thy_goal in OuterKeyword} - then the keyword file needs to be re-created! + \isacommand{function}). To achieve this kind of behaviour, you have to use + the kind indicator @{ML thy_goal in OuterKeyword} and the function @{ML + "local_theory_to_proof" in OuterSyntax} to set up the command. Note, + however, once you change the ``kind'' of a command from @{ML thy_decl in + OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs + to be re-created! Below we change \isacommand{foobar} so that it takes a proposition as argument and then starts a proof in order to prove it. Therefore in Line 13, @@ -956,34 +956,32 @@ *} ML%linenosgray{*let - fun set_up_thm str ctxt = + fun prove_prop str ctxt = let val prop = Syntax.read_prop ctxt str in Proof.theorem_i NONE (K I) [[(prop,[])]] ctxt end; - val prove_prop = OuterParse.prop >> - (fn str => Toplevel.print o - Toplevel.local_theory_to_proof NONE (set_up_thm str)) - + val prove_prop_parser = OuterParse.prop >> prove_prop val kind = OuterKeyword.thy_goal in - OuterSyntax.command "foobar" "proving a proposition" kind prove_prop + OuterSyntax.local_theory_to_proof "foobar" "proving a proposition" + kind prove_prop_parser end *} text {* - The function @{text set_up_thm} in Lines 2 to 7 takes a string (the proposition to be + The function @{text prove_prop} in Lines 2 to 7 takes a string (the proposition to be proved) and a context as argument. The context is necessary in order to be able to use @{ML Syntax.read_prop}, which converts a string into a proper proposition. In Line 6 the function @{ML Proof.theorem_i} 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 should be done with the theorem once it is proved (we chose to just forget - about it). Lines 9 to 11 contain the parser for the proposition. + about it). Line 9 contains the parser for the proposition. If you now type \isacommand{foobar}~@{text [quotes] "True \ True"}, you obtain the following - proof state: + proof state \begin{isabelle} \isacommand{foobar}~@{text [quotes] "True \ True"}\\ @@ -991,7 +989,7 @@ @{text "1. True \ True"} \end{isabelle} - and you can build the proof + and you can build the following proof \begin{isabelle} \isacommand{foobar}~@{text [quotes] "True \ True"}\\ @@ -1000,12 +998,6 @@ \isacommand{done} \end{isabelle} - - - (FIXME What do @{ML "Toplevel.theory"} - @{ML "Toplevel.print"} - @{ML Toplevel.local_theory} do?) - (FIXME read a name and show how to store theorems) *}