Ignore:
Timestamp:
Mar 6, 2013, 12:09:52 PM (7 years ago)
Author:
piccolo
Message:

modified joint_closed_internal_function definition (added condition on pseudo-registers)
added new record for parameters
modified state definition with option for framesT

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_semantics.ma

    r2688 r2783  
    5454
    5555record state (semp: sem_state_params): Type[0] ≝
    56  { st_frms: framesT semp
     56 { st_frms: option(framesT semp)
    5757 ; istack : internal_stack
    5858 ; carry: bebit
     
    103103
    104104definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    105  λp,frms,st. mk_state … frms (istack … st) (carry … st) (regs … st) (m … st).
     105 λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st).
    106106
    107107(*
     
    184184  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    185185  (* ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars *)
    186   ; save_frame: call_kind → call_dest uns_pars → ident → state_pc st_pars → res (state st_pars)
     186  ; save_frame: call_kind → call_dest uns_pars → state_pc st_pars → res (state st_pars)
    187187   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    188188     type of arguments. To be fixed using a dependent type *)
     
    528528match fd with
    529529[ Internal ifd ⇒
    530   let ident ≝ ? in
    531   ! st' ← save_frame … (kind_of_call … f) dest ident st ;
     530  ! st' ← save_frame … (kind_of_call … f) dest st ;
    532531  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
    533532  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
     
    536535  ! st' ← eval_external_call … efd args dest st ;
    537536  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
    538 ]. cases daemon qed. (*TODO*)
     537].
    539538
    540539definition eval_statement_no_pc :
Note: See TracChangeset for help on using the changeset viewer.