Changeset 1045 for src/RTLabs/syntax.ma


Ignore:
Timestamp:
Jun 29, 2011, 10:47:39 AM (8 years ago)
Author:
mulligan
Message:

resolved conflict in rtlabs

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/syntax.ma

    r888 r1045  
    1010include "common/Graphs.ma".
    1111
    12 (* Statements, including the label of successor(s). *)
     12definition immediate : Type[0] ≝ Byte.
     13
     14(* Addressing modes *)
     15
     16inductive 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
     25definition 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
     34definition addr ≝ λm.Vector register (addr_mode_args m).
    1335
    1436inductive statement : Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.