Changeset 751 for src/common


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/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • 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.