removed obsolete name convention "func"
authorhaftmann
Fri Sep 26 09:10:02 2008 +0200 (2008-09-26)
changeset 2837037f56e6e702d
parent 28369 196bd0305c0d
child 28371 471a356fdea9
removed obsolete name convention "func"
src/HOL/Code_Eval.thy
src/HOL/List.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/ex/Quickcheck.thy
src/Pure/Isar/constdefs.ML
src/Pure/Isar/specification.ML
src/Pure/Proof/extraction.ML
src/Tools/code/code_funcgr.ML
     1.1 --- a/src/HOL/Code_Eval.thy	Fri Sep 26 09:09:53 2008 +0200
     1.2 +++ b/src/HOL/Code_Eval.thy	Fri Sep 26 09:10:02 2008 +0200
     1.3 @@ -109,7 +109,7 @@
     1.4          |> Thm.varifyT;
     1.5      in
     1.6        thy
     1.7 -      |> Code.add_func thm
     1.8 +      |> Code.add_eqn thm
     1.9      end;
    1.10    fun interpretator (tyco, (raw_vs, raw_cs)) thy =
    1.11      let
    1.12 @@ -123,7 +123,7 @@
    1.13        val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    1.14      in
    1.15        thy
    1.16 -      |> Code.del_funcs const
    1.17 +      |> Code.del_eqns const
    1.18        |> fold (prove_term_of_eq ty) eqs
    1.19      end;
    1.20  in
     2.1 --- a/src/HOL/List.thy	Fri Sep 26 09:09:53 2008 +0200
     2.2 +++ b/src/HOL/List.thy	Fri Sep 26 09:10:02 2008 +0200
     2.3 @@ -3389,7 +3389,7 @@
     2.4        nibbles nibbles;
     2.5  in
     2.6    PureThy.note_thmss Thm.lemmaK [((Name.binding "nibble_pair_of_char_simps", []), [(thms, [])])]
     2.7 -  #-> (fn [(_, thms)] => fold_rev Code.add_func thms)
     2.8 +  #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
     2.9  end
    2.10  *}
    2.11  
     3.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Sep 26 09:09:53 2008 +0200
     3.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Sep 26 09:10:02 2008 +0200
     3.3 @@ -364,7 +364,7 @@
     3.4    in
     3.5      thy
     3.6      |> Code.add_case certs
     3.7 -    |> fold_rev Code.add_default_func case_rewrites
     3.8 +    |> fold_rev Code.add_default_eqn case_rewrites
     3.9    end;
    3.10  
    3.11  
    3.12 @@ -464,7 +464,7 @@
    3.13          fun get_thms () = (eq_refl, false)
    3.14            :: rev (map (rpair true) (get_eq' (Theory.deref thy_ref) dtco));
    3.15        in
    3.16 -        Code.add_funcl (const, Susp.delay get_thms) thy
    3.17 +        Code.add_eqnl (const, Susp.delay get_thms) thy
    3.18        end;
    3.19    in
    3.20      thy
    3.21 @@ -473,7 +473,7 @@
    3.22      |-> (fn thms => Class.prove_instantiation_instance (K (tac thms))
    3.23      #> LocalTheory.exit
    3.24      #> ProofContext.theory_of
    3.25 -    #> fold Code.del_func thms
    3.26 +    #> fold Code.del_eqn thms
    3.27      #> fold add_eq_thms dtcos)
    3.28    end;
    3.29  
     4.1 --- a/src/HOL/Tools/function_package/size.ML	Fri Sep 26 09:09:53 2008 +0200
     4.2 +++ b/src/HOL/Tools/function_package/size.ML	Fri Sep 26 09:10:02 2008 +0200
     4.3 @@ -212,7 +212,7 @@
     4.4      val ([size_thms], thy'') =  PureThy.add_thmss
     4.5        [(("size", size_eqns),
     4.6          [Simplifier.simp_add, Thm.declaration_attribute
     4.7 -              (fn thm => Context.mapping (Code.add_default_func thm) I)])] thy'
     4.8 +              (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
     4.9  
    4.10    in
    4.11      SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
     5.1 --- a/src/HOL/Tools/recfun_codegen.ML	Fri Sep 26 09:09:53 2008 +0200
     5.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Fri Sep 26 09:10:02 2008 +0200
     5.3 @@ -42,10 +42,10 @@
     5.4    handle TERM _ => tap (fn _ => warn thm);
     5.5  
     5.6  fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
     5.7 -  (add_thm opt_module thm #> Code.add_liberal_func thm) I);
     5.8 +  (add_thm opt_module thm #> Code.add_liberal_eqn thm) I);
     5.9  
    5.10  val add_default = Thm.declaration_attribute (fn thm => Context.mapping
    5.11 -  (add_thm NONE thm #> Code.add_default_func thm) I);
    5.12 +  (add_thm NONE thm #> Code.add_default_eqn thm) I);
    5.13  
    5.14  fun del_thm thm = case try const_of (prop_of thm)
    5.15   of SOME (s, _) => RecCodegenData.map
    5.16 @@ -53,7 +53,7 @@
    5.17    | NONE => tap (fn _ => warn thm);
    5.18  
    5.19  val del = Thm.declaration_attribute
    5.20 -  (fn thm => Context.mapping (del_thm thm #> Code.del_func thm) I)
    5.21 +  (fn thm => Context.mapping (del_thm thm #> Code.del_eqn thm) I)
    5.22  
    5.23  fun del_redundant thy eqs [] = eqs
    5.24    | del_redundant thy eqs (eq :: eqs') =
     6.1 --- a/src/HOL/Tools/record_package.ML	Fri Sep 26 09:09:53 2008 +0200
     6.2 +++ b/src/HOL/Tools/record_package.ML	Fri Sep 26 09:10:02 2008 +0200
     6.3 @@ -1543,8 +1543,8 @@
     6.4        ||>> PureThy.add_defs false (map Thm.no_attributes (ext_spec::dest_specs))
     6.5        ||>> PureThy.add_defs false (map Thm.no_attributes upd_specs)
     6.6        |-> (fn args as ((_, dest_defs), upd_defs) =>
     6.7 -          fold Code.add_default_func dest_defs
     6.8 -          #> fold Code.add_default_func upd_defs
     6.9 +          fold Code.add_default_eqn dest_defs
    6.10 +          #> fold Code.add_default_eqn upd_defs
    6.11            #> pair args);
    6.12      val ((([abs_inject, abs_inverse, abs_induct], ext_def :: dest_defs), upd_defs), defs_thy) =
    6.13        timeit_msg "record extension type/selector/update defs:" mk_defs;
    6.14 @@ -1949,9 +1949,9 @@
    6.15        ||>> ((PureThy.add_defs false o map Thm.no_attributes)
    6.16               [make_spec, fields_spec, extend_spec, truncate_spec])
    6.17        |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
    6.18 -          fold Code.add_default_func sel_defs
    6.19 -          #> fold Code.add_default_func upd_defs
    6.20 -          #> fold Code.add_default_func derived_defs
    6.21 +          fold Code.add_default_eqn sel_defs
    6.22 +          #> fold Code.add_default_eqn upd_defs
    6.23 +          #> fold Code.add_default_eqn derived_defs
    6.24            #> pair defs)
    6.25      val (((sel_defs, upd_defs), derived_defs), defs_thy) =
    6.26        timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
     7.1 --- a/src/HOL/Tools/typecopy_package.ML	Fri Sep 26 09:09:53 2008 +0200
     7.2 +++ b/src/HOL/Tools/typecopy_package.ML	Fri Sep 26 09:10:02 2008 +0200
     7.3 @@ -151,19 +151,19 @@
     7.4                ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], []);
     7.5        in
     7.6          thy
     7.7 -        |> Code.add_func eq
     7.8 -        |> Code.add_nonlinear_func eq_refl
     7.9 +        |> Code.add_eqn eq
    7.10 +        |> Code.add_nonlinear_eqn eq_refl
    7.11        end;
    7.12    in
    7.13      thy
    7.14      |> Code.add_datatype [(constr, ty_constr)]
    7.15 -    |> Code.add_func proj_def
    7.16 +    |> Code.add_eqn proj_def
    7.17      |> TheoryTarget.instantiation ([tyco], vs', [HOLogic.class_eq])
    7.18      |> add_def tyco
    7.19      |-> (fn thm => Class.prove_instantiation_instance (K (tac [thm]))
    7.20      #> LocalTheory.exit
    7.21      #> ProofContext.theory_of
    7.22 -    #> Code.del_func thm
    7.23 +    #> Code.del_eqn thm
    7.24      #> add_eq_thms)
    7.25    end;
    7.26  
     8.1 --- a/src/HOL/ex/Quickcheck.thy	Fri Sep 26 09:09:53 2008 +0200
     8.2 +++ b/src/HOL/ex/Quickcheck.thy	Fri Sep 26 09:10:02 2008 +0200
     8.3 @@ -130,7 +130,7 @@
     8.4              (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>index"},
     8.5                 random' $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"})
     8.6            val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
     8.7 -            (fn thm => Context.mapping (Code.del_func thm) I));
     8.8 +            (fn thm => Context.mapping (Code.del_eqn thm) I));
     8.9            fun add_code simps lthy =
    8.10              let
    8.11                val thy = ProofContext.theory_of lthy;
    8.12 @@ -142,9 +142,9 @@
    8.13                  o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm;
    8.14              in
    8.15                lthy
    8.16 -              |> LocalTheory.theory (Code.del_funcs c
    8.17 +              |> LocalTheory.theory (Code.del_eqns c
    8.18                     #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
    8.19 -                   #-> Code.add_func)
    8.20 +                   #-> Code.add_eqn)
    8.21              end;
    8.22          in
    8.23            thy
     9.1 --- a/src/Pure/Isar/constdefs.ML	Fri Sep 26 09:09:53 2008 +0200
     9.2 +++ b/src/Pure/Isar/constdefs.ML	Fri Sep 26 09:10:02 2008 +0200
     9.3 @@ -54,7 +54,7 @@
     9.4        thy
     9.5        |> Sign.add_consts_i [(c, T, mx)]
     9.6        |> PureThy.add_defs false [((name, def), atts)]
     9.7 -      |-> (fn [thm] => Code.add_default_func thm);
     9.8 +      |-> (fn [thm] => Code.add_default_eqn thm);
     9.9    in ((c, T), thy') end;
    9.10  
    9.11  fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
    10.1 --- a/src/Pure/Isar/specification.ML	Fri Sep 26 09:09:53 2008 +0200
    10.2 +++ b/src/Pure/Isar/specification.ML	Fri Sep 26 09:10:02 2008 +0200
    10.3 @@ -184,7 +184,7 @@
    10.4      val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
    10.5          (var, ((Name.map_name (suffix "_raw") name, []), rhs));
    10.6      val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
    10.7 -        ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);
    10.8 +        ((name, Code.add_default_eqn_attr :: atts), [prove lthy2 th]);
    10.9  
   10.10      val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
   10.11      val _ =
    11.1 --- a/src/Pure/Proof/extraction.ML	Fri Sep 26 09:09:53 2008 +0200
    11.2 +++ b/src/Pure/Proof/extraction.ML	Fri Sep 26 09:10:02 2008 +0200
    11.3 @@ -739,7 +739,7 @@
    11.4                        (ProofChecker.thm_of_proof thy'
    11.5                         (fst (Proofterm.freeze_thaw_prf prf))))))
    11.6               |> snd
    11.7 -             |> fold Code.add_default_func def_thms
    11.8 +             |> fold Code.add_default_eqn def_thms
    11.9             end
   11.10         | SOME _ => thy);
   11.11  
    12.1 --- a/src/Tools/code/code_funcgr.ML	Fri Sep 26 09:09:53 2008 +0200
    12.2 +++ b/src/Tools/code/code_funcgr.ML	Fri Sep 26 09:10:02 2008 +0200
    12.3 @@ -9,7 +9,7 @@
    12.4  signature CODE_FUNCGR =
    12.5  sig
    12.6    type T
    12.7 -  val funcs: T -> string -> (thm * bool) list
    12.8 +  val eqns: T -> string -> (thm * bool) list
    12.9    val typ: T -> string -> (string * sort) list * typ
   12.10    val all: T -> string list
   12.11    val pretty: theory -> T -> Pretty.T
   12.12 @@ -26,7 +26,7 @@
   12.13  
   12.14  type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
   12.15  
   12.16 -fun funcs funcgr =
   12.17 +fun eqns funcgr =
   12.18    these o Option.map snd o try (Graph.get_node funcgr);
   12.19  
   12.20  fun typ funcgr =
   12.21 @@ -97,7 +97,7 @@
   12.22      val tab = fold meets cs Vartab.empty;
   12.23    in map (Code_Unit.inst_thm tab) thms end;
   12.24  
   12.25 -fun resort_funcss thy algebra funcgr =
   12.26 +fun resort_eqnss thy algebra funcgr =
   12.27    let
   12.28      val typ_funcgr = try (fst o Graph.get_node funcgr);
   12.29      val resort_dep = (apsnd o burrow_fst) (resort_thms thy algebra typ_funcgr);
   12.30 @@ -105,22 +105,22 @@
   12.31        | resort_rec typ_of (c, thms as (thm, _) :: _) = if is_some (AxClass.inst_of_param thy c)
   12.32            then (true, (c, thms))
   12.33            else let
   12.34 -            val (_, (vs, ty)) = Code_Unit.head_func thm;
   12.35 +            val (_, (vs, ty)) = Code_Unit.head_eqn thm;
   12.36              val thms' as (thm', _) :: _ = burrow_fst (resort_thms thy algebra typ_of) thms
   12.37 -            val (_, (vs', ty')) = Code_Unit.head_func thm'; (*FIXME simplify check*)
   12.38 +            val (_, (vs', ty')) = Code_Unit.head_eqn thm'; (*FIXME simplify check*)
   12.39            in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end;
   12.40 -    fun resort_recs funcss =
   12.41 +    fun resort_recs eqnss =
   12.42        let
   12.43 -        fun typ_of c = case these (AList.lookup (op =) funcss c)
   12.44 -         of (thm, _) :: _ => (SOME o snd o Code_Unit.head_func) thm
   12.45 +        fun typ_of c = case these (AList.lookup (op =) eqnss c)
   12.46 +         of (thm, _) :: _ => (SOME o snd o Code_Unit.head_eqn) thm
   12.47            | [] => NONE;
   12.48 -        val (unchangeds, funcss') = split_list (map (resort_rec typ_of) funcss);
   12.49 +        val (unchangeds, eqnss') = split_list (map (resort_rec typ_of) eqnss);
   12.50          val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
   12.51 -      in (unchanged, funcss') end;
   12.52 -    fun resort_rec_until funcss =
   12.53 +      in (unchanged, eqnss') end;
   12.54 +    fun resort_rec_until eqnss =
   12.55        let
   12.56 -        val (unchanged, funcss') = resort_recs funcss;
   12.57 -      in if unchanged then funcss' else resort_rec_until funcss' end;
   12.58 +        val (unchanged, eqnss') = resort_recs eqnss;
   12.59 +      in if unchanged then eqnss' else resort_rec_until eqnss' end;
   12.60    in map resort_dep #> resort_rec_until end;
   12.61  
   12.62  fun instances_of thy algebra insts =
   12.63 @@ -157,7 +157,7 @@
   12.64      |> Graph.new_node (const, [])
   12.65      |> pair (SOME const)
   12.66    else let
   12.67 -    val thms = Code.these_funcs thy const
   12.68 +    val thms = Code.these_eqns thy const
   12.69        |> burrow_fst Code_Unit.norm_args
   12.70        |> burrow_fst (Code_Unit.norm_varnames Code_Name.purify_tvar Code_Name.purify_var);
   12.71      val rhs = consts_of (const, thms);
   12.72 @@ -176,18 +176,18 @@
   12.73        else I;
   12.74    in timeap (ensure_const' thy algebra funcgr const) end;
   12.75  
   12.76 -fun merge_funcss thy algebra raw_funcss funcgr =
   12.77 +fun merge_eqnss thy algebra raw_eqnss funcgr =
   12.78    let
   12.79 -    val funcss = raw_funcss
   12.80 -      |> resort_funcss thy algebra funcgr
   12.81 +    val eqnss = raw_eqnss
   12.82 +      |> resort_eqnss thy algebra funcgr
   12.83        |> filter_out (can (Graph.get_node funcgr) o fst);
   12.84 -    fun typ_func c [] = Code.default_typ thy c
   12.85 -      | typ_func c (thms as (thm, _) :: _) = (snd o Code_Unit.head_func) thm;
   12.86 -    fun add_funcs (const, thms) =
   12.87 -      Graph.new_node (const, (typ_func const thms, thms));
   12.88 -    fun add_deps (funcs as (const, thms)) funcgr =
   12.89 +    fun typ_eqn c [] = Code.default_typ thy c
   12.90 +      | typ_eqn c (thms as (thm, _) :: _) = (snd o Code_Unit.head_eqn) thm;
   12.91 +    fun add_eqns (const, thms) =
   12.92 +      Graph.new_node (const, (typ_eqn const thms, thms));
   12.93 +    fun add_deps (eqns as (const, thms)) funcgr =
   12.94        let
   12.95 -        val deps = consts_of funcs;
   12.96 +        val deps = consts_of eqns;
   12.97          val insts = instances_of_consts thy algebra funcgr
   12.98            (fold_consts (insert (op =)) (map fst thms) []);
   12.99        in
  12.100 @@ -198,8 +198,8 @@
  12.101         end;
  12.102    in
  12.103      funcgr
  12.104 -    |> fold add_funcs funcss
  12.105 -    |> fold add_deps funcss
  12.106 +    |> fold add_eqns eqnss
  12.107 +    |> fold add_deps eqnss
  12.108    end
  12.109  and ensure_consts thy algebra cs funcgr =
  12.110    let
  12.111 @@ -207,7 +207,7 @@
  12.112        |> fold (snd oo ensure_const thy algebra funcgr) cs;
  12.113    in
  12.114      funcgr
  12.115 -    |> fold (merge_funcss thy algebra)
  12.116 +    |> fold (merge_eqnss thy algebra)
  12.117           (map (AList.make (Graph.get_node auxgr))
  12.118           (rev (Graph.strong_conn auxgr)))
  12.119    end;