Ignore:
Timestamp:
May 6, 2011, 11:45:27 AM (9 years ago)
Author:
campbell
Message:

Update experimental version of Cminor semantics.

Location:
Deliverables/D3.3/Cminor-experiment
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/Cminor-experiment/semantics.ma

    r755 r787  
    139139].
    140140
     141definition init_locals : env → list ident → env ≝
     142foldr ?? (λid,en. add ?? en id Vundef).
     143
    141144definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
    142145λge,st.
     
    154157    | St_assign id e n ⇒ λk.
    155158        ! 〈tr,v〉 ← eval_expr ge e en sp m;
    156         ret ? 〈tr, State f n (St_skip ?) (add ?? en id v) m sp k〉
     159        ! en' ← update ?? en id v;
     160        ret ? 〈tr, State f n (St_skip ?) en' m sp k〉
    157161    | St_store chunk edst e n ⇒ λk.
    158162        ! 〈tr,vdst〉 ← eval_expr ge edst en sp m;
     
    215219        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
    216220        ! en ← bind_params args (f_params f);
    217         ret ? 〈E0, State f O (f_body f) en m' sp k〉
     221        ret ? 〈E0, State f O (f_body f) (init_locals en (f_vars f)) m' sp k〉
    218222    | External fn ⇒
    219223        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
     
    228232                [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? ]
    229233                | Some v ⇒ match dst with [ None ⇒ Error ?
    230                                           | Some id ⇒ OK ? (add ?? en id v) ]
     234                                          | Some id ⇒ update ?? en id v ]
    231235                ];
    232236        ret ? 〈E0, State f n (St_skip ?) en' m sp k'〉
  • Deliverables/D3.3/Cminor-experiment/syntax.ma

Note: See TracChangeset for help on using the changeset viewer.