Changeset 1369 for src/RTLabs/syntax.ma


Ignore:
Timestamp:
Oct 14, 2011, 10:56:45 AM (8 years ago)
Author:
campbell
Message:

Put type information into front-end unary ops.
Slight change to semantics: booleans produced by Onotbool can be any given
integer size.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/syntax.ma

    r1316 r1369  
    1313| St_cost : costlabel → label → statement
    1414| St_const : register → constant → label → statement
    15 | St_op1 : unary_operation → register → register → label → statement (* destination source *)
     15| St_op1 : ∀t,t'. unary_operation t t' → register → register → label → statement (* destination source *)
    1616| St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
    1717| St_load : memory_chunk → register → register → label → statement
     
    3131| St_cost _ l ⇒ P l
    3232| St_const _ _ l ⇒ P l
    33 | St_op1 _ _ _ l ⇒ P l
     33| St_op1 _ _ _ _ _ l ⇒ P l
    3434| St_op2 _ _ _ _ l ⇒ P l
    3535| St_load _ _ _ l ⇒ P l
Note: See TracChangeset for help on using the changeset viewer.