src/HOL/Tools/record.ML
changeset 35137 405bb7e38057
parent 35136 34206672b168
child 35138 ad213c602ec1
     1.1 --- a/src/HOL/Tools/record.ML	Mon Feb 15 22:24:19 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Mon Feb 15 22:40:03 2010 +0100
     1.3 @@ -381,7 +381,7 @@
     1.4    equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
     1.5    extfields = extfields, fieldext = fieldext }: record_data;
     1.6  
     1.7 -structure RecordsData = Theory_Data
     1.8 +structure Records_Data = Theory_Data
     1.9  (
    1.10    type T = record_data;
    1.11    val empty =
    1.12 @@ -434,7 +434,7 @@
    1.13  
    1.14  fun print_records thy =
    1.15    let
    1.16 -    val {records = recs, ...} = RecordsData.get thy;
    1.17 +    val {records = recs, ...} = Records_Data.get thy;
    1.18      val prt_typ = Syntax.pretty_typ_global thy;
    1.19  
    1.20      fun pretty_parent NONE = []
    1.21 @@ -454,20 +454,20 @@
    1.22  
    1.23  (* access 'records' *)
    1.24  
    1.25 -val get_record = Symtab.lookup o #records o RecordsData.get;
    1.26 +val get_record = Symtab.lookup o #records o Records_Data.get;
    1.27  
    1.28  fun put_record name info thy =
    1.29    let
    1.30      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
    1.31 -      RecordsData.get thy;
    1.32 +      Records_Data.get thy;
    1.33      val data = make_record_data (Symtab.update (name, info) records)
    1.34        sel_upd equalities extinjects extsplit splits extfields fieldext;
    1.35 -  in RecordsData.put data thy end;
    1.36 +  in Records_Data.put data thy end;
    1.37  
    1.38  
    1.39  (* access 'sel_upd' *)
    1.40  
    1.41 -val get_sel_upd = #sel_upd o RecordsData.get;
    1.42 +val get_sel_upd = #sel_upd o Records_Data.get;
    1.43  
    1.44  val is_selector = Symtab.defined o #selectors o get_sel_upd;
    1.45  val get_updates = Symtab.lookup o #updates o get_sel_upd;
    1.46 @@ -492,7 +492,7 @@
    1.47      val upds = map (suffix updateN) all ~~ all;
    1.48  
    1.49      val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
    1.50 -      equalities, extinjects, extsplit, splits, extfields, fieldext} = RecordsData.get thy;
    1.51 +      equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy;
    1.52      val data = make_record_data records
    1.53        {selectors = fold Symtab.update_new sels selectors,
    1.54          updates = fold Symtab.update_new upds updates,
    1.55 @@ -501,7 +501,7 @@
    1.56          foldcong = foldcong addcongs folds,
    1.57          unfoldcong = unfoldcong addcongs unfolds}
    1.58         equalities extinjects extsplit splits extfields fieldext;
    1.59 -  in RecordsData.put data thy end;
    1.60 +  in Records_Data.put data thy end;
    1.61  
    1.62  
    1.63  (* access 'equalities' *)
    1.64 @@ -509,12 +509,12 @@
    1.65  fun add_record_equalities name thm thy =
    1.66    let
    1.67      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
    1.68 -      RecordsData.get thy;
    1.69 +      Records_Data.get thy;
    1.70      val data = make_record_data records sel_upd
    1.71        (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext;
    1.72 -  in RecordsData.put data thy end;
    1.73 -
    1.74 -val get_equalities = Symtab.lookup o #equalities o RecordsData.get;
    1.75 +  in Records_Data.put data thy end;
    1.76 +
    1.77 +val get_equalities = Symtab.lookup o #equalities o Records_Data.get;
    1.78  
    1.79  
    1.80  (* access 'extinjects' *)
    1.81 @@ -522,13 +522,13 @@
    1.82  fun add_extinjects thm thy =
    1.83    let
    1.84      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
    1.85 -      RecordsData.get thy;
    1.86 +      Records_Data.get thy;
    1.87      val data =
    1.88        make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
    1.89          extsplit splits extfields fieldext;
    1.90 -  in RecordsData.put data thy end;
    1.91 -
    1.92 -val get_extinjects = rev o #extinjects o RecordsData.get;
    1.93 +  in Records_Data.put data thy end;
    1.94 +
    1.95 +val get_extinjects = rev o #extinjects o Records_Data.get;
    1.96  
    1.97  
    1.98  (* access 'extsplit' *)
    1.99 @@ -536,11 +536,11 @@
   1.100  fun add_extsplit name thm thy =
   1.101    let
   1.102      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   1.103 -      RecordsData.get thy;
   1.104 +      Records_Data.get thy;
   1.105      val data = make_record_data records sel_upd
   1.106        equalities extinjects (Symtab.update_new (name, thm) extsplit) splits
   1.107        extfields fieldext;
   1.108 -  in RecordsData.put data thy end;
   1.109 +  in Records_Data.put data thy end;
   1.110  
   1.111  
   1.112  (* access 'splits' *)
   1.113 @@ -548,19 +548,19 @@
   1.114  fun add_record_splits name thmP thy =
   1.115    let
   1.116      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   1.117 -      RecordsData.get thy;
   1.118 +      Records_Data.get thy;
   1.119      val data = make_record_data records sel_upd
   1.120        equalities extinjects extsplit (Symtab.update_new (name, thmP) splits)
   1.121        extfields fieldext;
   1.122 -  in RecordsData.put data thy end;
   1.123 -
   1.124 -val get_splits = Symtab.lookup o #splits o RecordsData.get;
   1.125 +  in Records_Data.put data thy end;
   1.126 +
   1.127 +val get_splits = Symtab.lookup o #splits o Records_Data.get;
   1.128  
   1.129  
   1.130  (* parent/extension of named record *)
   1.131  
   1.132 -val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o RecordsData.get);
   1.133 -val get_extension = Option.map #extension oo (Symtab.lookup o #records o RecordsData.get);
   1.134 +val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Records_Data.get);
   1.135 +val get_extension = Option.map #extension oo (Symtab.lookup o #records o Records_Data.get);
   1.136  
   1.137  
   1.138  (* access 'extfields' *)
   1.139 @@ -568,14 +568,14 @@
   1.140  fun add_extfields name fields thy =
   1.141    let
   1.142      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   1.143 -      RecordsData.get thy;
   1.144 +      Records_Data.get thy;
   1.145      val data =
   1.146        make_record_data records sel_upd
   1.147          equalities extinjects extsplit splits
   1.148          (Symtab.update_new (name, fields) extfields) fieldext;
   1.149 -  in RecordsData.put data thy end;
   1.150 -
   1.151 -val get_extfields = Symtab.lookup o #extfields o RecordsData.get;
   1.152 +  in Records_Data.put data thy end;
   1.153 +
   1.154 +val get_extfields = Symtab.lookup o #extfields o Records_Data.get;
   1.155  
   1.156  fun get_extT_fields thy T =
   1.157    let
   1.158 @@ -585,7 +585,7 @@
   1.159        in Long_Name.implode (rev (nm :: rst)) end;
   1.160      val midx = maxidx_of_typs (moreT :: Ts);
   1.161      val varifyT = varifyT midx;
   1.162 -    val {records, extfields, ...} = RecordsData.get thy;
   1.163 +    val {records, extfields, ...} = Records_Data.get thy;
   1.164      val (flds, (more, _)) = split_last (Symtab.lookup_list extfields name);
   1.165      val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
   1.166  
   1.167 @@ -607,15 +607,15 @@
   1.168  fun add_fieldext extname_types fields thy =
   1.169    let
   1.170      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   1.171 -      RecordsData.get thy;
   1.172 +      Records_Data.get thy;
   1.173      val fieldext' =
   1.174        fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
   1.175      val data =
   1.176        make_record_data records sel_upd equalities extinjects
   1.177          extsplit splits extfields fieldext';
   1.178 -  in RecordsData.put data thy end;
   1.179 -
   1.180 -val get_fieldext = Symtab.lookup o #fieldext o RecordsData.get;
   1.181 +  in Records_Data.put data thy end;
   1.182 +
   1.183 +val get_fieldext = Symtab.lookup o #fieldext o Records_Data.get;
   1.184  
   1.185  
   1.186  (* parent records *)
   1.187 @@ -1189,7 +1189,7 @@
   1.188              ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
   1.189            if is_selector thy s andalso is_some (get_updates thy u) then
   1.190              let
   1.191 -              val {sel_upd = {updates, ...}, extfields, ...} = RecordsData.get thy;
   1.192 +              val {sel_upd = {updates, ...}, extfields, ...} = Records_Data.get thy;
   1.193  
   1.194                fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
   1.195                      (case Symtab.lookup updates u of