1.1 --- a/src/HOL/Tools/record.ML Wed Jul 06 11:37:29 2011 +0200
1.2 +++ b/src/HOL/Tools/record.ML Wed Jul 06 13:31:12 2011 +0200
1.3 @@ -9,9 +9,9 @@
1.4
1.5 signature RECORD =
1.6 sig
1.7 - val print_type_abbr: bool Unsynchronized.ref
1.8 - val print_type_as_fields: bool Unsynchronized.ref
1.9 - val timing: bool Unsynchronized.ref
1.10 + val type_abbr: bool Config.T
1.11 + val type_as_fields: bool Config.T
1.12 + val timing: bool Config.T
1.13
1.14 type info =
1.15 {args: (string * sort) list,
1.16 @@ -256,9 +256,9 @@
1.17
1.18 (* timing *)
1.19
1.20 -val timing = Unsynchronized.ref false;
1.21 -fun timeit_msg s x = if ! timing then (warning s; timeit x) else x ();
1.22 -fun timing_msg s = if ! timing then warning s else ();
1.23 +val timing = Attrib.setup_config_bool @{binding record_timing} (K false);
1.24 +fun timeit_msg ctxt s x = if Config.get ctxt timing then (warning s; timeit x) else x ();
1.25 +fun timing_msg ctxt s = if Config.get ctxt timing then warning s else ();
1.26
1.27
1.28 (* syntax *)
1.29 @@ -792,8 +792,8 @@
1.30
1.31 (* print translations *)
1.32
1.33 -val print_type_abbr = Unsynchronized.ref true;
1.34 -val print_type_as_fields = Unsynchronized.ref true;
1.35 +val type_abbr = Attrib.setup_config_bool @{binding record_type_abbr} (K true);
1.36 +val type_as_fields = Attrib.setup_config_bool @{binding record_type_as_fields} (K true);
1.37
1.38
1.39 local
1.40 @@ -842,7 +842,7 @@
1.41 foldr1 field_types_tr'
1.42 (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
1.43 in
1.44 - if not (! print_type_as_fields) orelse null fields then raise Match
1.45 + if not (Config.get ctxt type_as_fields) orelse null fields then raise Match
1.46 else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
1.47 else
1.48 Syntax.const @{syntax_const "_record_type_scheme"} $ u $
1.49 @@ -864,7 +864,7 @@
1.50
1.51 fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
1.52 in
1.53 - if ! print_type_abbr then
1.54 + if Config.get ctxt type_abbr then
1.55 (case last_extT T of
1.56 SOME (name, _) =>
1.57 if name = last_ext then
1.58 @@ -1571,6 +1571,8 @@
1.59
1.60 fun extension_definition name fields alphas zeta moreT more vars thy =
1.61 let
1.62 + val ctxt = Proof_Context.init_global thy;
1.63 +
1.64 val base_name = Long_Name.base_name name;
1.65
1.66 val fieldTs = map snd fields;
1.67 @@ -1621,14 +1623,14 @@
1.68 in (term, thy') end
1.69 end;
1.70
1.71 - val _ = timing_msg "record extension preparing definitions";
1.72 + val _ = timing_msg ctxt "record extension preparing definitions";
1.73
1.74
1.75 (* 1st stage part 1: introduce the tree of new types *)
1.76
1.77 fun get_meta_tree () = build_meta_tree_type 1 thy vars more;
1.78 val (ext_body, typ_thy) =
1.79 - timeit_msg "record extension nested type def:" get_meta_tree;
1.80 + timeit_msg ctxt "record extension nested type def:" get_meta_tree;
1.81
1.82
1.83 (* prepare declarations and definitions *)
1.84 @@ -1644,12 +1646,12 @@
1.85 |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
1.86 ||> Theory.checkpoint
1.87 val ([ext_def], defs_thy) =
1.88 - timeit_msg "record extension constructor def:" mk_defs;
1.89 + timeit_msg ctxt "record extension constructor def:" mk_defs;
1.90
1.91
1.92 (* prepare propositions *)
1.93
1.94 - val _ = timing_msg "record extension preparing propositions";
1.95 + val _ = timing_msg ctxt "record extension preparing propositions";
1.96 val vars_more = vars @ [more];
1.97 val variants = map (fn Free (x, _) => x) vars_more;
1.98 val ext = mk_ext vars_more;
1.99 @@ -1686,7 +1688,7 @@
1.100 Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
1.101 rtac refl 1)));
1.102
1.103 - val inject = timeit_msg "record extension inject proof:" inject_prf;
1.104 + val inject = timeit_msg ctxt "record extension inject proof:" inject_prf;
1.105
1.106 (*We need a surjection property r = (| f = f r, g = g r ... |)
1.107 to prove other theorems. We haven't given names to the accessors
1.108 @@ -1708,7 +1710,7 @@
1.109 in
1.110 surject
1.111 end;
1.112 - val surject = timeit_msg "record extension surjective proof:" surject_prf;
1.113 + val surject = timeit_msg ctxt "record extension surjective proof:" surject_prf;
1.114
1.115 fun split_meta_prf () =
1.116 prove_standard [] split_meta_prop
1.117 @@ -1718,7 +1720,7 @@
1.118 etac meta_allE, atac,
1.119 rtac (prop_subst OF [surject]),
1.120 REPEAT o etac meta_allE, atac]);
1.121 - val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
1.122 + val split_meta = timeit_msg ctxt "record extension split_meta proof:" split_meta_prf;
1.123
1.124 fun induct_prf () =
1.125 let val (assm, concl) = induct_prop in
1.126 @@ -1728,7 +1730,7 @@
1.127 resolve_tac prems 2 THEN
1.128 asm_simp_tac HOL_ss 1)
1.129 end;
1.130 - val induct = timeit_msg "record extension induct proof:" induct_prf;
1.131 + val induct = timeit_msg ctxt "record extension induct proof:" induct_prf;
1.132
1.133 val ([induct', inject', surjective', split_meta'], thm_thy) =
1.134 defs_thy
1.135 @@ -1869,8 +1871,9 @@
1.136 |> Thm.instantiate
1.137 ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
1.138 |> AxClass.unoverload thy;
1.139 - val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq)
1.140 - val ensure_exhaustive_record = ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq)
1.141 + val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
1.142 + val ensure_exhaustive_record =
1.143 + ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
1.144 in
1.145 thy
1.146 |> Code.add_datatype [ext]
1.147 @@ -1894,6 +1897,8 @@
1.148
1.149 fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
1.150 let
1.151 + val ctxt = Proof_Context.init_global thy;
1.152 +
1.153 val prefix = Binding.name_of binding;
1.154 val name = Sign.full_name thy binding;
1.155 val full = Sign.full_name_path thy prefix;
1.156 @@ -1951,7 +1956,7 @@
1.157 |> Sign.qualified_path false binding
1.158 |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
1.159
1.160 - val _ = timing_msg "record preparing definitions";
1.161 + val _ = timing_msg ctxt "record preparing definitions";
1.162 val Type extension_scheme = extT;
1.163 val extension_name = unsuffix ext_typeN (fst extension_scheme);
1.164 val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
1.165 @@ -2055,7 +2060,7 @@
1.166 updaccs RL [updacc_cong_from_eq])
1.167 end;
1.168 val (accessor_thms, updator_thms, upd_acc_cong_assists) =
1.169 - timeit_msg "record getting tree access/updates:" get_access_update_thms;
1.170 + timeit_msg ctxt "record getting tree access/updates:" get_access_update_thms;
1.171
1.172 fun lastN xs = drop parent_fields_len xs;
1.173
1.174 @@ -2121,11 +2126,11 @@
1.175 [make_spec, fields_spec, extend_spec, truncate_spec]
1.176 ||> Theory.checkpoint
1.177 val (((sel_defs, upd_defs), derived_defs), defs_thy) =
1.178 - timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
1.179 + timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
1.180 mk_defs;
1.181
1.182 (* prepare propositions *)
1.183 - val _ = timing_msg "record preparing propositions";
1.184 + val _ = timing_msg ctxt "record preparing propositions";
1.185 val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
1.186 val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
1.187 val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
1.188 @@ -2205,17 +2210,17 @@
1.189
1.190 fun sel_convs_prf () =
1.191 map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
1.192 - val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
1.193 + val sel_convs = timeit_msg ctxt "record sel_convs proof:" sel_convs_prf;
1.194 fun sel_convs_standard_prf () = map Drule.export_without_context sel_convs;
1.195 val sel_convs_standard =
1.196 - timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
1.197 + timeit_msg ctxt "record sel_convs_standard proof:" sel_convs_standard_prf;
1.198
1.199 fun upd_convs_prf () =
1.200 map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
1.201 - val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
1.202 + val upd_convs = timeit_msg ctxt "record upd_convs proof:" upd_convs_prf;
1.203 fun upd_convs_standard_prf () = map Drule.export_without_context upd_convs;
1.204 val upd_convs_standard =
1.205 - timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
1.206 + timeit_msg ctxt "record upd_convs_standard proof:" upd_convs_standard_prf;
1.207
1.208 fun get_upd_acc_congs () =
1.209 let
1.210 @@ -2224,7 +2229,7 @@
1.211 val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
1.212 in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
1.213 val (fold_congs, unfold_congs) =
1.214 - timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
1.215 + timeit_msg ctxt "record upd fold/unfold congs:" get_upd_acc_congs;
1.216
1.217 val parent_induct = Option.map #induct_scheme (try List.last parents);
1.218
1.219 @@ -2235,7 +2240,7 @@
1.220 [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
1.221 try_param_tac rN ext_induct 1,
1.222 asm_simp_tac HOL_basic_ss 1]);
1.223 - val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
1.224 + val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" induct_scheme_prf;
1.225
1.226 fun induct_prf () =
1.227 let val (assm, concl) = induct_prop in
1.228 @@ -2244,7 +2249,7 @@
1.229 THEN try_param_tac "more" @{thm unit.induct} 1
1.230 THEN resolve_tac prems 1)
1.231 end;
1.232 - val induct = timeit_msg "record induct proof:" induct_prf;
1.233 + val induct = timeit_msg ctxt "record induct proof:" induct_prf;
1.234
1.235 fun cases_scheme_prf () =
1.236 let
1.237 @@ -2257,14 +2262,14 @@
1.238 in Object_Logic.rulify (mp OF [ind, refl]) end;
1.239
1.240 val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
1.241 - val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
1.242 + val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" cases_scheme_prf;
1.243
1.244 fun cases_prf () =
1.245 prove_standard [] cases_prop
1.246 (fn _ =>
1.247 try_param_tac rN cases_scheme 1 THEN
1.248 simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]);
1.249 - val cases = timeit_msg "record cases proof:" cases_prf;
1.250 + val cases = timeit_msg ctxt "record cases proof:" cases_prf;
1.251
1.252 fun surjective_prf () =
1.253 let
1.254 @@ -2280,7 +2285,7 @@
1.255 (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
1.256 (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
1.257 end;
1.258 - val surjective = timeit_msg "record surjective proof:" surjective_prf;
1.259 + val surjective = timeit_msg ctxt "record surjective proof:" surjective_prf;
1.260
1.261 fun split_meta_prf () =
1.262 prove false [] split_meta_prop
1.263 @@ -2290,10 +2295,10 @@
1.264 etac meta_allE, atac,
1.265 rtac (prop_subst OF [surjective]),
1.266 REPEAT o etac meta_allE, atac]);
1.267 - val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
1.268 + val split_meta = timeit_msg ctxt "record split_meta proof:" split_meta_prf;
1.269 fun split_meta_standardise () = Drule.export_without_context split_meta;
1.270 val split_meta_standard =
1.271 - timeit_msg "record split_meta standard:" split_meta_standardise;
1.272 + timeit_msg ctxt "record split_meta standard:" split_meta_standardise;
1.273
1.274 fun split_object_prf () =
1.275 let
1.276 @@ -2320,7 +2325,7 @@
1.277
1.278
1.279 val split_object_prf = future_forward_prf split_object_prf split_object_prop;
1.280 - val split_object = timeit_msg "record split_object proof:" split_object_prf;
1.281 + val split_object = timeit_msg ctxt "record split_object proof:" split_object_prf;
1.282
1.283
1.284 fun split_ex_prf () =
1.285 @@ -2333,7 +2338,7 @@
1.286 in
1.287 prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1)
1.288 end;
1.289 - val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
1.290 + val split_ex = timeit_msg ctxt "record split_ex proof:" split_ex_prf;
1.291
1.292 fun equality_tac thms =
1.293 let
1.294 @@ -2351,7 +2356,7 @@
1.295 Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
1.296 (*simp_all_tac ss (sel_convs) would also work but is less efficient*)
1.297 end);
1.298 - val equality = timeit_msg "record equality proof:" equality_prf;
1.299 + val equality = timeit_msg ctxt "record equality proof:" equality_prf;
1.300
1.301 val ((([sel_convs', upd_convs', sel_defs', upd_defs',
1.302 fold_congs', unfold_congs',