tuned spacing of sections;
authorwenzelm
Fri Aug 07 19:16:04 2009 +0200 (2009-08-07)
changeset 3233541fe1c93f218
parent 32334 f001e0f2ceb6
child 32336 e88b295aae35
tuned spacing of sections;
reduced line length;
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Thu Aug 06 22:30:27 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Fri Aug 07 19:16:04 2009 +0200
     1.3 @@ -4,7 +4,6 @@
     1.4  Extensible records with structural subtyping in HOL.
     1.5  *)
     1.6  
     1.7 -
     1.8  signature BASIC_RECORD =
     1.9  sig
    1.10    val record_simproc: simproc
    1.11 @@ -88,6 +87,8 @@
    1.12  val RepN = "Rep_";
    1.13  val AbsN = "Abs_";
    1.14  
    1.15 +
    1.16 +
    1.17  (*** utilities ***)
    1.18  
    1.19  fun but_last xs = fst (split_last xs);
    1.20 @@ -102,6 +103,7 @@
    1.21  fun range_type' T =
    1.22      range_type T handle Match => T;
    1.23  
    1.24 +
    1.25  (* messages *)
    1.26  
    1.27  fun trace_thm str thm =
    1.28 @@ -113,12 +115,14 @@
    1.29  fun trace_term str t =
    1.30      tracing (str ^ Syntax.string_of_term_global Pure.thy t);
    1.31  
    1.32 +
    1.33  (* timing *)
    1.34  
    1.35  val timing = ref false;
    1.36  fun timeit_msg s x = if !timing then (warning s; timeit x) else x ();
    1.37  fun timing_msg s = if !timing then warning s else ();
    1.38  
    1.39 +
    1.40  (* syntax *)
    1.41  
    1.42  fun prune n xs = Library.drop (n, xs);
    1.43 @@ -136,6 +140,7 @@
    1.44  val (op ===) = Trueprop o HOLogic.mk_eq;
    1.45  val (op ==>) = Logic.mk_implies;
    1.46  
    1.47 +
    1.48  (* morphisms *)
    1.49  
    1.50  fun mk_RepN name = suffix ext_typeN (prefix_base RepN name);
    1.51 @@ -147,6 +152,7 @@
    1.52  fun mk_Abs name repT absT =
    1.53    Const (mk_AbsN name,repT --> absT);
    1.54  
    1.55 +
    1.56  (* constructor *)
    1.57  
    1.58  fun mk_extC (name,T) Ts  = (suffix extN name, Ts ---> T);
    1.59 @@ -155,6 +161,7 @@
    1.60    let val Ts = map fastype_of ts
    1.61    in list_comb (Const (mk_extC (name,T) Ts),ts) end;
    1.62  
    1.63 +
    1.64  (* cases *)
    1.65  
    1.66  fun mk_casesC (name,T,vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT)
    1.67 @@ -163,6 +170,7 @@
    1.68    let val Ts = binder_types (fastype_of f)
    1.69    in Const (mk_casesC (name,T,vT) Ts) $ f end;
    1.70  
    1.71 +
    1.72  (* selector *)
    1.73  
    1.74  fun mk_selC sT (c,T) = (c,sT --> T);
    1.75 @@ -171,6 +179,7 @@
    1.76    let val sT = fastype_of s
    1.77    in Const (mk_selC sT (c,T)) $ s end;
    1.78  
    1.79 +
    1.80  (* updates *)
    1.81  
    1.82  fun mk_updC sfx sT (c,T) = (suffix sfx c, (T --> T) --> sT --> sT);
    1.83 @@ -181,6 +190,7 @@
    1.84  
    1.85  fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s
    1.86  
    1.87 +
    1.88  (* types *)
    1.89  
    1.90  fun dest_recT (typ as Type (c_ext_type, Ts as (T::_))) =
    1.91 @@ -209,6 +219,8 @@
    1.92        val rTs' = if i < 0 then rTs else Library.take (i,rTs)
    1.93    in Library.foldl (fn (s,(c,T)) => s ^ c) ("",rTs') end;
    1.94  
    1.95 +
    1.96 +
    1.97  (*** extend theory by record definition ***)
    1.98  
    1.99  (** record info **)
   1.100 @@ -766,20 +778,20 @@
   1.101        fun match rT T = (Sign.typ_match thy (varifyT rT,T)
   1.102                                                  Vartab.empty);
   1.103  
   1.104 -   in if !print_record_type_abbr
   1.105 -      then (case last_extT T of
   1.106 -             SOME (name,_)
   1.107 -              => if name = lastExt
   1.108 -                 then
   1.109 -                  (let
   1.110 -                     val subst = match schemeT T
   1.111 -                   in
   1.112 -                    if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree(zeta,Sign.defaultS thy))))
   1.113 -                    then mk_type_abbr subst abbr alphas
   1.114 -                    else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
   1.115 -                   end handle TYPE_MATCH => default_tr' ctxt tm)
   1.116 -                 else raise Match (* give print translation of specialised record a chance *)
   1.117 -            | _ => raise Match)
   1.118 +   in
   1.119 +     if !print_record_type_abbr then
   1.120 +       (case last_extT T of
   1.121 +         SOME (name, _) =>
   1.122 +          if name = lastExt then
   1.123 +            (let
   1.124 +               val subst = match schemeT T
   1.125 +             in
   1.126 +              if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
   1.127 +              then mk_type_abbr subst abbr alphas
   1.128 +              else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
   1.129 +             end handle TYPE_MATCH => default_tr' ctxt tm)
   1.130 +           else raise Match (* give print translation of specialised record a chance *)
   1.131 +        | _ => raise Match)
   1.132         else default_tr' ctxt tm
   1.133    end
   1.134  
   1.135 @@ -848,6 +860,8 @@
   1.136                                 (list_comb (Syntax.const name_sfx,ts))
   1.137    in (name_sfx, tr') end;
   1.138  
   1.139 +
   1.140 +
   1.141  (** record simprocs **)
   1.142  
   1.143  val record_quick_and_dirty_sensitive = ref false;
   1.144 @@ -1279,8 +1293,6 @@
   1.145           end)
   1.146  
   1.147  
   1.148 -
   1.149 -
   1.150  local
   1.151  val inductive_atomize = thms "induct_atomize";
   1.152  val inductive_rulify = thms "induct_rulify";
   1.153 @@ -1363,6 +1375,7 @@
   1.154       else Seq.empty
   1.155    end handle Subscript => Seq.empty;
   1.156  
   1.157 +
   1.158  (* wrapper *)
   1.159  
   1.160  val record_split_name = "record_split_tac";
   1.161 @@ -1400,6 +1413,7 @@
   1.162  fun induct_type_global name = [case_names_fields, Induct.induct_type name];
   1.163  fun cases_type_global name = [case_names_fields, Induct.cases_type name];
   1.164  
   1.165 +
   1.166  (* tactics *)
   1.167  
   1.168  fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
   1.169 @@ -1469,7 +1483,9 @@
   1.170    end;
   1.171  
   1.172  fun mixit convs refls =
   1.173 -  let fun f ((res,lhs,rhs),refl) = ((refl,List.revAppend (lhs,refl::tl rhs))::res,hd rhs::lhs,tl rhs);
   1.174 +  let
   1.175 +    fun f ((res,lhs,rhs),refl) =
   1.176 +      ((refl,List.revAppend (lhs,refl::tl rhs))::res,hd rhs::lhs,tl rhs);
   1.177    in #1 (Library.foldl f (([],[],convs),refls)) end;
   1.178  
   1.179  
   1.180 @@ -2166,8 +2182,10 @@
   1.181        end);
   1.182       val equality = timeit_msg "record equality proof:" equality_prf;
   1.183  
   1.184 -    val ((([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],derived_defs'],
   1.185 -            [surjective',equality']),[induct_scheme',induct',cases_scheme',cases']), thms_thy) =
   1.186 +    val ((([sel_convs', upd_convs', sel_defs', upd_defs',
   1.187 +          [split_meta', split_object', split_ex'], derived_defs'],
   1.188 +          [surjective', equality']),
   1.189 +          [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
   1.190        defs_thy
   1.191        |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
   1.192           [("select_convs", sel_convs_standard),
   1.193 @@ -2296,6 +2314,7 @@
   1.194  val add_record = gen_add_record read_typ read_raw_parent;
   1.195  val add_record_i = gen_add_record cert_typ (K I);
   1.196  
   1.197 +
   1.198  (* setup theory *)
   1.199  
   1.200  val setup =
   1.201 @@ -2304,6 +2323,7 @@
   1.202    Simplifier.map_simpset (fn ss =>
   1.203      ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]);
   1.204  
   1.205 +
   1.206  (* outer syntax *)
   1.207  
   1.208  local structure P = OuterParse and K = OuterKeyword in
   1.209 @@ -2320,6 +2340,5 @@
   1.210  
   1.211  end;
   1.212  
   1.213 -
   1.214 -structure BasicRecord: BASIC_RECORD = Record;
   1.215 -open BasicRecord;
   1.216 +structure Basic_Record: BASIC_RECORD = Record;
   1.217 +open Basic_Record;