Changeset 1386 for src/ERTL


Ignore:
Timestamp:
Oct 17, 2011, 1:58:47 AM (9 years ago)
Author:
sacerdot
Message:

Structure of semantic parameters simplified.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1385 r1386  
    6060    (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
    6161
    62 definition ertl_more_sem_params1 : more_sem_params1 … ertl_params1 ≝
    63  mk_more_sem_params1 ? ertl_params1 ertl_more_sem_params
    64   ertl_init_locals ertl_save_frame.
    65 
    6662(*CSC: XXXXX, for is_final only *)
    6763axiom ertl_fetch_result:
     
    118114definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
    119115 λglobals.
    120   mk_more_sem_params2 … ertl_more_sem_params1
     116  mk_more_sem_params2 … ertl_more_sem_params
    121117   (graph_fetch_statement …) (load_ra …) (ertl_fetch_result …)
    122    (ertl_pop_frame …) ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
     118   ertl_init_locals ertl_save_frame (ertl_pop_frame …)
     119   ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
    123120
    124121definition ertl_fullexec ≝
Note: See TracChangeset for help on using the changeset viewer.