Changeset 3572

Timestamp:

Jun 17, 2015, 6:42:45 PM (4 years ago)

Author:

piccolo

Message:

pass stack to mono stack in place

Location:

LTS

Files:

• mono_stack.ma (modified) (4 diffs)
• stack_monostack_pass.ma (added)

LTS/mono_stack.ma

@@ -15 +15 @@
 include "stack.ma".
 
-definition mono_stack_instr_params ≝ mk_instr_params DeqStackSeq (mk_DeqSet io_i io_i_eq io_i_eq_equality) 
- (mk_DeqSet unit (λ_.λ_.true) ?) (DeqSet_List DeqGuardCombinator) (mk_DeqSet unit (λ_.λ_.true) ?) (mk_DeqSet unit (λ_.λ_.true) ?).
-@hide_prf ** % // qed.
-
 definition mono_stack_store_t ≝ DeqProd (DeqSet_List DeqNat) (DeqProd DeqNat DeqNat).
 
 definition mono_stack_state_params:state_params≝
-mk_state_params mono_stack_instr_params stack_env_params flat_labels mono_stack_store_t (*DeqEnv*).
+mk_state_params stack_instr_params stack_env_params flat_labels mono_stack_store_t (*DeqEnv*).
 
 definition mono_push : mono_stack_store_t → DeqNat → mono_stack_store_t ≝ 
@@ -44 +40 @@
 | push_not ⇒ ! 〈val1,st1〉 ← mono_pop s;return mono_push st1 (1-val1)
 ].
-
-check assign_frame
 
 definition mono_stack_eval_seq: (seq_instr mono_stack_state_params)→ 
@@ -103 +97 @@
    ! new_fp ← read_frame (\fst st1) (\fst (\snd s)) O; (* 0 leggi il frame pointer precedente *)
    ! st2 ← mono_pop_frame st1 (\fst (\snd s)) ;(* 1: accorciare la lista fino a diventare lunga come \snd st1 ovvero il frame pointer corrente *)
-   let st3 ≝  mono_push st2 n in (* 2: pushare il valore n *)
-   return 〈(\fst st3),〈new_fp,(\snd(\snd s))〉〉. (* 3: ritornare lo stato con il nuovo fp *)
+   return 〈(\fst st2),〈new_fp,n〉〉. (* 3: ritornare lo stato con il nuovo fp *)
 
 definition mono_stack_init_store ≝ λn : ℕ.〈list_n … O  (to_shift + n),〈O,O〉〉.
@@ -120 +113 @@
 
 
-definition mono_stack_envitem≝ (env_item stack_env_params mono_stack_instr_params flat_labels).
+definition mono_stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).