+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* *)
+(* Sviluppato da: *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "compiler/environment.ma".
+
+(* ********************** *)
+(* GESTIONE AMBIENTE FLAT *)
+(* ********************** *)
+
+(* elemento: name + nel curId + nel desc *)
+inductive var_flatElem : Type ≝
+VAR_FLAT_ELEM: aux_str_type → ne_list (option nat) → ne_list desc_elem → var_flatElem.
+
+definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ _ ⇒ n ].
+definition get_cur_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ c _ ⇒ c ].
+definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ _ d ⇒ d ].
+
+(* ambiente globale: descrittori *)
+definition aux_flatEnv_type ≝ Prod nat (list var_flatElem).
+
+(* ambiente vuoto *)
+definition empty_flatEnv ≝ pair ?? O (nil var_flatElem).
+
+definition get_depth_flatEnv ≝ λenv:aux_flatEnv_type.match env with [ pair d _ ⇒ d ].
+definition get_subEnv_flatEnv ≝ λenv:aux_flatEnv_type.match env with [ pair _ s ⇒ s ].
+
+(* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
+let rec enter_flatEnv_aux (subEnv:list var_flatElem) on subEnv ≝
+ match subEnv with
+ [ nil ⇒ []
+ | cons h t ⇒ (VAR_FLAT_ELEM (get_name_flatVar h)
+ ((get_first_neList ? (get_cur_flatVar h))§§(get_cur_flatVar h))
+ (get_desc_flatVar h))::(enter_flatEnv_aux t)
+ ].
+
+definition enter_flatEnv ≝
+λenv.pair ?? (get_depth_flatEnv env) (enter_flatEnv_aux (get_subEnv_flatEnv env)).
+
+(* leave: elimina la testa (il "cur" corrente) *)
+let rec leave_flatEnv_aux (subEnv:list var_flatElem) on subEnv ≝
+ match subEnv with
+ [ nil ⇒ []
+ | cons h t ⇒ (VAR_FLAT_ELEM (get_name_flatVar h)
+ (cut_first_neList ? (get_cur_flatVar h))
+ (get_desc_flatVar h))::(leave_flatEnv_aux t)
+ ].
+
+definition leave_flatEnv ≝
+λenv.pair ?? (get_depth_flatEnv env) (leave_flatEnv_aux (get_subEnv_flatEnv env)).
+
+(* get_id *)
+let rec get_id_flatEnv_aux (subEnv:list var_flatElem) (name:aux_str_type) on subEnv ≝
+ match subEnv with
+ [ nil ⇒ None ?
+ | cons h t ⇒
+ match (match eqStr_str name (get_name_flatVar h) with
+ [ true ⇒ get_first_neList ? (get_cur_flatVar h)
+ | false ⇒ None ?
+ ]) with
+ [ None ⇒ get_id_flatEnv_aux t name
+ | Some x ⇒ Some ? x
+ ]
+ ].
+
+definition get_id_flatEnv ≝
+λe:aux_flatEnv_type.λstr:aux_str_type.
+ match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with
+ [ None ⇒ O | Some x ⇒ x ].
+
+(* get_desc *)
+let rec get_desc_flatEnv_aux (subEnv:list var_flatElem) (name:aux_strId_type) on subEnv ≝
+ match subEnv with
+ [ nil ⇒ None ?
+ | cons h t ⇒
+ match (match (eqStr_str (get_name_strId name) (get_name_flatVar h))⊗
+ (leb (S (get_id_strId name)) (len_neList ? (get_desc_flatVar h))) with
+ [ true ⇒ nth_neList ? (get_desc_flatVar h) (get_id_strId name)
+ | false ⇒ None ?
+ ]) with
+ [ None ⇒ get_desc_flatEnv_aux t name
+ | Some x ⇒ Some ? x
+ ]
+ ].
+
+definition get_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with
+ [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
+
+(* check_id *)
+definition check_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type.
+ match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ False | Some _ ⇒ True ].
+
+definition checkb_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type.
+ match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ false | Some _ ⇒ true ].
+
+lemma checkbidflatenv_to_checkidflatenv : ∀e,str.checkb_id_flatEnv e str = true → check_id_flatEnv e str.
+ unfold checkb_id_flatEnv;
+ unfold check_id_flatEnv;
+ intros;
+ letin K ≝ (get_id_flatEnv_aux (get_subEnv_flatEnv e) str);
+ elim K;
+ [ normalize; autobatch |
+ normalize; autobatch ]
+qed.
+
+definition checknot_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type.
+ match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ True | Some _ ⇒ False ].
+
+definition checknotb_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type.
+ match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ true | Some _ ⇒ false ].
+
+lemma checknotbidflatenv_to_checknotidflatenv : ∀e,str.checknotb_id_flatEnv e str = true → checknot_id_flatEnv e str.
+ unfold checknotb_id_flatEnv;
+ unfold checknot_id_flatEnv;
+ intros;
+ letin K ≝ (get_id_flatEnv_aux (get_subEnv_flatEnv e) str);
+ elim K;
+ [ normalize; autobatch |
+ normalize; autobatch ]
+qed.
+
+(* check_desc *)
+definition check_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ False | Some _ ⇒ True ].
+
+definition checkb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ false | Some _ ⇒ true ].
+
+lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str = true → check_desc_flatEnv e str.
+ unfold checkb_desc_flatEnv;
+ unfold check_desc_flatEnv;
+ intros;
+ letin K ≝ (get_desc_flatEnv_aux (get_subEnv_flatEnv e) str);
+ elim K;
+ [ normalize; autobatch |
+ normalize; autobatch ]
+qed.
+
+definition checknot_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ True | Some _ ⇒ False ].
+
+definition checknotb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ true | Some _ ⇒ false ].
+
+lemma checknotbdescflatenv_to_checknotdescflatenv : ∀e,str.checknotb_desc_flatEnv e str = true → checknot_desc_flatEnv e str.
+ unfold checknotb_desc_flatEnv;
+ unfold checknot_desc_flatEnv;
+ intros;
+ letin K ≝ (get_desc_flatEnv_aux (get_subEnv_flatEnv e) str);
+ elim K;
+ [ normalize; autobatch |
+ normalize; autobatch ]
+qed.
+
+(* aggiungi descrittore : in testa al primo ambiente *)
+let rec previous_cur_from_depth (depth:nat) on depth ≝
+ match depth with
+ [ O ⇒ «£(Some ? O)»
+ | S n ⇒ (previous_cur_from_depth n)&«£(None ?)»
+ ].
+
+let rec add_desc_flatEnv_aux (subEnv:list var_flatElem) (str:aux_str_type) (c:bool) (desc:ast_type) (depth:nat) (flag:bool) on subEnv ≝
+ match subEnv with
+ [ nil ⇒ match flag with
+ [ true ⇒ []
+ | false ⇒ [ VAR_FLAT_ELEM str (previous_cur_from_depth depth) «£(DESC_ELEM c desc)» ]
+ ]
+ | cons h t ⇒ (match eqStr_str str (get_name_flatVar h) with
+ [ true ⇒ VAR_FLAT_ELEM (get_name_flatVar h)
+ («£(Some ? (len_neList ? (get_desc_flatVar h)))»&(cut_first_neList ? (get_cur_flatVar h)))
+ ((get_desc_flatVar h)&«£(DESC_ELEM c desc)»)
+ | false ⇒ h
+ ])::(add_desc_flatEnv_aux t str c desc depth ((eqStr_str str (get_name_flatVar h)⊕flag)))
+ ].
+
+definition add_desc_flatEnv ≝ λenv,str,c,desc.add_desc_flatEnv_aux (get_subEnv_flatEnv env) str c desc (get_depth_flatEnv env) false.
+
+(* equivalenza *)
+definition env_to_flatEnv ≝
+ λe,fe.∀str.
+ check_desc_env e str →
+ check_id_flatEnv fe str →
+ check_desc_flatEnv fe (STR_ID str (get_id_flatEnv fe str)) →
+ get_desc_env e str = get_desc_flatEnv fe (STR_ID str (get_id_flatEnv fe str)).
+
+lemma empty_env_to_flatEnv : env_to_flatEnv empty_env empty_flatEnv.
+ unfold env_to_flatEnv;
+ unfold empty_env;
+ unfold empty_flatEnv;
+ simplify;
+ intros;
+ reflexivity.
+qed.
+
+lemma getdescenv_to_enter : ∀e,str.get_desc_env e str = get_desc_env (enter_env e) str.
+ intros 2;
+ elim e;
+ reflexivity.
+qed.
+
+lemma enter_env_to_flatEnv :
+ ∀e,fe.env_to_flatEnv e fe → env_to_flatEnv (enter_env e) (enter_flatEnv fe).
+ intros 2;
+ unfold env_to_flatEnv;
+ intros;
+ lapply (H str H1);
+ [ rewrite < (getdescenv_to_enter e str);
+ rewrite > Hletin;
+
+
+
+
+
+
+
+
+
+