isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:daf404920ab9
+:50d3059de9c6
 Most of the time, however, Isabelle developers have to deal with parsing
 tokens, not strings.  These token parsers have the type:
 *}
 ML %grayML{*type 'a parser = Token.T list -> 'a * Token.T list*}
+ML "Thy_Header.get_keywords'"
 text {*
 {\bf REDO!!}
 The reason for using token parsers is that theory syntax, as well as the
 The structure @{ML_struct  Token} defines several kinds of tokens (for
 example @{ML_ind Ident in Token} for identifiers, @{ML Keyword in
 Token} for keywords and @{ML_ind Command in Token} for commands). Some
 token parsers take into account the kind of tokens. The first example shows
 how to generate a token list out of a string using the function
-@{ML_ind scan in Outer_Syntax}. It is given the argument
+@{ML_ind explode in Token}. It is given the argument
 @{ML "Position.none"} since,
 at the moment, we are not interested in generating precise error
 messages. The following code
-@{ML_response_fake [display,gray] "Outer_Syntax.scan
+@{ML_response_fake [display,gray] "Token.explode
-(Keyword.get_lexicons ()) Position.none \"hello world\""
+(Thy_Header.get_keywords' @{context}) Position.none \"hello world\""
 "[Token (\<dots>,(Ident, \"hello\"),\<dots>),
 Token (\<dots>,(Space, \" \"),\<dots>),
 Token (\<dots>,(Ident, \"world\"),\<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. The second indicates a space.
 We can easily change what is recognised as a keyword with the function
-@{ML_ind define in Keyword}. For example calling it with
+@{ML_ind add_keywords in Thy_Header}. For example calling it with
 *}
-ML %grayML{*val _ = Keyword.define ("hello", NONE) *}
+setup {* Thy_Header.add_keywords [(("hello", Position.none),Keyword.no_spec)] *}
 text {*
 then lexing @{text [quotes] "hello world"} will produce
-@{ML_response_fake [display,gray] "Outer_Syntax.scan
+@{ML_response_fake [display,gray] "Token.explode
-(Keyword.get_lexicons ()) Position.none \"hello world\""
+(Thy_Header.get_keywords' @{context}) Position.none \"hello world\""
 "[Token (\<dots>,(Keyword, \"hello\"),\<dots>),
 Token (\<dots>,(Space, \" \"),\<dots>),
 Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
 Many parsing functions later on will require white space, comments and the like
 functions @{ML filter} and @{ML_ind is_proper in Token} to do this.
 For example:
 @{ML_response_fake [display,gray]
 "let
-val input = Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none \"hello world\"
+val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"hello world\"
 in
 filter Token.is_proper input
 end"
 "[Token (\<dots>,(Ident, \"hello\"), \<dots>), Token (\<dots>,(Ident, \"world\"), \<dots>)]"}
 For convenience we define the function:
 *}
 ML %grayML{*fun filtered_input str =
-filter Token.is_proper (Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none str) *}
+filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str) *}
+ML \<open>filtered_input "inductive | for"\<close>
 text {*
 If you now parse
 @{ML_response_fake [display,gray]
 "filtered_input \"inductive | for\""
 Token (\<dots>,(Keyword, \"|\"),\<dots>),
 Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
 you obtain a list consisting of only one command and two keyword tokens.
 If you want to see which keywords and commands are currently known to Isabelle,
-use the function @{ML_ind get_lexicons in Keyword}:
+use the function @{ML_ind get_keywords' in Thy_Header}:
-@{ML_response_fake [display,gray]
+You might have to adjust the @{text ML_print_depth} in order to
-"let
-val (keywords, commands) = Keyword.get_lexicons ()
-in
-(Scan.dest_lexicon commands, Scan.dest_lexicon keywords)
-end"
-"([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
-You might have to adjust the @{ML_ind default_print_depth} in order to
 see the complete list.
 The parser @{ML_ind "$$$" in Parse} parses a single keyword. For example:
 @{ML_response [display,gray]
 and then thread this information up the ``processing chain''. To see this,
 modify the function @{ML filtered_input}, described earlier, as follows
 *}
 ML %grayML{*fun filtered_input' str =
-filter Token.is_proper (Outer_Syntax.scan (Keyword.get_lexicons ()) (Position.line 7) str) *}
+filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 7) str) *}
 text {*
 where we pretend the parsed string starts on line 7. An example is
 @{ML_response_fake [display,gray]
 for terms and  types: you can just call the predefined parsers. Terms can
 be parsed using the function @{ML_ind term in Parse}. For example:
 @{ML_response_fake [display,gray]
 "let
-val input = Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none \"foo\"
+val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"foo\"
 in
 Parse.term input
 end"
 "(\"<markup>\", [])"}
 The result of the decoding is an XML-tree. You can see better what is going on if
 you replace @{ML Position.none} by @{ML "Position.line 42"}, say:
 @{ML_response_fake [display,gray]
 "let
-val input = Outer_Syntax.scan (Keyword.get_lexicons ()) (Position.line 42) \"foo\"
+val input = Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 42) \"foo\"
 in
 YXML.parse (fst (Parse.term input))
 end"
 "Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
 text {*
 For this we are going to use the parser:
 *}
 ML %linenosgray{*val spec_parser =
-Parse.fixes --
+Parse.vars --
 Scan.optional
 (Parse.$$$ "where" |--
 Parse.!!!
 (Parse.enum1 "|"
 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) []*}
 end"
 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
 [((even0,\<dots>),\<dots>),
 ((evenS,\<dots>),\<dots>),
 ((oddS,\<dots>),\<dots>)]), [])"}
+*}
+ML \<open>let
+val input = filtered_input
+"foo::\"int \<Rightarrow> bool\" and bar::nat (\"BAR\" 100) and blonk"
+in
+parse Parse.vars input
+end\<close>
+text {*
 As you see, the result is a pair consisting of a list of
 variables with optional type-annotation and syntax-annotation, and a list of
 rules where every rule has optionally a name and an attribute.
-The function @{ML_ind "fixes" in Parse} in Line 2 of the parser reads an
+The function @{ML_ind "vars" in Parse} in Line 2 of the parser reads an
 \isacommand{and}-separated
 list of variables that can include optional type annotations and syntax translations.
 For example:\footnote{Note that in the code we need to write
 @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes
 in the compound type.}
-@{ML_response [display,gray]
+@{ML_response_fake [display,gray]
 "let
 val input = filtered_input
 \"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
 in
-parse Parse.fixes input
+parse Parse.vars input
 end"
 "([(foo, SOME \<dots>, NoSyn),
-(bar, SOME \<dots>, Mixfix (\"BAR\", [], 100)),
+(bar, SOME \<dots>, Mixfix (Source {text=\"BAR\",...}, [], 100, \<dots>)),
 (blonk, NONE, NoSyn)],[])"}
 *}
 text {*
 Whenever types are given, they are stored in the @{ML SOME}s. The types are
 \end{readmore}
 *}
 text_raw {*
 \begin{exercise}
-Have a look at how the parser @{ML Parse_Spec.where_alt_specs} is implemented
+Have a look at how the parser @{ML Parse_Spec.where_multi_specs} is implemented
 in file @{ML_file "Pure/Isar/parse_spec.ML"}. This parser corresponds
 to the ``where-part'' of the introduction rules given above. Below
-we paraphrase the code of @{ML_ind where_alt_specs in Parse_Spec} adapted to our
+we paraphrase the code of @{ML_ind where_multi_specs in Parse_Spec} adapted to our
 purposes.
 \begin{isabelle}
 *}
 ML %linenosgray{*val spec_parser' =
-Parse.fixes --
+Parse.vars --
 Scan.optional
 (Parse.$$$ "where" |--
 Parse.!!!
 (Parse.enum1 "|"
 ((Parse_Spec.opt_thm_name ":" -- Parse.prop) --|
 *}
 ML %grayML{*let
 val do_nothing = Scan.succeed (Local_Theory.background_theory I)
 in
-Outer_Syntax.local_theory @{command_spec "foobar"}
+Outer_Syntax.local_theory @{command_keyword "foobar"}
 "description of foobar"
 do_nothing
 end *}
 text {*
 ML %grayML{*let
 fun trace_prop str =
 Local_Theory.background_theory (fn ctxt => (tracing str; ctxt))
 in
-Outer_Syntax.local_theory @{command_spec "foobar_trace"}
+Outer_Syntax.local_theory @{command_keyword "foobar_trace"}
 "traces a proposition"
 (Parse.prop >> trace_prop)
 end *}
 text {*
 val prop = Syntax.read_prop ctxt str
 in
 Proof.theorem NONE (K I) [[(prop, [])]] ctxt
 end
 in
-Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"}
+Outer_Syntax.local_theory_to_proof @{command_keyword "foobar_goal"}
 "proves a proposition"
 (Parse.prop >> goal_prop)
 end *}
 text {*
 ML %linenosgray{*let
 fun after_qed thm_name thms lthy =
 Local_Theory.note (thm_name, (flat thms)) lthy |> snd
-fun setup_proof (thm_name, {text, ...}) lthy =
+fun setup_proof (thm_name, src) lthy =
 let
+val text = Input.source_content src
 val trm = Code_Runtime.value lthy result_cookie ("", text)
 in
 Proof.theorem NONE (after_qed thm_name) [[(trm, [])]] lthy
 end
 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
 in
-Outer_Syntax.local_theory_to_proof @{command_spec "foobar_prove"}
+Outer_Syntax.local_theory_to_proof @{command_keyword "foobar_prove"}
 "proving a proposition"
 (parser >> setup_proof)
 end*}
 text {*
 \begin{isabelle}
 \isacommand{thm}~@{text "test"}\\
 @{text "> "}~@{thm TrueI}
 \end{isabelle}
-While this is everything you have to do for a new command when using jEdit,
+*}
-things are not as simple when using Emacs and ProofGeneral. We explain the details
-next.
-*}
+(*
-section {* Proof-General and Keyword Files *}
-text {*
-In order to use a new command in Emacs and Proof-General, you need a keyword
-file that can be loaded by ProofGeneral. To keep things simple we take as
-a running example the command \isacommand{foobar} from the previous section.
-A keyword file can be generated with the command-line:
-@{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 file will be named @{text
-"isar-keywords-foobar.el"}. This command requires log files to be
-present (in order to extract the keywords from them). To generate these log
-files, you first need to package the code above into a separate theory file named
-@{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the
-complete code.
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{figure}[t]
-\begin{graybox}\small
-\isacommand{theory}~@{text Command}\\
-\isacommand{imports}~@{text Main}\\
-\isacommand{keywords} @{text [quotes] "foobar"} @{text "::"} @{text "thy_decl"}\\
-\isacommand{begin}\\
-\isacommand{ML}~@{text "\<verbopen>"}\\
-@{ML
-"let
-val do_nothing = Scan.succeed (Local_Theory.background_theory I)
-in
-Outer_Syntax.local_theory @{command_spec \"foobar\"}
-\"description of foobar\"
-do_nothing
-end"}\\
-@{text "\<verbclose>"}\\
-\isacommand{end}
-\end{graybox}
-\caption{This file can be used to generate a log file. This log file in turn can
-be used 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 of the theories
-@{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as
-the log file for the theory @{text "Command.thy"}, which contains the new
-\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 easily compiled with the build-script from the Isabelle
-distribution.
-@{text [display]
-"$ ./build -m \"Pure\"
-$ ./build -m \"HOL\""}
-The @{text "Pure-ProofGeneral"} theory needs to be compiled with:
-@{text [display] "$ ./build -m \"Pure-ProofGeneral\" \"Pure\""}
-For the theory @{text "Command.thy"}, you first need to create a ``managed'' subdirectory
-with:
-@{text [display] "$ isabelle mkroot -d FoobarCommand"}
-This generates a directory containing the files:
-@{text [display]
-"./FoobarCommand/ROOT
-./FoobarCommand/document
-./FoobarCommand/document/root.tex"}
-You need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
-and add the line
-@{text [display] "no_document use_thy \"Command\";"}
-to the file @{text "./FoobarCommand/ROOT"}. You can now compile the theory by just typing:
-@{text [display] "$ isabelle build"}
-If the compilation succeeds, you have finally created all the necessary log files.
-They are stored in the directory
-@{text [display]  "~/.isabelle/heaps/Isabelle2012/polyml-5.2.1_x86-linux/log"}
-or something similar depending on your Isabelle distribution and architecture.
-One quick way to assign a shell variable to this directory is by typing
-@{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
-on the Unix prompt. If you now type @{text "ls $ISABELLE_LOGS"}, then the
-directory should include the files:
-@{text [display]
-"Pure.gz
-HOL.gz
-Pure-ProofGeneral.gz
-HOL-FoobarCommand.gz"}
-From them you can create the keyword files. Assuming the name
-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.\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 you can now use the command \isacommand{foobar}
-in Proof-General
-A similar procedure has to be done with any
-other new command, and also any new keyword that is introduced with
-the function @{ML_ind define in Keyword}. For example:
-*}
-ML %grayML{*val _ = Keyword.define ("blink", NONE) *}
-text {*
-Also if the kind of a command changes, from @{text "thy_decl"} to
-@{text "thy_goal"} say,  you need to recreate the keyword file.
-*}
 text {*
 {\bf TBD below}
 *}
+*)
 (*
 ML {*
 An example of a very simple method is:
 *}
 method_setup %gray foo =
 {* Scan.succeed
-(K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *}
+(fn ctxt => (SIMPLE_METHOD ((eresolve_tac ctxt [@{thm conjE}] THEN' resolve_tac ctxt [@{thm conjI}]) 1))) *}
 "foo method for conjE and conjI"
 text {*
 It defines the method @{text foo}, which takes no arguments (therefore the
 parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which
 lemma "True"
 apply(test)
 oops
 method_setup joker = {*
-Scan.lift (Scan.succeed (fn ctxt => Method.cheating ctxt true)) *} {* bla *}
+Scan.lift (Scan.succeed (fn ctxt => Method.cheating true)) *} {* bla *}
 lemma "False"
 apply(joker)
 oops
 text {* if true is set then always works *}
-ML {* atac *}
+ML {* assume_tac *}
-method_setup first_atac = {* Scan.lift (Scan.succeed (K (SIMPLE_METHOD (atac 1)))) *} {* bla *}
+method_setup first_atac = {* Scan.lift (Scan.succeed (fn ctxt => (SIMPLE_METHOD (assume_tac ctxt 1)))) *} {* bla *}
 ML {* HEADGOAL *}
 lemma "A \<Longrightarrow> A"
 apply(first_atac)
 oops
-method_setup my_atac = {* Scan.lift (Scan.succeed (K (SIMPLE_METHOD' atac))) *} {* bla *}
+method_setup my_atac = {* Scan.lift (Scan.succeed (fn ctxt => (SIMPLE_METHOD' (assume_tac ctxt)))) *} {* bla *}
 lemma "A \<Longrightarrow> A"
 apply(my_atac)
 oops
 *)
 ML {* resolve_tac *}
 method_setup myrule =
-{* Scan.lift (Scan.succeed (K (METHOD (fn thms => resolve_tac thms 1)))) *}
+{* Scan.lift (Scan.succeed (fn ctxt => (METHOD (fn thms => resolve_tac ctxt thms 1)))) *}
 {* bla *}
 lemma
 assumes a: "A \<Longrightarrow> B \<Longrightarrow> C"
 shows "C"

changeset 563	50d3059de9c6
parent 559	ffa5c4ec9611
child 565	cecd7a941885