# HG changeset patch # User Christian Urban # Date 1220668338 -7200 # Node ID 2a69b119cdeee74e8c82493310a1d3da8d6a7b6b # Parent cd861a121f60d39f5eb50166e1df758fd5679eaa added verbatim the notes by Jeremy diff -r cd861a121f60 -r 2a69b119cdee CookBook/Parsing.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Parsing.thy Sat Sep 06 04:32:18 2008 +0200 @@ -0,0 +1,660 @@ +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 + structure \texttt{Attrib}, but not published in its signature. + The source file \texttt{src/Pure/Isar/attrib.ML} shows the use of + \texttt{Attrib.add\_attributes} to add a number of attributes. + + \begin{verbatim} + FullAttrib.THEN_att : src -> attribute ; + FullAttrib.THEN_att atsrc (generic, ML_Context.thm "sym") ; + FullAttrib.THEN_att atsrc (generic, ML_Context.thm "all_comm") ; + \end{verbatim} + + \begin{verbatim} + Attrib.syntax : attribute cgatlp -> src -> attribute ; + Attrib.no_args : attribute -> src -> attribute ; + \end{verbatim} + When this is called as \texttt{syntax scan src (gc, th)} + the generic context \texttt{gc} is used + (and potentially changed to \texttt{gc'}) + by \texttt{scan} in parsing to obtain an attribute \texttt{attr} which would + then be applied to \texttt{(gc', th)}. + The source for parsing the attribute is the arguments part of \texttt{src}, + which must all be consumed by the parse. + + For example, for \texttt{Attrib.no\_args attr src}, the attribute parser + simply returns \texttt{attr}, requiring that the arguments part of + \texttt{src} must be empty. + + Some examples from \texttt{src/Pure/Isar/attrib.ML}, modified: + \begin{verbatim} + fun rot_att_n n (gc, th) = (gc, rotate_prems n th) ; + rot_att_n : int -> attribute ; + val rot_arg = Scan.lift (Scan.optional Args.int 1 : int atlp) : int cgatlp ; + val rotated_att : src -> attribute = + Attrib.syntax (rot_arg >> rot_att_n : attribute cgatlp) ; + + val THEN_arg : int cgatlp = Scan.lift + (Scan.optional (Args.bracks Args.nat : int atlp) 1 : int atlp) ; + + Attrib.thm : thm cgatlp ; + + THEN_arg -- Attrib.thm : (int * thm) cgatlp ; + + fun THEN_att_n (n, tht) (gc, th) = (gc, th RSN (n, tht)) ; + THEN_att_n : int * thm -> attribute ; + + val THEN_att : src -> attribute = Attrib.syntax + (THEN_arg -- Attrib.thm >> THEN_att_n : attribute cgatlp); + \end{verbatim} + The functions I've called \texttt{rot\_arg} and \texttt{THEN\_arg} + read an optional argument, which for \texttt{rotated} is an integer, + and for \texttt{THEN} is a natural enclosed in square brackets; + the default, if the argument is absent, is 1 in each case. + Functions \texttt{rot\_att\_n} and \texttt{THEN\_att\_n} turn these into + attributes, where \texttt{THEN\_att\_n} also requires a theorem, which is + parsed by \texttt{Attrib.thm}. + Infix operators \texttt{--} and \texttt{>>} are in the structure \texttt{Scan}. + +*} + +section{* Methods, and the \texttt{Method} structure *} + +text {* + The source file is \texttt{src/Pure/Isar/method.ML}. + The type \texttt{method} is defined by the datatype declaration + \begin{verbatim} + (* datatype method = Meth of thm list -> cases_tactic; *) + RuleCases.NO_CASES : tactic -> cases_tactic ; + \end{verbatim} + In fact \texttt{RAW\_METHOD\_CASES} (below) is exactly the constructor + \texttt{Meth}. + A \texttt{cases\_tactic} is an elaborated version of a tactic. + \texttt{NO\_CASES tac} is a \texttt{cases\_tactic} which consists of a + \texttt{cases\_tactic} without any further case information. + For further details see the description of structure \texttt{RuleCases} below. + The list of theorems to be passed to a method consists of the current + \emph{facts} in the proof. + + \begin{verbatim} + RAW_METHOD : (thm list -> tactic) -> method ; + METHOD : (thm list -> tactic) -> method ; + + SIMPLE_METHOD : tactic -> method ; + SIMPLE_METHOD' : (int -> tactic) -> method ; + SIMPLE_METHOD'' : ((int -> tactic) -> tactic) -> (int -> tactic) -> method ; + + RAW_METHOD_CASES : (thm list -> cases_tactic) -> method ; + METHOD_CASES : (thm list -> cases_tactic) -> method ; + \end{verbatim} + A method is, in its simplest form, a tactic; applying the method is to apply + the tactic to the current goal state. + + Applying \texttt{RAW\_METHOD tacf} creates a tactic by applying + \texttt{tacf} to the current {facts}, and applying that tactic to the + goal state. + + \texttt{METHOD} is similar but also first applies + \texttt{Goal.conjunction\_tac} to all subgoals. + + \texttt{SIMPLE\_METHOD tac} inserts the facts into all subgoals and then + applies \texttt{tacf}. + + \texttt{SIMPLE\_METHOD' tacf} inserts the facts and then + applies \texttt{tacf} to subgoal 1. + + \texttt{SIMPLE\_METHOD'' quant tacf} does this for subgoal(s) selected by + \texttt{quant}, which may be, for example, + \texttt{ALLGOALS} (all subgoals), + \texttt{TRYALL} (try all subgoals, failure is OK), + \texttt{FIRSTGOAL} (try subgoals until it succeeds once), + \texttt{(fn tacf => tacf 4)} (subgoal 4), etc + (see the \texttt{Tactical} structure, \cite[Chapter 4]{ref}). + + A method is stored in a theory as indicated by: + \begin{verbatim} + Method.add_method : + (bstring * (src -> Proof.context -> method) * string) -> theory trf ; + ( * + * ) + \end{verbatim} + where the first and third arguments are name and description of the method, + and the second is a function which parses the method input text + (including the method name, which has necessarily already been parsed). + + Here, \texttt{xxx} is a function declared in the code for the + structure \texttt{Method}, but not published in its signature. + The source file \texttt{src/Pure/Isar/method.ML} shows the use of + \texttt{Method.add\_method} to add a number of methods. + + +*} + + +end \ No newline at end of file diff -r cd861a121f60 -r 2a69b119cdee CookBook/ROOT.ML --- a/CookBook/ROOT.ML Fri Sep 05 09:49:51 2008 +0200 +++ b/CookBook/ROOT.ML Sat Sep 06 04:32:18 2008 +0200 @@ -2,5 +2,5 @@ use_thy "Intro"; use_thy "FirstSteps"; - +use_thy "Parsing"; use_thy "NamedThms"; diff -r cd861a121f60 -r 2a69b119cdee cookbook.pdf Binary file cookbook.pdf has changed