Changeset 751


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

Initial version of the Cminor syntax and semantics.

Location:
src
Files:
7 added
3 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
  • src/common/SmallstepExec.ma

    r731 r751  
    2121| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
    2222         repeat n' ?? exec g s1
     23].
     24
     25let rec trace_map (A,B:Type[0]) (f:A → res (trace × B))
     26                  (l:list A) on l : res (trace × (list B)) ≝
     27match l with
     28[ nil ⇒ OK ? 〈E0, [ ]〉
     29| cons h t ⇒
     30    do 〈tr,h'〉 ← f h;
     31    do 〈tr',t'〉 ← trace_map … f t;
     32    OK ? 〈tr ⧺ tr',h'::t'〉
    2333].
    2434
  • src/common/Values.ma

    r747 r751  
    265265  | bool_of_val_null:
    266266      ∀r. bool_of_val (Vnull r) true.
     267
     268definition eval_bool_of_val : val → res bool ≝
     269λv. match v with
     270[ Vint i ⇒ OK ? (notb (eq i zero))
     271| Vnull _ ⇒ OK ? false
     272| Vptr _ _ _ _ ⇒ OK ? true
     273| _ ⇒ Error ?
     274].
    267275
    268276definition neg : val → val ≝ λv.
Note: See TracChangeset for help on using the changeset viewer.