Changeset 745 for src


Ignore:
Timestamp:
Apr 8, 2011, 10:15:30 AM (10 years ago)
Author:
mulligan
Message:

Changes from yesterday. Slowly implementing the functorized imperative code from ERTL :(

Location:
src/ERTL
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed

  • src/ERTL/ERTL.ma

    r735 r745  
    44include "common/Graphs.ma".
    55
    6 definition AbstractRegister ≝ nat.
     6inductive AbstractRegister: Type[0] ≝
     7  mkAbstractRegister: Word → AbstractRegister.
     8
    79definition AbstractRegisters ≝ list AbstractRegister.
    810

  • src/ERTL/ERTLToLTL.ma

    r733 r745  
    11include "ERTL/ERTL.ma".
    2 
    3 inductive Decision: Type[0] ≝
    4   | Spill: Immediate → Decision
    5   | Colour: Register → Decision.
    62 

  • src/ERTL/Liveness.ma

    r735 r745  
    3232  | ERTL_St_Call_Id id v l ⇒ set_singleton l
    3333  | ERTL_St_CondAcc _ l1 l2 ⇒ set_union ? (set_singleton l1) (set_singleton l2)
    34   | _ ⇒ ?
    3534  ].
    3635
Note: See TracChangeset for help on using the changeset viewer.