src/HOL/Tools/datatype_codegen.ML
changeset 20835 27d049062b56
parent 20681 0e4df994ad34
child 20855 9f60d493c8fe
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Oct 02 23:00:50 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Oct 02 23:00:51 2006 +0200
     1.3 @@ -9,10 +9,8 @@
     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_eq_typecopy: theory -> string -> thm list
     1.8    val get_cert: theory -> bool * string -> thm list
     1.9    val get_cert_datatype: theory -> string -> thm list
    1.10 -  val get_cert_typecopy: theory -> string -> thm list
    1.11    val dest_case_expr: theory -> term
    1.12      -> ((string * typ) list * ((term * typ) * (term * term) list)) option
    1.13    val add_datatype_case_const: string -> theory -> theory
    1.14 @@ -29,11 +27,13 @@
    1.15    val get_codetypes_arities: theory -> (string * bool) list -> sort
    1.16      -> (string * (((string * sort list) * sort) * term list)) list option
    1.17    val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort
    1.18 -    -> (theory -> ((string * sort list) * sort) list -> (string * term list) list
    1.19 -    -> ((bstring * attribute list) * term) list) -> (theory -> theory) -> theory -> theory
    1.20 +    -> (((string * sort list) * sort) list -> (string * term list) list -> theory
    1.21 +    -> ((bstring * attribute list) * term) list * theory)
    1.22 +    -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory)
    1.23 +    -> theory -> theory
    1.24  
    1.25    val setup: theory -> theory
    1.26 -  val setup2: theory -> theory
    1.27 +  val setup_hooks: theory -> theory
    1.28  end;
    1.29  
    1.30  structure DatatypeCodegen : DATATYPE_CODEGEN =
    1.31 @@ -364,7 +364,7 @@
    1.32          val names = Name.invents ctxt "a" (length tys);
    1.33          val ctxt' = fold Name.declare names ctxt;
    1.34          val vs = map2 (curry Free) names tys;
    1.35 -      in (vs, ctxt) end;
    1.36 +      in (vs, ctxt') end;
    1.37      fun mk_dist ((co1, tys1), (co2, tys2)) =
    1.38        let
    1.39          val ((xs1, xs2), _) = Name.context
    1.40 @@ -400,17 +400,39 @@
    1.41        |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    1.42        |> map (fn thm => not_eq_quodlibet OF [thm])
    1.43    in inject @ distinct end
    1.44 -and get_cert_typecopy thy dtco =
    1.45 -  let
    1.46 -    val SOME { inject, ... } = TypecopyPackage.get_typecopy_info thy dtco;
    1.47 -    val thm = Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [inject]);
    1.48 -  in
    1.49 -    [thm]
    1.50 -  end;
    1.51  end (*local*);
    1.52  
    1.53 -fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
    1.54 -  | get_cert thy (false, dtco) = get_cert_typecopy thy dtco;
    1.55 +local
    1.56 +  val not_sym = thm "HOL.not_sym";
    1.57 +  val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
    1.58 +in fun get_eq_datatype thy dtco =
    1.59 +  let
    1.60 +    val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
    1.61 +    fun mk_triv_inject co =
    1.62 +      let
    1.63 +        val ct' = Thm.cterm_of thy
    1.64 +          (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
    1.65 +        val cty' = Thm.ctyp_of_term ct';
    1.66 +        val refl = Thm.prop_of HOL.refl;
    1.67 +        val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
    1.68 +          (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
    1.69 +          refl NONE;
    1.70 +      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
    1.71 +    val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
    1.72 +    val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
    1.73 +    val ctxt = Context.init_proof thy;
    1.74 +    val simpset = Simplifier.context ctxt
    1.75 +      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
    1.76 +    val cos = map (fn (co, tys) =>
    1.77 +        (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
    1.78 +    val tac = ALLGOALS (simp_tac simpset)
    1.79 +      THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
    1.80 +    val distinct =
    1.81 +      mk_distinct cos
    1.82 +      |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    1.83 +      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
    1.84 +  in inject1 @ inject2 @ distinct end;
    1.85 +end (*local*);
    1.86  
    1.87  fun add_datatype_case_const dtco thy =
    1.88    let
    1.89 @@ -429,8 +451,7 @@
    1.90  
    1.91  (** codetypes for code 2nd generation **)
    1.92  
    1.93 -type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
    1.94 -  -> theory -> theory;
    1.95 +(* abstraction over datatypes vs. type copies *)
    1.96  
    1.97  fun codetypes_dependency thy =
    1.98    let
    1.99 @@ -461,23 +482,54 @@
   1.100      |> map (AList.make (the o AList.lookup (op =) names))
   1.101    end;
   1.102  
   1.103 -fun mk_typecopy_spec ({ vs, constr, typ, ... } : TypecopyPackage.info) =
   1.104 -  (vs, [(constr, [typ])]);
   1.105 -
   1.106  fun get_spec thy (dtco, true) =
   1.107        (the o DatatypePackage.get_datatype_spec thy) dtco
   1.108    | get_spec thy (tyco, false) =
   1.109 -      (mk_typecopy_spec o the o TypecopyPackage.get_typecopy_info thy) tyco;
   1.110 +      TypecopyPackage.get_spec thy tyco;
   1.111 +
   1.112 +fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
   1.113 +  | get_cert thy (false, dtco) = [TypecopyPackage.get_cert thy dtco];
   1.114  
   1.115 -fun add_spec thy (tyco, is_dt) =
   1.116 -  (tyco, (is_dt, get_spec thy (tyco, is_dt)));
   1.117 +local
   1.118 +  val eq_def_sym = thm "eq_def" |> Thm.symmetric;
   1.119 +  val class_eq = "OperationalEquality.eq";
   1.120 +  fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
   1.121 +   of SOME _ => get_eq_datatype thy tyco
   1.122 +    | NONE => [TypecopyPackage.get_eq thy tyco];
   1.123 +  fun constrain_op_eq_thms thy thms =
   1.124 +    let
   1.125 +      fun add_eq (Const ("op =", ty)) =
   1.126 +            fold (insert (eq_fst (op =)))
   1.127 +              (Term.add_tvarsT ty [])
   1.128 +        | add_eq _ =
   1.129 +            I
   1.130 +      val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
   1.131 +      val instT = map (fn (v_i, sort) =>
   1.132 +        (Thm.ctyp_of thy (TVar (v_i, sort)),
   1.133 +           Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
   1.134 +    in
   1.135 +      thms
   1.136 +      |> map (Thm.instantiate (instT, []))
   1.137 +    end;
   1.138 +in
   1.139 +  fun get_eq thy tyco =
   1.140 +    get_eq_thms thy tyco
   1.141 +    |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
   1.142 +    |> constrain_op_eq_thms thy
   1.143 +    |> map (Tactic.rewrite_rule [eq_def_sym])
   1.144 +end;
   1.145 +
   1.146 +type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
   1.147 +  -> theory -> theory;
   1.148  
   1.149  fun add_codetypes_hook_bootstrap hook thy =
   1.150    let
   1.151 +    fun add_spec thy (tyco, is_dt) =
   1.152 +      (tyco, (is_dt, get_spec thy (tyco, is_dt)));
   1.153      fun datatype_hook dtcos thy =
   1.154        hook (map (add_spec thy) (map (rpair true) dtcos)) thy;
   1.155 -    fun typecopy_hook ((tyco, info )) thy =
   1.156 -      hook ([(tyco, (false, mk_typecopy_spec info))]) thy;
   1.157 +    fun typecopy_hook ((tyco, _)) thy =
   1.158 +      hook ([(tyco, (false, TypecopyPackage.get_spec thy tyco))]) thy;
   1.159    in
   1.160      thy
   1.161      |> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy))
   1.162 @@ -498,6 +550,23 @@
   1.163          val (vs::_, css) = split_list (map (the o DatatypePackage.get_datatype_spec thy) tycos);
   1.164        in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end;
   1.165  
   1.166 +
   1.167 +(* registering code types in code generator *)
   1.168 +
   1.169 +fun codetype_hook specs =
   1.170 +  let
   1.171 +    fun add (dtco, (flag, spec)) thy =
   1.172 +      let
   1.173 +        fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
   1.174 +      in
   1.175 +        CodegenData.add_datatype
   1.176 +          (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
   1.177 +      end;
   1.178 +  in fold add specs end;
   1.179 +
   1.180 +
   1.181 +(* instrumentalizing the sort algebra *)
   1.182 +
   1.183  fun get_codetypes_arities thy tycos sort =
   1.184    let
   1.185      val algebra = Sign.classes_of thy;
   1.186 @@ -538,114 +607,35 @@
   1.187              then NONE else SOME (arity, (tyco, cs)))) insts;
   1.188        in
   1.189          thy
   1.190 -        |> K ((not o null) arities) ? (ClassPackage.prove_instance_arity tac
   1.191 -             arities ("", []) (f thy arities css) #> after_qed)
   1.192 +        |> K ((not o null) arities) ? (
   1.193 +            f arities css
   1.194 +            #-> (fn defs =>
   1.195 +              ClassPackage.prove_instance_arity tac arities ("", []) defs
   1.196 +            #> after_qed arities css))
   1.197        end;
   1.198  
   1.199 +
   1.200 +(* operational equality *)
   1.201 +
   1.202  local
   1.203    val class_eq = "OperationalEquality.eq";
   1.204 -in fun add_eq_instance specs =
   1.205 -  prove_codetypes_arities
   1.206 -    (K (ClassPackage.intro_classes_tac []))
   1.207 -    (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   1.208 -    [class_eq] ((K o K o K) [])
   1.209 -end; (*local*)
   1.210 -
   1.211 -local
   1.212 -  val not_sym = thm "HOL.not_sym";
   1.213 -  val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
   1.214 -in fun get_eq_datatype thy dtco =
   1.215 +in fun eq_hook specs =
   1.216    let
   1.217 -(*     val _ = writeln "01";  *)
   1.218 -    val SOME (vs, cs) = DatatypePackage.get_datatype_spec (Context.check_thy thy) dtco;
   1.219 -(*     val _ = writeln "02";  *)
   1.220 -    fun mk_triv_inject co =
   1.221 +    fun add_eq_thms (dtco, (_, (vs, cs))) thy =
   1.222        let
   1.223 -        val ct' = Thm.cterm_of (Context.check_thy thy)
   1.224 -          (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
   1.225 -        val cty' = Thm.ctyp_of_term ct';
   1.226 -        val refl = Thm.prop_of HOL.refl;
   1.227 -        val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
   1.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)
   1.229 -          refl NONE;
   1.230 -      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
   1.231 -(*     val _ = writeln "03";  *)
   1.232 -    val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
   1.233 -(*     val _ = writeln "04";  *)
   1.234 -    val inject2 = (#inject o DatatypePackage.the_datatype (Context.check_thy thy)) dtco;
   1.235 -(*     val _ = writeln "05";  *)
   1.236 -    val ctxt = Context.init_proof (Context.check_thy thy);
   1.237 -(*     val _ = writeln "06";  *)
   1.238 -    val simpset = Simplifier.context ctxt
   1.239 -      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
   1.240 -(*     val _ = writeln "07";  *)
   1.241 -    val cos = map (fn (co, tys) =>
   1.242 -        (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
   1.243 -    val tac = ALLGOALS (simp_tac simpset)
   1.244 -      THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
   1.245 -(*     val _ = writeln "08";  *)
   1.246 -    val distinct =
   1.247 -      mk_distinct cos
   1.248 -      |> map (fn t => Goal.prove_global (Context.check_thy thy) [] [] t (K tac))
   1.249 -      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
   1.250 -(*     val _ = writeln "09";  *)
   1.251 -  in inject1 @ inject2 @ distinct end;
   1.252 -
   1.253 -fun get_eq_typecopy thy tyco =
   1.254 -  case TypecopyPackage.get_typecopy_info thy tyco
   1.255 -   of SOME { inject, ... } => [inject]
   1.256 -    | NONE => [];
   1.257 -
   1.258 -local
   1.259 -  val lift_not_thm = thm "HOL.Eq_FalseI";
   1.260 -  val lift_thm = thm "HOL.eq_reflection";
   1.261 -  val eq_def_sym = thm "eq_def" |> Thm.symmetric;
   1.262 -  fun get_eq_thms thy tyco = case DatatypePackage.get_datatype (Context.check_thy thy) tyco
   1.263 -   of SOME _ => get_eq_datatype (Context.check_thy thy) tyco
   1.264 -    | NONE => case TypecopyPackage.get_typecopy_info thy tyco
   1.265 -       of SOME _ => get_eq_typecopy thy tyco
   1.266 -        | NONE => [];
   1.267 -in
   1.268 -  fun get_eq thy tyco =
   1.269 -    get_eq_thms (Context.check_thy thy) tyco
   1.270 -(*     |> tap (fn _ => writeln "10")  *)
   1.271 -    |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) (Context.check_thy thy))
   1.272 -(*     |> tap (fn _ => writeln "11")  *)
   1.273 -    |> constrain_op_eq (Context.check_thy thy)
   1.274 -(*     |> tap (fn _ => writeln "12")  *)
   1.275 -    |> map (Tactic.rewrite_rule [eq_def_sym])
   1.276 -(*     |> tap (fn _ => writeln "13")  *)
   1.277 -end;
   1.278 -
   1.279 -end;
   1.280 -
   1.281 -fun add_eq_thms (dtco, (_, (vs, cs))) thy =
   1.282 -  let
   1.283 -    val thy_ref = Theory.self_ref thy;
   1.284 -    val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
   1.285 -    val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
   1.286 -    val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
   1.287 -  in
   1.288 -    CodegenData.add_funcl
   1.289 -      (c, CodegenData.lazy get_thms) thy
   1.290 -  end;
   1.291 -
   1.292 -fun codetype_hook dtcos theory =
   1.293 -  let
   1.294 -    fun add (dtco, (flag, spec)) thy =
   1.295 -      let
   1.296 -        fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
   1.297 +        val thy_ref = Theory.self_ref thy;
   1.298 +        val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
   1.299 +        val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
   1.300 +        val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
   1.301        in
   1.302 -        CodegenData.add_datatype
   1.303 -          (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
   1.304 +        CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
   1.305        end;
   1.306    in
   1.307 -    theory
   1.308 -    |> fold add dtcos
   1.309 +    prove_codetypes_arities (K (ClassPackage.intro_classes_tac []))
   1.310 +      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   1.311 +      [class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
   1.312    end;
   1.313 -
   1.314 -fun eq_hook dtcos =
   1.315 -  add_eq_instance dtcos (fold add_eq_thms dtcos);
   1.316 +end; (*local*)
   1.317  
   1.318  
   1.319  
   1.320 @@ -657,7 +647,7 @@
   1.321    #> DatatypeHooks.add (fold add_datatype_case_const)
   1.322    #> DatatypeHooks.add (fold add_datatype_case_defs)
   1.323  
   1.324 -val setup2 =
   1.325 +val setup_hooks =
   1.326    add_codetypes_hook_bootstrap codetype_hook
   1.327    #> add_codetypes_hook_bootstrap eq_hook
   1.328