--- a/src/HOL/Tools/datatype_codegen.ML Tue Aug 29 14:31:12 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Tue Aug 29 14:31:13 2006 +0200
@@ -2,11 +2,12 @@
ID: $Id$
Author: Stefan Berghofer & Florian Haftmann, TU Muenchen
-Code generator for inductive datatypes.
+Code generator for inductive datatypes and type copies ("code types").
*)
signature DATATYPE_CODEGEN =
sig
+ val get_eq: theory -> string -> thm list
val get_datatype_spec_thms: theory -> string
-> (((string * sort) list * (string * typ list) list) * tactic) option
val datatype_tac: theory -> string -> tactic
@@ -14,15 +15,19 @@
-> ((string * typ) list * ((term * typ) * (term * term) list)) option
val add_datatype_case_const: string -> theory -> theory
val add_datatype_case_defs: string -> theory -> theory
- val datatypes_dependency: theory -> string list list
- val add_hook_bootstrap: DatatypeHooks.hook -> theory -> theory
- val get_datatype_mut_specs: theory -> string list
- -> ((string * sort) list * (string * (string * typ list) list) list)
- val get_datatype_arities: theory -> string list -> sort
+
+ type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
+ -> theory -> theory
+ val codetypes_dependency: theory -> (string * bool) list list
+ val add_codetypes_hook_bootstrap: hook -> theory -> theory
+ val the_codetypes_mut_specs: theory -> (string * bool) list
+ -> ((string * sort) list * (string * (bool * (string * typ list) list)) list)
+ val get_codetypes_arities: theory -> (string * bool) list -> sort
-> (string * (((string * sort list) * sort) * term list)) list option
- val prove_arities: (thm list -> tactic) -> string list -> sort
+ val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort
-> (theory -> ((string * sort list) * sort) list -> (string * term list) list
-> ((bstring * attribute list) * term) list) -> theory -> theory
+
val setup: theory -> theory
end;
@@ -313,87 +318,7 @@
| datatype_tycodegen _ _ _ _ _ _ _ = NONE;
-(** code 2nd generation **)
-
-fun datatypes_dependency thy =
- let
- val dtnames = DatatypePackage.get_datatypes thy;
- fun add_node (dtname, _) =
- let
- fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> fold add_tycos tys
- | add_tycos _ = I;
- val deps = (filter (Symtab.defined dtnames) o maps (fn ty =>
- add_tycos ty [])
- o maps snd o snd o the o DatatypePackage.get_datatype_spec thy) dtname
- in
- Graph.default_node (dtname, ())
- #> fold (fn dtname' =>
- Graph.default_node (dtname', ())
- #> Graph.add_edge (dtname', dtname)
- ) deps
- end
- in
- Graph.empty
- |> Symtab.fold add_node dtnames
- |> Graph.strong_conn
- end;
-
-fun add_hook_bootstrap hook thy =
- thy
- |> fold hook (datatypes_dependency thy)
- |> DatatypeHooks.add hook;
-
-fun get_datatype_mut_specs thy (tycos as tyco :: _) =
- let
- val tycos' = (map (#1 o snd) o #descr o DatatypePackage.the_datatype thy) tyco;
- val _ = if gen_subset (op =) (tycos, tycos') then () else
- error ("datatype constructors are not mutually recursive: " ^ (commas o map quote) tycos);
- val (vs::_, css) = split_list (map (the o DatatypePackage.get_datatype_spec thy) tycos);
- in (vs, tycos ~~ css) end;
-
-fun get_datatype_arities thy tycos sort =
- let
- val algebra = Sign.classes_of thy;
- val (vs_proto, css_proto) = get_datatype_mut_specs thy tycos;
- val vs = map (fn (v, vsort) => (v, Sorts.inter_sort algebra (vsort, sort))) vs_proto;
- fun inst_type tyco (c, tys) =
- let
- val tys' = (map o map_atyps)
- (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) vs v))) tys
- in (c, tys') end;
- val css = map (fn (tyco, cs) => (tyco, (map (inst_type tyco) cs))) css_proto;
- fun mk_arity tyco =
- ((tyco, map snd vs), sort);
- fun typ_of_sort ty =
- let
- val arities = map (fn (tyco, _) => ((tyco, map snd vs), sort)) css;
- in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
- fun mk_cons tyco (c, tys) =
- let
- val ts = Name.names Name.context "a" tys;
- val ty = tys ---> Type (tyco, map TFree vs);
- in list_comb (Const (c, ty), map Free ts) end;
- in if forall (fn (_, cs) => forall (fn (_, tys) => forall typ_of_sort tys) cs) css
- then SOME (
- map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
- ) else NONE
- end;
-
-fun prove_arities tac tycos sort f thy =
- case get_datatype_arities thy tycos sort
- of NONE => thy
- | SOME insts => let
- fun proven ((tyco, asorts), sort) =
- Sorts.of_sort (Sign.classes_of thy)
- (Type (tyco, map TFree (Name.names Name.context "'a" asorts)), sort);
- val (arities, css) = (split_list o map_filter
- (fn (tyco, (arity, cs)) => if proven arity
- then NONE else SOME (arity, (tyco, cs)))) insts;
- in
- thy
- |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
- arities ("", []) (f thy arities css)
- end;
+(** datatypes for code 2nd generation **)
fun dtyp_of_case_const thy c =
get_first (fn (dtco, { case_name, ... }) => if case_name = c then SOME dtco else NONE)
@@ -423,6 +348,57 @@
| _ => NONE)
| _ => NONE;
+fun mk_distinct cos =
+ let
+ fun sym_product [] = []
+ | sym_product (x::xs) = map (pair x) xs @ sym_product xs;
+ fun mk_co_args (co, tys) ctxt =
+ let
+ val names = Name.invents ctxt "a" (length tys);
+ val ctxt' = fold Name.declare names ctxt;
+ val vs = map2 (curry Free) names tys;
+ in (vs, ctxt) end;
+ fun mk_dist ((co1, tys1), (co2, tys2)) =
+ let
+ val ((xs1, xs2), _) = Name.context
+ |> mk_co_args (co1, tys1)
+ ||>> mk_co_args (co2, tys2);
+ val prem = HOLogic.mk_eq
+ (list_comb (co1, xs1), list_comb (co2, xs2));
+ val t = HOLogic.mk_not prem;
+ in HOLogic.mk_Trueprop t end;
+ in map mk_dist (sym_product cos) end;
+
+local
+ val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
+in fun get_eq thy dtco =
+ let
+ val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
+ fun mk_triv_inject co =
+ let
+ val ct' = Thm.cterm_of thy
+ (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
+ val cty' = Thm.ctyp_of_term ct';
+ val refl = Thm.prop_of HOL.refl;
+ val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
+ (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
+ refl NONE;
+ in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
+ val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
+ val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
+ val ctxt = Context.init_proof thy;
+ val simpset = Simplifier.context ctxt
+ (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
+ val cos = map (fn (co, tys) =>
+ (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
+ val tac = ALLGOALS (simp_tac simpset)
+ THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
+ val distinct =
+ mk_distinct cos
+ |> map (fn t => Goal.prove_global thy [] [] t (K tac))
+ in inject1 @ inject2 @ distinct end;
+end (*local*);
+
fun datatype_tac thy dtco =
let
val ctxt = Context.init_proof thy;
@@ -458,6 +434,126 @@
fold CodegenTheorems.add_fun case_rewrites thy
end;
+
+(** codetypes for code 2nd generation **)
+
+type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
+ -> theory -> theory;
+
+fun codetypes_dependency thy =
+ let
+ val names =
+ map (rpair true) (Symtab.keys (DatatypePackage.get_datatypes thy))
+ @ map (rpair false) (TypecopyPackage.get_typecopies thy);
+ fun add_node (name, is_dt) =
+ let
+ fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> fold add_tycos tys
+ | add_tycos _ = I;
+ val tys = if is_dt then
+ (maps snd o snd o the o DatatypePackage.get_datatype_spec thy) name
+ else
+ [(#typ o the o TypecopyPackage.get_typecopy_info thy) name]
+ val deps = (filter (AList.defined (op =) names) o maps (fn ty =>
+ add_tycos ty [])) tys;
+ in
+ Graph.default_node (name, ())
+ #> fold (fn name' =>
+ Graph.default_node (name', ())
+ #> Graph.add_edge (name', name)
+ ) deps
+ end
+ in
+ Graph.empty
+ |> fold add_node names
+ |> Graph.strong_conn
+ |> map (AList.make (the o AList.lookup (op =) names))
+ end;
+
+fun mk_typecopy_spec ({ vs, constr, typ, ... } : TypecopyPackage.info) =
+ (vs, [(constr, [typ])]);
+
+fun get_spec thy (dtco, true) =
+ (the o DatatypePackage.get_datatype_spec thy) dtco
+ | get_spec thy (tyco, false) =
+ (mk_typecopy_spec o the o TypecopyPackage.get_typecopy_info thy) tyco;
+
+fun add_spec thy (tyco, is_dt) =
+ (tyco, (is_dt, get_spec thy (tyco, is_dt)));
+
+fun add_codetypes_hook_bootstrap hook thy =
+ let
+ fun datatype_hook dtcos thy =
+ hook (map (add_spec thy) (map (rpair true) dtcos)) thy;
+ fun typecopy_hook ((tyco, info )) thy =
+ hook ([(tyco, (false, mk_typecopy_spec info))]) thy;
+ in
+ thy
+ |> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy))
+ |> DatatypeHooks.add datatype_hook
+ |> TypecopyPackage.add_hook typecopy_hook
+ end;
+
+fun the_codetypes_mut_specs thy ([(tyco, is_dt)]) =
+ let
+ val (vs, cs) = get_spec thy (tyco, is_dt)
+ in (vs, [(tyco, (is_dt, cs))]) end
+ | the_codetypes_mut_specs thy (tycos' as (tyco, true) :: _) =
+ let
+ val tycos = map fst tycos';
+ val tycos'' = (map (#1 o snd) o #descr o DatatypePackage.the_datatype thy) tyco;
+ val _ = if gen_subset (op =) (tycos, tycos'') then () else
+ error ("datatype constructors are not mutually recursive: " ^ (commas o map quote) tycos);
+ val (vs::_, css) = split_list (map (the o DatatypePackage.get_datatype_spec thy) tycos);
+ in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end;
+
+fun get_codetypes_arities thy tycos sort =
+ let
+ val algebra = Sign.classes_of thy;
+ val (vs_proto, css_proto) = the_codetypes_mut_specs thy tycos;
+ val vs = map (fn (v, vsort) => (v, Sorts.inter_sort algebra (vsort, sort))) vs_proto;
+ fun inst_type tyco (c, tys) =
+ let
+ val tys' = (map o map_atyps)
+ (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) vs v))) tys
+ in (c, tys') end;
+ val css = map (fn (tyco, (_, cs)) => (tyco, (map (inst_type tyco) cs))) css_proto;
+ fun mk_arity tyco =
+ ((tyco, map snd vs), sort);
+ fun typ_of_sort ty =
+ let
+ val arities = map (fn (tyco, _) => ((tyco, map snd vs), sort)) css;
+ in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
+ fun mk_cons tyco (c, tys) =
+ let
+ val ts = Name.names Name.context "a" tys;
+ val ty = tys ---> Type (tyco, map TFree vs);
+ in list_comb (Const (c, ty), map Free ts) end;
+ in if forall (fn (_, cs) => forall (fn (_, tys) => forall typ_of_sort tys) cs) css
+ then SOME (
+ map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
+ ) else NONE
+ end;
+
+fun prove_codetypes_arities tac tycos sort f thy =
+ case get_codetypes_arities thy tycos sort
+ of NONE => thy
+ | SOME insts => let
+ fun proven ((tyco, asorts), sort) =
+ Sorts.of_sort (Sign.classes_of thy)
+ (Type (tyco, map TFree (Name.names Name.context "'a" asorts)), sort);
+ val (arities, css) = (split_list o map_filter
+ (fn (tyco, (arity, cs)) => if proven arity
+ then NONE else SOME (arity, (tyco, cs)))) insts;
+ in
+ thy
+ |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
+ arities ("", []) (f thy arities css)
+ end;
+
+
+
+(** theory setup **)
+
val setup =
add_codegen "datatype" datatype_codegen #>
add_tycodegen "datatype" datatype_tycodegen #>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/typecopy_package.ML Tue Aug 29 14:31:13 2006 +0200
@@ -0,0 +1,163 @@
+(* Title: HOL/Tools/typecopy_package.ML
+ ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+
+Introducing copies of types using trivial typedefs.
+*)
+
+signature TYPECOPY_PACKAGE =
+sig
+ type info = {
+ vs: (string * sort) list,
+ constr: string,
+ typ: typ,
+ inject: thm,
+ proj: string * typ,
+ proj_def: thm
+ }
+ val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
+ -> theory -> info * theory
+ val get_typecopies: theory -> string list
+ val get_typecopy_info: theory -> string -> info option
+ type hook = string * info -> theory -> theory;
+ val add_hook: hook -> theory -> theory;
+ val typecopy_fun_extr: theory -> string * typ -> thm list option
+ val typecopy_type_extr: theory -> string
+ -> (((string * sort) list * (string * typ list) list) * tactic) option
+ val print: theory -> unit
+ val setup: theory -> theory
+end;
+
+structure TypecopyPackage: TYPECOPY_PACKAGE =
+struct
+
+(* theory context reference *)
+
+val univ_witness = thm "Set.UNIV_witness"
+
+
+(* theory data *)
+
+type info = {
+ vs: (string * sort) list,
+ constr: string,
+ typ: typ,
+ inject: thm,
+ proj: string * typ,
+ proj_def: thm
+};
+
+type hook = string * info -> theory -> theory;
+
+structure TypecopyData = TheoryDataFun
+(struct
+ val name = "HOL/typecopy_package";
+ type T = info Symtab.table * (serial * hook) list;
+ val empty = (Symtab.empty, []);
+ val copy = I;
+ val extend = I;
+ fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) =
+ (Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2));
+ fun print thy (tab, _) =
+ let
+ fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
+ (Pretty.block o Pretty.breaks) [
+ Sign.pretty_typ thy (Type (tyco, map TFree vs)),
+ Pretty.str "=",
+ (Pretty.str o Sign.extern_const thy) constr,
+ Sign.pretty_typ thy typ,
+ Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str ")"]
+ ];
+ in
+ (Pretty.writeln o Pretty.block o Pretty.fbreaks) (
+ Pretty.str "type copies:"
+ :: map mk (Symtab.dest tab)
+ )
+ end;
+end);
+
+val print = TypecopyData.print;
+val get_typecopies = Symtab.keys o fst o TypecopyData.get;
+val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get;
+
+
+(* hook management *)
+
+fun add_hook hook =
+ (TypecopyData.map o apsnd o cons) (serial (), hook);
+
+fun invoke_hooks tyco_info thy =
+ fold (fn (_, f) => f tyco_info) ((snd o TypecopyData.get) thy) thy;
+
+
+(* add a type copy *)
+
+local
+
+fun gen_add_typecopy prep_typ (tyco, raw_vs) raw_ty constr_proj thy =
+ let
+ val ty = prep_typ thy raw_ty;
+ val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs;
+ val tac = Tactic.rtac UNIV_witness 1;
+ fun add_info ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
+ Rep_name = c_rep, Abs_inject = inject,
+ Abs_inverse = inverse, ... } : TypedefPackage.info ) thy =
+ let
+ val Type (tyco', _) = ty_abs;
+ val exists_thm =
+ UNIV_I
+ |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
+ val inject' = inject OF [exists_thm, exists_thm];
+ val proj_def = inverse OF [exists_thm];
+ val info = {
+ vs = vs,
+ constr = c_abs,
+ typ = ty_rep,
+ inject = inject',
+ proj = (c_rep, ty_abs --> ty_rep),
+ proj_def = proj_def
+ };
+ in
+ thy
+ |> (TypecopyData.map o apfst o Symtab.update_new) (tyco', info)
+ |> invoke_hooks (tyco', info)
+ |> pair info
+ end
+ in
+ thy
+ |> TypedefPackage.add_typedef_i false (SOME tyco) (tyco, map fst vs, NoSyn)
+ (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
+ |-> (fn info => add_info info)
+ end;
+
+in
+
+val add_typecopy = gen_add_typecopy Sign.certify_typ;
+
+end; (*local*)
+
+
+(* theory setup *)
+
+fun typecopy_type_extr thy tyco =
+ case get_typecopy_info thy tyco
+ of SOME { vs, constr, typ, inject, ... } => SOME ((vs, [(constr, [typ])]),
+ (ALLGOALS o match_tac) [eq_reflection]
+ THEN (ALLGOALS o match_tac) [inject])
+ | NONE => NONE;
+
+fun typecopy_fun_extr thy (c, ty) =
+ case (fst o strip_type) ty
+ of Type (tyco, _) :: _ =>
+ (case get_typecopy_info thy tyco
+ of SOME { proj_def, proj as (c', _), ... } =>
+ if c = c' then SOME [proj_def] else NONE
+ | NONE => NONE)
+ | _ => NONE;
+
+val setup =
+ TypecopyData.init
+ #> CodegenTheorems.add_fun_extr (these oo typecopy_fun_extr)
+ #> CodegenTheorems.add_datatype_extr typecopy_type_extr;
+
+end; (*struct*)