src/HOL/Tools/Function/fundef_common.ML
author wenzelm
Thu Jul 02 17:34:14 2009 +0200 (2009-07-02)
changeset 31902 862ae16a799d
parent 31775 2b04504fcb69
child 32603 e08fdd615333
permissions -rw-r--r--
renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;
     1 (*  Title:      HOL/Tools/Function/fundef_common.ML
     2     Author:     Alexander Krauss, TU Muenchen
     3 
     4 A package for general recursive function definitions. 
     5 Common definitions and other infrastructure.
     6 *)
     7 
     8 structure FundefCommon =
     9 struct
    10 
    11 local open FundefLib in
    12 
    13 (* Profiling *)
    14 val profile = ref false;
    15 
    16 fun PROFILE msg = if !profile then timeap_msg msg else I
    17 
    18 
    19 val acc_const_name = @{const_name "accp"}
    20 fun mk_acc domT R =
    21     Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
    22 
    23 val function_name = suffix "C"
    24 val graph_name = suffix "_graph"
    25 val rel_name = suffix "_rel"
    26 val dom_name = suffix "_dom"
    27 
    28 (* Termination rules *)
    29 
    30 structure TerminationRule = GenericDataFun
    31 (
    32   type T = thm list
    33   val empty = []
    34   val extend = I
    35   fun merge _ = Thm.merge_thms
    36 );
    37 
    38 val get_termination_rules = TerminationRule.get
    39 val store_termination_rule = TerminationRule.map o cons
    40 val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
    41 
    42 
    43 (* Function definition result data *)
    44 
    45 datatype fundef_result =
    46   FundefResult of
    47      {
    48       fs: term list,
    49       G: term,
    50       R: term,
    51 
    52       psimps : thm list, 
    53       trsimps : thm list option, 
    54 
    55       simple_pinducts : thm list, 
    56       cases : thm,
    57       termination : thm,
    58       domintros : thm list option
    59      }
    60 
    61 
    62 datatype fundef_context_data =
    63   FundefCtxData of
    64      {
    65       defname : string,
    66 
    67       (* contains no logical entities: invariant under morphisms *)
    68       add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list 
    69                   -> local_theory -> thm list * local_theory,
    70       case_names : string list,
    71 
    72       fs : term list,
    73       R : term,
    74       
    75       psimps: thm list,
    76       pinducts: thm list,
    77       termination: thm
    78      }
    79 
    80 fun morph_fundef_data (FundefCtxData {add_simps, case_names, fs, R, 
    81                                       psimps, pinducts, termination, defname}) phi =
    82     let
    83       val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
    84       val name = Binding.name_of o Morphism.binding phi o Binding.name
    85     in
    86       FundefCtxData { add_simps = add_simps, case_names = case_names,
    87                       fs = map term fs, R = term R, psimps = fact psimps, 
    88                       pinducts = fact pinducts, termination = thm termination,
    89                       defname = name defname }
    90     end
    91 
    92 structure FundefData = GenericDataFun
    93 (
    94   type T = (term * fundef_context_data) Item_Net.T;
    95   val empty = Item_Net.init
    96     (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
    97     fst;
    98   val copy = I;
    99   val extend = I;
   100   fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
   101 );
   102 
   103 val get_fundef = FundefData.get o Context.Proof;
   104 
   105 
   106 (* Generally useful?? *)
   107 fun lift_morphism thy f = 
   108     let 
   109       val term = Drule.term_rule thy f
   110     in
   111       Morphism.thm_morphism f $> Morphism.term_morphism term 
   112        $> Morphism.typ_morphism (Logic.type_map term)
   113     end
   114 
   115 fun import_fundef_data t ctxt =
   116     let
   117       val thy = ProofContext.theory_of ctxt
   118       val ct = cterm_of thy t
   119       val inst_morph = lift_morphism thy o Thm.instantiate 
   120 
   121       fun match (trm, data) = 
   122           SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
   123           handle Pattern.MATCH => NONE
   124     in 
   125       get_first match (Item_Net.retrieve (get_fundef ctxt) t)
   126     end
   127 
   128 fun import_last_fundef ctxt =
   129     case Item_Net.content (get_fundef ctxt) of
   130       [] => NONE
   131     | (t, data) :: _ =>
   132       let 
   133         val ([t'], ctxt') = Variable.import_terms true [t] ctxt
   134       in
   135         import_fundef_data t' ctxt'
   136       end
   137 
   138 val all_fundef_data = Item_Net.content o get_fundef
   139 
   140 fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) =
   141     FundefData.map (fold (fn f => Item_Net.insert (f, data)) fs)
   142     #> store_termination_rule termination
   143 
   144 
   145 (* Simp rules for termination proofs *)
   146 
   147 structure Termination_Simps = Named_Thms
   148 (
   149   val name = "termination_simp" 
   150   val description = "Simplification rule for termination proofs"
   151 );
   152 
   153 
   154 (* Default Termination Prover *)
   155 
   156 structure TerminationProver = GenericDataFun
   157 (
   158   type T = Proof.context -> Proof.method
   159   val empty = (fn _ => error "Termination prover not configured")
   160   val extend = I
   161   fun merge _ (a,b) = b (* FIXME *)
   162 );
   163 
   164 val set_termination_prover = TerminationProver.put
   165 val get_termination_prover = TerminationProver.get o Context.Proof
   166 
   167 
   168 (* Configuration management *)
   169 datatype fundef_opt 
   170   = Sequential
   171   | Default of string
   172   | DomIntros
   173   | Tailrec
   174 
   175 datatype fundef_config
   176   = FundefConfig of
   177    {
   178     sequential: bool,
   179     default: string,
   180     domintros: bool,
   181     tailrec: bool
   182    }
   183 
   184 fun apply_opt Sequential (FundefConfig {sequential, default, domintros,tailrec}) = 
   185     FundefConfig {sequential=true, default=default, domintros=domintros, tailrec=tailrec}
   186   | apply_opt (Default d) (FundefConfig {sequential, default, domintros,tailrec}) = 
   187     FundefConfig {sequential=sequential, default=d, domintros=domintros, tailrec=tailrec}
   188   | apply_opt DomIntros (FundefConfig {sequential, default, domintros,tailrec}) =
   189     FundefConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec}
   190   | apply_opt Tailrec (FundefConfig {sequential, default, domintros,tailrec}) =
   191     FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
   192 
   193 val default_config =
   194   FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), 
   195                  domintros=false, tailrec=false }
   196 
   197 
   198 (* Analyzing function equations *)
   199 
   200 fun split_def ctxt geq =
   201     let
   202       fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
   203       val qs = Term.strip_qnt_vars "all" geq
   204       val imp = Term.strip_qnt_body "all" geq
   205       val (gs, eq) = Logic.strip_horn imp
   206 
   207       val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
   208           handle TERM _ => error (input_error "Not an equation")
   209 
   210       val (head, args) = strip_comb f_args
   211 
   212       val fname = fst (dest_Free head)
   213           handle TERM _ => error (input_error "Head symbol must not be a bound variable")
   214     in
   215       (fname, qs, gs, args, rhs)
   216     end
   217 
   218 (* Check for all sorts of errors in the input *)
   219 fun check_defs ctxt fixes eqs =
   220     let
   221       val fnames = map (fst o fst) fixes
   222                                 
   223       fun check geq = 
   224           let
   225             fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
   226                                   
   227             val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
   228                                  
   229             val _ = fname mem fnames 
   230                     orelse input_error 
   231                              ("Head symbol of left hand side must be " 
   232                               ^ plural "" "one out of " fnames ^ commas_quote fnames)
   233                                             
   234             val _ = length args > 0 orelse input_error "Function has no arguments:"
   235 
   236             fun add_bvs t is = add_loose_bnos (t, 0, is)
   237             val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
   238                         |> map (fst o nth (rev qs))
   239                       
   240             val _ = null rvs orelse input_error 
   241                         ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
   242                          ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
   243                                     
   244             val _ = forall (not o Term.exists_subterm 
   245                              (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
   246                     orelse input_error "Defined function may not occur in premises or arguments"
   247 
   248             val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
   249             val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
   250             val _ = null funvars
   251                     orelse (warning (cat_lines 
   252                     ["Bound variable" ^ plural " " "s " funvars 
   253                      ^ commas_quote (map fst funvars) ^  
   254                      " occur" ^ plural "s" "" funvars ^ " in function position.",  
   255                      "Misspelled constructor???"]); true)
   256           in
   257             (fname, length args)
   258           end
   259 
   260       val _ = AList.group (op =) (map check eqs)
   261         |> map (fn (fname, ars) =>
   262              length (distinct (op =) ars) = 1
   263              orelse error ("Function " ^ quote fname ^
   264                            " has different numbers of arguments in different equations"))
   265 
   266       fun check_sorts ((fname, fT), _) =
   267           Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
   268           orelse error (cat_lines 
   269           ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
   270            setmp show_sorts true (Syntax.string_of_typ ctxt) fT])
   271 
   272       val _ = map check_sorts fixes
   273     in
   274       ()
   275     end
   276 
   277 (* Preprocessors *)
   278 
   279 type fixes = ((string * typ) * mixfix) list
   280 type 'a spec = (Attrib.binding * 'a list) list
   281 type preproc = fundef_config -> Proof.context -> fixes -> term spec 
   282                -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
   283 
   284 val fname_of = fst o dest_Free o fst o strip_comb o fst 
   285  o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
   286 
   287 fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
   288   | mk_case_names _ n 0 = []
   289   | mk_case_names _ n 1 = [n]
   290   | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
   291 
   292 fun empty_preproc check _ ctxt fixes spec =
   293     let 
   294       val (bnds, tss) = split_list spec
   295       val ts = flat tss
   296       val _ = check ctxt fixes ts
   297       val fnames = map (fst o fst) fixes
   298       val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
   299 
   300       fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
   301                                    (indices ~~ xs)
   302                         |> map (map snd)
   303 
   304       (* using theorem names for case name currently disabled *)
   305       val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
   306     in
   307       (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
   308     end
   309 
   310 structure Preprocessor = GenericDataFun
   311 (
   312   type T = preproc
   313   val empty : T = empty_preproc check_defs
   314   val extend = I
   315   fun merge _ (a, _) = a
   316 );
   317 
   318 val get_preproc = Preprocessor.get o Context.Proof
   319 val set_preproc = Preprocessor.map o K
   320 
   321 
   322 
   323 local 
   324   structure P = OuterParse and K = OuterKeyword
   325 
   326   val option_parser = 
   327       P.group "option" ((P.reserved "sequential" >> K Sequential)
   328                     || ((P.reserved "default" |-- P.term) >> Default)
   329                     || (P.reserved "domintros" >> K DomIntros)
   330                     || (P.reserved "tailrec" >> K Tailrec))
   331 
   332   fun config_parser default = 
   333       (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
   334         >> (fn opts => fold apply_opt opts default)
   335 in
   336   fun fundef_parser default_cfg = 
   337       config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
   338 end
   339 
   340 
   341 end
   342 end
   343