Changeset 735


Ignore:
Timestamp:
Apr 1, 2011, 6:12:57 PM (9 years ago)
Author:
mulligan
Message:

Changes from today

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r733 r735  
    44include "common/Graphs.ma".
    55
    6 definition Registers ≝ list Register.
    7 
    86definition AbstractRegister ≝ nat.
     7definition AbstractRegisters ≝ list AbstractRegister.
    98
    109inductive ERTLStatement: Type[0] ≝
     
    3029  | ERTL_St_Load: AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    3130  | ERTL_St_Store: AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    32   | ERTL_St_Call_Id: Identifier → Byte → Identifier → ERTLStatement.
     31  | ERTL_St_Call_Id: Identifier → Byte → Identifier → ERTLStatement
     32  | ERTL_St_CondAcc: AbstractRegister → Identifier → Identifier → ERTLStatement
     33  | ERTL_St_Return: AbstractRegisters → ERTLStatement.
    3334
    3435definition ERTLStatementGraph ≝ graph ERTLStatement.
  • src/ERTL/Liveness.ma

    r733 r735  
    1010  [ ERTL_St_Return _ ⇒ set_empty ?
    1111  | ERTL_St_Skip l ⇒ set_singleton l
     12  | ERTL_St_Comment comment l ⇒ set_singleton l
     13  | ERTL_St_Cost cost l ⇒ set_singleton l
     14  | ERTL_St_Set_Hdw r1 r2 l ⇒ set_singleton l
     15  | ERTL_St_Get_Hdw r1 r2 l ⇒ set_singleton l
     16  | ERTL_St_Hdw_To_Hdw r1 r2 l ⇒ set_singleton l
     17  | ERTL_St_NewFrame l ⇒ set_singleton l
     18  | ERTL_St_DelFrame l ⇒ set_singleton l
     19  | ERTL_St_FrameSize r l ⇒ set_singleton l
     20  | ERTL_St_Push r l ⇒ set_singleton l
     21  | ERTL_St_Pop r l ⇒ set_singleton l
     22  | ERTL_St_AddrH r l1 l2 ⇒ set_singleton l2
     23  | ERTL_St_AddrL r l1 l2 ⇒ set_singleton l2
     24  | ERTL_St_Int r v l ⇒ set_singleton l
     25  | ERTL_St_Move r1 r2 l ⇒ set_singleton l
     26  | ERTL_St_Opaccs opaccs r1 r2 r3 l ⇒ set_singleton l
     27  | ERTL_St_Op2 op2 r1 r2 r3 l ⇒ set_singleton l
     28  | ERTL_St_Op1 op1 r1 r2 l ⇒ set_singleton l
     29  | ERTL_St_ClearCarry l ⇒ set_singleton l
     30  | ERTL_St_Load r1 r2 r3 l ⇒ set_singleton l
     31  | ERTL_St_Store r1 r2 r3 l ⇒ set_singleton l
     32  | ERTL_St_Call_Id id v l ⇒ set_singleton l
    1233  | ERTL_St_CondAcc _ l1 l2 ⇒ set_union ? (set_singleton l1) (set_singleton l2)
    1334  | _ ⇒ ?
    1435  ].
     36
     37definition set_of_list ≝
     38  λn: nat.
     39  λl: list (BitVector n).
     40    foldr ? ? (set_insert ?) (set_empty ?) l.
  • src/utilities/IdentifierTools.ma

    r699 r735  
    99axiom new_universe: Identifier → Universe.
    1010axiom fresh: Universe → Identifier.
    11 
Note: See TracChangeset for help on using the changeset viewer.