Last change
on this file since 1423 was
1423,
checked in by sacerdot, 9 years ago

 spill no longer used
 BUG IN Interference: generating the destruct principle takes too long
 ERTLToLTL not compiling ATM

File size:
1.2 KB

Line  

1  include "ERTL/ERTL.ma". 

2  include "ERTL/liveness.ma". 

3  include "basics/jmeq.ma". 

4  

5  definition vertex ≝ register ⊎ Register. 

6  

7  inductive decision: Type[0] ≝ 

8   decision_spill: nat → decision 

9   decision_colour: Register → decision. 

10  

11  definition is_member ≝ 

12  λvertex. 

13  λregister_lattice. 

14  let 〈l, r〉 ≝ register_lattice in 

15  match vertex with 

16  [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l 

17   inr v ⇒ set_member ? eq_Register v r 

18  ]. 

19  

20  (* prop_colouring is the non interferece 

21  prop_colouring 2 and 3 together say that spilled_no is the number of spilled 

22  registers *) 

23  (* Wilmer: the generation of the destruct principle diverges; 

24  CtrC make the file pass *) 

25  record coloured_graph (v: valuation): Type[1] ≝ 

26  { colouring: vertex → decision 

27  ; spilled_no: nat 

28  ; prop_colouring: ∀l. ∀v1, v2: vertex. 

29  is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2 

30  ; prop_colouring2: 

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

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  axiom build: ∀valuation. coloured_graph valuation. 

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