tuned
authorhaftmann
Mon Oct 02 23:00:51 2006 +0200 (2006-10-02)
changeset 2083527d049062b56
parent 20834 9a24a9121e58
child 20836 9e40d815e002
tuned
src/HOL/Integ/NatBin.thy
src/HOL/OperationalEquality.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/ex/CodeEval.thy
src/Pure/Tools/codegen_funcgr.ML
src/Pure/Tools/codegen_names.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_thingol.ML
     1.1 --- a/src/HOL/Integ/NatBin.thy	Mon Oct 02 23:00:50 2006 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Mon Oct 02 23:00:51 2006 +0200
     1.3 @@ -790,7 +790,7 @@
     1.4  
     1.5  val nat_number_expand = thms "nat_number_expand";
     1.6  
     1.7 -fun elim_number_of_nat thy thms =
     1.8 +fun elim_number_of_nat thy ts =
     1.9    let
    1.10      fun bins_of (Const _) =
    1.11            I
    1.12 @@ -809,22 +809,19 @@
    1.13              | (t', ts) => bins_of t' #> fold bins_of ts;
    1.14      val simpset =
    1.15        HOL_basic_ss addsimps nat_number_expand;
    1.16 -    val rewrites  =
    1.17 -      []
    1.18 -      |> (fold o Drule.fold_terms) bins_of thms
    1.19 -      |> map (Simplifier.rewrite simpset o Thm.cterm_of thy);
    1.20 -  in if null rewrites then thms else
    1.21 -    map (CodegenData.rewrite_func rewrites) thms
    1.22 +  in
    1.23 +    []
    1.24 +    |> fold (bins_of o Thm.term_of) ts
    1.25 +    |> map (Simplifier.rewrite simpset o Thm.cterm_of thy)
    1.26    end;
    1.27  
    1.28  end;
    1.29  *}
    1.30  
    1.31  setup {*
    1.32 -  CodegenData.add_preproc NumeralNat.elim_number_of_nat
    1.33 +  CodegenData.add_inline_proc NumeralNat.elim_number_of_nat
    1.34  *}
    1.35  
    1.36 -
    1.37  subsection {* legacy ML bindings *}
    1.38  
    1.39  ML
     2.1 --- a/src/HOL/OperationalEquality.thy	Mon Oct 02 23:00:50 2006 +0200
     2.2 +++ b/src/HOL/OperationalEquality.thy	Mon Oct 02 23:00:51 2006 +0200
     2.3 @@ -18,17 +18,6 @@
     2.4  defs
     2.5    eq_def: "eq x y \<equiv> (x = y)"
     2.6  
     2.7 -ML {*
     2.8 -local
     2.9 -  val thy = the_context ();
    2.10 -  val const_eq = Sign.intern_const thy "eq";
    2.11 -  val type_bool = Type (Sign.intern_type thy "bool", []);
    2.12 -in
    2.13 -  val eq_def_sym = Thm.symmetric (thm "eq_def");
    2.14 -  val class_eq = Sign.intern_class thy "eq";
    2.15 -end
    2.16 -*}
    2.17 -
    2.18  
    2.19  subsection {* bool type *}
    2.20  
    2.21 @@ -47,31 +36,24 @@
    2.22    "eq p False = (\<not> p)" unfolding eq_def by auto
    2.23  
    2.24  
    2.25 -subsection {* preprocessor *}
    2.26 +subsection {* code generator setup *}
    2.27  
    2.28 -ML {*
    2.29 -fun constrain_op_eq thy thms =
    2.30 -  let
    2.31 -    fun add_eq (Const ("op =", ty)) =
    2.32 -          fold (insert (eq_fst (op = : indexname * indexname -> bool)))
    2.33 -            (Term.add_tvarsT ty [])
    2.34 -      | add_eq _ =
    2.35 -          I
    2.36 -    val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
    2.37 -    val instT = map (fn (v_i, sort) =>
    2.38 -      (Thm.ctyp_of thy (TVar (v_i, sort)),
    2.39 -         Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
    2.40 -  in
    2.41 -    thms
    2.42 -    |> map (Thm.instantiate (instT, []))
    2.43 -  end;
    2.44 -*}
    2.45 -
    2.46 -
    2.47 -subsection {* codegenerator setup *}
    2.48 +subsubsection {* preprocessor *}
    2.49  
    2.50  setup {*
    2.51 -  CodegenData.add_preproc constrain_op_eq
    2.52 +let
    2.53 +  val class_eq = "OperationalEquality.eq";
    2.54 +  fun constrain_op_eq thy ts =
    2.55 +    let
    2.56 +      fun add_eq (Const ("op =", ty)) =
    2.57 +            fold (insert (eq_fst (op = : indexname * indexname -> bool)))
    2.58 +              (Term.add_tvarsT ty [])
    2.59 +        | add_eq _ =
    2.60 +            I
    2.61 +      val eqs = (fold o fold_aterms) add_eq ts [];
    2.62 +      val inst = map (fn (v_i, _) => (v_i, [class_eq])) eqs;
    2.63 +    in inst end;
    2.64 +in CodegenData.add_constrains constrain_op_eq end
    2.65  *}
    2.66  
    2.67  declare eq_def [symmetric, code inline]
     3.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Oct 02 23:00:50 2006 +0200
     3.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Oct 02 23:00:51 2006 +0200
     3.3 @@ -9,10 +9,8 @@
     3.4  sig
     3.5    val get_eq: theory -> string -> thm list
     3.6    val get_eq_datatype: theory -> string -> thm list
     3.7 -  val get_eq_typecopy: theory -> string -> thm list
     3.8    val get_cert: theory -> bool * string -> thm list
     3.9    val get_cert_datatype: theory -> string -> thm list
    3.10 -  val get_cert_typecopy: theory -> string -> thm list
    3.11    val dest_case_expr: theory -> term
    3.12      -> ((string * typ) list * ((term * typ) * (term * term) list)) option
    3.13    val add_datatype_case_const: string -> theory -> theory
    3.14 @@ -29,11 +27,13 @@
    3.15    val get_codetypes_arities: theory -> (string * bool) list -> sort
    3.16      -> (string * (((string * sort list) * sort) * term list)) list option
    3.17    val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort
    3.18 -    -> (theory -> ((string * sort list) * sort) list -> (string * term list) list
    3.19 -    -> ((bstring * attribute list) * term) list) -> (theory -> theory) -> theory -> theory
    3.20 +    -> (((string * sort list) * sort) list -> (string * term list) list -> theory
    3.21 +    -> ((bstring * attribute list) * term) list * theory)
    3.22 +    -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory)
    3.23 +    -> theory -> theory
    3.24  
    3.25    val setup: theory -> theory
    3.26 -  val setup2: theory -> theory
    3.27 +  val setup_hooks: theory -> theory
    3.28  end;
    3.29  
    3.30  structure DatatypeCodegen : DATATYPE_CODEGEN =
    3.31 @@ -364,7 +364,7 @@
    3.32          val names = Name.invents ctxt "a" (length tys);
    3.33          val ctxt' = fold Name.declare names ctxt;
    3.34          val vs = map2 (curry Free) names tys;
    3.35 -      in (vs, ctxt) end;
    3.36 +      in (vs, ctxt') end;
    3.37      fun mk_dist ((co1, tys1), (co2, tys2)) =
    3.38        let
    3.39          val ((xs1, xs2), _) = Name.context
    3.40 @@ -400,17 +400,39 @@
    3.41        |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    3.42        |> map (fn thm => not_eq_quodlibet OF [thm])
    3.43    in inject @ distinct end
    3.44 -and get_cert_typecopy thy dtco =
    3.45 -  let
    3.46 -    val SOME { inject, ... } = TypecopyPackage.get_typecopy_info thy dtco;
    3.47 -    val thm = Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [inject]);
    3.48 -  in
    3.49 -    [thm]
    3.50 -  end;
    3.51  end (*local*);
    3.52  
    3.53 -fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
    3.54 -  | get_cert thy (false, dtco) = get_cert_typecopy thy dtco;
    3.55 +local
    3.56 +  val not_sym = thm "HOL.not_sym";
    3.57 +  val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
    3.58 +in fun get_eq_datatype thy dtco =
    3.59 +  let
    3.60 +    val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
    3.61 +    fun mk_triv_inject co =
    3.62 +      let
    3.63 +        val ct' = Thm.cterm_of thy
    3.64 +          (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
    3.65 +        val cty' = Thm.ctyp_of_term ct';
    3.66 +        val refl = Thm.prop_of HOL.refl;
    3.67 +        val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
    3.68 +          (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
    3.69 +          refl NONE;
    3.70 +      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
    3.71 +    val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
    3.72 +    val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
    3.73 +    val ctxt = Context.init_proof thy;
    3.74 +    val simpset = Simplifier.context ctxt
    3.75 +      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
    3.76 +    val cos = map (fn (co, tys) =>
    3.77 +        (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
    3.78 +    val tac = ALLGOALS (simp_tac simpset)
    3.79 +      THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
    3.80 +    val distinct =
    3.81 +      mk_distinct cos
    3.82 +      |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    3.83 +      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
    3.84 +  in inject1 @ inject2 @ distinct end;
    3.85 +end (*local*);
    3.86  
    3.87  fun add_datatype_case_const dtco thy =
    3.88    let
    3.89 @@ -429,8 +451,7 @@
    3.90  
    3.91  (** codetypes for code 2nd generation **)
    3.92  
    3.93 -type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
    3.94 -  -> theory -> theory;
    3.95 +(* abstraction over datatypes vs. type copies *)
    3.96  
    3.97  fun codetypes_dependency thy =
    3.98    let
    3.99 @@ -461,23 +482,54 @@
   3.100      |> map (AList.make (the o AList.lookup (op =) names))
   3.101    end;
   3.102  
   3.103 -fun mk_typecopy_spec ({ vs, constr, typ, ... } : TypecopyPackage.info) =
   3.104 -  (vs, [(constr, [typ])]);
   3.105 -
   3.106  fun get_spec thy (dtco, true) =
   3.107        (the o DatatypePackage.get_datatype_spec thy) dtco
   3.108    | get_spec thy (tyco, false) =
   3.109 -      (mk_typecopy_spec o the o TypecopyPackage.get_typecopy_info thy) tyco;
   3.110 +      TypecopyPackage.get_spec thy tyco;
   3.111 +
   3.112 +fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
   3.113 +  | get_cert thy (false, dtco) = [TypecopyPackage.get_cert thy dtco];
   3.114  
   3.115 -fun add_spec thy (tyco, is_dt) =
   3.116 -  (tyco, (is_dt, get_spec thy (tyco, is_dt)));
   3.117 +local
   3.118 +  val eq_def_sym = thm "eq_def" |> Thm.symmetric;
   3.119 +  val class_eq = "OperationalEquality.eq";
   3.120 +  fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
   3.121 +   of SOME _ => get_eq_datatype thy tyco
   3.122 +    | NONE => [TypecopyPackage.get_eq thy tyco];
   3.123 +  fun constrain_op_eq_thms thy thms =
   3.124 +    let
   3.125 +      fun add_eq (Const ("op =", ty)) =
   3.126 +            fold (insert (eq_fst (op =)))
   3.127 +              (Term.add_tvarsT ty [])
   3.128 +        | add_eq _ =
   3.129 +            I
   3.130 +      val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
   3.131 +      val instT = map (fn (v_i, sort) =>
   3.132 +        (Thm.ctyp_of thy (TVar (v_i, sort)),
   3.133 +           Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
   3.134 +    in
   3.135 +      thms
   3.136 +      |> map (Thm.instantiate (instT, []))
   3.137 +    end;
   3.138 +in
   3.139 +  fun get_eq thy tyco =
   3.140 +    get_eq_thms thy tyco
   3.141 +    |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
   3.142 +    |> constrain_op_eq_thms thy
   3.143 +    |> map (Tactic.rewrite_rule [eq_def_sym])
   3.144 +end;
   3.145 +
   3.146 +type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
   3.147 +  -> theory -> theory;
   3.148  
   3.149  fun add_codetypes_hook_bootstrap hook thy =
   3.150    let
   3.151 +    fun add_spec thy (tyco, is_dt) =
   3.152 +      (tyco, (is_dt, get_spec thy (tyco, is_dt)));
   3.153      fun datatype_hook dtcos thy =
   3.154        hook (map (add_spec thy) (map (rpair true) dtcos)) thy;
   3.155 -    fun typecopy_hook ((tyco, info )) thy =
   3.156 -      hook ([(tyco, (false, mk_typecopy_spec info))]) thy;
   3.157 +    fun typecopy_hook ((tyco, _)) thy =
   3.158 +      hook ([(tyco, (false, TypecopyPackage.get_spec thy tyco))]) thy;
   3.159    in
   3.160      thy
   3.161      |> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy))
   3.162 @@ -498,6 +550,23 @@
   3.163          val (vs::_, css) = split_list (map (the o DatatypePackage.get_datatype_spec thy) tycos);
   3.164        in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end;
   3.165  
   3.166 +
   3.167 +(* registering code types in code generator *)
   3.168 +
   3.169 +fun codetype_hook specs =
   3.170 +  let
   3.171 +    fun add (dtco, (flag, spec)) thy =
   3.172 +      let
   3.173 +        fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
   3.174 +      in
   3.175 +        CodegenData.add_datatype
   3.176 +          (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
   3.177 +      end;
   3.178 +  in fold add specs end;
   3.179 +
   3.180 +
   3.181 +(* instrumentalizing the sort algebra *)
   3.182 +
   3.183  fun get_codetypes_arities thy tycos sort =
   3.184    let
   3.185      val algebra = Sign.classes_of thy;
   3.186 @@ -538,114 +607,35 @@
   3.187              then NONE else SOME (arity, (tyco, cs)))) insts;
   3.188        in
   3.189          thy
   3.190 -        |> K ((not o null) arities) ? (ClassPackage.prove_instance_arity tac
   3.191 -             arities ("", []) (f thy arities css) #> after_qed)
   3.192 +        |> K ((not o null) arities) ? (
   3.193 +            f arities css
   3.194 +            #-> (fn defs =>
   3.195 +              ClassPackage.prove_instance_arity tac arities ("", []) defs
   3.196 +            #> after_qed arities css))
   3.197        end;
   3.198  
   3.199 +
   3.200 +(* operational equality *)
   3.201 +
   3.202  local
   3.203    val class_eq = "OperationalEquality.eq";
   3.204 -in fun add_eq_instance specs =
   3.205 -  prove_codetypes_arities
   3.206 -    (K (ClassPackage.intro_classes_tac []))
   3.207 -    (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   3.208 -    [class_eq] ((K o K o K) [])
   3.209 -end; (*local*)
   3.210 -
   3.211 -local
   3.212 -  val not_sym = thm "HOL.not_sym";
   3.213 -  val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
   3.214 -in fun get_eq_datatype thy dtco =
   3.215 +in fun eq_hook specs =
   3.216    let
   3.217 -(*     val _ = writeln "01";  *)
   3.218 -    val SOME (vs, cs) = DatatypePackage.get_datatype_spec (Context.check_thy thy) dtco;
   3.219 -(*     val _ = writeln "02";  *)
   3.220 -    fun mk_triv_inject co =
   3.221 +    fun add_eq_thms (dtco, (_, (vs, cs))) thy =
   3.222        let
   3.223 -        val ct' = Thm.cterm_of (Context.check_thy thy)
   3.224 -          (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
   3.225 -        val cty' = Thm.ctyp_of_term ct';
   3.226 -        val refl = Thm.prop_of HOL.refl;
   3.227 -        val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
   3.228 -          (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)
   3.229 -          refl NONE;
   3.230 -      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
   3.231 -(*     val _ = writeln "03";  *)
   3.232 -    val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
   3.233 -(*     val _ = writeln "04";  *)
   3.234 -    val inject2 = (#inject o DatatypePackage.the_datatype (Context.check_thy thy)) dtco;
   3.235 -(*     val _ = writeln "05";  *)
   3.236 -    val ctxt = Context.init_proof (Context.check_thy thy);
   3.237 -(*     val _ = writeln "06";  *)
   3.238 -    val simpset = Simplifier.context ctxt
   3.239 -      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
   3.240 -(*     val _ = writeln "07";  *)
   3.241 -    val cos = map (fn (co, tys) =>
   3.242 -        (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
   3.243 -    val tac = ALLGOALS (simp_tac simpset)
   3.244 -      THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
   3.245 -(*     val _ = writeln "08";  *)
   3.246 -    val distinct =
   3.247 -      mk_distinct cos
   3.248 -      |> map (fn t => Goal.prove_global (Context.check_thy thy) [] [] t (K tac))
   3.249 -      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
   3.250 -(*     val _ = writeln "09";  *)
   3.251 -  in inject1 @ inject2 @ distinct end;
   3.252 -
   3.253 -fun get_eq_typecopy thy tyco =
   3.254 -  case TypecopyPackage.get_typecopy_info thy tyco
   3.255 -   of SOME { inject, ... } => [inject]
   3.256 -    | NONE => [];
   3.257 -
   3.258 -local
   3.259 -  val lift_not_thm = thm "HOL.Eq_FalseI";
   3.260 -  val lift_thm = thm "HOL.eq_reflection";
   3.261 -  val eq_def_sym = thm "eq_def" |> Thm.symmetric;
   3.262 -  fun get_eq_thms thy tyco = case DatatypePackage.get_datatype (Context.check_thy thy) tyco
   3.263 -   of SOME _ => get_eq_datatype (Context.check_thy thy) tyco
   3.264 -    | NONE => case TypecopyPackage.get_typecopy_info thy tyco
   3.265 -       of SOME _ => get_eq_typecopy thy tyco
   3.266 -        | NONE => [];
   3.267 -in
   3.268 -  fun get_eq thy tyco =
   3.269 -    get_eq_thms (Context.check_thy thy) tyco
   3.270 -(*     |> tap (fn _ => writeln "10")  *)
   3.271 -    |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) (Context.check_thy thy))
   3.272 -(*     |> tap (fn _ => writeln "11")  *)
   3.273 -    |> constrain_op_eq (Context.check_thy thy)
   3.274 -(*     |> tap (fn _ => writeln "12")  *)
   3.275 -    |> map (Tactic.rewrite_rule [eq_def_sym])
   3.276 -(*     |> tap (fn _ => writeln "13")  *)
   3.277 -end;
   3.278 -
   3.279 -end;
   3.280 -
   3.281 -fun add_eq_thms (dtco, (_, (vs, cs))) thy =
   3.282 -  let
   3.283 -    val thy_ref = Theory.self_ref thy;
   3.284 -    val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
   3.285 -    val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
   3.286 -    val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
   3.287 -  in
   3.288 -    CodegenData.add_funcl
   3.289 -      (c, CodegenData.lazy get_thms) thy
   3.290 -  end;
   3.291 -
   3.292 -fun codetype_hook dtcos theory =
   3.293 -  let
   3.294 -    fun add (dtco, (flag, spec)) thy =
   3.295 -      let
   3.296 -        fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
   3.297 +        val thy_ref = Theory.self_ref thy;
   3.298 +        val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
   3.299 +        val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
   3.300 +        val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
   3.301        in
   3.302 -        CodegenData.add_datatype
   3.303 -          (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
   3.304 +        CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
   3.305        end;
   3.306    in
   3.307 -    theory
   3.308 -    |> fold add dtcos
   3.309 +    prove_codetypes_arities (K (ClassPackage.intro_classes_tac []))
   3.310 +      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   3.311 +      [class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
   3.312    end;
   3.313 -
   3.314 -fun eq_hook dtcos =
   3.315 -  add_eq_instance dtcos (fold add_eq_thms dtcos);
   3.316 +end; (*local*)
   3.317  
   3.318  
   3.319  
   3.320 @@ -657,7 +647,7 @@
   3.321    #> DatatypeHooks.add (fold add_datatype_case_const)
   3.322    #> DatatypeHooks.add (fold add_datatype_case_defs)
   3.323  
   3.324 -val setup2 =
   3.325 +val setup_hooks =
   3.326    add_codetypes_hook_bootstrap codetype_hook
   3.327    #> add_codetypes_hook_bootstrap eq_hook
   3.328  
     4.1 --- a/src/HOL/Tools/typecopy_package.ML	Mon Oct 02 23:00:50 2006 +0200
     4.2 +++ b/src/HOL/Tools/typecopy_package.ML	Mon Oct 02 23:00:51 2006 +0200
     4.3 @@ -19,8 +19,11 @@
     4.4      -> theory -> (string * info) * theory
     4.5    val get_typecopies: theory -> string list
     4.6    val get_typecopy_info: theory -> string -> info option
     4.7 -  type hook = string * info -> theory -> theory;
     4.8 -  val add_hook: hook -> theory -> theory;
     4.9 +  type hook = string * info -> theory -> theory
    4.10 +  val add_hook: hook -> theory -> theory
    4.11 +  val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
    4.12 +  val get_cert: theory -> string -> thm
    4.13 +  val get_eq: theory -> string -> thm
    4.14    val print: theory -> unit
    4.15    val setup: theory -> theory
    4.16  end;
    4.17 @@ -134,7 +137,28 @@
    4.18  end; (*local*)
    4.19  
    4.20  
    4.21 -(* hooks for projection function code *)
    4.22 +(* equality function equation *)
    4.23 +
    4.24 +fun get_eq thy tyco =
    4.25 +  (#inject o the o get_typecopy_info thy) tyco;
    4.26 +
    4.27 +
    4.28 +(* datatype specification and certificate *)
    4.29 +
    4.30 +fun get_spec thy tyco =
    4.31 +  let
    4.32 +    val SOME { vs, constr, typ, ... } = get_typecopy_info thy tyco
    4.33 +  in (vs, [(constr, [typ])]) end;
    4.34 +
    4.35 +local
    4.36 +  val bool_eq_implies = thm "iffD1";
    4.37 +  val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
    4.38 +in fun get_cert thy tyco =
    4.39 +  Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
    4.40 +end; (*local*)
    4.41 +
    4.42 +
    4.43 +(* hook for projection function code *)
    4.44  
    4.45  fun add_project (_ , { proj_def, ...} : info) =
    4.46    CodegenData.add_func proj_def;
     5.1 --- a/src/HOL/ex/CodeEval.thy	Mon Oct 02 23:00:50 2006 +0200
     5.2 +++ b/src/HOL/ex/CodeEval.thy	Mon Oct 02 23:00:51 2006 +0200
     5.3 @@ -39,15 +39,14 @@
     5.4  
     5.5  setup {*
     5.6  let
     5.7 -  fun mk thy arities _ =
     5.8 -    maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def
     5.9 -      (Type (tyco, map TFree (Name.names Name.context "'a" asorts)))
    5.10 -      |> tap (writeln o Sign.string_of_term thy))]) arities;
    5.11 +  fun mk arities _ thy =
    5.12 +    (maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def
    5.13 +      (Type (tyco, map TFree (Name.names Name.context "'a" asorts))))]) arities, thy);
    5.14    fun tac _ = ClassPackage.intro_classes_tac [];
    5.15    fun hook specs =
    5.16      DatatypeCodegen.prove_codetypes_arities tac
    5.17        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    5.18 -      [TypOf.class_typ_of] mk I
    5.19 +      [TypOf.class_typ_of] mk ((K o K) I)
    5.20  in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
    5.21  *}
    5.22  
    5.23 @@ -90,19 +89,27 @@
    5.24  
    5.25  setup {*
    5.26  let
    5.27 -  fun mk thy arities css =
    5.28 +  fun thy_note ((name, atts), thms) =
    5.29 +    PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
    5.30 +  fun thy_def ((name, atts), t) =
    5.31 +    PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
    5.32 +  fun mk arities css thy =
    5.33      let
    5.34        val vs = (Name.names Name.context "'a" o snd o fst o hd) arities;
    5.35 -      val raw_defs = map (TermOf.mk_terms_of_defs vs) css;
    5.36 -      fun mk' thy' = map (apfst (rpair [])) ((PrimrecPackage.mk_combdefs thy' o flat) raw_defs)
    5.37 -    in ClassPackage.assume_arities_thy thy arities mk' end;
    5.38 +      val defs = map (TermOf.mk_terms_of_defs vs) css;
    5.39 +      val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs;
    5.40 +    in
    5.41 +      thy
    5.42 +      |> PrimrecPackage.gen_primrec thy_note thy_def "" defs'
    5.43 +      |> snd
    5.44 +    end;
    5.45    fun tac _ = ClassPackage.intro_classes_tac [];
    5.46    fun hook specs =
    5.47      if (fst o hd) specs = (fst o dest_Type) Embed.typ_typ then I
    5.48      else
    5.49        DatatypeCodegen.prove_codetypes_arities tac
    5.50        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    5.51 -      [TermOf.class_term_of] mk I
    5.52 +      [TermOf.class_term_of] ((K o K o pair) []) mk
    5.53  in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
    5.54  *}
    5.55  
     6.1 --- a/src/Pure/Tools/codegen_funcgr.ML	Mon Oct 02 23:00:50 2006 +0200
     6.2 +++ b/src/Pure/Tools/codegen_funcgr.ML	Mon Oct 02 23:00:51 2006 +0200
     6.3 @@ -9,9 +9,10 @@
     6.4  sig
     6.5    type T;
     6.6    val mk_funcgr: theory -> CodegenConsts.const list -> (string * typ) list -> T
     6.7 +  val all_deps_of: T -> CodegenConsts.const list -> CodegenConsts.const list list
     6.8    val get_funcs: T -> CodegenConsts.const -> thm list
     6.9    val get_func_typs: T -> (CodegenConsts.const * typ) list
    6.10 -  val preprocess: theory -> thm list -> thm list
    6.11 +  val normalize: theory -> thm list -> thm list
    6.12    val print_codethms: theory -> CodegenConsts.const list -> unit
    6.13  end;
    6.14  
    6.15 @@ -98,7 +99,7 @@
    6.16      val (_, _, inst) = fold mk_inst (vars_of thm) (maxidx + 1, [], []);
    6.17    in Thm.instantiate ([], inst) thm end;
    6.18  
    6.19 -fun preprocess thy thms =
    6.20 +fun normalize thy thms =
    6.21    let
    6.22      fun burrow_thms f [] = []
    6.23        | burrow_thms f thms =
    6.24 @@ -110,7 +111,6 @@
    6.25        #2 (#1 (Variable.import true thms (ProofContext.init thy)));
    6.26    in
    6.27      thms
    6.28 -    |> CodegenData.preprocess thy
    6.29      |> map (abs_norm thy)
    6.30      |> burrow_thms (
    6.31          canonical_tvars thy
    6.32 @@ -119,43 +119,25 @@
    6.33         )
    6.34    end;
    6.35  
    6.36 -fun check_thms c thms =
    6.37 -  let
    6.38 -    fun check_head_lhs thm (lhs, rhs) =
    6.39 -      case strip_comb lhs
    6.40 -       of (Const (c', _), _) => if c' = c then ()
    6.41 -           else error ("Illegal function equation for " ^ quote c
    6.42 -             ^ ", actually defining " ^ quote c' ^ ": " ^ Display.string_of_thm thm)
    6.43 -        | _ => error ("Illegal function equation: " ^ Display.string_of_thm thm);
    6.44 -    fun check_vars_lhs thm (lhs, rhs) =
    6.45 -      if has_duplicates (op =)
    6.46 -          (fold_aterms (fn Free (v, _) => cons v | _ => I) lhs [])
    6.47 -      then error ("Repeated variables on left hand side of function equation:"
    6.48 -        ^ Display.string_of_thm thm)
    6.49 -      else ();
    6.50 -    fun check_vars_rhs thm (lhs, rhs) =
    6.51 -      if null (subtract (op =)
    6.52 -        (fold_aterms (fn Free (v, _) => cons v | _ => I) lhs [])
    6.53 -        (fold_aterms (fn Free (v, _) => cons v | _ => I) rhs []))
    6.54 -      then ()
    6.55 -      else error ("Free variables on right hand side of function equation:"
    6.56 -        ^ Display.string_of_thm thm)
    6.57 -    val tts = map (Logic.dest_equals o Logic.unvarify o Thm.prop_of) thms;
    6.58 -  in
    6.59 -    (map2 check_head_lhs thms tts; map2 check_vars_lhs thms tts;
    6.60 -      map2 check_vars_rhs thms tts; thms)
    6.61 -  end;
    6.62 -
    6.63  
    6.64  
    6.65  (** retrieval **)
    6.66  
    6.67  fun get_funcs funcgr (c_tys as (c, _)) =
    6.68 -  (check_thms c o these o Option.map snd o try (Constgraph.get_node funcgr)) c_tys;
    6.69 +  (these o Option.map snd o try (Constgraph.get_node funcgr)) c_tys;
    6.70  
    6.71  fun get_func_typs funcgr =
    6.72    AList.make (fst o Constgraph.get_node funcgr) (Constgraph.keys funcgr);
    6.73  
    6.74 +fun all_deps_of funcgr cs =
    6.75 +  let
    6.76 +    val conn = Constgraph.strong_conn funcgr;
    6.77 +    val order = rev conn;
    6.78 +  in
    6.79 +    (map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order
    6.80 +    |> filter_out null
    6.81 +  end;
    6.82 +
    6.83  local
    6.84  
    6.85  fun add_things_of thy f (c, thms) =
    6.86 @@ -234,7 +216,7 @@
    6.87      |> Constgraph.new_node (c, [])
    6.88      |> pair (SOME c)
    6.89    else let
    6.90 -    val thms = preprocess thy (CodegenData.these_funcs thy c);
    6.91 +    val thms = normalize thy (CodegenData.these_funcs thy c);
    6.92      val rhs = rhs_of thy (c, thms);
    6.93    in
    6.94      auxgr
     7.1 --- a/src/Pure/Tools/codegen_names.ML	Mon Oct 02 23:00:50 2006 +0200
     7.2 +++ b/src/Pure/Tools/codegen_names.ML	Mon Oct 02 23:00:51 2006 +0200
     7.3 @@ -236,33 +236,7 @@
     7.4  
     7.5  (* explicit given names with cache update *)
     7.6  
     7.7 -fun tyco_force (tyco, name) thy =
     7.8 -  let
     7.9 -    val names = NameSpace.unpack name;
    7.10 -    val (prefix, base) = split_last (NameSpace.unpack name);
    7.11 -    val prefix' = purify_prefix prefix;
    7.12 -    val base' = purify_base base;
    7.13 -    val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
    7.14 -      then ()
    7.15 -      else
    7.16 -        error ("Name violates naming conventions: " ^ quote name
    7.17 -          ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
    7.18 -    val names_ref = CodeName.get thy;
    7.19 -    val (Names names) = ! names_ref;
    7.20 -    val (tycotab, tycorev) = #tyco names;
    7.21 -    val _ = if Symtab.defined tycotab tyco
    7.22 -      then error ("Type constructor already named: " ^ quote tyco)
    7.23 -      else ();
    7.24 -    val _ = if Symtab.defined tycorev name
    7.25 -      then error ("Name already given to type constructor: " ^ quote name)
    7.26 -      else ();
    7.27 -    val _ = names_ref := map_tyco (K (Symtab.update_new (tyco, name) tycotab,
    7.28 -          Symtab.update_new (name, tyco) tycorev)) (Names names);
    7.29 -  in
    7.30 -    thy
    7.31 -  end;
    7.32 -
    7.33 -fun const_force (c_tys as (c, _), name) thy =
    7.34 +fun force get defined upd_names upd errname string_of (x, name) thy =
    7.35    let
    7.36      val names = NameSpace.unpack name;
    7.37      val (prefix, base) = split_last (NameSpace.unpack name);
    7.38 @@ -275,44 +249,25 @@
    7.39            ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
    7.40      val names_ref = CodeName.get thy;
    7.41      val (Names names) = ! names_ref;
    7.42 -    val (const, constrev) = #const names;
    7.43 -    val _ = if Consttab.defined const c_tys
    7.44 -      then error ("Constant already named: " ^ quote (CodegenConsts.string_of_const thy c_tys))
    7.45 +    val (tab, rev) = get names;
    7.46 +    val _ = if defined tab x
    7.47 +      then error ("Already named " ^ errname  ^ ": " ^ string_of thy x)
    7.48        else ();
    7.49 -    val _ = if Symtab.defined constrev name
    7.50 -      then error ("Name already given to constant: " ^ quote name)
    7.51 +    val _ = if Symtab.defined rev name
    7.52 +      then error ("Name already given to other " ^ errname ^ ": " ^ quote name)
    7.53        else ();
    7.54 -    val _ = names_ref := map_const (K (Consttab.update_new (c_tys, name) const,
    7.55 -          Symtab.update_new (name, c_tys) constrev)) (Names names);
    7.56 +    val _ = names_ref := upd_names (K (upd (x, name) tab,
    7.57 +          Symtab.update_new (name, x) rev)) (Names names);
    7.58    in
    7.59      thy
    7.60    end;
    7.61  
    7.62 -fun instance_force (instance, name) thy =
    7.63 -  let
    7.64 -    val names = NameSpace.unpack name;
    7.65 -    val (prefix, base) = split_last (NameSpace.unpack name);
    7.66 -    val prefix' = purify_prefix prefix;
    7.67 -    val base' = purify_base base;
    7.68 -    val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
    7.69 -      then ()
    7.70 -      else
    7.71 -        error ("Name violates naming conventions: " ^ quote name
    7.72 -          ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
    7.73 -    val names_ref = CodeName.get thy;
    7.74 -    val (Names names) = ! names_ref;
    7.75 -    val (inst, instrev) = #instance names;
    7.76 -    val _ = if Insttab.defined inst instance
    7.77 -      then error ("Instance already named: " ^ quote (fst instance) ^ ", " ^ quote (snd instance))
    7.78 -      else ();
    7.79 -    val _ = if Symtab.defined instrev name
    7.80 -      then error ("Name already given to instance: " ^ quote name)
    7.81 -      else ();
    7.82 -    val _ = names_ref := map_inst (K (Insttab.update_new (instance, name) inst,
    7.83 -          Symtab.update_new (name, instance) instrev)) (Names names);
    7.84 -  in
    7.85 -    thy
    7.86 -  end;
    7.87 +val tyco_force = force #tyco Symtab.defined map_tyco Symtab.update_new
    7.88 +  "type constructor" (K quote);
    7.89 +val instance_force = force #instance Insttab.defined map_inst Insttab.update_new
    7.90 +  "instance" (fn _ => fn (class, tyco) => quote class ^ ", " ^ quote tyco);
    7.91 +val const_force = force #const Consttab.defined map_const Consttab.update_new
    7.92 +  "constant" (quote oo CodegenConsts.string_of_const);
    7.93  
    7.94  
    7.95  (* naming policies *)
    7.96 @@ -442,21 +397,21 @@
    7.97  val (constnameK, typenameK, instnameK) = ("code_constname", "code_typename", "code_instname");
    7.98  
    7.99  val constnameP =
   7.100 -  OuterSyntax.command constnameK "declare code name for constant" K.thy_decl (
   7.101 +  OuterSyntax.improper_command constnameK "declare code name for constant" K.thy_decl (
   7.102      Scan.repeat1 (P.term -- P.name)
   7.103      >> (fn aliasses =>
   7.104            Toplevel.theory (fold const_force_e aliasses))
   7.105    );
   7.106  
   7.107  val typenameP =
   7.108 -  OuterSyntax.command typenameK "declare code name for type constructor" K.thy_decl (
   7.109 +  OuterSyntax.improper_command typenameK "declare code name for type constructor" K.thy_decl (
   7.110      Scan.repeat1 (P.xname -- P.name)
   7.111      >> (fn aliasses =>
   7.112            Toplevel.theory (fold tyco_force_e aliasses))
   7.113    );
   7.114  
   7.115  val instnameP =
   7.116 -  OuterSyntax.command instnameK "declare code name for instance relation" K.thy_decl (
   7.117 +  OuterSyntax.improper_command instnameK "declare code name for instance relation" K.thy_decl (
   7.118      Scan.repeat1 ((P.xname --| P.$$$ "::" -- P.xname) -- P.name)
   7.119      >> (fn aliasses =>
   7.120            Toplevel.theory (fold instance_force_e aliasses))
     8.1 --- a/src/Pure/Tools/codegen_package.ML	Mon Oct 02 23:00:50 2006 +0200
     8.2 +++ b/src/Pure/Tools/codegen_package.ML	Mon Oct 02 23:00:51 2006 +0200
     8.3 @@ -16,7 +16,6 @@
     8.4  
     8.5    type appgen;
     8.6    val add_appconst: string * appgen -> theory -> theory;
     8.7 -  val appgen_default: appgen;
     8.8    val appgen_numeral: (theory -> term -> IntInf.int) -> appgen;
     8.9    val appgen_char: (term -> int option) -> appgen;
    8.10    val appgen_case: (theory -> term
    8.11 @@ -101,8 +100,6 @@
    8.12    | check_strict has_seri x (true, _) =
    8.13        true;
    8.14  
    8.15 -fun no_strict (_, targets) = (false, targets);
    8.16 -
    8.17  fun ensure_def_class thy algbr funcgr strct cls trns =
    8.18    let
    8.19      fun defgen_class thy (algbr as ((proj_sort, _), _)) funcgr strct cls trns =
    8.20 @@ -114,7 +111,7 @@
    8.21                val idfs = map (CodegenNames.const thy o CodegenConsts.norm_of_typ thy) cs;
    8.22              in
    8.23                trns
    8.24 -              |> debug_msg (fn _ => "trying defgen class declaration for " ^ quote cls)
    8.25 +              |> tracing (fn _ => "trying defgen class declaration for " ^ quote cls)
    8.26                |> fold_map (ensure_def_class thy algbr funcgr strct) superclasses
    8.27                ||>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs
    8.28                |-> (fn (supcls, memtypes) => succeed
    8.29 @@ -126,7 +123,7 @@
    8.30      val cls' = CodegenNames.class thy cls;
    8.31    in
    8.32      trns
    8.33 -    |> debug_msg (fn _ => "generating class " ^ quote cls)
    8.34 +    |> tracing (fn _ => "generating class " ^ quote cls)
    8.35      |> ensure_def (defgen_class thy algbr funcgr strct) true ("generating class " ^ quote cls) cls'
    8.36      |> pair cls'
    8.37    end
    8.38 @@ -140,7 +137,7 @@
    8.39           (case CodegenData.get_datatype thy dtco
    8.40               of SOME (vs, cos) =>
    8.41                    trns
    8.42 -                  |> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco)
    8.43 +                  |> tracing (fn _ => "trying defgen datatype for " ^ quote dtco)
    8.44                    |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
    8.45                    ||>> fold_map (fn (c, tys) =>
    8.46                      fold_map (exprgen_type thy algbr funcgr strct) tys
    8.47 @@ -156,7 +153,7 @@
    8.48              |> fail ("Not a type constructor: " ^ quote dtco)
    8.49    in
    8.50      trns
    8.51 -    |> debug_msg (fn _ => "generating type constructor " ^ quote tyco)
    8.52 +    |> tracing (fn _ => "generating type constructor " ^ quote tyco)
    8.53      |> ensure_def (defgen_datatype thy algbr funcgr strct) strict
    8.54          ("generating type constructor " ^ quote tyco) tyco'
    8.55      |> pair tyco'
    8.56 @@ -182,7 +179,7 @@
    8.57        ||>> fold_map (exprgen_type thy algbr funcgr strct) tys
    8.58        |-> (fn (tyco, tys) => pair (tyco `%% tys));
    8.59  
    8.60 -exception CONSTRAIN of ((string * typ) * typ) * term option;
    8.61 +exception CONSTRAIN of (string * typ) * typ;
    8.62  
    8.63  fun exprgen_typinst thy (algbr as ((proj_sort, algebra), consts)) funcgr strct (ty_ctxt, sort_decl) trns =
    8.64    let
    8.65 @@ -225,7 +222,7 @@
    8.66      val insts = (op ~~ o apsnd (map (snd o dest_TVar)) oo pairself)
    8.67        (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
    8.68      val _ = if exists not (map (Sign.of_sort thy) insts)
    8.69 -      then raise CONSTRAIN (((c, ty_decl), ty_ctxt), NONE) else ();
    8.70 +      then raise CONSTRAIN ((c, ty_decl), ty_ctxt) else ();
    8.71    in
    8.72      trns
    8.73      |> fold_map (exprgen_typinst thy algbr funcgr strct) insts
    8.74 @@ -251,7 +248,7 @@
    8.75                  ||>> exprgen_term thy algbr funcgr strct (Const (m, ty));
    8.76              in
    8.77                trns
    8.78 -              |> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls
    8.79 +              |> tracing (fn _ => "trying defgen class instance for (" ^ quote cls
    8.80                     ^ ", " ^ quote tyco ^ ")")
    8.81                |> ensure_def_class thy algbr funcgr strct class
    8.82                ||>> ensure_def_tyco thy algbr funcgr strct tyco
    8.83 @@ -266,7 +263,7 @@
    8.84      val inst = CodegenNames.instance thy (cls, tyco);
    8.85    in
    8.86      trns
    8.87 -    |> debug_msg (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
    8.88 +    |> tracing (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
    8.89      |> ensure_def (defgen_inst thy algbr funcgr strct) true
    8.90           ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
    8.91      |> pair inst
    8.92 @@ -277,7 +274,7 @@
    8.93        case CodegenData.get_datatype_of_constr thy ((the o CodegenNames.const_rev thy) co)
    8.94         of SOME tyco =>
    8.95              trns
    8.96 -            |> debug_msg (fn _ => "trying defgen datatype constructor for " ^ quote co)
    8.97 +            |> tracing (fn _ => "trying defgen datatype constructor for " ^ quote co)
    8.98              |> ensure_def_tyco thy algbr funcgr strct tyco
    8.99              |-> (fn _ => succeed Bot)
   8.100          | _ =>
   8.101 @@ -288,7 +285,7 @@
   8.102        case AxClass.class_of_param thy ((fst o the o CodegenNames.const_rev thy) m)
   8.103         of SOME class =>
   8.104              trns
   8.105 -            |> debug_msg (fn _ => "trying defgen class operation for " ^ quote m)
   8.106 +            |> tracing (fn _ => "trying defgen class operation for " ^ quote m)
   8.107              |> ensure_def_class thy algbr funcgr strct class
   8.108              |-> (fn _ => succeed Bot)
   8.109          | _ =>
   8.110 @@ -300,28 +297,16 @@
   8.111                val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
   8.112                val ty = (Logic.unvarifyT o CodegenData.typ_func thy) eq_thm;
   8.113                val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
   8.114 -              fun dest_eqthm eq_thm =
   8.115 -                let
   8.116 -                  val ((t, args), rhs) =
   8.117 -                    (apfst strip_comb o Logic.dest_equals o Logic.unvarify o prop_of) eq_thm;
   8.118 -                in case t
   8.119 -                 of Const (c', _) => if c' = c then (args, rhs)
   8.120 -                     else error ("Illegal function equation for " ^ quote c
   8.121 -                       ^ ", actually defining " ^ quote c')
   8.122 -                  | _ => error ("Illegal function equation for " ^ quote c)
   8.123 -                end;
   8.124 +              val dest_eqthm =
   8.125 +                apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;
   8.126                fun exprgen_eq (args, rhs) trns =
   8.127                  trns
   8.128                  |> fold_map (exprgen_term thy algbr funcgr strct) args
   8.129                  ||>> exprgen_term thy algbr funcgr strct rhs;
   8.130 -              fun checkvars (args, rhs) =
   8.131 -                if CodegenThingol.vars_distinct args then (args, rhs)
   8.132 -                else error ("Repeated variables on left hand side of function")
   8.133              in
   8.134                trns
   8.135                |> message msg (fn trns => trns
   8.136                |> fold_map (exprgen_eq o dest_eqthm) eq_thms
   8.137 -              |-> (fn eqs => pair (map checkvars eqs))
   8.138                ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
   8.139                ||>> exprgen_type thy algbr funcgr strct ty
   8.140                |-> (fn ((eqs, vs), ty) => succeed (Fun (eqs, (vs, ty)))))
   8.141 @@ -342,7 +327,7 @@
   8.142      val strict = check_strict (CodegenSerializer.const_has_serialization thy) idf strct;
   8.143    in
   8.144      trns
   8.145 -    |> debug_msg (fn _ => "generating constant "
   8.146 +    |> tracing (fn _ => "generating constant "
   8.147          ^ (quote o CodegenConsts.string_of_const thy) (c, tys))
   8.148      |> ensure_def (get_defgen funcgr strct idf) strict ("generating constant "
   8.149           ^ CodegenConsts.string_of_const thy (c, tys)) idf
   8.150 @@ -415,24 +400,18 @@
   8.151          |> appgen_default thy algbr funcgr strct ((f, ty), ts);
   8.152  
   8.153  
   8.154 -(* entry points into extraction kernel *)
   8.155 +(* entrance points into extraction kernel *)
   8.156  
   8.157  fun ensure_def_const' thy algbr funcgr strct c trns =
   8.158    ensure_def_const thy algbr funcgr strct c trns
   8.159 -  handle CONSTRAIN (((c, ty), ty_decl), NONE) => error (
   8.160 +  handle CONSTRAIN ((c, ty), ty_decl) => error (
   8.161      "Constant " ^ c ^ " with most general type\n"
   8.162      ^ Sign.string_of_typ thy ty
   8.163      ^ "\noccurs with type\n"
   8.164 -    ^ Sign.string_of_typ thy ty_decl)
   8.165 -  handle CONSTRAIN (((c, ty), ty_decl), SOME t) => error ("In term " ^ (quote o Sign.string_of_term thy) t
   8.166 -    ^ ",\nconstant " ^ c ^ " with most general type\n"
   8.167 -    ^ Sign.string_of_typ thy ty
   8.168 -    ^ "\noccurs with type\n"
   8.169      ^ Sign.string_of_typ thy ty_decl);
   8.170 -
   8.171  fun exprgen_term' thy algbr funcgr strct t trns =
   8.172    exprgen_term thy algbr funcgr strct t trns
   8.173 -  handle CONSTRAIN (((c, ty), ty_decl), _) => error ("In term " ^ (quote o Sign.string_of_term thy) t
   8.174 +  handle CONSTRAIN ((c, ty), ty_decl) => error ("In term " ^ (quote o Sign.string_of_term thy) t
   8.175      ^ ",\nconstant " ^ c ^ " with most general type\n"
   8.176      ^ Sign.string_of_typ thy ty
   8.177      ^ "\noccurs with type\n"
   8.178 @@ -444,16 +423,13 @@
   8.179  
   8.180  fun appgen_numeral int_of_numeral thy algbr funcgr strct (app as (c, ts)) trns =
   8.181    case try (int_of_numeral thy) (list_comb (Const c, ts))
   8.182 -   of SOME i => (*if i < 0 then (*preprocessor eliminates negative numerals*)
   8.183 +   of SOME i =>
   8.184          trns
   8.185 -        |> appgen_default thy algbr funcgr (no_strict strct) app
   8.186 -      else*)
   8.187 -        trns
   8.188 -        |> appgen_default thy algbr funcgr (no_strict strct) app
   8.189 +        |> appgen_default thy algbr funcgr strct app
   8.190          |-> (fn e => pair (CodegenThingol.INum (i, e)))
   8.191      | NONE =>
   8.192          trns
   8.193 -        |> appgen_default thy algbr funcgr (no_strict strct) app;
   8.194 +        |> appgen_default thy algbr funcgr strct app;
   8.195  
   8.196  fun appgen_char char_to_index thy algbr funcgr strct (app as ((_, ty), _)) trns =
   8.197    case (char_to_index o list_comb o apfst Const) app
   8.198 @@ -521,9 +497,18 @@
   8.199  
   8.200  fun codegen_term thy t =
   8.201    let
   8.202 +    fun const_typ (c, ty) =
   8.203 +      let
   8.204 +        val const = CodegenConsts.norm_of_typ thy (c, ty);
   8.205 +        val funcgr = CodegenFuncgr.mk_funcgr thy [const] [];
   8.206 +      in case CodegenFuncgr.get_funcs funcgr const
   8.207 +       of (thm :: _) => CodegenData.typ_func thy thm
   8.208 +        | [] => Sign.the_const_type thy c
   8.209 +      end;
   8.210      val ct = Thm.cterm_of thy t;
   8.211 -    val thm = CodegenData.preprocess_cterm thy ct;
   8.212 -    val t' = (snd o Logic.dest_equals o Drule.plain_prop_of) thm;
   8.213 +    val (thm, ct') = CodegenData.preprocess_cterm thy
   8.214 +      (const_typ) ct;
   8.215 +    val t' = Thm.term_of ct';
   8.216      val cs_rhss = CodegenConsts.consts_of thy t';
   8.217    in
   8.218      (thm, generate thy cs_rhss (SOME []) NONE exprgen_term' t')
   8.219 @@ -540,18 +525,7 @@
   8.220      val _ = Term.fold_atyps (fn _ =>
   8.221        error ("Term" ^ Sign.string_of_term thy t ^ "is polymorhpic"))
   8.222        (Term.fastype_of t);
   8.223 -    fun preprocess_term t =
   8.224 -      let
   8.225 -        val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
   8.226 -        (* fake definition *)
   8.227 -        val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
   8.228 -          (Logic.mk_equals (x, t));
   8.229 -        fun err () = error "preprocess_term: bad preprocessor"
   8.230 -      in case map prop_of (CodegenFuncgr.preprocess thy [eq])
   8.231 -       of [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
   8.232 -        | _ => err ()
   8.233 -      end;
   8.234 -    val (_, t') = codegen_term thy (preprocess_term t);
   8.235 +    val (_, t') = codegen_term thy t;
   8.236    in
   8.237      CodegenSerializer.eval_term thy (ref_spec, t') (Code.get thy)
   8.238    end;
   8.239 @@ -613,7 +587,7 @@
   8.240     "code_class", "code_instance", "code_type", "code_const");
   8.241  
   8.242  val codeP =
   8.243 -  OuterSyntax.command codeK "generate and serialize executable code for constants" K.diag (
   8.244 +  OuterSyntax.improper_command codeK "generate and serialize executable code for constants" K.diag (
   8.245      Scan.repeat P.term
   8.246      -- Scan.repeat (P.$$$ "(" |--
   8.247          P.name :-- (fn target => (CodegenSerializer.parse_serializer target >> SOME) || pair NONE)
     9.1 --- a/src/Pure/Tools/codegen_thingol.ML	Mon Oct 02 23:00:50 2006 +0200
     9.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Mon Oct 02 23:00:51 2006 +0200
     9.3 @@ -95,8 +95,8 @@
     9.4    val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
     9.5    val elim_classes: module -> (iterm list * iterm) list * typscheme -> (iterm list * iterm) list * itype;
     9.6  
     9.7 -  val debug: bool ref;
     9.8 -  val debug_msg: ('a -> string) -> 'a -> 'a;
     9.9 +  val trace: bool ref;
    9.10 +  val tracing: ('a -> string) -> 'a -> 'a;
    9.11    val soft_exc: bool ref;
    9.12  
    9.13    val serialize:
    9.14 @@ -112,8 +112,8 @@
    9.15  
    9.16  (** auxiliary **)
    9.17  
    9.18 -val debug = ref false;
    9.19 -fun debug_msg f x = (if !debug then Output.tracing (f x) else (); x);
    9.20 +val trace = ref false;
    9.21 +fun tracing f x = (if !trace then Output.tracing (f x) else (); x);
    9.22  val soft_exc = ref true;
    9.23  
    9.24  fun unfoldl dest x =
    9.25 @@ -1057,7 +1057,7 @@
    9.26        ^ (if strict then " (strict)" else " (non-strict)");
    9.27      fun add_dp NONE = I
    9.28        | add_dp (SOME dep) =
    9.29 -          debug_msg (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
    9.30 +          tracing (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
    9.31            #> add_dep (dep, name);
    9.32      fun prep_def def modl =
    9.33        (check_prep_def modl def, modl);
    9.34 @@ -1077,22 +1077,22 @@
    9.35      modl
    9.36      |> (if can (get_def modl) name
    9.37          then
    9.38 -          debug_msg (fn _ => "asserting node " ^ quote name)
    9.39 +          tracing (fn _ => "asserting node " ^ quote name)
    9.40            #> add_dp dep
    9.41          else
    9.42 -          debug_msg (fn _ => "allocating node " ^ quote name ^ (if strict then " (strict)" else " (non-strict)"))
    9.43 +          tracing (fn _ => "allocating node " ^ quote name ^ (if strict then " (strict)" else " (non-strict)"))
    9.44            #> ensure_bot name
    9.45            #> add_dp dep
    9.46 -          #> debug_msg (fn _ => "creating node " ^ quote name)
    9.47 +          #> tracing (fn _ => "creating node " ^ quote name)
    9.48            #> invoke_generator name defgen
    9.49            #-> (fn def => prep_def def)
    9.50            #-> (fn def =>
    9.51 -             debug_msg (fn _ => "addition of " ^ name ^ " := " ^ (Pretty.output o pretty_def) def)
    9.52 -          #> debug_msg (fn _ => "adding")
    9.53 +             tracing (fn _ => "addition of " ^ name ^ " := " ^ (Pretty.output o pretty_def) def)
    9.54 +          #> tracing (fn _ => "adding")
    9.55            #> add_def_incr strict (name, def)
    9.56 -          #> debug_msg (fn _ => "postprocessing")
    9.57 +          #> tracing (fn _ => "postprocessing")
    9.58            #> postprocess_def (name, def)
    9.59 -          #> debug_msg (fn _ => "adding done")
    9.60 +          #> tracing (fn _ => "adding done")
    9.61         ))
    9.62      |> pair dep
    9.63    end;