helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                                                                        *)
  17 (* Sviluppato da:                                                         *)
  18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  19 (*                                                                        *)
  20 (* ********************************************************************** *)
  21
  22 include "compiler/environment.ma".
  23
  24 (* ********************** *)
  25 (* GESTIONE AMBIENTE FLAT *)
  26 (* ********************** *)
  27
  28 (* elemento: name + nel curId + nel desc *)
  29 inductive var_flatElem : Type ≝
  30 VAR_FLAT_ELEM: aux_str_type → ne_list (option nat) → ne_list desc_elem → var_flatElem.
  31
  32 definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ _ ⇒ n ].
  33 definition get_cur_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ c _ ⇒ c ].
  34 definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ _ d ⇒ d ].
  35
  36 (* ambiente globale: descrittori *)
  37 definition aux_flatEnv_type ≝ Prod nat (list var_flatElem).
  38
  39 (* ambiente vuoto *)
  40 definition empty_flatEnv ≝ pair ?? O (nil var_flatElem).
  41
  42 definition get_depth_flatEnv ≝ λenv:aux_flatEnv_type.match env with [ pair d _ ⇒ d ].
  43 definition get_subEnv_flatEnv ≝ λenv:aux_flatEnv_type.match env with [ pair _ s ⇒ s ].
  44
  45 (* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
  46 let rec enter_flatEnv_aux (subEnv:list var_flatElem) on subEnv ≝
  47  match subEnv with
  48   [ nil ⇒ []
  49   | cons h t ⇒ (VAR_FLAT_ELEM (get_name_flatVar h)
  50                               ((get_first_neList ? (get_cur_flatVar h))§§(get_cur_flatVar h))
  51                               (get_desc_flatVar h))::(enter_flatEnv_aux t)
  52   ].
  53
  54 definition enter_flatEnv ≝
  55 λenv.pair ?? (get_depth_flatEnv env) (enter_flatEnv_aux (get_subEnv_flatEnv env)).
  56
  57 (* leave: elimina la testa (il "cur" corrente) *)
  58 let rec leave_flatEnv_aux (subEnv:list var_flatElem) on subEnv ≝
  59  match subEnv with
  60   [ nil ⇒ []
  61   | cons h t ⇒ (VAR_FLAT_ELEM (get_name_flatVar h)
  62                               (cut_first_neList ? (get_cur_flatVar h))
  63                               (get_desc_flatVar h))::(leave_flatEnv_aux t)
  64   ].
  65
  66 definition leave_flatEnv ≝
  67 λenv.pair ?? (get_depth_flatEnv env) (leave_flatEnv_aux (get_subEnv_flatEnv env)).
  68
  69 (* get_id *)
  70 let rec get_id_flatEnv_aux (subEnv:list var_flatElem) (name:aux_str_type) on subEnv ≝
  71  match subEnv with
  72   [ nil ⇒ None ?
  73   | cons h t ⇒
  74    match (match eqStr_str name (get_name_flatVar h) with
  75           [ true ⇒ get_first_neList ? (get_cur_flatVar h)
  76           | false ⇒ None ?
  77           ]) with
  78    [ None ⇒ get_id_flatEnv_aux t name
  79    | Some x ⇒ Some ? x
  80    ]
  81   ].
  82
  83 definition get_id_flatEnv ≝
  84 λe:aux_flatEnv_type.λstr:aux_str_type.
  85  match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with
  86   [ None ⇒ O  | Some x ⇒ x ].
  87
  88 (* get_desc *)
  89 let rec get_desc_flatEnv_aux (subEnv:list var_flatElem) (name:aux_strId_type) on subEnv ≝
  90  match subEnv with
  91   [ nil ⇒ None ?
  92   | cons h t ⇒
  93    match (match (eqStr_str (get_name_strId name) (get_name_flatVar h))⊗
  94                 (leb (S (get_id_strId name)) (len_neList ? (get_desc_flatVar h))) with
  95           [ true ⇒ nth_neList ? (get_desc_flatVar h) (get_id_strId name)
  96           | false ⇒ None ?
  97           ]) with
  98    [ None ⇒ get_desc_flatEnv_aux t name
  99    | Some x ⇒ Some ? x
 100    ]
 101   ].
 102
 103 definition get_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
 104  match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with
 105   [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
 106
 107 (* check_id *)
 108 definition check_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type.
 109  match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ False | Some _ ⇒ True ].
 110
 111 definition checkb_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type.
 112  match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ false | Some _ ⇒ true ].
 113
 114 lemma checkbidflatenv_to_checkidflatenv : ∀e,str.checkb_id_flatEnv e str = true → check_id_flatEnv e str.
 115  unfold checkb_id_flatEnv;
 116  unfold check_id_flatEnv;
 117  intros;
 118  letin K ≝ (get_id_flatEnv_aux (get_subEnv_flatEnv e) str);
 119  elim K;
 120  [ normalize; autobatch |
 121    normalize; autobatch ]
 122 qed.
 123
 124 definition checknot_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type.
 125  match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ True | Some _ ⇒ False ].
 126
 127 definition checknotb_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type.
 128  match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ true | Some _ ⇒ false ].
 129
 130 lemma checknotbidflatenv_to_checknotidflatenv : ∀e,str.checknotb_id_flatEnv e str = true → checknot_id_flatEnv e str.
 131  unfold checknotb_id_flatEnv;
 132  unfold checknot_id_flatEnv;
 133  intros;
 134  letin K ≝ (get_id_flatEnv_aux (get_subEnv_flatEnv e) str);
 135  elim K;
 136  [ normalize; autobatch |
 137    normalize; autobatch ]
 138 qed.
 139
 140 (* check_desc *)
 141 definition check_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
 142  match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ False | Some _ ⇒ True ].
 143
 144 definition checkb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
 145  match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ false | Some _ ⇒ true ].
 146
 147 lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str = true → check_desc_flatEnv e str.
 148  unfold checkb_desc_flatEnv;
 149  unfold check_desc_flatEnv;
 150  intros;
 151  letin K ≝ (get_desc_flatEnv_aux (get_subEnv_flatEnv e) str);
 152  elim K;
 153  [ normalize; autobatch |
 154    normalize; autobatch ]
 155 qed.
 156
 157 definition checknot_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
 158  match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ True | Some _ ⇒ False ].
 159
 160 definition checknotb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
 161  match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ true | Some _ ⇒ false ].
 162
 163 lemma checknotbdescflatenv_to_checknotdescflatenv : ∀e,str.checknotb_desc_flatEnv e str = true → checknot_desc_flatEnv e str.
 164  unfold checknotb_desc_flatEnv;
 165  unfold checknot_desc_flatEnv;
 166  intros;
 167  letin K ≝ (get_desc_flatEnv_aux (get_subEnv_flatEnv e) str);
 168  elim K;
 169  [ normalize; autobatch |
 170    normalize; autobatch ]
 171 qed.
 172
 173 (* aggiungi descrittore : in testa al primo ambiente *)
 174 let rec previous_cur_from_depth (depth:nat) on depth ≝
 175  match depth with
 176   [ O ⇒ «£(Some ? O)»
 177   | S n ⇒ (previous_cur_from_depth n)&«£(None ?)»
 178   ].
 179
 180 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 ≝
 181  match subEnv with
 182   [ nil ⇒ match flag with
 183    [ true ⇒ []
 184    | false ⇒ [ VAR_FLAT_ELEM str (previous_cur_from_depth depth) «£(DESC_ELEM c desc)» ]
 185    ]
 186   | cons h t ⇒ (match eqStr_str str (get_name_flatVar h) with
 187                 [ true ⇒ VAR_FLAT_ELEM (get_name_flatVar h)
 188                                        («£(Some ? (len_neList ? (get_desc_flatVar h)))»&(cut_first_neList ? (get_cur_flatVar h)))
 189                                        ((get_desc_flatVar h)&«£(DESC_ELEM c desc)»)
 190                 | false ⇒ h
 191                 ])::(add_desc_flatEnv_aux t str c desc depth ((eqStr_str str (get_name_flatVar h)⊕flag)))
 192   ].
 193
 194 definition add_desc_flatEnv ≝ λenv,str,c,desc.add_desc_flatEnv_aux (get_subEnv_flatEnv env) str c desc (get_depth_flatEnv env) false.
 195
 196 (* equivalenza *)
 197 definition env_to_flatEnv ≝
 198  λe,fe.∀str.
 199   check_desc_env e str →
 200   check_id_flatEnv fe str →
 201   check_desc_flatEnv fe (STR_ID str (get_id_flatEnv fe str)) →
 202   get_desc_env e str = get_desc_flatEnv fe (STR_ID str (get_id_flatEnv fe str)).
 203
 204 lemma empty_env_to_flatEnv : env_to_flatEnv empty_env empty_flatEnv.
 205  unfold env_to_flatEnv;
 206  unfold empty_env;
 207  unfold empty_flatEnv;
 208  simplify;
 209  intros;
 210  reflexivity.
 211 qed.
 212
 213 lemma getdescenv_to_enter : ∀e,str.get_desc_env e str = get_desc_env (enter_env e) str.
 214  intros 2;
 215  elim e;
 216  reflexivity.
 217 qed.
 218
 219 lemma enter_env_to_flatEnv :
 220  ∀e,fe.env_to_flatEnv e fe → env_to_flatEnv (enter_env e) (enter_flatEnv fe).
 221  intros 2;
 222  unfold env_to_flatEnv;
 223  intros;
 224  lapply (H str H1);
 225  [ rewrite < (getdescenv_to_enter e str);
 226    rewrite > Hletin;
 227
 228
 229
 230
 231
 232
 233
 234
 235
 236