Changeset 1229 for src/ERTL/Interference.ma
 Timestamp:
 Sep 20, 2011, 1:26:46 PM (9 years ago)
 File:

 1 moved
Legend:
 Unmodified
 Added
 Removed

src/ERTL/Interference.ma
r1228 r1229 4 4 include "common/Order.ma". 5 5 include "common/Registers.ma". 6 include "ERTL/ERTL.ma". 7 include "ERTL/liveness.ma". 6 8 7 9 include "utilities/adt/table_adt.ma". … … 11 13 include "utilities/adt/register_table.ma". 12 14 15 definition vertex ≝ register ⊎ Register. 16 17 record graph: Type[0] ≝ 18 { 19 interferes: vertex → vertex → bool 20 }. 21 22 axiom build: ∀globals: list ident. ertl_internal_function globals → valuation × graph. 23 24 inductive decision: Type[0] ≝ 25  decision_spill: decision 26  decision_colour: Register → decision. 27 28 record coloured_graph (d: Type[0]): Type[1] ≝ 29 { 30 the_graph: graph; 31 colouring: register → d; 32 prop_colouring: ∀v1. ∀v2. (interferes the_graph (inl … v1) (inl … v2) = true) → colouring v1 ≠ colouring v2 33 }. 34 35 definition initial_colouring ≝ coloured_graph decision. 36 definition stack_colouring ≝ coloured_graph nat. 37 38 13 39 (* definition vertex_set ≝ set vertex. *) 14 40 definition vertex_priority_set ≝ priority_set vertex. 15 41 definition vertex_set_table ≝ set_table vertex (set vertex). 42 definition vertex_set ≝ set vertex. 16 43 definition Register_set_table ≝ set_table vertex (set Register). 17 44 definition Register_set ≝ set Register. 18 45 46 (* 19 47 record graph: Type[0] ≝ 20 48 { … … 487 515 nmr = PrioritySet.remove x graph.nmr; 488 516 } 489 490 axiom ig_mkppp: interference_graph → register → register → interference_graph. 491 axiom ig_mkpph: interference_graph → register → Register → interference_graph. 492 axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph. 493 axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph. 494 axiom ig_remove: interference_graph → vertex → interference_graph. 495 axiom ig_freeze: interference_graph → vertex → interference_graph. 496 axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph. 497 axiom ig_droph: interference_graph → interference_graph. 498 axiom ig_lookup: interference_graph → register → vertex. 499 axiom ig_registers: interference_graph → vertex → list register. 500 axiom ig_degree: interference_graph → vertex → nat. 501 axiom ig_lowest: interference_graph → option (vertex × nat). 502 axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat). 517 *) 518 519 *) 520 521 axiom ig_mkppp: graph → register → register → graph. 522 axiom ig_mkpph: graph → register → Register → graph. 523 axiom ig_coalesce: graph → vertex → vertex → graph. 524 axiom ig_coalesceh: graph → vertex → Register → graph. 525 axiom ig_remove: graph → vertex → graph. 526 axiom ig_freeze: graph → vertex → graph. 527 axiom ig_restrict: graph → (vertex → bool) → graph. 528 axiom ig_droph: graph → graph. 529 axiom ig_lookup: graph → register → vertex. 530 axiom ig_registers: graph → vertex → list register. 531 axiom ig_degree: graph → vertex → nat. 532 axiom ig_lowest: graph → option (vertex × nat). 533 axiom ig_lowest_non_move_related: graph → option (vertex × nat). 503 534 axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) → 504 interference_graph → option vertex.505 axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.506 axiom ig_ipp: interference_graph → vertex → vertex_set.507 axiom ig_iph: interference_graph → vertex → list Register.508 axiom ig_ppp: interference_graph → vertex → vertex_set.509 axiom ig_pph: interference_graph → vertex → list Register.535 graph → option vertex. 536 axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → graph → A → A. 537 axiom ig_ipp: graph → vertex → vertex_set. 538 axiom ig_iph: graph → vertex → list Register. 539 axiom ig_ppp: graph → vertex → vertex_set. 540 axiom ig_pph: graph → vertex → list Register. 510 541 definition ig_ppedge ≝ vertex × vertex. 511 axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge.542 axiom ig_pppick: graph → (ig_ppedge → bool) → option ig_ppedge. 512 543 definition ig_phedge ≝ vertex × Register. 513 axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge. 514 *) 544 axiom ig_phpick: graph → (ig_phedge → bool) → option ig_phedge.
Note: See TracChangeset
for help on using the changeset viewer.