tuned HOL/record package; enabled record_upd_simproc by default.
authorschirmer
Thu May 06 20:43:30 2004 +0200 (2004-05-06)
changeset 14709d01983034ded
parent 14708 c0a65132d79a
child 14710 247615bfffb8
tuned HOL/record package; enabled record_upd_simproc by default.
NEWS
src/HOL/Bali/DeclConcepts.thy
src/HOL/Tools/record_package.ML
     1.1 --- a/NEWS	Thu May 06 14:20:13 2004 +0200
     1.2 +++ b/NEWS	Thu May 06 20:43:30 2004 +0200
     1.3 @@ -34,15 +34,22 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* HOL/record: reimplementation of records to avoid performance
     1.8 -problems for type inference. Records are no longer composed of nested
     1.9 -field types, but of nested extension types. Therefore the record type
    1.10 -only grows linear in the number of extensions and not in the number of
    1.11 -fields.  The top-level (users) view on records is preserved.
    1.12 +
    1.13 +* HOL/record: reimplementation of records. Improved scalability for records with
    1.14 +many fields, avoiding performance problems for type inference. Records are no 
    1.15 +longer composed of nested field types,
    1.16 +but of nested extension types. Therefore the record type only grows
    1.17 +linear in the number of extensions and not in the number of fields.
    1.18 +The top-level (users) view on records is preserved. 
    1.19  Potential INCOMPATIBILITY only in strange cases, where the theory
    1.20 -depends on the old record representation. The type generated for a
    1.21 -record is called <record_name>_ext_type.
    1.22 -
    1.23 +depends on the old record representation. The type generated for
    1.24 +a record is called <record_name>_ext_type.    
    1.25 +
    1.26 +
    1.27 +* Simplifier: "record_upd_simproc" for simplification of multiple record 
    1.28 +updates enabled by default. 
    1.29 +INCOMPATIBILITY: old proofs break occasionally, since simplification
    1.30 +is more powerful by default.
    1.31  
    1.32  *** HOLCF ***
    1.33  
     2.1 --- a/src/HOL/Bali/DeclConcepts.thy	Thu May 06 14:20:13 2004 +0200
     2.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Thu May 06 20:43:30 2004 +0200
     2.3 @@ -163,7 +163,7 @@
     2.4  
     2.5  defs (overloaded)
     2.6  static_field_type_is_static_def: 
     2.7 - "is_static (m::('b::type) member_ext_type) \<equiv> static_val m"
     2.8 + "is_static (m::('b::type) member_ext_type) \<equiv> static_sel m"
     2.9  
    2.10  lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
    2.11  apply (cases m)
    2.12 @@ -412,14 +412,14 @@
    2.13  defs (overloaded)
    2.14  member_ext_type_resTy_def: 
    2.15   "resTy (m::('b::has_resTy) member_ext_type) 
    2.16 -  \<equiv> resTy (member.more_val m)" 
    2.17 +  \<equiv> resTy (member.more_sel m)" 
    2.18  
    2.19  instance mhead_ext_type :: ("type") has_resTy ..
    2.20  
    2.21  defs (overloaded)
    2.22  mhead_ext_type_resTy_def: 
    2.23   "resTy (m::('b mhead_ext_type)) 
    2.24 -  \<equiv> resT_val m" 
    2.25 +  \<equiv> resT_sel m" 
    2.26  
    2.27  lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
    2.28  apply (cases m)
     3.1 --- a/src/HOL/Tools/record_package.ML	Thu May 06 14:20:13 2004 +0200
     3.2 +++ b/src/HOL/Tools/record_package.ML	Thu May 06 20:43:30 2004 +0200
     3.3 @@ -39,7 +39,7 @@
     3.4  end;
     3.5  
     3.6  
     3.7 -structure RecordPackage :RECORD_PACKAGE =    
     3.8 +structure RecordPackage :RECORD_PACKAGE =     
     3.9  struct
    3.10  
    3.11  val rec_UNIV_I = thm "rec_UNIV_I";
    3.12 @@ -60,7 +60,7 @@
    3.13  val schemeN = "_scheme";
    3.14  val ext_typeN = "_ext_type"; 
    3.15  val extN ="_ext";
    3.16 -val ext_dest = "_val";
    3.17 +val ext_dest = "_sel";
    3.18  val updateN = "_update";
    3.19  val schemeN = "_scheme";
    3.20  val makeN = "make";
    3.21 @@ -74,19 +74,7 @@
    3.22  
    3.23  (*** utilities ***)
    3.24  
    3.25 -
    3.26 -fun last [] = error "RecordPackage.last: empty list"
    3.27 -  | last [x] = x
    3.28 -  | last (x::xs) = last xs;
    3.29 -
    3.30 -fun but_last [] = error "RecordPackage.but_last: empty list"
    3.31 -  | but_last [x] = []
    3.32 -  | but_last (x::xs) = x::but_last xs;
    3.33 -
    3.34 -fun remdups [] = []
    3.35 -  | remdups (x::xs) = x::remdups (filter_out (fn y => y=x) xs);
    3.36 -
    3.37 -fun is_suffix sfx s = is_some (try (unsuffix sfx) s);
    3.38 +fun but_last xs = fst (split_last xs);
    3.39  
    3.40  (* messages *)
    3.41  
    3.42 @@ -151,7 +139,7 @@
    3.43  fun dest_recT (typ as Type (c_ext_type, Ts as (T::_))) =
    3.44        (case try (unsuffix ext_typeN) c_ext_type of
    3.45          None => raise TYPE ("RecordPackage.dest_recT", [typ], [])
    3.46 -      | Some c => ((c, Ts), last Ts))
    3.47 +      | Some c => ((c, Ts), last_elem Ts))
    3.48    | dest_recT typ = raise TYPE ("RecordPackage.dest_recT", [typ], []);
    3.49  
    3.50  fun is_recT T =
    3.51 @@ -221,7 +209,7 @@
    3.52  
    3.53  structure RecordsArgs =
    3.54  struct
    3.55 -  val name = "HOL/records";    
    3.56 +  val name = "HOL/structures"; (* FIXME *)    
    3.57    type T = record_data;
    3.58  
    3.59    val empty =
    3.60 @@ -439,15 +427,15 @@
    3.61  
    3.62  fun gen_ext_fields_tr sep mark sfx more sg t =
    3.63    let 
    3.64 +    val msg = "error in record input: ";
    3.65      val fieldargs = dest_ext_fields sep mark t; 
    3.66      fun splitargs (field::fields) ((name,arg)::fargs) =
    3.67 -          if is_suffix name field
    3.68 +          if can (unsuffix name) field
    3.69            then let val (args,rest) = splitargs fields fargs
    3.70                 in (arg::args,rest) end
    3.71 -          else raise TERM ("gen_ext_fields_tr: expecting field " ^ field ^ 
    3.72 -                           " but got " ^ name, [t])
    3.73 +          else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t])
    3.74        | splitargs [] (fargs as (_::_)) = ([],fargs)
    3.75 -      | splitargs (_::_) [] = raise TERM ("gen_ext_fields_tr: expecting more fields", [t])
    3.76 +      | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t])
    3.77        | splitargs _ _ = ([],[]);
    3.78  
    3.79      fun mk_ext (fargs as (name,arg)::_) =
    3.80 @@ -459,24 +447,24 @@
    3.81                                          val more' = mk_ext rest;  
    3.82                                      in list_comb (Syntax.const (suffix sfx ext),args@[more'])
    3.83                                      end
    3.84 -                             | None => raise TERM("gen_ext_fields_tr: no fields defined for "
    3.85 +                             | None => raise TERM(msg ^ "no fields defined for "
    3.86                                                     ^ ext,[t]))
    3.87 -          | None => raise TERM ("gen_ext_fields_tr: "^ name ^" is no proper field",[t]))
    3.88 +          | None => raise TERM (msg ^ name ^" is no proper field",[t]))
    3.89        | mk_ext [] = more
    3.90  
    3.91    in mk_ext fieldargs end;   
    3.92  
    3.93  fun gen_ext_type_tr sep mark sfx more sg t =
    3.94    let 
    3.95 +    val msg = "error in record-type input: ";
    3.96      val fieldargs = dest_ext_fields sep mark t; 
    3.97      fun splitargs (field::fields) ((name,arg)::fargs) =
    3.98 -          if is_suffix name field
    3.99 +          if can (unsuffix name) field
   3.100            then let val (args,rest) = splitargs fields fargs
   3.101                 in (arg::args,rest) end
   3.102 -          else raise TERM ("gen_ext_type_tr: expecting field " ^ field ^ 
   3.103 -                           " but got " ^ name, [t])
   3.104 +          else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t])
   3.105        | splitargs [] (fargs as (_::_)) = ([],fargs)
   3.106 -      | splitargs (_::_) [] = raise TERM ("gen_ext_type_tr: expecting more fields", [t])
   3.107 +      | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t])
   3.108        | splitargs _ _ = ([],[]);
   3.109  
   3.110      fun get_sort xs n = (case assoc (xs,n) of 
   3.111 @@ -507,9 +495,9 @@
   3.112                         val more' = mk_ext rest;   
   3.113                       in list_comb (Syntax.const (suffix sfx ext),alphas'@[more']) 
   3.114                       end handle TUNIFY => raise 
   3.115 -                           TERM ("gen_ext_type_tr: type is no proper record (extension)", [t]))
   3.116 -               | None => raise TERM ("gen_ext_fields_tr: no fields defined for " ^ ext,[t]))
   3.117 -          | None => raise TERM ("gen_ext_fields_tr: "^ name ^" is no proper field",[t]))
   3.118 +                           TERM (msg ^ "type is no proper record (extension)", [t]))
   3.119 +               | None => raise TERM (msg ^ "no fields defined for " ^ ext,[t]))
   3.120 +          | None => raise TERM (msg ^ name ^" is no proper field",[t]))
   3.121        | mk_ext [] = more
   3.122  
   3.123    in mk_ext fieldargs end;   
   3.124 @@ -1125,8 +1113,8 @@
   3.125  
   3.126      (* code generator data *)
   3.127          (* Representation as nested pairs is revealed for codegeneration *)
   3.128 -    val [rep_code,abs_code] = map (Codegen.parse_mixfix (K (Bound 0))) ["I","I"];
   3.129 -    val ext_type_code = Codegen.parse_mixfix (K dummyT) "_";
   3.130 +    val [rep_code,abs_code] = map (Codegen.parse_mixfix (K (Bound 0))) ["(_)","(_)"];
   3.131 +    val ext_type_code = Codegen.parse_mixfix (K dummyT) "(_)";
   3.132      
   3.133      (* 1st stage: defs_thy *)
   3.134      val (defs_thy, ([abs_inject, abs_inverse, abs_induct],ext_def::dest_defs)) =
   3.135 @@ -1695,9 +1683,9 @@
   3.136  val setup =
   3.137   [RecordsData.init,
   3.138    Theory.add_trfuns ([], parse_translation, [], []),
   3.139 -  Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),  
   3.140 +  Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),   
   3.141    Simplifier.change_simpset_of Simplifier.addsimprocs
   3.142 -    [record_simproc, record_eq_simproc]];
   3.143 +    [record_simproc, record_upd_simproc, record_eq_simproc]];
   3.144  
   3.145  (* outer syntax *)
   3.146  
   3.147 @@ -1708,7 +1696,7 @@
   3.148      (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
   3.149  
   3.150  val recordP =
   3.151 -  OuterSyntax.command "record" "define extensible record" K.thy_decl   
   3.152 +  OuterSyntax.command "record" "define extensible record" K.thy_decl  
   3.153      (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));  
   3.154  
   3.155  val _ = OuterSyntax.add_parsers [recordP];