Changeset 2595 for src/joint/semantics.ma
- Timestamp:
- Jan 30, 2013, 7:25:39 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/semantics.ma
r2592 r2595 197 197 198 198 (* Paolo: save_frame separated from call_setup to factorize tailcall code *) 199 ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars199 (* ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars *) 200 200 ; save_frame: call_kind → call_dest uns_pars → ident → state_pc st_pars → res (state st_pars) 201 201 (*CSC: setup_call returns a res only because we can call a function with the wrong number and … … 218 218 }. 219 219 220 (* 220 221 definition allocate_locals : 221 222 ∀p,F.∀sup : sem_unserialized_params p F. … … 223 224 λp,F,sup,l,st. 224 225 let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in 225 set_regs … r st. 226 set_regs … r st. *) 226 227 227 228 definition helper_def_retrieve : … … 526 527 527 528 definition 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. 529 531 ! 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'. 532 setup_call … stack_size (joint_if_params … globals fn) args st. 532 533 533 534 definition 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.