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 book \cite{paulson-ml2}.

  Isabelle developers are usually concerned with writing parsers for outer

  syntax, either for new definitional packages or for calling tactics. The library 

  for writing such parsers in can roughly be split up 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"}.

*}

section {* Building Up Generic Parsers *}

text {*

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

  The function @{ML "(op $$)"} takes a string 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\"])"}

  This function will either succeed (as in the two examples above) or raise the exeption 

  There are three exceptions used in the parsing combinators:

  \begin{itemize}

  \end{itemize}

  takes a predicate as argument and then parses exactly one item from the input list 

  satisfying this prediate. For example the following parser either consumes an @{ML_text "h"}

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

  Two parser can be connected in sequence by using the funtion @{ML "(op --)"}. 

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

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

  The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing funtion 

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

  parser. For example

@{ML_response [display]

"let 

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

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

  val input = (explode \"hello\")  

in 

  (just_h input, just_e 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 "(op !!)"} helps to produce appropriate error messages

  during parsing. For example if one wants to parse @{ML_text p} 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}

  the parsing of @{ML_open "(p -- q)" for p q} fails. Because one loses the information 

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

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

  failure of @{ML_text r}, not by the absense of @{ML_text p} in the input. These situations

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

  on @{ML_text "hello"}, the parsing succeeds

  @{ML_response [display] 

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

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

  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

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

  to generate the correct error message for @{ML_text q} not following @{ML_text p}, then

  we have to write

*}

ML {*

  fun p_followed_by_q p q r =

  let 

  in

  end

*}

text {*

  Running this parser 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. 

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

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

*}

text {* 

@{ML_response [display]

"let 

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

in

  (($$ \"h\") -- ($$ \"e\") >> double) (explode \"hello\")

end"

"((\"hh\", \"ee\"), [\"l\", \"l\", \"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]

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

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

  (FIXME: In which situations is this useful?) 

*}

text {*

  The parser functions for the theory syntax are contained in the structure

*}

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

  value of type \texttt{'res}). 

  An exception is raised if an appropriate value 

  cannot be produced from the input.

  A range of exceptions can be used to identify different reasons 

  for the failure of a parse.

  This contrasts the standard parsing function in Standard ML,

  which is of type 

  \texttt{type ('res, 'src) reader = 'src -> ('res * 'src) option};

  (for example, \texttt{List.getItem} and \texttt{Substring.getc}).

  However, much of the discussion at 

  FIX file:/home/jeremy/html/ml/SMLBasis/string-cvt.html

  is relevant.

  Naturally one may convert between the two different sorts of parsing functions

  as follows:

  \begin{verbatim}

  open StringCvt ;

  type ('res, 'src) ex_reader = 'src -> 'res * 'src

  (* ex_reader : ('res, 'src) reader -> ('res, 'src) ex_reader *)

  fun ex_reader rdr src = Option.valOf (rdr src) ;

  (* reader : ('res, 'src) ex_reader -> ('res, 'src) reader *)

  fun reader exrdr src = SOME (exrdr src) handle _ => NONE ;

  \end{verbatim}

*}

section{* The \texttt{Scan} structure *}

text {* 

  The source file is \texttt{src/General/scan.ML}.

  This structure provides functions for using and combining parsing functions

  of the type \texttt{'src -> 'res * 'src}.

  Three exceptions are used:

  \begin{verbatim}

  exception MORE of string option;  (*need more input (prompt)*)

  exception FAIL of string option;  (*try alternatives (reason of failure)*)

  exception ABORT of string;        (*dead end*)

  \end{verbatim}

  Many functions in this structure (generally those with names composed of

  symbols) are declared as infix.

  Some functions from that structure are

  \begin{verbatim}

  |-- : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->

  'src -> 'res2 * 'src''

  --| : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->

  'src -> 'res1 * 'src''

  -- : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->

  'src -> ('res1 * 'res2) * 'src''

  ^^ : ('src -> string * 'src') * ('src' -> string * 'src'') ->

  'src -> string * 'src''

  \end{verbatim}

  These functions parse a result off the input source twice.

  \texttt{|--} and \texttt{--|} 

  return the first result and the second result, respectively.

  \texttt{--} returns both.

  \verb|^^| returns the result of concatenating the two results

  (which must be strings).

  Note how, although the types 

  \texttt{'src}, \texttt{'src'} and \texttt{'src''} will normally be the same,

  the types as shown help suggest the behaviour of the functions.

  \begin{verbatim}

  :-- : ('src -> 'res1 * 'src') * ('res1 -> 'src' -> 'res2 * 'src'') ->

  'src -> ('res1 * 'res2) * 'src''

  :|-- : ('src -> 'res1 * 'src') * ('res1 -> 'src' -> 'res2 * 'src'') ->

  'src -> 'res2 * 'src''

  \end{verbatim}

  These are similar to \texttt{|--} and \texttt{--|},

  except that the second parsing function can depend on the result of the first.

  \begin{verbatim}

  >> : ('src -> 'res1 * 'src') * ('res1 -> 'res2) -> 'src -> 'res2 * 'src'

  || : ('src -> 'res_src) * ('src -> 'res_src) -> 'src -> 'res_src

  \end{verbatim}

  \texttt{p >> f} applies a function \texttt{f} to the result of a parse.

  \texttt{||} tries a second parsing function if the first one

  fails by raising an exception of the form \texttt{FAIL \_}.

  \begin{verbatim}

  succeed : 'res -> ('src -> 'res * 'src) ;

  fail : ('src -> 'res_src) ;

  !! : ('src * string option -> string) -> 

  ('src -> 'res_src) -> ('src -> 'res_src) ;

  \end{verbatim}

  \texttt{succeed r} returns \texttt{r}, with the input unchanged.

  \texttt{fail} always fails, raising exception \texttt{FAIL NONE}.

  \texttt{!! f} only affects the failure mode, turning a failure that

  raises \texttt{FAIL \_} into a failure that raises \texttt{ABORT ...}.

  This is used to prevent recovery from the failure ---

  thus, in \texttt{!! parse1 || parse2}, if \texttt{parse1} fails, 

  it won't recover by trying \texttt{parse2}.

  \begin{verbatim}

  one : ('si -> bool) -> ('si list -> 'si * 'si list) ;

  some : ('si -> 'res option) -> ('si list -> 'res * 'si list) ;

  \end{verbatim}

  These require the input to be a list of items:

  they fail, raising \texttt{MORE NONE} if the list is empty.

  On other failures they raise \texttt{FAIL NONE} 

  \texttt{one p} takes the first

  item from the list if it satisfies \texttt{p}, otherwise fails.

  \texttt{some f} takes the first

  item from the list and applies \texttt{f} to it, failing if this returns

  \texttt{NONE}.  

  \begin{verbatim}

  many : ('si -> bool) -> 'si list -> 'si list * 'si list ; 

  \end{verbatim}

  \texttt{many p} takes items from the input until it encounters one 

  which does not satisfy \texttt{p}.  If it reaches the end of the input

  it fails, raising \texttt{MORE NONE}.

  \texttt{many1} (with the same type) fails if the first item 

  does not satisfy \texttt{p}.  

  \begin{verbatim}

  option : ('src -> 'res * 'src) -> ('src -> 'res option * 'src)

  optional : ('src -> 'res * 'src) -> 'res -> ('src -> 'res * 'src)

  \end{verbatim}

  \texttt{option}: 

  where the parser \texttt{f} succeeds with result \texttt{r} 

  or raises \texttt{FAIL \_},

  \texttt{option f} gives the result \texttt{SOME r} or \texttt{NONE}.

  \texttt{optional}: if parser \texttt{f} fails by raising \texttt{FAIL \_},

  \texttt{optional f default} provides the result \texttt{default}.

  \begin{verbatim}

  repeat : ('src -> 'res * 'src) -> 'src -> 'res list * 'src

  repeat1 : ('src -> 'res * 'src) -> 'src -> 'res list * 'src

  bulk : ('src -> 'res * 'src) -> 'src -> 'res list * 'src 

  \end{verbatim}

  \texttt{repeat f} repeatedly parses an item off the remaining input until 

  \texttt{f} fails with \texttt{FAIL \_}

  \texttt{repeat1} is as for \texttt{repeat}, but requires at least one

  successful parse.

  \begin{verbatim}

  lift : ('src -> 'res * 'src) -> ('ex * 'src -> 'res * ('ex * 'src))

  \end{verbatim}

  \texttt{lift} changes the source type of a parser by putting in an extra

  component \texttt{'ex}, which is ignored in the parsing.

  The \texttt{Scan} structure also provides the type \texttt{lexicon}, 

  HOW DO THEY WORK ?? TO BE COMPLETED

  \begin{verbatim}

  dest_lexicon: lexicon -> string list ;

  make_lexicon: string list list -> lexicon ;

  empty_lexicon: lexicon ;

  extend_lexicon: string list list -> lexicon -> lexicon ;

  merge_lexicons: lexicon -> lexicon -> lexicon ;

  is_literal: lexicon -> string list -> bool ;

  literal: lexicon -> string list -> string list * string list ;

  \end{verbatim}

  Two lexicons, for the commands and keywords, are stored and can be retrieved

  by:

  \begin{verbatim}

  val (command_lexicon, keyword_lexicon) = OuterSyntax.get_lexicons () ;

  val commands = Scan.dest_lexicon command_lexicon ;

  val keywords = Scan.dest_lexicon keyword_lexicon ;

  \end{verbatim}

*}

section{* The \texttt{OuterLex} structure *}

text {*

  The source file is @{text "src/Pure/Isar/outer_lex.ML"}.

  In some other source files its name is abbreviated:

  \begin{verbatim}

  structure T = OuterLex;

  \end{verbatim}

  This structure defines the type \texttt{token}.

  (The types

  \texttt{OuterLex.token},

  \texttt{OuterParse.token} and

  \texttt{SpecParse.token} are all the same).

  Input text is split up into tokens, and the input source type for many parsing

  functions is \texttt{token list}.

  The datatype definition (which is not published in the signature) is

  \begin{verbatim}

  datatype token = Token of Position.T * (token_kind * string);

  \end{verbatim}

  but here are some runnable examples for viewing tokens: 

*}

text {*

  FIXME

  @{text "

  begin{verbatim}

  type token = T.token ;

  val toks : token list = OuterSyntax.scan ``theory,imports;begin x.y.z apply ?v1 ?'a 'a -- || 44 simp (* xx *) { * fff * }'' ;

  print_depth 20 ;

  List.map T.text_of toks ;

  val proper_toks = List.filter T.is_proper toks ;