-(* 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 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
-definition pippodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
-definition pippodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32).
-definition plutodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
-definition plutodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
-definition plutodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32).
-
-definition map1 ≝ add_maxcur_map empty_env empty_flatEnv (empty_trasfMap ??) (empty_trasfMap ??) pippo false pippodesc1.
-definition env1 ≝ add_desc_env empty_env pippo false pippodesc1.
-definition fenv1 ≝ add_desc_flatEnv empty_flatEnv (next_nameId empty_env empty_flatEnv (empty_trasfMap ??) pippo) false pippodesc1.
-definition map2 ≝ add_maxcur_map env1 fenv1 map1 map1 pluto false plutodesc1.
-definition env2 ≝ add_desc_env env1 pluto false plutodesc1.
-definition fenv2 ≝ add_desc_flatEnv fenv1 (next_nameId ?? map1 pluto) false plutodesc1.
-
-definition env2' ≝ enter_env env2.
-definition map2' ≝ retype_e_to_enter env2 fenv2 map2.
-
-definition map3 ≝ add_maxcur_map env2' fenv2 map2' map2' pippo true pippodesc2.
-definition env3 ≝ add_desc_env env2' pippo true pippodesc2.
-definition fenv3 ≝ add_desc_flatEnv fenv2 (next_nameId ?? map2' pippo) true pippodesc2.
-definition map4 ≝ add_maxcur_map env3 fenv3 map3 map3 pluto true plutodesc2.
-definition env4 ≝ add_desc_env env3 pluto true plutodesc2.
-definition fenv4 ≝ add_desc_flatEnv fenv3 (next_nameId ?? map3 pluto) true plutodesc2.
-
-definition env4' ≝ enter_env env4.
-definition map4' ≝ retype_e_to_enter env4 fenv4 map4.
-
-definition map5 ≝ add_maxcur_map env4' fenv4 map4' map4' pippo false pippodesc3.
-definition env5 ≝ add_desc_env env4' pippo false pippodesc3.
-definition fenv5 ≝ add_desc_flatEnv fenv4 (next_nameId ?? map4' pippo) false pippodesc3.
-definition map6 ≝ add_maxcur_map env5 fenv5 map5 map5 pluto false plutodesc3.
-definition env6 ≝ add_desc_env env5 pluto false plutodesc3.
-definition fenv6 ≝ add_desc_flatEnv fenv5 (next_nameId ?? map5 pluto) false plutodesc3.
-
-definition map6' ≝ retype_e_to_leave env6 fenv6 map6.
-
-definition map7 ≝ rollback_map env4 fenv4 fenv6 (λx.add_desc_env (add_desc_env x pippo false pippodesc3) pluto false plutodesc3) map6' map4.
-
-definition map7' ≝ retype_e_to_leave env4 fenv6 map7.
-
-definition map8 ≝ rollback_map env2 fenv2 fenv6 (λx.add_desc_env (add_desc_env x pippo true pippodesc2) pluto true plutodesc2) map7' map2.
-*)
+(* invariante full -> invariante a un livello *)
+lemma env_to_flatEnv_inv_last :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv_one_level d e map fe.
+ intro;
+ cases d;
+ intros;
+ [ apply H
+ | simplify in H;
+ apply (proj1 ?? H)
+ ]
+qed.
+
+(* invariante caso base *)
+lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
+ unfold env_to_flatEnv_inv;
+ unfold empty_env;
+ unfold empty_map;
+ unfold empty_flatEnv;
+ simplify;
+ intros;
+ elim H.
+qed.
+
+(* invariante & leflatenv *)
+lemma leflatenv_to_inv :
+ ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
+ le_flatEnv fe fe' = true →
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv d e map fe'.
+ intro;
+ elim d;
+ [ simplify;
+ unfold env_to_flatEnv_inv_one_level;
+ intros;
+ split;
+ [ split;
+ [ lapply (H1 str H2);
+ apply (proj1 ?? (proj1 ?? Hletin))
+ | lapply (H1 str H2);
+ apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
+ ]
+ | lapply (H1 str H2);
+ rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
+ apply (proj2 ?? Hletin)
+ ]
+ | simplify in H2 ⊢ %;
+ cases H2;
+ split;
+ [ unfold env_to_flatEnv_inv_one_level;
+ intros;
+ split;
+ [ split;
+ [ lapply (H3 str H5);
+ apply (proj1 ?? (proj1 ?? Hletin))
+ | lapply (H3 str H5);
+ apply (leflatenv_to_check fe fe' ? H1 (proj2 ?? (proj1 ?? Hletin)))
+ ]
+ | lapply (H3 str H5);
+ rewrite < (leflatenv_to_get fe fe' ? H1 (proj2 ?? (proj1 ?? Hletin)));
+ apply (proj2 ?? Hletin)
+ ]
+ | apply (H ???? H1 H4)
+ ]
+ ].
+qed.
+
+(* invariante & enter *)
+lemma getidmap_to_enter :
+ ∀d.∀m:aux_map_type d.∀str.
+ get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
+ intros;
+ elim m;
+ [ simplify; reflexivity
+ | simplify; rewrite > H; reflexivity
+ ]
+qed.
+
+lemma checkdescenter_to_checkdesc :
+ ∀d.∀e:aux_env_type d.∀str.
+ check_desc_env (S d) (enter_env d e) str →
+ check_desc_env d e str.
+ intros;
+ unfold enter_env in H:(%);
+ simplify in H:(%);
+ apply H.
+qed.
+
+
+lemma env_map_flatEnv_enter_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe.
+ intro;
+ elim d;
+ [ simplify in H;
+ split;
+ [ unfold env_to_flatEnv_inv_one_level;
+ intros;
+ split;
+ [ split;
+ [ unfold check_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))
+ | unfold get_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj2 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))
+ ]
+ | unfold get_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj2 ?? (H str (checkdescenter_to_checkdesc ??? H1)))
+ ]
+ | rewrite > leave_env_enter_env;
+ rewrite > leave_map_enter_map;
+ change with (env_to_flatEnv_inv_one_level O e map fe);
+ apply H
+ ]
+ | split;
+ [ cases H1;
+ simplify in H2;
+ unfold env_to_flatEnv_inv_one_level;
+ intros;
+ split;
+ [ split;
+ [ unfold check_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj1 ?? (proj1 ?? (H2 str (checkdescenter_to_checkdesc ??? H4))))
+ | unfold get_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj2 ?? (proj1 ?? (H2 str (checkdescenter_to_checkdesc ??? H4))))
+ ]
+ | unfold get_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj2 ?? (H2 str (checkdescenter_to_checkdesc ??? H4)))
+ ]
+ | rewrite > leave_env_enter_env;
+ rewrite > leave_map_enter_map;
+ change with (env_to_flatEnv_inv (S n) e map fe);
+ apply H1
+ ]
+ ]
+qed.
+
+(* invariante & leave *)
+lemma env_map_flatEnv_leave_aux :
+ ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf.
+ env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe →
+ env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe.
+ intros;
+ simplify in H;
+ cases H;
+ apply H2.
+qed.
+
+(* invariante & add *)
+definition occurs_in_trsf ≝
+λtrsf:list (Prod3T aux_str_type bool ast_type).λstr.
+ fold_right_list ?? (λhe,b.eqStr_str (fst3T ??? he) str ⊕ b) false trsf.
+
+lemma occurs_in_subTrsf_r :
+ ∀a,l,str.
+ occurs_in_trsf (a::l) str = false →
+ occurs_in_trsf l str = false.
+ intros;
+ simplify in H:(%);
+ rewrite > (orb_false_false_r ?? H);
+ reflexivity.
+qed.
+
+lemma occurs_in_subTrsf_l :
+ ∀a,l,str.
+ occurs_in_trsf (a::l) str = false →
+ eqStr_str (fst3T ??? a) str = false.
+ intros;
+ simplify in H:(%);
+ rewrite > (orb_false_false ?? H);
+ reflexivity.
+qed.
+
+axiom get_id_map_aux_add_not_occurs :
+ ∀d.∀map:aux_map_type d.∀fe,trsf,str.
+ occurs_in_trsf trsf str = false →
+ get_id_map_aux d map str =
+ get_id_map_aux d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
+
+lemma get_id_map_add_not_occurs :
+ ∀d.∀map:aux_map_type d.∀fe,trsf,str.
+ occurs_in_trsf trsf str = false →
+ get_id_map d map str =
+ get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
+ intros;
+ unfold get_id_map;
+ rewrite < (get_id_map_aux_add_not_occurs ????? H);
+ reflexivity.
+qed.
+
+lemma check_id_map_not_occurs :
+ ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ check_id_map d map str →
+ check_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
+ intros;
+ whd in H1 ⊢ %;
+ rewrite < (get_id_map_aux_add_not_occurs ????? H);
+ apply H1.
+qed.
+
+lemma check_desc_flatEnv_not_occurs :
+ ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) →
+ check_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
+ intros;
+ rewrite < (get_id_map_add_not_occurs ????? H);
+ apply (leflatenv_to_check ??? (buildtrasfenvadd_to_le ????) H1).
+qed.
+
+lemma get_desc_flatEnv_not_occurs :
+ ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) →
+ get_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)) =
+ get_desc_flatEnv fe (STR_ID str (get_id_map d map str)).
+ intros;
+ rewrite < (get_id_map_add_not_occurs ????? H);
+ rewrite < (leflatenv_to_get ??? (buildtrasfenvadd_to_le ????) H1);
+ reflexivity.
+qed.
+
+axiom get_desc_env_aux_not_occurs :
+ ∀d.∀e:aux_env_type d.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ get_desc_env_aux d (build_trasfEnv_env d trsf e) str =
+ get_desc_env_aux d e str.
+
+lemma get_desc_env_not_occurs :
+ ∀d.∀e:aux_env_type d.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ get_desc_env d (build_trasfEnv_env d trsf e) str =
+ get_desc_env d e str.
+ intros;
+ unfold get_desc_env;
+ rewrite > (get_desc_env_aux_not_occurs ???? H);
+ reflexivity.
+qed.
+
+lemma check_desc_env_not_occurs :
+ ∀d.∀e:aux_env_type d.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ check_desc_env d (build_trasfEnv_env d trsf e) str →
+ check_desc_env d e str.
+ intros 5;
+ unfold check_desc_env;
+ intro;
+ rewrite < (get_desc_env_aux_not_occurs ???? H);
+ apply H1.
+qed.
+
+axiom get_id_map_aux_add_occurs :
+ ∀d.∀map:aux_map_type d.∀fe,trsf,str.
+ occurs_in_trsf trsf str = true →
+ ∃x.get_id_map_aux d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str = Some ? x.
+
+lemma check_id_map_occurs :
+ ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = true →
+ check_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
+ intros;
+ cases (get_id_map_aux_add_occurs d map fe trsf str H);
+ unfold check_id_map;
+ rewrite > H1;
+ simplify;
+ apply I.
+qed.
+
+axiom check_desc_flatEnv_occurs :
+ ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = true →
+ check_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
+
+axiom get_desc_env_eq_get_desc_flatEnv_occurs :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = true →
+ get_desc_env d (build_trasfEnv_env d trsf e) str =
+ get_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
+
+axiom leave_env_build_trasfEnv :
+ ∀d.∀e:aux_env_type (S d).∀trsf.
+ leave_env d (build_trasfEnv_env (S d) trsf e) = leave_env d e.
+
+axiom leave_map_build_trasfEnv_mapFe:
+ ∀d.∀map:aux_map_type (S d).∀fe.∀trsf.
+ leave_map d (fst ?? (build_trasfEnv_mapFe (S d) trsf (pair ?? map fe))) =
+ leave_map d map.
+
+lemma env_map_flatEnv_add_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env d trsf e)
+ (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
+ intro;
+ cases d;
+ [ intros;
+ simplify in H;
+ simplify;
+ intros 2;
+ apply (bool_elim ? (occurs_in_trsf trsf str));
+ [ intro;
+ split
+ [ split
+ [ apply (check_id_map_occurs ????? H2)
+ | apply (check_desc_flatEnv_occurs ????? H2)
+ ]
+ | apply (get_desc_env_eq_get_desc_flatEnv_occurs ?????? H2)
+ ]
+ | intro;
+ cases (H str (check_desc_env_not_occurs ???? H2 H1));
+ split
+ [ split
+ [ apply (check_id_map_not_occurs ????? H2 (proj1 ?? H3))
+ | apply (check_desc_flatEnv_not_occurs ????? H2 (proj2 ?? H3))
+ ]
+ | rewrite > (get_desc_flatEnv_not_occurs ????? H2 (proj2 ?? H3));
+ rewrite > (get_desc_env_not_occurs ???? H2);
+ apply H4
+ ]
+ ]
+ | intros;
+ simplify in H;
+ cases H;
+ unfold env_to_flatEnv_inv_one_level in H1;
+ split;
+ [ intros 2;
+ apply (bool_elim ? (occurs_in_trsf trsf str));
+ [ intro;
+ split
+ [ split
+ [ apply (check_id_map_occurs ????? H4)
+ | apply (check_desc_flatEnv_occurs ????? H4)
+ ]
+ | apply (get_desc_env_eq_get_desc_flatEnv_occurs ?????? H4)
+ ]
+ | intro;
+ split;
+ [ split
+ [ apply (check_id_map_not_occurs ????? H4 (proj1 ?? (proj1 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))))
+ | apply (check_desc_flatEnv_not_occurs ????? H4 (proj2 ?? (proj1 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))))
+ ]
+ | rewrite > (get_desc_flatEnv_not_occurs ????? H4 (proj2 ?? (proj1 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))));
+ rewrite > (get_desc_env_not_occurs ???? H4);
+ apply (proj2 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))
+ ]
+ ]
+ | change with (env_to_flatEnv_inv n (leave_env n (build_trasfEnv_env (S n) trsf e))
+ (leave_map n (fst ?? (build_trasfEnv_mapFe (S n) trsf (pair ?? map fe))))
+ (snd ?? (build_trasfEnv_mapFe (S n) trsf (pair ?? map fe))));
+ rewrite > leave_map_build_trasfEnv_mapFe;
+ rewrite > leave_env_build_trasfEnv;
+ apply (leflatenv_to_inv ?????? H2);
+ apply buildtrasfenvadd_to_le
+ ]
+ ].
+qed.
+
+lemma env_map_flatEnv_addNil_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env d [] e)
+ (fst ?? (build_trasfEnv_mapFe d [] (pair ?? map fe)))
+ (snd ?? (build_trasfEnv_mapFe d [] (pair ?? map fe))).
+ intros;
+ simplify;
+ apply H.
+qed.
+
+lemma env_map_flatEnv_addSingle_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀name,const,desc.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv d
+ (add_desc_env d e name const desc)
+ (fst ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe)))
+ (snd ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe))).
+ intros;
+ apply (env_map_flatEnv_add_aux d e map fe [ tripleT ??? name const desc ]);
+ apply H.
+qed.
+
+lemma env_map_flatEnv_addJoin_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe:aux_flatEnv_type.∀name,const,desc,trsf.
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env d trsf (add_desc_env d e name const desc))
+ map fe →
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env d ([ tripleT ??? name const desc ]@trsf) e)
+ map fe.
+ intros;
+ simplify;
+ apply H.
+qed.
+
+(* ********************************************* *)
+
+lemma newid_from_init :
+ ∀d.∀e:aux_env_type d.∀name,const,desc.
+ ast_id d (add_desc_env d e name const desc) const desc.
+ intros;
+ lapply (AST_ID d (add_desc_env d e name const desc) name ?);
+ [ elim e;
+ simplify;
+ rewrite > (eq_to_eqstr ?? (refl_eq ??));
+ simplify;
+ apply I
+ | cut (const = get_const_desc (get_desc_env d (add_desc_env d e name const desc) name) ∧
+ desc = get_type_desc (get_desc_env d (add_desc_env d e name const desc) name));
+ [ rewrite > (proj1 ?? Hcut) in ⊢ (? ? ? % ?);
+ rewrite > (proj2 ?? Hcut) in ⊢ (? ? ? ? %);
+ apply Hletin
+ | split;
+ [ elim e;
+ simplify;
+ rewrite > (eq_to_eqstr ?? (refl_eq ??));
+ simplify;
+ reflexivity
+ | elim e;
+ simplify;
+ rewrite > (eq_to_eqstr ?? (refl_eq ??));
+ simplify;
+ reflexivity
+ ]
+ ]
+ ].
+qed.