1.1 --- a/src/HOL/Tools/record.ML Wed Jul 06 17:19:34 2011 +0100
1.2 +++ b/src/HOL/Tools/record.ML Wed Jul 06 23:11:59 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 @@ -670,6 +670,15 @@
1.30
1.31 local
1.32
1.33 +fun split_args (field :: fields) ((name, arg) :: fargs) =
1.34 + if can (unsuffix name) field then
1.35 + let val (args, rest) = split_args fields fargs
1.36 + in (arg :: args, rest) end
1.37 + else raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name)
1.38 + | split_args [] (fargs as (_ :: _)) = ([], fargs)
1.39 + | split_args (_ :: _) [] = raise Fail "expecting more fields"
1.40 + | split_args _ _ = ([], []);
1.41 +
1.42 fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
1.43 (name, arg)
1.44 | field_type_tr t = raise TERM ("field_type_tr", [t]);
1.45 @@ -683,15 +692,6 @@
1.46 val thy = Proof_Context.theory_of ctxt;
1.47 fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
1.48
1.49 - fun split_args (field :: fields) ((name, arg) :: fargs) =
1.50 - if can (unsuffix name) field then
1.51 - let val (args, rest) = split_args fields fargs
1.52 - in (arg :: args, rest) end
1.53 - else err ("expecting field " ^ field ^ " but got " ^ name)
1.54 - | split_args [] (fargs as (_ :: _)) = ([], fargs)
1.55 - | split_args (_ :: _) [] = err "expecting more fields"
1.56 - | split_args _ _ = ([], []);
1.57 -
1.58 fun mk_ext (fargs as (name, _) :: _) =
1.59 (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
1.60 SOME (ext, alphas) =>
1.61 @@ -700,7 +700,8 @@
1.62 let
1.63 val (fields', _) = split_last fields;
1.64 val types = map snd fields';
1.65 - val (args, rest) = split_args (map fst fields') fargs;
1.66 + val (args, rest) = split_args (map fst fields') fargs
1.67 + handle Fail msg => err msg;
1.68 val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
1.69 val midx = fold Term.maxidx_typ argtypes 0;
1.70 val varifyT = varifyT midx;
1.71 @@ -717,8 +718,8 @@
1.72 list_comb
1.73 (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
1.74 end
1.75 - | NONE => err ("no fields defined for " ^ ext))
1.76 - | NONE => err (name ^ " is no proper field"))
1.77 + | NONE => err ("no fields defined for " ^ quote ext))
1.78 + | NONE => err (quote name ^ " is no proper field"))
1.79 | mk_ext [] = more;
1.80 in
1.81 mk_ext (field_types_tr t)
1.82 @@ -742,27 +743,18 @@
1.83 val thy = Proof_Context.theory_of ctxt;
1.84 fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
1.85
1.86 - fun split_args (field :: fields) ((name, arg) :: fargs) =
1.87 - if can (unsuffix name) field
1.88 - then
1.89 - let val (args, rest) = split_args fields fargs
1.90 - in (arg :: args, rest) end
1.91 - else err ("expecting field " ^ field ^ " but got " ^ name)
1.92 - | split_args [] (fargs as (_ :: _)) = ([], fargs)
1.93 - | split_args (_ :: _) [] = err "expecting more fields"
1.94 - | split_args _ _ = ([], []);
1.95 -
1.96 fun mk_ext (fargs as (name, _) :: _) =
1.97 (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
1.98 SOME (ext, _) =>
1.99 (case get_extfields thy ext of
1.100 SOME fields =>
1.101 let
1.102 - val (args, rest) = split_args (map fst (fst (split_last fields))) fargs;
1.103 + val (args, rest) = split_args (map fst (fst (split_last fields))) fargs
1.104 + handle Fail msg => err msg;
1.105 val more' = mk_ext rest;
1.106 in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
1.107 - | NONE => err ("no fields defined for " ^ ext))
1.108 - | NONE => err (name ^ " is no proper field"))
1.109 + | NONE => err ("no fields defined for " ^ quote ext))
1.110 + | NONE => err (quote name ^ " is no proper field"))
1.111 | mk_ext [] = more;
1.112 in mk_ext (fields_tr t) end;
1.113
1.114 @@ -774,7 +766,7 @@
1.115
1.116
1.117 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
1.118 - Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg)
1.119 + Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg)
1.120 | field_update_tr t = raise TERM ("field_update_tr", [t]);
1.121
1.122 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
1.123 @@ -800,8 +792,8 @@
1.124
1.125 (* print translations *)
1.126
1.127 -val print_type_abbr = Unsynchronized.ref true;
1.128 -val print_type_as_fields = Unsynchronized.ref true;
1.129 +val type_abbr = Attrib.setup_config_bool @{binding record_type_abbr} (K true);
1.130 +val type_as_fields = Attrib.setup_config_bool @{binding record_type_as_fields} (K true);
1.131
1.132
1.133 local
1.134 @@ -850,7 +842,7 @@
1.135 foldr1 field_types_tr'
1.136 (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
1.137 in
1.138 - if not (! print_type_as_fields) orelse null fields then raise Match
1.139 + if not (Config.get ctxt type_as_fields) orelse null fields then raise Match
1.140 else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
1.141 else
1.142 Syntax.const @{syntax_const "_record_type_scheme"} $ u $
1.143 @@ -872,7 +864,7 @@
1.144
1.145 fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
1.146 in
1.147 - if ! print_type_abbr then
1.148 + if Config.get ctxt type_abbr then
1.149 (case last_extT T of
1.150 SOME (name, _) =>
1.151 if name = last_ext then
1.152 @@ -1377,7 +1369,7 @@
1.153 @{const_name all} => all_thm
1.154 | @{const_name All} => All_thm RS eq_reflection
1.155 | @{const_name Ex} => Ex_thm RS eq_reflection
1.156 - | _ => error "split_simproc"))
1.157 + | _ => raise Fail "split_simproc"))
1.158 else NONE
1.159 end)
1.160 else NONE
1.161 @@ -1579,6 +1571,8 @@
1.162
1.163 fun extension_definition name fields alphas zeta moreT more vars thy =
1.164 let
1.165 + val ctxt = Proof_Context.init_global thy;
1.166 +
1.167 val base_name = Long_Name.base_name name;
1.168
1.169 val fieldTs = map snd fields;
1.170 @@ -1629,14 +1623,14 @@
1.171 in (term, thy') end
1.172 end;
1.173
1.174 - val _ = timing_msg "record extension preparing definitions";
1.175 + val _ = timing_msg ctxt "record extension preparing definitions";
1.176
1.177
1.178 (* 1st stage part 1: introduce the tree of new types *)
1.179
1.180 fun get_meta_tree () = build_meta_tree_type 1 thy vars more;
1.181 val (ext_body, typ_thy) =
1.182 - timeit_msg "record extension nested type def:" get_meta_tree;
1.183 + timeit_msg ctxt "record extension nested type def:" get_meta_tree;
1.184
1.185
1.186 (* prepare declarations and definitions *)
1.187 @@ -1652,19 +1646,19 @@
1.188 |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
1.189 ||> Theory.checkpoint
1.190 val ([ext_def], defs_thy) =
1.191 - timeit_msg "record extension constructor def:" mk_defs;
1.192 + timeit_msg ctxt "record extension constructor def:" mk_defs;
1.193
1.194
1.195 (* prepare propositions *)
1.196
1.197 - val _ = timing_msg "record extension preparing propositions";
1.198 + val _ = timing_msg ctxt "record extension preparing propositions";
1.199 val vars_more = vars @ [more];
1.200 val variants = map (fn Free (x, _) => x) vars_more;
1.201 val ext = mk_ext vars_more;
1.202 val s = Free (rN, extT);
1.203 val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
1.204
1.205 - val inject_prop =
1.206 + val inject_prop = (* FIXME local x x' *)
1.207 let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
1.208 HOLogic.mk_conj (HOLogic.eq_const extT $
1.209 mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
1.210 @@ -1676,7 +1670,7 @@
1.211 val induct_prop =
1.212 (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
1.213
1.214 - val split_meta_prop =
1.215 + val split_meta_prop = (* FIXME local P *)
1.216 let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
1.217 Logic.mk_equals
1.218 (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
1.219 @@ -1694,7 +1688,7 @@
1.220 Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
1.221 rtac refl 1)));
1.222
1.223 - val inject = timeit_msg "record extension inject proof:" inject_prf;
1.224 + val inject = timeit_msg ctxt "record extension inject proof:" inject_prf;
1.225
1.226 (*We need a surjection property r = (| f = f r, g = g r ... |)
1.227 to prove other theorems. We haven't given names to the accessors
1.228 @@ -1716,7 +1710,7 @@
1.229 in
1.230 surject
1.231 end;
1.232 - val surject = timeit_msg "record extension surjective proof:" surject_prf;
1.233 + val surject = timeit_msg ctxt "record extension surjective proof:" surject_prf;
1.234
1.235 fun split_meta_prf () =
1.236 prove_standard [] split_meta_prop
1.237 @@ -1726,7 +1720,7 @@
1.238 etac meta_allE, atac,
1.239 rtac (prop_subst OF [surject]),
1.240 REPEAT o etac meta_allE, atac]);
1.241 - val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
1.242 + val split_meta = timeit_msg ctxt "record extension split_meta proof:" split_meta_prf;
1.243
1.244 fun induct_prf () =
1.245 let val (assm, concl) = induct_prop in
1.246 @@ -1736,7 +1730,7 @@
1.247 resolve_tac prems 2 THEN
1.248 asm_simp_tac HOL_ss 1)
1.249 end;
1.250 - val induct = timeit_msg "record extension induct proof:" induct_prf;
1.251 + val induct = timeit_msg ctxt "record extension induct proof:" induct_prf;
1.252
1.253 val ([induct', inject', surjective', split_meta'], thm_thy) =
1.254 defs_thy
1.255 @@ -1797,6 +1791,7 @@
1.256
1.257 fun mk_random_eq tyco vs extN Ts =
1.258 let
1.259 + (* FIXME local i etc. *)
1.260 val size = @{term "i::code_numeral"};
1.261 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1.262 val T = Type (tyco, map TFree vs);
1.263 @@ -1816,23 +1811,25 @@
1.264
1.265 fun mk_full_exhaustive_eq tyco vs extN Ts =
1.266 let
1.267 + (* FIXME local i etc. *)
1.268 val size = @{term "i::code_numeral"};
1.269 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1.270 val T = Type (tyco, map TFree vs);
1.271 val test_function = Free ("f", termifyT T --> @{typ "term list option"});
1.272 val params = Name.invent_names Name.context "x" Ts;
1.273 - fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
1.274 - --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
1.275 + fun full_exhaustiveT T =
1.276 + (termifyT T --> @{typ "Code_Evaluation.term list option"}) -->
1.277 + @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"};
1.278 fun mk_full_exhaustive T =
1.279 Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
1.280 - full_exhaustiveT T)
1.281 + full_exhaustiveT T);
1.282 val lhs = mk_full_exhaustive T $ test_function $ size;
1.283 val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
1.284 val rhs = fold_rev (fn (v, T) => fn cont =>
1.285 - mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc
1.286 + mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc;
1.287 in
1.288 (lhs, rhs)
1.289 - end
1.290 + end;
1.291
1.292 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
1.293 let
1.294 @@ -1844,7 +1841,7 @@
1.295 |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
1.296 |> snd
1.297 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
1.298 - end
1.299 + end;
1.300
1.301 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
1.302 let
1.303 @@ -1877,8 +1874,9 @@
1.304 |> Thm.instantiate
1.305 ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
1.306 |> AxClass.unoverload thy;
1.307 - val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq)
1.308 - val ensure_exhaustive_record = ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq)
1.309 + val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
1.310 + val ensure_exhaustive_record =
1.311 + ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
1.312 in
1.313 thy
1.314 |> Code.add_datatype [ext]
1.315 @@ -1902,6 +1900,8 @@
1.316
1.317 fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
1.318 let
1.319 + val ctxt = Proof_Context.init_global thy;
1.320 +
1.321 val prefix = Binding.name_of binding;
1.322 val name = Sign.full_name thy binding;
1.323 val full = Sign.full_name_path thy prefix;
1.324 @@ -1959,7 +1959,7 @@
1.325 |> Sign.qualified_path false binding
1.326 |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
1.327
1.328 - val _ = timing_msg "record preparing definitions";
1.329 + val _ = timing_msg ctxt "record preparing definitions";
1.330 val Type extension_scheme = extT;
1.331 val extension_name = unsuffix ext_typeN (fst extension_scheme);
1.332 val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
1.333 @@ -2063,7 +2063,7 @@
1.334 updaccs RL [updacc_cong_from_eq])
1.335 end;
1.336 val (accessor_thms, updator_thms, upd_acc_cong_assists) =
1.337 - timeit_msg "record getting tree access/updates:" get_access_update_thms;
1.338 + timeit_msg ctxt "record getting tree access/updates:" get_access_update_thms;
1.339
1.340 fun lastN xs = drop parent_fields_len xs;
1.341
1.342 @@ -2129,11 +2129,11 @@
1.343 [make_spec, fields_spec, extend_spec, truncate_spec]
1.344 ||> Theory.checkpoint
1.345 val (((sel_defs, upd_defs), derived_defs), defs_thy) =
1.346 - timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
1.347 + timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
1.348 mk_defs;
1.349
1.350 (* prepare propositions *)
1.351 - val _ = timing_msg "record preparing propositions";
1.352 + val _ = timing_msg ctxt "record preparing propositions";
1.353 val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
1.354 val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
1.355 val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
1.356 @@ -2213,17 +2213,17 @@
1.357
1.358 fun sel_convs_prf () =
1.359 map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
1.360 - val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
1.361 + val sel_convs = timeit_msg ctxt "record sel_convs proof:" sel_convs_prf;
1.362 fun sel_convs_standard_prf () = map Drule.export_without_context sel_convs;
1.363 val sel_convs_standard =
1.364 - timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
1.365 + timeit_msg ctxt "record sel_convs_standard proof:" sel_convs_standard_prf;
1.366
1.367 fun upd_convs_prf () =
1.368 map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
1.369 - val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
1.370 + val upd_convs = timeit_msg ctxt "record upd_convs proof:" upd_convs_prf;
1.371 fun upd_convs_standard_prf () = map Drule.export_without_context upd_convs;
1.372 val upd_convs_standard =
1.373 - timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
1.374 + timeit_msg ctxt "record upd_convs_standard proof:" upd_convs_standard_prf;
1.375
1.376 fun get_upd_acc_congs () =
1.377 let
1.378 @@ -2232,7 +2232,7 @@
1.379 val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
1.380 in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
1.381 val (fold_congs, unfold_congs) =
1.382 - timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
1.383 + timeit_msg ctxt "record upd fold/unfold congs:" get_upd_acc_congs;
1.384
1.385 val parent_induct = Option.map #induct_scheme (try List.last parents);
1.386
1.387 @@ -2243,7 +2243,7 @@
1.388 [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
1.389 try_param_tac rN ext_induct 1,
1.390 asm_simp_tac HOL_basic_ss 1]);
1.391 - val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
1.392 + val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" induct_scheme_prf;
1.393
1.394 fun induct_prf () =
1.395 let val (assm, concl) = induct_prop in
1.396 @@ -2252,7 +2252,7 @@
1.397 THEN try_param_tac "more" @{thm unit.induct} 1
1.398 THEN resolve_tac prems 1)
1.399 end;
1.400 - val induct = timeit_msg "record induct proof:" induct_prf;
1.401 + val induct = timeit_msg ctxt "record induct proof:" induct_prf;
1.402
1.403 fun cases_scheme_prf () =
1.404 let
1.405 @@ -2265,14 +2265,14 @@
1.406 in Object_Logic.rulify (mp OF [ind, refl]) end;
1.407
1.408 val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
1.409 - val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
1.410 + val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" cases_scheme_prf;
1.411
1.412 fun cases_prf () =
1.413 prove_standard [] cases_prop
1.414 (fn _ =>
1.415 try_param_tac rN cases_scheme 1 THEN
1.416 simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]);
1.417 - val cases = timeit_msg "record cases proof:" cases_prf;
1.418 + val cases = timeit_msg ctxt "record cases proof:" cases_prf;
1.419
1.420 fun surjective_prf () =
1.421 let
1.422 @@ -2288,7 +2288,7 @@
1.423 (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
1.424 (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
1.425 end;
1.426 - val surjective = timeit_msg "record surjective proof:" surjective_prf;
1.427 + val surjective = timeit_msg ctxt "record surjective proof:" surjective_prf;
1.428
1.429 fun split_meta_prf () =
1.430 prove false [] split_meta_prop
1.431 @@ -2298,10 +2298,10 @@
1.432 etac meta_allE, atac,
1.433 rtac (prop_subst OF [surjective]),
1.434 REPEAT o etac meta_allE, atac]);
1.435 - val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
1.436 + val split_meta = timeit_msg ctxt "record split_meta proof:" split_meta_prf;
1.437 fun split_meta_standardise () = Drule.export_without_context split_meta;
1.438 val split_meta_standard =
1.439 - timeit_msg "record split_meta standard:" split_meta_standardise;
1.440 + timeit_msg ctxt "record split_meta standard:" split_meta_standardise;
1.441
1.442 fun split_object_prf () =
1.443 let
1.444 @@ -2328,7 +2328,7 @@
1.445
1.446
1.447 val split_object_prf = future_forward_prf split_object_prf split_object_prop;
1.448 - val split_object = timeit_msg "record split_object proof:" split_object_prf;
1.449 + val split_object = timeit_msg ctxt "record split_object proof:" split_object_prf;
1.450
1.451
1.452 fun split_ex_prf () =
1.453 @@ -2341,7 +2341,7 @@
1.454 in
1.455 prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1)
1.456 end;
1.457 - val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
1.458 + val split_ex = timeit_msg ctxt "record split_ex proof:" split_ex_prf;
1.459
1.460 fun equality_tac thms =
1.461 let
1.462 @@ -2359,7 +2359,7 @@
1.463 Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
1.464 (*simp_all_tac ss (sel_convs) would also work but is less efficient*)
1.465 end);
1.466 - val equality = timeit_msg "record equality proof:" equality_prf;
1.467 + val equality = timeit_msg ctxt "record equality proof:" equality_prf;
1.468
1.469 val ((([sel_convs', upd_convs', sel_defs', upd_defs',
1.470 fold_congs', unfold_congs',
1.471 @@ -2411,7 +2411,7 @@
1.472 |> add_extsplit extension_name ext_split
1.473 |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
1.474 |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
1.475 - |> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
1.476 + |> add_fieldext (extension_name, snd extension) names
1.477 |> add_code ext_tyco vs extT ext simps' ext_inject
1.478 |> Sign.restore_naming thy;
1.479
2.1 --- a/src/Pure/General/markup.ML Wed Jul 06 17:19:34 2011 +0100
2.2 +++ b/src/Pure/General/markup.ML Wed Jul 06 23:11:59 2011 +0200
2.3 @@ -378,12 +378,13 @@
2.4
2.5 local
2.6 val default = {output = default_output};
2.7 - val modes = Unsynchronized.ref (Symtab.make [("", default)]);
2.8 + val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
2.9 in
2.10 - fun add_mode name output = CRITICAL (fn () =>
2.11 - Unsynchronized.change modes (Symtab.update_new (name, {output = output})));
2.12 + fun add_mode name output =
2.13 + Synchronized.change modes (Symtab.update_new (name, {output = output}));
2.14 fun get_mode () =
2.15 - the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
2.16 + the_default default
2.17 + (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
2.18 end;
2.19
2.20 fun output m = if is_empty m then no_output else #output (get_mode ()) m;
3.1 --- a/src/Pure/General/output.ML Wed Jul 06 17:19:34 2011 +0100
3.2 +++ b/src/Pure/General/output.ML Wed Jul 06 23:11:59 2011 +0200
3.3 @@ -55,12 +55,13 @@
3.4
3.5 local
3.6 val default = {output = default_output, escape = default_escape};
3.7 - val modes = Unsynchronized.ref (Symtab.make [("", default)]);
3.8 + val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
3.9 in
3.10 - fun add_mode name output escape = CRITICAL (fn () =>
3.11 - Unsynchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})));
3.12 + fun add_mode name output escape =
3.13 + Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
3.14 fun get_mode () =
3.15 - the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
3.16 + the_default default
3.17 + (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
3.18 end;
3.19
3.20 fun output_width x = #output (get_mode ()) x;
4.1 --- a/src/Pure/General/pretty.ML Wed Jul 06 17:19:34 2011 +0100
4.2 +++ b/src/Pure/General/pretty.ML Wed Jul 06 23:11:59 2011 +0200
4.3 @@ -75,12 +75,13 @@
4.4
4.5 local
4.6 val default = {indent = default_indent};
4.7 - val modes = Unsynchronized.ref (Symtab.make [("", default)]);
4.8 + val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
4.9 in
4.10 - fun add_mode name indent = CRITICAL (fn () =>
4.11 - Unsynchronized.change modes (Symtab.update_new (name, {indent = indent})));
4.12 + fun add_mode name indent =
4.13 + Synchronized.change modes (Symtab.update_new (name, {indent = indent}));
4.14 fun get_mode () =
4.15 - the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
4.16 + the_default default
4.17 + (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
4.18 end;
4.19
4.20 fun mode_indent x y = #indent (get_mode ()) x y;
5.1 --- a/src/Pure/Isar/code.ML Wed Jul 06 17:19:34 2011 +0100
5.2 +++ b/src/Pure/Isar/code.ML Wed Jul 06 23:11:59 2011 +0200
5.3 @@ -247,11 +247,12 @@
5.4
5.5 type kind = { empty: Object.T };
5.6
5.7 -val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
5.8 +val kinds = Synchronized.var "Code_Data" (Datatab.empty: kind Datatab.table);
5.9
5.10 -fun invoke f k = case Datatab.lookup (! kinds) k
5.11 - of SOME kind => f kind
5.12 - | NONE => raise Fail "Invalid code data identifier";
5.13 +fun invoke f k =
5.14 + (case Datatab.lookup (Synchronized.value kinds) k of
5.15 + SOME kind => f kind
5.16 + | NONE => raise Fail "Invalid code data identifier");
5.17
5.18 in
5.19
5.20 @@ -259,7 +260,7 @@
5.21 let
5.22 val k = serial ();
5.23 val kind = { empty = empty };
5.24 - val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
5.25 + val _ = Synchronized.change kinds (Datatab.update (k, kind));
5.26 in k end;
5.27
5.28 fun invoke_init k = invoke (fn kind => #empty kind) k;
6.1 --- a/src/Pure/ROOT.ML Wed Jul 06 17:19:34 2011 +0100
6.2 +++ b/src/Pure/ROOT.ML Wed Jul 06 23:11:59 2011 +0200
6.3 @@ -20,6 +20,13 @@
6.4 use "General/print_mode.ML";
6.5 use "General/alist.ML";
6.6 use "General/table.ML";
6.7 +
6.8 +use "Concurrent/simple_thread.ML";
6.9 +
6.10 +use "Concurrent/synchronized.ML";
6.11 +if Multithreading.available then ()
6.12 +else use "Concurrent/synchronized_sequential.ML";
6.13 +
6.14 use "General/output.ML";
6.15 use "General/timing.ML";
6.16 use "General/properties.ML";
6.17 @@ -63,16 +70,10 @@
6.18
6.19 (* concurrency within the ML runtime *)
6.20
6.21 -use "Concurrent/simple_thread.ML";
6.22 -
6.23 use "Concurrent/single_assignment.ML";
6.24 if Multithreading.available then ()
6.25 else use "Concurrent/single_assignment_sequential.ML";
6.26
6.27 -use "Concurrent/synchronized.ML";
6.28 -if Multithreading.available then ()
6.29 -else use "Concurrent/synchronized_sequential.ML";
6.30 -
6.31 if String.isPrefix "smlnj" ml_system then ()
6.32 else use "Concurrent/time_limit.ML";
6.33
7.1 --- a/src/Pure/System/isabelle_process.ML Wed Jul 06 17:19:34 2011 +0100
7.2 +++ b/src/Pure/System/isabelle_process.ML Wed Jul 06 23:11:59 2011 +0200
7.3 @@ -20,7 +20,7 @@
7.4 val is_active: unit -> bool
7.5 val add_command: string -> (string list -> unit) -> unit
7.6 val command: string -> string list -> unit
7.7 - val crashes: exn list Unsynchronized.ref
7.8 + val crashes: exn list Synchronized.var
7.9 val init: string -> string -> unit
7.10 end;
7.11
7.12 @@ -41,18 +41,19 @@
7.13
7.14 local
7.15
7.16 -val global_commands = Unsynchronized.ref (Symtab.empty: (string list -> unit) Symtab.table);
7.17 +val commands =
7.18 + Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table);
7.19
7.20 in
7.21
7.22 -fun add_command name cmd = CRITICAL (fn () =>
7.23 - Unsynchronized.change global_commands (fn cmds =>
7.24 +fun add_command name cmd =
7.25 + Synchronized.change commands (fn cmds =>
7.26 (if not (Symtab.defined cmds name) then ()
7.27 else warning ("Redefining Isabelle process command " ^ quote name);
7.28 - Symtab.update (name, cmd) cmds)));
7.29 + Symtab.update (name, cmd) cmds));
7.30
7.31 fun command name args =
7.32 - (case Symtab.lookup (! global_commands) name of
7.33 + (case Symtab.lookup (Synchronized.value commands) name of
7.34 NONE => error ("Undefined Isabelle process command " ^ quote name)
7.35 | SOME cmd => cmd args);
7.36
7.37 @@ -118,12 +119,12 @@
7.38
7.39 (* protocol loop -- uninterruptible *)
7.40
7.41 -val crashes = Unsynchronized.ref ([]: exn list);
7.42 +val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
7.43
7.44 local
7.45
7.46 fun recover crash =
7.47 - (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
7.48 + (Synchronized.change crashes (cons crash);
7.49 warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
7.50
7.51 fun read_chunk stream len =
8.1 --- a/src/Pure/System/isar.ML Wed Jul 06 17:19:34 2011 +0100
8.2 +++ b/src/Pure/System/isar.ML Wed Jul 06 23:11:59 2011 +0200
8.3 @@ -17,7 +17,7 @@
8.4 val undo: int -> unit
8.5 val kill: unit -> unit
8.6 val kill_proof: unit -> unit
8.7 - val crashes: exn list Unsynchronized.ref
8.8 + val crashes: exn list Synchronized.var
8.9 val toplevel_loop: TextIO.instream ->
8.10 {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
8.11 val loop: unit -> unit
8.12 @@ -113,7 +113,7 @@
8.13
8.14 (* toplevel loop -- uninterruptible *)
8.15
8.16 -val crashes = Unsynchronized.ref ([]: exn list);
8.17 +val crashes = Synchronized.var "Isar.crashes" ([]: exn list);
8.18
8.19 local
8.20
8.21 @@ -128,7 +128,7 @@
8.22 handle exn =>
8.23 (Output.error_msg (ML_Compiler.exn_message exn)
8.24 handle crash =>
8.25 - (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
8.26 + (Synchronized.change crashes (cons crash);
8.27 warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
8.28 raw_loop secure src)
8.29 end;
9.1 --- a/src/Pure/context.ML Wed Jul 06 17:19:34 2011 +0100
9.2 +++ b/src/Pure/context.ML Wed Jul 06 23:11:59 2011 +0200
9.3 @@ -128,10 +128,10 @@
9.4 extend: Object.T -> Object.T,
9.5 merge: pretty -> Object.T * Object.T -> Object.T};
9.6
9.7 -val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
9.8 +val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
9.9
9.10 fun invoke name f k x =
9.11 - (case Datatab.lookup (! kinds) k of
9.12 + (case Datatab.lookup (Synchronized.value kinds) k of
9.13 SOME kind =>
9.14 if ! timing andalso name <> "" then
9.15 Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.str_of (#pos kind))
9.16 @@ -149,7 +149,7 @@
9.17 let
9.18 val k = serial ();
9.19 val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
9.20 - val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
9.21 + val _ = Synchronized.change kinds (Datatab.update (k, kind));
9.22 in k end;
9.23
9.24 val extend_data = Datatab.map invoke_extend;
9.25 @@ -475,15 +475,15 @@
9.26
9.27 local
9.28
9.29 -val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table);
9.30 +val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Object.T) Datatab.table);
9.31
9.32 fun invoke_init k =
9.33 - (case Datatab.lookup (! kinds) k of
9.34 + (case Datatab.lookup (Synchronized.value kinds) k of
9.35 SOME init => init
9.36 | NONE => raise Fail "Invalid proof data identifier");
9.37
9.38 fun init_data thy =
9.39 - Datatab.map (fn k => fn _ => invoke_init k thy) (! kinds);
9.40 + Datatab.map (fn k => fn _ => invoke_init k thy) (Synchronized.value kinds);
9.41
9.42 fun init_new_data data thy =
9.43 Datatab.merge (K true) (data, init_data thy);
9.44 @@ -511,7 +511,7 @@
9.45 fun declare init =
9.46 let
9.47 val k = serial ();
9.48 - val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, init)));
9.49 + val _ = Synchronized.change kinds (Datatab.update (k, init));
9.50 in k end;
9.51
9.52 fun get k dest prf =
10.1 --- a/src/Pure/name.ML Wed Jul 06 17:19:34 2011 +0100
10.2 +++ b/src/Pure/name.ML Wed Jul 06 23:11:59 2011 +0200
10.3 @@ -7,6 +7,7 @@
10.4 signature NAME =
10.5 sig
10.6 val uu: string
10.7 + val uu_: string
10.8 val aT: string
10.9 val bound: int -> string
10.10 val is_bound: string -> bool
10.11 @@ -35,6 +36,7 @@
10.12 (** common defaults **)
10.13
10.14 val uu = "uu";
10.15 +val uu_ = "uu_";
10.16 val aT = "'a";
10.17
10.18
11.1 --- a/src/Pure/term.ML Wed Jul 06 17:19:34 2011 +0100
11.2 +++ b/src/Pure/term.ML Wed Jul 06 23:11:59 2011 +0200
11.3 @@ -762,7 +762,7 @@
11.4
11.5 (*Form an abstraction over a free variable.*)
11.6 fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
11.7 -fun absdummy (T, body) = Abs (Name.internal Name.uu, T, body);
11.8 +fun absdummy (T, body) = Abs (Name.uu_, T, body);
11.9
11.10 (*Abstraction over a list of free variables*)
11.11 fun list_abs_free ([ ] , t) = t