theory Parsing

imports Main

begin

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 ;

  List.map T.kind_of proper_toks ;

  List.map T.unparse proper_toks ;

  List.map T.val_of proper_toks ;

  end{verbatim}"}

*}

text {*

  The function \texttt{is\_proper : token -> bool} identifies tokens which are

  not white space or comments: many parsing functions assume require spaces or

  comments to have been filtered out.

  There is a special end-of-file token:

  \begin{verbatim}

  val (tok_eof : token, is_eof : token -> bool) = T.stopper ; 

  (* end of file token *)

  \end{verbatim}

*}

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

text {*

  The source file is \texttt{src/Pure/Isar/outer\_parse.ML}.

  In some other source files its name is abbreviated:

  \begin{verbatim}

  structure P = OuterParse;

  \end{verbatim}

  Here the parsers use \texttt{token list} as the input source type. 

  Some of the parsers simply select the first token, provided that it is of the

  right kind (as returned by \texttt{T.kind\_of}): these are 

  \texttt{ command, keyword, short\_ident, long\_ident, sym\_ident, term\_var,

  type\_ident, type\_var, number, string, alt\_string, verbatim, sync, eof}

  Others select the first token, provided that it is one of several kinds,

  (eg, \texttt{name, xname, text, typ}).

  \begin{verbatim}

  type 'a tlp = token list -> 'a * token list ; (* token list parser *)

  $$$ : string -> string tlp

  nat : int tlp ;

  maybe : 'a tlp -> 'a option tlp ;

  \end{verbatim}

  \texttt{\$\$\$ s} returns the first token,

  if it equals \texttt{s} \emph{and} \texttt{s} is a keyword.

  \texttt{nat} returns the first token, if it is a number, and evaluates it.

  \texttt{maybe}: if \texttt{p} returns \texttt{r}, 

  then \texttt{maybe p} returns \texttt{SOME r} ;

  if the first token is an underscore, it returns \texttt{NONE}.

  A few examples:

  \begin{verbatim}

  P.list : 'a tlp -> 'a list tlp ; (* likewise P.list1 *)

  P.and_list : 'a tlp -> 'a list tlp ; (* likewise P.and_list1 *)

  val toks : token list = OuterSyntax.scan "44 ,_, 66,77" ;

  val proper_toks = List.filter T.is_proper toks ;

  P.list P.nat toks ; (* OK, doesn't recognize white space *)

  P.list P.nat proper_toks ; (* fails, doesn't recognize what follows ',' *)

  P.list (P.maybe P.nat) proper_toks ; (* fails, end of input *)

  P.list (P.maybe P.nat) (proper_toks @ [tok_eof]) ; (* OK *)

  val toks : token list = OuterSyntax.scan "44 and 55 and 66 and 77" ;

  P.and_list P.nat (List.filter T.is_proper toks @ [tok_eof]) ; (* ??? *)

  \end{verbatim}

  The following code helps run examples:

  \begin{verbatim}

  fun parse_str tlp str = 

  let val toks : token list = OuterSyntax.scan str ;

  val proper_toks = List.filter T.is_proper toks @ [tok_eof] ;

  val (res, rem_toks) = tlp proper_toks ;

  val rem_str = String.concat

  (Library.separate " " (List.map T.unparse rem_toks)) ;

  in (res, rem_str) end ;

  \end{verbatim}

  Some examples from \texttt{src/Pure/Isar/outer\_parse.ML}

  \begin{verbatim}

  val type_args =

  type_ident >> Library.single ||

  $$$ "(" |-- !!! (list1 type_ident --| $$$ ")") ||

  Scan.succeed [];

  \end{verbatim}

  There are three ways parsing a list of type arguments can succeed.

  The first line reads a single type argument, and turns it into a singleton

  list.

  The second line reads "(", and then the remainder, ignoring the "(" ;

  the remainder consists of a list of type identifiers (at least one),

  and then a ")" which is also ignored.

  The \texttt{!!!} ensures that if the parsing proceeds this far and then fails,

  it won't try the third line (see the description of \texttt{Scan.!!}).

  The third line consumes no input and returns the empty list.

  \begin{verbatim}

  fun triple2 (x, (y, z)) = (x, y, z);

  val arity = xname -- ($$$ "::" |-- !!! (

  Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) []

  -- sort)) >> triple2;

  \end{verbatim}

  The parser \texttt{arity} reads a typename $t$, then ``\texttt{::}'' (which is

  ignored), then optionally a list $ss$ of sorts and then another sort $s$.

  The result $(t, (ss, s))$ is transformed by \texttt{triple2} to $(t, ss, s)$.

  The second line reads the optional list of sorts:

  it reads first ``\texttt{(}'' and last ``\texttt{)}'', which are both ignored,

  and between them a comma-separated list of sorts.

  If this list is absent, the default \texttt{[]} provides the list of sorts.

  \begin{verbatim}

  parse_str P.type_args "('a, 'b) ntyp" ;

  parse_str P.type_args "'a ntyp" ;

  parse_str P.type_args "ntyp" ;

  parse_str P.arity "ty :: tycl" ;

  parse_str P.arity "ty :: (tycl1, tycl2) tycl" ;

  \end{verbatim}

*}

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

text {*

  The source file is \texttt{src/Pure/Isar/spec\_parse.ML}.

  This structure contains token list parsers for more complicated values.

  For example, 

  \begin{verbatim}

  open SpecParse ;

  attrib : Attrib.src tok_rdr ; 

  attribs : Attrib.src list tok_rdr ;

  opt_attribs : Attrib.src list tok_rdr ;

  xthm : (thmref * Attrib.src list) tok_rdr ;

  xthms1 : (thmref * Attrib.src list) list tok_rdr ;

  parse_str attrib "simp" ;

  parse_str opt_attribs "hello" ;

  val (ass, "") = parse_str attribs "[standard, xxxx, simp, intro, OF sym]" ;

  map Args.dest_src ass ;

  val (asrc, "") = parse_str attrib "THEN trans [THEN sym]" ;

  parse_str xthm "mythm [attr]" ;

  parse_str xthms1 "thm1 [attr] thms2" ;

  \end{verbatim}

  As you can see, attributes are described using types of the \texttt{Args}

  structure, described below.

*}

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

text {*

  The source file is \texttt{src/Pure/Isar/args.ML}.

  The primary type of this structure is the \texttt{src} datatype;

  the single constructors not published in the signature, but 

  \texttt{Args.src} and \texttt{Args.dest\_src}

  are in fact the constructor and destructor functions.

  Note that the types \texttt{Attrib.src} and \texttt{Method.src}

  are in fact \texttt{Args.src}.

  \begin{verbatim}

  src : (string * Args.T list) * Position.T -> Args.src ;

  dest_src : Args.src -> (string * Args.T list) * Position.T ;

  Args.pretty_src : Proof.context -> Args.src -> Pretty.T ;

  fun pr_src ctxt src = Pretty.string_of (Args.pretty_src ctxt src) ;

  val thy = ML_Context.the_context () ;

  val ctxt = ProofContext.init thy ;

  map (pr_src ctxt) ass ;

  \end{verbatim}

  So an \texttt{Args.src} consists of the first word, then a list of further 

  ``arguments'', of type \texttt{Args.T}, with information about position in the

  input.

  \begin{verbatim}

  (* how an Args.src is parsed *)

  P.position : 'a tlp -> ('a * Position.T) tlp ;

  P.arguments : Args.T list tlp ;

  val parse_src : Args.src tlp =

  P.position (P.xname -- P.arguments) >> Args.src ;

  \end{verbatim}

  \begin{verbatim}

  val ((first_word, args), pos) = Args.dest_src asrc ;

  map Args.string_of args ;

  \end{verbatim}

  The \texttt{Args} structure contains more parsers and parser transformers 

  for which the input source type is \texttt{Args.T list}.  For example,

  \begin{verbatim}

  type 'a atlp = Args.T list -> 'a * Args.T list ;

  open Args ;

  nat : int atlp ; (* also Args.int *)

  thm_sel : PureThy.interval list atlp ;

  list : 'a atlp -> 'a list atlp ;

  attribs : (string -> string) -> Args.src list atlp ;

  opt_attribs : (string -> string) -> Args.src list atlp ;

  (* parse_atl_str : 'a atlp -> (string -> 'a * string) ;

  given an Args.T list parser, to get a string parser *)

  fun parse_atl_str atlp str = 

  let val (ats, rem_str) = parse_str P.arguments str ;

  val (res, rem_ats) = atlp ats ;

  in (res, String.concat (Library.separate " "

  (List.map Args.string_of rem_ats @ [rem_str]))) end ;

  parse_atl_str Args.int "-1-," ;

  parse_atl_str (Scan.option Args.int) "x1-," ;

  parse_atl_str Args.thm_sel "(1-,4,13-22)" ;

  val (ats as atsrc :: _, "") = parse_atl_str (Args.attribs I)

  "[THEN trans [THEN sym], simp, OF sym]" ;

  \end{verbatim}

  From here, an attribute is interpreted using \texttt{Attrib.attribute}.

  \texttt{Args} has a large number of functions which parse an \texttt{Args.src}

  and also refer to a generic context.  

  Note the use of \texttt{Scan.lift} for this.

  (as does \texttt{Attrib} - RETHINK THIS)

  (\texttt{Args.syntax} shown below has type specialised)

  \begin{verbatim}

  type ('res, 'src) parse_fn = 'src -> 'res * 'src ;

  type 'a cgatlp = ('a, Context.generic * Args.T list) parse_fn ;

  Scan.lift : 'a atlp -> 'a cgatlp ;

  term : term cgatlp ;

  typ : typ cgatlp ;

  Args.syntax : string -> 'res cgatlp -> src -> ('res, Context.generic) parse_fn ;

  Attrib.thm : thm cgatlp ;

  Attrib.thms : thm list cgatlp ;

  Attrib.multi_thm : thm list cgatlp ;

  (* parse_cgatl_str : 'a cgatlp -> (string -> 'a * string) ;

  given a (Context.generic * Args.T list) parser, to get a string parser *)

  fun parse_cgatl_str cgatlp str = 

  let 

    (* use the current generic context *)

    val generic = Context.Theory thy ;

    val (ats, rem_str) = parse_str P.arguments str ;

    (* ignore any change to the generic context *)

    val (res, (_, rem_ats)) = cgatlp (generic, ats) ;

  in (res, String.concat (Library.separate " "

      (List.map Args.string_of rem_ats @ [rem_str]))) end ;

  \end{verbatim}

*}

section{* Attributes, and the \texttt{Attrib} structure *}

text {*

  The type \texttt{attribute} is declared in \texttt{src/Pure/thm.ML}.

  The source file for the \texttt{Attrib} structure is

  \texttt{src/Pure/Isar/attrib.ML}.

  Most attributes use a theorem to change a generic context (for example, 

  by declaring that the theorem should be used, by default, in simplification),

  or change a theorem (which most often involves referring to the current

  theory). 

  The functions \texttt{Thm.rule\_attribute} and

  \texttt{Thm.declaration\_attribute} create attributes of these kinds.

  \begin{verbatim}

  type attribute = Context.generic * thm -> Context.generic * thm;

  type 'a trf = 'a -> 'a ; (* transformer of a given type *)

  Thm.rule_attribute  : (Context.generic -> thm -> thm) -> attribute ;

  Thm.declaration_attribute : (thm -> Context.generic trf) -> attribute ;

  Attrib.print_attributes : theory -> unit ;

  Attrib.pretty_attribs : Proof.context -> src list -> Pretty.T list ;

  List.app Pretty.writeln (Attrib.pretty_attribs ctxt ass) ;

  \end{verbatim}

  An attribute is stored in a theory as indicated by:

  \begin{verbatim}

  Attrib.add_attributes : 

  (bstring * (src -> attribute) * string) list -> theory trf ; 

  (*

  Attrib.add_attributes [("THEN", THEN_att, "resolution with rule")] ;

  *)

  \end{verbatim}

  where the first and third arguments are name and description of the attribute,

  and the second is a function which parses the attribute input text 

  (including the attribute name, which has necessarily already been parsed).

  Here, \texttt{THEN\_att} is a function declared in the code for the