1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
18 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
20 (* ********************************************************************** *)
22 include "compiler/environment.ma".
24 (* ********************** *)
25 (* GESTIONE AMBIENTE FLAT *)
26 (* ********************** *)
28 (* STRUTTURA AMBIENTE FLAT *)
30 (* elemento: name + desc *)
31 inductive flatVar_elem : Type ≝
32 VAR_FLAT_ELEM: aux_strId_type → desc_elem → flatVar_elem.
35 definition aux_flatEnv_type ≝ list flatVar_elem.
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 ].
42 definition empty_flatEnv ≝ nil flatVar_elem.
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 ≝
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 ]].
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 ].
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 ].
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 ].
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;
67 letin K ≝ (get_desc_flatEnv_aux e str);
69 [ normalize; autobatch |
70 normalize; autobatch ]
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.
78 (* STRUTTURA MAPPA TRASFORMAZIONE *)
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.
85 definition aux_trasfMap_type ≝ λe,fe.list (maxCur_elem e fe).
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 ].
92 (* mappa di trasformazione vuota *)
93 definition empty_trasfMap ≝ λe,fe.nil (maxCur_elem e fe).
95 (* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *)
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 ≝
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 ]].
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))
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)
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)).
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))).
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) ≝
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) ]
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)
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))
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.
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.
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' ≝
181 [ nil ⇒ empty_trasfMap e fe'
183 match get_maxcur_map e fe snap (get_name_maxCur ?? h) with
184 [ None ⇒ retype_enter_leave_to_e e fe' f [h]
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
191 (* sequenza di utilizzo:
195 |DICHIARAZIONE "pippo":
196 | -) MAP1 <- add_maxcur_map MAP0 "pippo"
197 | -) ENV1 <- add_desc_flatEnv ENV0 (name_to_nameId MAP1 "pippo") DESC
200 | -) name_to_nameId MAP1 "pippo"
202 |PREPARAZIONE ENTRATA BLOCCO INTERNO:
203 | -) SNAP <- build_snapshot MAP1
207 |DICHIARAZIONE "pippo":
208 | -) MAP2 <- add_maxcur_map MAP1 "pippo"
209 | -) ENV2 <- add_desc_flatEnv ENV (name_to_nameId MAP2 "pippo") DESC
212 | -) name_to_nameId MAP2 "pippo"
214 |PREPARAZIONE USCITA BLOCCO INTERNO:
215 | -) MAP3 <- rollback_map MAP2 SNAP
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).
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.
237 definition env2' ≝ enter_env env2.
238 definition map2' ≝ retype_e_to_enter env2 fenv2 map2.
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.
247 definition env4' ≝ enter_env env4.
248 definition map4' ≝ retype_e_to_enter env4 fenv4 map4.
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.
257 definition map6' ≝ retype_e_to_leave env6 fenv6 map6.
259 definition map7 ≝ rollback_map env4 fenv4 fenv6 (λx.add_desc_env (add_desc_env x pippo false pippodesc3) pluto false plutodesc3) map6' map4.
261 definition map7' ≝ retype_e_to_leave env4 fenv6 map7.
263 definition map8 ≝ rollback_map env2 fenv2 fenv6 (λx.add_desc_env (add_desc_env x pippo true pippodesc2) pluto true plutodesc2) map7' map2.