source: LTS/variable.ma @ 3562

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

definition to_shift : ℕ ≝ 2.

definition activation_frame ≝ DeqSet_List DeqNat.

let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) (def : A) on n : list A ≝ 
match l with
[ nil ⇒ match n with [ O ⇒ [a] | S m ⇒ def :: update … (nil ?) m a def ]
| cons x xs ⇒ match n with [O ⇒ a :: xs | S m ⇒ x :: update … xs m a def]
].

definition assign_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.λn:DeqNat.update … env (|env| - v - fp -1) n O.

definition read_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.nth_opt … (|env| -v -fp -1) env.

let rec frame_sem_expr (env:activation_frame) (e: expr) on e : (option nat) ≝
 match e with
  [ Var v ⇒ read_frame env (to_shift+v) O
  | Const n ⇒ Some ? n
  | Plus e1 e2 ⇒ !n1 ← frame_sem_expr env e1;
                 !n2 ← frame_sem_expr env e2;
                 return (n1+n2)
  | Minus e1 e2 ⇒ !n1 ← frame_sem_expr env e1;
                  !n2 ← frame_sem_expr env e2;
                  return (n1-n2)
  ].

let rec frame_sem_condition (env:activation_frame) (c:condition) on c : option bool ≝
  match c with
   [ Eq e1 e2 ⇒ !n ← frame_sem_expr env e1;
                !m ← frame_sem_expr env e2;
                return (eqb n m)
   | Not c ⇒ !b ← frame_sem_condition env c;
             return (notb b)
   ].



definition frame_store_t≝ DeqProd (DeqSet_List (DeqProd activation_frame variable)) (DeqProd DeqNat DeqNat). (*frame_pointer e stack_pointer*)

definition frame_env_params ≝ mk_env_params unit.

definition frame_state_params:state_params≝
mk_state_params imp_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).

definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return \fst hd.

definition frame_assign_var ≝ λenv:frame_store_t.λv:variable.λn:DeqNat.
match \fst env with
[ nil ⇒ None ?
| cons hd tl ⇒ let 〈e,var〉 ≝ hd in return 〈(〈assign_frame e v (\fst (\snd env)) n,var〉 :: tl),\snd env〉
].

definition frame_eval_seq:(seq_instr frame_state_params)→(store_type frame_state_params)→ option (store_type frame_state_params)≝
λi,s.match i with
[sNop ⇒ Some ? s
|sAss v e ⇒ !env ← frame_current_env … s;
            ! n ← frame_sem_expr env e;
            frame_assign_var s v n
].


definition frame_eval_io:(io_instr frame_state_params)→(store_type frame_state_params)→ option (store_type frame_state_params)≝?.
// qed.

definition frame_eval_cond_cond:(cond_instr frame_state_params)→ (store_type frame_state_params)→ option (bool × (store_type frame_state_params))≝λc,s.
!env ← frame_current_env s;
!b ← frame_sem_condition env c;
return 〈b,s〉.


definition frame_eval_loop_cond:(loop_instr frame_state_params)→ (store_type frame_state_params)→ option (bool × (store_type frame_state_params))≝
frame_eval_cond_cond.

definition frame_eval_call:(signature frame_state_params imp_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝
λsgn,e,st.
    let 〈var,act_exp〉 ≝ e in
    !env ← frame_current_env … st;
    !n ← frame_sem_expr env act_exp;
    frame_assign_var 〈(〈(nil ?),var〉::(\fst st)),(\snd st)〉 O n.

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

definition frame_init_store: (store_type frame_state_params)≝ 〈[〈(nil ?),O〉],〈O,O〉〉.


definition frame_sem_state_params : sem_state_params frame_state_params ≝ mk_sem_state_params frame_state_params frame_eval_seq frame_eval_io
frame_eval_cond_cond frame_eval_loop_cond frame_eval_call frame_return_call frame_init_store.

  (* Abitare tipo Instructions *)
  
definition frame_Instructions≝Instructions frame_state_params flat_labels.

definition frame_signature≝signature frame_state_params frame_state_params.


definition frame_envitem≝ (env_item frame_env_params imp_instr_params flat_labels).