Changeset 1051 for src/RTLabs
- Timestamp:
- Jul 4, 2011, 1:49:31 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/syntax.ma
r1046 r1051 9 9 include "ASM/Vector.ma". 10 10 include "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 with27 [ Aindexed _ ⇒ 128 | Aindexed2 ⇒ 229 | Aglobal _ _ ⇒ 030 | Abased _ _ ⇒ 131 | Ainstack _ ⇒ 032 ].33 34 definition addr ≝ λm.Vector register (addr_mode_args m).35 11 36 12 inductive statement : Type[0] ≝
Note: See TracChangeset
for help on using the changeset viewer.