Changeset 1385 for src/ERTL


Ignore:
Timestamp:
Oct 17, 2011, 1:40:13 AM (9 years ago)
Author:
sacerdot
Message:
  1. fetch_result and pop_frame now takes the genv in input
  2. implementation of fetch_result for RTL completed All RTL axioms but the ones related to external functions are now closed.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1384 r1385  
    4343(*CSC: could we use here a dependent type to avoid the Error case? *)
    4444axiom EmptyStack: String.
    45 definition ertl_pop_frame: state … ertl_sem_params → res (state … ertl_sem_params) ≝
    46  λst.
     45definition ertl_pop_frame:
     46 ∀globals. genv … (ertl_params globals) → state … ertl_sem_params → res (state … ertl_sem_params) ≝
     47 λglobals,ge,st.
    4748  let frms ≝ st_frms ? st in
    4849  match frms with
     
    6162definition ertl_more_sem_params1 : more_sem_params1 … ertl_params1 ≝
    6263 mk_more_sem_params1 ? ertl_params1 ertl_more_sem_params
    63   ertl_init_locals ertl_pop_frame ertl_save_frame.
     64  ertl_init_locals ertl_save_frame.
    6465
    6566(*CSC: XXXXX, for is_final only *)
    66 axiom ertl_fetch_result: state ertl_sem_params → res (list beval).
     67axiom ertl_fetch_result:
     68 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list beval).
    6769
    6870(*CSC: XXXX, for external functions only*)
     
    117119 λglobals.
    118120  mk_more_sem_params2 … ertl_more_sem_params1
    119    (graph_fetch_statement …) (load_ra …) ertl_fetch_result
    120     ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
     121   (graph_fetch_statement …) (load_ra …) (ertl_fetch_result …)
     122   (ertl_pop_frame …) ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
    121123
    122124definition ertl_fullexec ≝
Note: See TracChangeset for help on using the changeset viewer.