Changeset 1371 for src/ERTL/semantics.ma


Ignore:
Timestamp:
Oct 14, 2011, 1:42:42 PM (9 years ago)
Author:
sacerdot
Message:

save_frame changed to accept also the formal/actual argument pairs, required
in the RTL semantics. The function returns now a res, but this could be fixed
with a dependent type for function call to disallow calling a function with the
wrong arguments.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1359 r1371  
    5151     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
    5252
    53 definition ertl_save_frame: unit → state … ertl_sem_params → state … ertl_sem_params ≝
    54  λ_.λst.
    55   set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st)) st.
     53definition ertl_save_frame: nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
     54 λ_.λ_.λ_.λst.
     55  OK …
     56   (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
     57    (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
    5658
    5759definition ertl_more_sem_params1 : more_sem_params1 … ertl_params1 ≝
Note: See TracChangeset for help on using the changeset viewer.