new structure for code generator modules
authorhaftmann
Fri Aug 10 17:10:03 2007 +0200 (2007-08-10)
changeset 24222a8a28c15c5cc
parent 24221 dd4a7ea0e64a
child 24223 fa9421d52c74
new structure for code generator modules
src/HOL/Library/Efficient_Nat.thy
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Aug 10 17:10:02 2007 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Aug 10 17:10:03 2007 +0200
     1.3 @@ -239,7 +239,7 @@
     1.4  *}
     1.5  
     1.6  setup {*
     1.7 -  CodegenData.add_inline_proc ("nat_of_int_of_number_of", nat_of_int_of_number_of)
     1.8 +  Code.add_inline_proc ("nat_of_int_of_number_of", nat_of_int_of_number_of)
     1.9  *}
    1.10  
    1.11  text {*
    1.12 @@ -268,15 +268,8 @@
    1.13  (*<*)
    1.14  
    1.15  ML {*
    1.16 -local
    1.17 -  val Suc_if_eq = thm "Suc_if_eq";
    1.18 -  val Suc_clause = thm "Suc_clause";
    1.19 -  fun contains_suc t = member (op =) (term_consts t) "Suc";
    1.20 -in
    1.21 -
    1.22  fun remove_suc thy thms =
    1.23    let
    1.24 -    val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
    1.25      val vname = Name.variant (map fst
    1.26        (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
    1.27      val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
    1.28 @@ -302,7 +295,7 @@
    1.29               (Drule.instantiate'
    1.30                 [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
    1.31                   SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
    1.32 -               Suc_if_eq')) (Thm.forall_intr cv' th)
    1.33 +               @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
    1.34        in
    1.35          case map_filter (fn th'' =>
    1.36              SOME (th'', singleton
    1.37 @@ -321,7 +314,8 @@
    1.38  
    1.39  fun eqn_suc_preproc thy ths =
    1.40    let
    1.41 -    val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
    1.42 +    val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
    1.43 +    fun contains_suc t = member (op =) (term_consts t) @{const_name Suc};
    1.44    in
    1.45      if forall (can dest) ths andalso
    1.46        exists (contains_suc o dest) ths
    1.47 @@ -330,10 +324,9 @@
    1.48  
    1.49  fun remove_suc_clause thy thms =
    1.50    let
    1.51 -    val Suc_clause' = Thm.transfer thy Suc_clause;
    1.52      val vname = Name.variant (map fst
    1.53        (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
    1.54 -    fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
    1.55 +    fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
    1.56        | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
    1.57        | find_var _ = NONE;
    1.58      fun find_thm th =
    1.59 @@ -351,7 +344,7 @@
    1.60                  [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
    1.61                     abstract_over (Sucv,
    1.62                       HOLogic.dest_Trueprop (prop_of th')))))),
    1.63 -                 SOME (cert v)] Suc_clause'))
    1.64 +                 SOME (cert v)] @{thm Suc_clause}))
    1.65              (Thm.forall_intr (cert v) th'))
    1.66          in
    1.67            remove_suc_clause thy (map (fn th''' =>
    1.68 @@ -369,8 +362,6 @@
    1.69      then remove_suc_clause thy ths else ths
    1.70    end;
    1.71  
    1.72 -end; (*local*)
    1.73 -
    1.74  fun lift_obj_eq f thy =
    1.75    map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
    1.76    #> f thy
    1.77 @@ -381,8 +372,8 @@
    1.78  setup {*
    1.79    Codegen.add_preprocessor eqn_suc_preproc
    1.80    #> Codegen.add_preprocessor clause_suc_preproc
    1.81 -  #> CodegenData.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc)
    1.82 -  #> CodegenData.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc)
    1.83 +  #> Code.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc)
    1.84 +  #> Code.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc)
    1.85  *}
    1.86  (*>*)
    1.87