isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:74846cb0fff9
+:693711a0c702
 @{ML_response [display,gray] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
 @{ML_response [display,gray] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
+The type of a parser is defined as
 This function will either succeed (as in the two examples above) or raise the exception
 @{text "FAIL"} if no string can be consumed. For example trying to parse
 @{ML_response_fake [display,gray] "($$ \"x\") (explode \"world\")"
 "Exception FAIL raised"}
 "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
 Note how the result of consumed strings builds up on the left as nested pairs.
 If, as in the previous example, you want to parse a particular string,
-then one should use the function @{ML Scan.this_string}:
+then you should use the function @{ML Scan.this_string}:
 @{ML_response [display,gray] "Scan.this_string \"hell\" (explode \"hello\")"
 "(\"hell\", [\"o\"])"}
 Parsers that explore alternatives can be constructed using the function @{ML
 @{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (explode \"hhhh\")"
 "([\"h\", \"h\", \"h\", \"h\"], [])"}
 @{ML Symbol.stopper} is the ``end-of-input'' indicator for parsing strings;
-other stoppers need to be used when parsing tokens, for example. However, this kind of
+other stoppers need to be used when parsing, for example, tokens. However, this kind of
 manually wrapping is often already done by the surrounding infrastructure.
 The function @{ML Scan.repeat} can be used with @{ML Scan.one} to read any
 string as in
 section {* Parsing Theory Syntax *}
 text {*
 Most of the time, however, Isabelle developers have to deal with parsing
-tokens, not strings.  This is because the parsers for the theory syntax, as
+tokens, not strings.  These token parsers will have the type
-well as the parsers for the arguments of proof methods the type @{ML_type OuterLex.token}
+*}
-(which is identical to the type @{ML_type OuterParse.token}).  There are also handy
-parsers for ML-expressions and ML-files.
+ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}
+text {*
+This reason for using token parsers is that theory syntax, as well as the
+parsers for the arguments of proof methods, use the type @{ML_type
+OuterLex.token} (which is identical to the type @{ML_type
+OuterParse.token}).  However, there are also handy parsers for
+ML-expressions and ML-files.
 \begin{readmore}
 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"}.
 kind of tokens.
 *}
 text {*
 The first example shows how to generate a token list out of a string using
-the function @{ML "OuterSyntax.scan"}. It is given below @{ML "Position.none"}
+the function @{ML "OuterSyntax.scan"}. It is given the argument @{ML "Position.none"}
-as argument since, at the moment, we are not interested in generating
+since, at the moment, we are not interested in 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>),
 "let
 val (keywords, commands) = OuterKeyword.get_lexicons ()
 in
 (Scan.dest_lexicon commands, Scan.dest_lexicon keywords)
 end"
-"([\"}\",\"{\",\<dots>],[\"\<rightleftharpoons>\",\"\<leftharpoondown>\",\<dots>])"}
+"([\"}\", \"{\", \<dots>],[\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
 The parser @{ML "OuterParse.$$$"} parses a single keyword. For example:
 @{ML_response [display,gray]
 "let
 val input1 = filtered_input \"where for\"
 val input2 = filtered_input \"| in\"
 in
 (OuterParse.$$$ \"where\" input1, OuterParse.$$$ \"|\" input2)
 end"
-"((\"where\",\<dots>),(\"|\",\<dots>))"}
+"((\"where\",\<dots>), (\"|\",\<dots>))"}
 Like before, you can sequentially connect parsers with @{ML "--"}. For example:
 @{ML_response [display,gray]
 "let
 val input = filtered_input \"| in\"
 in
 (OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\") input
 end"
-"((\"|\",\"in\"),[])"}
+"((\"|\", \"in\"),[])"}
 The parser @{ML "OuterParse.enum s p" for s p} parses a possibly empty
 list of items recognised by the parser @{text p}, where the items being parsed
 are separated by the string @{text s}. For example:
 "let
 val input = filtered_input \"in | in | in foo\"
 in
 (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
 end"
-"([\"in\",\"in\",\"in\"],[\<dots>])"}
+"([\"in\", \"in\", \"in\"],[\<dots>])"}
 @{ML "OuterParse.enum1"} works similarly, except that the parsed list must
 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
 val input = filtered_input \"in | in | in\"
 in
 Scan.finite OuterLex.stopper
 (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
 end"
-"([\"in\",\"in\",\"in\"],[])"}
+"([\"in\", \"in\", \"in\"],[])"}
 The following function will help to run examples.
 *}
 Whenever there is a possibility that the processing of user input can fail,
 it is a good idea to give as much information about where the error
 occured. For this Isabelle can attach positional information to tokens
 and then thread this information up the processing chain. To see this,
-modify the function @{ML filtered_input} described earlier to be
+modify the function @{ML filtered_input} described earlier to
 *}
 ML{*fun filtered_input' str =
 filter OuterLex.is_proper (OuterSyntax.scan (Position.line 7) str) *}
 The positional information is stored so that code called later on will be
 able to give more precise error messages.
 \begin{readmore}
-The functions to do with input and outout of XML and YXML are defined
+The functions to do with input and output of XML and YXML are defined
 in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}.
 \end{readmore}
 *}
 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
 text {*
 Note that the parser does not parse the keyword \simpleinductive, even if it is
 meant to process definitions as shown above. The parser of the keyword
-will be given by the infrastructure that will eventually calls @{ML spec_parser}.
+will be given by the infrastructure that will eventually call @{ML spec_parser}.
 To see what the parser returns, let us parse the string corresponding to the
 definition of @{term even} and @{term odd}:
 (name, map Args.dest_src attrib)
 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
 @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some
-attributes.
+attributes. The name has to end with @{text [quotes] ":"}---see argument of
+@{ML SpecParse.opt_thm_name} in Line 9.
-For the inductive definitions described above only the attibutes @{text "[intro]"} and
-@{text "[simp]"} make sense.
 \begin{readmore}
 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"}
 and @{ML_file "Pure/Isar/args.ML"}.
 \end{readmore}
 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. The directory should include the files:
+on the Unix prompt. If you now also type @{text "ls $ISABELLE_LOGS"}, then the
+directory should include the files:
 @{text [display]
 "Pure.gz
 HOL.gz
 Pure-ProofGeneral.gz
 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.
-(FIXME: explain @{ML Toplevel.print} etc)
 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"}\\
 \isacommand{apply}@{text "(rule conjI)"}\\
 \isacommand{apply}@{text "(rule TrueI)+"}\\
 \isacommand{done}
 \end{isabelle}
+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.
 (FIXME What do @{ML "Toplevel.theory"}
 @{ML "Toplevel.print"}
-@{ML Toplevel.local_theory}?)
+@{ML Toplevel.local_theory} do?)
 (FIXME read a name and show how to store theorems)
 *}

changeset 128	693711a0c702
parent 127	74846cb0fff9
child 131	8db9195bb3e9