isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:185921021551
+:e450fa467e3f
 theory Parsing
-imports Base "Package/Simple_Inductive_Package"
+imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package"
 uses "Parsing.ML"
 begin
 chapter {* Parsing *}
 text {*
+Isabelle distinguishes between \emph{outer} and \emph{inner}
-Isabelle distinguishes between \emph{outer} and \emph{inner} syntax.
+syntax. Commands, such as \isacommand{definition}, \isacommand{inductive}
-Commands, such as \isacommand{definition}, \isacommand{inductive} and so
+and so on, belong to the outer syntax, whereas terms, types and so on belong
-on, belong to the outer syntax, whereas terms, types and so on belong to the
+to the inner syntax. For parsing inner syntax, Isabelle uses a rather
-inner syntax. For parsing inner syntax,
+general and sophisticated algorithm, which is driven by priority
-Isabelle uses a rather general and sophisticated algorithm, which
+grammars. Parsers for outer syntax are built up by functional parsing
-is driven by priority grammars. Parsers for outer syntax are built up by functional
+combinators. These combinators are a well-established technique for parsing,
-parsing combinators. These combinators are a well-established technique for parsing,
+which has, for example, been described in Paulson's classic ML-book
-which has, for example, been described in Paulson's classic ML-book \cite{paulson-ml2}.
+\cite{paulson-ml2}.  Isabelle developers are usually concerned with writing
-Isabelle developers are usually concerned with writing these outer syntax parsers,
+these outer syntax parsers, either for new definitional packages or for
-either for new definitional packages or for calling methods with specific arguments.
+calling methods with specific arguments.
 \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
 "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 OuterParse} in the file @{ML_file
-"Pure/Isar/outer_parse.ML"}. Specific parsers for packages are defined
+"Pure/Isar/outer_parse.ML"}. Specific parsers for packages are defined in
-in @{ML_file "Pure/Isar/spec_parse.ML"}. Parsers for method arguments
+@{ML_file "Pure/Isar/spec_parse.ML"}. Parsers for method arguments are
-are defined in @{ML_file "Pure/Isar/args.ML"}.
+defined in @{ML_file "Pure/Isar/args.ML"}.
 \end{readmore}
 *}
 section {* Building Generic Parsers *}
 in
 (hw input1, hw input2)
 end"
 "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
-The functions @{ML_ind  "|--"} and @{ML_ind  "--|"} work like the sequencing function
+The functions @{ML_ind "|--"} and @{ML_ind "--|"} work like the sequencing
-for parsers, except that they discard the item being parsed by the first (respectively second)
+function for parsers, except that they discard the item being parsed by the
-parser. For example:
+first (respectively second) parser. For example:
 @{ML_response [display,gray]
 "let
 val just_e = $$ \"h\" |-- $$ \"e\"
 val just_h = $$ \"h\" --| $$ \"e\"
 @{text [display]
 "$ isabelle keywords -k foobar
 $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
 The result is the file @{text "isar-keywords-foobar.el"}. It should contain
-the string @{text "foobar"} twice.\footnote{To see whether things are fine, check
+the string @{text "foobar"} twice.\footnote{To see whether things are fine,
-that @{text "grep foobar"} on this file returns something
+check that @{text "grep foobar"} on this file returns something non-empty.}
-non-empty.}  This keyword file needs to
+This keyword file needs to be copied into the directory @{text
-be copied into the directory @{text "~/.isabelle/etc"}. To make ProofGeneral
+"~/.isabelle/etc"}. To make ProofGeneral aware of it, you have to start
-aware of this keyword file, you have to start Isabelle with the option @{text
+Isabelle with the option @{text "-k foobar"}, that is:
-"-k foobar"}, that is:
 @{text [display] "$ isabelle emacs -k foobar a_theory_file"}
 If you now build a theory on top of @{text "Command.thy"},
-then the command \isacommand{foobar} can be used.
+then the command \isacommand{foobar} can be used. You can just write
-Similarly with any other new command, and also any new keyword that is
+*}
-introduced with
+foobar
+text {*
+but you will not see any action as we chose to implement this command to do
+nothing.  A similarly procedure has to be done with any other new command, and
+also any new keyword that is introduced with @{ML_ind OuterKeyword.keyword}.
 *}
 ML{*val _ = OuterKeyword.keyword "blink" *}
 text {*
-At the moment the command \isacommand{foobar} is not very useful. Let us refine
+At the moment the command \isacommand{foobar} is not very useful. Let us
-it a bit
+refine it a bit next by letting it take a proposition as argument and
-next by letting it take a proposition as argument and printing this proposition
+printing this proposition inside the tracing buffer.
-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_ind  succeed in Scan} does not parse any argument, but immediately
 returns the simple function @{ML "LocalTheory.theory I"}. We can
 LocalTheory.theory (fn lthy => (tracing str; lthy))
 val trace_prop_parser = OuterParse.prop >> trace_prop
 val kind = OuterKeyword.thy_decl
 in
-OuterSyntax.local_theory "foobar" "traces a proposition"
+OuterSyntax.local_theory "foobar_trace" "traces a proposition"
 kind trace_prop_parser
 end *}
+text {*
-text {*
+The command is now \isacommand{foobar\_trace} and can be used to
-Now you can type
+see the proposition in the tracing buffer.
+*}
-\begin{isabelle}
-\isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+foobar_trace "True \<and> False"
-@{text "> \"True \<and> False\""}
-\end{isabelle}
+text {*
-and see the proposition in the tracing buffer.
 Note that so far we used @{ML_ind  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
 "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
+Below we change \isacommand{foobar\_trace} 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
 end;
 val prove_prop_parser = OuterParse.prop >> prove_prop
 val kind = OuterKeyword.thy_goal
 in
-OuterSyntax.local_theory_to_proof "foobar" "proving a proposition"
+OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition"
 kind prove_prop_parser
 end *}
 text {*
 The function @{text prove_prop} in Lines 2 to 7 takes a string (the proposition to be
 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). Line 9 contains the parser for the proposition.
-If you now type \isacommand{foobar}~@{text [quotes] "True \<and> True"}, you obtain the following
+If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \<and> True"},
-proof state
+you obtain the following proof state
+*}
-\begin{isabelle}
-\isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
+foobar_goal "True \<and> True"
-@{text "goal (1 subgoal):"}\\
+txt {*
-@{text "1. True \<and> True"}
+\begin{minipage}{\textwidth}
-\end{isabelle}
+@{subgoals [display]}
+\end{minipage}\medskip
-and you can build the following proof
+and can prove the proposition as follows.
-\begin{isabelle}
+*}
-\isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
+apply(rule conjI)
-\isacommand{apply}@{text "(rule conjI)"}\\
+apply(rule TrueI)+
-\isacommand{apply}@{text "(rule TrueI)+"}\\
+done
-\isacommand{done}
-\end{isabelle}
+text {*
 (FIXME: read a name and show how to store theorems; see @{ML_ind  note in LocalTheory})
 *}
+ML_val{*val r = ref (NONE:(unit -> term) option)*}
+ML{*let
+fun setup_proof (txt, pos) lthy =
+let
+val trm = ML_Context.evaluate lthy true ("r", r) txt
+in
+Proof.theorem_i NONE (K I) [[(trm,[])]] lthy
+end;
+val setup_proof_parser = OuterParse.ML_source >> setup_proof
+val kind = OuterKeyword.thy_goal
+in
+OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition"
+kind setup_proof_parser
+end*}
+foobar_prove {* @{prop "True"} *}
+apply(rule TrueI)
+done
 section {* Methods (TBD) *}

changeset 321	e450fa467e3f
parent 319	6bce4acf7f2a
child 322	2b7c08d90e2e