Line | |
---|

1 | include "ERTL/ERTL.ma". |
---|

2 | include "ERTL/liveness.ma". |
---|

3 | |
---|

4 | definition vertex ≝ register ⊎ Register. |
---|

5 | |
---|

6 | inductive decision: Type[0] ≝ |
---|

7 | | decision_spill: nat → decision |
---|

8 | | decision_colour: Register → decision. |
---|

9 | |
---|

10 | definition is_member ≝ |
---|

11 | λvertex. |
---|

12 | λregister_lattice. |
---|

13 | let 〈l, r〉 ≝ register_lattice in |
---|

14 | match vertex with |
---|

15 | [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l |
---|

16 | | inr v ⇒ set_member ? eq_Register v r |
---|

17 | ]. |
---|

18 | |
---|

19 | (* prop_colouring is the non interferece |
---|

20 | prop_colouring 2 and 3 together say that spilled_no is the number of spilled |
---|

21 | registers *) |
---|

22 | (* Wilmer: the generation of the destruct principle diverges; |
---|

23 | Ctr-C make the file pass *) |
---|

24 | record coloured_graph (v: valuation): Type[1] ≝ |
---|

25 | { colouring: vertex → decision |
---|

26 | ; spilled_no: nat |
---|

27 | ; prop_colouring: ∀l. ∀v1, v2: vertex. |
---|

28 | is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2 |
---|

29 | ; prop_colouring2: |
---|

30 | ∀v1:vertex. (∃l. bool_to_Prop (is_member v1 (v l))) → ∀i. colouring v1 = decision_spill i → lt i spilled_no |
---|

31 | ; prop_colouring3: |
---|

32 | spilled_no = 0 ∨ |
---|

33 | ∃l.∃v1:vertex. bool_to_Prop (is_member v1 (v l)) ∧ colouring v1 = decision_spill (minus spilled_no 1) |
---|

34 | }. |
---|

35 | |
---|

36 | axiom build: ∀valuation. coloured_graph valuation. |
---|

**Note:** See

TracBrowser
for help on using the repository browser.