Changeset 1232 for src/ERTL/Interference.ma
- Timestamp:
- Sep 21, 2011, 11:24:02 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/Interference.ma
r1230 r1232 15 15 definition vertex ≝ register ⊎ Register. 16 16 17 record graph: Type[0] ≝ 17 inductive decision: Type[0] ≝ 18 | decision_spill: nat → decision 19 | decision_colour: Register → decision. 20 21 definition is_member ≝ 22 λvertex. 23 λregister_lattice. 24 let 〈l, r〉 ≝ register_lattice in 25 match vertex with 26 [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l 27 | inr v ⇒ set_member ? eq_Register v r 28 ]. 29 30 record coloured_graph (v: valuation): Type[1] ≝ 18 31 { 19 interferes: vertex → vertex → bool 32 colouring: vertex → decision; 33 prop_colouring: ∀l. ∀v1, v2: vertex. 34 is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2 20 35 }. 21 36 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 axiom colour_initial: graph → initial_colouring. 37 definition stack_colouring ≝ coloured_graph nat. 38 axiom colour_stack: graph → stack_colouring. 39 37 axiom build: ∀valuation. coloured_graph valuation. 40 38 41 39 (* definition vertex_set ≝ set vertex. *) … … 517 515 nmr = PrioritySet.remove x graph.nmr; 518 516 } 519 *)520 521 *)522 517 523 518 axiom ig_mkppp: graph → register → register → graph. … … 527 522 axiom ig_remove: graph → vertex → graph. 528 523 axiom ig_freeze: graph → vertex → graph. 529 axiom ig_restrict: graph → ( register → bool) → graph. (* XXX: change *)524 axiom ig_restrict: graph → (vertex → bool) → graph. 530 525 axiom ig_droph: graph → graph. 531 526 axiom ig_lookup: graph → register → vertex. … … 545 540 definition ig_phedge ≝ vertex × Register. 546 541 axiom ig_phpick: graph → (ig_phedge → bool) → option ig_phedge. 542 *) 543 *)
Note: See TracChangeset
for help on using the changeset viewer.