Changeset 1045 for src/RTLabs/syntax.ma

Timestamp:

Jun 29, 2011, 10:47:39 AM (10 years ago)

Author:

mulligan

Message:

resolved conflict in rtlabs

File:

• src/RTLabs/syntax.ma (modified) (1 diff)

src/RTLabs/syntax.ma

@@ -10 +10 @@
 include "common/Graphs.ma".
 
-(* Statements, including the label of successor(s). *)
+definition immediate : Type[0] ≝ Byte.
+
+(* Addressing modes *)
+
+inductive addressing : Type[0] ≝
+(* dpm: changed from int to Byte *)
+| Aindexed  : immediate → addressing         (* r1 + offset *)
+| Aindexed2 : addressing                     (* r1 + r2 *)
+| Aglobal   : ident → immediate → addressing (* global + offset *)
+| Abased    : ident → immediate → addressing (* global + offset + r1 *)
+| Ainstack  : immediate → addressing         (* stack + offset *)
+.
+
+definition addr_mode_args : addressing → nat ≝
+λa. match a with
+[ Aindexed _  ⇒ 1
+| Aindexed2   ⇒ 2
+| Aglobal _ _ ⇒ 0
+| Abased _ _  ⇒ 1
+| Ainstack _  ⇒ 0
+].
+
+definition addr ≝ λm.Vector register (addr_mode_args m).
 
 inductive statement : Type[0] ≝