Changeset 887 for src/RTLabs/syntax.ma


Ignore:
Timestamp:
Jun 6, 2011, 3:55:23 PM (9 years ago)
Author:
campbell
Message:

Start bringing RTLabs into line with the prototype compiler:

  • a coarse-grained type is associated with every register
  • the special addressing modes have been removed
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/syntax.ma

    r878 r887  
    1010include "common/Graphs.ma".
    1111
    12 (* XXX: ASTish stuff *)
    13 
    14 definition immediate : Type[0] ≝ int.
    15 
    16 (* Addressing modes *)
    17 
    18 inductive addressing : Type[0] ≝
    19 | Aindexed  : immediate → addressing         (* r1 + offset *)
    20 | Aindexed2 : addressing                     (* r1 + r2 *)
    21 | Aglobal   : ident → immediate → addressing (* global + offset *)
    22 | Abased    : ident → immediate → addressing (* global + offset + r1 *)
    23 | Ainstack  : immediate → addressing         (* stack + offset *)
    24 .
    25 
    26 definition addr_mode_args : addressing → nat ≝
    27 λa. match a with
    28 [ Aindexed _  ⇒ 1
    29 | Aindexed2   ⇒ 2
    30 | Aglobal _ _ ⇒ 0
    31 | Abased _ _  ⇒ 1
    32 | Ainstack _  ⇒ 0
    33 ].
    34 
    35 definition addr ≝ λm.Vector register (addr_mode_args m).
    36 
    3712(* Statements, including the label of successor(s). *)
    3813
     
    4318| St_op1 : unary_operation → register → register → label → statement
    4419| St_op2 : binary_operation → register → register → register → label → statement
    45 | St_load : memory_chunk → ∀m:addressing. addr m → register → label → statement
    46 | St_store : memory_chunk → ∀m:addressing. addr m → register → label → statement
     20| St_load : memory_chunk → register → register → label → statement
     21| St_store : memory_chunk → register → register → label → statement
    4722| St_call_id : ident → list register → option register → label → statement
    4823| St_call_ptr : register → list register → option register → label → statement
     
    6035{ f_labgen    : universe LabelTag
    6136; f_reggen    : universe RegisterTag
    62 ; f_sig       : signature
    63 ; f_result    : option register
    64 ; f_params    : list register
    65 ; f_locals    : list register
    66 ; f_ptrs      : list register
     37; f_result    : option (register × typ)
     38; f_params    : list (register × typ)
     39; f_locals    : list (register × typ)
    6740; f_stacksize : nat
    6841; f_graph     : graph statement
Note: See TracChangeset for help on using the changeset viewer.