1.1 --- a/src/HOL/Ctr_Sugar.thy	Mon Dec 02 20:31:54 2013 +0100
     1.2 +++ b/src/HOL/Ctr_Sugar.thy	Mon Dec 02 20:31:54 2013 +0100
     1.3 @@ -40,6 +40,7 @@
     1.4  
     1.5  ML_file "Tools/ctr_sugar_util.ML"
     1.6  ML_file "Tools/ctr_sugar_tactics.ML"
     1.7 +ML_file "Tools/ctr_sugar_code.ML"
     1.8  ML_file "Tools/ctr_sugar.ML"
     1.9  
    1.10  end

     2.1 --- a/src/HOL/Inductive.thy	Mon Dec 02 20:31:54 2013 +0100
     2.2 +++ b/src/HOL/Inductive.thy	Mon Dec 02 20:31:54 2013 +0100
     2.3 @@ -274,7 +274,7 @@
     2.4  ML_file "Tools/Datatype/datatype_prop.ML"
     2.5  ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
     2.6  ML_file "Tools/Datatype/rep_datatype.ML"
     2.7 -ML_file "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
     2.8 +ML_file "Tools/Datatype/datatype_codegen.ML"
     2.9  ML_file "Tools/Datatype/primrec.ML"
    2.10  
    2.11  text{* Lambda-abstractions with pattern matching: *}

     3.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Dec 02 20:31:54 2013 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Dec 02 20:31:54 2013 +0100
     3.3 @@ -6,152 +6,24 @@
     3.4  
     3.5  signature DATATYPE_CODEGEN =
     3.6  sig
     3.7 -  val setup: theory -> theory
     3.8  end;
     3.9  
    3.10  structure Datatype_Codegen : DATATYPE_CODEGEN =
    3.11  struct
    3.12  
    3.13 -(** generic code generator **)
    3.14 +fun add_code_for_datatype fcT_name thy =
    3.15 +  let
    3.16 +    val (As', ctr_specs) = Datatype_Data.the_spec thy fcT_name;
    3.17 +    val {inject = inject_thms, distinct = distinct_thms, case_rewrites = case_thms, ...} =
    3.18 +      Datatype_Data.the_info thy fcT_name;
    3.19  
    3.20 -(* liberal addition of code data for datatypes *)
    3.21 -
    3.22 -fun mk_constr_consts thy vs tyco cos =
    3.23 -  let
    3.24 -    val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos;
    3.25 -    val cs' = map (fn c_ty as (_, ty) => (Axclass.unoverload_const thy c_ty, ty)) cs;
    3.26 +    val As = map TFree As';
    3.27 +    val fcT = Type (fcT_name, As);
    3.28 +    val ctrs = map (fn (c, arg_Ts) => (c, arg_Ts ---> fcT)) ctr_specs;
    3.29    in
    3.30 -    if is_some (try (Code.constrset_of_consts thy) cs')
    3.31 -    then SOME cs
    3.32 -    else NONE
    3.33 +    Ctr_Sugar_Code.add_ctr_code fcT_name As ctrs inject_thms distinct_thms case_thms thy
    3.34    end;
    3.35  
    3.36 -
    3.37 -(* case certificates *)
    3.38 -
    3.39 -fun mk_case_cert thy tyco =
    3.40 -  let
    3.41 -    val raw_thms = #case_rewrites (Datatype_Data.the_info thy tyco);
    3.42 -    val thms as hd_thm :: _ = raw_thms
    3.43 -      |> Conjunction.intr_balanced
    3.44 -      |> Thm.unvarify_global
    3.45 -      |> Conjunction.elim_balanced (length raw_thms)
    3.46 -      |> map Simpdata.mk_meta_eq
    3.47 -      |> map Drule.zero_var_indexes;
    3.48 -    val params = fold_aterms (fn (Free (v, _)) => insert (op =) v | _ => I) (Thm.prop_of hd_thm) [];
    3.49 -    val rhs = hd_thm
    3.50 -      |> Thm.prop_of
    3.51 -      |> Logic.dest_equals
    3.52 -      |> fst
    3.53 -      |> Term.strip_comb
    3.54 -      |> apsnd (fst o split_last)
    3.55 -      |> list_comb;
    3.56 -    val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
    3.57 -    val asm = Thm.cterm_of thy (Logic.mk_equals (lhs, rhs));
    3.58 -  in
    3.59 -    thms
    3.60 -    |> Conjunction.intr_balanced
    3.61 -    |> rewrite_rule [Thm.symmetric (Thm.assume asm)]
    3.62 -    |> Thm.implies_intr asm
    3.63 -    |> Thm.generalize ([], params) 0
    3.64 -    |> Axclass.unoverload thy
    3.65 -    |> Thm.varifyT_global
    3.66 -  end;
    3.67 -
    3.68 -
    3.69 -(* equality *)
    3.70 -
    3.71 -fun mk_eq_eqns thy tyco =
    3.72 -  let
    3.73 -    val (vs, cos) = Datatype_Data.the_spec thy tyco;
    3.74 -    val {descr, index, inject = inject_thms, distinct = distinct_thms, ...} =
    3.75 -      Datatype_Data.the_info thy tyco;
    3.76 -    val ty = Type (tyco, map TFree vs);
    3.77 -    fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT) $ t1 $ t2;
    3.78 -    fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, @{term True});
    3.79 -    fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, @{term False});
    3.80 -    val triv_injects =
    3.81 -      map_filter
    3.82 -        (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
    3.83 -          | _ => NONE) cos;
    3.84 -    fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
    3.85 -      trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
    3.86 -    val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr]) index);
    3.87 -    fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
    3.88 -      [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
    3.89 -    val distincts = maps prep_distinct (nth (Datatype_Prop.make_distincts [descr]) index);
    3.90 -    val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
    3.91 -    val simp_ctxt =
    3.92 -      Simplifier.global_context thy HOL_basic_ss
    3.93 -        addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms));
    3.94 -    fun prove prop =
    3.95 -      Goal.prove_sorry_global thy [] [] prop (K (ALLGOALS (simp_tac simp_ctxt)))
    3.96 -      |> Simpdata.mk_eq;
    3.97 -  in (map prove (triv_injects @ injects @ distincts), prove refl) end;
    3.98 -
    3.99 -fun add_equality vs tycos thy =
   3.100 -  let
   3.101 -    fun add_def tyco lthy =
   3.102 -      let
   3.103 -        val ty = Type (tyco, map TFree vs);
   3.104 -        fun mk_side const_name =
   3.105 -          Const (const_name, ty --> ty --> HOLogic.boolT) $ Free ("x", ty) $ Free ("y", ty);
   3.106 -        val def =
   3.107 -          HOLogic.mk_Trueprop (HOLogic.mk_eq
   3.108 -            (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq}));
   3.109 -        val def' = Syntax.check_term lthy def;
   3.110 -        val ((_, (_, thm)), lthy') =
   3.111 -          Specification.definition (NONE, (Attrib.empty_binding, def')) lthy;
   3.112 -        val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy);
   3.113 -        val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
   3.114 -      in (thm', lthy') end;
   3.115 -    fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms);
   3.116 -    fun prefix tyco =
   3.117 -      Binding.qualify true (Long_Name.base_name tyco) o Binding.qualify true "eq" o Binding.name;
   3.118 -    fun add_eq_thms tyco =
   3.119 -      `(fn thy => mk_eq_eqns thy tyco)
   3.120 -      #-> (fn (thms, thm) =>
   3.121 -        Global_Theory.note_thmss Thm.lemmaK
   3.122 -          [((prefix tyco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
   3.123 -            ((prefix tyco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
   3.124 -      #> snd;
   3.125 -  in
   3.126 -    thy
   3.127 -    |> Class.instantiation (tycos, vs, [HOLogic.class_equal])
   3.128 -    |> fold_map add_def tycos
   3.129 -    |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
   3.130 -         (fn _ => fn def_thms => tac def_thms) def_thms)
   3.131 -    |-> (fn def_thms => fold Code.del_eqn def_thms)
   3.132 -    |> fold add_eq_thms tycos
   3.133 -  end;
   3.134 -
   3.135 -
   3.136 -(* register a datatype etc. *)
   3.137 -
   3.138 -fun add_all_code config tycos thy =
   3.139 -  let
   3.140 -    val (vs :: _, coss) = split_list (map (Datatype_Data.the_spec thy) tycos);
   3.141 -    val any_css = map2 (mk_constr_consts thy vs) tycos coss;
   3.142 -    val css = if exists is_none any_css then [] else map_filter I any_css;
   3.143 -    val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) tycos;
   3.144 -    val certs = map (mk_case_cert thy) tycos;
   3.145 -    val tycos_eq =
   3.146 -      filter_out
   3.147 -        (fn tyco => Sorts.has_instance (Sign.classes_of thy) tyco [HOLogic.class_equal]) tycos;
   3.148 -  in
   3.149 -    if null css then thy
   3.150 -    else
   3.151 -      thy
   3.152 -      |> tap (fn _ => Datatype_Aux.message config "Registering datatype for code generator ...")
   3.153 -      |> fold Code.add_datatype css
   3.154 -      |> fold_rev Code.add_default_eqn case_rewrites
   3.155 -      |> fold Code.add_case certs
   3.156 -      |> not (null tycos_eq) ? add_equality vs tycos_eq
   3.157 -   end;
   3.158 -
   3.159 -
   3.160 -(** theory setup **)
   3.161 -
   3.162 -val setup = Datatype_Data.interpretation add_all_code;
   3.163 +val _ = Theory.setup (Datatype_Data.interpretation (K (fold add_code_for_datatype)));
   3.164  
   3.165  end;

     4.1 --- a/src/HOL/Tools/ctr_sugar.ML	Mon Dec 02 20:31:54 2013 +0100
     4.2 +++ b/src/HOL/Tools/ctr_sugar.ML	Mon Dec 02 20:31:54 2013 +0100
     4.3 @@ -66,6 +66,7 @@
     4.4  
     4.5  open Ctr_Sugar_Util
     4.6  open Ctr_Sugar_Tactics
     4.7 +open Ctr_Sugar_Code
     4.8  
     4.9  type ctr_sugar =
    4.10    {ctrs: term list,
    4.11 @@ -926,11 +927,13 @@
    4.12          (ctr_sugar,
    4.13           lthy
    4.14           |> not rep_compat ?
    4.15 -            (Local_Theory.declaration {syntax = false, pervasive = true}
    4.16 -               (fn phi => Case_Translation.register
    4.17 -                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
    4.18 +            Local_Theory.declaration {syntax = false, pervasive = true}
    4.19 +              (fn phi => Case_Translation.register
    4.20 +                 (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
    4.21           |> Local_Theory.notes (anonymous_notes @ notes) |> snd
    4.22 -         |> register_ctr_sugar fcT_name ctr_sugar)
    4.23 +         |> register_ctr_sugar fcT_name ctr_sugar
    4.24 +         |> Local_Theory.background_theory
    4.25 +           (add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms case_thms))
    4.26        end;
    4.27    in
    4.28      (goalss, after_qed, lthy')

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/ctr_sugar_code.ML	Mon Dec 02 20:31:54 2013 +0100
     5.3 @@ -0,0 +1,129 @@
     5.4 +(*  Title:      HOL/Tools/ctr_sugar_code.ML
     5.5 +    Author:     Jasmin Blanchette, TU Muenchen
     5.6 +    Author:     Dmitriy Traytel, TU Muenchen
     5.7 +    Author:     Stefan Berghofer, TU Muenchen
     5.8 +    Author:     Florian Haftmann, TU Muenchen
     5.9 +    Copyright   2001-2013
    5.10 +
    5.11 +Code generation for freely generated types.
    5.12 +*)
    5.13 +
    5.14 +signature CTR_SUGAR_CODE =
    5.15 +sig
    5.16 +  val add_ctr_code: string -> typ list -> (string * typ) list -> thm list -> thm list -> thm list ->
    5.17 +    theory -> theory
    5.18 +end;
    5.19 +
    5.20 +structure Ctr_Sugar_Code : CTR_SUGAR_CODE =
    5.21 +struct
    5.22 +
    5.23 +open Ctr_Sugar_Util
    5.24 +
    5.25 +val eqN = "eq"
    5.26 +val reflN = "refl"
    5.27 +val simpsN = "simps"
    5.28 +
    5.29 +fun mk_case_certificate thy raw_thms =
    5.30 +  let
    5.31 +    val thms as thm1 :: _ = raw_thms
    5.32 +      |> Conjunction.intr_balanced
    5.33 +      |> Thm.unvarify_global
    5.34 +      |> Conjunction.elim_balanced (length raw_thms)
    5.35 +      |> map Simpdata.mk_meta_eq
    5.36 +      |> map Drule.zero_var_indexes;
    5.37 +    val params = Term.add_free_names (Thm.prop_of thm1) [];
    5.38 +    val rhs = thm1
    5.39 +      |> Thm.prop_of |> Logic.dest_equals |> fst |> Term.strip_comb
    5.40 +      ||> fst o split_last |> list_comb;
    5.41 +    val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
    5.42 +    val assum = Thm.cterm_of thy (Logic.mk_equals (lhs, rhs));
    5.43 +  in
    5.44 +    thms
    5.45 +    |> Conjunction.intr_balanced
    5.46 +    |> rewrite_rule [Thm.symmetric (Thm.assume assum)]
    5.47 +    |> Thm.implies_intr assum
    5.48 +    |> Thm.generalize ([], params) 0
    5.49 +    |> Axclass.unoverload thy
    5.50 +    |> Thm.varifyT_global
    5.51 +  end;
    5.52 +
    5.53 +fun mk_free_ctr_equations fcT ctrs inject_thms distinct_thms thy =
    5.54 +  let
    5.55 +    fun mk_fcT_eq (t, u) = Const (@{const_name HOL.equal}, fcT --> fcT --> HOLogic.boolT) $ t $ u;
    5.56 +    fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True});
    5.57 +    fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False});
    5.58 +
    5.59 +    val monomorphic_prop_of = prop_of o Thm.unvarify_global o Drule.zero_var_indexes;
    5.60 +
    5.61 +    fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs);
    5.62 +    fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)];
    5.63 +
    5.64 +    val triv_inject_goals =
    5.65 +      map_filter (fn c as (_, T) =>
    5.66 +          if T = fcT then SOME (HOLogic.mk_Trueprop (true_eq (Const c, Const c))) else NONE)
    5.67 +        ctrs;
    5.68 +    val inject_goals = map (massage_inject o monomorphic_prop_of) inject_thms;
    5.69 +    val distinct_goals = maps (massage_distinct o monomorphic_prop_of) distinct_thms;
    5.70 +    val refl_goal = HOLogic.mk_Trueprop (true_eq (Free ("x", fcT), Free ("x", fcT)));
    5.71 +
    5.72 +    val simp_ctxt =
    5.73 +      Simplifier.global_context thy HOL_basic_ss
    5.74 +        addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms));
    5.75 +
    5.76 +    fun prove goal =
    5.77 +      Goal.prove_sorry_global thy [] [] goal (K (ALLGOALS (simp_tac simp_ctxt)))
    5.78 +      |> Simpdata.mk_eq;
    5.79 +  in
    5.80 +    (map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal)
    5.81 +  end;
    5.82 +
    5.83 +fun add_equality fcT fcT_name As ctrs inject_thms distinct_thms =
    5.84 +  let
    5.85 +    fun add_def lthy =
    5.86 +      let
    5.87 +        fun mk_side const_name =
    5.88 +          Const (const_name, fcT --> fcT --> HOLogic.boolT) $ Free ("x", fcT) $ Free ("y", fcT);
    5.89 +        val spec =
    5.90 +          mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
    5.91 +          |> Syntax.check_term lthy;
    5.92 +        val ((_, (_, raw_def)), lthy') =
    5.93 +          Specification.definition (NONE, (Attrib.empty_binding, spec)) lthy;
    5.94 +        val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); (* FIXME? *)
    5.95 +        val def = singleton (Proof_Context.export lthy' ctxt_thy) raw_def;
    5.96 +      in
    5.97 +        (def, lthy')
    5.98 +      end;
    5.99 +
   5.100 +    fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms);
   5.101 +
   5.102 +    val qualify =
   5.103 +      Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name;
   5.104 +  in
   5.105 +    Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])
   5.106 +    #> add_def
   5.107 +    #-> Class.prove_instantiation_exit_result (map o Morphism.thm) (K tac) o single
   5.108 +    #-> fold Code.del_eqn
   5.109 +    #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
   5.110 +    #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
   5.111 +      [((qualify reflN, [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
   5.112 +        ((qualify simpsN, [Code.add_default_eqn_attribute]), [(rev thms, [])])])
   5.113 +    #> snd
   5.114 +  end;
   5.115 +
   5.116 +fun add_ctr_code fcT_name As ctrs inject_thms distinct_thms case_thms thy =
   5.117 +  let
   5.118 +    val fcT = Type (fcT_name, As);
   5.119 +    val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs;
   5.120 +  in
   5.121 +    if can (Code.constrset_of_consts thy) unover_ctrs then
   5.122 +      thy
   5.123 +      |> Code.add_datatype ctrs
   5.124 +      |> fold_rev Code.add_default_eqn case_thms
   5.125 +      |> Code.add_case (mk_case_certificate thy case_thms)
   5.126 +      |> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal])
   5.127 +        ? add_equality fcT fcT_name As ctrs inject_thms distinct_thms
   5.128 +    else
   5.129 +      thy
   5.130 +  end;
   5.131 +
   5.132 +end;