Changeset 1384 for src/ERTL


Ignore:
Timestamp:
Oct 16, 2011, 7:42:25 PM (8 years ago)
Author:
sacerdot
Message:
  • fetch_ra taken out of pop_frame again since it is used uniformly and it is also required for is_final
  • fetch_ra made abstract since it gets a different implementation in RTL
  • old fetch_ra renamed into load_ra (to match the save_ra name)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1381 r1384  
    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) × address) ≝
     45definition ertl_pop_frame: state … ertl_sem_params → res (state … ertl_sem_params) ≝
    4646 λst.
    47   do 〈st,ra〉 ← fetch_ra … st;
    4847  let frms ≝ st_frms ? st in
    4948  match frms with
    5049  [ nil ⇒ Error ? [MSG EmptyStack]
    5150  | cons hd tl ⇒
    52      OK … (〈set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st),ra〉) ].
     51     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
    5352
    5453definition ertl_save_frame:
     
    118117 λglobals.
    119118  mk_more_sem_params2 … ertl_more_sem_params1
    120    (graph_fetch_statement …) ertl_fetch_result ertl_fetch_external_args ertl_set_result
    121     (ertl_exec_extended …).
     119   (graph_fetch_statement …) (load_ra …) ertl_fetch_result
     120    ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
    122121
    123122definition ertl_fullexec ≝
Note: See TracChangeset for help on using the changeset viewer.