Changeset 1318


Ignore:
Timestamp:
Oct 7, 2011, 1:48:24 PM (8 years ago)
Author:
sacerdot
Message:

Frame management implemented.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1313 r1318  
    3434definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.
    3535
    36 (*CSC: XXXXX *)
    37 axiom ertl_init_locals : list register → (register_env beval) × hw_register_env → (register_env beval) × hw_register_env.
    38 axiom ertl_pop_frame: state … ertl_sem_params → res (state … ertl_sem_params).
    39 axiom ertl_save_frame: state … ertl_sem_params → state … ertl_sem_params.
     36definition ertl_init_locals :
     37 list register →
     38  (register_env beval) × hw_register_env → (register_env beval) × hw_register_env ≝
     39 λlocals,lenv.
     40  〈foldl … (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals, \snd lenv〉.
     41
     42(*CSC: could we use here a dependent type to avoid the Error case? *)
     43axiom EmptyStack: String.
     44definition ertl_pop_frame: state … ertl_sem_params → res (state … ertl_sem_params) ≝
     45 λst.
     46  let frms ≝ st_frms ? st in
     47  match frms with
     48  [ nil ⇒ Error ? [MSG EmptyStack]
     49  | cons hd tl ⇒
     50     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
     51
     52definition ertl_save_frame: state … ertl_sem_params → state … ertl_sem_params ≝
     53 λst.
     54  set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st)) st.
    4055
    4156definition ertl_more_sem_params1 : more_sem_params1 … ertl_params1 ≝
Note: See TracChangeset for help on using the changeset viewer.