tuned datatype_codegen setup
authorhaftmann
Thu Oct 04 19:54:46 2007 +0200 (2007-10-04)
changeset 24845abcd15369ffa
parent 24844 98c006a30218
child 24846 d8ff870a11ff
tuned datatype_codegen setup
src/HOL/Datatype.thy
src/HOL/Inductive.thy
src/HOL/Tools/datatype_codegen.ML
     1.1 --- a/src/HOL/Datatype.thy	Thu Oct 04 19:54:44 2007 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Thu Oct 04 19:54:46 2007 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  
     1.5  theory Datatype
     1.6  imports Finite_Set
     1.7 +uses "Tools/datatype_codegen.ML"
     1.8  begin
     1.9  
    1.10  typedef (Node)
    1.11 @@ -527,9 +528,6 @@
    1.12  by auto
    1.13  
    1.14  
    1.15 -subsection {* Finishing the datatype package setup *}
    1.16 -
    1.17 -setup "DatatypeCodegen.setup_hooks"
    1.18  text {* hides popular names *}
    1.19  hide (open) type node item
    1.20  hide (open) const Push Node Atom Leaf Numb Lim Split Case
    1.21 @@ -685,6 +683,8 @@
    1.22  
    1.23  subsubsection {* Code generator setup *}
    1.24  
    1.25 +setup DatatypeCodegen.setup
    1.26 +
    1.27  definition
    1.28    is_none :: "'a option \<Rightarrow> bool" where
    1.29    is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
     2.1 --- a/src/HOL/Inductive.thy	Thu Oct 04 19:54:44 2007 +0200
     2.2 +++ b/src/HOL/Inductive.thy	Thu Oct 04 19:54:46 2007 +0200
     2.3 @@ -17,7 +17,6 @@
     2.4    ("Tools/datatype_abs_proofs.ML")
     2.5    ("Tools/datatype_case.ML")
     2.6    ("Tools/datatype_package.ML")
     2.7 -  ("Tools/datatype_codegen.ML")
     2.8    ("Tools/primrec_package.ML")
     2.9  begin
    2.10  
    2.11 @@ -108,8 +107,6 @@
    2.12  use "Tools/datatype_package.ML"
    2.13  setup DatatypePackage.setup
    2.14  use "Tools/primrec_package.ML"
    2.15 -use "Tools/datatype_codegen.ML"
    2.16 -setup DatatypeCodegen.setup
    2.17  
    2.18  use "Tools/inductive_codegen.ML"
    2.19  setup InductiveCodegen.setup
     3.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Oct 04 19:54:44 2007 +0200
     3.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Oct 04 19:54:46 2007 +0200
     3.3 @@ -29,7 +29,6 @@
     3.4      -> theory -> theory
     3.5  
     3.6    val setup: theory -> theory
     3.7 -  val setup_hooks: theory -> theory
     3.8  end;
     3.9  
    3.10  structure DatatypeCodegen : DATATYPE_CODEGEN =
    3.11 @@ -433,6 +432,7 @@
    3.12      |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
    3.13      |> Thm.implies_intr asm
    3.14      |> Thm.generalize ([], params) 0
    3.15 +    |> Conv.fconv_rule (Class.unoverload thy)
    3.16      |> Thm.varifyT
    3.17    end;
    3.18  
    3.19 @@ -587,13 +587,6 @@
    3.20  
    3.21  (** theory setup **)
    3.22  
    3.23 -fun add_datatype_case_const dtco thy =
    3.24 -  let
    3.25 -    val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;
    3.26 -  in
    3.27 -    CodePackage.add_appconst (case_name, CodePackage.appgen_case dest_case_expr) thy
    3.28 -  end;
    3.29 -
    3.30  fun add_datatype_case_defs dtco thy =
    3.31    let
    3.32      val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
    3.33 @@ -601,15 +594,15 @@
    3.34      fold_rev Code.add_default_func case_rewrites thy
    3.35    end;
    3.36  
    3.37 +fun add_datatype_case_certs dtco thy =
    3.38 +  Code.add_case (get_case_cert thy dtco) thy;
    3.39 +
    3.40  val setup = 
    3.41    add_codegen "datatype" datatype_codegen
    3.42    #> add_tycodegen "datatype" datatype_tycodegen
    3.43 -  #> DatatypePackage.interpretation (fold add_datatype_case_const)
    3.44 +  #> DatatypePackage.interpretation (fold add_datatype_case_certs)
    3.45    #> DatatypePackage.interpretation (fold add_datatype_case_defs)
    3.46 -
    3.47 -val setup_hooks =
    3.48 -  add_codetypes_hook codetype_hook
    3.49 +  #> add_codetypes_hook codetype_hook
    3.50    #> add_codetypes_hook eq_hook
    3.51  
    3.52 -
    3.53  end;