src/HOL/Tools/datatype_codegen.ML
changeset 20597 65fe827aa595
parent 20439 1bf42b262a38
child 20608 86cb35b93f01
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 19 15:22:03 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 19 15:22:05 2006 +0200
     1.3 @@ -8,9 +8,11 @@
     1.4  signature DATATYPE_CODEGEN =
     1.5  sig
     1.6    val get_eq: theory -> string -> thm list
     1.7 -  val get_datatype_spec_thms: theory -> string
     1.8 -    -> (((string * sort) list * (string * typ list) list) * tactic) option
     1.9 -  val datatype_tac: theory -> string -> tactic
    1.10 +  val get_eq_datatype: theory -> string -> thm list
    1.11 +  val get_eq_typecopy: theory -> string -> thm list
    1.12 +  val get_cert: theory -> bool * string -> thm list
    1.13 +  val get_cert_datatype: theory -> string -> thm list
    1.14 +  val get_cert_typecopy: theory -> string -> thm list
    1.15    val dest_case_expr: theory -> term
    1.16      -> ((string * typ) list * ((term * typ) * (term * term) list)) option
    1.17    val add_datatype_case_const: string -> theory -> theory
    1.18 @@ -18,6 +20,8 @@
    1.19  
    1.20    type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
    1.21      -> theory -> theory
    1.22 +  val codetype_hook: hook
    1.23 +  val eq_hook: hook
    1.24    val codetypes_dependency: theory -> (string * bool) list list
    1.25    val add_codetypes_hook_bootstrap: hook -> theory -> theory
    1.26    val the_codetypes_mut_specs: theory -> (string * bool) list
    1.27 @@ -26,9 +30,10 @@
    1.28      -> (string * (((string * sort list) * sort) * term list)) list option
    1.29    val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort
    1.30      -> (theory -> ((string * sort list) * sort) list -> (string * term list) list
    1.31 -    -> ((bstring * attribute list) * term) list) -> theory -> theory
    1.32 +    -> ((bstring * attribute list) * term) list) -> (theory -> theory) -> theory -> theory
    1.33  
    1.34    val setup: theory -> theory
    1.35 +  val setup2: theory -> theory
    1.36  end;
    1.37  
    1.38  structure DatatypeCodegen : DATATYPE_CODEGEN =
    1.39 @@ -370,26 +375,20 @@
    1.40    in map mk_dist (sym_product cos) end;
    1.41  
    1.42  local
    1.43 -  val not_sym = thm "HOL.not_sym";
    1.44 +  val bool_eq_implies = thm "iffD1";
    1.45 +  val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
    1.46 +  val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
    1.47    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
    1.48 -in fun get_eq thy dtco =
    1.49 +  val not_eq_quodlibet = thm "not_eq_quodlibet";
    1.50 +in fun get_cert_datatype thy dtco =
    1.51    let
    1.52      val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
    1.53 -    fun mk_triv_inject co =
    1.54 -      let
    1.55 -        val ct' = Thm.cterm_of thy
    1.56 -          (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
    1.57 -        val cty' = Thm.ctyp_of_term ct';
    1.58 -        val refl = Thm.prop_of HOL.refl;
    1.59 -        val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
    1.60 -          (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
    1.61 -          refl NONE;
    1.62 -      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
    1.63 -    val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
    1.64 -    val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
    1.65 +    val inject = (#inject o DatatypePackage.the_datatype thy) dtco
    1.66 +      |> map (fn thm => bool_eq_implies OF [thm] )
    1.67 +      |> map (Tactic.rewrite_rule [rew_eq, rew_conj]);
    1.68      val ctxt = Context.init_proof thy;
    1.69      val simpset = Simplifier.context ctxt
    1.70 -      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
    1.71 +      (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
    1.72      val cos = map (fn (co, tys) =>
    1.73          (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
    1.74      val tac = ALLGOALS (simp_tac simpset)
    1.75 @@ -397,30 +396,19 @@
    1.76      val distinct =
    1.77        mk_distinct cos
    1.78        |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    1.79 -      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
    1.80 -  in inject1 @ inject2 @ distinct end;
    1.81 +      |> map (fn thm => not_eq_quodlibet OF [thm])
    1.82 +  in inject @ distinct end
    1.83 +and get_cert_typecopy thy dtco =
    1.84 +  let
    1.85 +    val SOME { inject, ... } = TypecopyPackage.get_typecopy_info thy dtco;
    1.86 +    val thm = Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [inject]);
    1.87 +  in
    1.88 +    [thm]
    1.89 +  end;
    1.90  end (*local*);
    1.91  
    1.92 -fun datatype_tac thy dtco =
    1.93 -  let
    1.94 -    val ctxt = Context.init_proof thy;
    1.95 -    val inject = (#inject o DatatypePackage.the_datatype thy) dtco;
    1.96 -    val simpset = Simplifier.context ctxt
    1.97 -      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
    1.98 -  in
    1.99 -    (TRY o ALLGOALS o match_tac) [HOL.eq_reflection]
   1.100 -    THEN (
   1.101 -      (ALLGOALS o match_tac) (eqTrueI :: inject)
   1.102 -      ORELSE (ALLGOALS o simp_tac) simpset
   1.103 -    )
   1.104 -    THEN (ALLGOALS o match_tac) [HOL.refl, Drule.reflexive_thm]
   1.105 -  end;
   1.106 -
   1.107 -fun get_datatype_spec_thms thy dtco =
   1.108 -  case DatatypePackage.get_datatype_spec thy dtco
   1.109 -   of SOME vs_cos =>
   1.110 -        SOME (vs_cos, datatype_tac thy dtco)
   1.111 -    | NONE => NONE;
   1.112 +fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
   1.113 +  | get_cert thy (false, dtco) = get_cert_typecopy thy dtco;
   1.114  
   1.115  fun add_datatype_case_const dtco thy =
   1.116    let
   1.117 @@ -433,7 +421,7 @@
   1.118    let
   1.119      val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
   1.120    in
   1.121 -    fold CodegenTheorems.add_fun case_rewrites thy
   1.122 +    fold_rev CodegenData.add_func case_rewrites thy
   1.123    end;
   1.124  
   1.125  
   1.126 @@ -536,7 +524,7 @@
   1.127      ) else NONE
   1.128    end;
   1.129  
   1.130 -fun prove_codetypes_arities tac tycos sort f thy =
   1.131 +fun prove_codetypes_arities tac tycos sort f after_qed thy =
   1.132    case get_codetypes_arities thy tycos sort
   1.133     of NONE => thy
   1.134      | SOME insts => let
   1.135 @@ -548,20 +536,128 @@
   1.136              then NONE else SOME (arity, (tyco, cs)))) insts;
   1.137        in
   1.138          thy
   1.139 -        |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
   1.140 -             arities ("", []) (f thy arities css)
   1.141 +        |> K ((not o null) arities) ? (ClassPackage.prove_instance_arity tac
   1.142 +             arities ("", []) (f thy arities css) #> after_qed)
   1.143        end;
   1.144  
   1.145 +local
   1.146 +  val class_eq = "OperationalEquality.eq";
   1.147 +in fun add_eq_instance specs =
   1.148 +  prove_codetypes_arities
   1.149 +    (K (ClassPackage.intro_classes_tac []))
   1.150 +    (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   1.151 +    [class_eq] ((K o K o K) [])
   1.152 +end; (*local*)
   1.153 +
   1.154 +local
   1.155 +  val not_sym = thm "HOL.not_sym";
   1.156 +  val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
   1.157 +in fun get_eq_datatype thy dtco =
   1.158 +  let
   1.159 +    val _ = writeln "01";
   1.160 +    val SOME (vs, cs) = DatatypePackage.get_datatype_spec (Context.check_thy thy) dtco;
   1.161 +    val _ = writeln "02";
   1.162 +    fun mk_triv_inject co =
   1.163 +      let
   1.164 +        val ct' = Thm.cterm_of (Context.check_thy thy)
   1.165 +          (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
   1.166 +        val cty' = Thm.ctyp_of_term ct';
   1.167 +        val refl = Thm.prop_of HOL.refl;
   1.168 +        val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
   1.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)
   1.170 +          refl NONE;
   1.171 +      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
   1.172 +    val _ = writeln "03";
   1.173 +    val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
   1.174 +    val _ = writeln "04";
   1.175 +    val inject2 = (#inject o DatatypePackage.the_datatype (Context.check_thy thy)) dtco;
   1.176 +    val _ = writeln "05";
   1.177 +    val ctxt = Context.init_proof (Context.check_thy thy);
   1.178 +    val _ = writeln "06";
   1.179 +    val simpset = Simplifier.context ctxt
   1.180 +      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
   1.181 +    val _ = writeln "07";
   1.182 +    val cos = map (fn (co, tys) =>
   1.183 +        (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
   1.184 +    val tac = ALLGOALS (simp_tac simpset)
   1.185 +      THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
   1.186 +    val _ = writeln "08";
   1.187 +    val distinct =
   1.188 +      mk_distinct cos
   1.189 +      |> map (fn t => Goal.prove_global (Context.check_thy thy) [] [] t (K tac))
   1.190 +      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
   1.191 +    val _ = writeln "09";
   1.192 +  in inject1 @ inject2 @ distinct end;
   1.193 +
   1.194 +fun get_eq_typecopy thy tyco =
   1.195 +  case TypecopyPackage.get_typecopy_info thy tyco
   1.196 +   of SOME { inject, ... } => [inject]
   1.197 +    | NONE => [];
   1.198 +
   1.199 +local
   1.200 +  val lift_not_thm = thm "HOL.Eq_FalseI";
   1.201 +  val lift_thm = thm "HOL.eq_reflection";
   1.202 +  val eq_def_sym = thm "eq_def" |> Thm.symmetric;
   1.203 +  fun get_eq_thms thy tyco = case DatatypePackage.get_datatype (Context.check_thy thy) tyco
   1.204 +   of SOME _ => get_eq_datatype (Context.check_thy thy) tyco
   1.205 +    | NONE => case TypecopyPackage.get_typecopy_info thy tyco
   1.206 +       of SOME _ => get_eq_typecopy thy tyco
   1.207 +        | NONE => [];
   1.208 +in
   1.209 +  fun get_eq thy tyco =
   1.210 +    get_eq_thms (Context.check_thy thy) tyco
   1.211 +    |> tap (fn _ => writeln "10")
   1.212 +    |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) (Context.check_thy thy))
   1.213 +    |> tap (fn _ => writeln "11")
   1.214 +    |> constrain_op_eq (Context.check_thy thy)
   1.215 +    |> tap (fn _ => writeln "12")
   1.216 +    |> map (Tactic.rewrite_rule [eq_def_sym])
   1.217 +    |> tap (fn _ => writeln "13")
   1.218 +end;
   1.219 +
   1.220 +end;
   1.221 +
   1.222 +fun add_eq_thms (dtco, (_, (vs, cs))) thy =
   1.223 +  let
   1.224 +    val thy_ref = Theory.self_ref thy;
   1.225 +    val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
   1.226 +    val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
   1.227 +    val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> tap (fn _ => writeln "14x") |> rev |> tap (fn _ => writeln "15x"));
   1.228 +  in
   1.229 +    CodegenData.add_funcl
   1.230 +      (c, CodegenData.lazy get_thms) thy
   1.231 +  end;
   1.232 +
   1.233 +fun codetype_hook dtcos theory =
   1.234 +  let
   1.235 +    fun add (dtco, (flag, spec)) thy =
   1.236 +      let
   1.237 +        fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
   1.238 +      in
   1.239 +        CodegenData.add_datatype
   1.240 +          (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
   1.241 +      end;
   1.242 +  in
   1.243 +    theory
   1.244 +    |> fold add dtcos
   1.245 +  end;
   1.246 +
   1.247 +fun eq_hook dtcos =
   1.248 +  add_eq_instance dtcos (fold add_eq_thms dtcos);
   1.249 +
   1.250  
   1.251  
   1.252  (** theory setup **)
   1.253  
   1.254  val setup = 
   1.255 -  add_codegen "datatype" datatype_codegen #>
   1.256 -  add_tycodegen "datatype" datatype_tycodegen #>
   1.257 -  CodegenTheorems.add_datatype_extr
   1.258 -    get_datatype_spec_thms #>
   1.259 -  DatatypeHooks.add (fold add_datatype_case_const) #>
   1.260 -  DatatypeHooks.add (fold add_datatype_case_defs)
   1.261 +  add_codegen "datatype" datatype_codegen
   1.262 +  #> add_tycodegen "datatype" datatype_tycodegen 
   1.263 +  #> DatatypeHooks.add (fold add_datatype_case_const)
   1.264 +  #> DatatypeHooks.add (fold add_datatype_case_defs)
   1.265 +
   1.266 +val setup2 =
   1.267 +  add_codetypes_hook_bootstrap codetype_hook
   1.268 +  #> add_codetypes_hook_bootstrap eq_hook
   1.269 +
   1.270  
   1.271  end;