Changeset 1051 for src/RTLabs


Ignore:
Timestamp:
Jul 4, 2011, 1:49:31 PM (10 years ago)
Author:
mulligan
Message:

removed superfluous addressing mode code from RTLabs/syntax.ma

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTLabs/syntax.ma

    r1046 r1051  
    99include "ASM/Vector.ma".
    1010include "common/Graphs.ma".
    11 
    12 definition immediate : Type[0] ≝ Byte.
    13 
    14 (* Addressing modes *)
    15 
    16 inductive addressing : Type[0] ≝
    17 (* dpm: changed from int to Byte *)
    18 | Aindexed  : immediate → addressing         (* r1 + offset *)
    19 | Aindexed2 : addressing                     (* r1 + r2 *)
    20 | Aglobal   : ident → immediate → addressing (* global + offset *)
    21 | Abased    : ident → immediate → addressing (* global + offset + r1 *)
    22 | Ainstack  : immediate → addressing         (* stack + offset *)
    23 .
    24 
    25 definition addr_mode_args : addressing → nat ≝
    26 λa. match a with
    27 [ Aindexed _  ⇒ 1
    28 | Aindexed2   ⇒ 2
    29 | Aglobal _ _ ⇒ 0
    30 | Abased _ _  ⇒ 1
    31 | Ainstack _  ⇒ 0
    32 ].
    33 
    34 definition addr ≝ λm.Vector register (addr_mode_args m).
    3511
    3612inductive statement : Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.