Last change
on this file since 1730 was
1730,
checked in by sacerdot, 8 years ago

Minor changes while studying the proof.

File size:
1.3 KB

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  CtrC 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: (*CSC: the existguarded premise is just to make the proof more general *) 

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

31  (* CSC: useless for the proof and very weak 

32  ; prop_colouring3: 

33  spilled_no = 0 ∨ 

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

35  *) 

36  }. 

37  

38  axiom build: ∀valuation. coloured_graph valuation. 

Note: See
TracBrowser
for help on using the repository browser.