# HG changeset patch # User wenzelm # Date 1249665364 -7200 # Node ID 41fe1c93f218ba71b250b93fe6eb8c5dfcb6afce # Parent f001e0f2ceb67f471926c9f2658c86f70a5d8cfa tuned spacing of sections; reduced line length; diff -r f001e0f2ceb6 -r 41fe1c93f218 src/HOL/Tools/record.ML --- 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;