Ignore:
Timestamp:
Mar 7, 2013, 12:10:42 PM (7 years ago)
Author:
tranquil
Message:
  • added global notation for existence in Type[1] (\exists[1] x.P)
  • in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
  • in joint_semantics, moved out and around some parameters in primitive semantics functions
  • fixed all back end semantics
  • added skeleton files for single passes correctness proofs
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_semantics.ma

    r2783 r2796  
    199199      state st_pars → res (list beval)
    200200  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
    201     ident → F globals (* current *) → state st_pars → res (state st_pars)
     201    ident (* current *) → state st_pars → res (state st_pars)
    202202  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
    203     ident → F globals (* current *) → state st_pars → res (state st_pars × program_counter)
     203    ident (* current *) → call_dest uns_pars (* current ret *) →
     204      state st_pars → res (state st_pars × program_counter)
    204205  }.
    205206
     
    407408definition eval_seq_no_pc :
    408409 ∀p:sem_params.∀globals.∀ge:genv p globals.ident →
    409  joint_closed_internal_function p globals →
    410410  joint_seq p globals → state p →
    411411  res (state p) ≝
    412  λp,globals,ge,curr_id,curr_fn,seq,st.
     412 λp,globals,ge,curr_id,seq,st.
    413413 match seq with
    414414  [ extension_seq c ⇒
    415     eval_ext_seq … ge c curr_id curr_fn st
     415    eval_ext_seq … ge c curr_id st
    416416  | LOAD dst addrl addrh ⇒
    417417    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    539539definition eval_statement_no_pc :
    540540 ∀p:sem_params.∀globals.∀ge:genv p globals.
    541  ident → joint_closed_internal_function p globals (* current *) →
     541 ident (* current *) →
    542542 joint_statement p globals → state p → res (state p) ≝
    543  λp,globals,ge,curr_id,curr_fn,s,st.
     543 λp,globals,ge,curr_id,s,st.
    544544  match s with
    545545  [ sequential s next ⇒
    546546    match s with
    547     [ step_seq s ⇒ eval_seq_no_pc … ge curr_id curr_fn s st
     547    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id s st
    548548    | _ ⇒ return st
    549549    ]
     
    553553definition eval_return ≝
    554554λp : sem_params.λglobals : list ident.λge : genv p globals.
    555 λcurr_id.λcurr_fn : joint_closed_internal_function ??.
     555λcurr_id.λcurr_ret : call_dest p.
    556556λst : state p.
    557 ! st' ← pop_frame … ge curr_id curr_fn st ;
     557! st' ← pop_frame … ge curr_id curr_ret st ;
    558558! nxt ← next_of_call_pc … ge (\snd … st') ;
    559559return
     
    562562definition eval_tailcall ≝
    563563λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f.
    564 λcurr_fn : joint_closed_internal_function ??.
     564λcurr_ret : call_dest p.
    565565λst : state_pc p.
    566566! bl ← block_of_call … ge f st : IO ???;
     
    572572  return mk_state_pc … st' pc (last_pop … st)
    573573| External efd ⇒
    574   let curr_dest ≝ joint_if_result ?? curr_fn in
    575   ! st' ← eval_external_call … efd args curr_dest st ;
    576   eval_return … ge curr_f curr_fn st
     574  ! st' ← eval_external_call … efd args curr_ret st ;
     575  eval_return … ge curr_f curr_ret st
    577576].
    578577
     
    598597    ]
    599598  | final s ⇒
     599    let curr_ret ≝ joint_if_result … curr_fn in
    600600    match s with
    601601    [ GOTO l ⇒ goto … ge l st
    602     | RETURN ⇒ eval_return … ge curr_id curr_fn st
     602    | RETURN ⇒ eval_return … ge curr_id curr_ret st
    603603    | TAILCALL _ f args ⇒
    604       eval_tailcall … ge f args curr_id curr_fn st
     604      eval_tailcall … ge f args curr_id curr_ret st
    605605    ]
    606606  | FCOND _ a lbltrue lblfalse ⇒
     
    618618  λp,globals,ge,st.
    619619  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
    620   ! st' ← eval_statement_no_pc … ge id fn s st : IO ???;
     620  ! st' ← eval_statement_no_pc … ge id s st : IO ???;
    621621  let st'' ≝ set_no_pc … st' st in
    622622  eval_statement_advance … ge id fn s st''.
    623623
    624 (* Paolo: what if in an intermediate language main finishes with an external
    625   tailcall? Maybe it should rely on an FEnd flow command issued, but that's
    626   not static... *)
    627624definition is_final: ∀p: sem_params.∀globals.
    628625  genv p globals → program_counter → state_pc p → option int ≝
     
    632629  [ final s' ⇒
    633630    match s' with
    634     [ RETURN ⇒
    635       do st' ← pop_frame … ge id fn st;
     631    [ RETURN ⇒
     632      let curr_ret ≝ joint_if_result … fn in
     633      do st' ← pop_frame … ge id curr_ret st;
    636634      if eq_program_counter (\snd … st') exit then
    637       do vals ← read_result … ge (joint_if_result … fn) st ;
     635      do vals ← read_result … ge curr_ret st ;
    638636        Word_of_list_beval vals
    639637      else
Note: See TracChangeset for help on using the changeset viewer.