theory Parsing

imports Base

begin

chapter {* Parsing *}

text {*

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

  Theory commands, such as \isacommand{definition}, \isacommand{inductive} and so

  on, belong to the outer syntax, whereas items inside double quotation marks, such 

  as terms, types and so on, belong to the inner syntax. For parsing inner syntax, 

  Isabelle uses a rather general and sophisticated algorithm due to Earley, 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 tactics 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"}.

  \end{readmore}

*}

section {* Building Generic Parsers *}

text {*

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

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

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

  @{ML_text "FAIL"} if no string can be consumed. For example trying to parse

  @{ML_response_fake [display] "($$ \"x\") (explode \"world\")" 

                               "Exception FAIL raised"}

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

  There are three exceptions used in the parsing combinators:

  \begin{itemize}

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

  might be explored. 

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

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

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

  It is used for example in the function @{ML "(op !!)"} (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 "(op $$)"} is the function @{ML

  Scan.one}, in that it takes a predicate as argument and then parses exactly

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

  [quotes] "w"}:

@{ML_response [display] 

"let 

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

  val input1 = (explode \"hello\")

  val input2 = (explode \"world\")

in

    (hw input1, hw input2)

end"

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

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

  sequence can be achieved by

  @{ML_response [display] "(($$ \"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.  

  Parsers that explore 

  alternatives can be constructed using the function @{ML "(op ||)"}. For example, the 

  parser @{ML_open "(p || q)" for p q} returns the result of @{ML_text "p"}, in case it succeeds, 

  otherwise it returns the result of @{ML_text "q"}. For example

@{ML_response [display] 

"let 

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

  val input1 = (explode \"hello\")

  val input2 = (explode \"world\")

in

  (hw input1, hw input2)

end"

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

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

  parser. For example

@{ML_response [display]

"let 

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

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

  val input = (explode \"hello\")  

in 

  (just_e input, just_h input)

end"

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

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

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

  the default value @{ML_text "x"}. For example

@{ML_response [display]

"let 

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

  val input1 = (explode \"hello\")

  val input2 = (explode \"world\")  

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]

"let 

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

  val input1 = (explode \"hello\")

  val input2 = (explode \"world\")  

in 

  (p input1, p input2)

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

  The function @{ML "(op !!)"} helps to produce appropriate error messages

  during parsing. For example if one wants to parse that @{ML_text p} is immediately 

  followed by @{ML_text q}, or start a completely different parser @{ML_text r},

  one might write

  @{ML_open [display] "(p -- q) || r" for p q r}

  However, this parser is problematic for producing an appropriate error message, in case

  the parsing of @{ML_open "(p -- q)" for p q} fails. Because in that case one loses with the parser

  above the information 

  that @{ML_text p} should be followed by @{ML_text q}. To see this consider the case in

  which @{ML_text p} 

  is present in the input, but not @{ML_text q}. That means @{ML_open "(p -- q)" for p q} will fail 

  and the 

  parser for the input ``p-followed-by-q'' and therefore will also fail. The error message is then 

  caused by the

  parsing in case of a failure and invokes an error message. For example if we invoke the parser

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

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

  @{ML_response [display] 

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

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

  but if we invoke it on @{ML_text [quotes] "world"}

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

                               "Exception ABORT raised"}

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

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

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

  @{ML_response_fake [display] "Scan.error ((!! (fn _ => \"foo\") ($$ \"h\")))"

                               "Exception Error \"foo\" raised"}

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

  (FIXME: give reference to later place). 

  Returning to our example of parsing @{ML_open "(p -- q) || r" for p q r}. If we want

  to generate the correct error message for p-followed-by-q, then

  we have to write:

*}

ML {* 

fun p_followed_by_q p q r =

  let 

     val err = (fn _ => p ^ " is not followed by " ^ q)

  in

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

  end

*}

text {*

  Running this parser with

  @{ML_response_fake [display] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"holle\")"

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

  gives the correct error message. Running it with

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

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

  yields the expected parsing. 

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

  often as it succeeds. For example

  @{ML_response [display] "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 @{ML_text "p"} 

  succeeds at least once.

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

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

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

  them we can write

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

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

  However, this kind of manually wrapping needs to be done only very rarely

  in practise, because it is already done by the infrastructure for you. 

  After parsing succeeded, one nearly always wants to apply a function on the parsed 

  items. This is done using the function @{ML_open "(p >> f)" for p f} which runs 

  first the parser @{ML_text p} and upon successful completion applies the 

  function @{ML_text f} to the result. For example

@{ML_response [display]

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

  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]

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

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

  (FIXME: In which situations is this useful? Give examples.) 

*}

section {* Parsing Theory Syntax *}

text {*

  Most of the time, however, Isabelle developers have to deal with parsing tokens, not strings.

  This is because the parsers for the theory syntax, as well as the parsers for the 

  argument syntax of proof methods and attributes use the type 

  @{ML_type OuterLex.token} (which is identical to the type @{ML_type OuterParse.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 token (for example 

  @{ML "OuterLex.Ident"} for identifiers, @{ML "OuterLex.Keyword"} for keywords and

  @{ML "OuterLex.Command"} for commands). Some token parsers take into account the 

  kind of token.

  We can generate a token list out of a string using the function @{ML

  "OuterSyntax.scan"}, which we give below @{ML "Position.none"} as argument

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

  messages. The following

@{ML_response_fake [display] "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

  @{ML_text [quotes] "hello"} and @{ML_text [quotes] "world"} do not match any

  other syntactic category.\footnote{Note that because of a possible a bug in

  the PolyML runtime system the result is printed as @{text "?"}, instead of

  the token.} The second indicates a space.

  Many parsing functions later on will require spaces, comments and the like

  to have been filtered out.  In what follows below, we are going to use the 

  functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example

@{ML_response_fake [display]

"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 are going to use the function

*}

ML {* 

fun filtered_input str = 

       filter OuterLex.is_proper (OuterSyntax.scan Position.none str) 

*}

text {*

  If we parse

@{ML_response_fake [display] 

"filtered_input \"inductive | for\"" 

"[Token (\<dots>,(Command, \"inductive\"),\<dots>), 

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

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

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

  the following (you might have to adjust the @{ML print_depth} in order to

  see the complete list):

@{ML_response_fake [display] 

"let 

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

in 

  (Scan.dest_lexicon commands, Scan.dest_lexicon keywords)

end" 

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

  Now the parser @{ML "OuterParse.$$$"} parses a single keyword. For example

@{ML_response [display]

"let 

  val input1 = filtered_input \"where for\"

  val input2 = filtered_input \"| in\"

in 

  (OuterParse.$$$ \"where\" input1, OuterParse.$$$ \"|\" input2)

end"

"((\"where\",\<dots>),(\"|\",\<dots>))"}

  Like before, we can sequentially connect parsers with @{ML "(op --)"}. For example 

@{ML_response [display]

"let 

  val input = filtered_input \"| in\"

in 

  (OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\") input

end"

"((\"|\",\"in\"),[])"}

  The parser @{ML_open "OuterParse.enum s p" for s p} parses a possibly empty 

  list of items recognised by the parser @{ML_text p}, where the items are 

  separated by the string @{ML_text s}. For example

@{ML_response [display]

"let 

  val input = filtered_input \"in | in | in end\"

in 

  (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input

end" 

"([\"in\",\"in\",\"in\"],[\<dots>])"}

  @{ML "OuterParse.enum1"} works similarly, except that the parsed list must

  be non-empty. Note that we had to add a @{ML_text [quotes] "end"} at the end

  of the parsed string, otherwise the parser would have consumed all tokens

  and then failed with the exception @{ML_text "MORE"}. Like in the previous

  section, we can avoid this exception using the wrapper @{ML

  Scan.finite}. This time, however, we have to use the ``stopper-token'' @{ML

  OuterLex.stopper}. We can write

@{ML_response [display]

"let 

  val input = filtered_input \"in | in | in\"

in 

  Scan.finite OuterLex.stopper (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input

end" 

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

  The function @{ML "OuterParse.!!!"} can be used to force termination of the

  parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section), 

  except that the error message is fixed to be @{text [quotes] "Outer syntax error"}

  with a relatively precise description of the failure. For example:

@{ML_response_fake [display]

"let 

  val input = filtered_input \"in |\"

  val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\"

in 

  Scan.error (OuterParse.!!! parse_bar_then_in) input 

end"

"Exception ERROR \"Outer syntax error: keyword \"|\" expected, 

but keyword in was found\" raised"

}

*}

section {* Positional Information *}

text {*

  @{ML OuterParse.position}

*}

ML {*

  OuterParse.position

*}

section {* Parsing Inner Syntax *}

ML {*

let 

  val input = OuterSyntax.scan Position.none "0"

in 

  OuterParse.prop input

end 

*}

ML {*

  OuterParse.opt_target

*}

ML {*

  OuterParse.opt_target --

  OuterParse.fixes -- 

  OuterParse.for_fixes --

  Scan.optional (OuterParse.$$$ "where" |--

    OuterParse.!!! (OuterParse.enum1 "|" (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []

*}

text {* (FIXME funny output for a proposition) *}

chapter {* Parsing *}

text {*

  Lots of Standard ML code is given in this document, for various reasons,

  including:

  \begin{itemize}

  \item direct quotation of code found in the Isabelle source files,

  or simplified versions of such code

  \item identifiers found in the Isabelle source code, with their types 

  (or specialisations of their types)

  \item code examples, which can be run by the reader, to help illustrate the

  behaviour of functions found in the Isabelle source code

  \item ancillary functions, not from the Isabelle source code, 

  which enable the reader to run relevant code examples

  \item type abbreviations, which help explain the uses of certain functions

  \end{itemize}

*}

section {* Parsing Isar input *}

text {*

  The typical parsing function has the type

  \texttt{'src -> 'res * 'src}, with input  

  of type \texttt{'src}, returning a result 

  of type \texttt{'res}, which is (or is derived from) the first part of the

  input, and also returning the remainder of the input.

  (In the common case, when it is clear what the ``remainder of the input''

  means, we will just say that the functions ``returns'' the