theory Parsing

imports Base "Package/Simple_Inductive_Package"

begin

chapter {* Parsing *}

text {*

  Isabelle distinguishes between \emph{outer} and \emph{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}

  \end{readmore}

*}

section {* Building Generic Parsers *}

text {*

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

  The function @{ML "$$"} 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\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}

  @{ML_response [display,gray] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}

  The function @{ML "$$"} 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"}

  will raise the exception @{text "FAIL"}.

  There are three exceptions used in the parsing combinators:

  \begin{itemize}

  \item @{text "FAIL"} is used to indicate that alternative routes of parsing 

  might be explored. 

  \item @{text "MORE"} indicates that there is not enough input for the parser. For example 

  in @{text "($$ \"h\") []"}.

  \item @{text "ABORT"} is the exception that is raised when a dead end is reached. 

  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).

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

  Scan.one}, 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\")

in

end"

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

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

  For example parsing @{text "h"}, @{text "e"} and @{text "l"} (in this 

  order) you can achieve by:

  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 should use the function @{ML Scan.this_string}:

  Parsers that explore alternatives can be constructed using the function @{ML

  "||"}. 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] 

"let 

in

  (hw input1, hw input2)

end"

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

  The functions @{ML "|--"} and @{ML "--|"} work like the sequencing function 

  for parsers, except that they discard the item being parsed by the first (respectively second)

  parser. For example:

@{ML_response [display,gray]

"let 

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 

  @{text "p"}, if it succeeds; otherwise it returns 

  the default value @{text "x"}. For example:

@{ML_response [display,gray]

"let 

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

in 

  (p input1, p input2)

end" 

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

  The function @{ML Scan.option} works similarly, except no default value can

  be given. Instead, the result is wrapped as an @{text "option"}-type. For example:

@{ML_response [display,gray]

"let 

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

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

  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, if the parsing of @{ML "(p -- q)" for p q} fails. Because in that

  case you lose the information that @{text p} should be followed by @{text q}.

  To see this assume that @{text p} is present in the input, but it is not

  followed by @{text q}. That means @{ML "(p -- q)" for p q} will fail and

  hence the alternative parser @{text r} will be tried. However, in many

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

  of @{text r}, not by the absence of @{text q} in the input. This kind of

  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

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

  @{ML_response [display,gray] 

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

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

                               "Exception ABORT raised"}

  then the parsing aborts and the error message @{text "foo"} is printed. In order to

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

  @{ML "Scan.error"}. For example:

  This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.local_theory"} 

  (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

*}

ML{*fun p_followed_by_q p q r =

let 

in

  ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)

end *}

text {*

  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"} 

  produces the correct error message. Running it with

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

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

  yields the expected parsing. 

  The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as 

  often as it succeeds. For example:

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

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

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

  @{ML "Scan.repeat1"} is similar, but requires that the parser @{text "p"} 

  succeeds at least once.

  Also note that the parser would have aborted with the exception @{text MORE}, if

  you had run it only on just @{text [quotes] "hhhh"}. This can be avoided by using

  the wrapper @{ML Scan.finite} and the ``stopper-token'' @{ML Symbol.stopper}. With

  them you can write:

  @{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, 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

  @{ML_response [display,gray] 

"let 

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

in

   Scan.finite Symbol.stopper p input

end" 

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

  where the function @{ML Symbol.not_eof} ensures that we do not read beyond the 

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

  The function @{ML "Scan.unless p q" for p q} 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\") (explode \"hello\")"

                               "Exception FAIL raised"}

  fails, while

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

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

  succeeds. 

  The functions @{ML Scan.repeat} and @{ML Scan.unless} 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))

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 "(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]

"let 

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

in

  (($$ \"h\") -- ($$ \"e\") >> double) (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)

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.

  (FIXME:  move to an earlier place)

  The function @{ML Scan.ahead} parses some input, but leaves the original

  input unchanged. For example:

  @{ML_response [display,gray]

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

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

  The function @{ML Scan.lift} 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]

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

  (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

  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

  \end{exercise}

*}

section {* Parsing Theory Syntax *}

text {*

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

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

*}

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}.

  \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 @{ML "Ident" in OuterLex} for identifiers, @{ML "Keyword" in

  OuterLex} for keywords and @{ML "Command" in OuterLex} 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

  "OuterSyntax.scan"}. It is given the argument @{ML "Position.none"} since,

  at the moment, we are not interested in generating precise error

  messages. The following code\footnote{Note that because of a possible bug in

  the PolyML runtime system, the result is printed as @{text [quotes] "?"},

  instead of the tokens.}