Ignore:
Timestamp:
Nov 22, 2012, 6:40:31 PM (8 years ago)
Author:
piccolo
Message:

fixed Traces and semantics
added commutation record (not yet finished) and proofs in lineariseProof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2481 r2484  
    170170  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
    171171  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
    172   ; fetch_ra: state st_pars → res (program_counter × (state st_pars))
    173 
    174   ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
     172
     173  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
    175174  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    176   ; save_frame: program_counter → call_dest uns_pars → state st_pars → res (state st_pars)
     175  ; save_frame: call_dest uns_pars → state_pc st_pars → res (state st_pars)
    177176   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    178177     type of arguments. To be fixed using a dependent type *)
     
    187186  (* from now on, parameters that use the type of functions *)
    188187  ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
    189   (* change of pc must be left to *_flow execution *)
    190188  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
    191189    (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in (state st_pars)
    192190  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
    193     (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
     191    (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state_pc st_pars)
    194192  }.
    195193
    196 (*coercion msu_pars_to_ss_pars nocomposites :
    197 ∀p,F.∀msup : more_sem_unserialized_params p F.sem_state_params
    198  ≝ st_pars
    199 on _msup : more_sem_unserialized_params ?? to sem_state_params.*)
    200 
     194definition allocate_locals :
     195  ∀p,F.∀sup : sem_unserialized_params p F.
     196  list (localsT p) → state sup → state sup ≝
     197  λp,F,sup,l,st.
     198  let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in
     199  set_regs … r st.
    201200
    202201definition helper_def_retrieve :
     
    382381*)
    383382
    384 definition next : ∀p : sem_params.succ p → state p → program_counter → state_pc p ≝
    385  λp,l,st,pc.
    386  let newpc ≝ succ_pc ? p … pc l in
     383definition next : ∀p : sem_params.succ p → state_pc p → state_pc p ≝
     384 λp,l,st.
     385 let newpc ≝ succ_pc ? p … (pc … st) l in
    387386 mk_state_pc … st newpc.
    388387
     
    426425let stack_size ≝ stack_sizes … ge i in
    427426! st' ← setup_call … stack_size (joint_if_params … fn) args st ;
    428 let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
    429 return set_regs p regs st.
     427return allocate_locals … p (joint_if_locals … fn) st.
    430428
    431429definition eval_seq_no_pc :
    432430 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) →
    433   state p → program_counter → joint_seq p globals →
     431  state p → joint_seq p globals →
    434432  IO io_out io_in (state p) ≝
    435  λp,globals,ge,curr_fn,st,next,seq.
     433 λp,globals,ge,curr_fn,st,seq.
    436434 match seq return λx.IO ??? with
    437435  [ extension_seq c ⇒
     
    487485    match description_of_function … fn return λx.description_of_function … fn = x → ? with
    488486    [ Internal fd ⇒ λprf.
    489       ! st' ← save_frame … next dest st ;
    490       eval_internal_call_no_pc … ge «fn, ?» args st'  (* only pc changes *)
     487      eval_internal_call_no_pc … ge «fn, ?» args st  (* only pc changes *)
    491488    | External fd ⇒ λ_.eval_external_call … fd args dest st
    492489    ] (refl …)
     
    505502definition eval_seq_pc :
    506503 ∀p:sem_params.∀globals.∀ge:genv p globals.
    507   state p → program_counter → joint_seq p globals →
    508   res program_counter
    509   λp,globals,ge,st,next,s.
     504  state_pc p → ? → joint_seq p globals →
     505  res (state_pc p)
     506  λp,globals,ge,st,nxt,s.
    510507  match s with
    511508  [ CALL f args dest ⇒
    512509    ! fn ← function_of_call … ge st f;
    513510    match ? return λx.description_of_function … fn = x → ? with
    514     [ Internal _ ⇒ λprf.return eval_internal_call_pc … ge «fn, ?»
    515     | External _ ⇒ λ_.return next
     511    [ Internal _ ⇒ λprf.
     512      let pc ≝ eval_internal_call_pc … ge «fn, ?» in
     513      ! st' ← save_frame … dest st ;
     514      return mk_state_pc … st' pc
     515    | External _ ⇒ λ_.return next p nxt st
    516516    ] (refl …)
    517   | _ ⇒ return next
     517  | _ ⇒ return next p nxt st
    518518  ].
    519519@(description_of_internal_function … prf)
     
    528528  match s with
    529529  [ sequential s next ⇒
    530     let next_ptr ≝ succ_pc ? p (pc … st) next in
    531530    match s return λ_.IO ??? with
    532531    [ step_seq s ⇒
    533       ! st' ← eval_seq_no_pc … ge curr_fn st next_ptr s ;
    534       ! pc' ← eval_seq_pc … ge st next_ptr s ;
    535       return mk_state_pc … st' pc'
     532      ! st' ← eval_seq_no_pc … ge curr_fn st s ;
     533      let st'' ≝ mk_state_pc … st' (pc … st) in
     534      eval_seq_pc ?? ge st'' next s
    536535    | COND a l ⇒
    537536      ! v ← acca_retrieve … st a ;
     
    549548      ! pc' ← pc_of_label ? p ? ge (pc … st) l ;
    550549      return mk_state_pc … st pc'
    551     | RETURN ⇒
    552       ! st' ← pop_frame … curr_fn st ;
    553       ! 〈pc', st''〉 ← fetch_ra … p st' ;
    554       return mk_state_pc … st'' pc'
     550    | RETURN ⇒ pop_frame … curr_fn st
    555551    | TAILCALL _ f args ⇒
    556552      ! fn ← function_of_call … ge st f : IO ???;
     
    562558        let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in
    563559        ! st' ← eval_external_call ??? fd args curr_dest st ;
    564         ! st'' ← pop_frame … curr_fn st ;
    565         ! 〈pc', st'''〉 ← fetch_ra … p st'' ;
    566         return mk_state_pc … st''' pc'
     560        pop_frame … curr_fn st'
    567561      ] (refl …)
    568562    ]
     
    590584    match s' with
    591585    [ RETURN ⇒
    592       do 〈ra, st'〉 ← fetch_ra … st;
    593       if eq_program_counter ra exit then
     586      do st' ← pop_frame … ge f st;
     587      if eq_program_counter (pc … st') exit then
    594588       do vals ← read_result … ge (joint_if_result … fn) st' ;
    595589       Word_of_list_beval vals
Note: See TracChangeset for help on using the changeset viewer.