ProgTutorial/Parsing.thy
changeset 321 e450fa467e3f
parent 319 6bce4acf7f2a
child 322 2b7c08d90e2e
--- a/ProgTutorial/Parsing.thy	Fri Aug 21 16:23:51 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Sat Aug 22 02:56:08 2009 +0200
@@ -1,22 +1,22 @@
 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} syntax. 
-  Commands, such as \isacommand{definition}, \isacommand{inductive} and so
-  on, belong to the outer syntax, whereas terms, types and so on belong to the 
-  inner syntax. For parsing inner syntax, 
-  Isabelle uses a rather general and sophisticated algorithm, which 
-  is driven by priority grammars. Parsers for outer syntax are built up by functional
-  parsing combinators. These combinators are a well-established technique for parsing, 
-  which has, for example, been described in Paulson's classic ML-book \cite{paulson-ml2}.
-  Isabelle developers are usually concerned with writing these outer syntax parsers, 
-  either for new definitional packages or for calling methods with specific arguments. 
+  Isabelle distinguishes between \emph{outer} and \emph{inner}
+  syntax. Commands, such as \isacommand{definition}, \isacommand{inductive}
+  and so on, belong to the outer syntax, whereas terms, types and so on belong
+  to the inner syntax. For parsing inner syntax, Isabelle uses a rather
+  general and sophisticated algorithm, which is driven by priority
+  grammars. Parsers for outer syntax are built up by functional parsing
+  combinators. These combinators are a well-established technique for parsing,
+  which has, for example, been described in Paulson's classic ML-book
+  \cite{paulson-ml2}.  Isabelle developers are usually concerned with writing
+  these outer syntax parsers, either for new definitional packages or for
+  calling methods with specific arguments.
 
   \begin{readmore}
   The library for writing parser combinators is split up, roughly, into two
@@ -25,9 +25,9 @@
   "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
-  in @{ML_file "Pure/Isar/spec_parse.ML"}. Parsers for method arguments
-  are defined in @{ML_file "Pure/Isar/args.ML"}.
+  "Pure/Isar/outer_parse.ML"}. Specific parsers for packages are defined in
+  @{ML_file "Pure/Isar/spec_parse.ML"}. Parsers for method arguments are
+  defined in @{ML_file "Pure/Isar/args.ML"}.
   \end{readmore}
 
 *}
@@ -136,9 +136,9 @@
 end"
   "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
 
-  The functions @{ML_ind  "|--"} and @{ML_ind  "--|"} work like the sequencing function 
-  for parsers, except that they discard the item being parsed by the first (respectively second)
-  parser. For example:
+  The functions @{ML_ind "|--"} and @{ML_ind "--|"} work like the sequencing
+  function for parsers, except that they discard the item being parsed by the
+  first (respectively second) parser. For example:
   
 @{ML_response [display,gray]
 "let 
@@ -944,29 +944,34 @@
    $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
-  that @{text "grep foobar"} on this file returns something
-  non-empty.}  This keyword file needs to
-  be copied into the directory @{text "~/.isabelle/etc"}. To make ProofGeneral
-  aware of this keyword file, you have to start Isabelle with the option @{text
-  "-k foobar"}, that is:
+  the string @{text "foobar"} twice.\footnote{To see whether things are fine,
+  check that @{text "grep foobar"} on this file returns something non-empty.}
+  This keyword file needs to be copied into the directory @{text
+  "~/.isabelle/etc"}. To make ProofGeneral aware of it, you have to start
+  Isabelle with the option @{text "-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. 
-  Similarly with any other new command, and also any new keyword that is 
-  introduced with
+  then the command \isacommand{foobar} can be used. You can just write
+*}
+
+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 
-  it a bit 
-  next by letting it take a proposition as argument and printing this proposition 
-  inside the tracing buffer. 
+  At the moment the command \isacommand{foobar} is not very useful. Let us
+  refine it a bit next by letting it take a proposition as argument and
+  printing this proposition 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
@@ -985,21 +990,18 @@
   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 {*
+  The command is now \isacommand{foobar\_trace} and can be used to 
+  see the proposition in the tracing buffer.  
+*}
+
+foobar_trace "True \<and> False"
 
 text {*
-  Now you can type
-
-  \begin{isabelle}
-  \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
-  @{text "> \"True \<and> False\""}
-  \end{isabelle}
-  
-  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
@@ -1014,7 +1016,7 @@
   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}.
 *}
@@ -1030,7 +1032,7 @@
   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 *}
 
@@ -1044,28 +1046,49 @@
   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 
-  proof state
-
-  \begin{isabelle}
-  \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
-  @{text "goal (1 subgoal):"}\\
-  @{text "1. True \<and> True"}
-  \end{isabelle}
+  If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \<and> True"},
+  you obtain the following proof state
+*}
 
-  and you can build the following proof
+foobar_goal "True \<and> True"
+txt {*
+  \begin{minipage}{\textwidth}
+  @{subgoals [display]}
+  \end{minipage}\medskip
 
-  \begin{isabelle}
-  \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
-  \isacommand{apply}@{text "(rule conjI)"}\\
-  \isacommand{apply}@{text "(rule TrueI)+"}\\
-  \isacommand{done}
-  \end{isabelle}
+  and can prove the proposition as follows.
+*}
+apply(rule conjI)
+apply(rule TrueI)+
+done
+
+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
+