Ignore:
Timestamp:
Jan 30, 2013, 7:25:39 PM (7 years ago)
Author:
tranquil
Message:
  • dropped locals and exit from definition of joint_if_function
  • new definition of blocks to accomodate ERTLptr pass
  • stated properties of translation as axioms
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2592 r2595  
    197197 
    198198  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    199   ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
     199  (* ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars *)
    200200  ; save_frame: call_kind → call_dest uns_pars → ident → state_pc st_pars → res (state st_pars)
    201201   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
     
    218218  }.
    219219
     220(*
    220221definition allocate_locals :
    221222  ∀p,F.∀sup : sem_unserialized_params p F.
     
    223224  λp,F,sup,l,st.
    224225  let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in
    225   set_regs … r st.
     226  set_regs … r st. *)
    226227
    227228definition helper_def_retrieve :
     
    526527
    527528definition eval_internal_call ≝
    528 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args,st.
     529λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
     530λst : state p.
    529531! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    530 ! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
    531 return allocate_locals … p (joint_if_locals … fn) st'.
     532setup_call … stack_size (joint_if_params … globals fn) args st.
    532533
    533534definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
Note: See TracChangeset for help on using the changeset viewer.