Changeset 1369 for src/RTLabs


Ignore:
Timestamp:
Oct 14, 2011, 10:56:45 AM (9 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.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1238 r1369  
    9898      ! locals ← reg_store r v (locals f);
    9999      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    100   | St_op1 op dst src l ⇒
     100  | St_op1 _ _ op dst src l ⇒
    101101      ! v ← reg_retrieve (locals f) src;
    102       ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
     102      ! v' ← opt_to_res … (msg FailedOp) (eval_unop ?? op v);
    103103      ! locals ← reg_store dst v' (locals f);
    104104      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
  • 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.