source: LTS/stack.ma @ 3560

(**************************************************************************)
(*       ___                                                              *)
(*      ||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 "variable.ma".

inductive guard_combinators : Type[0] ≝ 
| push_var: variable → guard_combinators
| push_const : DeqNat → guard_combinators
| push_plus : guard_combinators
| push_minus : guard_combinators
| push_eq : guard_combinators
| push_not : guard_combinators.

definition eq_guard_combinator : guard_combinators → guard_combinators → bool ≝ 
λx.match x with
[ push_var v1⇒ λy.match y with [push_var v2 ⇒ eqb v1 v2 | _ ⇒ false]
| push_const n1 ⇒ λy.match y with [push_const n2 ⇒ eqb n1 n2 | _ ⇒ false]
| push_plus ⇒ λy.match y with [push_plus ⇒ true | _ ⇒ false ]
| push_minus ⇒  λy.match y with [push_minus ⇒ true | _⇒  false ]
| push_eq ⇒  λy.match y with [push_eq ⇒ true | _ ⇒ false ]
| push_not ⇒ λy.match y with [push_not ⇒ true | _ ⇒ false ]
].

lemma eq_guard_combinator_elim : ∀P : bool → Prop.
∀c1,c2.(c1 = c2 → P true) → (c1 ≠ c2 → P false) → 
P(eq_guard_combinator c1 c2).
#P *
[#v1 | #n1 ]
*
[1,7,13,19,25,31: #v2 |2,8,14,20,26,32: #n2]
normalize #H1 #H2 try @H1 try @H2 //
try(% #EQ destruct) 
[ @(eqb_elim … v1 v2) [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
| @(eqb_elim … n1 n2) [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
]
qed.

inductive stack_seq:Type[0]≝ 
| pop_Ass: variable → stack_seq 
| push : guard_combinators → stack_seq.

definition eq_stack_seq : stack_seq → stack_seq → bool ≝ 
λx.match x with
[ pop_Ass v1 ⇒ λy.match y with [pop_Ass v2 ⇒ eqb v1 v2 | _ ⇒ false ]
| push c1 ⇒ λy.match y with [push c2 ⇒ eq_guard_combinator c1 c2 | _ ⇒ false]
].

lemma eq_stack_seq_elim : ∀P : bool → Prop.
∀x1,x2.(x1 = x2 → P true) → (x1 ≠ x2 → P false) → 
P(eq_stack_seq x1 x2).
#P * [#v1 | #c1] * [1,3: #v2 |*: #c2] #H1 #H2 try(@H2 % #EQ destruct)
[ normalize @(eqb_elim … v1 v2) [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
| whd in match eq_stack_seq; normalize nodelta @eq_guard_combinator_elim /2/
 * #H @H2 % #EQ destruct @H %
]
qed.

definition DeqStackSeq ≝ mk_DeqSet stack_seq eq_stack_seq ?.
@hide_prf #x #y @eq_stack_seq_elim
[ #EQ destruct % // | * #H % [ #EQ destruct | #EQ destruct cases(H (refl …)) ]
qed.

definition DeqGuardCombinator ≝ mk_DeqSet guard_combinators eq_guard_combinator ?.
@hide_prf #x #y @eq_guard_combinator_elim
[ #EQ destruct % // | * #H % [ #EQ destruct | #EQ destruct cases(H (refl …)) ]
qed.
 
definition 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) variable (mk_DeqSet unit (λ_.λ_.true) ?).
@hide_prf ** % // qed.

definition stack_state_params:state_params≝
mk_state_params stack_instr_params imp_env_params flat_labels frame_store_t (*DeqEnv*).

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

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

definition eval_combinators : guard_combinators → (store_type stack_state_params)→ option (store_type stack_state_params)≝
λc,s.match c with
[ push_var x ⇒ ! curr_env ← frame_current_env s;
               ! n ← read_frame curr_env (to_shift+x) O;
                 push s n
| push_const n ⇒ push s n
| push_plus ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (val1 + val2)
| push_minus ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (val1 - val2)
| push_eq ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (if eqb val1 val2 then 1 else O)
| push_not ⇒ ! 〈val1,st1〉 ← pop s;push st1 (1-val1)
].


definition stack_eval_seq: (seq_instr stack_state_params)→(store_type stack_state_params)→ option (store_type stack_state_params)≝
λi,s.match i with
[ pop_Ass v ⇒ ! 〈val1,st1〉 ← pop s;frame_assign_var st1 (to_shift +v) val1
| push c ⇒ eval_combinators c s
].

definition stack_eval_cond_cond:
(list guard_combinators) → (store_type stack_state_params)→ option (bool × (store_type stack_state_params))≝
λl,st.! fin_St ← m_fold Option … eval_combinators l st;
      !〈val,st2〉← pop fin_St;
      return 〈eqb val 1,st2〉.


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)〉 fpt n
  ].

definition stack_return_call:frame_store_t→ (option frame_store_t)≝
λs.match (\fst s) with 
[nil⇒ None ?
|cons hd tl⇒ let 〈env,v〉≝ hd in
             !〈n,st1〉 ← pop s;
             frame_assign_var 〈tl,\snd s〉 v n
].
 


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.

  (* Abitare tipo Instructions *)
  
definition stack_Instructions≝Instructions stack_state_params flat_labels.

definition stack_signature≝signature stack_state_params stack_state_params.


definition stack_envitem≝ (env_item imp_env_params stack_instr_params flat_labels).