--- a/src/HOL/Tools/record.ML Thu Aug 06 22:30:27 2009 +0200
+++ b/src/HOL/Tools/record.ML Fri Aug 07 19:16:04 2009 +0200
@@ -4,7 +4,6 @@
Extensible records with structural subtyping in HOL.
*)
-
signature BASIC_RECORD =
sig
val record_simproc: simproc
@@ -88,6 +87,8 @@
val RepN = "Rep_";
val AbsN = "Abs_";
+
+
(*** utilities ***)
fun but_last xs = fst (split_last xs);
@@ -102,6 +103,7 @@
fun range_type' T =
range_type T handle Match => T;
+
(* messages *)
fun trace_thm str thm =
@@ -113,12 +115,14 @@
fun trace_term str t =
tracing (str ^ Syntax.string_of_term_global Pure.thy t);
+
(* timing *)
val timing = 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 ();
+
(* syntax *)
fun prune n xs = Library.drop (n, xs);
@@ -136,6 +140,7 @@
val (op ===) = Trueprop o HOLogic.mk_eq;
val (op ==>) = Logic.mk_implies;
+
(* morphisms *)
fun mk_RepN name = suffix ext_typeN (prefix_base RepN name);
@@ -147,6 +152,7 @@
fun mk_Abs name repT absT =
Const (mk_AbsN name,repT --> absT);
+
(* constructor *)
fun mk_extC (name,T) Ts = (suffix extN name, Ts ---> T);
@@ -155,6 +161,7 @@
let val Ts = map fastype_of ts
in list_comb (Const (mk_extC (name,T) Ts),ts) end;
+
(* cases *)
fun mk_casesC (name,T,vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT)
@@ -163,6 +170,7 @@
let val Ts = binder_types (fastype_of f)
in Const (mk_casesC (name,T,vT) Ts) $ f end;
+
(* selector *)
fun mk_selC sT (c,T) = (c,sT --> T);
@@ -171,6 +179,7 @@
let val sT = fastype_of s
in Const (mk_selC sT (c,T)) $ s end;
+
(* updates *)
fun mk_updC sfx sT (c,T) = (suffix sfx c, (T --> T) --> sT --> sT);
@@ -181,6 +190,7 @@
fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s
+
(* types *)
fun dest_recT (typ as Type (c_ext_type, Ts as (T::_))) =
@@ -209,6 +219,8 @@
val rTs' = if i < 0 then rTs else Library.take (i,rTs)
in Library.foldl (fn (s,(c,T)) => s ^ c) ("",rTs') end;
+
+
(*** extend theory by record definition ***)
(** record info **)
@@ -766,20 +778,20 @@
fun match rT T = (Sign.typ_match thy (varifyT rT,T)
Vartab.empty);
- in if !print_record_type_abbr
- then (case last_extT T of
- SOME (name,_)
- => if name = lastExt
- then
- (let
- val subst = match schemeT T
- in
- if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree(zeta,Sign.defaultS thy))))
- then mk_type_abbr subst abbr alphas
- else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
- end handle TYPE_MATCH => default_tr' ctxt tm)
- else raise Match (* give print translation of specialised record a chance *)
- | _ => raise Match)
+ in
+ if !print_record_type_abbr then
+ (case last_extT T of
+ SOME (name, _) =>
+ if name = lastExt then
+ (let
+ val subst = match schemeT T
+ in
+ if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
+ then mk_type_abbr subst abbr alphas
+ else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
+ end handle TYPE_MATCH => default_tr' ctxt tm)
+ else raise Match (* give print translation of specialised record a chance *)
+ | _ => raise Match)
else default_tr' ctxt tm
end
@@ -848,6 +860,8 @@
(list_comb (Syntax.const name_sfx,ts))
in (name_sfx, tr') end;
+
+
(** record simprocs **)
val record_quick_and_dirty_sensitive = ref false;
@@ -1279,8 +1293,6 @@
end)
-
-
local
val inductive_atomize = thms "induct_atomize";
val inductive_rulify = thms "induct_rulify";
@@ -1363,6 +1375,7 @@
else Seq.empty
end handle Subscript => Seq.empty;
+
(* wrapper *)
val record_split_name = "record_split_tac";
@@ -1400,6 +1413,7 @@
fun induct_type_global name = [case_names_fields, Induct.induct_type name];
fun cases_type_global name = [case_names_fields, Induct.cases_type name];
+
(* tactics *)
fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
@@ -1469,7 +1483,9 @@
end;
fun mixit convs refls =
- let fun f ((res,lhs,rhs),refl) = ((refl,List.revAppend (lhs,refl::tl rhs))::res,hd rhs::lhs,tl rhs);
+ let
+ fun f ((res,lhs,rhs),refl) =
+ ((refl,List.revAppend (lhs,refl::tl rhs))::res,hd rhs::lhs,tl rhs);
in #1 (Library.foldl f (([],[],convs),refls)) end;
@@ -2166,8 +2182,10 @@
end);
val equality = timeit_msg "record equality proof:" equality_prf;
- val ((([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],derived_defs'],
- [surjective',equality']),[induct_scheme',induct',cases_scheme',cases']), thms_thy) =
+ val ((([sel_convs', upd_convs', sel_defs', upd_defs',
+ [split_meta', split_object', split_ex'], derived_defs'],
+ [surjective', equality']),
+ [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
defs_thy
|> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
[("select_convs", sel_convs_standard),
@@ -2296,6 +2314,7 @@
val add_record = gen_add_record read_typ read_raw_parent;
val add_record_i = gen_add_record cert_typ (K I);
+
(* setup theory *)
val setup =
@@ -2304,6 +2323,7 @@
Simplifier.map_simpset (fn ss =>
ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]);
+
(* outer syntax *)
local structure P = OuterParse and K = OuterKeyword in
@@ -2320,6 +2340,5 @@
end;
-
-structure BasicRecord: BASIC_RECORD = Record;
-open BasicRecord;
+structure Basic_Record: BASIC_RECORD = Record;
+open Basic_Record;