helm/software/matita/contribs/assembly/compiler/env_to_flatenv.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 (* STRUTTURA AMBIENTE FLAT *)
  29
  30 (* elemento: name + desc *)
  31 inductive flatVar_elem : Type ≝
  32 VAR_FLAT_ELEM: aux_strId_type → desc_elem → flatVar_elem.
  33
  34 (* tipo pubblico *)
  35 definition aux_flatEnv_type ≝ list flatVar_elem.
  36
  37 (* getter *)
  38 definition get_nameId_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
  39 definition get_desc_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
  40
  41 (* ambiente vuoto *)
  42 definition empty_flatEnv ≝ nil flatVar_elem.
  43
  44 (* recupera descrittore da ambiente : dummy se non esiste (impossibile) *)
  45 let rec get_desc_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) on e ≝
  46 match e with
  47  [ nil ⇒ None ?
  48  | cons h tl ⇒ match strCmp_strId str (get_nameId_flatVar h) with
  49   [ true ⇒ Some ? (get_desc_flatVar h)
  50   | false ⇒ get_desc_flatEnv_aux tl str ]].
  51
  52 definition get_desc_flatEnv ≝
  53 λe:aux_flatEnv_type.λstr:aux_strId_type.
  54  match get_desc_flatEnv_aux e str with
  55   [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
  56
  57 definition check_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
  58  match get_desc_flatEnv_aux e str with [ None ⇒ False | Some _ ⇒ True ].
  59
  60 definition checkb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
  61  match get_desc_flatEnv_aux e str with [ None ⇒ false | Some _ ⇒ true ].
  62
  63 lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str = true → check_desc_flatEnv e str.
  64  unfold checkb_desc_flatEnv;
  65  unfold check_desc_flatEnv;
  66  intros;
  67  letin K ≝ (get_desc_flatEnv_aux e str);
  68  elim K;
  69  [ normalize; autobatch |
  70    normalize; autobatch ]
  71 qed.
  72
  73 (* aggiungi descrittore ad ambiente: in testa *)
  74 definition add_desc_flatEnv ≝
  75 λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
  76  (VAR_FLAT_ELEM str (DESC_ELEM b t))::e.
  77
  78 (* STRUTTURA MAPPA TRASFORMAZIONE *)
  79
  80 (* elemento: nome + cur + max + dimostrazione *)
  81 inductive maxCur_elem (e:aux_env_type) (fe:aux_flatEnv_type) : Type ≝
  82 MAX_CUR_ELEM: ∀str:aux_str_type.∀cur:nat.nat → (check_desc_env e str → get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) → maxCur_elem e fe.
  83
  84 (* tipo pubblico *)
  85 definition aux_trasfMap_type ≝ λe,fe.list (maxCur_elem e fe).
  86
  87 (* getter *)
  88 definition get_name_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM n _ _ _ ⇒ n ].
  89 definition get_cur_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM _ c _ _ ⇒ c ].
  90 definition get_max_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM _ _ m _ ⇒ m ].
  91
  92 (* mappa di trasformazione vuota *)
  93 definition empty_trasfMap ≝ λe,fe.nil (maxCur_elem e fe).
  94
  95 (* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *)
  96
  97 (* recupera descrittore da mappa trasformazione : dummy se non esiste (impossibile) *)
  98 let rec get_maxcur_map (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) (str:aux_str_type) on map ≝
  99  match map with
 100   [ nil ⇒ None ?
 101   | cons h tl ⇒ match strCmp_str str (get_name_maxCur e fe h) with
 102    [ true ⇒ Some ? h | false ⇒ get_maxcur_map e fe tl str ]].
 103
 104 (* prossimo nome *)
 105 definition next_nameId ≝
 106 λe,fe.λmap:aux_trasfMap_type e fe.λstr:aux_str_type.
 107  match get_maxcur_map e fe map str with
 108   [ None ⇒ STR_ID str 0
 109   | Some maxcur ⇒ STR_ID str (S (get_max_maxCur e fe maxcur))
 110   ].
 111
 112 (* nome -> nome + id *)
 113 definition name_to_nameId ≝
 114 λe,fe.λmap:aux_trasfMap_type e fe.λstr:aux_str_type.
 115  match get_maxcur_map e fe map str with
 116   [ None ⇒ STR_ID str 0
 117   | Some maxcur ⇒ STR_ID str (get_cur_maxCur e fe maxcur)
 118   ].
 119
 120 (* NB: se cerco qualcos'altro il risultato e' invariato *)
 121 axiom add_maxcur_map_aux_false : ∀e,fe,str,cur,str',b',desc',map.
 122 (check_desc_env e str →
 123  get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
 124 (strCmp_str str str' = false) →
 125 (check_desc_env (add_desc_env e str' b' desc') str →
 126  get_desc_env (add_desc_env e str' b' desc') str =
 127  get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str cur)).
 128
 129 (* NB: se cerco cio' che e' appena stato aggiunto, deve essere uguale *)
 130 axiom add_maxcur_map_aux_true : ∀e,fe,str,cur,max,str',b',desc',map.
 131 (check_desc_env e str →
 132  get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
 133 (strCmp_str str str' = true) →
 134 (check_desc_env (add_desc_env e str' b' desc') str →
 135  get_desc_env (add_desc_env e str' b' desc') str =
 136  get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str (S max))).
 137
 138 (* aggiungi/aggiorna descrittore mappa trasformazione *)
 139 let rec add_maxcur_map_aux (e:aux_env_type) (fe:aux_flatEnv_type) (map,fMap:aux_trasfMap_type e fe)
 140                            (str:aux_str_type) (b:bool) (desc:ast_type) (flag:bool) on map
 141  : aux_trasfMap_type (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc) ≝
 142 match map with
 143  [ nil ⇒
 144     match flag with
 145      [ true ⇒ []
 146      | false ⇒
 147         [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
 148            str O O (False_rect ? daemon) ]
 149      ]
 150  | cons h tl ⇒ match h with
 151   [ MAX_CUR_ELEM str' cur' max' dim' ⇒
 152      match strCmp_str str' str return λx.(strCmp_str str' str = x) → ? with
 153       [ true ⇒ λp:(strCmp_str str' str = true).
 154             [ MAX_CUR_ELEM  (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
 155                             str' (S max') (S max')
 156                             (add_maxcur_map_aux_true e fe str' cur' max' str b desc fMap dim' p)
 157             ]@(add_maxcur_map_aux e fe tl fMap str b desc true)
 158       | false ⇒ λp:(strCmp_str str' str = false).
 159              [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
 160                             str' cur' max'
 161                             (add_maxcur_map_aux_false e fe str' cur' str b desc fMap dim' p)
 162              ]@(add_maxcur_map_aux e fe tl fMap str b desc flag)
 163       ] (refl_eq ? (strCmp_str str' str))
 164   ]
 165  ].
 166
 167 definition add_maxcur_map ≝
 168 λe:aux_env_type.λfe:aux_flatEnv_type.λmap,fMap:aux_trasfMap_type e fe.λstr:aux_str_type.λb:bool.λdesc:ast_type.
 169 add_maxcur_map_aux e fe map fMap str b desc false.
 170
 171 (* NB: leave ... enter e' equivalente a e originale *)
 172 axiom retype_enter_leave_to_e: ∀e,fe,f. aux_trasfMap_type (leave_env (f (enter_env e))) fe → aux_trasfMap_type e fe.
 173 (* NB: enter non cambia fe *)
 174 axiom retype_e_to_enter: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (enter_env e) fe.
 175 (* NB: leave non cambia fe *)
 176 axiom retype_e_to_leave: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (leave_env e) fe.
 177
 178 let rec rollback_map (e:aux_env_type) (fe,fe':aux_flatEnv_type) (f:aux_env_type → aux_env_type) (map:aux_trasfMap_type (leave_env (f (enter_env e))) fe')
 179  (snap:aux_trasfMap_type e fe) on map : aux_trasfMap_type e fe' ≝
 180  match map with
 181   [ nil ⇒ empty_trasfMap e fe'
 182   | cons h tl ⇒
 183      match get_maxcur_map e fe snap (get_name_maxCur ?? h) with
 184    [ None ⇒ retype_enter_leave_to_e e fe' f [h]
 185    | Some new ⇒
 186       [ MAX_CUR_ELEM ?? (get_name_maxCur ?? h) (get_cur_maxCur ?? new)
 187         (get_max_maxCur ?? h) (False_rect ? daemon) ]
 188    ] @ rollback_map e fe fe' f tl snap
 189   ].
 190
 191 (* sequenza di utilizzo:
 192
 193 [BLOCCO ESTERNO]
 194
 195 |DICHIARAZIONE "pippo":
 196 | -) MAP1 <- add_maxcur_map MAP0 "pippo"
 197 | -) ENV1 <- add_desc_flatEnv ENV0 (name_to_nameId MAP1 "pippo") DESC
 198 |
 199 |ACCESSO "pippo":
 200 | -) name_to_nameId MAP1 "pippo"
 201 |
 202 |PREPARAZIONE ENTRATA BLOCCO INTERNO:
 203 | -) SNAP <- build_snapshot MAP1
 204
 205   |[BLOCCO INTERNO]
 206   |
 207   |DICHIARAZIONE "pippo":
 208   |  -) MAP2 <- add_maxcur_map MAP1 "pippo"
 209   |  -) ENV2 <- add_desc_flatEnv ENV (name_to_nameId MAP2 "pippo") DESC
 210   |
 211   |ACCESSO "pippo":
 212   | -) name_to_nameId MAP2 "pippo"
 213   |
 214   |PREPARAZIONE USCITA BLOCCO INTERNO:
 215   | -) MAP3 <- rollback_map MAP2 SNAP
 216
 217 | ...
 218 *)
 219
 220 (* mini test
 221 definition pippo ≝ [ ch_P ].
 222 definition pluto ≝ [ ch_Q ].
 223 definition pippodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
 224 definition pippodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
 225 definition pippodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32).
 226 definition plutodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
 227 definition plutodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
 228 definition plutodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32).
 229
 230 definition map1 ≝ add_maxcur_map empty_env empty_flatEnv (empty_trasfMap ??) (empty_trasfMap ??) pippo false pippodesc1.
 231 definition env1 ≝ add_desc_env empty_env pippo false pippodesc1.
 232 definition fenv1 ≝ add_desc_flatEnv empty_flatEnv (next_nameId empty_env empty_flatEnv (empty_trasfMap ??) pippo) false pippodesc1.
 233 definition map2 ≝ add_maxcur_map env1 fenv1 map1 map1 pluto false plutodesc1.
 234 definition env2 ≝ add_desc_env env1 pluto false plutodesc1.
 235 definition fenv2 ≝ add_desc_flatEnv fenv1 (next_nameId ?? map1 pluto) false plutodesc1.
 236
 237 definition env2' ≝ enter_env env2.
 238 definition map2' ≝ retype_e_to_enter env2 fenv2 map2.
 239
 240 definition map3 ≝ add_maxcur_map env2' fenv2 map2' map2' pippo true pippodesc2.
 241 definition env3 ≝ add_desc_env env2' pippo true pippodesc2.
 242 definition fenv3 ≝ add_desc_flatEnv fenv2 (next_nameId ?? map2' pippo) true pippodesc2.
 243 definition map4 ≝ add_maxcur_map env3 fenv3 map3 map3 pluto true plutodesc2.
 244 definition env4 ≝ add_desc_env env3 pluto true plutodesc2.
 245 definition fenv4 ≝ add_desc_flatEnv fenv3 (next_nameId ?? map3 pluto) true plutodesc2.
 246
 247 definition env4' ≝ enter_env env4.
 248 definition map4' ≝ retype_e_to_enter env4 fenv4 map4.
 249
 250 definition map5 ≝ add_maxcur_map env4' fenv4 map4' map4' pippo false pippodesc3.
 251 definition env5 ≝ add_desc_env env4' pippo false pippodesc3.
 252 definition fenv5 ≝ add_desc_flatEnv fenv4 (next_nameId ?? map4' pippo) false pippodesc3.
 253 definition map6 ≝ add_maxcur_map env5 fenv5 map5 map5 pluto false plutodesc3.
 254 definition env6 ≝ add_desc_env env5 pluto false plutodesc3.
 255 definition fenv6 ≝ add_desc_flatEnv fenv5 (next_nameId ?? map5 pluto) false plutodesc3.
 256
 257 definition map6' ≝ retype_e_to_leave env6 fenv6 map6.
 258
 259 definition map7 ≝ rollback_map env4 fenv4 fenv6 (λx.add_desc_env (add_desc_env x pippo false pippodesc3) pluto false plutodesc3) map6' map4.
 260
 261 definition map7' ≝ retype_e_to_leave env4 fenv6 map7.
 262
 263 definition map8 ≝ rollback_map env2 fenv2 fenv6 (λx.add_desc_env (add_desc_env x pippo true pippodesc2) pluto true plutodesc2) map7' map2.
 264 *)