Changeset 1218
 Timestamp:
 Sep 15, 2011, 4:56:30 PM (9 years ago)
 Location:
 src/utilities
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/Interference.ma
r1212 r1218 12 12 definition vertex_set ≝ set vertex. 13 13 definition vertex_priority_set ≝ priority_set vertex. 14 definition vertex_set_table ≝ set_table vertex (set vertex). 15 definition Register_set_table ≝ set_table vertex (set Register). 14 16 definition Register_set ≝ set Register. 15 17 16 record graph: Type[ 1] ≝18 record graph: Type[0] ≝ 17 19 { 18 20 ig_regmap : register_table; 19 ig_ivv : vertex_set ;20 ig_ivh : Register_set ;21 ig_ivv : vertex_set_table; 22 ig_ivh : Register_set_table; 21 23 ig_pvv : vertex_set; 22 24 ig_pvh : Register_set; … … 24 26 ig_nmr : vertex_priority_set 25 27 }. 28 29 definition set_ivv ≝ 30 λgraph. 31 λivv: vertex_set_table. 32 let regmap ≝ ig_regmap graph in 33 let ivh ≝ ig_ivh graph in 34 let pvv ≝ ig_pvv graph in 35 let pvh ≝ ig_pvh graph in 36 let degree ≝ ig_degree graph in 37 let nmr ≝ ig_nmr graph in 38 mk_graph 39 regmap ivv ivh pvv pvh degree nmr. 40 41 definition set_ivh ≝ 42 λgraph. 43 λivh: Register_set_table. 44 let regmap ≝ ig_regmap graph in 45 let ivv ≝ ig_ivv graph in 46 let pvv ≝ ig_pvv graph in 47 let pvh ≝ ig_pvh graph in 48 let degree ≝ ig_degree graph in 49 let nmr ≝ ig_nmr graph in 50 mk_graph 51 regmap ivv ivh pvv pvh degree nmr. 52 53 definition set_degree ≝ 54 λgraph. 55 λdegree: vertex_priority_set. 56 let regmap ≝ ig_regmap graph in 57 let ivv ≝ ig_ivv graph in 58 let ivh ≝ ig_ivh graph in 59 let pvv ≝ ig_pvv graph in 60 let pvh ≝ ig_pvh graph in 61 let nmr ≝ ig_nmr graph in 62 mk_graph 63 regmap ivv ivh pvv pvh degree nmr. 64 65 definition set_nmr ≝ 66 λgraph. 67 λnmr: vertex_priority_set. 68 let regmap ≝ ig_regmap graph in 69 let ivv ≝ ig_ivv graph in 70 let ivh ≝ ig_ivh graph in 71 let pvv ≝ ig_pvv graph in 72 let pvh ≝ ig_pvh graph in 73 let degree ≝ ig_degree graph in 74 mk_graph 75 regmap ivv ivh pvv pvh degree nmr. 76 77 definition sg_neighboursv ≝ 78 λgraph: graph. 79 λv: vertex. 80 set_tbl_find … v (ig_ivv graph). 81 82 definition sg_existsvv ≝ 83 λgraph. 84 λv1. 85 λv2. 86 match sg_neighboursv graph v2 with 87 [ None ⇒ false (* XXX: ok? *) 88  Some neigh ⇒ set_member ? v1 neigh 89 ]. 90 91 definition sg_neighboursh ≝ 92 λgraph. 93 λv. 94 set_tbl_find ? ? v (ig_ivh graph). 95 96 definition sg_existsvh ≝ 97 λgraph. 98 λv. 99 λh. 100 match sg_neighboursh graph v with 101 [ None ⇒ false (* XXX: ok? *) 102  Some neigh ⇒ set_member ? h neigh 103 ]. 104 105 definition sg_degree ≝ 106 λgraph. 107 λv. 108 match sg_neighboursv graph v with 109 [ None ⇒ None ? 110  Some neigh ⇒ 111 match sg_neighboursh graph v with 112 [ None ⇒ None ? 113  Some neigh' ⇒ Some ? ((set_size … neigh) + (set_size … neigh')) 114 ] 115 ]. 116 117 definition sg_hwregs ≝ 118 λgraph: graph. 119 let union ≝ λkey: vertex. set_union ? in 120 set_tbl_fold vertex ? ? union (ig_ivh graph) (set_empty Register). 121 122 axiom sg_iter: Type[0]. (* XXX: todo when i can be bothered *) 123 124 definition sg_mkvvi ≝ 125 λgraph. 126 λv1. 127 λv2. 128 set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (ig_ivv graph)). 129 130 definition sg_mkvv ≝ 131 λgraph. 132 λv1. 133 λv2. 134 if eq_nat v1 v2 then 135 graph 136 else if sg_existsvv graph v1 v2 then 137 graph 138 else 139 sg_mkvvi graph v1 v2. 140 141 definition sg_rmvv ≝ 142 λgraph. 143 λv1. 144 λv2. 145 set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (ig_ivv graph)). 146 147 definition sg_rmvvifx ≝ 148 λgraph. 149 λv1. 150 λv2. 151 if sg_existsvv graph v1 v2 then 152 sg_rmvv graph v1 v2 153 else 154 graph. 155 156 definition sg_mkvhi ≝ 157 λgraph. 158 λv. 159 λh. 160 set_ivh graph (set_tbl_update … v (set_insert … h) (ig_ivh graph)). 161 162 definition sg_mkvh ≝ 163 λgraph. 164 λv. 165 λh. 166 if sg_existsvh graph v h then 167 graph 168 else 169 sg_mkvhi graph v h. 170 171 definition sg_rmvh ≝ 172 λgraph. 173 λv. 174 λh. 175 set_ivh graph (set_tbl_update … v (set_remove … h) (ig_ivh graph)). 176 177 definition sg_rmvhifx ≝ 178 λgraph. 179 λv. 180 λh. 181 if sg_existsvh graph v h then 182 sg_rmvh graph v h 183 else 184 graph. 185 186 definition sg_coalesce ≝ 187 λg. 188 λx. 189 λy. 190 match sg_neighboursv g x with 191 [ None ⇒ None ? 192  Some neigh ⇒ 193 let graph ≝ set_fold ? graph (λw. λg. 194 sg_mkvv (sg_rmvv g x w) y w) neigh g 195 in 196 match sg_neighboursh g x with 197 [ None ⇒ None ? 198  Some neigh ⇒ 199 let graph ≝ set_fold ? ? (λh. λg. 200 sg_mkvh (sg_rmvh g x h) y h) neigh g 201 in 202 Some … graph 203 ] 204 ]. 205 206 definition sg_coalesceh ≝ 207 λg. 208 λx. 209 λh. 210 match sg_neighboursv g x with 211 [ None ⇒ None ? 212  Some neigh ⇒ 213 let graph ≝ set_fold ? graph (λw. λg. 214 sg_mkvh (sg_rmvv g x w) w h) neigh g 215 in 216 match sg_neighboursh g x with 217 [ None ⇒ None ? 218  Some neigh ⇒ 219 let graph ≝ set_fold ? ? (λk. λg. 220 sg_rmvh graph x k) neigh g 221 in 222 Some … graph 223 ] 224 ]. 225 226 definition sg_remove ≝ 227 λg. 228 λx. 229 match sg_neighboursv g x with 230 [ None ⇒ None ? 231  Some neigh ⇒ 232 let graph ≝ 233 set_fold … (λw. λgraph. 234 sg_rmvv graph x w) neigh g 235 in 236 match sg_neighboursh graph x with 237 [ None ⇒ None ? 238  Some neigh ⇒ 239 let graph ≝ set_fold … (λh. λg. 240 sg_rmvh g x h) neigh graph 241 in 242 Some ? graph 243 ] 244 ]. 245 246 definition ig_mkvvi ≝ 247 λgraph. 248 λv1. 249 λv2. 250 let graph ≝ sg_mkvvi graph v1 v2 in 251 let graph ≝ sg_rmvvifx graph v1 v2 in 252 let degree' ≝ pset_increment ? v1 (repr 1) (pset_increment ? v2 (repr 1) (ig_degree graph)) in 253 let nmr' ≝ pset_incrementifx ? v1 (repr 1) (pset_incrementifx ? v2 (repr 1) (ig_nmr graph)) in 254 set_degree (set_nmr graph nmr') degree'. 255 256 definition ig_rmvv ≝ 257 λgraph. 258 λv1. 259 λv2. 260 let graph ≝ sg_rmvv graph v1 v2 in 261 let degree' ≝ pset_increment ? v1 (neg (repr 1)) (pset_increment ? v2 (neg (repr 1)) (ig_degree graph)) in 262 let nmr' ≝ pset_incrementifx ? v1 (neg (repr 1)) (pset_incrementifx ? v2 (neg (repr 1)) (ig_nmr graph)) in 263 set_degree (set_nmr graph nmr') degree'. 264 265 definition ig_mkvhi ≝ 266 λgraph. 267 λv. 268 λh. 269 let graph ≝ sg_mkvhi graph v h in 270 let graph ≝ sg_rmvhifx graph v h in 271 let degree ≝ pset_increment ? v (repr 1) (ig_degree graph) in 272 let nmr ≝ pset_incrementifx ? v (repr 1) (ig_nmr graph) in 273 set_degree (set_nmr graph nmr) degree. 274 275 definition ig_rmvh ≝ 276 λgraph. 277 λv. 278 λh. 279 let graph ≝ sg_rmvh graph v h in 280 let degree ≝ pset_increment ? v (neg (repr 1)) (ig_degree graph) in 281 let nmr ≝ pset_incrementifx ? v (neg (repr 1)) (ig_nmr graph) in 282 set_degree (set_nmr graph nmr) degree. 283 284 definition pref_nmr ≝ 285 λgraph. 286 λv. 287 match sg_neighboursv graph v with 288 [ None ⇒ false (* XXX: ok? *) 289  Some neigh ⇒ 290 match sg_neighboursh graph v with 291 [ None ⇒ false 292  Some neigh' ⇒ 293 andb (set_is_empty ? neigh) (set_is_empty ? neigh') 294 ] 295 ]. 296 297 definition pref_mkcheck ≝ 298 λgraph. 299 λv. 300 if pref_nmr graph v then 301 let nmr' ≝ pset_remove ? v (ig_nmr graph) in 302 set_nmr graph nmr' 303 else 304 graph. 305 306 definition pref_mkvvi ≝ 307 λgraph. 308 λv1. 309 λv2. 310 if sg_existsvv graph v1 v2 then 311 graph 312 else 313 let graph ≝ pref_mkcheck graph v1 in 314 let graph ≝ pref_mkcheck graph v2 in 315 sg_mkvvi graph v1 v2. 316 317 definition pref_mkvhi ≝ 318 λgraph. 319 λv. 320 λh. 321 if sg_existsvh graph v h then 322 graph 323 else 324 let graph ≝ pref_mkcheck graph v in 325 sg_mkvhi graph v h. 326 327 (* XXX: look at this carefully *) 328 definition pref_rmcheck ≝ 329 λgraph. 330 λv. 331 if pref_nmr graph v then 332 match pset_lookup ? v (ig_degree graph) with 333 [ None ⇒ graph (* XXX: ok? *) 334  Some pref ⇒ 335 let nmr ≝ pset_insert ? v pref (ig_nmr graph) in 336 set_nmr graph nmr 337 ] 338 else 339 graph. 340 341 definition pref_rmvv ≝ 342 λgraph. 343 λv1. 344 λv2. 345 let graph ≝ sg_rmvv graph v1 v2 in 346 let graph ≝ pref_rmcheck graph v1 in 347 let graph ≝ pref_rmcheck graph v2 in 348 graph. 349 350 definition pref_rmvh ≝ 351 λgraph. 352 λv. 353 λh. 354 let graph ≝ sg_rmvh graph v h in 355 let graph ≝ pref_rmcheck graph v in 356 graph. 357 358 26 359 27 360 definition ig_create ≝ … … 34 367 〈v + 1, table'', priority''〉) 〈0, rt_empty …, ps_empty …〉 regs 35 368 in 36 mk_graph table'' (set_ empty …) (set_empty …) (set_empty …)369 mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_empty …) 37 370 (set_empty …) priority'' priority''. 38 371 39 definition neighboursv ≝ 40 λgraph: graph. 41 λv: vertex. 42 set_tbl_find … v (ig_ivv graph). 43 44 method neighborsv graph v = 45 VertexSetMap.find v (self#getvv graph) 372 46 373 47 374 definition ig_mkipp ≝ 
src/utilities/adt/priority_set_adt.ma
r1210 r1218 2 2 include "basics/list.ma". 3 3 include "arithmetics/nat.ma". 4 include "common/Integers.ma". 4 5 5 6 include "utilities/adt/ordering.ma". … … 8 9 axiom priority_set: Type[0] → Type[0]. 9 10 10 axiom ps _empty: ∀elt_type. priority_set elt_type.11 axiom ps _size: ∀elt_type. priority_set elt_type → nat.11 axiom pset_empty: ∀elt_type. priority_set elt_type. 12 axiom pset_size: ∀elt_type. priority_set elt_type → nat. 12 13 13 axiom ps _to_list: ∀elt_type. priority_set elt_type → list (elt_type × nat).14 axiom pset_to_list: ∀elt_type. priority_set elt_type → list (elt_type × nat). 14 15 15 axiom ps _insert: ∀elt_type. elt_type → nat → priority_set elt_type → priority_set elt_type.16 axiom ps _remove: ∀elt_type. elt_type → priority_set elt_type → priority_set elt_type.17 axiom ps _lookup: ∀elt_type. elt_type → priority_set elt_type → option nat.16 axiom pset_insert: ∀elt_type. elt_type → nat → priority_set elt_type → priority_set elt_type. 17 axiom pset_remove: ∀elt_type. elt_type → priority_set elt_type → priority_set elt_type. 18 axiom pset_lookup: ∀elt_type. elt_type → priority_set elt_type → option nat. 18 19 19 axiom ps_increment: ∀elt_type. elt_type → priority_set elt_type → priority_set elt_type. 20 axiom ps_modify: ∀elt_type. elt_type → nat → priority_set elt_type → priority_set elt_type. 21 axiom ps_lowest: ∀elt_type. priority_set elt_type → option (elt_type × nat). 20 axiom pset_increment: ∀elt_type. elt_type → int → priority_set elt_type → priority_set elt_type. 21 axiom pset_incrementifx: ∀elt_type. elt_type → int → priority_set elt_type → priority_set elt_type. 22 axiom pset_modify: ∀elt_type. elt_type → int → priority_set elt_type → priority_set elt_type. 23 axiom pset_lowest: ∀elt_type. priority_set elt_type → option (elt_type × nat). 22 24 23 axiom ps _equal: ∀elt_type. priority_set elt_type → priority_set elt_type → bool.25 axiom pset_equal: ∀elt_type. priority_set elt_type → priority_set elt_type → bool. 24 26 25 axiom ps _map: ∀elt_type. ∀a: Type[0]. (elt_type → a) → priority_set elt_type → priority_set a.26 axiom ps _fold: ∀elt_type. ∀a: Type[0]. (elt_type → nat → a → a) → priority_set elt_type → a → a.27 axiom pset_map: ∀elt_type. ∀a: Type[0]. (elt_type → a) → priority_set elt_type → priority_set a. 28 axiom pset_fold: ∀elt_type. ∀a: Type[0]. (elt_type → int → a → a) → priority_set elt_type → a → a. 27 29 28 definition ps _is_empty ≝30 definition pset_is_empty ≝ 29 31 λelt_type : Type[0]. 30 32 λpriority_set : priority_set elt_type. 31 ps _size … priority_set = 0.33 pset_size … priority_set = 0. 32 34 33 definition ps _singleton ≝35 definition pset_singleton ≝ 34 36 λelt_type : Type[0]. 35 37 λelt : elt_type. 36 38 λpriority : nat. 37 ps _insert … elt priority (ps_empty elt_type).39 pset_insert … elt priority (pset_empty elt_type). 38 40 39 definition from_list ≝41 definition pset_from_list ≝ 40 42 λelt_type : Type[0]. 41 43 λthe_list : list (elt_type × nat). 42 44 foldr … (λelt_priority. 43 45 let 〈elt, priority〉 ≝ elt_priority in 44 ps _insert elt_type elt priority)45 (ps _empty …) the_list.46 pset_insert elt_type elt priority) 47 (pset_empty …) the_list. 
src/utilities/adt/set_adt.ma
r1210 r1218 2 2 include "basics/list.ma". 3 3 include "arithmetics/nat.ma". 4 include "ASM/Util.ma". 4 5 5 6 include "utilities/adt/ordering.ma". … … 23 24 λelt_type: Type[0]. 24 25 λset: set elt_type. 25 set_size elt_type set =0.26 eq_nat (set_size elt_type set) 0. 26 27 27 28 definition set_singleton ≝ 
src/utilities/adt/set_table_adt.ma
r1212 r1218 7 7 axiom set_table: Type[0] → Type[0] → Type[0]. 8 8 9 axiom set_tbl_find: ∀key_type, a. key_type → set_table key_type (set a) → option a. 9 axiom set_tbl_empty: ∀key_type, a. set_table key_type a. 10 axiom set_tbl_find: ∀key_type, a. key_type → set_table key_type (set a) → option (set a). 10 11 axiom set_tbl_add: ∀key_type, a. key_type → set a 11 12 → set_table key_type (set a) → set_table key_type (set a). … … 19 20 set_table key_type (set a) → set_table key_type (set a). 20 21 axiom set_tbl_fold: ∀key_type, a, b: Type[0]. (key_type → a → b → b) 21 → set_table key_type (set a)> b > b.22 → set_table key_type a > b > b. 22 23 axiom set_tbl_pick: ∀key_type, a. set_table key_type (set a) → 23 24 (key_type → a → bool) → option (key_type × a). 25 26 27 axiom set_tbl_homo_mkbiedge: ∀key_type. key_type → key_type → set_table key_type (set key_type) → set_table key_type (set key_type). 28 axiom set_tbl_homo_rmbiedge: ∀key_type. key_type → key_type → set_table key_type (set key_type) → set_table key_type (set key_type). 29 axiom set_tbl_homo_reverse: ∀key_type. set_table key_type (set key_type) → set_table key_type (set key_type). 30 axiom set_tbl_homo_restrict: ∀key_type. (key_type → bool) → set_table key_type (set key_type) → set_table key_type (set key_type). 
src/utilities/adt/table_adt.ma
r1210 r1218 35 35 axiom tbl_map : ∀key_type, rng_type. ∀a: Type[0]. (rng_type → a) → table key_type rng_type 36 36 → table key_type a. 37 axiom tbl_fold : ∀key_type, rng_type. ∀a: Type[0]. (key_type → a → a) → table key_type rng_type → a → a.37 axiom tbl_fold : ∀key_type, a, b: Type[0]. (key_type → a → b → b) → table key_type a → b → b. 38 38 39 39 definition tbl_is_empty ≝
Note: See TracChangeset
for help on using the changeset viewer.