src/HOL/Tools/Function/function_common.ML
author wenzelm
Fri Dec 13 20:20:15 2013 +0100 (2013-12-13)
changeset 54740 91f54d386680
parent 54295 45a5523d4a63
child 56245 84fc7dfa3cd4
permissions -rw-r--r--
maintain morphism names for diagnostic purposes;
     1 (*  Title:      HOL/Tools/Function/function_common.ML
     2     Author:     Alexander Krauss, TU Muenchen
     3 
     4 Common definitions and other infrastructure for the function package.
     5 *)
     6 
     7 signature FUNCTION_DATA =
     8 sig
     9 
    10 type info =
    11  {is_partial : bool,
    12   defname : string,
    13     (* contains no logical entities: invariant under morphisms: *)
    14   add_simps : (binding -> binding) -> string -> (binding -> binding) ->
    15     Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
    16   fnames : string list,
    17   case_names : string list,
    18   fs : term list,
    19   R : term,
    20   dom: term,
    21   psimps: thm list,
    22   pinducts: thm list,
    23   simps : thm list option,
    24   inducts : thm list option,
    25   termination : thm,
    26   cases : thm list,
    27   pelims: thm list list,
    28   elims: thm list list option}
    29 
    30 end
    31 
    32 structure Function_Data : FUNCTION_DATA =
    33 struct
    34 
    35 type info =
    36  {is_partial : bool,
    37   defname : string,
    38     (* contains no logical entities: invariant under morphisms: *)
    39   add_simps : (binding -> binding) -> string -> (binding -> binding) ->
    40     Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
    41   fnames : string list,
    42   case_names : string list,
    43   fs : term list,
    44   R : term,
    45   dom: term,
    46   psimps: thm list,
    47   pinducts: thm list,
    48   simps : thm list option,
    49   inducts : thm list option,
    50   termination : thm,
    51   cases : thm list,
    52   pelims : thm list list,
    53   elims : thm list list option}
    54 
    55 end
    56 
    57 signature FUNCTION_COMMON =
    58 sig
    59   include FUNCTION_DATA
    60   val profile : bool Unsynchronized.ref
    61   val PROFILE : string -> ('a -> 'b) -> 'a -> 'b
    62   val mk_acc : typ -> term -> term
    63   val function_name : string -> string
    64   val graph_name : string -> string
    65   val rel_name : string -> string
    66   val dom_name : string -> string
    67   val apply_termination_rule : Proof.context -> int -> tactic
    68   datatype function_result = FunctionResult of
    69    {fs: term list,
    70     G: term,
    71     R: term,
    72     dom: term,
    73     psimps : thm list,
    74     simple_pinducts : thm list,
    75     cases : thm list,
    76     pelims : thm list list,
    77     termination : thm,
    78     domintros : thm list option}
    79   val transform_function_data : info -> morphism -> info
    80   val get_function : Proof.context -> (term * info) Item_Net.T
    81   val import_function_data : term -> Proof.context -> info option
    82   val import_last_function : Proof.context -> info option
    83   val add_function_data : info -> Context.generic -> Context.generic
    84   structure Termination_Simps: NAMED_THMS
    85   val set_termination_prover : (Proof.context -> tactic) -> Context.generic -> Context.generic
    86   val get_termination_prover : Proof.context -> tactic
    87   val store_termination_rule : thm -> Context.generic -> Context.generic
    88   datatype function_config = FunctionConfig of
    89    {sequential: bool,
    90     default: string option,
    91     domintros: bool,
    92     partials: bool}
    93   val default_config : function_config
    94   val split_def : Proof.context -> (string -> 'a) -> term ->
    95     string * (string * typ) list * term list * term list * term
    96   val check_defs : Proof.context -> ((string * typ) * 'a) list -> term list -> unit
    97   type fixes = ((string * typ) * mixfix) list
    98   type 'a spec = (Attrib.binding * 'a list) list
    99   type preproc = function_config -> Proof.context -> fixes -> term spec ->
   100     (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
   101   val fname_of : term -> string
   102   val mk_case_names : int -> string -> int -> string list
   103   val empty_preproc : (Proof.context -> ((string * typ) * mixfix) list -> term list -> 'c) -> preproc
   104   val get_preproc: Proof.context -> preproc
   105   val set_preproc: preproc -> Context.generic -> Context.generic
   106   val function_parser : function_config ->
   107     ((function_config * (binding * string option * mixfix) list) * (Attrib.binding * string) list) parser
   108 end
   109 
   110 structure Function_Common : FUNCTION_COMMON =
   111 struct
   112 
   113 open Function_Data
   114 
   115 local open Function_Lib in
   116 
   117 (* Profiling *)
   118 val profile = Unsynchronized.ref false;
   119 
   120 fun PROFILE msg = if !profile then timeap_msg msg else I
   121 
   122 val acc_const_name = @{const_name Wellfounded.accp}
   123 fun mk_acc domT R =
   124   Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
   125 
   126 val function_name = suffix "C"
   127 val graph_name = suffix "_graph"
   128 val rel_name = suffix "_rel"
   129 val dom_name = suffix "_dom"
   130 
   131 (* Termination rules *)
   132 
   133 (* FIXME just one data slot (record) per program unit *)
   134 structure TerminationRule = Generic_Data
   135 (
   136   type T = thm list
   137   val empty = []
   138   val extend = I
   139   val merge = Thm.merge_thms
   140 );
   141 
   142 val get_termination_rules = TerminationRule.get
   143 val store_termination_rule = TerminationRule.map o cons
   144 val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
   145 
   146 
   147 (* Function definition result data *)
   148 
   149 datatype function_result = FunctionResult of
   150  {fs: term list,
   151   G: term,
   152   R: term,
   153   dom: term,
   154   psimps : thm list,
   155   simple_pinducts : thm list,
   156   cases : thm list,
   157   pelims : thm list list,
   158   termination : thm,
   159   domintros : thm list option}
   160 
   161 fun transform_function_data ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
   162   simps, inducts, termination, defname, is_partial, cases, pelims, elims} : info) phi =
   163     let
   164       val term = Morphism.term phi
   165       val thm = Morphism.thm phi
   166       val fact = Morphism.fact phi
   167       val name = Binding.name_of o Morphism.binding phi o Binding.name
   168     in
   169       { add_simps = add_simps, case_names = case_names, fnames = fnames,
   170         fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
   171         pinducts = fact pinducts, simps = Option.map fact simps,
   172         inducts = Option.map fact inducts, termination = thm termination,
   173         defname = name defname, is_partial=is_partial, cases = fact cases,
   174         elims = Option.map (map fact) elims, pelims = map fact pelims }
   175     end
   176 
   177 (* FIXME just one data slot (record) per program unit *)
   178 structure FunctionData = Generic_Data
   179 (
   180   type T = (term * info) Item_Net.T;
   181   val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
   182   val extend = I;
   183   fun merge tabs : T = Item_Net.merge tabs;
   184 )
   185 
   186 val get_function = FunctionData.get o Context.Proof;
   187 
   188 fun lift_morphism thy f =
   189   let
   190     fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
   191   in
   192     Morphism.morphism "lift_morphism"
   193       {binding = [],
   194        typ = [Logic.type_map term],
   195        term = [term],
   196        fact = [map f]}
   197   end
   198 
   199 fun import_function_data t ctxt =
   200   let
   201     val thy = Proof_Context.theory_of ctxt
   202     val ct = cterm_of thy t
   203     val inst_morph = lift_morphism thy o Thm.instantiate
   204 
   205     fun match (trm, data) =
   206       SOME (transform_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
   207       handle Pattern.MATCH => NONE
   208   in
   209     get_first match (Item_Net.retrieve (get_function ctxt) t)
   210   end
   211 
   212 fun import_last_function ctxt =
   213   case Item_Net.content (get_function ctxt) of
   214     [] => NONE
   215   | (t, _) :: _ =>
   216     let
   217       val ([t'], ctxt') = Variable.import_terms true [t] ctxt
   218     in
   219       import_function_data t' ctxt'
   220     end
   221 
   222 fun add_function_data (data : info as {fs, termination, ...}) =
   223   FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
   224   #> store_termination_rule termination
   225 
   226 
   227 (* Simp rules for termination proofs *)
   228 
   229 structure Termination_Simps = Named_Thms
   230 (
   231   val name = @{binding termination_simp}
   232   val description = "simplification rules for termination proofs"
   233 )
   234 
   235 
   236 (* Default Termination Prover *)
   237 
   238 (* FIXME just one data slot (record) per program unit *)
   239 structure TerminationProver = Generic_Data
   240 (
   241   type T = Proof.context -> tactic
   242   val empty = (fn _ => error "Termination prover not configured")
   243   val extend = I
   244   fun merge (a, _) = a
   245 )
   246 
   247 val set_termination_prover = TerminationProver.put
   248 fun get_termination_prover ctxt = TerminationProver.get (Context.Proof ctxt) ctxt
   249 
   250 
   251 (* Configuration management *)
   252 datatype function_opt
   253   = Sequential
   254   | Default of string
   255   | DomIntros
   256   | No_Partials
   257 
   258 datatype function_config = FunctionConfig of
   259  {sequential: bool,
   260   default: string option,
   261   domintros: bool,
   262   partials: bool}
   263 
   264 fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials}) =
   265     FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials}
   266   | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials}) =
   267     FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials}
   268   | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials}) =
   269     FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials}
   270   | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials}) =
   271     FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false}
   272 
   273 val default_config =
   274   FunctionConfig { sequential=false, default=NONE,
   275     domintros=false, partials=true}
   276 
   277 
   278 (* Analyzing function equations *)
   279 
   280 fun split_def ctxt check_head geq =
   281   let
   282     fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
   283     val qs = Term.strip_qnt_vars "all" geq
   284     val imp = Term.strip_qnt_body "all" geq
   285     val (gs, eq) = Logic.strip_horn imp
   286 
   287     val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
   288       handle TERM _ => error (input_error "Not an equation")
   289 
   290     val (head, args) = strip_comb f_args
   291 
   292     val fname = fst (dest_Free head) handle TERM _ => ""
   293     val _ = check_head fname
   294   in
   295     (fname, qs, gs, args, rhs)
   296   end
   297 
   298 (* Check for all sorts of errors in the input *)
   299 fun check_defs ctxt fixes eqs =
   300   let
   301     val fnames = map (fst o fst) fixes
   302 
   303     fun check geq =
   304       let
   305         fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
   306 
   307         fun check_head fname =
   308           member (op =) fnames fname orelse
   309           input_error ("Illegal equation head. Expected " ^ commas_quote fnames)
   310 
   311         val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq
   312 
   313         val _ = length args > 0 orelse input_error "Function has no arguments:"
   314 
   315         fun add_bvs t is = add_loose_bnos (t, 0, is)
   316         val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
   317                     |> map (fst o nth (rev qs))
   318 
   319         val _ = null rvs orelse input_error
   320           ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^
   321            " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
   322 
   323         val _ = forall (not o Term.exists_subterm
   324           (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args)
   325           orelse input_error "Defined function may not occur in premises or arguments"
   326 
   327         val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
   328         val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
   329         val _ = null funvars orelse (warning (cat_lines
   330           ["Bound variable" ^ plural " " "s " funvars ^
   331           commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^
   332           " in function position.", "Misspelled constructor???"]); true)
   333       in
   334         (fname, length args)
   335       end
   336 
   337     val grouped_args = AList.group (op =) (map check eqs)
   338     val _ = grouped_args
   339       |> map (fn (fname, ars) =>
   340         length (distinct (op =) ars) = 1
   341         orelse error ("Function " ^ quote fname ^
   342           " has different numbers of arguments in different equations"))
   343 
   344     val not_defined = subtract (op =) (map fst grouped_args) fnames
   345     val _ = null not_defined
   346       orelse error ("No defining equations for function" ^
   347         plural " " "s " not_defined ^ commas_quote not_defined)
   348 
   349     fun check_sorts ((fname, fT), _) =
   350       Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS)
   351       orelse error (cat_lines
   352       ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
   353        Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
   354 
   355     val _ = map check_sorts fixes
   356   in
   357     ()
   358   end
   359 
   360 (* Preprocessors *)
   361 
   362 type fixes = ((string * typ) * mixfix) list
   363 type 'a spec = (Attrib.binding * 'a list) list
   364 type preproc = function_config -> Proof.context -> fixes -> term spec ->
   365   (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
   366 
   367 val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o
   368   HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
   369 
   370 fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
   371   | mk_case_names _ n 0 = []
   372   | mk_case_names _ n 1 = [n]
   373   | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
   374 
   375 fun empty_preproc check (_: function_config) (ctxt: Proof.context) (fixes: fixes) spec =
   376   let
   377     val (bnds, tss) = split_list spec
   378     val ts = flat tss
   379     val _ = check ctxt fixes ts
   380     val fnames = map (fst o fst) fixes
   381     val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
   382 
   383     fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
   384       (indices ~~ xs) |> map (map snd)
   385 
   386     (* using theorem names for case name currently disabled *)
   387     val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
   388   in
   389     (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
   390   end
   391 
   392 (* FIXME just one data slot (record) per program unit *)
   393 structure Preprocessor = Generic_Data
   394 (
   395   type T = preproc
   396   val empty : T = empty_preproc check_defs
   397   val extend = I
   398   fun merge (a, _) = a
   399 )
   400 
   401 val get_preproc = Preprocessor.get o Context.Proof
   402 val set_preproc = Preprocessor.map o K
   403 
   404 
   405 
   406 local
   407   val option_parser = Parse.group (fn () => "option")
   408     ((Parse.reserved "sequential" >> K Sequential)
   409      || ((Parse.reserved "default" |-- Parse.term) >> Default)
   410      || (Parse.reserved "domintros" >> K DomIntros)
   411      || (Parse.reserved "no_partials" >> K No_Partials))
   412 
   413   fun config_parser default =
   414     (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) [])
   415      >> (fn opts => fold apply_opt opts default)
   416 in
   417   fun function_parser default_cfg =
   418       config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
   419 end
   420 
   421 
   422 end
   423 end