isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:abc7f90188af
+:8def50824320
 theory Parsing
 imports Base "Package/Simple_Inductive_Package"
 begin
 chapter {* Parsing *}
 text {*
 ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}
 text {*
 The 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
+OuterLex.token}.
-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"}.
 \end{readmore}
-The structure @{ML_struct OuterLex} defines several kinds of tokens (for example
+The structure @{ML_struct OuterLex} defines several kinds of tokens (for
-@{ML "Ident" in OuterLex} for identifiers, @{ML "Keyword" in OuterLex} for keywords and
+example @{ML "Ident" in OuterLex} for identifiers, @{ML "Keyword" in
-@{ML "Command" in OuterLex} for commands). Some token parsers take into account the
+OuterLex} for keywords and @{ML "Command" in OuterLex} for commands). Some
-kind of tokens.
+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
+"OuterSyntax.scan"}. It is given the argument @{ML "Position.none"} since,
-text {*
+at the moment, we are not interested in generating precise error
-The first example shows how to generate a token list out of a string using
+messages. The following code\footnote{Note that because of a possible bug in
-the function @{ML "OuterSyntax.scan"}. It is given the argument @{ML "Position.none"}
+the PolyML runtime system, the result is printed as @{text [quotes] "?"},
-since, at the moment, we are not interested in generating
+instead of the tokens.}
-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>),
 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.\footnote{Note that because of a possible bug in
+other syntactic category. The second indicates a space.
-the PolyML runtime system, the result is printed as @{text [quotes] "?"}, instead of
-the tokens.} The second indicates a space.
+We can easily change what is recognised as a keyword with
+@{ML OuterKeyword.keyword}. For example calling this function
+*}
+ML{*val _ = OuterKeyword.keyword "hello"*}
+text {*
+then lexing @{text [quotes] "hello world"} will produce
+@{ML_response_fake [display,gray] "OuterSyntax.scan 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 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} to do this. For example:
 filter OuterLex.is_proper input
 end"
 "[Token (\<dots>,(Ident, \"hello\"), \<dots>), Token (\<dots>,(Ident, \"world\"), \<dots>)]"}
 For convenience we define the function:
 *}
 ML{*fun filtered_input str =
 filter OuterLex.is_proper (OuterSyntax.scan Position.none str) *}
 text {*
 If you now parse
 @{ML_response_fake [display,gray]
 "filtered_input \"inductive | for\""
 "[Token (\<dots>,(Command, \"inductive\"),\<dots>),
 in
 (OuterParse.$$$ \"where\" input1, OuterParse.$$$ \"|\" input2)
 end"
 "((\"where\",\<dots>), (\"|\",\<dots>))"}
+Any non-keyword string can be parsed with the function @{ML OuterParse.reserved}.
+For example:
+@{ML_response [display,gray]
+"let
+val p = OuterParse.reserved \"bar\"
+val input = filtered_input \"bar\"
+in
+p input
+end"
+"(\"bar\",[])"}
 Like before, you can sequentially connect parsers with @{ML "--"}. For example:
 @{ML_response [display,gray]
 "let
 val input = filtered_input \"| in\"
 (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
 end"
 "([\"in\", \"in\", \"in\"], [])"}
 The following function will help to run examples.
 *}
 ML{*fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input *}
 text {*
 \begin{readmore}
 The functions related to positions are implemented in the file
 @{ML_file "Pure/General/position.ML"}.
 \end{readmore}
+*}
+text {*
+(FIXME: there are also handy parsers for ML-expressions and ML-files)
 *}
 section {* Context Parser (TBD) *}
 text {*
 @{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.
+Similarly with any other new command, and also any new keyword that is
+introduced with
+*}
-At the moment \isacommand{foobar} is not very useful. Let us refine it a bit
+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.
 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
 \isacommand{apply}@{text "(rule conjI)"}\\
 \isacommand{apply}@{text "(rule TrueI)+"}\\
 \isacommand{done}
 \end{isabelle}
-(FIXME read a name and show how to store theorems)
+(FIXME: read a name and show how to store theorems)
 *}
 section {* Methods (TBD) *}
 text {*

changeset 230	8def50824320
parent 229	abc7f90188af
child 236	7b6d81ff9d9a