Changeset 2590 for src/joint/Traces.ma


Ignore:
Timestamp:
Jan 24, 2013, 7:52:38 PM (8 years ago)
Author:
piccolo
Message:

added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc case in place in ERTLptr translation

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2562 r2590  
    4747λpars.
    4848let p ≝ prog pars in
     49let spars ≝ prog_spars pars in
     50let genv ≝ globalenv_noinit ? p in
     51let get_pc_lbl ≝ λid,lbl.
     52  ! bl ← block_of_funct_id … spars genv id ;
     53  pc_of_label … genv bl lbl in
    4954mk_evaluation_params
    5055  (prog_var_names … p)
    51   (prog_spars pars)
    52   (mk_genv_gen ?? (globalenv_noinit ? p) ? (stack_sizes pars))
     56  spars
     57  (mk_genv_gen ?? genv ? (stack_sizes pars) get_pc_lbl)
    5358 (* (prog_io pars) *).
    5459#s #H
     
    7984  (* use exit_pc as ra and call_dest_for_main as dest *)
    8085  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
    81   ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) st0' ;
     86  ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) (prog_main … p) st0' ;
    8287  let st0'' ≝ set_no_pc … st0_no_pc st0' in
    8388  ! bl ← block_of_call … ge (inl … main) st0'';
Note: See TracChangeset for help on using the changeset viewer.