code generation 2 adjustments
authorhaftmann
Tue Sep 19 15:22:05 2006 +0200 (2006-09-19)
changeset 2059765fe827aa595
parent 20596 3950e65f48f8
child 20598 f8031b91c946
code generation 2 adjustments
src/HOL/Library/EfficientNat.thy
src/HOL/Library/ExecutableRat.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/Tools/typedef_codegen.ML
src/HOL/ex/Classpackage.thy
src/HOL/ex/CodeCollections.thy
src/HOL/ex/CodeEval.thy
src/HOL/ex/Codegenerator.thy
src/HOL/ex/ROOT.ML
src/Pure/IsaMakefile
     1.1 --- a/src/HOL/Library/EfficientNat.thy	Tue Sep 19 15:22:03 2006 +0200
     1.2 +++ b/src/HOL/Library/EfficientNat.thy	Tue Sep 19 15:22:05 2006 +0200
     1.3 @@ -126,8 +126,8 @@
     1.4    unfolding nat_less_def by simp
     1.5  lemma [code func, code inline]: "(m <= n) = nat_less_equal m n"
     1.6    unfolding nat_less_equal_def by simp
     1.7 -lemma [code func, code inline]: "(m = n) = nat_eq m n"
     1.8 -  unfolding nat_eq_def by simp
     1.9 +lemma [code func, code inline]: "OperationalEquality.eq m n = nat_eq m n"
    1.10 +  unfolding nat_eq_def eq_def by simp
    1.11  lemma [code func]:
    1.12    "int_aux i n = (if nat_eq n 0 then i else int_aux (i + 1) (nat_minus n 1))"
    1.13    unfolding nat_eq_def nat_minus_def int_aux_def by simp
    1.14 @@ -273,8 +273,8 @@
    1.15  setup {*
    1.16    Codegen.add_preprocessor eqn_suc_preproc
    1.17    #> Codegen.add_preprocessor clause_suc_preproc
    1.18 -  #> CodegenTheorems.add_preproc (lift_obj_eq eqn_suc_preproc)
    1.19 -  #> CodegenTheorems.add_preproc (lift_obj_eq clause_suc_preproc)
    1.20 +  #> CodegenData.add_preproc (lift_obj_eq eqn_suc_preproc)
    1.21 +  #> CodegenData.add_preproc (lift_obj_eq clause_suc_preproc)
    1.22  *}
    1.23  (*>*)
    1.24  
     2.1 --- a/src/HOL/Library/ExecutableRat.thy	Tue Sep 19 15:22:03 2006 +0200
     2.2 +++ b/src/HOL/Library/ExecutableRat.thy	Tue Sep 19 15:22:05 2006 +0200
     2.3 @@ -48,8 +48,8 @@
     2.4    to_rat :: "erat \<Rightarrow> rat"
     2.5    to_rat_def: "to_rat r = (case r of (Rat a p q) \<Rightarrow>
     2.6         if a then Fract p q else Fract (uminus p) q)"
     2.7 -  eq_rat :: "erat \<Rightarrow> erat \<Rightarrow> bool"
     2.8 -  "eq_rat r s = (norm r = norm s)"
     2.9 +  eq_erat :: "erat \<Rightarrow> erat \<Rightarrow> bool"
    2.10 +  "eq_erat r s = (norm r = norm s)"
    2.11  
    2.12  defs (overloaded)
    2.13    zero_rat_def: "0 == Rat True 0 1"
    2.14 @@ -117,7 +117,7 @@
    2.15    "op * :: erat \<Rightarrow> erat \<Rightarrow> erat"
    2.16    "inverse :: erat \<Rightarrow> erat"
    2.17    "op <= :: erat \<Rightarrow> erat \<Rightarrow> bool"
    2.18 -  eq_rat
    2.19 +  eq_erat
    2.20    (SML) (Haskell)
    2.21  
    2.22  code_const Fract
    2.23 @@ -156,8 +156,12 @@
    2.24    (SML "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
    2.25    (Haskell "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
    2.26  
    2.27 -code_const "op = :: rat \<Rightarrow> rat \<Rightarrow> bool"
    2.28 -  (SML "{*eq_rat*}")
    2.29 -  (Haskell "{*eq_rat*}")
    2.30 +instance rat :: eq ..
    2.31 +
    2.32 +code_const "OperationalEquality.eq :: rat \<Rightarrow> rat \<Rightarrow> bool"
    2.33 +  (SML "{*eq_erat*}")
    2.34 +  (Haskell "{*eq_erat*}")
    2.35 +
    2.36 +code_gen (SML -)
    2.37  
    2.38  end
     3.1 --- a/src/HOL/Library/ExecutableSet.thy	Tue Sep 19 15:22:03 2006 +0200
     3.2 +++ b/src/HOL/Library/ExecutableSet.thy	Tue Sep 19 15:22:05 2006 +0200
     3.3 @@ -9,14 +9,21 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -section {* Definitional rewrites *}
     3.8 +section {* Definitional equality rewrites *}
     3.9 +
    3.10 +instance set :: (eq) eq ..
    3.11  
    3.12  lemma [code target: Set]:
    3.13    "(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)"
    3.14    by blast
    3.15  
    3.16 +lemma [code func]:
    3.17 +  "OperationalEquality.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)"
    3.18 +  unfolding eq_def by blast
    3.19 +
    3.20  declare bex_triv_one_point1 [symmetric, standard, code]
    3.21  
    3.22 +
    3.23  section {* HOL definitions *}
    3.24  
    3.25  subsection {* Basic definitions *}
    3.26 @@ -24,9 +31,9 @@
    3.27  definition
    3.28    flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
    3.29    "flip f a b = f b a"
    3.30 -  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
    3.31 +  member :: "'a list \<Rightarrow> 'a\<Colon>eq \<Rightarrow> bool"
    3.32    "member xs x = (x \<in> set xs)"
    3.33 -  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.34 +  insertl :: "'a\<Colon>eq\<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.35    "insertl x xs = (if member xs x then xs else x#xs)"
    3.36  
    3.37  lemma
    3.38 @@ -44,6 +51,7 @@
    3.39  declare drop_first.simps [code target: List]
    3.40  
    3.41  declare remove1.simps [code del]
    3.42 +ML {* reset CodegenData.strict_functyp *}
    3.43  lemma [code target: List]:
    3.44    "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
    3.45  proof (cases "member xs x")
    3.46 @@ -53,6 +61,7 @@
    3.47    have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
    3.48    with True show ?thesis by simp
    3.49  qed
    3.50 +ML {* set CodegenData.strict_functyp *}
    3.51  
    3.52  lemma member_nil [simp]:
    3.53    "member [] = (\<lambda>x. False)"
    3.54 @@ -84,8 +93,7 @@
    3.55  
    3.56  subsection {* Derived definitions *}
    3.57  
    3.58 -
    3.59 -function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.60 +function unionl :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.61  where
    3.62    "unionl [] ys = ys"
    3.63  | "unionl xs ys = foldr insertl xs ys"
    3.64 @@ -94,7 +102,7 @@
    3.65  lemmas unionl_def = unionl.simps(2)
    3.66  declare unionl.simps[code]
    3.67  
    3.68 -function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.69 +function intersect :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.70  where
    3.71    "intersect [] ys = []"
    3.72  | "intersect xs [] = []"
    3.73 @@ -104,7 +112,7 @@
    3.74  lemmas intersect_def = intersect.simps(3)
    3.75  declare intersect.simps[code]
    3.76  
    3.77 -function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.78 +function subtract :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.79  where
    3.80    "subtract [] ys = ys"
    3.81  | "subtract xs [] = []"
    3.82 @@ -114,7 +122,7 @@
    3.83  lemmas subtract_def = subtract.simps(3)
    3.84  declare subtract.simps[code]
    3.85  
    3.86 -function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
    3.87 +function map_distinct :: "('a \<Rightarrow> 'b\<Colon>eq) \<Rightarrow> 'a list \<Rightarrow> 'b list"
    3.88  where
    3.89    "map_distinct f [] = []"
    3.90  | "map_distinct f xs = foldr (insertl o f) xs []"
    3.91 @@ -123,7 +131,7 @@
    3.92  lemmas map_distinct_def = map_distinct.simps(2)
    3.93  declare map_distinct.simps[code]
    3.94  
    3.95 -function unions :: "'a list list \<Rightarrow> 'a list"
    3.96 +function unions :: "'a\<Colon>eq list list \<Rightarrow> 'a list"
    3.97  where
    3.98    "unions [] = []"
    3.99    "unions xs = foldr unionl xs []"
   3.100 @@ -132,14 +140,14 @@
   3.101  lemmas unions_def = unions.simps(2)
   3.102  declare unions.simps[code]
   3.103  
   3.104 -consts intersects :: "'a list list \<Rightarrow> 'a list"
   3.105 +consts intersects :: "'a\<Colon>eq list list \<Rightarrow> 'a list"
   3.106  primrec
   3.107    "intersects (x#xs) = foldr intersect xs x"
   3.108  
   3.109  definition
   3.110 -  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list"
   3.111 +  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b\<Colon>eq list) \<Rightarrow> 'b list"
   3.112    "map_union xs f = unions (map f xs)"
   3.113 -  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list"
   3.114 +  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b\<Colon>eq list) \<Rightarrow> 'b list"
   3.115    "map_inter xs f = intersects (map f xs)"
   3.116  
   3.117  
   3.118 @@ -266,11 +274,6 @@
   3.119    "ExecutableSet.insertl" "List.insertl"
   3.120    "ExecutableSet.drop_first" "List.drop_first"
   3.121  
   3.122 -code_gen
   3.123 -  insertl unionl intersect flip subtract map_distinct
   3.124 -  unions intersects map_union map_inter Blall Blex
   3.125 -  (SML) (Haskell) 
   3.126 -
   3.127  code_const "{}"
   3.128    (SML target_atom "[]")
   3.129    (Haskell target_atom "[]")
   3.130 @@ -319,4 +322,6 @@
   3.131    (SML "{*Blex*}")
   3.132    (Haskell "{*Blex*}")
   3.133  
   3.134 +code_gen (SML -) (SML _)
   3.135 +
   3.136  end
     4.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 19 15:22:03 2006 +0200
     4.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 19 15:22:05 2006 +0200
     4.3 @@ -8,9 +8,11 @@
     4.4  signature DATATYPE_CODEGEN =
     4.5  sig
     4.6    val get_eq: theory -> string -> thm list
     4.7 -  val get_datatype_spec_thms: theory -> string
     4.8 -    -> (((string * sort) list * (string * typ list) list) * tactic) option
     4.9 -  val datatype_tac: theory -> string -> tactic
    4.10 +  val get_eq_datatype: theory -> string -> thm list
    4.11 +  val get_eq_typecopy: theory -> string -> thm list
    4.12 +  val get_cert: theory -> bool * string -> thm list
    4.13 +  val get_cert_datatype: theory -> string -> thm list
    4.14 +  val get_cert_typecopy: theory -> string -> thm list
    4.15    val dest_case_expr: theory -> term
    4.16      -> ((string * typ) list * ((term * typ) * (term * term) list)) option
    4.17    val add_datatype_case_const: string -> theory -> theory
    4.18 @@ -18,6 +20,8 @@
    4.19  
    4.20    type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
    4.21      -> theory -> theory
    4.22 +  val codetype_hook: hook
    4.23 +  val eq_hook: hook
    4.24    val codetypes_dependency: theory -> (string * bool) list list
    4.25    val add_codetypes_hook_bootstrap: hook -> theory -> theory
    4.26    val the_codetypes_mut_specs: theory -> (string * bool) list
    4.27 @@ -26,9 +30,10 @@
    4.28      -> (string * (((string * sort list) * sort) * term list)) list option
    4.29    val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort
    4.30      -> (theory -> ((string * sort list) * sort) list -> (string * term list) list
    4.31 -    -> ((bstring * attribute list) * term) list) -> theory -> theory
    4.32 +    -> ((bstring * attribute list) * term) list) -> (theory -> theory) -> theory -> theory
    4.33  
    4.34    val setup: theory -> theory
    4.35 +  val setup2: theory -> theory
    4.36  end;
    4.37  
    4.38  structure DatatypeCodegen : DATATYPE_CODEGEN =
    4.39 @@ -370,26 +375,20 @@
    4.40    in map mk_dist (sym_product cos) end;
    4.41  
    4.42  local
    4.43 -  val not_sym = thm "HOL.not_sym";
    4.44 +  val bool_eq_implies = thm "iffD1";
    4.45 +  val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
    4.46 +  val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
    4.47    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
    4.48 -in fun get_eq thy dtco =
    4.49 +  val not_eq_quodlibet = thm "not_eq_quodlibet";
    4.50 +in fun get_cert_datatype thy dtco =
    4.51    let
    4.52      val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
    4.53 -    fun mk_triv_inject co =
    4.54 -      let
    4.55 -        val ct' = Thm.cterm_of thy
    4.56 -          (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
    4.57 -        val cty' = Thm.ctyp_of_term ct';
    4.58 -        val refl = Thm.prop_of HOL.refl;
    4.59 -        val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
    4.60 -          (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
    4.61 -          refl NONE;
    4.62 -      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
    4.63 -    val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
    4.64 -    val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
    4.65 +    val inject = (#inject o DatatypePackage.the_datatype thy) dtco
    4.66 +      |> map (fn thm => bool_eq_implies OF [thm] )
    4.67 +      |> map (Tactic.rewrite_rule [rew_eq, rew_conj]);
    4.68      val ctxt = Context.init_proof thy;
    4.69      val simpset = Simplifier.context ctxt
    4.70 -      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
    4.71 +      (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
    4.72      val cos = map (fn (co, tys) =>
    4.73          (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
    4.74      val tac = ALLGOALS (simp_tac simpset)
    4.75 @@ -397,30 +396,19 @@
    4.76      val distinct =
    4.77        mk_distinct cos
    4.78        |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    4.79 -      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
    4.80 -  in inject1 @ inject2 @ distinct end;
    4.81 +      |> map (fn thm => not_eq_quodlibet OF [thm])
    4.82 +  in inject @ distinct end
    4.83 +and get_cert_typecopy thy dtco =
    4.84 +  let
    4.85 +    val SOME { inject, ... } = TypecopyPackage.get_typecopy_info thy dtco;
    4.86 +    val thm = Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [inject]);
    4.87 +  in
    4.88 +    [thm]
    4.89 +  end;
    4.90  end (*local*);
    4.91  
    4.92 -fun datatype_tac thy dtco =
    4.93 -  let
    4.94 -    val ctxt = Context.init_proof thy;
    4.95 -    val inject = (#inject o DatatypePackage.the_datatype thy) dtco;
    4.96 -    val simpset = Simplifier.context ctxt
    4.97 -      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
    4.98 -  in
    4.99 -    (TRY o ALLGOALS o match_tac) [HOL.eq_reflection]
   4.100 -    THEN (
   4.101 -      (ALLGOALS o match_tac) (eqTrueI :: inject)
   4.102 -      ORELSE (ALLGOALS o simp_tac) simpset
   4.103 -    )
   4.104 -    THEN (ALLGOALS o match_tac) [HOL.refl, Drule.reflexive_thm]
   4.105 -  end;
   4.106 -
   4.107 -fun get_datatype_spec_thms thy dtco =
   4.108 -  case DatatypePackage.get_datatype_spec thy dtco
   4.109 -   of SOME vs_cos =>
   4.110 -        SOME (vs_cos, datatype_tac thy dtco)
   4.111 -    | NONE => NONE;
   4.112 +fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
   4.113 +  | get_cert thy (false, dtco) = get_cert_typecopy thy dtco;
   4.114  
   4.115  fun add_datatype_case_const dtco thy =
   4.116    let
   4.117 @@ -433,7 +421,7 @@
   4.118    let
   4.119      val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
   4.120    in
   4.121 -    fold CodegenTheorems.add_fun case_rewrites thy
   4.122 +    fold_rev CodegenData.add_func case_rewrites thy
   4.123    end;
   4.124  
   4.125  
   4.126 @@ -536,7 +524,7 @@
   4.127      ) else NONE
   4.128    end;
   4.129  
   4.130 -fun prove_codetypes_arities tac tycos sort f thy =
   4.131 +fun prove_codetypes_arities tac tycos sort f after_qed thy =
   4.132    case get_codetypes_arities thy tycos sort
   4.133     of NONE => thy
   4.134      | SOME insts => let
   4.135 @@ -548,20 +536,128 @@
   4.136              then NONE else SOME (arity, (tyco, cs)))) insts;
   4.137        in
   4.138          thy
   4.139 -        |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
   4.140 -             arities ("", []) (f thy arities css)
   4.141 +        |> K ((not o null) arities) ? (ClassPackage.prove_instance_arity tac
   4.142 +             arities ("", []) (f thy arities css) #> after_qed)
   4.143        end;
   4.144  
   4.145 +local
   4.146 +  val class_eq = "OperationalEquality.eq";
   4.147 +in fun add_eq_instance specs =
   4.148 +  prove_codetypes_arities
   4.149 +    (K (ClassPackage.intro_classes_tac []))
   4.150 +    (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   4.151 +    [class_eq] ((K o K o K) [])
   4.152 +end; (*local*)
   4.153 +
   4.154 +local
   4.155 +  val not_sym = thm "HOL.not_sym";
   4.156 +  val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
   4.157 +in fun get_eq_datatype thy dtco =
   4.158 +  let
   4.159 +    val _ = writeln "01";
   4.160 +    val SOME (vs, cs) = DatatypePackage.get_datatype_spec (Context.check_thy thy) dtco;
   4.161 +    val _ = writeln "02";
   4.162 +    fun mk_triv_inject co =
   4.163 +      let
   4.164 +        val ct' = Thm.cterm_of (Context.check_thy thy)
   4.165 +          (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
   4.166 +        val cty' = Thm.ctyp_of_term ct';
   4.167 +        val refl = Thm.prop_of HOL.refl;
   4.168 +        val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
   4.169 +          (K o SOME) (Thm.cterm_of (Context.check_thy thy) (Var (v, Thm.typ_of cty')), Thm.ctyp_of (Context.check_thy thy) ty) | _ => I)
   4.170 +          refl NONE;
   4.171 +      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
   4.172 +    val _ = writeln "03";
   4.173 +    val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
   4.174 +    val _ = writeln "04";
   4.175 +    val inject2 = (#inject o DatatypePackage.the_datatype (Context.check_thy thy)) dtco;
   4.176 +    val _ = writeln "05";
   4.177 +    val ctxt = Context.init_proof (Context.check_thy thy);
   4.178 +    val _ = writeln "06";
   4.179 +    val simpset = Simplifier.context ctxt
   4.180 +      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
   4.181 +    val _ = writeln "07";
   4.182 +    val cos = map (fn (co, tys) =>
   4.183 +        (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
   4.184 +    val tac = ALLGOALS (simp_tac simpset)
   4.185 +      THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
   4.186 +    val _ = writeln "08";
   4.187 +    val distinct =
   4.188 +      mk_distinct cos
   4.189 +      |> map (fn t => Goal.prove_global (Context.check_thy thy) [] [] t (K tac))
   4.190 +      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
   4.191 +    val _ = writeln "09";
   4.192 +  in inject1 @ inject2 @ distinct end;
   4.193 +
   4.194 +fun get_eq_typecopy thy tyco =
   4.195 +  case TypecopyPackage.get_typecopy_info thy tyco
   4.196 +   of SOME { inject, ... } => [inject]
   4.197 +    | NONE => [];
   4.198 +
   4.199 +local
   4.200 +  val lift_not_thm = thm "HOL.Eq_FalseI";
   4.201 +  val lift_thm = thm "HOL.eq_reflection";
   4.202 +  val eq_def_sym = thm "eq_def" |> Thm.symmetric;
   4.203 +  fun get_eq_thms thy tyco = case DatatypePackage.get_datatype (Context.check_thy thy) tyco
   4.204 +   of SOME _ => get_eq_datatype (Context.check_thy thy) tyco
   4.205 +    | NONE => case TypecopyPackage.get_typecopy_info thy tyco
   4.206 +       of SOME _ => get_eq_typecopy thy tyco
   4.207 +        | NONE => [];
   4.208 +in
   4.209 +  fun get_eq thy tyco =
   4.210 +    get_eq_thms (Context.check_thy thy) tyco
   4.211 +    |> tap (fn _ => writeln "10")
   4.212 +    |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) (Context.check_thy thy))
   4.213 +    |> tap (fn _ => writeln "11")
   4.214 +    |> constrain_op_eq (Context.check_thy thy)
   4.215 +    |> tap (fn _ => writeln "12")
   4.216 +    |> map (Tactic.rewrite_rule [eq_def_sym])
   4.217 +    |> tap (fn _ => writeln "13")
   4.218 +end;
   4.219 +
   4.220 +end;
   4.221 +
   4.222 +fun add_eq_thms (dtco, (_, (vs, cs))) thy =
   4.223 +  let
   4.224 +    val thy_ref = Theory.self_ref thy;
   4.225 +    val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
   4.226 +    val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
   4.227 +    val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> tap (fn _ => writeln "14x") |> rev |> tap (fn _ => writeln "15x"));
   4.228 +  in
   4.229 +    CodegenData.add_funcl
   4.230 +      (c, CodegenData.lazy get_thms) thy
   4.231 +  end;
   4.232 +
   4.233 +fun codetype_hook dtcos theory =
   4.234 +  let
   4.235 +    fun add (dtco, (flag, spec)) thy =
   4.236 +      let
   4.237 +        fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
   4.238 +      in
   4.239 +        CodegenData.add_datatype
   4.240 +          (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
   4.241 +      end;
   4.242 +  in
   4.243 +    theory
   4.244 +    |> fold add dtcos
   4.245 +  end;
   4.246 +
   4.247 +fun eq_hook dtcos =
   4.248 +  add_eq_instance dtcos (fold add_eq_thms dtcos);
   4.249 +
   4.250  
   4.251  
   4.252  (** theory setup **)
   4.253  
   4.254  val setup = 
   4.255 -  add_codegen "datatype" datatype_codegen #>
   4.256 -  add_tycodegen "datatype" datatype_tycodegen #>
   4.257 -  CodegenTheorems.add_datatype_extr
   4.258 -    get_datatype_spec_thms #>
   4.259 -  DatatypeHooks.add (fold add_datatype_case_const) #>
   4.260 -  DatatypeHooks.add (fold add_datatype_case_defs)
   4.261 +  add_codegen "datatype" datatype_codegen
   4.262 +  #> add_tycodegen "datatype" datatype_tycodegen 
   4.263 +  #> DatatypeHooks.add (fold add_datatype_case_const)
   4.264 +  #> DatatypeHooks.add (fold add_datatype_case_defs)
   4.265 +
   4.266 +val setup2 =
   4.267 +  add_codetypes_hook_bootstrap codetype_hook
   4.268 +  #> add_codetypes_hook_bootstrap eq_hook
   4.269 +
   4.270  
   4.271  end;
     5.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Sep 19 15:22:03 2006 +0200
     5.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 19 15:22:05 2006 +0200
     5.3 @@ -308,7 +308,7 @@
     5.4    (snd o PureThy.add_thmss [(("simps", simps), []),
     5.5      (("", List.concat case_thms @ size_thms @ 
     5.6            List.concat distinct  @ rec_thms), [Simplifier.simp_add]),
     5.7 -    (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
     5.8 +    (("", size_thms @ rec_thms),             [setmp CodegenData.strict_functyp false (RecfunCodegen.add NONE)]),
     5.9      (("", List.concat inject),               [iff_add]),
    5.10      (("", map name_notE (List.concat distinct)),  [Classical.safe_elim NONE]),
    5.11      (("", weak_case_congs),                  [cong_att])]);
    5.12 @@ -479,9 +479,10 @@
    5.13         strip_abs (length dts) t, is_dependent (length dts) t))
    5.14        (constrs ~~ fs);
    5.15      fun count_cases (cs, (_, _, true)) = cs
    5.16 -      | count_cases (cs, (cname, (_, body), false)) = (case AList.lookup (op =) cs body of
    5.17 -          NONE => (body, [cname]) :: cs
    5.18 -        | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs);
    5.19 +      | count_cases (cs, (cname, (_, body), false)) =
    5.20 +          case AList.lookup (op = : term * term -> bool) cs body
    5.21 +           of NONE => (body, [cname]) :: cs
    5.22 +            | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs;
    5.23      val cases' = sort (int_ord o Library.swap o pairself (length o snd))
    5.24        (Library.foldl count_cases ([], cases));
    5.25      fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
    5.26 @@ -558,33 +559,42 @@
    5.27  
    5.28  (********************* axiomatic introduction of datatypes ********************)
    5.29  
    5.30 -fun add_and_get_axioms_atts label tnames attss ts thy =
    5.31 -  foldr (fn (((tname, atts), t), (thy', axs)) =>
    5.32 -    let
    5.33 -      val ([ax], thy'') =
    5.34 -        thy'
    5.35 -        |> Theory.add_path tname
    5.36 -        |> PureThy.add_axioms_i [((label, t), atts)];
    5.37 -    in (Theory.parent_path thy'', ax::axs)
    5.38 -    end) (thy, []) (tnames ~~ attss ~~ ts) |> swap;
    5.39 +fun add_axiom label t atts thy =
    5.40 +  thy
    5.41 +  |> PureThy.add_axioms_i [((label, t), atts)];
    5.42 +
    5.43 +fun add_axioms label ts atts thy =
    5.44 +  thy
    5.45 +  |> PureThy.add_axiomss_i [((label, ts), atts)];
    5.46  
    5.47 -fun add_and_get_axioms label tnames =
    5.48 -  add_and_get_axioms_atts label tnames (replicate (length tnames) []);
    5.49 +fun add_and_get_axioms_atts label tnames ts attss =
    5.50 +  fold_map (fn (tname, (atts, t)) => fn thy =>
    5.51 +    thy
    5.52 +    |> Theory.add_path tname
    5.53 +    |> add_axiom label t atts
    5.54 +    ||> Theory.parent_path
    5.55 +    |-> (fn [ax] => pair ax)) (tnames ~~ (attss ~~ ts));
    5.56  
    5.57 -fun add_and_get_axiomss label tnames tss thy =
    5.58 -  foldr (fn ((tname, ts), (thy', axss)) =>
    5.59 -    let
    5.60 -      val ([axs], thy'') =
    5.61 -        thy'
    5.62 -        |> Theory.add_path tname
    5.63 -        |> PureThy.add_axiomss_i [((label, ts), [])];
    5.64 -    in (Theory.parent_path thy'', axs::axss)
    5.65 -    end) (thy, []) (tnames ~~ tss) |> swap;
    5.66 +fun add_and_get_axioms label tnames ts =
    5.67 +  add_and_get_axioms_atts label tnames ts (replicate (length tnames) []);
    5.68 +
    5.69 +fun add_and_get_axiomss label tnames tss =
    5.70 +  fold_map (fn (tname, ts) => fn thy =>
    5.71 +    thy
    5.72 +    |> Theory.add_path tname
    5.73 +    |> add_axioms label ts []
    5.74 +    ||> Theory.parent_path
    5.75 +    |-> (fn [ax] => pair ax)) (tnames ~~ tss);
    5.76  
    5.77  fun specify_consts args thy =
    5.78 -  let val specs =
    5.79 -    args |> map (fn (c, T, mx) => Const (Sign.full_name thy (Syntax.const_name c mx), T));
    5.80 -  in thy |> Theory.add_consts_i args |> Theory.add_finals_i false specs end;
    5.81 +  let
    5.82 +    val specs = map (fn (c, T, mx) =>
    5.83 +      Const (Sign.full_name thy (Syntax.const_name c mx), T)) args;
    5.84 +  in
    5.85 +    thy
    5.86 +    |> Sign.add_consts_i args
    5.87 +    |> Theory.add_finals_i false specs
    5.88 +  end;
    5.89  
    5.90  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    5.91      case_names_induct case_names_exhausts thy =
    5.92 @@ -675,10 +685,9 @@
    5.93      val ((([induct], [rec_thms]), inject), thy3) =
    5.94        thy2
    5.95        |> Theory.add_path (space_implode "_" new_type_names)
    5.96 -      |> PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
    5.97 -          [case_names_induct])]
    5.98 -      ||>> PureThy.add_axiomss_i [(("recs", rec_axs), [])]
    5.99 -      ||> (if no_size then I else snd o PureThy.add_axiomss_i [(("size", size_axs), [])])
   5.100 +      |> add_axiom "induct" (DatatypeProp.make_ind descr sorts) [case_names_induct]
   5.101 +      ||>> add_axioms "recs" rec_axs []
   5.102 +      ||> (if no_size then I else add_axioms "size" size_axs [] #> snd)
   5.103        ||> Theory.parent_path
   5.104        ||>> add_and_get_axiomss "inject" new_type_names
   5.105              (DatatypeProp.make_injs descr sorts);
   5.106 @@ -688,7 +697,7 @@
   5.107  
   5.108      val exhaust_ts = DatatypeProp.make_casedists descr sorts;
   5.109      val (exhaustion, thy5) = add_and_get_axioms_atts "exhaust" new_type_names
   5.110 -      (map Library.single case_names_exhausts) exhaust_ts thy4;
   5.111 +      exhaust_ts (map single case_names_exhausts) thy4;
   5.112      val (case_thms, thy6) = add_and_get_axiomss "cases" new_type_names
   5.113        (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
   5.114      val (split_ts, split_asm_ts) = ListPair.unzip
   5.115 @@ -924,11 +933,9 @@
   5.116        Theory.add_types (map (fn (tvs, tname, mx, _) =>
   5.117          (tname, length tvs, mx)) dts);
   5.118  
   5.119 -    val sign = Theory.sign_of tmp_thy;
   5.120 -
   5.121      val (tyvars, _, _, _)::_ = dts;
   5.122      val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
   5.123 -      let val full_tname = Sign.full_name sign (Syntax.type_name tname mx)
   5.124 +      let val full_tname = Sign.full_name tmp_thy (Syntax.type_name tname mx)
   5.125        in (case duplicates (op =) tvs of
   5.126              [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
   5.127                    else error ("Mutually recursive datatypes must have same type parameters")
   5.128 @@ -943,12 +950,12 @@
   5.129        let
   5.130          fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =
   5.131            let
   5.132 -            val (cargs', sorts'') = Library.foldl (prep_typ sign) (([], sorts'), cargs);
   5.133 +            val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs);
   5.134              val _ = (case foldr add_typ_tfree_names [] cargs' \\ tvs of
   5.135                  [] => ()
   5.136                | vs => error ("Extra type variables on rhs: " ^ commas vs))
   5.137 -          in (constrs @ [((if flat_names then Sign.full_name sign else
   5.138 -                Sign.full_name_path sign tname) (Syntax.const_name cname mx'),
   5.139 +          in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
   5.140 +                Sign.full_name_path tmp_thy tname) (Syntax.const_name cname mx'),
   5.141                     map (dtyp_of_typ new_dts) cargs')],
   5.142                constr_syntax' @ [(cname, mx')], sorts'')
   5.143            end handle ERROR msg =>
   5.144 @@ -961,7 +968,7 @@
   5.145        in
   5.146          case duplicates (op =) (map fst constrs') of
   5.147             [] =>
   5.148 -             (dts' @ [(i, (Sign.full_name sign (Syntax.type_name tname mx),
   5.149 +             (dts' @ [(i, (Sign.full_name tmp_thy (Syntax.type_name tname mx),
   5.150                  map DtTFree tvs, constrs'))],
   5.151                constr_syntax @ [constr_syntax'], sorts', i + 1)
   5.152           | dups => error ("Duplicate constructors " ^ commas dups ^
   5.153 @@ -969,9 +976,9 @@
   5.154        end;
   5.155  
   5.156      val (dts', constr_syntax, sorts', i) = Library.foldl prep_dt_spec (([], [], [], 0), dts);
   5.157 -    val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
   5.158 +    val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
   5.159      val dt_info = get_datatypes thy;
   5.160 -    val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
   5.161 +    val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
   5.162      val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
   5.163        if err then error ("Nonemptiness check failed for datatype " ^ s)
   5.164        else raise exn;
     6.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Sep 19 15:22:03 2006 +0200
     6.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Sep 19 15:22:05 2006 +0200
     6.3 @@ -17,7 +17,7 @@
     6.4  
     6.5  open Codegen;
     6.6  
     6.7 -structure CodegenData = TheoryDataFun
     6.8 +structure RecCodegenData = TheoryDataFun
     6.9  (struct
    6.10    val name = "HOL/recfun_codegen";
    6.11    type T = (thm * string option) list Symtab.table;
    6.12 @@ -40,27 +40,27 @@
    6.13    let
    6.14      fun add thm =
    6.15        if Pattern.pattern (lhs_of thm) then
    6.16 -        CodegenData.map
    6.17 +        RecCodegenData.map
    6.18            (Symtab.update_list ((fst o const_of o prop_of) thm, (thm, optmod)))
    6.19        else tap (fn _ => warn thm)
    6.20        handle TERM _ => tap (fn _ => warn thm);
    6.21    in
    6.22      add thm
    6.23 -    #> CodegenTheorems.add_fun thm
    6.24 +    #> CodegenData.add_func thm
    6.25    end);
    6.26  
    6.27  fun del_thm thm thy =
    6.28    let
    6.29 -    val tab = CodegenData.get thy;
    6.30 +    val tab = RecCodegenData.get thy;
    6.31      val (s, _) = const_of (prop_of thm);
    6.32    in case Symtab.lookup tab s of
    6.33        NONE => thy
    6.34      | SOME thms =>
    6.35 -        CodegenData.put (Symtab.update (s, gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy
    6.36 +        RecCodegenData.put (Symtab.update (s, gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy
    6.37    end handle TERM _ => (warn thm; thy);
    6.38  
    6.39  val del = Thm.declaration_attribute
    6.40 -  (fn thm => Context.map_theory (del_thm thm #> CodegenTheorems.del_fun thm))
    6.41 +  (fn thm => Context.map_theory (del_thm thm #> CodegenData.del_func thm))
    6.42  
    6.43  fun del_redundant thy eqs [] = eqs
    6.44    | del_redundant thy eqs (eq :: eqs') =
    6.45 @@ -70,7 +70,7 @@
    6.46      in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
    6.47  
    6.48  fun get_equations thy defs (s, T) =
    6.49 -  (case Symtab.lookup (CodegenData.get thy) s of
    6.50 +  (case Symtab.lookup (RecCodegenData.get thy) s of
    6.51       NONE => ([], "")
    6.52     | SOME thms => 
    6.53         let val thms' = del_redundant thy []
    6.54 @@ -172,10 +172,10 @@
    6.55  
    6.56  
    6.57  val setup =
    6.58 -  CodegenData.init #>
    6.59 +  RecCodegenData.init #>
    6.60    add_codegen "recfun" recfun_codegen #>
    6.61    add_attribute ""
    6.62      (Args.del |-- Scan.succeed del
    6.63 -     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add);
    6.64 +     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> (fn name => setmp CodegenData.strict_functyp false (add name)));
    6.65  
    6.66  end;
     7.1 --- a/src/HOL/Tools/typecopy_package.ML	Tue Sep 19 15:22:03 2006 +0200
     7.2 +++ b/src/HOL/Tools/typecopy_package.ML	Tue Sep 19 15:22:05 2006 +0200
     7.3 @@ -21,9 +21,6 @@
     7.4    val get_typecopy_info: theory -> string -> info option
     7.5    type hook = string * info -> theory -> theory;
     7.6    val add_hook: hook -> theory -> theory;
     7.7 -  val typecopy_fun_extr: theory -> string * typ -> thm list option
     7.8 -  val typecopy_type_extr: theory -> string
     7.9 -    -> (((string * sort) list * (string * typ list) list) * tactic) option
    7.10    val print: theory -> unit
    7.11    val setup: theory -> theory
    7.12  end;
    7.13 @@ -137,27 +134,13 @@
    7.14  end; (*local*)
    7.15  
    7.16  
    7.17 -(* theory setup *)
    7.18 -
    7.19 -fun typecopy_type_extr thy tyco =
    7.20 -  case get_typecopy_info thy tyco
    7.21 -   of SOME { vs, constr, typ, inject, ... } => SOME ((vs, [(constr, [typ])]),
    7.22 -       (ALLGOALS o match_tac) [eq_reflection]
    7.23 -          THEN (ALLGOALS o match_tac) [inject])
    7.24 -    | NONE => NONE;
    7.25 +(* hooks for projection function code *)
    7.26  
    7.27 -fun typecopy_fun_extr thy (c, ty) =
    7.28 -  case (fst o strip_type) ty
    7.29 -   of Type (tyco, _) :: _ =>
    7.30 -        (case get_typecopy_info thy tyco
    7.31 -          of SOME { proj_def, proj as (c', _), ... } =>
    7.32 -              if c = c' then SOME [proj_def] else NONE
    7.33 -           | NONE => NONE)
    7.34 -    | _ => NONE;
    7.35 +fun add_project (_ , { proj_def, ...} : info) =
    7.36 +  CodegenData.add_func proj_def;
    7.37  
    7.38  val setup =
    7.39    TypecopyData.init
    7.40 -  #> CodegenTheorems.add_fun_extr (these oo typecopy_fun_extr)
    7.41 -  #> CodegenTheorems.add_datatype_extr typecopy_type_extr;
    7.42 +  #> add_hook add_project;
    7.43  
    7.44  end; (*struct*)
     8.1 --- a/src/HOL/Tools/typedef_codegen.ML	Tue Sep 19 15:22:03 2006 +0200
     8.2 +++ b/src/HOL/Tools/typedef_codegen.ML	Tue Sep 19 15:22:05 2006 +0200
     8.3 @@ -7,12 +7,6 @@
     8.4  
     8.5  signature TYPEDEF_CODEGEN =
     8.6  sig
     8.7 -  val get_triv_typedef: theory -> string
     8.8 -    -> ((((string * sort) list * (string * typ list) list) * thm) *
     8.9 -          ((string * typ) * thm)) option
    8.10 -  val typedef_fun_extr: theory -> string * typ -> thm list option
    8.11 -  val typedef_type_extr: theory -> string
    8.12 -    -> (((string * sort) list * (string * typ list) list) * tactic) option
    8.13    val setup: theory -> theory
    8.14  end;
    8.15  
    8.16 @@ -106,42 +100,8 @@
    8.17             end)
    8.18    | typedef_tycodegen thy defs gr dep module brack _ = NONE;
    8.19  
    8.20 -fun get_triv_typedef thy tyco =
    8.21 -  case TypedefPackage.get_info thy tyco
    8.22 -   of SOME {abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, Rep_name = c_rep,
    8.23 -     set_def = SOME def, Abs_inject = inject, Abs_inverse = inverse, ... } =>
    8.24 -        let
    8.25 -          val exists_thm =
    8.26 -            UNIV_I
    8.27 -            |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] []
    8.28 -            |> rewrite_rule [symmetric def];
    8.29 -        in case try (op OF) (inject, [exists_thm, exists_thm])
    8.30 -         of SOME eq_thm =>
    8.31 -              SOME (((Term.add_tfreesT (Type.no_tvars ty_abs) [], [(c_abs, [ty_rep])]), eq_thm),
    8.32 -                ((c_rep, ty_abs --> ty_rep), inverse OF [exists_thm]))
    8.33 -          | NONE => NONE
    8.34 -        end
    8.35 -    | _ => NONE;
    8.36 -
    8.37 -fun typedef_type_extr thy tyco =
    8.38 -  case get_triv_typedef thy tyco
    8.39 -   of SOME ((vs_cs, thm), _) => SOME (vs_cs,
    8.40 -       (ALLGOALS o match_tac) [eq_reflection]
    8.41 -            THEN (ALLGOALS o match_tac) [thm])
    8.42 -    | NONE => NONE;
    8.43 -
    8.44 -fun typedef_fun_extr thy (c, ty) =
    8.45 -  case (fst o strip_type) ty
    8.46 -   of Type (tyco, _) :: _ =>
    8.47 -        (case get_triv_typedef thy tyco
    8.48 -         of SOME (_, ((c', _), thm)) => if c = c' then SOME [thm] else NONE
    8.49 -          | NONE => NONE)
    8.50 -    | _ => NONE;
    8.51 -
    8.52  val setup =
    8.53    Codegen.add_codegen "typedef" typedef_codegen
    8.54    #> Codegen.add_tycodegen "typedef" typedef_tycodegen
    8.55 -  #> CodegenTheorems.add_fun_extr (these oo typedef_fun_extr)
    8.56 -  #> CodegenTheorems.add_datatype_extr typedef_type_extr
    8.57  
    8.58  end;
     9.1 --- a/src/HOL/ex/Classpackage.thy	Tue Sep 19 15:22:03 2006 +0200
     9.2 +++ b/src/HOL/ex/Classpackage.thy	Tue Sep 19 15:22:05 2006 +0200
     9.3 @@ -26,7 +26,7 @@
     9.4    from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
     9.5  qed
     9.6  
     9.7 -instance (type) list :: semigroup
     9.8 +instance list :: (type) semigroup
     9.9    "xs \<otimes> ys \<equiv> xs @ ys"
    9.10  proof
    9.11    fix xs ys zs :: "'a list"
    9.12 @@ -52,7 +52,7 @@
    9.13    from monoidl_num_def show "\<one> \<otimes> k = k" by simp
    9.14  qed
    9.15  
    9.16 -instance (type) list :: monoidl
    9.17 +instance list :: (type) monoidl
    9.18    "\<one> \<equiv> []"
    9.19  proof
    9.20    fix xs :: "'a list"
    9.21 @@ -67,7 +67,7 @@
    9.22  class monoid = monoidl +
    9.23    assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
    9.24  
    9.25 -instance monoid_list_def: (type) list :: monoid
    9.26 +instance monoid_list_def: list :: (type) monoid
    9.27  proof
    9.28    fix xs :: "'a list"
    9.29    show "xs \<otimes> \<one> = xs"
    9.30 @@ -288,26 +288,26 @@
    9.31    "\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>"
    9.32  using pow_def nat_pow_one inv_one by simp
    9.33  
    9.34 -instance semigroup_prod_def: (semigroup, semigroup) * :: semigroup
    9.35 +instance semigroup_prod_def: * :: (semigroup, semigroup) semigroup
    9.36    mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
    9.37                (x1 \<otimes> y1, x2 \<otimes> y2)"
    9.38  by default (simp_all add: split_paired_all semigroup_prod_def assoc)
    9.39  
    9.40 -instance monoidl_prod_def: (monoidl, monoidl) * :: monoidl
    9.41 +instance monoidl_prod_def: * :: (monoidl, monoidl) monoidl
    9.42    one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
    9.43  by default (simp_all add: split_paired_all monoidl_prod_def neutl)
    9.44  
    9.45 -instance monoid_prod_def: (monoid, monoid) * :: monoid
    9.46 +instance monoid_prod_def: * :: (monoid, monoid) monoid
    9.47  by default (simp_all add: split_paired_all monoid_prod_def neutr)
    9.48  
    9.49 -instance monoid_comm_prod_def: (monoid_comm, monoid_comm) * :: monoid_comm
    9.50 +instance monoid_comm_prod_def: * :: (monoid_comm, monoid_comm) monoid_comm
    9.51  by default (simp_all add: split_paired_all monoidl_prod_def comm)
    9.52  
    9.53 -instance group_prod_def: (group, group) * :: group
    9.54 +instance group_prod_def: * :: (group, group) group
    9.55    inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
    9.56  by default (simp_all add: split_paired_all group_prod_def invl)
    9.57  
    9.58 -instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
    9.59 +instance group_comm_prod_def: * :: (group_comm, group_comm) group_comm
    9.60  by default (simp_all add: split_paired_all group_prod_def comm)
    9.61  
    9.62  definition
    10.1 --- a/src/HOL/ex/CodeCollections.thy	Tue Sep 19 15:22:03 2006 +0200
    10.2 +++ b/src/HOL/ex/CodeCollections.thy	Tue Sep 19 15:22:05 2006 +0200
    10.3 @@ -5,7 +5,7 @@
    10.4  header {* Collection classes as examples for code generation *}
    10.5  
    10.6  theory CodeCollections
    10.7 -imports CodeOperationalEquality
    10.8 +imports Main
    10.9  begin
   10.10  
   10.11  section {* Collection classes as examples for code generation *}
   10.12 @@ -119,7 +119,7 @@
   10.13  
   10.14  termination by (auto_term "{}")
   10.15  
   10.16 -instance (ordered) option :: ordered
   10.17 +instance option :: (ordered) ordered
   10.18    "x <<= y == le_option' x y"
   10.19  proof (default, unfold ordered_option_def)
   10.20    fix x
   10.21 @@ -149,7 +149,7 @@
   10.22    "le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
   10.23  termination by (auto_term "{}")
   10.24  
   10.25 -instance (ordered, ordered) * :: ordered
   10.26 +instance * :: (ordered, ordered) ordered
   10.27    "x <<= y == le_pair' x y"
   10.28  apply (default, unfold "ordered_*_def", unfold split_paired_all)
   10.29  apply simp_all
   10.30 @@ -238,11 +238,11 @@
   10.31    "inf == ()"
   10.32    by default (simp add: infimum_unit_def)
   10.33  
   10.34 -instance (ordered) option :: infimum
   10.35 +instance option :: (ordered) infimum
   10.36    "inf == None"
   10.37    by default (simp add: infimum_option_def)
   10.38  
   10.39 -instance (infimum, infimum) * :: infimum
   10.40 +instance * :: (infimum, infimum) infimum
   10.41    "inf == (inf, inf)"
   10.42    by default (unfold "infimum_*_def", unfold split_paired_all, auto intro: inf)
   10.43  
   10.44 @@ -333,7 +333,7 @@
   10.45  apply (rule member_enum)+
   10.46  sorry*)
   10.47  
   10.48 -instance (enum) option :: enum
   10.49 +instance option :: (enum) enum
   10.50    "_4": "enum == None # map Some enum"
   10.51  proof (default, unfold enum_option_def)
   10.52    fix x :: "'a::enum option"
   10.53 @@ -398,13 +398,11 @@
   10.54    "test1 = sum [None, Some True, None, Some False]"
   10.55    "test2 = (inf :: nat \<times> unit)"
   10.56  
   10.57 -code_gen eq
   10.58  code_gen "op <<="
   10.59  code_gen "op <<"
   10.60  code_gen inf
   10.61  code_gen between
   10.62  code_gen index
   10.63 -code_gen sum
   10.64  code_gen test1
   10.65  code_gen test2
   10.66  
    11.1 --- a/src/HOL/ex/CodeEval.thy	Tue Sep 19 15:22:03 2006 +0200
    11.2 +++ b/src/HOL/ex/CodeEval.thy	Tue Sep 19 15:22:05 2006 +0200
    11.3 @@ -13,7 +13,7 @@
    11.4  subsection {* The typ_of class *}
    11.5  
    11.6  class typ_of =
    11.7 -  fixes typ_of :: "'a option \<Rightarrow> typ"
    11.8 +  fixes typ_of :: "'a itself \<Rightarrow> typ"
    11.9  
   11.10  ML {*
   11.11  structure TypOf =
   11.12 @@ -22,17 +22,15 @@
   11.13  local
   11.14    val thy = the_context ();
   11.15    val const_typ_of = Sign.intern_const thy "typ_of";
   11.16 -  val const_None = Sign.intern_const thy "None";
   11.17 -  fun typ_option ty = Type (Sign.intern_type (the_context ()) "option", [ty]);
   11.18 -  fun term_typ_of ty = Const (const_typ_of, typ_option ty --> Embed.typ_typ);
   11.19 +  fun term_typ_of ty = Const (const_typ_of, Term.itselfT ty --> Embed.typ_typ);
   11.20  in
   11.21    val class_typ_of = Sign.intern_class thy "typ_of";
   11.22 -  fun term_typ_of_None ty =
   11.23 -    term_typ_of ty $ Const (const_None, typ_option ty);
   11.24 +  fun term_typ_of_type ty =
   11.25 +    term_typ_of ty $ Logic.mk_type ty;
   11.26    fun mk_typ_of_def ty =
   11.27      let
   11.28 -      val lhs = term_typ_of ty $ Free ("x", typ_option ty)
   11.29 -      val rhs = Embed.term_typ (fn v => term_typ_of_None (TFree v)) ty
   11.30 +      val lhs = term_typ_of ty $ Free ("x", Term.itselfT ty)
   11.31 +      val rhs = Embed.term_typ (fn v => term_typ_of_type (TFree v)) ty
   11.32      in Logic.mk_equals (lhs, rhs) end;
   11.33  end;
   11.34  
   11.35 @@ -41,14 +39,15 @@
   11.36  
   11.37  setup {*
   11.38  let
   11.39 -  fun mk _ arities _ =
   11.40 +  fun mk thy arities _ =
   11.41      maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def
   11.42 -      (Type (tyco, map TFree (Name.names Name.context "'a" asorts))))]) arities;
   11.43 +      (Type (tyco, map TFree (Name.names Name.context "'a" asorts)))
   11.44 +      |> tap (writeln o Sign.string_of_term thy))]) arities;
   11.45    fun tac _ = ClassPackage.intro_classes_tac [];
   11.46    fun hook specs =
   11.47      DatatypeCodegen.prove_codetypes_arities tac
   11.48        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   11.49 -      [TypOf.class_typ_of] mk
   11.50 +      [TypOf.class_typ_of] mk I
   11.51  in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
   11.52  *}
   11.53  
   11.54 @@ -56,7 +55,7 @@
   11.55  subsection {* term_of class *}
   11.56  
   11.57  class term_of = typ_of +
   11.58 -  constrains typ_of :: "'a option \<Rightarrow> typ"
   11.59 +  constrains typ_of :: "'a itself \<Rightarrow> typ"
   11.60    fixes term_of :: "'a \<Rightarrow> term"
   11.61  
   11.62  ML {*
   11.63 @@ -77,7 +76,7 @@
   11.64            val lhs : term = term_term_of dty $ c;
   11.65            val rhs : term = Embed.term_term
   11.66              (fn (v, ty) => term_term_of ty $ Free (v, ty))
   11.67 -            (Embed.term_typ (fn (v, sort) => TypOf.term_typ_of_None (TFree (v, sort)))) c
   11.68 +            (Embed.term_typ (fn (v, sort) => TypOf.term_typ_of_type (TFree (v, sort)))) c
   11.69          in
   11.70            HOLogic.mk_eq (lhs, rhs)
   11.71          end;
   11.72 @@ -103,7 +102,7 @@
   11.73      else
   11.74        DatatypeCodegen.prove_codetypes_arities tac
   11.75        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   11.76 -      [TermOf.class_term_of] mk
   11.77 +      [TermOf.class_term_of] mk I
   11.78  in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
   11.79  *}
   11.80  
   11.81 @@ -116,10 +115,9 @@
   11.82  ML {*
   11.83  signature EVAL =
   11.84  sig
   11.85 -  val eval_term: term -> theory -> term * theory
   11.86 -  val eval_term' : theory -> term -> term
   11.87 +  val eval_term: theory -> term -> term
   11.88    val term: string -> unit
   11.89 -  val eval_ref: term ref
   11.90 +  val eval_ref: term option ref
   11.91    val oracle: string * (theory * exn -> term)
   11.92    val method: Method.src -> Proof.context -> Method.method
   11.93  end;
   11.94 @@ -127,30 +125,24 @@
   11.95  structure Eval : EVAL =
   11.96  struct
   11.97  
   11.98 -val eval_ref = ref Logic.protectC;
   11.99 -
  11.100 -fun eval_term t =
  11.101 -  CodegenPackage.eval_term
  11.102 -    (("Eval.eval_ref", eval_ref), TermOf.mk_term_of t);
  11.103 +val eval_ref = ref NONE;
  11.104  
  11.105 -fun eval_term' thy t =
  11.106 -  let
  11.107 -    val thy' = Theory.copy thy;
  11.108 -    val (t', _) = eval_term t thy';
  11.109 -  in t' end;
  11.110 +fun eval_term thy t =
  11.111 +  CodegenPackage.eval_term
  11.112 +    thy (("Eval.eval_ref", eval_ref), TermOf.mk_term_of t);
  11.113  
  11.114  fun term t =
  11.115    let
  11.116      val thy = the_context ();
  11.117 -    val t' = eval_term' thy (Sign.read_term thy t);
  11.118 -  in () end;
  11.119 +    val t = eval_term thy (Sign.read_term thy t);
  11.120 +  in (writeln o Sign.string_of_term thy) t end;
  11.121  
  11.122  val lift_eq_Trueprop = thm "lift_eq_Trueprop";
  11.123  
  11.124  exception Eval of term;
  11.125  
  11.126  val oracle = ("Eval", fn (thy, Eval t) =>
  11.127 -  Logic.mk_equals (t, eval_term' thy t));
  11.128 +  Logic.mk_equals (t, eval_term thy t));
  11.129  
  11.130  val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
  11.131  
  11.132 @@ -194,8 +186,6 @@
  11.133  and ('a, 'b) cair =
  11.134      Cair 'a 'b
  11.135  
  11.136 -code_gen term_of
  11.137 -
  11.138  ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *}
  11.139  
  11.140  lemma
  11.141 @@ -207,4 +197,4 @@
  11.142  lemma
  11.143    "fst (snd (fst ( ((Some (2::nat), (Suc 0, ())), [0::nat]) ))) = Suc (Suc 0) - 1" by eval
  11.144  
  11.145 -end
  11.146 +end
  11.147 \ No newline at end of file
    12.1 --- a/src/HOL/ex/Codegenerator.thy	Tue Sep 19 15:22:03 2006 +0200
    12.2 +++ b/src/HOL/ex/Codegenerator.thy	Tue Sep 19 15:22:05 2006 +0200
    12.3 @@ -27,8 +27,6 @@
    12.4  definition
    12.5    swap :: "'a * 'b \<Rightarrow> 'b * 'a"
    12.6    "swap p = (let (x, y) = p in (y, x))"
    12.7 -  swapp :: "'a * 'b \<Rightarrow> 'c * 'd \<Rightarrow> ('a * 'c) * ('b * 'd)"
    12.8 -  "swapp = (\<lambda>(x, y) (z, w). ((x, z), (y, w)))"
    12.9    appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
   12.10    "appl p = (let (f, x) = p in f x)"
   12.11  
   12.12 @@ -91,8 +89,14 @@
   12.13    h "Mymod.A.B.f"
   12.14  
   12.15  code_gen xor
   12.16 -code_gen one "0::nat" "1::nat"
   12.17 -code_gen "0::int" "1::int" n fac
   12.18 +code_gen one
   12.19 +code_gen "0::int" "1::int"
   12.20 +  (SML) (Haskell)
   12.21 +code_gen n
   12.22 +  (SML) (Haskell)
   12.23 +code_gen fac
   12.24 +  (SML) (Haskell)
   12.25 +code_gen n
   12.26    (SML) (Haskell)
   12.27  code_gen
   12.28    "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   12.29 @@ -101,7 +105,9 @@
   12.30    "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
   12.31    "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
   12.32  code_gen
   12.33 -  Pair fst snd Let split swap swapp appl
   12.34 +  Pair fst snd Let split swap
   12.35 +code_gen
   12.36 +  appl
   12.37  code_gen
   12.38    k
   12.39    "op + :: int \<Rightarrow> int \<Rightarrow> int"
   12.40 @@ -122,43 +128,31 @@
   12.41  code_gen
   12.42    mut1 mut2
   12.43  code_gen
   12.44 -  "op @" filter concat foldl foldr hd tl
   12.45 -  last butlast list_all2
   12.46 -  map 
   12.47 -  nth 
   12.48 -  list_update
   12.49 -  take
   12.50 -  drop
   12.51 -  takeWhile
   12.52 -  dropWhile
   12.53 -  rev
   12.54 -  zip
   12.55 -  upt
   12.56 -  remdups
   12.57    remove1
   12.58    null
   12.59 -  "distinct"
   12.60    replicate
   12.61    rotate1
   12.62    rotate
   12.63    splice
   12.64 -  (SML) (Haskell)
   12.65 +code_gen
   12.66 +  remdups
   12.67 +  "distinct"
   12.68  code_gen
   12.69    foo1 foo3
   12.70  code_gen
   12.71 -  "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
   12.72 -  "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
   12.73 -  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
   12.74 -  "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   12.75 -  "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   12.76 -  "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
   12.77 -  "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   12.78 -  "op = :: point \<Rightarrow> point \<Rightarrow> bool"
   12.79 -  "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   12.80 -  "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   12.81 +  "OperationalEquality.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
   12.82 +  "OperationalEquality.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
   12.83 +  "OperationalEquality.eq :: int \<Rightarrow> int \<Rightarrow> bool"
   12.84 +  "OperationalEquality.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   12.85 +  "OperationalEquality.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   12.86 +  "OperationalEquality.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
   12.87 +  "OperationalEquality.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
   12.88 +  "OperationalEquality.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   12.89 +  "OperationalEquality.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   12.90 +  "OperationalEquality.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
   12.91  code_gen
   12.92    f g h
   12.93  
   12.94 -code_gen (SML -)
   12.95 +code_gen (SML -) (SML _)
   12.96  
   12.97  end
   12.98 \ No newline at end of file
    13.1 --- a/src/HOL/ex/ROOT.ML	Tue Sep 19 15:22:03 2006 +0200
    13.2 +++ b/src/HOL/ex/ROOT.ML	Tue Sep 19 15:22:05 2006 +0200
    13.3 @@ -6,7 +6,6 @@
    13.4  
    13.5  no_document time_use_thy "Classpackage";
    13.6  no_document time_use_thy "Codegenerator";
    13.7 -no_document time_use_thy "CodeOperationalEquality";
    13.8  no_document time_use_thy "CodeCollections";
    13.9  no_document time_use_thy "CodeEval";
   13.10  no_document time_use_thy "CodeRandom";
    14.1 --- a/src/Pure/IsaMakefile	Tue Sep 19 15:22:03 2006 +0200
    14.2 +++ b/src/Pure/IsaMakefile	Tue Sep 19 15:22:05 2006 +0200
    14.3 @@ -59,9 +59,9 @@
    14.4    Tools/am_interpreter.ML Tools/am_util.ML	\
    14.5    Tools/codegen_consts.ML	\
    14.6    Tools/codegen_names.ML	\
    14.7 -  Tools/class_package.ML		\
    14.8 +  Tools/class_package.ML Tools/codegen_data.ML	\
    14.9    Tools/codegen_package.ML Tools/codegen_serializer.ML				\
   14.10 -  Tools/codegen_theorems.ML Tools/codegen_simtype.ML				\
   14.11 +  Tools/codegen_funcgr.ML Tools/codegen_simtype.ML				\
   14.12    Tools/codegen_thingol.ML Tools/compute.ML					\
   14.13    Tools/invoke.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML		\
   14.14    assumption.ML axclass.ML codegen.ML compress.ML conjunction.ML consts.ML	\