theory Parsing

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

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

  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)

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

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

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

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

  that @{ML_ind explode} in @{ML_struct Symbol} is aware of character

  sequences, for example @{text "\<foo>"}, that have a special meaning in

  Isabelle. To see the difference consider

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

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

  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 

  @{ML_ind  "||" in Scan}. 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 

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

  The function @{ML_ind option in Scan} 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\")

  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

  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_ind error in Scan}. For example:

  @{ML_response_fake [display,gray] 

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

  "Exception Error \"foo\" raised"}

  This ``prefixing'' is usually done by wrappers such as @{ML_ind local_theory in OuterSyntax} 

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

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

  @{ML_ind repeat1 in Scan} 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 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 

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

  (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

  example @{ML_ind Ident in OuterLex} for identifiers, @{ML Keyword in

  OuterLex} for keywords and @{ML_ind 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_ind scan in OuterSyntax}. 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.}

@{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_ind keyword in OuterKeyword}. For example calling it with 

*}

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 

  functions @{ML filter} and @{ML_ind is_proper in OuterLex} to do this. 

  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)