Changeset 1386 for src/RTL


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/RTL/semantics.ma

    r1385 r1386  
    8888qed.
    8989
    90 definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
    91  mk_more_sem_params1 ? rtl_params1 rtl_more_sem_params
    92   rtl_init_locals rtl_save_frame.
    93 
    9490(*CSC: XXXX, for external functions only*)
    9591axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val).
     
    117113definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
    118114 λglobals.
    119   mk_more_sem_params2 … rtl_more_sem_params1
     115  mk_more_sem_params2 … rtl_more_sem_params
    120116   (graph_fetch_statement …) rtl_fetch_ra (rtl_fetch_result …)
    121    (rtl_pop_frame …) rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
     117   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
     118   rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
    122119
    123120definition rtl_fullexec ≝
Note: See TracChangeset for help on using the changeset viewer.