Changeset 2564 for src/ERTL


Ignore:
Timestamp:
Dec 19, 2012, 12:46:59 PM (7 years ago)
Author:
piccolo
Message:

ERTL fully repaired, useless part of return value of pop_ra
removed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r2563 r2564  
    117117  set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.
    118118
     119axiom FunctionNotFound: errmsg.
     120
    119121definition eval_ertl_seq:
    120  ∀globals. genv ERTL globals →
    121   ertl_seq → ident → joint_internal_function ERTL globals → state ERTL_state →
    122    IO io_out io_in (state ERTL_state) ≝
    123  λglobals,ge,stm,id,curr_fn,st.
    124  let framesize : Byte ≝ bitvector_of_nat 8 (joint_if_stacksize … curr_fn) in
     122 ∀F. ∀globals. genv_gen F globals →
     123  ertl_seq → ident → state ERTL_state →
     124   res (state ERTL_state) ≝
     125 λF,globals,ge,stm,id,st.
     126 ! framesize ← opt_to_res … FunctionNotFound  (stack_sizes … ge id);
     127 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
    125128  match stm with
    126129   [ ertl_new_frame ⇒
     
    174177  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
    175178  (* pair_reg_move_     ≝ *) ertl_eval_move
    176 (*  (* fetch_ra           ≝ *) ?(*(pop_ra …)*) *)
    177179  (* allocate_local     ≝ *) ertl_allocate_local
    178180  (* save_frame         ≝ *) ertl_save_frame
     
    184186  (* read_result        ≝ *) (λ_.λ_.λ_.
    185187     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    186   (* eval_ext_seq       ≝ *) ?(*eval_ertl_seq*)
    187 (*  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
    188   (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) *)
    189   (* pop_frame          ≝ *) ?(*(λ_.λ_.?(*return st_no_pc ? st*))*)
    190 (*  (* post_op2           ≝ *) (λ_.λ_.ertl_post_op2)) *)).
    191 [ (* pop_frame *) cases daemon (* Handle last-popped correctly *)
    192 | @eval_ertl_seq (* Handle type of call *)
    193 ]
     188  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
     189  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …)).
Note: See TracChangeset for help on using the changeset viewer.