# HG changeset patch # User schirmer # Date 1083869010 -7200 # Node ID d01983034dedff0d4ee2f35adf75cee42c5cfb56 # Parent c0a65132d79a79edc6f4e3fea8888882512a295d tuned HOL/record package; enabled record_upd_simproc by default. diff -r c0a65132d79a -r d01983034ded NEWS --- a/NEWS Thu May 06 14:20:13 2004 +0200 +++ b/NEWS Thu May 06 20:43:30 2004 +0200 @@ -34,15 +34,22 @@ *** HOL *** -* HOL/record: reimplementation of records to avoid performance -problems for type inference. Records are no longer composed of nested -field types, but of nested extension types. Therefore the record type -only grows linear in the number of extensions and not in the number of -fields. The top-level (users) view on records is preserved. + +* HOL/record: reimplementation of records. Improved scalability for records with +many fields, avoiding performance problems for type inference. Records are no +longer composed of nested field types, +but of nested extension types. Therefore the record type only grows +linear in the number of extensions and not in the number of fields. +The top-level (users) view on records is preserved. Potential INCOMPATIBILITY only in strange cases, where the theory -depends on the old record representation. The type generated for a -record is called _ext_type. - +depends on the old record representation. The type generated for +a record is called _ext_type. + + +* Simplifier: "record_upd_simproc" for simplification of multiple record +updates enabled by default. +INCOMPATIBILITY: old proofs break occasionally, since simplification +is more powerful by default. *** HOLCF *** diff -r c0a65132d79a -r d01983034ded src/HOL/Bali/DeclConcepts.thy --- a/src/HOL/Bali/DeclConcepts.thy Thu May 06 14:20:13 2004 +0200 +++ b/src/HOL/Bali/DeclConcepts.thy Thu May 06 20:43:30 2004 +0200 @@ -163,7 +163,7 @@ defs (overloaded) static_field_type_is_static_def: - "is_static (m::('b::type) member_ext_type) \ static_val m" + "is_static (m::('b::type) member_ext_type) \ static_sel m" lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m" apply (cases m) @@ -412,14 +412,14 @@ defs (overloaded) member_ext_type_resTy_def: "resTy (m::('b::has_resTy) member_ext_type) - \ resTy (member.more_val m)" + \ resTy (member.more_sel m)" instance mhead_ext_type :: ("type") has_resTy .. defs (overloaded) mhead_ext_type_resTy_def: "resTy (m::('b mhead_ext_type)) - \ resT_val m" + \ resT_sel m" lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m" apply (cases m) diff -r c0a65132d79a -r d01983034ded src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Thu May 06 14:20:13 2004 +0200 +++ b/src/HOL/Tools/record_package.ML Thu May 06 20:43:30 2004 +0200 @@ -39,7 +39,7 @@ end; -structure RecordPackage :RECORD_PACKAGE = +structure RecordPackage :RECORD_PACKAGE = struct val rec_UNIV_I = thm "rec_UNIV_I"; @@ -60,7 +60,7 @@ val schemeN = "_scheme"; val ext_typeN = "_ext_type"; val extN ="_ext"; -val ext_dest = "_val"; +val ext_dest = "_sel"; val updateN = "_update"; val schemeN = "_scheme"; val makeN = "make"; @@ -74,19 +74,7 @@ (*** utilities ***) - -fun last [] = error "RecordPackage.last: empty list" - | last [x] = x - | last (x::xs) = last xs; - -fun but_last [] = error "RecordPackage.but_last: empty list" - | but_last [x] = [] - | but_last (x::xs) = x::but_last xs; - -fun remdups [] = [] - | remdups (x::xs) = x::remdups (filter_out (fn y => y=x) xs); - -fun is_suffix sfx s = is_some (try (unsuffix sfx) s); +fun but_last xs = fst (split_last xs); (* messages *) @@ -151,7 +139,7 @@ fun dest_recT (typ as Type (c_ext_type, Ts as (T::_))) = (case try (unsuffix ext_typeN) c_ext_type of None => raise TYPE ("RecordPackage.dest_recT", [typ], []) - | Some c => ((c, Ts), last Ts)) + | Some c => ((c, Ts), last_elem Ts)) | dest_recT typ = raise TYPE ("RecordPackage.dest_recT", [typ], []); fun is_recT T = @@ -221,7 +209,7 @@ structure RecordsArgs = struct - val name = "HOL/records"; + val name = "HOL/structures"; (* FIXME *) type T = record_data; val empty = @@ -439,15 +427,15 @@ fun gen_ext_fields_tr sep mark sfx more sg t = let + val msg = "error in record input: "; val fieldargs = dest_ext_fields sep mark t; fun splitargs (field::fields) ((name,arg)::fargs) = - if is_suffix name field + if can (unsuffix name) field then let val (args,rest) = splitargs fields fargs in (arg::args,rest) end - else raise TERM ("gen_ext_fields_tr: expecting field " ^ field ^ - " but got " ^ name, [t]) + else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t]) | splitargs [] (fargs as (_::_)) = ([],fargs) - | splitargs (_::_) [] = raise TERM ("gen_ext_fields_tr: expecting more fields", [t]) + | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t]) | splitargs _ _ = ([],[]); fun mk_ext (fargs as (name,arg)::_) = @@ -459,24 +447,24 @@ val more' = mk_ext rest; in list_comb (Syntax.const (suffix sfx ext),args@[more']) end - | None => raise TERM("gen_ext_fields_tr: no fields defined for " + | None => raise TERM(msg ^ "no fields defined for " ^ ext,[t])) - | None => raise TERM ("gen_ext_fields_tr: "^ name ^" is no proper field",[t])) + | None => raise TERM (msg ^ name ^" is no proper field",[t])) | mk_ext [] = more in mk_ext fieldargs end; fun gen_ext_type_tr sep mark sfx more sg t = let + val msg = "error in record-type input: "; val fieldargs = dest_ext_fields sep mark t; fun splitargs (field::fields) ((name,arg)::fargs) = - if is_suffix name field + if can (unsuffix name) field then let val (args,rest) = splitargs fields fargs in (arg::args,rest) end - else raise TERM ("gen_ext_type_tr: expecting field " ^ field ^ - " but got " ^ name, [t]) + else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t]) | splitargs [] (fargs as (_::_)) = ([],fargs) - | splitargs (_::_) [] = raise TERM ("gen_ext_type_tr: expecting more fields", [t]) + | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t]) | splitargs _ _ = ([],[]); fun get_sort xs n = (case assoc (xs,n) of @@ -507,9 +495,9 @@ val more' = mk_ext rest; in list_comb (Syntax.const (suffix sfx ext),alphas'@[more']) end handle TUNIFY => raise - TERM ("gen_ext_type_tr: type is no proper record (extension)", [t])) - | None => raise TERM ("gen_ext_fields_tr: no fields defined for " ^ ext,[t])) - | None => raise TERM ("gen_ext_fields_tr: "^ name ^" is no proper field",[t])) + TERM (msg ^ "type is no proper record (extension)", [t])) + | None => raise TERM (msg ^ "no fields defined for " ^ ext,[t])) + | None => raise TERM (msg ^ name ^" is no proper field",[t])) | mk_ext [] = more in mk_ext fieldargs end; @@ -1125,8 +1113,8 @@ (* code generator data *) (* Representation as nested pairs is revealed for codegeneration *) - val [rep_code,abs_code] = map (Codegen.parse_mixfix (K (Bound 0))) ["I","I"]; - val ext_type_code = Codegen.parse_mixfix (K dummyT) "_"; + val [rep_code,abs_code] = map (Codegen.parse_mixfix (K (Bound 0))) ["(_)","(_)"]; + val ext_type_code = Codegen.parse_mixfix (K dummyT) "(_)"; (* 1st stage: defs_thy *) val (defs_thy, ([abs_inject, abs_inverse, abs_induct],ext_def::dest_defs)) = @@ -1695,9 +1683,9 @@ val setup = [RecordsData.init, Theory.add_trfuns ([], parse_translation, [], []), - Theory.add_advanced_trfuns ([], adv_parse_translation, [], []), + Theory.add_advanced_trfuns ([], adv_parse_translation, [], []), Simplifier.change_simpset_of Simplifier.addsimprocs - [record_simproc, record_eq_simproc]]; + [record_simproc, record_upd_simproc, record_eq_simproc]]; (* outer syntax *) @@ -1708,7 +1696,7 @@ (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const); val recordP = - OuterSyntax.command "record" "define extensible record" K.thy_decl + OuterSyntax.command "record" "define extensible record" K.thy_decl (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z))); val _ = OuterSyntax.add_parsers [recordP];