Changeset 735 for src/ERTL/ERTL.ma


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

Changes from today

File:
1 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.
Note: See TracChangeset for help on using the changeset viewer.