Changeset 2942 for src/ERTLptr/Interference.ma
- Timestamp:
- Mar 23, 2013, 1:37:22 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTLptr/Interference.ma
r2845 r2942 8 8 prop_colouring 2 and 3 together say that spilled_no is the number of spilled 9 9 registers *) 10 (* Wilmer: the generation of the destruct principle diverges; 11 Ctr-C make the file pass *) 12 record coloured_graph (after: valuation register_lattice): Type[1] ≝ 10 record coloured_graph (before: valuation register_lattice): Type[1] ≝ 13 11 { colouring: vertex → decision 14 12 ; spilled_no: nat 15 13 ; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 → 16 lives v1 ( after l) → lives v2 (afterl) → colouring v1 ≠ colouring v214 lives v1 (before l) → lives v2 (before l) → colouring v1 ≠ colouring v2 17 15 ; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *) 18 ∀v1:vertex. (∃l. bool_to_Prop (lives v1 ( afterl))) → ∀i. colouring v1 = decision_spill i → i < spilled_no16 ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (before l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no 19 17 }. 20 18 21 19 definition coloured_graph_computer ≝ 22 20 ∀globals. 23 joint_internal_function ERTLptr globals →24 ∀ valuation.25 coloured_graph valuation.21 ∀fn:joint_internal_function ERTLptr globals. 22 ∀liveafter. 23 coloured_graph (livebefore globals fn liveafter).
Note: See TracChangeset
for help on using the changeset viewer.