--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* ********************** *)
+
+(* STRUTTURA AMBIENTE FLAT *)
+
+(* elemento: name + desc *)
+inductive flatVar_elem : Type ≝
+VAR_FLAT_ELEM: aux_strId_type → desc_elem → flatVar_elem.
+
+(* tipo pubblico *)
+definition aux_flatEnv_type ≝ list flatVar_elem.
+
+(* getter *)
+definition get_nameId_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
+definition get_desc_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
+
+(* ambiente vuoto *)
+definition empty_flatEnv ≝ nil flatVar_elem.
+
+(* STRUTTURA MAPPA TRASFORMAZIONE *)
+
+(* elemento: nome + max + cur *)
+inductive maxCur_elem : Type ≝
+MAX_CUR_ELEM: aux_str_type → nat → nat → maxCur_elem.
+
+(* tipo pubblico *)
+definition aux_trasfMap_type ≝ list maxCur_elem.
+
+(* getter *)
+definition get_name_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM n _ _ ⇒ n ].
+definition get_max_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM _ m _ ⇒ m ].
+definition get_cur_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM _ _ c ⇒ c ].
+
+(* mappa di trasformazione vuota *)
+definition empty_trasfMap ≝ nil maxCur_elem.
+
+(* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *)
+
+(* recupera descrittore da mappa trasformazione : dummy se non esiste (impossibile) *)
+let rec get_maxcur_from_map_aux (map:aux_trasfMap_type) (str:aux_str_type) (dummy:option maxCur_elem) on map ≝
+ match map with
+ [ nil ⇒ dummy
+ | cons h tl ⇒ match strCmp_str str (get_name_maxCur h) with
+ [ true ⇒ Some ? h | false ⇒ get_maxcur_from_map_aux tl str dummy ]].
+
+definition get_maxcur_from_map ≝
+λmap:aux_trasfMap_type.λstr:aux_str_type.
+ match get_maxcur_from_map_aux map str (None ?) with
+ [ None ⇒ MAX_CUR_ELEM str 0 0 | Some x ⇒ x ].
+
+(* aggiungi/aggiorna descrittore mappa trasformazione *)
+let rec add_maxcur_map_aux (map:aux_trasfMap_type) (str:aux_str_type) (flag:bool) on map ≝
+ match map with
+ [ nil ⇒ match flag with
+ [ true ⇒ []
+ | false ⇒ [MAX_CUR_ELEM str 0 0]
+ ]
+ | cons h tl ⇒ match strCmp_str str (get_name_maxCur h) with
+ [ true ⇒ [MAX_CUR_ELEM str (S (get_max_maxCur h)) (S (get_max_maxCur h))]@(add_maxcur_map_aux tl str true)
+ | false ⇒ [h]@(add_maxcur_map_aux tl str flag)
+ ]
+ ].
+
+definition add_maxcur_map ≝
+λmap:aux_trasfMap_type.λstr:aux_str_type.add_maxcur_map_aux map str false.
+
+(* nome -> nome + id *)
+definition name_to_nameId ≝
+λmap:aux_trasfMap_type.λstr:aux_str_type.
+ STR_ID str (get_cur_maxCur (get_maxcur_from_map map str)).
+
+(* recupera descrittore da ambiente : dummy se non esiste (impossibile) *)
+let rec get_desc_from_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) (dummy:option desc_elem) on e ≝
+match e with
+ [ nil ⇒ dummy
+ | cons h tl ⇒ match strCmp_strId str (get_nameId_flatVar h) with
+ [ true ⇒ Some ? (get_desc_flatVar h)
+ | false ⇒ get_desc_from_flatEnv_aux tl str dummy ]].
+
+definition get_desc_from_flatEnv ≝
+λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_from_flatEnv_aux e str (None ?) with
+ [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
+
+(* aggiungi descrittore ad ambiente *)
+definition add_desc_flatEnv ≝
+λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
+ e@[ VAR_FLAT_ELEM str (DESC_ELEM b t) ].
+
+(* snapshot della mappa trasformazione *)
+let rec build_snapshot (map:aux_trasfMap_type) on map ≝
+ match map with
+ [ nil ⇒ []
+ | cons h tl ⇒ [ STR_ID (get_name_maxCur h) (get_cur_maxCur h) ]@(build_snapshot tl)
+ ].
+
+(* uscita da un blocco, rollback di cur in mappa di trasformazione *)
+let rec find_in_snapshot (snap:list aux_strId_type) (str:aux_str_type) on snap ≝
+ match snap with
+ [ nil ⇒ None ?
+ | cons h tl ⇒ match strCmp_str str (get_name_strId h) with
+ [ true ⇒ Some ? (get_id_strId h)
+ | false ⇒ find_in_snapshot tl str
+ ]
+ ].
+
+let rec rollback_map (map:aux_trasfMap_type) (snap:list aux_strId_type) on map ≝
+ match map with
+ [ nil ⇒ empty_trasfMap
+ | cons h tl ⇒ match find_in_snapshot snap (get_name_maxCur h) with
+ [ None ⇒ [h]
+ | Some newCur ⇒ [ MAX_CUR_ELEM (get_name_maxCur h) (get_max_maxCur h) newCur ]
+ ]@(rollback_map tl snap)
+ ].
+
+(* sequenza di utilizzo:
+
+[BLOCCO ESTERNO]
+
+|DICHIARAZIONE "pippo":
+| -) MAP1 <- add_maxcur_map MAP0 "pippo"
+| -) ENV1 <- add_desc_flatEnv ENV0 (name_to_nameId MAP1 "pippo") DESC
+|
+|ACCESSO "pippo":
+| -) name_to_nameId MAP1 "pippo"
+|
+|PREPARAZIONE ENTRATA BLOCCO INTERNO:
+| -) SNAP <- build_snapshot MAP1
+
+ |[BLOCCO INTERNO]
+ |
+ |DICHIARAZIONE "pippo":
+ | -) MAP2 <- add_maxcur_map MAP1 "pippo"
+ | -) ENV2 <- add_desc_flatEnv ENV (name_to_nameId MAP2 "pippo") DESC
+ |
+ |ACCESSO "pippo":
+ | -) name_to_nameId MAP2 "pippo"
+ |
+ |PREPARAZIONE USCITA BLOCCO INTERNO:
+ | -) MAP3 <- rollback_map MAP2 SNAP
+
+| ...
+*)
+
+(* mini test
+definition pippo ≝ [ ch_P ].
+definition pluto ≝ [ ch_Q ].
+definition pippodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
+definition pippodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
+definition pippodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2).
+definition plutodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
+definition plutodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
+definition plutodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_WORD16) 2).
+
+definition map1 ≝ add_maxcur_map empty_trasfMap pippo.
+definition env1 ≝ add_desc_flatEnv empty_flatEnv (name_to_nameId map1 pippo) pippodesc1.
+definition map2 ≝ add_maxcur_map map1 pluto.
+definition env2 ≝ add_desc_flatEnv env1 (name_to_nameId map2 pluto) plutodesc1.
+
+definition snap1 ≝ build_snapshot map2.
+
+definition map3 ≝ add_maxcur_map map2 pippo.
+definition env3 ≝ add_desc_flatEnv env2 (name_to_nameId map3 pippo) pippodesc2.
+definition map4 ≝ add_maxcur_map map3 pluto.
+definition env4 ≝ add_desc_flatEnv env3 (name_to_nameId map4 pluto) plutodesc2.
+
+definition snap2 ≝ build_snapshot map4.
+
+definition map5 ≝ add_maxcur_map map4 pippo.
+definition env5 ≝ add_desc_flatEnv env4 (name_to_nameId map5 pippo) pippodesc3.
+definition map6 ≝ add_maxcur_map map5 pluto.
+definition env6 ≝ add_desc_flatEnv env5 (name_to_nameId map6 pluto) plutodesc3.
+
+definition map7 ≝ rollback_map map6 snap2.
+
+definition map8 ≝ rollback_map map7 snap1.
+
+lemma checkenv : None ? = Some ? env6.
+normalize; elim daemon.
+qed.
+
+lemma checkmap : None ? = Some ? map8.
+normalize; elim daemon.
+qed.
+
+lemma checksnap : None ? = Some ? snap2.
+normalize; elim daemon.
+qed.
+*)
projects / helm.git / blobdiff