theory Parsing

imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package"

uses "Parsing.ML"

begin

chapter {* Parsing *}

text {*

  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 OuterParse} in the file @{ML_file

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

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

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

  \end{readmore}

*}

section {* Building Generic Parsers *}

text {*

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

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

  or raise the exception @{text "FAIL"} if no string can be consumed. For

  example trying to parse

  @{ML_response_fake [display,gray] 

  "($$ \"x\") (Symbol.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).

@{ML_response_fake [display,gray]

"let 

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

in

  (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 

  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\"]))"}

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

  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 

  result of @{text "p"}, in case it succeeds, otherwise it returns the

  result of @{text "q"}. For example:

@{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\"]))"}

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

  first (respectively second) parser. 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 

  @{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\"

  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\"]))"}

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

@{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\"]))"}

  input unchanged. For example:

  @{ML_response [display,gray]

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

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

  during 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 a useful error

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

  parser above 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

  circumstances this will be the wrong parser for the input ``@{text "p"}-followed-by-something''

  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

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

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

  @{ML_response [display,gray] 

  "(!! (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 _ => \"foo\") ($$ \"h\")) (Symbol.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_response_fake [display,gray] 

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

  "Exception Error \"foo\" raised"}

  (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

  of parsing @{text "p"}-followed-by-@{text "q"}, then you have to write:

*}

ML{*fun p_followed_by_q p q r =

let 

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

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

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

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

  succeeds at least once.

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

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

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

  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\"], [])"}

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

  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. 

  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 

  @{ML "(p >> f)" for p f} 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) 

  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 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\"]))"}

  (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

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

  nesting of comments.

  \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

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

@{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. The second indicates a space.

  We can easily change what is recognised as a keyword with the 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 white space, comments and the like

  to have already been filtered out.  So from now on we are going to use the 

  For example:

@{ML_response_fake [display,gray]

"let

   val input = OuterSyntax.scan Position.none \"hello world\"

in

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

 Token (\<dots>,(Keyword, \"|\"),\<dots>), 

 Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}

  you obtain a list consisting of only one command and two keyword tokens.

  If you want to see which keywords and commands are currently known to Isabelle, 

  type:

@{ML_response_fake [display,gray] 

"let 

  val (keywords, commands) = OuterKeyword.get_lexicons ()

in 

  (Scan.dest_lexicon commands, Scan.dest_lexicon keywords)

end" 

"([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}

  see the complete list.

@{ML_response [display,gray]