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 (* 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.
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 ].
36 (* ambiente globale: descrittori *)
37 definition aux_flatEnv_type ≝ Prod nat (list var_flatElem).
40 definition empty_flatEnv ≝ pair ?? O (nil var_flatElem).
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 ].
45 (* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
46 let rec enter_flatEnv_aux (subEnv:list var_flatElem) on subEnv ≝
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)
54 definition enter_flatEnv ≝
55 λenv.pair ?? (get_depth_flatEnv env) (enter_flatEnv_aux (get_subEnv_flatEnv env)).
57 (* leave: elimina la testa (il "cur" corrente) *)
58 let rec leave_flatEnv_aux (subEnv:list var_flatElem) on subEnv ≝
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)
66 definition leave_flatEnv ≝
67 λenv.pair ?? (get_depth_flatEnv env) (leave_flatEnv_aux (get_subEnv_flatEnv env)).
70 let rec get_id_flatEnv_aux (subEnv:list var_flatElem) (name:aux_str_type) on subEnv ≝
74 match (match eqStr_str name (get_name_flatVar h) with
75 [ true ⇒ get_first_neList ? (get_cur_flatVar h)
78 [ None ⇒ get_id_flatEnv_aux t name
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 ].
89 let rec get_desc_flatEnv_aux (subEnv:list var_flatElem) (name:aux_strId_type) on subEnv ≝
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)
98 [ None ⇒ get_desc_flatEnv_aux t name
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 ].
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 ].
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 ].
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;
118 letin K ≝ (get_id_flatEnv_aux (get_subEnv_flatEnv e) str);
120 [ normalize; autobatch |
121 normalize; autobatch ]
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 ].
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 ].
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;
134 letin K ≝ (get_id_flatEnv_aux (get_subEnv_flatEnv e) str);
136 [ normalize; autobatch |
137 normalize; autobatch ]
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 ].
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 ].
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;
151 letin K ≝ (get_desc_flatEnv_aux (get_subEnv_flatEnv e) str);
153 [ normalize; autobatch |
154 normalize; autobatch ]
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 ].
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 ].
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;
167 letin K ≝ (get_desc_flatEnv_aux (get_subEnv_flatEnv e) str);
169 [ normalize; autobatch |
170 normalize; autobatch ]
173 (* aggiungi descrittore : in testa al primo ambiente *)
174 let rec previous_cur_from_depth (depth:nat) on depth ≝
177 | S n ⇒ (previous_cur_from_depth n)&«£(None ?)»
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 ≝
182 [ nil ⇒ match flag with
184 | false ⇒ [ VAR_FLAT_ELEM str (previous_cur_from_depth depth) «£(DESC_ELEM c desc)» ]
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)»)
191 ])::(add_desc_flatEnv_aux t str c desc depth ((eqStr_str str (get_name_flatVar h)⊕flag)))
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.
197 definition env_to_flatEnv ≝
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)).
204 lemma empty_env_to_flatEnv : env_to_flatEnv empty_env empty_flatEnv.
205 unfold env_to_flatEnv;
207 unfold empty_flatEnv;
213 lemma getdescenv_to_enter : ∀e,str.get_desc_env e str = get_desc_env (enter_env e) str.
219 lemma enter_env_to_flatEnv :
220 ∀e,fe.env_to_flatEnv e fe → env_to_flatEnv (enter_env e) (enter_flatEnv fe).
222 unfold env_to_flatEnv;
225 [ rewrite < (getdescenv_to_enter e str);