Ignore:
Timestamp:
Apr 12, 2011, 12:32:33 PM (9 years ago)
Author:
campbell
Message:

Track some of the changes to the prototype in RTLabs.

Just one register in each place now, f_ptrs is present but not checked.
The changes to memory quantities have been glossed over for now.
A new difference from the prototype: return registers are optional.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs-syntax.ma

    r747 r750  
    1313
    1414definition immediate : Type[0] ≝ int.
    15 definition registers ≝ Sig nat (Vector register).
    1615
    1716(* Addressing modes *)
     
    3433].
    3534
    36 definition addr ≝ λm.Vector registers (addr_mode_args m).
     35definition addr ≝ λm.Vector register (addr_mode_args m).
    3736
    3837(* Statements, including the label of successor(s). *)
     
    4140| St_skip : label → statement
    4241| St_cost : costlabel → label → statement
    43 | St_const : registers → constant → label → statement
    44 | St_op1 : unary_operation → registers → registers → label → statement
    45 | St_op2 : binary_operation → registers → registers → registers → label → statement
    46 | St_load : memory_chunk → ∀m:addressing. addr m → registers → label → statement
    47 | St_store : memory_chunk → ∀m:addressing. addr m → registers → label → statement
    48 | St_call_id : ident → list registers → registers → signature → label → statement
    49 | St_call_ptr : registers → list registers → registers → signature → label → statement
    50 | St_tailcall_id : ident → list registers → signature → statement
    51 | St_tailcall_ptr : registers → list registers → signature → statement
     42| St_const : register → constant → label → statement
     43| St_op1 : unary_operation → register → register → label → statement
     44| 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
     47| St_call_id : ident → list register → option register → signature → label → statement
     48| St_call_ptr : register → list register → option register → signature → label → statement
     49| St_tailcall_id : ident → list register → signature → statement
     50| St_tailcall_ptr : register → list register → signature → statement
    5251(* Um, what? *)
    5352| St_condcst : constant → label → label → statement
    54 | St_cond1 : unary_operation → registers → label → label → statement
    55 | St_cond2 : binary_operation → registers → registers → label → label → statement
    56 | St_jumptable : registers → list label → statement
    57 | St_return : registers → statement
     53| St_cond1 : unary_operation → register → label → label → statement
     54| St_cond2 : binary_operation → register → register → label → label → statement
     55| St_jumptable : register → list label → statement
     56| St_return : register → statement
    5857.
    5958
     
    6261; f_reggen    : universe RegisterTag
    6362; f_sig       : signature
    64 ; f_result    : registers
    65 ; f_params    : list registers
    66 ; f_locals    : list registers
     63; f_result    : option register
     64; f_params    : list register
     65; f_locals    : list register
     66; f_ptrs      : list register
    6767; f_stacksize : nat
    6868; f_graph     : graph statement
     
    7272(* XXX: matita interpretations bug workaround *)
    7373definition f_stacksize : internal_function → nat ≝
    74 λf.match f with [ mk_internal_function _ _ _ _ _ _ s _ _  _ ⇒ s ].
     74λf.match f with [ mk_internal_function _ _ _ _ _ _ _ s _ _  _ ⇒ s ].
    7575
    7676(* Global variables only need to be given their size at this stage of
     
    8484     return and jump tables?)
    8585   - seems like load and store ought to have types that control the size of the
    86      registers list based on the addressing mode; similarly, memory_chunk and
    87      registers are probably related.
     86     register list based on the addressing mode; similarly, memory_chunk and
     87     register are probably related.
    8888   - label and register generation really tell us something about the sets of
    89      labels and registers that may appear, perhaps it should be renamed, or the
     89     labels and register that may appear, perhaps it should be renamed, or the
    9090     graph made dependent on them to make it obvious, etc.
    9191 *)
Note: See TracChangeset for help on using the changeset viewer.