let rec get_desc_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) on e ≝
match e with
[ nil ⇒ None ?
- | cons h tl ⇒ match strCmp_strId str (get_nameId_flatVar h) with
+ | cons h tl ⇒ match eqStrId_str str (get_nameId_flatVar h) with
[ true ⇒ Some ? (get_desc_flatVar h)
| false ⇒ get_desc_flatEnv_aux tl str ]].
normalize; autobatch ]
qed.
-(* aggiungi descrittore ad ambiente: in testa *)
+(* aggiungi descrittore ad ambiente: in coda *)
definition add_desc_flatEnv ≝
λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
- (VAR_FLAT_ELEM str (DESC_ELEM b t))::e.
+ e@[VAR_FLAT_ELEM str (DESC_ELEM b t)].
+
+(* controllo fe <= fe' *)
+definition eq_flatEnv_elem ≝
+λe1,e2.match e1 with
+ [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
+ [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
+
+lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
+ intros 3;
+ rewrite < H;
+ elim e1;
+ simplify;
+ rewrite > (eq_to_eqstrid a a (refl_eq ??));
+ rewrite > (eq_to_eqdescelem d d (refl_eq ??));
+ reflexivity.
+qed.
+
+lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
+ intros 2;
+ elim e1 0;
+ elim e2 0;
+ intros 4;
+ simplify;
+ intro;
+ rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
+ rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
+ reflexivity.
+qed.
+
+let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
+match fe with
+ [ nil ⇒ true
+ | cons h tl ⇒ match fe' with
+ [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
+ ].
+
+lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
+ intro;
+ elim fe 0;
+ [ intros; exists; [ apply fe' | reflexivity ]
+ | intros 4; elim fe';
+ [ simplify in H1:(%); destruct H1
+ | simplify in H2:(%);
+ rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
+ cases (H l1 (andb_true_true_r ?? H2));
+ simplify;
+ rewrite < H3;
+ exists; [ apply x | reflexivity ]
+ ]
+ ].
+qed.
+
+lemma leflatenv_to_check : ∀fe,fe',str.
+ (le_flatEnv fe fe' = true) →
+ (check_desc_flatEnv fe str) →
+ (check_desc_flatEnv fe' str).
+ intros 4;
+ cases (leflatEnv_to_le fe fe' H);
+ rewrite < H1;
+ elim fe 0;
+ [ intro; simplify in H2:(%); elim H2;
+ | intros 3;
+ simplify;
+ cases (eqStrId_str str (get_nameId_flatVar a));
+ [ simplify; intro; apply H3
+ | simplify;
+ apply H2
+ ]
+ ].
+qed.
+
+lemma adddescflatenv_to_leflatenv : ∀fe,n,b,t.le_flatEnv fe (add_desc_flatEnv fe n b t) = true.
+intros;
+ change in ⊢ (? ? (? ? %) ?) with (fe@[VAR_FLAT_ELEM n (DESC_ELEM b t)]);
+ elim fe 0;
+ [ 1: reflexivity
+ | 2: do 3 intro;
+ unfold le_flatEnv;
+ change in ⊢ (? ? % ?) with ((eq_flatEnv_elem a a)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)])));
+ unfold eq_flatEnv_elem;
+ elim a;
+ change in ⊢ (? ? % ?) with ((eqStrId_str a1 a1)⊗(eqDesc_elem d d)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)])));
+ rewrite > (eq_to_eqstrid a1 a1 (refl_eq ??));
+ rewrite > (eq_to_eqdescelem d d (refl_eq ??));
+ rewrite > H;
+ reflexivity
+ ].
+qed.
(* STRUTTURA MAPPA TRASFORMAZIONE *)
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 ≝
match map with
[ nil ⇒ None ?
- | cons h tl ⇒ match strCmp_str str (get_name_maxCur e fe h) with
+ | cons h tl ⇒ match eqStr_str str (get_name_maxCur e fe h) with
[ true ⇒ Some ? h | false ⇒ get_maxcur_map e fe tl str ]].
(* prossimo nome *)
axiom add_maxcur_map_aux_false : ∀e,fe,str,cur,str',b',desc',map.
(check_desc_env e str →
get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
-(strCmp_str str str' = false) →
+(eqStr_str str str' = false) →
(check_desc_env (add_desc_env e str' b' desc') str →
get_desc_env (add_desc_env e str' b' desc') str =
get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str cur)).
axiom add_maxcur_map_aux_true : ∀e,fe,str,cur,max,str',b',desc',map.
(check_desc_env e str →
get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
-(strCmp_str str str' = true) →
+(eqStr_str str str' = true) →
(check_desc_env (add_desc_env e str' b' desc') str →
get_desc_env (add_desc_env e str' b' desc') str =
get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str (S max))).
+axiom add_maxcur_map_aux_new : ∀e,fe,str,b,desc,map.
+ check_desc_env (add_desc_env e str b desc) str →
+ get_desc_env (add_desc_env e str b desc) str =
+ get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str) b desc) (STR_ID str 0).
+
+(* NB: avendo poi in input la dimostrazione "check_desc_env e (get_name_ast_id e b t ast)" ha senso *)
+axiom ast_to_astfe_id_aux : ∀e,fe.∀map:aux_trasfMap_type e fe.∀str.
+ check_desc_env e str → check_desc_flatEnv fe (name_to_nameId e fe map str).
+
+axiom ast_to_astfe_dec_aux : ∀e,str,b,t,fe,map.
+ check_not_already_def_env e str →
+ check_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str) b t) (next_nameId e fe map str).
+
(* aggiungi/aggiorna descrittore mappa trasformazione *)
let rec add_maxcur_map_aux (e:aux_env_type) (fe:aux_flatEnv_type) (map,fMap:aux_trasfMap_type e fe)
(str:aux_str_type) (b:bool) (desc:ast_type) (flag:bool) on map
[ true ⇒ []
| false ⇒
[ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
- str O O (False_rect ? daemon) ]
+ str 0 0 (add_maxcur_map_aux_new e fe str b desc fMap) ]
]
| cons h tl ⇒ match h with
[ MAX_CUR_ELEM str' cur' max' dim' ⇒
- match strCmp_str str' str return λx.(strCmp_str str' str = x) → ? with
- [ true ⇒ λp:(strCmp_str str' str = true).
+ match eqStr_str str' str return λx.(eqStr_str str' str = x) → ? with
+ [ true ⇒ λp:(eqStr_str str' str = true).
[ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
str' (S max') (S max')
(add_maxcur_map_aux_true e fe str' cur' max' str b desc fMap dim' p)
]@(add_maxcur_map_aux e fe tl fMap str b desc true)
- | false ⇒ λp:(strCmp_str str' str = false).
+ | false ⇒ λp:(eqStr_str str' str = false).
[ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
str' cur' max'
(add_maxcur_map_aux_false e fe str' cur' str b desc fMap dim' p)
]@(add_maxcur_map_aux e fe tl fMap str b desc flag)
- ] (refl_eq ? (strCmp_str str' str))
+ ] (refl_eq ? (eqStr_str str' str))
]
].
λe:aux_env_type.λfe:aux_flatEnv_type.λmap,fMap:aux_trasfMap_type e fe.λstr:aux_str_type.λb:bool.λdesc:ast_type.
add_maxcur_map_aux e fe map fMap str b desc false.
+(* composizione di funzioni generata da una lista di nome x const x tipo *)
+definition aux_trasfEnv_type ≝ list (Prod3T aux_str_type bool ast_type).
+
+let rec build_trasfEnv (trasf:aux_trasfEnv_type) on trasf : aux_env_type → aux_env_type ≝
+ match trasf with
+ [ nil ⇒ (λx.x)
+ | cons h tl ⇒ (λx.(build_trasfEnv tl) (add_desc_env x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
+ ].
+
+lemma build_trasfEnv_exists_aux : ∀a.∀trsf:aux_trasfEnv_type.∀c.
+ ∃b.build_trasfEnv trsf (c§§a) = (b§§a).
+ intros 2;
+ elim trsf;
+ [ simplify; exists; [apply c | reflexivity]
+ | simplify; apply H; ]
+qed.
+
+lemma eq_enter_leave : ∀e,trsf.leave_env (build_trasfEnv trsf (enter_env e)) = e.
+ intros;
+ change in ⊢ (? ? (? (? ? %)) ?) with ([]§§e);
+ cases (build_trasfEnv_exists_aux e trsf []);
+ rewrite > H;
+ reflexivity.
+qed.
+
(* NB: leave ... enter e' equivalente a e originale *)
-axiom retype_enter_leave_to_e: ∀e,fe,f. aux_trasfMap_type (leave_env (f (enter_env e))) fe → aux_trasfMap_type e fe.
+lemma retype_enter_leave_to_e_aux : ∀e,fe,str,cur,trsf.
+ (check_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str →
+ get_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str = get_desc_flatEnv fe (STR_ID str cur)) →
+ (check_desc_env e str →
+ get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)).
+ intros 5;
+ rewrite > (eq_enter_leave e trsf);
+ intros;
+ apply H;
+ apply H1.
+qed.
+
+let rec retype_enter_leave_to_e (e:aux_env_type) (fe:aux_flatEnv_type) (trsf:aux_trasfEnv_type)
+ (map:aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe) on map : aux_trasfMap_type e fe ≝
+ match map with
+ [ nil ⇒ []
+ | cons h tl ⇒ match h with
+ [ MAX_CUR_ELEM str cur max dim ⇒
+ [MAX_CUR_ELEM e fe str cur max (retype_enter_leave_to_e_aux e fe str cur trsf dim)]@(retype_enter_leave_to_e e fe trsf tl)
+ ]].
+
+lemma retype_e_to_enter_leave_aux : ∀e,fe,str,cur,trsf.
+ (check_desc_env e str →
+ get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
+ (check_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str →
+ get_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str = get_desc_flatEnv fe (STR_ID str cur)).
+ intros 5;
+ rewrite < (eq_enter_leave e trsf) in ⊢ ((? % ?→?)→?);
+ rewrite < (eq_enter_leave e trsf) in ⊢ ((?→? ? (? % ?) ?)→?);
+ intros;
+ apply H;
+ apply H1.
+qed.
+
+let rec retype_e_to_enter_leave (e:aux_env_type) (fe:aux_flatEnv_type) (trsf:aux_trasfEnv_type)
+ (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe ≝
+ match map with
+ [ nil ⇒ []
+ | cons h tl ⇒ match h with
+ [ MAX_CUR_ELEM str cur max dim ⇒
+ [MAX_CUR_ELEM (leave_env ((build_trasfEnv trsf) (enter_env e))) fe str cur max (retype_e_to_enter_leave_aux e fe str cur trsf dim)]@(retype_e_to_enter_leave e fe trsf tl)
+ ]].
+
(* NB: enter non cambia fe *)
-axiom retype_e_to_enter: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (enter_env e) fe.
+lemma retype_e_to_enter_aux : ∀e,fe,str,cur.
+ (check_desc_env e str →
+ get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
+ (check_desc_env (enter_env e) str →
+ get_desc_env (enter_env e) str = get_desc_flatEnv fe (STR_ID str cur)).
+ intros 6;
+ rewrite > H;
+ [ reflexivity
+ | apply H1
+ ].
+qed.
+
+let rec retype_e_to_enter (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (enter_env e) fe ≝
+ match map with
+ [ nil ⇒ []
+ | cons h tl ⇒ match h with
+ [ MAX_CUR_ELEM str cur max dim ⇒
+ [MAX_CUR_ELEM (enter_env e) fe str cur max (retype_e_to_enter_aux e fe str cur dim)]@(retype_e_to_enter e fe tl)
+ ]].
+
(* NB: leave non cambia fe *)
-axiom retype_e_to_leave: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (leave_env e) fe.
+axiom retype_e_to_leave_aux : ∀e,fe,str,cur.
+ (check_desc_env e str →
+ get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
+ (check_desc_env (leave_env e) str →
+ get_desc_env (leave_env e) str = get_desc_flatEnv fe (STR_ID str cur)).
+
+let rec retype_e_to_leave (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (leave_env e) fe ≝
+ match map with
+ [ nil ⇒ []
+ | cons h tl ⇒ match h with
+ [ MAX_CUR_ELEM str cur max dim ⇒
+ [MAX_CUR_ELEM (leave_env e) fe str cur max (retype_e_to_leave_aux e fe str cur dim)]@(retype_e_to_leave e fe tl)
+ ]].
-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')
+let rec rollback_map (e:aux_env_type) (fe,fe':aux_flatEnv_type) (trsf:aux_trasfEnv_type) (map:aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe')
(snap:aux_trasfMap_type e fe) on map : aux_trasfMap_type e fe' ≝
match map with
[ nil ⇒ empty_trasfMap e fe'
| cons h tl ⇒
match get_maxcur_map e fe snap (get_name_maxCur ?? h) with
- [ None ⇒ retype_enter_leave_to_e e fe' f [h]
+ [ None ⇒ retype_enter_leave_to_e e fe' trsf [h]
| Some new ⇒
[ MAX_CUR_ELEM ?? (get_name_maxCur ?? h) (get_cur_maxCur ?? new)
(get_max_maxCur ?? h) (False_rect ? daemon) ]
- ] @ rollback_map e fe fe' f tl snap
+ ] @ rollback_map e fe fe' trsf tl snap
].
(* sequenza di utilizzo:
| ...
*)
-(* mini test
+(* mini test
definition pippo ≝ [ ch_P ].
definition pluto ≝ [ ch_Q ].
definition pippodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
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 ≝ rollback_map env4 fenv4 fenv6 [ tripleT ??? pluto false plutodesc3 ; tripleT ??? pippo false pippodesc3 ] 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.
+definition map8 ≝ rollback_map env2 fenv2 fenv6 [ tripleT ??? pluto true plutodesc2 ; tripleT ??? pippo true pippodesc2 ] map7' map2.
*)
projects / helm.git / blobdiff