theory Parsing

imports Base "Package/Simple_Inductive_Package"

keywords "foobar" "foobar_trace" :: thy_decl and

         "foobar_goal" "foobar_prove" :: thy_goal

begin

  \begin{flushright}

  {\em An important principle underlying the success and popularity of Unix\\ is

  the philosophy of building on the work of others.} \\[1ex]

  Tony Travis in an email about the\\ ``LINUX is obsolete'' debate 

  \end{flushright}

  \begin{flushright}

  {\em

  Document your code as if someone else might have to take it over at any 

  moment and know what to do with it. That person might actually be you -- 

  how often have you had to revisit your own code and thought to yourself, 

  what was I trying to do here?} \\[1ex]

  Phil Chu in ``Seven Habits of Highly Effective Programmers'' 

  \end{flushright}

  Isabelle distinguishes between \emph{outer} and \emph{inner}

  syntax. Commands, such as \isacommand{definition}, \isacommand{inductive}

  and so on, belong to the outer syntax, whereas terms, types and so on belong

  to the inner syntax. For parsing inner syntax, Isabelle uses a rather

  general and sophisticated algorithm, which is driven by priority

  grammars. Parsers for outer syntax are built up by functional parsing

  combinators. These combinators are a well-established technique for parsing,

  which has, for example, been described in Paulson's classic ML-book

  \cite{paulson-ml2}.  Isabelle developers are usually concerned with writing

  these outer syntax parsers, either for new definitional packages or for

  calling methods with specific arguments.

  \begin{readmore}

  The library for writing parser combinators is split up, roughly, into two

  parts: The first part consists of a collection of generic parser combinators

  defined in the structure @{ML_struct Scan} in the file @{ML_file

  "Pure/General/scan.ML"}. The second part of the library consists of

  combinators for dealing with specific token types, which are defined in the

  structure @{ML_struct Parse} in the file @{ML_file

  "Pure/Isar/parse.ML"}. In addition specific parsers for packages are 

  defined in @{ML_file "Pure/Isar/parse_spec.ML"}. Parsers for method arguments 

  are defined in @{ML_file "Pure/Isar/args.ML"}.

  \end{readmore}

  Let us first have a look at parsing strings using generic parsing

  combinators. The function @{ML_ind "$$" in Scan} takes a string as argument and will

  ``consume'' this string from a given input list of strings. ``Consume'' in

  this context means that it will return a pair consisting of this string and

  the rest of the input list. For example:

  @{ML_response [display,gray] 

  "($$ \"h\") (Symbol.explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}

  @{ML_response [display,gray] 

  "($$ \"w\") (Symbol.explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}

  The function @{ML "$$"} will either succeed (as in the two examples above)

  example trying to parse

  @{ML_response_fake [display,gray] 

  "($$ \"x\") (Symbol.explode \"world\")" 

  "Exception FAIL raised"}

  fail if you try to consume more than a single character.

  There are three exceptions that are raised by the parsing combinators:

  \begin{itemize}

  might be explored. 

  It is used for example in the function @{ML "!!"} (see below).

  \end{itemize}

  However, note that these exceptions are private to the parser and cannot be accessed

  by the programmer (for example to handle them).

  In the examples above we use the function @{ML_ind explode in Symbol} from the

  structure @{ML_struct Symbol}, instead of the more standard library function

  @{ML_ind explode in String}, for obtaining an input list for the parser. The reason is

  that @{ML explode in Symbol} is aware of character

  Isabelle. To see the difference consider

@{ML_response_fake [display,gray]

"let 

  val input = \"\<foo> bar\"

in

  (String.explode input, Symbol.explode input)

end"

"([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"],

 [\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}

  Slightly more general than the parser @{ML "$$"} is the function 

  @{ML_ind one in Scan}, in that it takes a predicate as argument and 

  then parses exactly

  one item from the input list satisfying this predicate. For example the

  following parser either consumes an @{text [quotes] "h"} or a @{text

  [quotes] "w"}:

@{ML_response [display,gray] 

"let 

  val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")

  val input1 = Symbol.explode \"hello\"

  val input2 = Symbol.explode \"world\"

in

  (hw input1, hw input2)

end"

    "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}

  Two parsers can be connected in sequence by using the function @{ML_ind "--" in Scan}. 

  order) you can achieve by:

  @{ML_response [display,gray] 

  "($$ \"h\" -- $$ \"e\" -- $$ \"l\") (Symbol.explode \"hello\")"

  "(((\"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 you can use the function @{ML_ind this_string in Scan}.

  @{ML_response [display,gray] 

  "Scan.this_string \"hell\" (Symbol.explode \"hello\")"

  "(\"hell\", [\"o\"])"}

  Parsers that explore alternatives can be constructed using the function 

  @{ML_ind  "||" in Scan}. The parser @{ML "(p || q)" for p q} returns the

@{ML_response [display,gray] 

"let 

  val hw = $$ \"h\" || $$ \"w\"

  val input1 = Symbol.explode \"hello\"

  val input2 = Symbol.explode \"world\"

in

  (hw input1, hw input2)

end"

  "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}

  The functions @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} work like the sequencing

  function for parsers, except that they discard the item being parsed by the

  first (respectively second) parser. That means the item being dropped is the 

  one that @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} ``point'' away.

  For example:

@{ML_response [display,gray]

"let 

  val just_e = $$ \"h\" |-- $$ \"e\" 

  val just_h = $$ \"h\" --| $$ \"e\" 

  val input = Symbol.explode \"hello\"  

in 

  (just_e input, just_h input)

end"

  "((\"e\", [\"l\", \"l\", \"o\"]), (\"h\", [\"l\", \"l\", \"o\"]))"}

  The parser @{ML "Scan.optional p x" for p x} returns the result of the parser 

@{ML_response [display,gray]

"let 

  val p = Scan.optional ($$ \"h\") \"x\"

  val input1 = Symbol.explode \"hello\"

  val input2 = Symbol.explode \"world\"  

in 

  (p input1, p input2)

end" 

 "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}

  The function @{ML_ind option in Scan} works similarly, except no default value can

@{ML_response [display,gray]

"let 

  val p = Scan.option ($$ \"h\")

  val input1 = Symbol.explode \"hello\"

  val input2 = Symbol.explode \"world\"  

in 

  (p input1, p input2)

end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}

  The function @{ML_ind ahead in Scan} parses some input, but leaves the original

  input unchanged. For example:

  @{ML_response [display,gray]

  "Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")" 

  "(\"foo\", [\"f\", \"o\", \"o\"])"} 

  The function @{ML_ind "!!" in Scan} helps with producing appropriate error messages

  you might write:

  @{ML [display,gray] "(p -- q) || r" for p q r}

  However, this parser is problematic for producing a useful error

  message, if the parsing of @{ML "(p -- q)" for p q} fails. Because with the

  and therefore will also fail. The error message is then caused by the failure

  situation can be avoided when using the function @{ML "!!"}.  This function

  aborts the whole process of parsing in case of a failure and prints an error

  message. For example if you invoke the parser

  @{ML [display,gray] "!! (fn _ => fn _ =>\"foo\") ($$ \"h\")"}

  on @{text [quotes] "hello"}, the parsing succeeds

  @{ML_response [display,gray] 

  "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")" 

  "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}

  but if you invoke it on @{text [quotes] "world"}

  @{ML_response_fake [display,gray] "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"

                               "Exception ABORT raised"}

  see the error message properly, you need to prefix the parser with the function 

  @{ML_ind error in Scan}. For example:

  @{ML_response_fake [display,gray] 

  "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"

  "Exception Error \"foo\" raised"}

  This kind of ``prefixing'' to see the correct error message is usually done by wrappers 

  such as @{ML_ind local_theory in Outer_Syntax} 

  (see Section~\ref{sec:newcommand} which explains this function in more detail). 

  Let us now return to our example of parsing @{ML "(p -- q) || r" for p q

  r}. If you want to generate the correct error message for failure

let 

  val err_msg = fn _ => p ^ " is not followed by " ^ q

in

  ($$ p -- (!! (fn _ => err_msg) ($$ q))) || ($$ r -- $$ r)

  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\") (Symbol.explode \"holle\")"

                               "Exception ERROR \"h is not followed by e\" raised"} 

  produces the correct error message. Running it with

  @{ML_response [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"wworld\")"

                          "((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}

  yields the expected parsing. 

  long as it succeeds. For example:

  @{ML_response [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")" 

                "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}

  Note that @{ML_ind repeat in Scan} stores the parsed items in a list. The function

  succeeds at least once.

  you had it run with the string @{text [quotes] "hhhh"}. This can be avoided by using

  the wrapper @{ML_ind finite in Scan} and the ``stopper-token'' 

  @{ML_ind stopper in Symbol}. With them you can write:

  @{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")" 

                "([\"h\", \"h\", \"h\", \"h\"], [])"}

  The function @{ML stopper in Symbol} is the ``end-of-input'' indicator for parsing strings;

  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_ind repeat in Scan} can be used with @{ML_ind one in Scan} to read any 

  string as in

  @{ML_response [display,gray] 

"let 

   val p = Scan.repeat (Scan.one Symbol.not_eof)

   val input = Symbol.explode \"foo bar foo\"

in

   Scan.finite Symbol.stopper p input

end" 

"([\"f\", \"o\", \"o\", \" \", \"b\", \"a\", \"r\", \" \", \"f\", \"o\", \"o\"], [])"}

  where the function @{ML_ind not_eof in Symbol} ensures that we do not read beyond the 

  end of the input string (i.e.~stopper symbol).

  The function @{ML_ind unless in Scan} takes two parsers: if the first one can 

  parse the input, then the whole parser fails; if not, then the second is tried. Therefore

  @{ML_response_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"

                               "Exception FAIL raised"}

  fails, while

  @{ML_response [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"world\")"

                          "(\"w\",[\"o\", \"r\", \"l\", \"d\"])"}

  succeeds. 

  The functions @{ML_ind repeat in Scan} and @{ML_ind unless in Scan} can 

  be combined to read any input until a certain marker symbol is reached. In the 

  example below the marker symbol is a @{text [quotes] "*"}.

  @{ML_response [display,gray]

"let 

  val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))

  val input1 = Symbol.explode \"fooooo\"

  val input2 = Symbol.explode \"foo*ooo\"

in

  (Scan.finite Symbol.stopper p input1, 

   Scan.finite Symbol.stopper p input2)

end"

"(([\"f\", \"o\", \"o\", \"o\", \"o\", \"o\"], []),

 ([\"f\", \"o\", \"o\"], [\"*\", \"o\", \"o\", \"o\"]))"}

  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_ind ">>" in Scan} where 

  @{ML "(p >> f)" for p f} runs 

@{ML_response [display,gray]

"let 

  fun double (x, y) = (x ^ x, y ^ y) 

  val parser = $$ \"h\" -- $$ \"e\"

in

  (parser >> double) (Symbol.explode \"hello\")

end"

"((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}

  doubles the two parsed input strings; or

  @{ML_response [display,gray] 

"let 

   val p = Scan.repeat (Scan.one Symbol.not_eof)

   val input = Symbol.explode \"foo bar foo\" 

in

   Scan.finite Symbol.stopper (p >> implode) input

end" 

"(\"foo bar foo\",[])"}

  where the single-character strings in the parsed output are transformed

  back into one string.

  The function @{ML_ind lift in Scan} takes a parser and a pair as arguments. This function applies

  the given parser to the second component of the pair and leaves the  first component 

  untouched. For example

@{ML_response [display,gray]

"Scan.lift ($$ \"h\" -- $$ \"e\") (1, Symbol.explode \"hello\")"

"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}

  Be aware of recursive parsers. Suppose you want to read strings separated by

  commas and by parentheses into a tree datastructure; for example, generating

  the tree corresponding to the string @{text [quotes] "(A, A), (A, A)"} where

  datatype:

    Lf of string 

  Since nested parentheses should be treated in a meaningful way---for example

  the string @{text [quotes] "((A))"} should be read into a single 

  leaf---you might implement the following parser.

  $$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")"  

and parse_tree s = 

  This parser corresponds to the grammar:

  \begin{center}

  \begin{tabular}{lcl}

  \end{tabular}

  \end{center}

  parser @{ML parse_basic} reads either a leaf or a tree enclosed in

  parentheses. The parser @{ML parse_tree} reads either a pair of trees

  separated by a comma, or acts like @{ML parse_basic}. Unfortunately,

  because of the mutual recursion, this parser will immediately run into a

  loop, even if it is called without any input. For example

  @{ML_response_fake_both [display, gray]

  "parse_tree \"A\""

  "*** Exception- TOPLEVEL_ERROR raised"}

  raises an exception indicating that the stack limit is reached. Such

  looping parser are not useful, because of ML's strict evaluation of

  arguments. Therefore we need to delay the execution of the

  parser until an input is given. This can be done by adding the parsed

  string as an explicit argument. So the parser above should be implemented

  as follows.

  ($$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")") xs 

and parse_tree s xs = 

  While the type of the parser is unchanged by the addition, its behaviour 

  changed: with this version of the parser the execution is delayed until 

  exactly the parser what we wanted. An example is as follows:

  @{ML_response [display, gray]

  "let

  val input = Symbol.explode \"(A,((A))),A\"

in

  Scan.finite Symbol.stopper (parse_tree \"A\") input

end"

  "(Br (Br (Lf \"A\", Lf \"A\"), Lf \"A\"), [])"}

  \begin{exercise}\label{ex:scancmts}

  Write a parser that parses an input string so that any comment enclosed

  function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML

  "s1 ^ s ^ s2" for s1 s2 s}. Hint: To simplify the task ignore the proper 

  nesting of comments.

  \end{exercise}

  Most of the time, however, Isabelle developers have to deal with parsing

  tokens, not strings.  These token parsers have the type: