Changeset 1423 for src/ERTL/Interference.ma
 Timestamp:
 Oct 19, 2011, 6:05:50 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/Interference.ma
r1282 r1423 1 1 include "ERTL/ERTL.ma". 2 2 include "ERTL/liveness.ma". 3 include "basics/jmeq.ma". 3 4 4 5 definition vertex ≝ register ⊎ Register. … … 17 18 ]. 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 *) 19 25 record coloured_graph (v: valuation): Type[1] ≝ 20 { 21 colouring: vertex → decision; 22 prop_colouring: ∀l. ∀v1, v2: vertex. 23 is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2 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) 24 35 }. 25 36
Note: See TracChangeset
for help on using the changeset viewer.