source: LTS/mono_stack.ma @ 3586

(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "stack.ma".

definition mono_stack_store_t ≝ DeqProd (DeqSet_List DeqNat) (DeqProd DeqNat DeqNat).

definition mono_stack_state_params:state_params≝
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 ≝ 
λs,n.〈n::(\fst s),(\snd s)〉.

definition mono_pop : (mono_stack_store_t) → option (DeqNat × (mono_stack_store_t)) ≝
λs.match \fst s with
[nil ⇒ None ?
|cons x xs ⇒ return 〈x,〈xs,(\snd s)〉〉
].

definition mono_eval_combinators : guard_combinators → (mono_stack_store_t)→ option (mono_stack_store_t)≝
λc,s.match c with
[ push_var x ⇒  
                ! n ← read_frame (\fst s) (to_shift+x) (\fst (\snd s));
                return mono_push s n
| push_const n ⇒ return mono_push s n
| push_plus ⇒ ! 〈val1,st1〉 ← mono_pop s; ! 〈val2,st2〉 ← mono_pop st1; return mono_push st2 (val2 + val1)
| push_minus ⇒ ! 〈val1,st1〉 ← mono_pop s; ! 〈val2,st2〉 ← mono_pop st1; return mono_push st2 (val2 - val1)
| push_eq ⇒ ! 〈val1,st1〉 ← mono_pop s; ! 〈val2,st2〉 ← mono_pop st1; return mono_push st2 (if eqb val2 val1 then 1 else O)
| push_not ⇒ ! 〈val1,st1〉 ← mono_pop s;return mono_push st1 (1-val1)
].

definition mono_stack_eval_seq: stack_seq→ 
mono_stack_store_t→ option mono_stack_store_t≝
λi,s.match i with
[ pop_Ass v ⇒ ! 〈val1,st1〉 ← mono_pop s; ! new_env ← (assign_frame (\fst s) (to_shift +v) (\fst (\snd s)) val1); return 〈new_env,(\snd s)〉
| push c ⇒ mono_eval_combinators c s
| popreg v ⇒ ! x ← assign_frame (\fst s) (to_shift +v) (\fst (\snd s)) (\snd (\snd s)); return 〈x,(\snd s)〉
].

definition mono_stack_eval_cond_cond:
(list guard_combinators) → mono_stack_store_t→ option (bool × mono_stack_store_t)≝
λl,st.! fin_St ← m_fold Option … mono_eval_combinators l st;
      !〈val,st2〉← mono_pop fin_St;
      return 〈eqb val 1,st2〉.

definition mono_stack_signature≝signature mono_stack_state_params mono_stack_state_params.

definition mono_stack_eval_call:mono_stack_signature → 
mono_stack_store_t → (option mono_stack_store_t)≝ 
λsgn.λst.
    !〈exp_val,st1〉 ← mono_pop st;
    let new_fp ≝ (|(\fst st1)|) in
    let st2 ≝ mono_push st1 (\fst (\snd st)) in
    let st3 ≝ mono_push st2 O in
    let st4 ≝ mono_push st3 exp_val in
    let new_frame ≝ list_n … O (pred (to_shift + (f_pars … sgn))) in
    return 〈new_frame @ (\fst st4),〈new_fp,(\snd(\snd st))〉〉.

let rec reduce_list (A : Type[0]) (l : list A) (n : ℕ) on l : option (list A) ≝ 
match n with
[ O ⇒ return nil ?
| S m ⇒ match l with 
  [ nil ⇒ None ? 
  | cons x xs ⇒ ! tl ← reduce_list … xs m; return cons ? x tl
  ]
].

lemma reduce_list_def : ∀A : Type[0].∀l,l' : list A.∀n : ℕ.
reduce_list … l n = return l' → 
|l'| = n ∧ ∃l''.l = l'@l''.
#A #l elim l
[ #l' * normalize [|#m] #EQ destruct % /2/ ]
#x #xs #IH #l' * [ whd in ⊢ (??%% → ?); #EQ destruct % /2/]
#m change with (m_bind ?????) in ⊢ (??%? → ?); #H
cases(bind_inversion ????? H) -H #l'' * #EQl'' whd in ⊢ (??%% → ?);
#EQ destruct % [ whd in match (length ??); @eq_f @(proj1 … (IH … EQl''))]
cases(proj2 … (IH … EQl'')) #l''' #EQl''' %{l'''} >EQl''' %
qed.

definition mono_pop_frame : mono_stack_store_t → ℕ → option mono_stack_store_t ≝ 
λst,n.! new_env ← reduce_list … (\fst st) n; return 〈new_env,(\snd st)〉.


definition mono_stack_return_call:mono_stack_store_t → (option mono_stack_store_t)≝
λs.!〈n,st1〉 ← mono_pop s;
   ! 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 *)
   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〉〉.

definition mono_stack_sem_state_params : ℕ → sem_state_params mono_stack_state_params ≝ 
λn.mk_sem_state_params mono_stack_state_params mono_stack_eval_seq ?
(λ_.mono_stack_eval_cond_cond (nil ?)) mono_stack_eval_cond_cond (λx.λ_.mono_stack_eval_call x) (λ_.mono_stack_return_call) 
(mono_stack_init_store n). * qed.

  (* Abitare tipo Instructions *)
  
definition mono_stack_Instructions≝Instructions mono_stack_state_params flat_labels.


definition mono_stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).