Changeset 2878


Ignore:
Timestamp:
Mar 15, 2013, 11:32:51 AM (4 years ago)
Author:
tranquil
Message:

backtracked some changes that were not ready for commit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_semantics.ma

    r2876 r2878  
    5959 ; carry: bebit
    6060 ; regs: regsT semp
    61  ; stack_usage : ℕ
    6261 ; m: bemem
    6362 }.
     
    8079
    8180definition set_m: ∀p. bemem → state p → state p ≝
    82  λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st)
    83   (stack_usage … st) m.
     81 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m.
    8482
    8583definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
    86  λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs
    87   (stack_usage … st) (m … st).
     84 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st).
    8885
    8986definition set_sp: ∀p. ? → state p → state p ≝
    9087 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
    91  mk_state p (st_frms … st) (istack … st) (carry … st) regs' (stack_usage … st) (m … st).
     88 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).
    9289
    9390definition set_carry: ∀p. bebit → state p → state p ≝
    94  λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st)
    95  (stack_usage … st) (m … st).
     91 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st).
    9692
    9793definition set_istack: ∀p. internal_stack → state p → state p ≝
    98  λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st)
    99  (stack_usage … st)  (m … st).
     94 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st).
    10095
    10196definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     
    109104
    110105definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    111  λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st)
    112  (stack_usage … st) (m … st).
     106 λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st).
    113107
    114108(*
     
    519513      set_result … p vs dest st.
    520514
    521 definition increment_stack_usage : ∀p.ℕ → state p → state p ≝
    522 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st)
    523   (stack_usage … st + n) (m … st).
    524 
    525 definition decrement_stack_usage : ∀p.ℕ → state p → state p ≝
    526 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st)
    527   (stack_usage … st - n) (m … st).
    528 
    529515definition eval_internal_call ≝
    530516λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
    531517λst : state p.
    532518! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    533 ! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
    534 return increment_stack_usage … stack_size st'.
     519setup_call … stack_size (joint_if_params … globals fn) args st.
    535520
    536521definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
     
    571556λst : state p.
    572557! st' ← pop_frame … ge curr_id curr_ret st ;
    573 ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_id] (stack_sizes … ge curr_id) ;
    574 let st'' ≝ decrement_stack_usage … stack_size (\fst st') in
    575558! nxt ← next_of_call_pc … ge (\snd … st') ;
    576559return
    577   next … nxt (set_last_pop … (\snd … st') 〈st'', \snd st'〉) (* now address pushed on stack are calling ones! *).
     560  next … nxt (set_last_pop … (\snd … st') st') (* now address pushed on stack are calling ones! *).
    578561
    579562definition eval_tailcall ≝
     
    585568match fd with
    586569[ Internal ifd ⇒
    587   ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_f] (stack_sizes … ge curr_f) ;
    588   let st' ≝ decrement_stack_usage … stack_size st in
    589   ! st'' ← eval_internal_call p globals ge i ifd args st' ;
     570  ! st' ← eval_internal_call p globals ge i ifd args st ;
    590571  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
    591   return mk_state_pc … st'' pc (last_pop … st)
     572  return mk_state_pc … st' pc (last_pop … st)
    592573| External efd ⇒
    593574  ! st' ← eval_external_call … efd args curr_ret st ;
Note: See TracChangeset for help on using the changeset viewer.