Changeset 2564 for src/joint


Ignore:
Timestamp:
Dec 19, 2012, 12:46:59 PM (7 years ago)
Author:
piccolo
Message:

ERTL fully repaired, useless part of return value of pop_ra
removed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2562 r2564  
    9898 λp,s,st. mk_state_pc … s (pc … st) (last_pop … st).
    9999
    100 definition set_last_pop: ∀p. ? → state_pc p → state_pc p ≝
    101  λp,s,st. mk_state_pc … (st_no_pc … st) (pc … st) s.
     100definition set_last_pop: ∀p. ? → state p × program_counter → state_pc p ≝
     101 λp,s,st. mk_state_pc … (\fst … st) (\snd … st) s.
    102102
    103103definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
     
    199199    ident → F globals (* current *) → state st_pars → res (state st_pars)
    200200  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
    201     ident → F globals (* current *) → state st_pars → res (state_pc st_pars)
     201    ident → F globals (* current *) → state st_pars → res (state st_pars × program_counter)
    202202  }.
    203203
     
    257257  push … st' addrh.
    258258
    259 definition pop_ra : ∀p.state p → res (program_counter × (state p)) ≝
     259definition pop_ra : ∀p.state p → res (state p × program_counter) ≝
    260260 λp,st.
    261261  ! 〈addrh, st'〉 ← pop … st;
    262262  ! 〈addrl, st''〉 ← pop … st';
    263263  ! pr ← pc_of_bevals [addrh; addrl];
    264   return 〈pr, st''〉.
     264  return 〈st'',pr〉.
    265265
    266266(* parameters that are defined by serialization *)
     
    553553λst : state p.
    554554! st' ← pop_frame … ge curr_id curr_fn st ;
    555 ! nxt ← next_of_call_pc … ge (pc … st') ;
     555! nxt ← next_of_call_pc … ge (\snd … st') ;
    556556return
    557   set_last_pop … (pc … st') (next … nxt st') (* now address pushed on stack are calling ones! *).
     557  next … nxt (set_last_pop … (\snd … st') st') (* now address pushed on stack are calling ones! *).
    558558
    559559definition eval_tailcall ≝
     
    631631    [ RETURN ⇒
    632632      do st' ← pop_frame … ge id fn st;
    633       if eq_program_counter (pc … st') exit then
     633      if eq_program_counter (\snd … st') exit then
    634634      do vals ← read_result … ge (joint_if_result … fn) st ;
    635635        Word_of_list_beval vals
Note: See TracChangeset for help on using the changeset viewer.