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