Changeset 1218 for src/utilities/Interference.ma
- Timestamp:
- Sep 15, 2011, 4:56:30 PM (9 years ago)
- File:
-
- 1 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 ≝
Note: See TracChangeset
for help on using the changeset viewer.