src/HOL/Tools/datatype_codegen.ML
changeset 22423 c1836b14c63a
parent 22331 7df6bc8cf0b0
child 22429 09e794384323
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Mar 09 08:45:50 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Mar 09 08:45:53 2007 +0100
     1.3 @@ -9,8 +9,6 @@
     1.4  sig
     1.5    val get_eq: theory -> string -> thm list
     1.6    val get_eq_datatype: theory -> string -> thm list
     1.7 -  val get_cert: theory -> bool * string -> thm list
     1.8 -  val get_cert_datatype: theory -> string -> thm list
     1.9    val dest_case_expr: theory -> term
    1.10      -> ((string * typ) list * ((term * typ) * (term * term) list)) option
    1.11    val add_datatype_case_const: string -> theory -> theory
    1.12 @@ -28,7 +26,7 @@
    1.13      -> (string * (arity * term list)) list option
    1.14    val prove_codetypes_arities: tactic -> (string * bool) list -> sort
    1.15      -> (arity list -> (string * term list) list -> theory
    1.16 -    -> ((bstring * Attrib.src list) * term) list * theory)
    1.17 +      -> ((bstring * Attrib.src list) * term) list * theory)
    1.18      -> (arity list -> (string * term list) list -> theory -> theory)
    1.19      -> theory -> theory
    1.20  
    1.21 @@ -379,35 +377,6 @@
    1.22    in map mk_dist (sym_product cos) end;
    1.23  
    1.24  local
    1.25 -  val bool_eq_implies = iffD1;
    1.26 -  val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
    1.27 -  val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
    1.28 -  val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
    1.29 -  val not_eq_quodlibet = thm "not_eq_quodlibet";
    1.30 -in
    1.31 -
    1.32 -fun get_cert_datatype thy dtco =
    1.33 -  let
    1.34 -    val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
    1.35 -    val inject = (#inject o DatatypePackage.the_datatype thy) dtco
    1.36 -      |> map (fn thm => bool_eq_implies OF [thm] )
    1.37 -      |> map (MetaSimplifier.rewrite_rule [rew_eq, rew_conj]);
    1.38 -    val ctxt = ProofContext.init thy;
    1.39 -    val simpset = Simplifier.context ctxt
    1.40 -      (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
    1.41 -    val cos = map (fn (co, tys) =>
    1.42 -        (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
    1.43 -    val tac = ALLGOALS (simp_tac simpset)
    1.44 -      THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
    1.45 -    val distinct =
    1.46 -      mk_distinct cos
    1.47 -      |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    1.48 -      |> map (fn thm => not_eq_quodlibet OF [thm])
    1.49 -  in inject @ distinct end
    1.50 -
    1.51 -end;
    1.52 -
    1.53 -local
    1.54    val not_sym = thm "HOL.not_sym";
    1.55    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
    1.56    val refl = thm "refl";
    1.57 @@ -496,9 +465,6 @@
    1.58    | get_spec thy (tyco, false) =
    1.59        TypecopyPackage.get_spec thy tyco;
    1.60  
    1.61 -fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
    1.62 -  | get_cert thy (false, dtco) = [TypecopyPackage.get_cert thy dtco];
    1.63 -
    1.64  local
    1.65    fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    1.66     of SOME _ => get_eq_datatype thy tyco
    1.67 @@ -559,20 +525,20 @@
    1.68  
    1.69  (* registering code types in code generator *)
    1.70  
    1.71 -fun codetype_hook specs =
    1.72 -  let
    1.73 -    fun add (dtco, (flag, spec)) thy =
    1.74 -      let
    1.75 -        fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
    1.76 -      in
    1.77 -        CodegenData.add_datatype
    1.78 -          (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
    1.79 -      end;
    1.80 -  in fold add specs end;
    1.81 +val codetype_hook =
    1.82 +  fold (fn (dtco, (_, spec)) => CodegenData.add_datatype (dtco, spec));
    1.83  
    1.84  
    1.85  (* instrumentalizing the sort algebra *)
    1.86  
    1.87 +(*fun assume_arities_of_sort thy arities ty_sort =
    1.88 +  let
    1.89 +    val pp = Sign.pp thy;
    1.90 +    val algebra = Sign.classes_of thy
    1.91 +      |> fold (fn (tyco, asorts, sort) =>
    1.92 +           Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities;
    1.93 +  in Sorts.of_sort algebra ty_sort end;
    1.94 +
    1.95  fun get_codetypes_arities thy tycos sort =
    1.96    let
    1.97      val algebra = Sign.classes_of thy;
    1.98 @@ -588,7 +554,7 @@
    1.99      fun typ_of_sort ty =
   1.100        let
   1.101          val arities = map (fn (tyco, _) => (tyco, map snd vs, sort)) css;
   1.102 -      in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
   1.103 +      in assume_arities_of_sort thy arities (ty, sort) end;
   1.104      fun mk_cons tyco (c, tys) =
   1.105        let
   1.106          val ts = Name.names Name.context "a" tys;
   1.107 @@ -598,7 +564,34 @@
   1.108      then SOME (
   1.109        map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
   1.110      ) else NONE
   1.111 -  end;
   1.112 +  end;*)
   1.113 +
   1.114 +fun get_codetypes_arities thy tycos sort =
   1.115 +  let
   1.116 +    val pp = Sign.pp thy;
   1.117 +    val algebra = Sign.classes_of thy;
   1.118 +    val (vs_proto, css_proto) = the_codetypes_mut_specs thy tycos;
   1.119 +    val vs = map (fn (v, vsort) => (v, Sorts.inter_sort algebra (vsort, sort))) vs_proto;
   1.120 +    val css = map (fn (tyco, (_, cs)) => (tyco, cs)) css_proto;
   1.121 +    val algebra' = algebra
   1.122 +      |> fold (fn (tyco, _) =>
   1.123 +           Sorts.add_arities pp (tyco, map (fn class => (class, map snd vs)) sort)) css;
   1.124 +    fun typ_sort_inst ty = CodegenConsts.typ_sort_inst algebra' (Logic.varifyT ty, sort);
   1.125 +    val venv = Vartab.empty
   1.126 +      |> fold (fn (v, sort) => Vartab.update_new ((v, 0), sort)) vs
   1.127 +      |> fold (fn (_, cs) => fold (fn (_, tys) => fold typ_sort_inst tys) cs) css;
   1.128 +    fun inst (v, _) = (v, (the o Vartab.lookup venv) (v, 0));
   1.129 +    val vs' = map inst vs;
   1.130 +    fun mk_arity tyco = (tyco, map snd vs', sort);
   1.131 +    fun mk_cons tyco (c, tys) =
   1.132 +      let
   1.133 +        val tys' = (map o Term.map_type_tfree) (TFree o inst) tys;
   1.134 +        val ts = Name.names Name.context "a" tys';
   1.135 +        val ty = (tys' ---> Type (tyco, map TFree vs'));
   1.136 +      in list_comb (Const (c, ty), map Free ts) end;
   1.137 +  in
   1.138 +    map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css |> SOME
   1.139 +  end handle Class_Error => NONE;
   1.140  
   1.141  fun prove_codetypes_arities tac tycos sort f after_qed thy =
   1.142    case get_codetypes_arities thy tycos sort