Changeset 751 for src/RTLabs


Ignore:
Timestamp:
Apr 13, 2011, 6:52:10 PM (9 years ago)
Author:
campbell
Message:

Initial version of the Cminor syntax and semantics.

File:
1 edited

Legend:

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

    r750 r751  
    22(* XXX NB: I haven't checked all of these semantics against the prototype
    33           compilers yet! *)
    4 
    5 include "RTLabs/RTLabs-syntax.ma".
    64
    75include "common/Errors.ma".
     
    97include "common/IO.ma".
    108include "common/SmallstepExec.ma".
     9
     10include "RTLabs/RTLabs-syntax.ma".
    1111
    1212definition genv ≝ (genv_t Genv) (fundef internal_function).
     
    8787. /2/ [ 1,2: cases loc | cases (sp f) ] // qed.
    8888
    89 definition is_true_val : val → res bool ≝
    90 λv. match v with
    91 [ Vint i ⇒ OK ? (notb (eq i zero))
    92 | Vnull _ ⇒ OK ? false
    93 | Vptr _ _ _ _ ⇒ OK ? true
    94 | _ ⇒ Error ?
    95 ].
    96 
    9789
    9890(* XXX put somewhere sensible *)
     
    160152  | St_condcst cst ltrue lfalse ⇒
    161153      ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
    162       ! b ← is_true_val v;
     154      ! b ← eval_bool_of_val v;
    163155      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    164156  | St_cond1 op src ltrue lfalse ⇒
    165157      ! v ← reg_retrieve (locals f) src;
    166158      ! v' ← opt_to_res … (eval_unop op v);
    167       ! b ← is_true_val v';
     159      ! b ← eval_bool_of_val v';
    168160      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    169161  | St_cond2 op src1 src2 ltrue lfalse ⇒
     
    171163      ! v2 ← reg_retrieve (locals f) src2;
    172164      ! v' ← opt_to_res … (eval_binop op v1 v2);
    173       ! b ← is_true_val v';
     165      ! b ← eval_bool_of_val v';
    174166      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    175167
Note: See TracChangeset for help on using the changeset viewer.