--- a/src/HOL/Tools/record.ML Wed Jul 06 17:19:34 2011 +0100
+++ b/src/HOL/Tools/record.ML Wed Jul 06 23:11:59 2011 +0200
@@ -9,9 +9,9 @@
signature RECORD =
sig
- val print_type_abbr: bool Unsynchronized.ref
- val print_type_as_fields: bool Unsynchronized.ref
- val timing: bool Unsynchronized.ref
+ val type_abbr: bool Config.T
+ val type_as_fields: bool Config.T
+ val timing: bool Config.T
type info =
{args: (string * sort) list,
@@ -256,9 +256,9 @@
(* timing *)
-val timing = Unsynchronized.ref false;
-fun timeit_msg s x = if ! timing then (warning s; timeit x) else x ();
-fun timing_msg s = if ! timing then warning s else ();
+val timing = Attrib.setup_config_bool @{binding record_timing} (K false);
+fun timeit_msg ctxt s x = if Config.get ctxt timing then (warning s; timeit x) else x ();
+fun timing_msg ctxt s = if Config.get ctxt timing then warning s else ();
(* syntax *)
@@ -670,6 +670,15 @@
local
+fun split_args (field :: fields) ((name, arg) :: fargs) =
+ if can (unsuffix name) field then
+ let val (args, rest) = split_args fields fargs
+ in (arg :: args, rest) end
+ else raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name)
+ | split_args [] (fargs as (_ :: _)) = ([], fargs)
+ | split_args (_ :: _) [] = raise Fail "expecting more fields"
+ | split_args _ _ = ([], []);
+
fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
(name, arg)
| field_type_tr t = raise TERM ("field_type_tr", [t]);
@@ -683,15 +692,6 @@
val thy = Proof_Context.theory_of ctxt;
fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
- fun split_args (field :: fields) ((name, arg) :: fargs) =
- if can (unsuffix name) field then
- let val (args, rest) = split_args fields fargs
- in (arg :: args, rest) end
- else err ("expecting field " ^ field ^ " but got " ^ name)
- | split_args [] (fargs as (_ :: _)) = ([], fargs)
- | split_args (_ :: _) [] = err "expecting more fields"
- | split_args _ _ = ([], []);
-
fun mk_ext (fargs as (name, _) :: _) =
(case get_fieldext thy (Proof_Context.intern_const ctxt name) of
SOME (ext, alphas) =>
@@ -700,7 +700,8 @@
let
val (fields', _) = split_last fields;
val types = map snd fields';
- val (args, rest) = split_args (map fst fields') fargs;
+ val (args, rest) = split_args (map fst fields') fargs
+ handle Fail msg => err msg;
val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
val midx = fold Term.maxidx_typ argtypes 0;
val varifyT = varifyT midx;
@@ -717,8 +718,8 @@
list_comb
(Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
end
- | NONE => err ("no fields defined for " ^ ext))
- | NONE => err (name ^ " is no proper field"))
+ | NONE => err ("no fields defined for " ^ quote ext))
+ | NONE => err (quote name ^ " is no proper field"))
| mk_ext [] = more;
in
mk_ext (field_types_tr t)
@@ -742,27 +743,18 @@
val thy = Proof_Context.theory_of ctxt;
fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
- fun split_args (field :: fields) ((name, arg) :: fargs) =
- if can (unsuffix name) field
- then
- let val (args, rest) = split_args fields fargs
- in (arg :: args, rest) end
- else err ("expecting field " ^ field ^ " but got " ^ name)
- | split_args [] (fargs as (_ :: _)) = ([], fargs)
- | split_args (_ :: _) [] = err "expecting more fields"
- | split_args _ _ = ([], []);
-
fun mk_ext (fargs as (name, _) :: _) =
(case get_fieldext thy (Proof_Context.intern_const ctxt name) of
SOME (ext, _) =>
(case get_extfields thy ext of
SOME fields =>
let
- val (args, rest) = split_args (map fst (fst (split_last fields))) fargs;
+ val (args, rest) = split_args (map fst (fst (split_last fields))) fargs
+ handle Fail msg => err msg;
val more' = mk_ext rest;
in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
- | NONE => err ("no fields defined for " ^ ext))
- | NONE => err (name ^ " is no proper field"))
+ | NONE => err ("no fields defined for " ^ quote ext))
+ | NONE => err (quote name ^ " is no proper field"))
| mk_ext [] = more;
in mk_ext (fields_tr t) end;
@@ -774,7 +766,7 @@
fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
- Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg)
+ Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg)
| field_update_tr t = raise TERM ("field_update_tr", [t]);
fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
@@ -800,8 +792,8 @@
(* print translations *)
-val print_type_abbr = Unsynchronized.ref true;
-val print_type_as_fields = Unsynchronized.ref true;
+val type_abbr = Attrib.setup_config_bool @{binding record_type_abbr} (K true);
+val type_as_fields = Attrib.setup_config_bool @{binding record_type_as_fields} (K true);
local
@@ -850,7 +842,7 @@
foldr1 field_types_tr'
(map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
in
- if not (! print_type_as_fields) orelse null fields then raise Match
+ if not (Config.get ctxt type_as_fields) orelse null fields then raise Match
else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
else
Syntax.const @{syntax_const "_record_type_scheme"} $ u $
@@ -872,7 +864,7 @@
fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
in
- if ! print_type_abbr then
+ if Config.get ctxt type_abbr then
(case last_extT T of
SOME (name, _) =>
if name = last_ext then
@@ -1377,7 +1369,7 @@
@{const_name all} => all_thm
| @{const_name All} => All_thm RS eq_reflection
| @{const_name Ex} => Ex_thm RS eq_reflection
- | _ => error "split_simproc"))
+ | _ => raise Fail "split_simproc"))
else NONE
end)
else NONE
@@ -1579,6 +1571,8 @@
fun extension_definition name fields alphas zeta moreT more vars thy =
let
+ val ctxt = Proof_Context.init_global thy;
+
val base_name = Long_Name.base_name name;
val fieldTs = map snd fields;
@@ -1629,14 +1623,14 @@
in (term, thy') end
end;
- val _ = timing_msg "record extension preparing definitions";
+ val _ = timing_msg ctxt "record extension preparing definitions";
(* 1st stage part 1: introduce the tree of new types *)
fun get_meta_tree () = build_meta_tree_type 1 thy vars more;
val (ext_body, typ_thy) =
- timeit_msg "record extension nested type def:" get_meta_tree;
+ timeit_msg ctxt "record extension nested type def:" get_meta_tree;
(* prepare declarations and definitions *)
@@ -1652,19 +1646,19 @@
|> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
||> Theory.checkpoint
val ([ext_def], defs_thy) =
- timeit_msg "record extension constructor def:" mk_defs;
+ timeit_msg ctxt "record extension constructor def:" mk_defs;
(* prepare propositions *)
- val _ = timing_msg "record extension preparing propositions";
+ val _ = timing_msg ctxt "record extension preparing propositions";
val vars_more = vars @ [more];
val variants = map (fn Free (x, _) => x) vars_more;
val ext = mk_ext vars_more;
val s = Free (rN, extT);
val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
- val inject_prop =
+ val inject_prop = (* FIXME local x x' *)
let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
HOLogic.mk_conj (HOLogic.eq_const extT $
mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
@@ -1676,7 +1670,7 @@
val induct_prop =
(All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
- val split_meta_prop =
+ val split_meta_prop = (* FIXME local P *)
let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
Logic.mk_equals
(All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
@@ -1694,7 +1688,7 @@
Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
rtac refl 1)));
- val inject = timeit_msg "record extension inject proof:" inject_prf;
+ val inject = timeit_msg ctxt "record extension inject proof:" inject_prf;
(*We need a surjection property r = (| f = f r, g = g r ... |)
to prove other theorems. We haven't given names to the accessors
@@ -1716,7 +1710,7 @@
in
surject
end;
- val surject = timeit_msg "record extension surjective proof:" surject_prf;
+ val surject = timeit_msg ctxt "record extension surjective proof:" surject_prf;
fun split_meta_prf () =
prove_standard [] split_meta_prop
@@ -1726,7 +1720,7 @@
etac meta_allE, atac,
rtac (prop_subst OF [surject]),
REPEAT o etac meta_allE, atac]);
- val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
+ val split_meta = timeit_msg ctxt "record extension split_meta proof:" split_meta_prf;
fun induct_prf () =
let val (assm, concl) = induct_prop in
@@ -1736,7 +1730,7 @@
resolve_tac prems 2 THEN
asm_simp_tac HOL_ss 1)
end;
- val induct = timeit_msg "record extension induct proof:" induct_prf;
+ val induct = timeit_msg ctxt "record extension induct proof:" induct_prf;
val ([induct', inject', surjective', split_meta'], thm_thy) =
defs_thy
@@ -1797,6 +1791,7 @@
fun mk_random_eq tyco vs extN Ts =
let
+ (* FIXME local i etc. *)
val size = @{term "i::code_numeral"};
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
val T = Type (tyco, map TFree vs);
@@ -1816,23 +1811,25 @@
fun mk_full_exhaustive_eq tyco vs extN Ts =
let
+ (* FIXME local i etc. *)
val size = @{term "i::code_numeral"};
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
val T = Type (tyco, map TFree vs);
val test_function = Free ("f", termifyT T --> @{typ "term list option"});
val params = Name.invent_names Name.context "x" Ts;
- fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
- --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
+ fun full_exhaustiveT T =
+ (termifyT T --> @{typ "Code_Evaluation.term list option"}) -->
+ @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"};
fun mk_full_exhaustive T =
Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
- full_exhaustiveT T)
+ full_exhaustiveT T);
val lhs = mk_full_exhaustive T $ test_function $ size;
val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
val rhs = fold_rev (fn (v, T) => fn cont =>
- mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc
+ mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc;
in
(lhs, rhs)
- end
+ end;
fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
let
@@ -1844,7 +1841,7 @@
|-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
|> snd
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end
+ end;
fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
let
@@ -1877,8 +1874,9 @@
|> Thm.instantiate
([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
|> AxClass.unoverload thy;
- val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq)
- val ensure_exhaustive_record = ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq)
+ val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
+ val ensure_exhaustive_record =
+ ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
in
thy
|> Code.add_datatype [ext]
@@ -1902,6 +1900,8 @@
fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
let
+ val ctxt = Proof_Context.init_global thy;
+
val prefix = Binding.name_of binding;
val name = Sign.full_name thy binding;
val full = Sign.full_name_path thy prefix;
@@ -1959,7 +1959,7 @@
|> Sign.qualified_path false binding
|> extension_definition extension_name fields alphas_ext zeta moreT more vars;
- val _ = timing_msg "record preparing definitions";
+ val _ = timing_msg ctxt "record preparing definitions";
val Type extension_scheme = extT;
val extension_name = unsuffix ext_typeN (fst extension_scheme);
val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
@@ -2063,7 +2063,7 @@
updaccs RL [updacc_cong_from_eq])
end;
val (accessor_thms, updator_thms, upd_acc_cong_assists) =
- timeit_msg "record getting tree access/updates:" get_access_update_thms;
+ timeit_msg ctxt "record getting tree access/updates:" get_access_update_thms;
fun lastN xs = drop parent_fields_len xs;
@@ -2129,11 +2129,11 @@
[make_spec, fields_spec, extend_spec, truncate_spec]
||> Theory.checkpoint
val (((sel_defs, upd_defs), derived_defs), defs_thy) =
- timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
+ timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
mk_defs;
(* prepare propositions *)
- val _ = timing_msg "record preparing propositions";
+ val _ = timing_msg ctxt "record preparing propositions";
val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
@@ -2213,17 +2213,17 @@
fun sel_convs_prf () =
map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
- val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
+ val sel_convs = timeit_msg ctxt "record sel_convs proof:" sel_convs_prf;
fun sel_convs_standard_prf () = map Drule.export_without_context sel_convs;
val sel_convs_standard =
- timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
+ timeit_msg ctxt "record sel_convs_standard proof:" sel_convs_standard_prf;
fun upd_convs_prf () =
map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
- val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
+ val upd_convs = timeit_msg ctxt "record upd_convs proof:" upd_convs_prf;
fun upd_convs_standard_prf () = map Drule.export_without_context upd_convs;
val upd_convs_standard =
- timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
+ timeit_msg ctxt "record upd_convs_standard proof:" upd_convs_standard_prf;
fun get_upd_acc_congs () =
let
@@ -2232,7 +2232,7 @@
val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
val (fold_congs, unfold_congs) =
- timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
+ timeit_msg ctxt "record upd fold/unfold congs:" get_upd_acc_congs;
val parent_induct = Option.map #induct_scheme (try List.last parents);
@@ -2243,7 +2243,7 @@
[case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
try_param_tac rN ext_induct 1,
asm_simp_tac HOL_basic_ss 1]);
- val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
+ val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" induct_scheme_prf;
fun induct_prf () =
let val (assm, concl) = induct_prop in
@@ -2252,7 +2252,7 @@
THEN try_param_tac "more" @{thm unit.induct} 1
THEN resolve_tac prems 1)
end;
- val induct = timeit_msg "record induct proof:" induct_prf;
+ val induct = timeit_msg ctxt "record induct proof:" induct_prf;
fun cases_scheme_prf () =
let
@@ -2265,14 +2265,14 @@
in Object_Logic.rulify (mp OF [ind, refl]) end;
val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
- val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
+ val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" cases_scheme_prf;
fun cases_prf () =
prove_standard [] cases_prop
(fn _ =>
try_param_tac rN cases_scheme 1 THEN
simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]);
- val cases = timeit_msg "record cases proof:" cases_prf;
+ val cases = timeit_msg ctxt "record cases proof:" cases_prf;
fun surjective_prf () =
let
@@ -2288,7 +2288,7 @@
(Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
(rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
end;
- val surjective = timeit_msg "record surjective proof:" surjective_prf;
+ val surjective = timeit_msg ctxt "record surjective proof:" surjective_prf;
fun split_meta_prf () =
prove false [] split_meta_prop
@@ -2298,10 +2298,10 @@
etac meta_allE, atac,
rtac (prop_subst OF [surjective]),
REPEAT o etac meta_allE, atac]);
- val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
+ val split_meta = timeit_msg ctxt "record split_meta proof:" split_meta_prf;
fun split_meta_standardise () = Drule.export_without_context split_meta;
val split_meta_standard =
- timeit_msg "record split_meta standard:" split_meta_standardise;
+ timeit_msg ctxt "record split_meta standard:" split_meta_standardise;
fun split_object_prf () =
let
@@ -2328,7 +2328,7 @@
val split_object_prf = future_forward_prf split_object_prf split_object_prop;
- val split_object = timeit_msg "record split_object proof:" split_object_prf;
+ val split_object = timeit_msg ctxt "record split_object proof:" split_object_prf;
fun split_ex_prf () =
@@ -2341,7 +2341,7 @@
in
prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1)
end;
- val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
+ val split_ex = timeit_msg ctxt "record split_ex proof:" split_ex_prf;
fun equality_tac thms =
let
@@ -2359,7 +2359,7 @@
Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
(*simp_all_tac ss (sel_convs) would also work but is less efficient*)
end);
- val equality = timeit_msg "record equality proof:" equality_prf;
+ val equality = timeit_msg ctxt "record equality proof:" equality_prf;
val ((([sel_convs', upd_convs', sel_defs', upd_defs',
fold_congs', unfold_congs',
@@ -2411,7 +2411,7 @@
|> add_extsplit extension_name ext_split
|> 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_fieldext (extension_name, snd extension) names
|> add_code ext_tyco vs extT ext simps' ext_inject
|> Sign.restore_naming thy;