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 (* STRUTTURA MAPPA TRASFORMAZIONE *)
  45
  46 (* elemento: nome + max + cur *)
  47 inductive maxCur_elem : Type ≝
  48 MAX_CUR_ELEM: aux_str_type → nat → nat → maxCur_elem.
  49
  50 (* tipo pubblico *)
  51 definition aux_trasfMap_type ≝ list maxCur_elem.
  52
  53 (* getter *)
  54 definition get_name_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM n _ _ ⇒ n ].
  55 definition get_max_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM _ m _ ⇒ m ].
  56 definition get_cur_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM _ _ c ⇒ c ].
  57
  58 (* mappa di trasformazione vuota *)
  59 definition empty_trasfMap ≝ nil maxCur_elem.
  60
  61 (* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *)
  62
  63 (* recupera descrittore da mappa trasformazione : dummy se non esiste (impossibile) *)
  64 let rec get_maxcur_from_map_aux (map:aux_trasfMap_type) (str:aux_str_type) (dummy:option maxCur_elem) on map ≝
  65  match map with
  66   [ nil ⇒ dummy
  67   | cons h tl ⇒ match strCmp_str str (get_name_maxCur h) with
  68    [ true ⇒ Some ? h | false ⇒ get_maxcur_from_map_aux tl str dummy ]].
  69
  70 definition get_maxcur_from_map ≝
  71 λmap:aux_trasfMap_type.λstr:aux_str_type.
  72  match get_maxcur_from_map_aux map str (None ?) with
  73   [ None ⇒ MAX_CUR_ELEM str 0 0 | Some x ⇒ x ].
  74
  75 (* aggiungi/aggiorna descrittore mappa trasformazione *)
  76 let rec add_maxcur_map_aux (map:aux_trasfMap_type) (str:aux_str_type) (flag:bool) on map ≝
  77  match map with
  78   [ nil ⇒ match flag with
  79     [ true ⇒ []
  80     | false ⇒ [MAX_CUR_ELEM str 0 0]
  81     ]
  82   | cons h tl ⇒ match strCmp_str str (get_name_maxCur h) with
  83    [ true ⇒ [MAX_CUR_ELEM str (S (get_max_maxCur h)) (S (get_max_maxCur h))]@(add_maxcur_map_aux tl str true)
  84    | false ⇒ [h]@(add_maxcur_map_aux tl str flag)
  85    ]
  86   ].
  87
  88 definition add_maxcur_map ≝
  89 λmap:aux_trasfMap_type.λstr:aux_str_type.add_maxcur_map_aux map str false.
  90
  91 (* nome -> nome + id *)
  92 definition name_to_nameId ≝
  93 λmap:aux_trasfMap_type.λstr:aux_str_type.
  94  STR_ID str (get_cur_maxCur (get_maxcur_from_map map str)).
  95
  96 (* recupera descrittore da ambiente : dummy se non esiste (impossibile) *)
  97 let rec get_desc_from_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) (dummy:option desc_elem) on e ≝
  98 match e with
  99  [ nil ⇒ dummy
 100  | cons h tl ⇒ match strCmp_strId str (get_nameId_flatVar h) with
 101   [ true ⇒ Some ? (get_desc_flatVar h)
 102   | false ⇒ get_desc_from_flatEnv_aux tl str dummy ]].
 103
 104 definition get_desc_from_flatEnv ≝
 105 λe:aux_flatEnv_type.λstr:aux_strId_type.
 106  match get_desc_from_flatEnv_aux e str (None ?) with
 107   [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
 108
 109 (* aggiungi descrittore ad ambiente *)
 110 definition add_desc_flatEnv ≝
 111 λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
 112  e@[ VAR_FLAT_ELEM str (DESC_ELEM b t) ].
 113
 114 (* snapshot della mappa trasformazione *)
 115 let rec build_snapshot (map:aux_trasfMap_type) on map ≝
 116  match map with
 117   [ nil ⇒ []
 118   | cons h tl ⇒ [ STR_ID (get_name_maxCur h) (get_cur_maxCur h) ]@(build_snapshot tl)
 119   ].
 120
 121 (* uscita da un blocco, rollback di cur in mappa di trasformazione *)
 122 let rec find_in_snapshot (snap:list aux_strId_type) (str:aux_str_type) on snap ≝
 123  match snap with
 124   [ nil ⇒ None ?
 125   | cons h tl ⇒ match strCmp_str str (get_name_strId h) with
 126    [ true ⇒ Some ? (get_id_strId h)
 127    | false ⇒ find_in_snapshot tl str
 128    ]
 129   ].
 130
 131 let rec rollback_map (map:aux_trasfMap_type) (snap:list aux_strId_type) on map ≝
 132  match map with
 133   [ nil ⇒ empty_trasfMap
 134   | cons h tl ⇒ match find_in_snapshot snap (get_name_maxCur h) with
 135    [ None ⇒ [h]
 136    | Some newCur ⇒ [ MAX_CUR_ELEM (get_name_maxCur h) (get_max_maxCur h) newCur ]
 137    ]@(rollback_map tl snap)
 138   ].
 139
 140 (* sequenza di utilizzo:
 141
 142 [BLOCCO ESTERNO]
 143
 144 |DICHIARAZIONE "pippo":
 145 | -) MAP1 <- add_maxcur_map MAP0 "pippo"
 146 | -) ENV1 <- add_desc_flatEnv ENV0 (name_to_nameId MAP1 "pippo") DESC
 147 |
 148 |ACCESSO "pippo":
 149 | -) name_to_nameId MAP1 "pippo"
 150 |
 151 |PREPARAZIONE ENTRATA BLOCCO INTERNO:
 152 | -) SNAP <- build_snapshot MAP1
 153
 154   |[BLOCCO INTERNO]
 155   |
 156   |DICHIARAZIONE "pippo":
 157   |  -) MAP2 <- add_maxcur_map MAP1 "pippo"
 158   |  -) ENV2 <- add_desc_flatEnv ENV (name_to_nameId MAP2 "pippo") DESC
 159   |
 160   |ACCESSO "pippo":
 161   | -) name_to_nameId MAP2 "pippo"
 162   |
 163   |PREPARAZIONE USCITA BLOCCO INTERNO:
 164   | -) MAP3 <- rollback_map MAP2 SNAP
 165
 166 | ...
 167 *)
 168
 169 (* mini test
 170 definition pippo ≝ [ ch_P ].
 171 definition pluto ≝ [ ch_Q ].
 172 definition pippodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
 173 definition pippodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
 174 definition pippodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2).
 175 definition plutodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
 176 definition plutodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
 177 definition plutodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_WORD16) 2).
 178
 179 definition map1 ≝ add_maxcur_map empty_trasfMap pippo.
 180 definition env1 ≝ add_desc_flatEnv empty_flatEnv (name_to_nameId map1 pippo) pippodesc1.
 181 definition map2 ≝ add_maxcur_map map1 pluto.
 182 definition env2 ≝ add_desc_flatEnv env1 (name_to_nameId map2 pluto) plutodesc1.
 183
 184 definition snap1 ≝ build_snapshot map2.
 185
 186 definition map3 ≝ add_maxcur_map map2 pippo.
 187 definition env3 ≝ add_desc_flatEnv env2 (name_to_nameId map3 pippo) pippodesc2.
 188 definition map4 ≝ add_maxcur_map map3 pluto.
 189 definition env4 ≝ add_desc_flatEnv env3 (name_to_nameId map4 pluto) plutodesc2.
 190
 191 definition snap2 ≝ build_snapshot map4.
 192
 193 definition map5 ≝ add_maxcur_map map4 pippo.
 194 definition env5 ≝ add_desc_flatEnv env4 (name_to_nameId map5 pippo) pippodesc3.
 195 definition map6 ≝ add_maxcur_map map5 pluto.
 196 definition env6 ≝ add_desc_flatEnv env5 (name_to_nameId map6 pluto) plutodesc3.
 197
 198 definition map7 ≝ rollback_map map6 snap2.
 199
 200 definition map8 ≝ rollback_map map7 snap1.
 201
 202 lemma checkenv : None ? = Some ? env6.
 203 normalize; elim daemon.
 204 qed.
 205
 206 lemma checkmap : None ? = Some ? map8.
 207 normalize; elim daemon.
 208 qed.
 209
 210 lemma checksnap : None ? = Some ? snap2.
 211 normalize; elim daemon.
 212 qed.
 213 *)