1.1 --- a/src/HOL/Tools/Function/function.ML	Sat Jan 02 23:18:58 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/function.ML	Sat Jan 02 23:18:58 2010 +0100
     1.3 @@ -7,6 +7,8 @@
     1.4  
     1.5  signature FUNCTION =
     1.6  sig
     1.7 +    include FUNCTION_DATA
     1.8 +
     1.9      val add_function :  (binding * typ option * mixfix) list
    1.10                         -> (Attrib.binding * term) list
    1.11                         -> Function_Common.function_config
    1.12 @@ -23,6 +25,8 @@
    1.13  
    1.14      val setup : theory -> theory
    1.15      val get_congs : Proof.context -> thm list
    1.16 +
    1.17 +    val get_info : Proof.context -> term -> info
    1.18  end
    1.19  
    1.20  
    1.21 @@ -105,15 +109,16 @@
    1.22                     [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
    1.23              ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros
    1.24  
    1.25 -          val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
    1.26 -                                      pinducts=snd pinducts', termination=termination',
    1.27 -                                      fs=fs, R=R, defname=defname }
    1.28 +          val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
    1.29 +            pinducts=snd pinducts', termination=termination', fs=fs, R=R,
    1.30 +            defname=defname, is_partial=true }
    1.31 +
    1.32            val _ =
    1.33              if not is_external then ()
    1.34              else Specification.print_consts lthy (K false) (map fst fixes)
    1.35          in
    1.36            lthy
    1.37 -          |> Local_Theory.declaration false (add_function_data o morph_function_data cdata)
    1.38 +          |> Local_Theory.declaration false (add_function_data o morph_function_data info)
    1.39          end
    1.40      in
    1.41        lthy
    1.42 @@ -127,14 +132,14 @@
    1.43  fun gen_termination_proof prep_term raw_term_opt lthy =
    1.44      let
    1.45        val term_opt = Option.map (prep_term lthy) raw_term_opt
    1.46 -      val data = the (case term_opt of
    1.47 +      val info = the (case term_opt of
    1.48                          SOME t => (import_function_data t lthy
    1.49                            handle Option.Option =>
    1.50                              error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
    1.51                        | NONE => (import_last_function lthy handle Option.Option => error "Not a function"))
    1.52  
    1.53 -        val FunctionCtxData { termination, R, add_simps, case_names, psimps,
    1.54 -                            pinducts, defname, ...} = data
    1.55 +        val { termination, fs, R, add_simps, case_names, psimps,
    1.56 +          pinducts, defname, ...} = info
    1.57          val domT = domain_type (fastype_of R)
    1.58          val goal = HOLogic.mk_Trueprop
    1.59                       (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
    1.60 @@ -145,6 +150,10 @@
    1.61                full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
    1.62              val tsimps = map remove_domain_condition psimps
    1.63              val tinduct = map remove_domain_condition pinducts
    1.64 +
    1.65 +            val info' = { is_partial=false, defname=defname, add_simps=add_simps,
    1.66 +              case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
    1.67 +              termination=termination }
    1.68              fun qualify n = Binding.name n
    1.69                |> Binding.qualify true defname
    1.70            in
    1.71 @@ -154,6 +163,7 @@
    1.72                 ((qualify "induct",
    1.73                   [Attrib.internal (K (Rule_Cases.case_names case_names))]),
    1.74                  tinduct) |> snd
    1.75 +            |> Local_Theory.declaration false (add_function_data o morph_function_data info')
    1.76            end
    1.77      in
    1.78        lthy
    1.79 @@ -196,6 +206,8 @@
    1.80  
    1.81  val get_congs = Function_Ctx_Tree.get_function_congs
    1.82  
    1.83 +fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
    1.84 +  |> the_single |> snd
    1.85  
    1.86  (* outer syntax *)
    1.87  

     2.1 --- a/src/HOL/Tools/Function/function_common.ML	Sat Jan 02 23:18:58 2010 +0100
     2.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sat Jan 02 23:18:58 2010 +0100
     2.3 @@ -5,9 +5,49 @@
     2.4  Common definitions and other infrastructure.
     2.5  *)
     2.6  
     2.7 +signature FUNCTION_DATA =
     2.8 +sig
     2.9 +
    2.10 +type info =
    2.11 + {is_partial : bool,
    2.12 +  defname : string,
    2.13 +    (* contains no logical entities: invariant under morphisms: *)
    2.14 +  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
    2.15 +    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
    2.16 +  case_names : string list,
    2.17 +  fs : term list,
    2.18 +  R : term,
    2.19 +  psimps: thm list,
    2.20 +  pinducts: thm list,
    2.21 +  termination: thm
    2.22 + }  
    2.23 +
    2.24 +end
    2.25 +
    2.26 +structure Function_Data : FUNCTION_DATA =
    2.27 +struct
    2.28 +
    2.29 +type info =
    2.30 + {is_partial : bool,
    2.31 +  defname : string,
    2.32 +    (* contains no logical entities: invariant under morphisms: *)
    2.33 +  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
    2.34 +    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
    2.35 +  case_names : string list,
    2.36 +  fs : term list,
    2.37 +  R : term,
    2.38 +  psimps: thm list,
    2.39 +  pinducts: thm list,
    2.40 +  termination: thm
    2.41 + }  
    2.42 +
    2.43 +end
    2.44 +
    2.45  structure Function_Common =
    2.46  struct
    2.47  
    2.48 +open Function_Data
    2.49 +
    2.50  local open Function_Lib in
    2.51  
    2.52  (* Profiling *)
    2.53 @@ -58,41 +98,21 @@
    2.54        domintros : thm list option
    2.55       }
    2.56  
    2.57 -
    2.58 -datatype function_context_data =
    2.59 -  FunctionCtxData of
    2.60 -     {
    2.61 -      defname : string,
    2.62 -
    2.63 -      (* contains no logical entities: invariant under morphisms *)
    2.64 -      add_simps : (binding -> binding) -> string -> (binding -> binding) ->
    2.65 -        Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
    2.66 -
    2.67 -      case_names : string list,
    2.68 -
    2.69 -      fs : term list,
    2.70 -      R : term,
    2.71 -      
    2.72 -      psimps: thm list,
    2.73 -      pinducts: thm list,
    2.74 -      termination: thm
    2.75 -     }
    2.76 -
    2.77 -fun morph_function_data (FunctionCtxData {add_simps, case_names, fs, R, 
    2.78 -                                      psimps, pinducts, termination, defname}) phi =
    2.79 +fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
    2.80 +  termination, defname, is_partial} : info) phi =
    2.81      let
    2.82        val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
    2.83        val name = Binding.name_of o Morphism.binding phi o Binding.name
    2.84      in
    2.85 -      FunctionCtxData { add_simps = add_simps, case_names = case_names,
    2.86 -                      fs = map term fs, R = term R, psimps = fact psimps, 
    2.87 -                      pinducts = fact pinducts, termination = thm termination,
    2.88 -                      defname = name defname }
    2.89 +      { add_simps = add_simps, case_names = case_names,
    2.90 +        fs = map term fs, R = term R, psimps = fact psimps, 
    2.91 +        pinducts = fact pinducts, termination = thm termination,
    2.92 +        defname = name defname, is_partial=is_partial }
    2.93      end
    2.94  
    2.95  structure FunctionData = Generic_Data
    2.96  (
    2.97 -  type T = (term * function_context_data) Item_Net.T;
    2.98 +  type T = (term * info) Item_Net.T;
    2.99    val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
   2.100    val extend = I;
   2.101    fun merge tabs : T = Item_Net.merge tabs;
   2.102 @@ -135,7 +155,7 @@
   2.103  
   2.104  val all_function_data = Item_Net.content o get_function
   2.105  
   2.106 -fun add_function_data (data as FunctionCtxData {fs, termination, ...}) =
   2.107 +fun add_function_data (data : info as {fs, termination, ...}) =
   2.108      FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
   2.109      #> store_termination_rule termination
   2.110