isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:f6f8f8ba1eb1
+:f2dea0465bb4
 @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")"
 "Exception ABORT raised"}
 then the parsing aborts and the error message @{text "foo"} is printed out. In order to
-see the error message properly, we need to prefix the parser with the function
+see the error message, we need to prefix the parser with the function
 @{ML "Scan.error"}. For example
 @{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
 "Exception Error \"foo\" raised"}
 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"}.
 The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}.
 \end{readmore}
-The structure @{ML_struct OuterLex} defines several kinds of token (for example
+The structure @{ML_struct OuterLex} defines several kinds of tokens (for example
 @{ML "Ident" in OuterLex} for identifiers, @{ML "Keyword" in OuterLex} for keywords and
 @{ML "Command" in OuterLex} for commands). Some token parsers take into account the
-kind of token.
+kind of tokens.
 *}
 text {*
 For the examples below, we can generate a token list out of a string using
 the function @{ML "OuterSyntax.scan"}, which we give below @{ML
 "Position.none"} as argument since, at the moment, we are not interested in
-generating precise error messages. The following
+generating precise error messages. The following code
 @{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\""
 "[Token (\<dots>,(Ident, \"hello\"),\<dots>),
 Token (\<dots>,(Space, \" \"),\<dots>),
 produces three tokens where the first and the last are identifiers, since
 @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any
 other syntactic category.\footnote{Note that because of a possible a bug in
 the PolyML runtime system the result is printed as @{text "?"}, instead of
-the token.} The second indicates a space.
+the tokens.} The second indicates a space.
 Many parsing functions later on will require spaces, comments and the like
 to have already been filtered out.  So from now on we are going to use the
 functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example
 Token (\<dots>,(Keyword, \"|\"),\<dots>),
 Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
 we obtain a list consisting of only a command and two keyword tokens.
 If you want to see which keywords and commands are currently known, type in
-the following (you might have to adjust the @{ML print_depth} in order to
+the following code (you might have to adjust the @{ML print_depth} in order to
 see the complete list):
 @{ML_response_fake [display,gray]
 "let
 val (keywords, commands) = OuterKeyword.get_lexicons ()
 (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
 end"
 "([\"in\",\"in\",\"in\"],[\<dots>])"}
 @{ML "OuterParse.enum1"} works similarly, except that the parsed list must
-be non-empty. Note that we had to add an @{text [quotes] "foo"} at the end
+be non-empty. Note that we had to add a string @{text [quotes] "foo"} at the end
 of the parsed string, otherwise the parser would have consumed all tokens
 and then failed with the exception @{text "MORE"}. Like in the previous
 section, we can avoid this exception using the wrapper @{ML
 Scan.finite}. This time, however, we have to use the ``stopper-token'' @{ML
 OuterLex.stopper}. We can write
 Scan.finite OuterLex.stopper
 (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
 end"
 "([\"in\",\"in\",\"in\"],[])"}
-The following function will help us later to run examples
+The following function will help to run examples.
 *}
 ML{*fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input *}
 @{text [display] "$ isabelle keywords -k foobar some_log_files"}
 The option @{text "-k foobar"} indicates which postfix the name of the keyword file
 will be assigned. In the case above the generated file will be named @{text
-"isar-keywords-foobar.el"}. As indicated, this command requires log files to be
+"isar-keywords-foobar.el"}. As can be seen, this command requires log files to be
 present (in order to extract the keywords from them). To generate these log
 files, we first package the code above into a separate theory file named
 @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the
 complete code.
 in
 OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing
 end"}\\
 \isa{\isacharverbatimclose}\\
 \isacommand{end}
-\end{graybox}
+\end{graybox}\\[-4mm]
-\caption{The file @{text "Command.thy"} is necessary for generating a log
+\caption{\small 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}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-For our purposes it is sufficient to use the log files for the theories
+For our purposes it is sufficient to use the log files of the theories
 @{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as
-the theory @{text "Command.thy"} containing the new
+the log file for the theory @{text "Command.thy"}, which contains the new
-\isacommand{foobar}-command. If you target another logics besides HOL, such
+\isacommand{foobar}-command. If you target other logics besides HOL, such
 as Nominal or ZF, then you need to adapt the log files appropriately.
 @{text Pure} and @{text HOL} are usually compiled during the installation of
 Isabelle. So log files for them should be already available. If not, then
-they can be conveniently compiled using build-script from the Isabelle
+they can be conveniently compiled with the help of the build-script from the Isabelle
 distribution
 @{text [display]
 "$ ./build -m \"Pure\"
 "Pure.gz
 HOL.gz
 Pure-ProofGeneral.gz
 HOL-FoobarCommand.gz"}
-They are the ones we need for creating the keyword files. Assuming the name
+From them we create the keyword files. Assuming the name
-of the directory is in  @{text "ISABELLE_LOGS"},
+of the directory is in  @{text "$ISABELLE_LOGS"},
 then the Unix command for creating the keyword file is:
 @{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 (check for example that @{text "grep foobar
 isar-keywords-foobar.el"} returns something non-empty).  This keyword file
 needs to be copied into the directory @{text "~/.isabelle/etc"}. To make
-Isabelle aware of this keyword file, we have to start it with the option @{text
+Isabelle aware of this keyword file, we have to start Isabelle with the option @{text
 "-k foobar"}, i.e.
 @{text [display] "$ isabelle -k foobar a_theory_file"}
-If we now run the original code
+If we now build a theory on top of @{text "Command.thy"},
+then we can make use of the command \isacommand{foobar}.
+Similarly with any other new command.
+At the moment \isacommand{foobar} is not very useful. Let us refine it a bit
+next by taking 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
+because of @{ML Scan.succeed} does not parse any argument, but immediately
+returns the simple toplevel function @{ML "Toplevel.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
+finally does nothing. For this we can write
 *}
 ML{*let
-val do_nothing = Scan.succeed (Toplevel.theory I)
+fun trace_top_lvl str =
-val kind = OuterKeyword.thy_decl
+Toplevel.theory (fn thy => (tracing str; thy))
-in
-OuterSyntax.command "foobar" "description of foobar" kind do_nothing
+val trace_prop = OuterParse.prop >> trace_top_lvl
-end *}
-text {*
-then we can make use of \isacommand{foobar} in a theory that builds on @{text "Command.thy"}!
-Similarly with any other new command.
-At the moment \isacommand{foobar} is not very useful. Let us next refine it a bit
-by taking 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 because of @{ML Scan.succeed} does not parse
-any argument, but immediately returns the simple toplevel function
-@{ML "Toplevel.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 and finally does nothing. For this we can write
-*}
-ML{*let
-val trace_prop =
-OuterParse.prop >> (fn str => (tracing str; (Toplevel.theory I)))
 val kind = OuterKeyword.thy_decl
 in
 OuterSyntax.command "foobar" "traces a proposition" kind trace_prop
 end *}
 text {*
-Now we can type for example
+Now we can type
 \begin{isabelle}
 \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
-@{text "> True \<and> False"}
+@{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
 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
+\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 (think of
+and then ``open up'' a proof in order to prove the proposition (for example
 \isacommand{lemma}) or prove some other properties (for example in
-\isacommand{function}). To achieve this behaviour, we have to use the kind
+\isacommand{function}). To achieve this kind of behaviour, we have to use the kind
 indicator @{ML thy_goal in OuterKeyword}.
-Below we change \isacommand{foobar} so that it expects a proposition as
+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
 below, we set the kind indicator to @{ML thy_goal in OuterKeyword}.
 *}
 ML%linenumbers{*let
 fun set_up_thm str ctxt =
 let
 val prop = Syntax.read_prop ctxt str
 in
-Proof.theorem_i NONE (K I) [[(Syntax.read_prop ctxt str,[])]] ctxt
+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))
 text {*
 The function @{text set_up_thm} takes a string (the proposition to be
 proved) and a context.  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. In Lines 9 to 11 contain the parser for the proposition.
+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). In Lines 9 to 11 contain the parser for the proposition.
 If we now type \isacommand{foobar}~@{text [quotes] "True \<and> True"}, we obtain the following
 proof state:
 \begin{isabelle}
 \isacommand{apply}@{text "(rule TrueI)+"}\\
 \isacommand{done}
 \end{isabelle}
-(FIXME What does @{text "Toplevel.theory"}?)
+(FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?)
 (FIXME Explain @{text "OuterKeyword.thy_decl"} and parser)
-*}
+(FIXME read a name and show how to store theorems)
+(FIXME possibly also read a locale)
+*}
+(*<*)
 chapter {* Parsing *}
 text {*
 Lots of Standard ML code is given in this document, for various reasons,
 Naturally one may convert between the two different sorts of parsing functions
 as follows:
 \begin{verbatim}
 open StringCvt ;
 type ('res, 'src) ex_reader = 'src -> 'res * 'src
-(* ex_reader : ('res, 'src) reader -> ('res, 'src) ex_reader *)
+ex_reader : ('res, 'src) reader -> ('res, 'src) ex_reader
 fun ex_reader rdr src = Option.valOf (rdr src) ;
-(* reader : ('res, 'src) ex_reader -> ('res, 'src) reader *)
+reader : ('res, 'src) ex_reader -> ('res, 'src) reader
 fun reader exrdr src = SOME (exrdr src) handle _ => NONE ;
 \end{verbatim}
 *}
 The source file \texttt{src/Pure/Isar/method.ML} shows the use of
 \texttt{Method.add\_method} to add a number of methods.
 *}
+(*>*)
+end
-end

changeset 75	f2dea0465bb4
parent 74	f6f8f8ba1eb1
child 80	95e9c4556221