Changeset 1045 for src/RTLabs/syntax.ma
- Timestamp:
- Jun 29, 2011, 10:47:39 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/syntax.ma
r888 r1045 10 10 include "common/Graphs.ma". 11 11 12 (* Statements, including the label of successor(s). *) 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). 13 35 14 36 inductive statement : Type[0] ≝
Note: See TracChangeset
for help on using the changeset viewer.