src/HOL/Tools/record.ML
changeset 32335 41fe1c93f218
parent 32283 3bebc195c124
child 32740 9dd0a2f83429
child 32743 c4e9a48bc50e
--- 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;