# HG changeset patch # User haftmann # Date 1282143789 -7200 # Node ID 5c69afe3df06f4d682594c2d6da503985316db0f # Parent f2709bc1e41f07357d4063c63481898ddccac1e9# Parent e30c782329bfaf903f1839e4b79a77e01ed6d8dc merged diff -r f2709bc1e41f -r 5c69afe3df06 NEWS --- 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. diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/Bali/DeclConcepts.thy --- 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 \ 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 \ (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 \ 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 \ 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 diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/Bali/Name.thy --- 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) "\pid::pname,tid::tname\" diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/Bali/TypeRel.thy --- 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\S\NT") by auto -lemma widen_Object:"\isrtype G T;ws_prog G\ \ G\RefT T \ Class Object" -apply (case_tac T) -apply (auto) -apply (subgoal_tac "G\qtname_ext_type\\<^sub>C Object") -apply (auto intro: subcls_ObjectI) -done +lemma widen_Object: + assumes "isrtype G T" and "ws_prog G" + shows "G\RefT T \ Class Object" +proof (cases T) + case (ClassT C) with assms have "G\C\\<^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)]: "\G\S\U; \C. is_class G C \ G\C\\<^sub>C Object\ \ \T. G\U\T \ G\S\T" diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/IsaMakefile --- 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 \ diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/Nitpick_Examples/Typedef_Nits.thy --- 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] diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/Record.thy --- 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 diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/Tools/Datatype/datatype_codegen.ML --- 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; diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/Tools/quickcheck_generators.ML --- 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 \ code_numeral \ 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; diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/Tools/quickcheck_record.ML --- 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; diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/Tools/record.ML --- 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; diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/Tools/typecopy.ML --- 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; diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/Tools/typedef_codegen.ML --- 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; diff -r f2709bc1e41f -r 5c69afe3df06 src/HOL/Typedef.thy --- 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