Ignore:
Timestamp:
Mar 23, 2013, 1:37:22 AM (7 years ago)
Author:
sacerdot
Message:

Many changes:

  1. Coloured graphs are now specified in terms of livebefore
  2. Type of livebefore changed so that it is now a valuation transformer
  3. Several axioms can now be inhabited in ERTLptrToLTLProof

Problems:
ERTLtoERTLptrOK is broken beyond my understanding. This pass should have
been unaffected by the changes, but it is not so. Why?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/Interference.ma

    r2845 r2942  
    88   prop_colouring 2 and 3 together say that spilled_no is the number of spilled
    99   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] ≝
     10record coloured_graph (before: valuation register_lattice): Type[1] ≝
    1311{ colouring: vertex → decision
    1412; spilled_no: nat
    1513; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 →
    16   lives v1 (after l) → lives v2 (after l) → colouring v1 ≠ colouring v2
     14  lives v1 (before l) → lives v2 (before l) → colouring v1 ≠ colouring v2
    1715; 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 (after l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no
     16   ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (before l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no
    1917}.
    2018
    2119definition coloured_graph_computer ≝
    2220 ∀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.