Changeset 1384 for src/ERTL/semantics.ma
- Timestamp:
- Oct 16, 2011, 7:42:25 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/semantics.ma
r1381 r1384 43 43 (*CSC: could we use here a dependent type to avoid the Error case? *) 44 44 axiom EmptyStack: String. 45 definition ertl_pop_frame: state … ertl_sem_params → res ( (state … ertl_sem_params) × address) ≝45 definition ertl_pop_frame: state … ertl_sem_params → res (state … ertl_sem_params) ≝ 46 46 λst. 47 do 〈st,ra〉 ← fetch_ra … st;48 47 let frms ≝ st_frms ? st in 49 48 match frms with 50 49 [ nil ⇒ Error ? [MSG EmptyStack] 51 50 | 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)) ]. 53 52 54 53 definition ertl_save_frame: … … 118 117 λglobals. 119 118 mk_more_sem_params2 … ertl_more_sem_params1 120 (graph_fetch_statement …) ertl_fetch_result ertl_fetch_external_args ertl_set_result121 (ertl_exec_extended …).119 (graph_fetch_statement …) (load_ra …) ertl_fetch_result 120 ertl_fetch_external_args ertl_set_result (ertl_exec_extended …). 122 121 123 122 definition ertl_fullexec ≝
Note: See TracChangeset
for help on using the changeset viewer.