Changeset 1223 for src/utilities
 Timestamp:
 Sep 16, 2011, 5:15:35 PM (8 years ago)
 Location:
 src/utilities
 Files:

 6 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/Interference.ma
r1219 r1223 2 2 include "basics/list.ma". 3 3 include "common/Graphs.ma". 4 include "common/Order.ma". 4 5 include "common/Registers.ma". 5 6 … … 10 11 include "utilities/adt/register_table.ma". 11 12 12 definition vertex_set ≝ set vertex. 13 (* definition vertex_set ≝ set vertex. *) 13 14 definition vertex_priority_set ≝ priority_set vertex. 14 15 definition vertex_set_table ≝ set_table vertex (set vertex). … … 18 19 record graph: Type[0] ≝ 19 20 { 20 ig_regmap : register_table;21 ig_ivv : vertex_set_table;22 ig_ivh : Register_set_table;23 ig_pvv : vertex_set;24 ig_pvh : Register_set;25 ig_degree : vertex_priority_set;26 ig_nmr : vertex_priority_set21 g_regmap : register_table; 22 g_ivv : vertex_set_table; 23 g_ivh : Register_set_table; 24 g_pvv : vertex_set_table; 25 g_pvh : Register_set_table; 26 g_degree : vertex_priority_set; 27 g_nmr : vertex_priority_set 27 28 }. 28 29 … … 30 31 λgraph. 31 32 λivv: vertex_set_table. 32 let regmap ≝ ig_regmap graph in33 let ivh ≝ ig_ivh graph in34 let pvv ≝ ig_pvv graph in35 let pvh ≝ ig_pvh graph in36 let degree ≝ ig_degree graph in37 let nmr ≝ ig_nmr graph in33 let regmap ≝ g_regmap graph in 34 let ivh ≝ g_ivh graph in 35 let pvv ≝ g_pvv graph in 36 let pvh ≝ g_pvh graph in 37 let degree ≝ g_degree graph in 38 let nmr ≝ g_nmr graph in 38 39 mk_graph 39 40 regmap ivv ivh pvv pvh degree nmr. … … 42 43 λgraph. 43 44 λivh: Register_set_table. 44 let regmap ≝ ig_regmap graph in45 let ivv ≝ ig_ivv graph in46 let pvv ≝ ig_pvv graph in47 let pvh ≝ ig_pvh graph in48 let degree ≝ ig_degree graph in49 let nmr ≝ ig_nmr graph in45 let regmap ≝ g_regmap graph in 46 let ivv ≝ g_ivv graph in 47 let pvv ≝ g_pvv graph in 48 let pvh ≝ g_pvh graph in 49 let degree ≝ g_degree graph in 50 let nmr ≝ g_nmr graph in 50 51 mk_graph 51 52 regmap ivv ivh pvv pvh degree nmr. … … 54 55 λgraph. 55 56 λdegree: vertex_priority_set. 56 let regmap ≝ ig_regmap graph in57 let ivv ≝ ig_ivv graph in58 let ivh ≝ ig_ivh graph in59 let pvv ≝ ig_pvv graph in60 let pvh ≝ ig_pvh graph in61 let nmr ≝ ig_nmr graph in57 let regmap ≝ g_regmap graph in 58 let ivv ≝ g_ivv graph in 59 let ivh ≝ g_ivh graph in 60 let pvv ≝ g_pvv graph in 61 let pvh ≝ g_pvh graph in 62 let nmr ≝ g_nmr graph in 62 63 mk_graph 63 64 regmap ivv ivh pvv pvh degree nmr. … … 66 67 λgraph. 67 68 λnmr: vertex_priority_set. 68 let regmap ≝ ig_regmap graph in69 let ivv ≝ ig_ivv graph in70 let ivh ≝ ig_ivh graph in71 let pvv ≝ ig_pvv graph in72 let pvh ≝ ig_pvh graph in73 let degree ≝ ig_degree graph in69 let regmap ≝ g_regmap graph in 70 let ivv ≝ g_ivv graph in 71 let ivh ≝ g_ivh graph in 72 let pvv ≝ g_pvv graph in 73 let pvh ≝ g_pvh graph in 74 let degree ≝ g_degree graph in 74 75 mk_graph 75 76 regmap ivv ivh pvv pvh degree nmr. … … 78 79 λgraph: graph. 79 80 λv: vertex. 80 set_tbl_find … v ( ig_ivv graph).81 set_tbl_find … v (g_ivv graph). 81 82 82 83 definition sg_existsvv ≝ … … 86 87 match sg_neighboursv graph v2 with 87 88 [ None ⇒ false (* XXX: ok? *) 88  Some neigh ⇒ set_member ? v1 neigh89  Some neigh ⇒ set_member ? eq_nat v1 neigh 89 90 ]. 90 91 … … 92 93 λgraph. 93 94 λv. 94 set_tbl_find ? ? v ( ig_ivh graph).95 set_tbl_find ? ? v (g_ivh graph). 95 96 96 97 definition sg_existsvh ≝ … … 100 101 match sg_neighboursh graph v with 101 102 [ None ⇒ false (* XXX: ok? *) 102  Some neigh ⇒ set_member ? h neigh103  Some neigh ⇒ set_member ? eq_Register h neigh 103 104 ]. 104 105 … … 118 119 λgraph: graph. 119 120 let union ≝ λkey: vertex. set_union ? in 120 set_tbl_fold vertex ? ? union ( ig_ivh graph) (set_empty Register).121 set_tbl_fold vertex ? ? union (g_ivh graph) (set_empty Register). 121 122 122 123 axiom sg_iter: Type[0]. (* XXX: todo when i can be bothered *) … … 126 127 λv1. 127 128 λv2. 128 set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 ( ig_ivv graph)).129 set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (g_ivv graph)). 129 130 130 131 definition sg_mkvv ≝ … … 143 144 λv1. 144 145 λv2. 145 set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 ( ig_ivv graph)).146 set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (g_ivv graph)). 146 147 147 148 definition sg_rmvvifx ≝ … … 158 159 λv. 159 160 λh. 160 set_ivh graph (set_tbl_update … v (set_insert … h) ( ig_ivh graph)).161 set_ivh graph (set_tbl_update … v (set_insert … h) (g_ivh graph)). 161 162 162 163 definition sg_mkvh ≝ … … 173 174 λv. 174 175 λh. 175 set_ivh graph (set_tbl_update … v (set_remove … h) ( ig_ivh graph)).176 set_ivh graph (set_tbl_update … v (set_remove … h) (g_ivh graph)). 176 177 177 178 definition sg_rmvhifx ≝ … … 250 251 let graph ≝ sg_mkvvi graph v1 v2 in 251 252 let graph ≝ sg_rmvvifx graph v1 v2 in 252 let degree' ≝ pset_increment ? v1 (repr 1) (pset_increment ? v2 (repr 1) ( ig_degree graph)) in253 let nmr' ≝ pset_incrementifx ? v1 (repr 1) (pset_incrementifx ? v2 (repr 1) ( ig_nmr graph)) in253 let degree' ≝ pset_increment ? v1 (repr 1) (pset_increment ? v2 (repr 1) (g_degree graph)) in 254 let nmr' ≝ pset_incrementifx ? v1 (repr 1) (pset_incrementifx ? v2 (repr 1) (g_nmr graph)) in 254 255 set_degree (set_nmr graph nmr') degree'. 255 256 … … 259 260 λv2. 260 261 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)) in262 let nmr' ≝ pset_incrementifx ? v1 (neg (repr 1)) (pset_incrementifx ? v2 (neg (repr 1)) ( ig_nmr graph)) in262 let degree' ≝ pset_increment ? v1 (neg (repr 1)) (pset_increment ? v2 (neg (repr 1)) (g_degree graph)) in 263 let nmr' ≝ pset_incrementifx ? v1 (neg (repr 1)) (pset_incrementifx ? v2 (neg (repr 1)) (g_nmr graph)) in 263 264 set_degree (set_nmr graph nmr') degree'. 264 265 … … 269 270 let graph ≝ sg_mkvhi graph v h in 270 271 let graph ≝ sg_rmvhifx graph v h in 271 let degree ≝ pset_increment ? v (repr 1) ( ig_degree graph) in272 let nmr ≝ pset_incrementifx ? v (repr 1) ( ig_nmr graph) in272 let degree ≝ pset_increment ? v (repr 1) (g_degree graph) in 273 let nmr ≝ pset_incrementifx ? v (repr 1) (g_nmr graph) in 273 274 set_degree (set_nmr graph nmr) degree. 274 275 … … 278 279 λh. 279 280 let graph ≝ sg_rmvh graph v h in 280 let degree ≝ pset_increment ? v (neg (repr 1)) ( ig_degree graph) in281 let nmr ≝ pset_incrementifx ? v (neg (repr 1)) ( ig_nmr graph) in281 let degree ≝ pset_increment ? v (neg (repr 1)) (g_degree graph) in 282 let nmr ≝ pset_incrementifx ? v (neg (repr 1)) (g_nmr graph) in 282 283 set_degree (set_nmr graph nmr) degree. 283 284 … … 299 300 λv. 300 301 if pref_nmr graph v then 301 let nmr' ≝ pset_remove ? v ( ig_nmr graph) in302 let nmr' ≝ pset_remove ? v (g_nmr graph) in 302 303 set_nmr graph nmr' 303 304 else … … 330 331 λv. 331 332 if pref_nmr graph v then 332 match pset_lookup ? v ( ig_degree graph) with333 match pset_lookup ? v (g_degree graph) with 333 334 [ None ⇒ graph (* XXX: ok? *) 334 335  Some pref ⇒ 335 let nmr ≝ pset_insert ? v pref ( ig_nmr graph) in336 let nmr ≝ pset_insert ? v pref (g_nmr graph) in 336 337 set_nmr graph nmr 337 338 ] … … 355 356 let graph ≝ pref_rmcheck graph v in 356 357 graph. 358 359 definition ig_ipp ≝ sg_neighboursv. 360 definition ig_iph ≝ sg_neighboursh. 361 definition ig_ppp ≝ sg_neighboursv. 362 definition ig_pph ≝ sg_neighboursh. 363 definition ig_degree ≝ λgraph. λv. pset_lookup ? v (g_degree graph). 364 definition ig_lowest ≝ λgraph. pset_lowest ? (g_degree graph). 365 definition ig_lowest_non_move_related ≝ λgraph. pset_lowest ? (g_nmr graph). 366 definition ig_fold ≝ λA: Type[0]. λf: vertex → A → A. λgraph. λaccu. 367 rt_fold … (λv. λ_. λaccu. f v accu) (g_regmap graph) accu. 368 369 definition ig_minimum: ∀a: Type[0]. (a → a → order) → (vertex → a) → graph → option vertex ≝ 370 λa: Type[0]. 371 λcompare: a → a → order. 372 λf: vertex → a. 373 λgraph. 374 let folded ≝ ig_fold … (λw. λaccu. 375 let dw ≝ f w in 376 match accu with 377 [ None ⇒ Some … 〈dw, w〉 378  Some dv_v ⇒ 379 let 〈dv, v〉 ≝ dv_v in 380 match compare dw dv with 381 [ order_lt ⇒ Some … 〈dw, w〉 382  _ ⇒ accu 383 ] 384 ]) graph (None …) 385 in 386 match folded with 387 [ None ⇒ None … 388  Some ignore_v ⇒ 389 let 〈ignore, v〉 ≝ ignore_v in 390 Some … v 391 ]. 392 393 definition ig_ppedge ≝ vertex × vertex. 394 395 definition ig_pppick ≝ λgraph. λp. set_tbl_pick … (g_pvv graph) p. 396 397 definition ig_phedge ≝ vertex × Register. 398 399 definition ig_phpick ≝ λgraph. λp. set_tbl_pick … (g_pvh graph) p. 357 400 358 401 definition ig_create ≝ … … 365 408 〈v + 1, table'', priority''〉) 〈0, rt_empty …, pset_empty …〉 regs 366 409 in 367 mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_empty …) 368 (set_empty …) priority'' priority''. 369 370 371 410 mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_tbl_empty …) 411 (set_tbl_empty …) priority'' priority''. 412 definition ig_lookup ≝ λgraph. λr. rt_backward r (g_regmap graph). 413 definition ig_registers ≝ λgraph. λv. rt_forward v (g_regmap graph). 372 414 definition ig_mkipp ≝ 373 λset_impl. 374 λgraph: interference_graph set_impl. 415 λgraph. 375 416 λregs1. 376 417 λregs2. 377 set_fold … (ig_Reg_set … graph) (λr1. λgraph. 378 let v1 ≝ lookup … graph r1 in 379 set_fold … (ig_Reg_set … graph) (λr2. λgraph. 380 ig_mkvv … 381 382 let mkipp graph regs1 regs2 = 383 Register.Set.fold (fun r1 graph > 384 let v1 = lookup graph r1 in 385 Register.Set.fold (fun r2 graph > 386 interference#mkvv graph v1 (lookup graph r2) 387 ) regs2 graph 388 ) regs1 graph 389 390 axiom ig_mkiph: graph → list register → list Register → 391 graph. 392 393 definition ig_mki: graph → (list register) × (list Register) → 394 (list register) × (list Register) → graph ≝ 418 set_fold … (λr1. λgraph. 419 let v1 ≝ ig_lookup graph r1 in 420 set_fold … (λr2. λgraph. 421 sg_mkvv graph v1 (ig_lookup graph r2) 422 ) regs2 graph 423 ) regs1 graph. 424 definition ig_mkiph ≝ 425 λgraph. 426 λregs. 427 λhwregs. 428 set_fold … (λr. λgraph. 429 let v ≝ ig_lookup graph r in 430 set_fold … (λh. λgraph. 431 sg_mkvh graph v h 432 ) hwregs graph 433 ) regs graph. 434 definition ig_mki ≝ 395 435 λgraph. 396 436 λregs1_hwregs1. 397 437 λregs2_hwregs2. 398 let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in 399 let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in 400 let graph ≝ ig_mkipp graph regs1 regs2 in 401 let graph ≝ ig_mkiph graph regs1 hwregs2 in 402 let graph ≝ ig_mkiph graph regs2 hwregs1 in 403 graph. 438 let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in 439 let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in 440 let graph ≝ ig_mkipp graph regs1 regs2 in 441 let graph ≝ ig_mkiph graph regs1 hwregs2 in 442 let graph ≝ ig_mkiph graph regs2 hwregs1 in 443 graph. 444 definition ig_mkppp ≝ 445 λgraph. 446 λr1. 447 λr2. 448 let v1 ≝ ig_lookup graph r1 in 449 let v2 ≝ ig_lookup graph r2 in 450 let graph ≝ sg_mkvv graph v1 v2 in 451 graph. 452 definition ig_mkpph ≝ 453 λgraph. 454 λr. 455 λh. 456 let v ≝ ig_lookup graph r in 457 let graph ≝ sg_mkvh graph v h in 458 graph. 459 (* 460 (* XXX: precondition: 461 x \not\eq y 462 existsvv graph x y == false i.e. coalesce interfering edges *) 463 definition ig_coalesce ≝ 464 λgraph. 465 λx. 466 λy. 467 let graph ≝ sg_coalesce graph x y in 468 469 let coalesce graph x y = 470 471 assert (x <> y); (* attempt to coalesce one vertex with itself *) 472 assert (not (interference#existsvv graph x y)); (* attempt to coalesce two interfering vertices *) 473 474 (* Perform coalescing in the two subgraphs. *) 475 476 let graph = interference#coalesce graph x y in 477 let graph = preference#coalesce graph x y in 478 479 (* Remove [x] from all tables. *) 480 481 { 482 graph with 483 regmap = RegMap.coalesce x y graph.regmap; 484 ivh = Vertex.Map.remove x graph.ivh; 485 pvh = Vertex.Map.remove x graph.pvh; 486 degree = PrioritySet.remove x graph.degree; 487 nmr = PrioritySet.remove x graph.nmr; 488 } 404 489 405 490 axiom ig_mkppp: interference_graph → register → register → interference_graph. … … 427 512 definition ig_phedge ≝ vertex × Register. 428 513 axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge. 514 *) 
src/utilities/adt/priority_set_adt.ma
r1218 r1223 4 4 include "common/Integers.ma". 5 5 6 include "utilities/adt/ordering.ma".7 6 include "ASM/Util.ma". 8 7 
src/utilities/adt/register_table.ma
r1211 r1223 1 1 include "ASM/I8051.ma". 2 2 include "common/Registers.ma". 3 include "utilities/adt/ordering.ma".4 3 include "utilities/adt/set_adt.ma". 5 4 6 5 definition vertex ≝ nat. (* XXX: int in o'caml *) 7 6 7 (* 8 8 axiom Register_ordered: ordered Register. 9 9 axiom register_ordered: ordered register. 10 10 axiom vertex_ordered: ordered vertex. 11 *) 11 12 12 13 axiom register_table: Type[0]. 13 14 14 15 axiom rt_empty : register_table. 16 17 axiom rt_insert: vertex → set Register → register_table → register_table. 15 18 16 19 axiom rt_forward : vertex → register_table → set Register. 
src/utilities/adt/set_adt.ma
r1218 r1223 3 3 include "arithmetics/nat.ma". 4 4 include "ASM/Util.ma". 5 6 include "utilities/adt/ordering.ma".7 5 8 6 axiom set: Type[0] → Type[0]. … … 13 11 axiom set_insert: ∀elt_type. elt_type → set elt_type → set elt_type. 14 12 axiom set_remove: ∀elt_type. elt_type → set elt_type → set elt_type. 15 axiom set_member: ∀elt_type. elt_type → set elt_type → bool.13 axiom set_member: ∀elt_type. (elt_type → elt_type → bool) → elt_type → set elt_type → bool. 16 14 axiom set_forall: ∀elt_type. (elt_type → bool) → set elt_type → bool. 17 15 axiom set_exists: ∀elt_type. (elt_type → bool) → set elt_type → bool. 18 16 axiom set_filter: ∀elt_type. (elt_type → bool) → set elt_type → set elt_type. 19 axiom set_equal: ∀elt_type. set elt_type → set elt_type → bool.20 17 axiom set_map: ∀elt_type, a. (elt_type → a) → set elt_type → set a. 21 18 axiom set_fold: ∀elt_type, a: Type[0]. (elt_type → a → a) → set elt_type → a → a. 19 axiom set_equal: ∀elt_type: Type[0]. (elt_type → elt_type → bool) → 20 set elt_type → set elt_type → bool. 21 22 (* XXX: define in terms of primitives *) 23 axiom set_diff: ∀elt_type: Type[0]. set elt_type → set elt_type → set elt_type. 22 24 23 25 definition set_is_empty ≝ … … 47 49 definition set_subset ≝ 48 50 λelt_type: Type[0]. 51 λeq : elt_type → elt_type → bool. 49 52 λleft : set elt_type. 50 53 λright : set elt_type. 51 set_forall elt_type (λelt. set_member elt_type e lt right) left.54 set_forall elt_type (λelt. set_member elt_type eq elt right) left. 52 55 53 56 definition set_subseteq ≝ 54 57 λelt_type: Type[0]. 58 λeq : elt_type → elt_type → bool. 55 59 λleft : set elt_type. 56 60 λright : set elt_type. 57 set_equal elt_type left right ∧ (set_subset elt_typeleft right).61 set_equal elt_type eq left right ∧ (set_subset elt_type eq left right). 58 62 59 63 definition set_union ≝ … … 65 69 definition set_intersection ≝ 66 70 λelt_type: Type[0]. 71 λeq : elt_type → elt_type → bool. 67 72 λleft : set elt_type. 68 73 λright : set elt_type. 69 set_filter elt_type (λelt. set_member elt_type e lt right) left.74 set_filter elt_type (λelt. set_member elt_type eq elt right) left. 
src/utilities/adt/set_table_adt.ma
r1218 r1223 3 3 include "utilities/adt/set_adt.ma". 4 4 include "utilities/adt/table_adt.ma". 5 include "utilities/adt/ordering.ma".6 5 7 6 axiom set_table: Type[0] → Type[0] → Type[0]. … … 22 21 → set_table key_type a > b > b. 23 22 axiom set_tbl_pick: ∀key_type, a. set_table key_type (set a) → 24 ( key_type → a→ bool) → option (key_type × a).23 ((key_type × a) → bool) → option (key_type × a). 25 24 26 25 
src/utilities/adt/table_adt.ma
r1218 r1223 5 5 include "arithmetics/nat.ma". 6 6 7 include "utilities/adt/ordering.ma".8 7 include "utilities/adt/equal.ma". 9 8
Note: See TracChangeset
for help on using the changeset viewer.