isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:a9eb69749c93
+:1dc03eaa7cb9
 @{ML "Scan.error"}. For example:
 @{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
 r}. If you want to generate the correct error message for p-followed-by-q,
 then you have to write:
 *}
 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:
 *}
 ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}
 specifications of function definitions, inductive predicates and so on. In
 Chapter~\ref{chp:package}, for example, we will need to parse specifications
 for inductive predicates of the form:
 *}
+(*
 simple_inductive
 even and odd
 where
 even0: "even 0"
 | evenS: "odd n \<Longrightarrow> even (Suc n)"
 | oddS: "even n \<Longrightarrow> odd (Suc n)"
+*)
 text {*
 For this we are going to use the parser:
 *}
 @{ML_response [display,gray]
 "let
 val input = filtered_input
 \"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
 in
 parse OuterParse.fixes input
 end"
 "([(foo, SOME \"\\^E\\^Ftoken\\^Eint \<Rightarrow> bool\\^E\\^F\\^E\", NoSyn),
 (bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)),
 (blonk, NONE, NoSyn)],[])"}
 *}
 \begin{readmore}
 The data structure for syntax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
 \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
+list of introduction rules, that is propositions with theorem annotations
-annotations. The introduction rules are propositions parsed by @{ML
+such as rule names and attributes. The introduction rules are propositions
-OuterParse.prop}. However, they can include an optional theorem name plus
+parsed by @{ML OuterParse.prop}. However, they can include an optional
-some attributes. For example
+theorem name plus some attributes. For example
 @{ML_response [display,gray] "let
 val input = filtered_input \"foo_lemma[intro,dest!]:\"
 val ((name, attrib), _) = parse (SpecParse.thm_name \":\") input
 in
 *}
 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
 ProofGeneral. This results in some subtle configuration issues, which we
 will explain in this section.
 at all. We shall name this command \isacommand{foobar}. On the ML-level it can be
 defined as:
 *}
 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
+The crucial function @{ML OuterSyntax.local_theory} expects a name for the command, a
-short description, a kind indicator (which we will explain later on more thoroughly) and a
+short description, a kind indicator (which we will explain later more thoroughly) and a
-parser producing a top-level transition function (its purpose will also explained
+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
 file that can be loaded by ProofGeneral. This is to enable ProofGeneral to
 recognise \isacommand{foobar} as a command. Such a keyword file can be
 \isacommand{imports}~@{text Main}\\
 \isacommand{begin}\\
 \isacommand{ML}~@{text "\<verbopen>"}\\
 @{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 "\<verbclose>"}\\
 \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}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 inside the tracing buffer.
 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 =
+fun trace_prop str =
-Toplevel.theory (fn thy => (tracing str; thy))
+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 {*
 Now you can type
 @{text "> \"True \<and> False\""}
 \end{isabelle}
 and see the proposition in the tracing buffer.
-Note that so far we used @{ML thy_decl in OuterKeyword} as the kind indicator
+Note that so far we used @{ML thy_decl in OuterKeyword} as the kind
-for the command.  This means that the command finishes as soon as the
+indicator for the command.  This means that the command finishes as soon as
-arguments are processed. Examples of this kind of commands are
+the arguments are processed. Examples of this kind of commands are
-\isacommand{definition} and \isacommand{declare}.  In other cases,
+\isacommand{definition} and \isacommand{declare}.  In other cases, commands
-commands are expected to parse some arguments, for example a proposition,
+are expected to parse some arguments, for example a proposition, and then
-and then ``open up'' a proof in order to prove the proposition (for example
+``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
+\isacommand{function}). To achieve this kind of behaviour, you have to use
-indicator @{ML thy_goal in OuterKeyword}.  Note, however, once you change the
+the kind indicator @{ML thy_goal in OuterKeyword} and the function @{ML
-``kind'' of a command from @{ML thy_decl in OuterKeyword} to @{ML thy_goal in OuterKeyword}
+"local_theory_to_proof" in OuterSyntax} to set up the command.  Note,
-then the keyword file needs to be re-created!
+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,
 we set the kind indicator to @{ML thy_goal in OuterKeyword}.
 *}
 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 >>
+val prove_prop_parser = OuterParse.prop >> prove_prop
-(fn str => Toplevel.print o
-Toplevel.local_theory_to_proof NONE (set_up_thm str))
 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 \<and> True"}, you obtain the following
-proof state:
+proof state
 \begin{isabelle}
 \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
 @{text "goal (1 subgoal):"}\\
 @{text "1. True \<and> True"}
 \end{isabelle}
-and you can build the proof
+and you can build the following proof
 \begin{isabelle}
 \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
 \isacommand{apply}@{text "(rule conjI)"}\\
 \isacommand{apply}@{text "(rule TrueI)+"}\\
 \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)
 *}
 section {* Methods (TBD) *}

changeset 222	1dc03eaa7cb9
parent 221	a9eb69749c93
parent 219	98d43270024f
child 227	a00c7721fc3b