Changeset 3566 for LTS/stack.ma

Timestamp:

Jun 17, 2015, 4:23:08 PM (4 years ago)

Author:

piccolo

Message:

 

File:

• LTS/stack.ma (modified) (4 diffs)

LTS/stack.ma

@@ -81 +81 @@
 @hide_prf ** % // qed.
 
+definition stack_env_params ≝ mk_env_params ℕ.
+
 definition stack_state_params:state_params≝
-mk_state_params stack_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
+mk_state_params stack_instr_params stack_env_params flat_labels frame_store_t (*DeqEnv*).
 
 definition push : (store_type stack_state_params) → DeqNat → option (store_type stack_state_params) ≝ 
@@ -125 +127 @@
 
 
+let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝
+match n with
+[ O ⇒ nil ?
+| S m ⇒ a :: list_n … a m
+].
+
 definition stack_eval_call:(signature stack_state_params stack_state_params)→ act_params_type stack_state_params → 
 frame_store_t → (option frame_store_t)≝
-λsgn,var,st.
-  match sgn with 
-  [ mk_signature fun fpt rt ⇒
-    !〈n,st1〉 ← pop st;
-    frame_assign_var 〈(〈(nil ?),var〉::(\fst st1)),(\snd st1)〉 O n
-  ].
+λsgn.λvar,st.
+    !〈n,st1〉 ← pop st;  
+    frame_assign_var 〈(〈list_n … O (pred (to_shift + (f_pars … sgn))),var〉::(\fst st1)),(\snd st1)〉 to_shift n.
 
 definition stack_return_call:frame_store_t→ (option frame_store_t)≝
@@ -142 +147 @@
 ].
  
+definition stack_init_store ≝ λn : ℕ.〈[〈list_n … O (to_shift + n),O〉],〈O,O〉〉.
 
 
-definition stack_sem_state_params : sem_state_params stack_state_params ≝ mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io
-(λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) frame_init_store.
+definition stack_sem_state_params : ℕ → sem_state_params stack_state_params ≝ 
+λn.mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io
+(λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) (stack_init_store n).
 
   (* Abitare tipo Instructions *)
@@ -154 +161 @@
 
 
-definition stack_envitem≝ (env_item frame_env_params stack_instr_params flat_labels).
+definition stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).