Changeset 2590 for src/joint


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

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

Location:
src/joint
Files:
2 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'';
  • src/joint/semantics.ma

    r2570 r2590  
    1717; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ?
    1818; stack_sizes : ident → option ℕ
     19; get_pc_from_label : ident (* current function *) → label → res program_counter
    1920}.
    2021
     
    7576definition exit_pc : program_counter ≝
    7677  mk_program_counter «mk_block Code (-1), refl …» one.
     78
     79definition null_pc : program_counter ≝
     80    mk_program_counter «mk_block Code OZ, refl …» one.
    7781
    7882definition set_m: ∀p. bemem → state p → state p ≝
     
    194198  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    195199  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
    196   ; save_frame: call_kind → call_dest uns_pars → state_pc st_pars → res (state st_pars)
     200  ; save_frame: call_kind → call_dest uns_pars → ident → state_pc st_pars → res (state st_pars)
    197201   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    198202     type of arguments. To be fixed using a dependent type *)
     
    484488  ] (refl …).
    485489
    486 (* to be used in implementations *)
    487 definition block_of_call_id ≝  λF.λsp:sem_state_params.
    488   λge: genv_t F.λid.λst:state sp.
     490definition block_of_funct_id ≝  λF.λsp:sem_state_params.
     491  λge: genv_t F.λid.
    489492  opt_to_res … [MSG BadFunction; CTX … id] (
    490493    ! bl ← find_symbol … ge id;
     
    530533definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
    531534
     535
    532536definition eval_call ≝
    533537λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
     
    537541match fd with
    538542[ Internal ifd ⇒
    539   ! st' ← save_frame … (kind_of_call … f) dest st ;
     543  let ident ≝ ? in
     544  ! st' ← save_frame … (kind_of_call … f) dest ident st ;
    540545  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
    541546  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
     
    544549  ! st' ← eval_external_call … efd args dest st ;
    545550  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
    546 ].
     551]. cases daemon qed. (*TODO*)
    547552
    548553definition eval_statement_no_pc :
Note: See TracChangeset for help on using the changeset viewer.