isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:7e04dc2368b0
+:fbcb89d84ba6
 in
 (hw input1, hw input2)
 end"
 "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
-Two parser can be connected in sequence by using the function @{ML "--"}.
+Two parsers can be connected in sequence by using the function @{ML "--"}.
-For example parsing @{text "h"}, @{text "e"} and @{text "l"} in this
+For example parsing @{text "h"}, @{text "e"} and @{text "l"} (in this
-sequence you can achieve by:
+order) you can achieve by:
 @{ML_response [display,gray] "(($$ \"h\") -- ($$ \"e\") -- ($$ \"l\")) (explode \"hello\")"
 "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
 Note how the result of consumed strings builds up on the left as nested pairs.
 @{ML_response [display,gray] "Scan.this_string \"hell\" (explode \"hello\")"
 "(\"hell\", [\"o\"])"}
 Parsers that explore alternatives can be constructed using the function @{ML
-"||"}. For example, the parser @{ML "(p || q)" for p q} returns the
+"||"}. The parser @{ML "(p || q)" for p q} returns the
 result of @{text "p"}, in case it succeeds, otherwise it returns the
 result of @{text "q"}. For example:
 @{ML_response [display,gray]
 in
 (p input1, p input2)
 end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
 The function @{ML "!!"} helps to produce appropriate error messages
-during parsing. For example if you want to parse that @{text p} is immediately
+for parsing. For example if you want to parse @{text p} immediately
 followed by @{text q}, or start a completely different parser @{text r},
 you might write:
 @{ML [display,gray] "(p -- q) || r" for p q r}
 However, this parser is problematic for producing an appropriate error
-message, in case the parsing of @{ML "(p -- q)" for p q} fails. Because in
+message, if the parsing of @{ML "(p -- q)" for p q} fails. Because in that
-that case you lose the information that @{text p} should be followed by
+case you lose the information that @{text p} should be followed by @{text q}.
-@{text q}. To see this consider the case in which @{text p} is present in
+To see this assume that @{text p} is present in the input, but it is not
-the input, but not @{text q}. That means @{ML "(p -- q)" for p q} will fail
+followed by @{text q}. That means @{ML "(p -- q)" for p q} will fail and
-and the alternative parser @{text r} will be tried. However in many
+hence the alternative parser @{text r} will be tried. However, in many
-circumstance this will be the wrong parser for the input ``p-followed-by-q''
+circumstances this will be the wrong parser for the input ``p-followed-by-something''
-and therefore will also fail. The error message is then caused by the
+and therefore will also fail. The error message is then caused by the failure
-failure of @{text r}, not by the absence of @{text q} in the input. This
+of @{text r}, not by the absence of @{text q} in the input. This kind of
-kind of situation can be avoided when using the function @{ML "!!"}.
+situation can be avoided when using the function @{ML "!!"}.  This function
-This function aborts the whole process of parsing in case of a
+aborts the whole process of parsing in case of a failure and prints an error
-failure and prints an error message. For example if you invoke the parser
+message. For example if you invoke the parser
 @{ML [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\"))"}
 on @{text [quotes] "hello"}, the parsing succeeds
 ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
 end *}
 text {*
-Running this parser with the @{text [quotes] "h"} and @{text [quotes] "e"}, and
+Running this parser with the arguments
+@{text [quotes] "h"}, @{text [quotes] "e"} and @{text [quotes] "w"}, and
 the input @{text [quotes] "holle"}
 @{ML_response_fake [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"holle\")"
 "Exception ERROR \"h is not followed by e\" raised"}
 Scan.finite Symbol.stopper p input2)
 end"
 "(([\"f\", \"o\", \"o\", \"o\", \"o\", \"o\"], []),
 ([\"f\", \"o\", \"o\"], [\"*\", \"o\", \"o\", \"o\"]))"}
-After parsing is done, you nearly always want to apply a function on the parsed
+After parsing is done, you almost always want to apply a function to the parsed
 items. One way to do this is the function @{ML "(p >> f)" for p f}, which runs
 first the parser @{text p} and upon successful completion applies the
 function @{text f} to the result. For example
 @{ML_response [display,gray]
 (FIXME: In which situations is this useful? Give examples.)
 \begin{exercise}\label{ex:scancmts}
 Write a parser that parses an input string so that any comment enclosed
-inside @{text "(*\<dots>*)"} is replaced by a the same comment but enclosed inside
+within @{text "(*\<dots>*)"} is replaced by the same comment but enclosed within
 @{text "(**\<dots>**)"} in the output string. To enclose a string, you can use the
 function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML
 "s1 ^ s ^ s2" for s1 s2 s}.
 \end{exercise}
 *}
 (FIXME: or give parser for numbers)
 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
+occurred. 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
 *}
 ML{*fun filtered_input' str =
 section {* Parsing Specifications\label{sec:parsingspecs} *}
 text {*
 There are a number of special purpose parsers that help with parsing
 specifications of function definitions, inductive predicates and so on. In
-Capter~\ref{chp:package}, for example, we will need to parse specifications
+Chapter~\ref{chp:package}, for example, we will need to parse specifications
 for inductive predicates of the form:
 *}
 simple_inductive
 even and odd
 text {*
 Whenever types are given, they are stored in the @{ML SOME}s. The types are
 not yet used to type the variables: this must be done by type-inference later
 on. Since types are part of the inner syntax they are strings with some
 encoded information (see previous section). If a syntax translation is
-present for a variable, then it is stored in the @{ML Mixfix} datastructure;
+present for a variable, then it is stored in the @{ML Mixfix} data structure;
 no syntax translation is indicated by @{ML NoSyn}.
 \begin{readmore}
-The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
+The data structure for syntax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
 \end{readmore}
 Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
 list of introduction rules, that is propositions with theorem
 annotations. The introduction rules are propositions parsed by @{ML
 \texttt{SpecParse.token} are all the same).
 Input text is split up into tokens, and the input source type for many parsing
 functions is \texttt{token list}.
-The datatype definition (which is not published in the signature) is
+The data type definition (which is not published in the signature) is
 \begin{verbatim}
 datatype token = Token of Position.T * (token_kind * string);
 \end{verbatim}
 but here are some runnable examples for viewing tokens:
 section{* The \texttt{Args} structure *}
 text {*
 The source file is \texttt{src/Pure/Isar/args.ML}.
-The primary type of this structure is the \texttt{src} datatype;
+The primary type of this structure is the \texttt{src} data type;
 the single constructors not published in the signature, but
 \texttt{Args.src} and \texttt{Args.dest\_src}
 are in fact the constructor and destructor functions.
 Note that the types \texttt{Attrib.src} and \texttt{Method.src}
 are in fact \texttt{Args.src}.

changeset 220	fbcb89d84ba6
parent 211	d5accbc67e1b
child 221	a9eb69749c93