Changeset 2595 for src/joint/semantics.ma

Timestamp:

Jan 30, 2013, 7:25:39 PM (8 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:

• src/joint/semantics.ma (modified) (4 diffs)

src/joint/semantics.ma

@@ -197 +197 @@
   
   (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
-  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
+  (* ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars *)
   ; save_frame: call_kind → call_dest uns_pars → ident → state_pc st_pars → res (state st_pars)
    (*CSC: setup_call returns a res only because we can call a function with the wrong number and
@@ -218 +218 @@
   }.
 
+(*
 definition allocate_locals :
   ∀p,F.∀sup : sem_unserialized_params p F.
@@ -223 +224 @@
   λp,F,sup,l,st.
   let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in
-  set_regs … r st. 
+  set_regs … r st. *)
 
 definition helper_def_retrieve : 
@@ -526 +527 @@
 
 definition eval_internal_call ≝
-λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args,st.
+λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
+λst : state p.
 ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
-! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
-return allocate_locals … p (joint_if_locals … fn) st'.
+setup_call … stack_size (joint_if_params … globals fn) args st.
 
 definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].