Changeset 1390 for src/ERTL/semantics.ma


Ignore:
Timestamp:
Oct 17, 2011, 11:43:52 AM (9 years ago)
Author:
sacerdot
Message:

All fetch_result implementations have been factorized out, leaving only a
result_regs function. All axioms in joint_LTL_LIN_semantics but the ones for
external functions have been implemented.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1389 r1390  
    6060    (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
    6161
    62 definition ertl_fetch_result:
    63  ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list beval) ≝
     62definition ertl_result_regs:
     63 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list register) ≝
    6464 λglobals,ge,st.
    6565  do fn ← graph_fetch_function … globals ge st ;
    66   let ret_val_regs ≝ joint_if_result … fn in
    67    mmap … (λreg.greg_retrieve ertl_sem_params st reg) ret_val_regs.
     66  OK … (joint_if_result … fn).
    6867
    6968(*CSC: XXXX, for external functions only*)
     
    117116 λglobals.
    118117  mk_more_sem_params2 … ertl_more_sem_params
    119    (graph_fetch_statement …) (load_ra …) (ertl_fetch_result …)
     118   (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
    120119   ertl_init_locals ertl_save_frame (ertl_pop_frame …)
    121120   ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
Note: See TracChangeset for help on using the changeset viewer.