Changeset 1298 for src/joint


Ignore:
Timestamp:
Oct 5, 2011, 9:41:42 PM (8 years ago)
Author:
sacerdot
Message:
  • fetch_statement now takes in input the globalenv
  • fetch_statement and rtl_succ implemented for RTL; the implementation should be generic enough to work on every graph language
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1294 r1298  
    6060 ; init_locals : localsT p → regsT … more_sparams
    6161 
    62  ; fetch_statement: state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
     62 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
    6363 ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
    6464
     
    205205definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
    206206 λglobals,p,ge,st.
    207   ! s ← fetch_statement … st;
     207  ! s ← fetch_statement … ge st;
    208208  match s with
    209209    [ GOTO l ⇒ ret ? 〈E0, goto … l st〉
     
    310310qed.
    311311
    312 definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝
    313  λglobals,p,exit,registersno,st. res_to_opt … (
    314   do s ← fetch_statement … st;
     312definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. genv … p → address → nat → state p → option int ≝
     313 λglobals,p,ge,exit,registersno,st.res_to_opt … (
     314  do s ← fetch_statement … ge st;
    315315  match s with
    316316   [ RETURN ⇒
     
    335335definition joint_exec: trans_system io_out io_in ≝
    336336  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
    337    (λG.is_final (globals G) (sparams2 G) (exit G) (registersno G))
     337   (λG.is_final (globals G) (sparams2 G) (genv2 G) (exit G) (registersno G))
    338338   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
    339339
Note: See TracChangeset for help on using the changeset viewer.