Ignore:
Timestamp:
Dec 4, 2012, 6:16:25 PM (7 years ago)
Author:
tranquil
Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2491 r2529  
    1616{ ge :> genv_t (fundef (F globals))
    1717; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ?
    18 ; stack_sizes : (Σi.is_internal_function ? ge i) →
     18; stack_sizes : ident → option
    1919}.
    20 
    21 definition stack_sizes_lift :
    22 ∀pars_in, pars_out : params.
    23 ∀trans : ∀globals.joint_closed_internal_function pars_in globals →
    24                   joint_closed_internal_function pars_out globals.
    25 ∀prog_in : program (joint_function pars_in) ℕ.
    26 let prog_out ≝
    27   transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
    28 ((Σi.is_internal_function_of_program … prog_out i) → ℕ) →
    29 ((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝
    30 λpars_in,pars_out,prog_in,trans,stack_sizes.
    31 λi.stack_sizes «i, if_propagate … (pi2 … i)».
    3220
    3321definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
     
    122110*)
    123111
    124 (* bevals hold a function pointer (BVptr) *)
    125 definition funct_of_bevals : ∀F,ge.
    126   beval → beval → option (Σi.is_function F ge i) ≝
    127 λF,ge,dpl,dph.
    128 ! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ;
    129 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ (* ← check this condition in front end *)
    130    match ptype ptr with [ Code ⇒ true | _ ⇒ false] then (* ← already checked in funct_of_block? *)
    131    funct_of_block … (pblock ptr)
    132 else None ?.
    133 
    134112axiom ProgramCounterOutOfCode : String.
    135113axiom PointNotFound : String.
     
    144122definition fetch_function:
    145123 ∀F.
     124 ∀ge : genv_t F.
     125  (Σb.block_region b = Code) →
     126  res (ident×F) ≝
     127 λF,ge,bl.
     128 opt_to_res … [MSG BadFunction]
     129  (! id ← symbol_for_block … ge bl ;
     130   ! fd ← find_funct_ptr … ge bl ;
     131   return 〈id, fd〉).
     132
     133definition fetch_internal_function :
     134 ∀F.
    146135 ∀ge : genv_t (fundef F).
    147   program_counter →
    148   res (Σi.is_internal_function … ge i) ≝
    149  λpars,ge,p.
    150  opt_to_res … [MSG BadFunction; MSG BadPointer]
    151     (int_funct_of_block … ge (pc_block p)).
     136  (Σb.block_region b = Code) →
     137  res (ident×F) ≝
     138 λF,ge,bl.
     139 ! 〈id, fd〉 ← fetch_function … ge bl ;
     140 match fd with
     141 [ Internal ifd ⇒ return 〈id, ifd〉
     142 | _ ⇒ Error … [MSG BadFunction]
     143 ].
    152144
    153145record sem_unserialized_params
     
    171163  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
    172164
     165  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    173166  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
    174   (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    175167  ; save_frame: call_dest uns_pars → state_pc st_pars → res (state st_pars)
    176168   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
     
    187179  ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
    188180  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
    189     (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in (state st_pars)
     181    ident → F globals (* current *) → state st_pars → res (state st_pars)
    190182  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
    191     (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state_pc st_pars)
     183    ident → F globals (* current *) → state st_pars → res (state_pc st_pars)
    192184  }.
    193185
     
    241233 return 〈bv, set_istack … is st〉.
    242234
    243 definition save_ra : ∀p. state p → program_counter → res (state p) ≝
     235definition push_ra : ∀p. state p → program_counter → res (state p) ≝
    244236 λp,st,l.
    245237  let 〈addrl,addrh〉 ≝  beval_pair_of_pc l in
     
    247239  push … st' addrh.
    248240
    249 definition load_ra : ∀p.state p → res (program_counter × (state p)) ≝
     241definition pop_ra : ∀p.state p → res (program_counter × (state p)) ≝
    250242 λp,st.
    251243  ! 〈addrh, st'〉 ← pop … st;
     
    255247
    256248(* parameters that are defined by serialization *)
    257 record more_sem_params (pp : params) : Type[1] ≝
    258   { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp)
    259   ; offset_of_point : code_point pp → Pos
    260   ; point_of_offset : Pos → code_point pp
     249record sem_params : Type[1] ≝
     250  { spp :> params
     251  ; msu_pars :> sem_unserialized_params spp (joint_closed_internal_function spp)
     252  ; offset_of_point : code_point spp → Pos
     253  ; point_of_offset : Pos → code_point spp
    261254  ; point_of_offset_of_point :
    262255    ∀pt.point_of_offset (offset_of_point pt) = pt
     
    278271ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
    279272
    280 definition pc_of_point : ∀p.more_sem_params p
    281   program_counter → code_point p → program_counter ≝
    282   λp,msp,ptr,pt.
    283   mk_program_counter (pc_block ptr) (offset_of_point ? msp pt).
     273definition pc_of_point : ∀p:sem_params.(Σb.block_region b = Code)
     274  code_point p → program_counter ≝
     275  λp,bl,pt.
     276  mk_program_counter bl (offset_of_point p pt).
    284277
    285278definition point_of_pc :
    286   ∀p.more_sem_params p → program_counter → code_point p ≝
    287   λp,msp,ptr.point_of_offset p msp (pc_offset ptr).
    288 
    289 lemma point_of_pointer_of_point :
    290   ∀p,msp.∀ptr,pt.
    291   point_of_pc ? msp (pc_of_point p msp ptr pt) = pt.
    292 #p #msp #ptr #pt normalize // qed.
    293 
    294 lemma pointer_of_point_block :
    295   ∀p,msp,ptr,pt.
    296   pc_block (pc_of_point p msp ptr pt) = pc_block ptr.
    297 #p #msp #ptr #pt % qed. (* can probably do without *)
    298 
    299 lemma pointer_of_point_uses_block :
    300   ∀p,msp.∀ptr1,ptr2.∀pt.pc_block ptr1 = pc_block ptr2 →
    301     pc_of_point p msp ptr1 pt = pc_of_point p msp ptr2 pt.
    302 #p #msp #ptr1 #ptr2 #pc #EQ normalize >EQ % qed.
    303 
    304 lemma pointer_of_point_of_pointer :
    305   ∀p,msp.∀ptr1,ptr2.
    306     pc_block ptr1 = pc_block ptr2 →
    307     pc_of_point p msp ptr1 (point_of_pc p msp ptr2) = ptr2.
    308 #p #msp #ptr1 * #bl2 #o2 #EQ normalize >offset_of_point_of_offset >EQ % qed.
    309 
    310 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
     279  ∀p:sem_params.program_counter → code_point p ≝
     280  λp,ptr.point_of_offset p (pc_offset ptr).
     281
     282lemma point_of_pc_of_point :
     283  ∀p,bl,pt.
     284  point_of_pc p (pc_of_point p bl pt) = pt.
     285#p #bl #pt normalize // qed.
     286
     287lemma pc_of_point_of_pc :
     288  ∀p,ptr.
     289    pc_of_point p (pc_block ptr) (point_of_pc p ptr) = ptr.
     290#p * #bl #off normalize >offset_of_point_of_offset % qed.
     291
     292definition fetch_statement: ∀p : sem_params.∀globals.
    311293  ∀ge : genv_t (joint_function p globals). program_counter →
    312   res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝
    313   λp,msp,globals,ge,ptr.
    314   ! f ← fetch_function … ge ptr ;
    315   let fn ≝ if_of_function … f in
    316   let pt ≝ point_of_pc ? msp ptr in
     294  res (ident × (joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
     295  λp,globals,ge,ptr.
     296  ! 〈id, fn〉 ← fetch_internal_function … ge (pc_block ptr) ;
     297  let pt ≝ point_of_pc p ptr in
    317298  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
    318   return 〈f, stmt〉.
    319 
    320 definition pc_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
    321   genv_t (joint_function p globals) → program_counter → label → res program_counter ≝
    322   λp,msp,globals,ge,ptr,lbl.
    323   ! f ← fetch_function … ge ptr ;
    324   let fn ≝ if_of_function …  ge f in
     299  return 〈id, fn, stmt〉.
     300
     301definition pc_of_label : ∀p : sem_params.∀globals.
     302  genv_t (joint_function p globals) → (Σb.block_region b = Code) → label → res program_counter ≝
     303  λp,globals,ge,bl,lbl.
     304  ! 〈i, fn〉 ← fetch_internal_function … ge bl ;
    325305  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
    326306            (point_of_label … (joint_if_code … fn) lbl) ;
    327   return pc_of_point p msp ptr pt.
    328 
    329 definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
     307  return mk_program_counter bl (offset_of_point p pt).
     308
     309definition succ_pc : ∀p : sem_params.
    330310  program_counter → succ p → program_counter ≝
    331   λp,msp,ptr,nxt.
    332   let curr ≝ point_of_pc p msp ptr in
    333   pc_of_point p msp ptr (point_of_succ p curr nxt).
    334 
     311  λp,ptr,nxt.
     312  let curr ≝ point_of_pc p ptr in
     313  pc_of_point p (pc_block ptr) (point_of_succ p curr nxt).
     314
     315(*
    335316record sem_params : Type[1] ≝
    336317  { spp :> params
    337318  ; more_sem_pars :> more_sem_params spp
    338319  }.
    339 
     320*)
    340321(* definition msu_pars_of_s_pars :
    341322∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
     
    371352
    372353definition goto: ∀p : sem_params.∀globals.
    373   genv_t (joint_function p globals) → label → state p → program_counter → res (state_pc p) ≝
    374  λp,globals,ge,l,st,b.
    375   ! newpc ← pc_of_label ? p … ge b l ;
    376   return mk_state_pc ? st newpc.
     354  genv_t (joint_function p globals) → label → state_pc p → res (state_pc p) ≝
     355 λp,globals,ge,l,st.
     356  ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ;
     357  return mk_state_pc st newpc.
    377358
    378359(*
     
    383364definition next : ∀p : sem_params.succ p → state_pc p → state_pc p ≝
    384365 λp,l,st.
    385  let newpc ≝ succ_pc ? p … (pc … st) l in
     366 let newpc ≝ succ_pc … (pc … st) l in
    386367 mk_state_pc … st newpc.
    387368
    388 
    389 definition function_of_call ≝ λp:sem_params.λglobals.
     369definition code_block_of_block : block → option (Σb.block_region b = Code) ≝
     370λbl.match block_region bl
     371  return λx.block_region bl = x → option (Σb.block_region b = Code) with
     372  [ Code ⇒ λprf.Some ? «bl, prf»
     373  | XData ⇒ λ_.None ?
     374  ] (refl …).
     375
     376definition block_of_call ≝ λp:sem_params.λglobals.
    390377  λge: genv_t (joint_function p globals).λst : state p.λf.
    391   match f with
    392   [ inl id ⇒
    393     opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id)
    394   | inr addr ⇒
    395     ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
    396     ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
    397     opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h)
    398   ].
     378  ! bl ← match f with
     379    [ inl id ⇒ opt_to_res … [MSG BadFunction; CTX … id] (find_symbol … ge id)
     380    | inr addr ⇒
     381      ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
     382      ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
     383      ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
     384      if eq_bv … (bv_zero …) (offv (poff ptr)) then
     385        return (pblock … ptr)
     386      else
     387        Error … [MSG BadFunction; MSG BadPointer]
     388    ] ;
     389  opt_to_res … [MSG BadFunction; MSG BadPointer] (code_block_of_block bl).
    399390
    400391(* Paolo: why external calls do not need args?? *)
    401392definition eval_external_call ≝
    402 λp,F.λp' : sem_unserialized_params p F.λfn,args,dest,st.
    403       ! params ← fetch_external_args … p' fn st args : IO ???;
     393λp : sem_params.λfn,args,dest,st.
     394      ! params ← fetch_external_args … p fn st args : IO ???;
    404395      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    405396      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     
    408399         fixed once we fully implement external functions. *)
    409400      let vs ≝ [mk_val ? evres] in
    410       set_result … p' vs dest st.
    411 
    412 definition eval_internal_call_pc ≝
    413 λp : sem_params.λglobals : list ident.λge : genv_t (joint_function p globals).λi.
    414 let fn ≝ if_of_function … ge i in
    415 let l' ≝ joint_if_entry ?? fn in
    416 mk_program_counter (block_of_funct … ge (pi1 … i)) (offset_of_point ? p … l').
    417 [ @block_of_funct_ident_is_code
    418 | cases i /2 by internal_function_is_function/
    419 ]
    420 qed.
     401      set_result … p vs dest st.
     402
     403axiom MissingStackSize : String.
    421404
    422405definition eval_internal_call_no_pc ≝
    423 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st.
    424 let fn ≝ if_of_function … ge i in
    425 let stack_size ≝ stack_sizes … ge i in
    426 ! st' ← setup_call … stack_size (joint_if_params … fn) args st ;
     406λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args,st.
     407! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
     408! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
    427409return allocate_locals … p (joint_if_locals … fn) st.
    428410
     411axiom NoSuccessor : String.
     412definition next_of_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) →
     413  program_counter → res (succ p) ≝
     414λp,globals,ge,pc.
     415  ! 〈id_fn, stmt〉 ← fetch_statement … ge pc ;
     416  match stmt with
     417  [ sequential _ nxt ⇒ return nxt
     418  | _ ⇒ Error … [MSG NoSuccessor]
     419  ].
     420
    429421definition eval_seq_no_pc :
    430  ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) →
    431   state p → joint_seq p globals →
    432   IO io_out io_in (state p) ≝
    433  λp,globals,ge,curr_fn,st,seq.
    434  match seq return λx.IO ??? with
     422 ∀p:sem_params.∀globals.∀ge:genv p globals.ident →
     423 joint_closed_internal_function p globals →
     424  joint_seq p globals → state p →
     425  res (state p) ≝
     426 λp,globals,ge,curr_id,curr_fn,seq,st.
     427 match seq with
    435428  [ extension_seq c ⇒
    436     eval_ext_seq … ge c curr_fn st
     429    eval_ext_seq … ge c curr_id curr_fn st
    437430  | LOAD dst addrl addrh ⇒
    438431    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    481474  | MOVE dst_src ⇒
    482475    pair_reg_move … st dst_src
    483   | CALL f args dest ⇒
    484     ! fn ← function_of_call … ge st f : IO ???;
    485     match description_of_function … fn return λx.description_of_function … fn = x → ? with
    486     [ Internal fd ⇒ λprf.
    487       eval_internal_call_no_pc … ge «fn, ?» args st  (* only pc changes *)
    488     | External fd ⇒ λ_.eval_external_call … fd args dest st
    489     ] (refl …)
    490   | _ ⇒ return st
     476  | _ ⇒ return st (* for calls do everything in eval_seq_advance *)
    491477  ].
    492 [ @hide_prf
     478  @hide_prf
    493479  @find_symbol_in_globals
    494480  lapply prf
     
    497483  [@eq_identifier_elim #H * >H %1 % ]
    498484  #G %2 @IH @G
    499 | @(description_of_internal_function … prf)
    500 ]
    501485qed.
    502486
    503 definition eval_seq_pc :
     487definition eval_seq_call ≝
     488λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
     489λst : state_pc p.
     490! bl ← block_of_call … ge st f : IO ???;
     491! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
     492match fd with
     493[ Internal ifd ⇒
     494  ! st' ← save_frame … dest st ;
     495  ! st'' ← eval_internal_call_no_pc p globals ge i ifd args st' ;
     496  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
     497  return mk_state_pc … st'' pc
     498| External efd ⇒
     499  ! st' ← eval_external_call … efd args dest st ;
     500  return mk_state_pc … st' (succ_pc p (pc … st) nxt)
     501].
     502
     503definition eval_seq_advance :
    504504 ∀p:sem_params.∀globals.∀ge:genv p globals.
    505   state_pc p → ? → joint_seq p globals
    506   res (state_pc p) ≝
    507   λp,globals,ge,st,nxt,s.
     505  joint_seq p globals → succ p → state_pc p
     506  IO io_out io_in (state_pc p) ≝
     507  λp,globals,ge,s,nxt,st.
    508508  match s with
    509509  [ CALL f args dest ⇒
    510     ! fn ← function_of_call … ge st f;
    511     match ? return λx.description_of_function … fn = x → ? with
    512     [ Internal _ ⇒ λprf.
    513       let pc ≝ eval_internal_call_pc … ge «fn, ?» in
    514       ! st' ← save_frame … dest st ;
    515       return mk_state_pc … st' pc
    516     | External _ ⇒ λ_.return next p nxt st
    517     ] (refl …)
    518   | _ ⇒ return next p nxt st
     510    eval_seq_call … ge f args dest nxt st
     511  | _ ⇒ return next … nxt st
    519512  ].
    520 @(description_of_internal_function … prf)
    521 qed.
    522 
    523 definition eval_statement :
     513
     514definition eval_statement_no_pc :
    524515 ∀p:sem_params.∀globals.∀ge:genv p globals.
    525  (Σi.is_internal_function … ge i) → state_pc p →
    526   ∀s:joint_statement p globals.
    527   IO io_out io_in (state_pc p) ≝
    528   λp,g,ge,curr_fn,st,s.
     516 ident → joint_closed_internal_function p globals (* current *) →
     517 joint_statement p globals → state p → res (state p) ≝
     518 λp,globals,ge,curr_id,curr_fn,s,st.
    529519  match s with
    530520  [ sequential s next ⇒
     521    match s with
     522    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id curr_fn s st
     523    | COND a l ⇒ return st
     524    ]
     525  | final s ⇒ return st
     526  ].
     527
     528definition eval_return ≝
     529λp : sem_params.λglobals : list ident.λge : genv p globals.
     530λcurr_id.λcurr_fn : joint_closed_internal_function ??.
     531λst : state p.
     532! st' ← pop_frame … ge curr_id curr_fn st ;
     533! nxt ← next_of_pc … ge (pc … st') ;
     534return next … nxt st' (* now address pushed on stack are calling ones! *).
     535
     536definition eval_tailcall ≝
     537λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f.
     538λcurr_fn : joint_closed_internal_function ??.
     539λst : state_pc p.
     540! bl ← block_of_call … ge st f : IO ???;
     541! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
     542match fd with
     543[ Internal ifd ⇒
     544  ! st' ← eval_internal_call_no_pc p globals ge i ifd args st ;
     545  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
     546  return mk_state_pc … st' pc
     547| External efd ⇒
     548  let curr_dest ≝ joint_if_result ?? curr_fn in
     549  ! st' ← eval_external_call … efd args curr_dest st ;
     550  eval_return … ge curr_f curr_fn st
     551].
     552
     553definition eval_statement_advance :
     554 ∀p:sem_params.∀globals.∀ge:genv p globals.
     555 ident → joint_closed_internal_function p globals →
     556  joint_statement p globals → state_pc p →
     557  IO io_out io_in (state_pc p) ≝
     558  λp,g,ge,curr_id,curr_fn,s,st.
     559  match s with
     560  [ sequential s nxt ⇒
    531561    match s return λ_.IO ??? with
    532562    [ step_seq s ⇒
    533       ! st' ← eval_seq_no_pc … ge curr_fn st s ;
    534       let st'' ≝ mk_state_pc … st' (pc … st) in
    535       eval_seq_pc ?? ge st'' next s
     563      eval_seq_advance … ge s nxt st
    536564    | COND a l ⇒
    537565      ! v ← acca_retrieve … st a ;
    538566      ! b ← bool_of_beval … v ;
    539       ! pc' ←
    540         if b then
    541           pc_of_label ? p … ge (pc … st) l
    542         else
    543           return succ_pc ? p (pc … st) next ;
    544       return mk_state_pc … st pc'
     567      if b then
     568        goto … ge l st
     569      else
     570        return next … nxt st
    545571    ]
    546572  | final s ⇒
    547573    match s with
    548     [ GOTO l ⇒
    549       ! pc' ← pc_of_label ? p ? ge (pc … st) l ;
    550       return mk_state_pc … st pc'
    551     | RETURN ⇒ pop_frame … curr_fn st
     574    [ GOTO l ⇒ goto … ge l st
     575    | RETURN ⇒ eval_return … ge curr_id curr_fn st
    552576    | TAILCALL _ f args ⇒
    553       ! fn ← function_of_call … ge st f : IO ???;
    554       match ? return λx.description_of_function … fn = x → ? with
    555       [ Internal _ ⇒ λprf.
    556         let pc' ≝ eval_internal_call_pc … ge «fn, ?» in
    557         return mk_state_pc … st pc'
    558       | External fd ⇒ λ_.
    559         let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in
    560         ! st' ← eval_external_call ??? fd args curr_dest st ;
    561         pop_frame … curr_fn st'
    562       ] (refl …)
     577      eval_tailcall … ge f args curr_id curr_fn st
    563578    ]
    564579  ].
    565 @(description_of_internal_function … prf)
    566 qed.
    567580
    568581definition eval_state : ∀p:sem_params. ∀globals: list ident.
     
    570583  state_pc p → IO io_out io_in (state_pc p) ≝
    571584  λp,globals,ge,st.
    572   ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
    573   eval_statement … ge fn st s.
     585  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
     586  ! st' ← eval_statement_no_pc … ge id fn s st : IO ???;
     587  let st'' ≝ mk_state_pc … st' (pc … st) in
     588  eval_statement_advance … ge id fn s st''.
    574589
    575590(* Paolo: what if in an intermediate language main finishes with an external
     
    579594  genv p globals → program_counter → state_pc p → option int ≝
    580595 λp,globals,ge,exit,st.res_to_opt ? (
    581   do 〈f,s〉 ← fetch_statement ? p … ge (pc … st);
    582   let fn ≝ if_of_function … f in
     596  do 〈id,fn,s〉 ← fetch_statement  … ge (pc … st);
    583597  match s with
    584598  [ final s' ⇒
    585599    match s' with
    586600    [ RETURN ⇒
    587       do st' ← pop_frame … ge f st;
    588       if eq_program_counter (pc … st') exit then
    589        do vals ← read_result … ge (joint_if_result … fn) st' ;
     601      do st' ← pop_frame … ge id fn st;
     602      ! nxt ← next_of_pc … ge (pc … st') ;
     603      let pc' ≝ succ_pc … (pc … st') nxt in
     604      if eq_program_counter pc' exit then
     605       do vals ← read_result … ge (joint_if_result … fn) st ;
    590606       Word_of_list_beval vals
    591607      else
Note: See TracChangeset for help on using the changeset viewer.