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 (* ********************** *)
29 inductive var_flatElem : Type ≝
30 VAR_FLAT_ELEM: aux_strId_type → desc_elem → var_flatElem.
32 definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
33 definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
35 definition aux_flatEnv_type ≝ list var_flatElem.
37 definition empty_flatEnv ≝ nil var_flatElem.
39 (* mappa: nome + max + cur *)
40 inductive n_list : nat → Type ≝
42 | n_cons: ∀n.option nat → n_list n → n_list (S n).
44 definition defined_nList ≝
45 λd.λl:n_list d.match l with [ n_nil ⇒ False | n_cons _ _ _ ⇒ True ].
47 definition cut_first_nList : Πd.n_list d → ? → n_list (pred d) ≝
48 λd.λl:n_list d.λp:defined_nList ? l.
51 return λX.λY:n_list X.defined_nList X Y → n_list (pred X)
53 [ n_nil ⇒ λp:defined_nList O n_nil.False_rect ? p
54 | n_cons n h t ⇒ λp:defined_nList (S n) (n_cons n h t).t
57 definition get_first_nList : Πd.n_list d → ? → option nat ≝
58 λd.λl:n_list d.λp:defined_nList ? l.
61 return λX.λY:n_list X.defined_nList X Y → option nat
63 [ n_nil ⇒ λp:defined_nList O n_nil.False_rect ? p
64 | n_cons n h t ⇒ λp:defined_nList (S n) (n_cons n h t).h
67 inductive map_elem (d:nat) : Type ≝
68 MAP_ELEM: aux_str_type → nat → n_list (S d) → map_elem d.
70 definition get_name_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM n _ _ ⇒ n ].
71 definition get_max_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ m _ ⇒ m ].
72 definition get_cur_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ _ c ⇒ c ].
74 definition aux_map_type ≝ λd.list (map_elem d).
76 definition empty_map ≝ nil (map_elem O).
78 theorem defined_nList_S_to_true :
79 ∀d.∀l:n_list (S d).defined_nList (S d) l = True.
83 | intros; simplify; reflexivity
87 lemma defined_get_id :
88 ∀d.∀h:map_elem d.defined_nList (S d) (get_cur_mapElem d h).
90 rewrite > (defined_nList_S_to_true ? (get_cur_mapElem d h));
95 let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝
98 | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
99 [ true ⇒ get_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ??)
100 | false ⇒ get_id_map_aux d t name
104 definition get_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
105 match get_id_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
108 let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝
111 | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
112 [ true ⇒ Some ? (get_max_mapElem d h)
113 | false ⇒ get_max_map_aux d t name
117 definition get_max_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
118 match get_max_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
121 definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
122 match get_id_map_aux d map name with [ None ⇒ False | Some _ ⇒ True ].
124 definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
125 match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ].
127 lemma checkbidmap_to_checkidmap : ∀d.∀map:aux_map_type d.∀name.checkb_id_map d map name = true → check_id_map d map name.
128 unfold checkb_id_map;
131 elim (get_id_map_aux d map name) 0;
132 [ simplify; intro; destruct H
133 | simplify; intros; apply I
137 definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
138 match get_id_map_aux d map name with [ None ⇒ True | Some _ ⇒ False ].
140 definition checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
141 match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ].
143 lemma checknotbidmap_to_checknotidmap : ∀d.∀map:aux_map_type d.∀name.checknotb_id_map d map name = true → checknot_id_map d map name.
144 unfold checknotb_id_map;
145 unfold checknot_id_map;
147 elim (get_id_map_aux d map name) 0;
148 [ simplify; intro; apply I
149 | simplify; intros; destruct H
154 let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝
157 | cons h t ⇒ match eqStrId_str name (get_name_flatVar h) with
158 [ true ⇒ Some ? (get_desc_flatVar h)
159 | false ⇒ get_desc_flatEnv_aux t name
163 definition get_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
164 match get_desc_flatEnv_aux fe str with
165 [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
167 definition check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
168 match get_desc_flatEnv_aux fe str with [ None ⇒ False | Some _ ⇒ True ].
170 definition checkb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
171 match get_desc_flatEnv_aux fe str with [ None ⇒ false | Some _ ⇒ true ].
173 lemma checkbdescflatenv_to_checkdescflatenv : ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str.
174 unfold checkb_desc_flatEnv;
175 unfold check_desc_flatEnv;
177 elim (get_desc_flatEnv_aux fe str) 0;
178 [ simplify; intro; destruct H
179 | simplify; intros; apply I
183 definition checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
184 match get_desc_flatEnv_aux fe str with [ None ⇒ True | Some _ ⇒ False ].
186 definition checknotb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
187 match get_desc_flatEnv_aux fe str with [ None ⇒ true | Some _ ⇒ false ].
189 lemma checknotbdescflatenv_to_checknotdescflatenv : ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str.
190 unfold checknotb_desc_flatEnv;
191 unfold checknot_desc_flatEnv;
193 elim (get_desc_flatEnv_aux fe str) 0;
194 [ simplify; intro; apply I
195 | simplify; intros; destruct H
200 definition eq_flatEnv_elem ≝
202 [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
203 [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
205 lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
210 rewrite > (eq_to_eqstrid a a (refl_eq ??));
211 rewrite > (eq_to_eqdescelem d d (refl_eq ??));
215 lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
222 rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
223 rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
227 let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
230 | cons h tl ⇒ match fe' with
231 [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
234 lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true.
240 rewrite > (eq_to_eqflatenv a a (refl_eq ??));
246 lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
249 [ intros; exists; [ apply fe' | reflexivity ]
250 | intros 4; elim fe';
251 [ simplify in H1:(%); destruct H1
252 | simplify in H2:(%);
253 rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
254 cases (H l1 (andb_true_true_r ?? H2));
257 exists; [ apply x | reflexivity ]
262 lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
268 rewrite > (eq_to_eqflatenv a a (refl_eq ??));
274 lemma leflatenv_to_check : ∀fe,fe',str.
275 (le_flatEnv fe fe' = true) →
276 (check_desc_flatEnv fe str) →
277 (check_desc_flatEnv fe' str).
279 cases (leflatEnv_to_le fe fe' H);
282 [ intro; simplify in H2:(%); elim H2;
285 cases (eqStrId_str str (get_name_flatVar a));
286 [ simplify; intro; apply H3
292 lemma leflatenv_to_get : ∀fe,fe',str.
293 (le_flatEnv fe fe' = true) →
294 (check_desc_flatEnv fe str) →
295 (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
297 cases (leflatEnv_to_le fe fe' H);
305 cases (eqStrId_str str (get_name_flatVar a));
310 unfold check_desc_flatEnv;
311 unfold get_desc_flatEnv;
312 cases (get_desc_flatEnv_aux l str);
313 [ simplify; intros; elim H3
314 | simplify; intros; rewrite < (H2 H3); reflexivity
321 definition env_to_flatEnv_inv ≝
322 λd.λe:aux_env_type.λmap:aux_map_type d.λfe:aux_flatEnv_type.
324 check_desc_env e str →
325 (check_id_map d map str ∧
326 check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
327 get_desc_env e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
329 lemma inv_to_checkdescflatenv :
330 ∀d.∀e.∀map:aux_map_type d.∀fe.
331 env_to_flatEnv_inv d e map fe →
332 (∀str.check_desc_env e str → check_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
334 unfold env_to_flatEnv_inv in H:(%);
336 apply (proj2 ?? (proj1 ?? Hletin));
339 lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
340 unfold env_to_flatEnv_inv;
343 unfold empty_flatEnv;
347 [ split; apply H | reflexivity ].
350 lemma leflatenv_to_inv :
351 ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
352 le_flatEnv fe fe' = true →
353 env_to_flatEnv_inv d e map fe →
354 env_to_flatEnv_inv d e map fe'.
356 unfold env_to_flatEnv_inv;
360 [ lapply (H1 str H2);
361 apply (proj1 ?? (proj1 ?? Hletin))
362 | lapply (H1 str H2);
363 apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
365 | lapply (H1 str H2);
366 rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
367 apply (proj2 ?? Hletin)
371 (* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
372 let rec enter_map d (map:aux_map_type d) on map ≝
377 (get_name_mapElem d h)
378 (get_max_mapElem d h)
380 (get_first_nList ? (get_cur_mapElem d h) (defined_get_id ??))
381 (get_cur_mapElem d h))
385 lemma getidmap_to_enter :
386 ∀d.∀m:aux_map_type d.∀str.
387 get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
390 [ simplify; reflexivity
391 | simplify; rewrite > H; reflexivity
395 lemma env_map_flatEnv_enter_aux :
396 ∀d.∀e.∀map:aux_map_type d.∀fe.
397 env_to_flatEnv_inv d e map fe → env_to_flatEnv_inv (S d) (enter_env e) (enter_map d map) fe.
401 unfold env_to_flatEnv_inv;
405 [ simplify; intros; split;
406 [ apply (proj1 ?? (H str H1)) | apply (proj2 ?? (H str H1)); ]
407 | simplify; intros; split;
408 [ rewrite > (getidmap_to_enter d l str); apply (proj1 ?? (H1 str H2))
409 | rewrite > (getidmap_to_enter d l str); apply (proj2 ?? (H1 str H2))
413 [ simplify; intros; split;
414 [ apply (proj1 ?? (H1 str H2)) | apply (proj2 ?? (H1 str H2)) ]
415 | simplify; intros; split;
416 [ rewrite > (getidmap_to_enter d l str); apply (proj1 ?? (H2 str H3))
417 | rewrite > (getidmap_to_enter d l str); apply (proj2 ?? (H2 str H3))
423 (* leave: elimina la testa (il "cur" corrente) *)
424 let rec leave_map d (map:aux_map_type (S d)) on map ≝
429 (get_name_mapElem (S d) h)
430 (get_max_mapElem (S d) h)
431 (cut_first_nList ? (get_cur_mapElem (S d) h) (defined_get_id ??))
435 (* aggiungi descrittore *)
436 let rec new_map_elem_from_depth_aux (d:nat) on d ≝
441 | S n ⇒ n_cons n (None ?) (new_map_elem_from_depth_aux n)
444 let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
447 | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
448 [ true ⇒ MAP_ELEM d name max (n_cons d (Some ? max) (cut_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ??)))
450 ]::(new_max_map_aux d t name max)
453 definition add_desc_env_flatEnv_map ≝
454 λd.λmap:aux_map_type d.λstr.
455 match get_max_map_aux d map str with
456 [ None ⇒ map@[ MAP_ELEM d str O (n_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ]
457 | Some x ⇒ new_max_map_aux d map str (S x)
460 definition add_desc_env_flatEnv_fe ≝
461 λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
462 fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
463 (DESC_ELEM c desc) ].
465 let rec build_trasfEnv_env (trsf:list (Prod3T aux_str_type bool ast_type)) e on trsf ≝
468 | cons h t ⇒ build_trasfEnv_env t (add_desc_env e (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))
471 let rec build_trasfEnv_mapFe (trasf:list ?) d (mfe:Prod (aux_map_type d) aux_flatEnv_type) on trasf ≝
475 build_trasfEnv_mapFe t d (pair ?? (add_desc_env_flatEnv_map d (fst ?? mfe) (fst3T ??? h))
476 (add_desc_env_flatEnv_fe d (fst ?? mfe) (snd ?? mfe) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
479 (* avanzamento delle dimostrazioni *)
480 axiom env_map_flatEnv_add_aux :
481 ∀d.∀e.∀map:aux_map_type d.∀fe.∀trsf.
482 env_to_flatEnv_inv d e map fe →
484 (build_trasfEnv_env trsf e)
485 (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe)))
486 (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))).
488 axiom env_map_flatEnv_add_aux_fe :
489 ∀d.∀map:aux_map_type d.∀fe,trsf.
490 ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))).
492 lemma buildtrasfenvadd_to_le :
493 ∀d.∀m:aux_map_type d.∀fe,trsf.
494 le_flatEnv fe (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) = true.
496 cases (env_map_flatEnv_add_aux_fe d m fe trsf);
498 rewrite > (le_to_leflatenv fe x);
502 axiom env_map_flatEnv_leave_aux :
503 ∀d.∀e.∀map:aux_map_type (S d).∀fe.
504 env_to_flatEnv_inv (S d) e map fe →
510 (* avanzamento congiunto oggetti + dimostrazioni *)
511 inductive env_map_flatEnv :
512 Πd.Πe.Πm:aux_map_type d.Πfe,fe'.
513 env_to_flatEnv_inv d e m fe' →
514 le_flatEnv fe fe' = true → Type ≝
515 ENV_MAP_FLATENV_EMPTY: env_map_flatEnv O
520 env_map_flatEnv_empty_aux
521 (eq_to_leflatenv ?? (refl_eq ??))
522 | ENV_MAP_FLATENV_ENTER: ∀d,e.∀m:aux_map_type d.∀fe,fe'.
523 ∀dimInv:env_to_flatEnv_inv d e m fe'.
524 ∀dimLe:le_flatEnv fe fe' = true.
525 env_map_flatEnv d e m fe fe' dimInv dimLe →
526 env_map_flatEnv (S d)
531 (env_map_flatEnv_enter_aux d e m fe' dimInv)
532 (eq_to_leflatenv ?? (refl_eq ??))
533 | ENV_MAP_FLATENV_ADD: ∀d,e.∀m:aux_map_type d.∀fe,fe'.
534 ∀dimInv:env_to_flatEnv_inv d e m fe'.
535 ∀dimLe:le_flatEnv fe fe' = true.∀trsf.
536 env_map_flatEnv d e m fe fe' dimInv dimLe →
538 (build_trasfEnv_env trsf e)
539 (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe')))
541 (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe')))
542 (env_map_flatEnv_add_aux d e m fe' trsf dimInv)
543 (buildtrasfenvadd_to_le d m fe' trsf)
544 | ENV_MAP_FLATENV_LEAVE: ∀d,e.∀m:aux_map_type (S d).∀fe,fe'.
545 ∀dimInv:env_to_flatEnv_inv (S d) e m fe'.
546 ∀dimLe:le_flatEnv fe fe' = true.
547 env_map_flatEnv (S d) e m fe fe' dimInv dimLe →
553 (env_map_flatEnv_leave_aux d e m fe' dimInv)
554 (eq_to_leflatenv ?? (refl_eq ??)).