--- a/NEWS Wed Aug 18 14:55:10 2010 +0200
+++ b/NEWS Wed Aug 18 17:03:09 2010 +0200
@@ -35,6 +35,18 @@
*** HOL ***
+* Records: logical foundation type for records do not carry a '_type' suffix
+any longer. INCOMPATIBILITY.
+
+* Code generation for records: more idiomatic representation of record types.
+Warning: records are not covered by ancient SML code generation any longer.
+INCOMPATIBILITY. In cases of need, a suitable rep_datatype declaration
+helps to succeed then:
+
+ record 'a foo = ...
+ ...
+ rep_datatype foo_ext ...
+
* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
INCOMPATIBILITY.
--- a/src/HOL/Bali/DeclConcepts.thy Wed Aug 18 14:55:10 2010 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy Wed Aug 18 17:03:09 2010 +0200
@@ -98,7 +98,7 @@
lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
by (simp add: acc_modi_accmodi_def)
-instantiation decl_ext_type:: (type) has_accmodi
+instantiation decl_ext :: (type) has_accmodi
begin
definition
@@ -150,7 +150,7 @@
class has_declclass =
fixes declclass:: "'a \<Rightarrow> qtname"
-instantiation qtname_ext_type :: (type) has_declclass
+instantiation qtname_ext :: (type) has_declclass
begin
definition
@@ -162,7 +162,7 @@
lemma qtname_declclass_def:
"declclass q \<equiv> (q::qtname)"
- by (induct q) (simp add: declclass_qtname_ext_type_def)
+ by (induct q) (simp add: declclass_qtname_ext_def)
lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
by (simp add: qtname_declclass_def)
@@ -186,14 +186,14 @@
class has_static =
fixes is_static :: "'a \<Rightarrow> bool"
-instantiation decl_ext_type :: (has_static) has_static
+instantiation decl_ext :: (has_static) has_static
begin
instance ..
end
-instantiation member_ext_type :: (type) has_static
+instantiation member_ext :: (type) has_static
begin
instance ..
@@ -457,21 +457,21 @@
class has_resTy =
fixes resTy:: "'a \<Rightarrow> ty"
-instantiation decl_ext_type :: (has_resTy) has_resTy
+instantiation decl_ext :: (has_resTy) has_resTy
begin
instance ..
end
-instantiation member_ext_type :: (has_resTy) has_resTy
+instantiation member_ext :: (has_resTy) has_resTy
begin
instance ..
end
-instantiation mhead_ext_type :: (type) has_resTy
+instantiation mhead_ext :: (type) has_resTy
begin
instance ..
@@ -487,7 +487,7 @@
lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
by (simp add: mhead_def mhead_resTy_simp)
-instantiation prod :: ("type","has_resTy") has_resTy
+instantiation prod :: (type, has_resTy) has_resTy
begin
definition
--- a/src/HOL/Bali/Name.thy Wed Aug 18 14:55:10 2010 +0200
+++ b/src/HOL/Bali/Name.thy Wed Aug 18 17:03:09 2010 +0200
@@ -75,7 +75,7 @@
end
definition
- qtname_qtname_def: "qtname (q::'a qtname_ext_type) = q"
+ qtname_qtname_def: "qtname (q::'a qtname_scheme) = q"
translations
(type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
--- a/src/HOL/Bali/TypeRel.thy Wed Aug 18 14:55:10 2010 +0200
+++ b/src/HOL/Bali/TypeRel.thy Wed Aug 18 17:03:09 2010 +0200
@@ -512,12 +512,13 @@
apply (ind_cases "G\<turnstile>S\<preceq>NT")
by auto
-lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object"
-apply (case_tac T)
-apply (auto)
-apply (subgoal_tac "G\<turnstile>qtname_ext_type\<preceq>\<^sub>C Object")
-apply (auto intro: subcls_ObjectI)
-done
+lemma widen_Object:
+ assumes "isrtype G T" and "ws_prog G"
+ shows "G\<turnstile>RefT T \<preceq> Class Object"
+proof (cases T)
+ case (ClassT C) with assms have "G\<turnstile>C\<preceq>\<^sub>C Object" by (auto intro: subcls_ObjectI)
+ with ClassT show ?thesis by auto
+qed simp_all
lemma widen_trans_lemma [rule_format (no_asm)]:
"\<lbrakk>G\<turnstile>S\<preceq>U; \<forall>C. is_class G C \<longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object\<rbrakk> \<Longrightarrow> \<forall>T. G\<turnstile>U\<preceq>T \<longrightarrow> G\<turnstile>S\<preceq>T"
--- a/src/HOL/IsaMakefile Wed Aug 18 14:55:10 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Aug 18 17:03:09 2010 +0200
@@ -213,7 +213,6 @@
Tools/sat_funcs.ML \
Tools/sat_solver.ML \
Tools/split_rule.ML \
- Tools/typedef_codegen.ML \
Tools/typedef.ML \
Transitive_Closure.thy \
Typedef.thy \
@@ -303,7 +302,6 @@
Tools/Predicate_Compile/predicate_compile_specialisation.ML \
Tools/Predicate_Compile/predicate_compile_pred.ML \
Tools/quickcheck_generators.ML \
- Tools/quickcheck_record.ML \
Tools/Qelim/cooper.ML \
Tools/Qelim/cooper_procedure.ML \
Tools/Qelim/qelim.ML \
@@ -343,7 +341,6 @@
Tools/string_code.ML \
Tools/string_syntax.ML \
Tools/transfer.ML \
- Tools/typecopy.ML \
Tools/TFL/casesplit.ML \
Tools/TFL/dcterm.ML \
Tools/TFL/post.ML \
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Aug 18 14:55:10 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Aug 18 17:03:09 2010 +0200
@@ -174,9 +174,9 @@
Xcoord :: int
Ycoord :: int
-lemma "make_point_ext_type (dest_point_ext_type a) = a"
+lemma "Abs_point_ext (Rep_point_ext a) = a"
nitpick [expect = none]
-by (rule dest_point_ext_type_inverse)
+by (fact Rep_point_ext_inverse)
lemma "Fract a b = of_int a / of_int b"
nitpick [card = 1, expect = none]
--- a/src/HOL/Record.thy Wed Aug 18 14:55:10 2010 +0200
+++ b/src/HOL/Record.thy Wed Aug 18 17:03:09 2010 +0200
@@ -10,7 +10,7 @@
theory Record
imports Plain Quickcheck
-uses ("Tools/typecopy.ML") ("Tools/record.ML") ("Tools/quickcheck_record.ML")
+uses ("Tools/record.ML")
begin
subsection {* Introduction *}
@@ -452,9 +452,7 @@
subsection {* Record package *}
-use "Tools/typecopy.ML" setup Typecopy.setup
use "Tools/record.ML" setup Record.setup
-use "Tools/quickcheck_record.ML" setup Quickcheck_Record.setup
hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Aug 18 14:55:10 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Aug 18 17:03:09 2010 +0200
@@ -16,9 +16,9 @@
(* liberal addition of code data for datatypes *)
-fun mk_constr_consts thy vs dtco cos =
+fun mk_constr_consts thy vs tyco cos =
let
- val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
+ val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos;
val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
in if is_some (try (Code.constrset_of_consts thy) cs')
then SOME cs
@@ -62,12 +62,12 @@
(* equality *)
-fun mk_eq_eqns thy dtco =
+fun mk_eq_eqns thy tyco =
let
- val (vs, cos) = Datatype_Data.the_spec thy dtco;
+ val (vs, cos) = Datatype_Data.the_spec thy tyco;
val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
- Datatype_Data.the_info thy dtco;
- val ty = Type (dtco, map TFree vs);
+ Datatype_Data.the_info thy tyco;
+ val ty = Type (tyco, map TFree vs);
fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
$ t1 $ t2;
fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
@@ -88,11 +88,11 @@
|> Simpdata.mk_eq;
in (map prove (triv_injects @ injects @ distincts), prove refl) end;
-fun add_equality vs dtcos thy =
+fun add_equality vs tycos thy =
let
- fun add_def dtco lthy =
+ fun add_def tyco lthy =
let
- val ty = Type (dtco, map TFree vs);
+ val ty = Type (tyco, map TFree vs);
fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
$ Free ("x", ty) $ Free ("y", ty);
val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -105,35 +105,37 @@
in (thm', lthy') end;
fun tac thms = Class.intro_classes_tac []
THEN ALLGOALS (ProofContext.fact_tac thms);
- fun prefix dtco = Binding.qualify true (Long_Name.base_name dtco) o Binding.qualify true "eq" o Binding.name;
- fun add_eq_thms dtco =
+ fun prefix tyco = Binding.qualify true (Long_Name.base_name tyco) o Binding.qualify true "eq" o Binding.name;
+ fun add_eq_thms tyco =
Theory.checkpoint
- #> `(fn thy => mk_eq_eqns thy dtco)
+ #> `(fn thy => mk_eq_eqns thy tyco)
#-> (fn (thms, thm) => PureThy.note_thmss Thm.lemmaK
- [((prefix dtco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
- ((prefix dtco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
+ [((prefix tyco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
+ ((prefix tyco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
#> snd
in
thy
- |> Class.instantiation (dtcos, vs, [HOLogic.class_eq])
- |> fold_map add_def dtcos
+ |> Class.instantiation (tycos, vs, [HOLogic.class_eq])
+ |> fold_map add_def tycos
|-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
(fn _ => fn def_thms => tac def_thms) def_thms)
|-> (fn def_thms => fold Code.del_eqn def_thms)
- |> fold add_eq_thms dtcos
+ |> fold add_eq_thms tycos
end;
(* register a datatype etc. *)
-fun add_all_code config dtcos thy =
+fun add_all_code config tycos thy =
let
- val (vs :: _, coss) = (split_list o map (Datatype_Data.the_spec thy)) dtcos;
- val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
+ val (vs :: _, coss) = (split_list o map (Datatype_Data.the_spec thy)) tycos;
+ val any_css = map2 (mk_constr_consts thy vs) tycos coss;
val css = if exists is_none any_css then []
else map_filter I any_css;
- val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) dtcos;
- val certs = map (mk_case_cert thy) dtcos;
+ val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) tycos;
+ val certs = map (mk_case_cert thy) tycos;
+ val tycos_eq = filter_out
+ (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_eq]) tycos;
in
if null css then thy
else thy
@@ -141,7 +143,7 @@
|> fold Code.add_datatype css
|> fold_rev Code.add_default_eqn case_rewrites
|> fold Code.add_case certs
- |> add_equality vs dtcos
+ |> not (null tycos_eq) ? add_equality vs tycos_eq
end;
--- a/src/HOL/Tools/quickcheck_generators.ML Wed Aug 18 14:55:10 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Wed Aug 18 17:03:09 2010 +0200
@@ -10,10 +10,8 @@
val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
-> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
-> seed -> (('a -> 'b) * (unit -> term)) * seed
- val random_aux_specification: string -> string -> term list -> local_theory -> local_theory
- val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
- -> string list -> string list * string list -> typ list * typ list
- -> term list * (term * term) list
+ val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
+ -> (string * sort -> string * sort) option
val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
val compile_generator_expr:
theory -> bool -> term -> int -> term list option * (bool list * bool)
@@ -219,11 +217,11 @@
val is_rec = exists is_some ks;
val k = fold (fn NONE => I | SOME k => Integer.max k) ks 0;
val vs = Name.names Name.context "x" (map snd simple_tTs);
- val vs' = (map o apsnd) termifyT vs;
val tc = HOLogic.mk_return T @{typ Random.seed}
(HOLogic.mk_valtermify_app c vs simpleT);
- val t = HOLogic.mk_ST (map (fn (t, _) => (t, @{typ Random.seed})) tTs ~~ map SOME vs')
- tc @{typ Random.seed} (SOME T, @{typ Random.seed});
+ val t = HOLogic.mk_ST
+ (map2 (fn (t, _) => fn (v, T') => ((t, @{typ Random.seed}), SOME ((v, termifyT T')))) tTs vs)
+ tc @{typ Random.seed} (SOME T, @{typ Random.seed});
val tk = if is_rec
then if k = 0 then size
else @{term "Quickcheck.beyond :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
@@ -245,7 +243,7 @@
val auxs_rhss = map mk_select gen_exprss;
in (random_auxs, auxs_lhss ~~ auxs_rhss) end;
-fun mk_random_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
+fun instantiate_random_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
let
val _ = Datatype_Aux.message config "Creating quickcheck generators ...";
val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
@@ -272,11 +270,11 @@
fun perhaps_constrain thy insts raw_vs =
let
- fun meet_random (T, sort) = Sorts.meet_sort (Sign.classes_of thy)
+ fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy)
(Logic.varifyT_global T, sort);
val vtab = Vartab.empty
|> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
- |> fold meet_random insts;
+ |> fold meet insts;
in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
end handle Sorts.CLASS_ERROR _ => NONE;
@@ -297,7 +295,7 @@
can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
in if has_inst then thy
else case perhaps_constrain thy (random_insts @ term_of_insts) typerep_vs
- of SOME constrain => mk_random_datatype config descr
+ of SOME constrain => instantiate_random_datatype config descr
(map constrain typerep_vs) tycos prfx (names, auxnames)
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
| NONE => thy
@@ -385,22 +383,19 @@
fun compile_generator_expr thy report t =
let
val Ts = (map snd o fst o strip_abs) t;
- in
- if report then
- let
- val t' = mk_reporting_generator_expr thy t Ts;
- val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref)
- (fn proc => fn g => fn s => g s #>> ((apfst o Option.map o map) proc)) thy t' [];
- in
- compile #> Random_Engine.run
- end
- else
- let
- val t' = mk_generator_expr thy t Ts;
- val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
- (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
- val dummy_report = ([], false)
- in fn s => ((compile #> Random_Engine.run) s, dummy_report) end
+ in if report then
+ let
+ val t' = mk_reporting_generator_expr thy t Ts;
+ val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref)
+ (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) thy t' [];
+ in compile #> Random_Engine.run end
+ else
+ let
+ val t' = mk_generator_expr thy t Ts;
+ val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
+ (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+ val dummy_report = ([], false)
+ in compile #> Random_Engine.run #> rpair dummy_report end
end;
--- a/src/HOL/Tools/quickcheck_record.ML Wed Aug 18 14:55:10 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Title: HOL/Tools/quickcheck_record.ML
- Author: Florian Haftmann, TU Muenchen
-
-Quickcheck generators for records.
-*)
-
-signature QUICKCHECK_RECORD =
-sig
- val ensure_random_typecopy: string -> theory -> theory
- val setup: theory -> theory
-end;
-
-structure Quickcheck_Record : QUICKCHECK_RECORD =
-struct
-
-fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
-val size = @{term "i::code_numeral"};
-
-fun mk_random_typecopy tyco vs constr T' thy =
- let
- val mk_const = curry (Sign.mk_const thy);
- val Ts = map TFree vs;
- val T = Type (tyco, Ts);
- val Tm = termifyT T;
- val Tm' = termifyT T';
- val v = "x";
- val t_v = Free (v, Tm');
- val t_constr = Const (constr, T' --> T);
- val lhs = HOLogic.mk_random T size;
- val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))]
- (HOLogic.mk_return Tm @{typ Random.seed}
- (mk_const "Code_Evaluation.valapp" [T', T]
- $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
- @{typ Random.seed} (SOME Tm, @{typ Random.seed});
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
- in
- thy
- |> Class.instantiation ([tyco], vs, @{sort random})
- |> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
- |> snd
- |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end;
-
-fun ensure_random_typecopy tyco thy =
- let
- val SOME { vs = raw_vs, constr, typ = raw_T, ... } =
- Typecopy.get_info thy tyco;
- val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
- val T = map_atyps (fn TFree (v, sort) =>
- TFree (v, constrain sort @{sort random})) raw_T;
- val vs' = Term.add_tfreesT T [];
- val vs = map (fn (v, sort) =>
- (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
- val can_inst = Sign.of_sort thy (T, @{sort random});
- in if can_inst then mk_random_typecopy tyco vs constr T thy else thy end;
-
-val setup = Typecopy.interpretation ensure_random_typecopy;
-
-end;
--- a/src/HOL/Tools/record.ML Wed Aug 18 14:55:10 2010 +0200
+++ b/src/HOL/Tools/record.ML Wed Aug 18 17:03:09 2010 +0200
@@ -93,21 +93,29 @@
fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *)
);
-fun do_typedef b repT alphas thy =
+fun get_typedef_info tyco vs (({ rep_type, Abs_name, Rep_name, ...},
+ { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy =
let
- val (b_constr, b_proj) = (Binding.prefix_name "make_" b, Binding.prefix_name "dest_" b);
- fun get_thms thy tyco =
- let
- val SOME { vs, constr, typ = repT, proj_inject, proj_constr, ... } =
- Typecopy.get_info thy tyco;
- val absT = Type (tyco, map TFree vs);
- in
- ((proj_inject, proj_constr), Const (constr, repT --> absT), absT)
- end;
+ val exists_thm =
+ UNIV_I
+ |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
+ val proj_constr = Abs_inverse OF [exists_thm];
+ val absT = Type (tyco, map TFree vs);
in
thy
- |> Typecopy.typecopy (b, alphas) repT b_constr b_proj
- |-> (fn (tyco, _) => `(fn thy => get_thms thy tyco))
+ |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))
+ end
+
+fun do_typedef raw_tyco repT raw_vs thy =
+ let
+ val ctxt = ProofContext.init_global thy |> Variable.declare_typ repT;
+ val vs = map (ProofContext.check_tfree ctxt) raw_vs;
+ val tac = Tactic.rtac UNIV_witness 1;
+ in
+ thy
+ |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
+ (HOLogic.mk_UNIV repT) NONE tac
+ |-> (fn (tyco, info) => get_typedef_info tyco vs info)
end;
fun mk_cons_tuple (left, right) =
@@ -127,7 +135,7 @@
let
val repT = HOLogic.mk_prodT (leftT, rightT);
- val (((rep_inject, abs_inverse), absC, absT), typ_thy) =
+ val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =
thy
|> do_typedef b repT alphas
||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
@@ -155,7 +163,6 @@
cdef_thy
|> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
|> Sign.restore_naming thy
- |> Code.add_default_eqn isom_def;
in
((isom, cons $ isom), thm_thy)
end;
@@ -230,8 +237,8 @@
val wN = "w";
val moreN = "more";
val schemeN = "_scheme";
-val ext_typeN = "_ext_type";
-val inner_typeN = "_inner_type";
+val ext_typeN = "_ext";
+val inner_typeN = "_inner";
val extN ="_ext";
val updateN = "_update";
val makeN = "make";
@@ -1614,7 +1621,8 @@
val ext_binding = Binding.name (suffix extN base_name);
val ext_name = suffix extN name;
- val extT = Type (suffix ext_typeN name, map TFree alphas_zeta);
+ val ext_tyco = suffix ext_typeN name
+ val extT = Type (ext_tyco, map TFree alphas_zeta);
val ext_type = fields_moreTs ---> extT;
@@ -1768,10 +1776,9 @@
[("ext_induct", induct),
("ext_inject", inject),
("ext_surjective", surject),
- ("ext_split", split_meta)])
- ||> Code.add_default_eqn ext_def;
-
- in ((extT, induct', inject', surjective', split_meta', ext_def), thm_thy) end;
+ ("ext_split", split_meta)]);
+
+ in (((ext_name, ext_type), (ext_tyco, alphas_zeta), extT, induct', inject', surjective', split_meta', ext_def), thm_thy) end;
fun chunks [] [] = []
| chunks [] xs = [xs]
@@ -1815,6 +1822,73 @@
in Thm.implies_elim thm' thm end;
+(* code generation *)
+
+fun instantiate_random_record tyco vs extN Ts thy =
+ let
+ val size = @{term "i::code_numeral"};
+ fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
+ val T = Type (tyco, map TFree vs);
+ val Tm = termifyT T;
+ val params = Name.names Name.context "x" Ts;
+ val lhs = HOLogic.mk_random T size;
+ val tc = HOLogic.mk_return Tm @{typ Random.seed}
+ (HOLogic.mk_valtermify_app extN params T);
+ val rhs = HOLogic.mk_ST
+ (map (fn (v, T') => ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
+ tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
+ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+ in
+ thy
+ |> Class.instantiation ([tyco], vs, @{sort random})
+ |> `(fn lthy => Syntax.check_term lthy eq)
+ |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
+ |> snd
+ |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+ end;
+
+fun ensure_random_record ext_tyco vs extN Ts thy =
+ let
+ val algebra = Sign.classes_of thy;
+ val has_inst = can (Sorts.mg_domain algebra ext_tyco) @{sort random};
+ in if has_inst then thy
+ else case Quickcheck_Generators.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs
+ of SOME constrain => instantiate_random_record ext_tyco (map constrain vs) extN
+ ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
+ | NONE => thy
+ end;
+
+fun add_code ext_tyco vs extT ext simps inject thy =
+ let
+ val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
+ (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT),
+ Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
+ fun tac eq_def = Class.intro_classes_tac []
+ THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
+ THEN ALLGOALS (rtac @{thm refl});
+ fun mk_eq thy eq_def = Simplifier.rewrite_rule
+ [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
+ fun mk_eq_refl thy = @{thm HOL.eq_refl}
+ |> Thm.instantiate
+ ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], [])
+ |> AxClass.unoverload thy;
+ in
+ thy
+ |> Code.add_datatype [ext]
+ |> fold Code.add_default_eqn simps
+ |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_eq])
+ |> `(fn lthy => Syntax.check_term lthy eq)
+ |-> (fn eq => Specification.definition
+ (NONE, (Attrib.empty_binding, eq)))
+ |-> (fn (_, (_, eq_def)) =>
+ Class.prove_instantiation_exit_result Morphism.thm
+ (fn _ => fn eq_def => tac eq_def) eq_def)
+ |-> (fn eq_def => fn thy => thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
+ |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
+ |> ensure_random_record ext_tyco vs (fst ext) ((fst o strip_type o snd) ext)
+ end;
+
+
(* definition *)
fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
@@ -1870,7 +1944,7 @@
val extension_name = full binding;
- val ((extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
+ val ((ext, (ext_tyco, vs), extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
thy
|> Sign.qualified_path false binding
|> extension_definition extension_name fields alphas_ext zeta moreT more vars;
@@ -2042,12 +2116,6 @@
upd_specs
||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
[make_spec, fields_spec, extend_spec, truncate_spec]
- |->
- (fn defs as ((sel_defs, upd_defs), derived_defs) =>
- fold Code.add_default_eqn sel_defs
- #> fold Code.add_default_eqn upd_defs
- #> fold Code.add_default_eqn derived_defs
- #> pair defs)
||> Theory.checkpoint
val (((sel_defs, upd_defs), derived_defs), defs_thy) =
timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
@@ -2330,6 +2398,7 @@
|> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
|> add_extfields extension_name (fields @ [(full_moreN, moreT)])
|> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
+ |> add_code ext_tyco vs extT ext simps' ext_inject
|> Sign.restore_naming thy;
in final_thy end;
--- a/src/HOL/Tools/typecopy.ML Wed Aug 18 14:55:10 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,134 +0,0 @@
-(* Title: HOL/Tools/typecopy.ML
- Author: Florian Haftmann, TU Muenchen
-
-Introducing copies of types using trivial typedefs; datatype-like abstraction.
-*)
-
-signature TYPECOPY =
-sig
- type info = { vs: (string * sort) list, typ: typ, constr: string, proj: string,
- constr_inject: thm, proj_inject: thm, constr_proj: thm, proj_constr: thm }
- val typecopy: binding * (string * sort) list -> typ -> binding -> binding
- -> theory -> (string * info) * theory
- val get_info: theory -> string -> info option
- val interpretation: (string -> theory -> theory) -> theory -> theory
- val add_default_code: string -> theory -> theory
- val setup: theory -> theory
-end;
-
-structure Typecopy: TYPECOPY =
-struct
-
-(* theory data *)
-
-type info = {
- vs: (string * sort) list,
- typ: typ,
- constr: string,
- proj: string,
- constr_inject: thm,
- proj_inject: thm,
- constr_proj: thm,
- proj_constr: thm
-};
-
-structure Typecopy_Data = Theory_Data
-(
- type T = info Symtab.table;
- val empty = Symtab.empty;
- val extend = I;
- fun merge data = Symtab.merge (K true) data;
-);
-
-val get_info = Symtab.lookup o Typecopy_Data.get;
-
-
-(* interpretation of type copies *)
-
-structure Typecopy_Interpretation = Interpretation(type T = string val eq = op =);
-val interpretation = Typecopy_Interpretation.interpretation;
-
-
-(* introducing typecopies *)
-
-fun add_info tyco vs (({ rep_type, Abs_name, Rep_name, ...},
- { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy =
- let
- val exists_thm =
- UNIV_I
- |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
- val constr_inject = Abs_inject OF [exists_thm, exists_thm];
- val proj_constr = Abs_inverse OF [exists_thm];
- val info = {
- vs = vs,
- typ = rep_type,
- constr = Abs_name,
- proj = Rep_name,
- constr_inject = constr_inject,
- proj_inject = Rep_inject,
- constr_proj = Rep_inverse,
- proj_constr = proj_constr
- };
- in
- thy
- |> (Typecopy_Data.map o Symtab.update_new) (tyco, info)
- |> Typecopy_Interpretation.data tyco
- |> pair (tyco, info)
- end
-
-fun typecopy (raw_tyco, raw_vs) raw_ty constr proj thy =
- let
- val ty = Sign.certify_typ thy raw_ty;
- val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
- val vs = map (ProofContext.check_tfree ctxt) raw_vs;
- val tac = Tactic.rtac UNIV_witness 1;
- in
- thy
- |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
- (HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac
- |-> (fn (tyco, info) => add_info tyco vs info)
- end;
-
-
-(* default code setup *)
-
-fun add_default_code tyco thy =
- let
- val SOME { vs, typ = ty_rep, constr = c, proj, proj_constr, proj_inject, ... } =
- get_info thy tyco;
- val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
- val ty = Type (tyco, map TFree vs);
- val proj = Const (proj, ty --> ty_rep);
- val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
- val eq_lhs = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
- $ t_x $ t_y;
- val eq_rhs = HOLogic.mk_eq (proj $ t_x, proj $ t_y);
- val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (eq_lhs, eq_rhs);
- fun tac eq_thm = Class.intro_classes_tac []
- THEN (Simplifier.rewrite_goals_tac
- (map Simpdata.mk_eq [eq_thm, @{thm eq}, proj_inject]))
- THEN ALLGOALS (rtac @{thm refl});
- fun mk_eq_refl thy = @{thm HOL.eq_refl}
- |> Thm.instantiate
- ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global ty)], [])
- |> AxClass.unoverload thy;
- in
- thy
- |> Code.add_datatype [constr]
- |> Code.add_eqn proj_constr
- |> Class.instantiation ([tyco], vs, [HOLogic.class_eq])
- |> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition
- (NONE, (Attrib.empty_binding, eq)))
- |-> (fn (_, (_, eq_thm)) =>
- Class.prove_instantiation_exit_result Morphism.thm
- (fn _ => fn eq_thm => tac eq_thm) eq_thm)
- |-> (fn eq_thm => Code.add_eqn eq_thm)
- |> (fn thy => Code.add_nbe_eqn (mk_eq_refl thy) thy)
- end;
-
-val setup =
- Typecopy_Interpretation.init
- #> interpretation add_default_code
-
-end;
--- a/src/HOL/Tools/typedef_codegen.ML Wed Aug 18 14:55:10 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-(* Title: HOL/Tools/typedef_codegen.ML
- Author: Stefan Berghofer, TU Muenchen
-
-Code generators for trivial typedefs.
-*)
-
-signature TYPEDEF_CODEGEN =
-sig
- val setup: theory -> theory
-end;
-
-structure TypedefCodegen: TYPEDEF_CODEGEN =
-struct
-
-fun typedef_codegen thy defs dep module brack t gr =
- let
- fun get_name (Type (tname, _)) = tname
- | get_name _ = "";
- fun mk_fun s T ts =
- let
- val (_, gr') = Codegen.invoke_tycodegen thy defs dep module false T gr;
- val (ps, gr'') =
- fold_map (Codegen.invoke_codegen thy defs dep module true) ts gr';
- val id = Codegen.mk_qual_id module (Codegen.get_const_id gr'' s)
- in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end;
- fun lookup f T =
- (* FIXME handle multiple typedef interpretations (!??) *)
- (case Typedef.get_info_global thy (get_name T) of
- [info] => f info
- | _ => "");
- in
- (case strip_comb t of
- (Const (s, Type ("fun", [T, U])), ts) =>
- if lookup (#Rep_name o #1) T = s andalso
- is_none (Codegen.get_assoc_type thy (get_name T))
- then mk_fun s T ts
- else if lookup (#Abs_name o #1) U = s andalso
- is_none (Codegen.get_assoc_type thy (get_name U))
- then mk_fun s U ts
- else NONE
- | _ => NONE)
- end;
-
-fun mk_tyexpr [] s = Codegen.str s
- | mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)]
- | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
-
-fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
- (case Typedef.get_info_global thy s of
- (* FIXME handle multiple typedef interpretations (!??) *)
- [({abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}, _)] =>
- if is_some (Codegen.get_assoc_type thy tname) then NONE
- else
- let
- val module' = Codegen.if_library
- (Codegen.thyname_of_type thy tname) module;
- val node_id = tname ^ " (type)";
- val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
- (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
- Ts ||>>
- Codegen.mk_const_id module' Abs_name ||>>
- Codegen.mk_const_id module' Rep_name ||>>
- Codegen.mk_type_id module' s;
- val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
- in
- SOME (tyexpr, case try (Codegen.get_node gr') node_id of
- NONE =>
- let
- val (p :: ps, gr'') = fold_map
- (Codegen.invoke_tycodegen thy defs node_id module' false)
- (oldT :: Us) (Codegen.add_edge (node_id, dep)
- (Codegen.new_node (node_id, (NONE, "", "")) gr'));
- val s =
- Codegen.string_of (Pretty.block [Codegen.str "datatype ",
- mk_tyexpr ps (snd ty_id),
- Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
- Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
- Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
- Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
- Codegen.str "x) = x;"]) ^ "\n\n" ^
- (if member (op =) (!Codegen.mode) "term_of" then
- Codegen.string_of (Pretty.block [Codegen.str "fun ",
- Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
- Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
- Codegen.str "x) =", Pretty.brk 1,
- Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
- Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
- Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
- Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
- Codegen.str "x;"]) ^ "\n\n"
- else "") ^
- (if member (op =) (!Codegen.mode) "test" then
- Codegen.string_of (Pretty.block [Codegen.str "fun ",
- Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
- Codegen.str "i =", Pretty.brk 1,
- Pretty.block [Codegen.str (Abs_id ^ " ("),
- Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
- Codegen.str "i);"]]) ^ "\n\n"
- else "")
- in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
- | SOME _ => Codegen.add_edge (node_id, dep) gr')
- end
- | _ => NONE)
- | typedef_tycodegen thy defs dep module brack _ gr = NONE;
-
-val setup =
- Codegen.add_codegen "typedef" typedef_codegen
- #> Codegen.add_tycodegen "typedef" typedef_tycodegen
-
-end;
--- a/src/HOL/Typedef.thy Wed Aug 18 14:55:10 2010 +0200
+++ b/src/HOL/Typedef.thy Wed Aug 18 17:03:09 2010 +0200
@@ -6,9 +6,7 @@
theory Typedef
imports Set
-uses
- ("Tools/typedef.ML")
- ("Tools/typedef_codegen.ML")
+uses ("Tools/typedef.ML")
begin
ML {*
@@ -115,6 +113,5 @@
end
use "Tools/typedef.ML" setup Typedef.setup
-use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
end