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/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
Note: See TracChangeset for help on using the changeset viewer.