definition get_const_desc ≝ λd:desc_elem.match d with [ DESC_ELEM c _ ⇒ c ].
definition get_type_desc ≝ λd:desc_elem.match d with [ DESC_ELEM _ t ⇒ t ].
+definition eqDesc_elem ≝ λd,d'.(eq_bool (get_const_desc d) (get_const_desc d'))⊗(eq_ast_type (get_type_desc d) (get_type_desc d')).
+
+lemma eq_to_eqdescelem : ∀d,d'.d = d' → eqDesc_elem d d' = true.
+ intros 3;
+ rewrite < H;
+ elim d;
+ simplify;
+ rewrite > (eq_to_eqbool b b (refl_eq ??));
+ rewrite > (eq_to_eqasttype a a (refl_eq ??));
+ reflexivity.
+qed.
+
+lemma eqdescelem_to_eq : ∀d,d'.eqDesc_elem d d' = true → d = d'.
+ intros 2;
+ elim d 0;
+ elim d' 0;
+ intros 4;
+ simplify;
+ intro;
+ rewrite > (eqbool_to_eq b1 b (andb_true_true ?? H));
+ rewrite > (eqasttype_to_eq a1 a (andb_true_true_r ?? H));
+ reflexivity.
+qed.
+
definition get_name_var ≝ λv:var_elem.match v with [ VAR_ELEM n _ ⇒ n ].
definition get_desc_var ≝ λv:var_elem.match v with [ VAR_ELEM _ d ⇒ d ].
definition empty_env ≝ ne_nil ? (nil var_elem ).
(* setter *)
-definition enter_env ≝ λe:aux_env_type.e&empty_env.
-definition leave_env ≝ λe:aux_env_type.cut_last_neList ? e.
+definition enter_env ≝ λe:aux_env_type.empty_env&e.
+definition leave_env ≝ λe:aux_env_type.cut_first_neList ? e.
-(* recupera descrittore da ambiente *)
+(* recupera descrittore da ambiente: il primo trovato, ma e' anche l'unico *)
let rec get_desc_from_lev_env (env:list var_elem ) (str:aux_str_type) on env ≝
match env with
[ nil ⇒ None ?
- | cons h t ⇒ match strCmp_str str (get_name_var h) with
+ | cons h t ⇒ match eqStr_str str (get_name_var h) with
[ true ⇒ Some ? (get_desc_var h)
| false ⇒ get_desc_from_lev_env t str ]].
-(* recupera descrittore da ambiente globale *)
-let rec get_desc_env_aux (env:aux_env_type) (res:option desc_elem) (str:aux_str_type) on env ≝
+(* recupera descrittore da ambiente globale: il primo trovato *)
+let rec get_desc_env_aux (env:aux_env_type) (str:aux_str_type) on env ≝
match env with
- [ ne_nil h ⇒ match get_desc_from_lev_env h str with
- [ None ⇒ res | Some res' ⇒ Some ? res' ]
- | ne_cons h t ⇒ get_desc_env_aux t (match get_desc_from_lev_env h str with
- [ None ⇒ res | Some res' ⇒ Some ? res' ]) str ].
+ [ ne_nil h ⇒ get_desc_from_lev_env h str
+ | ne_cons h t ⇒ match get_desc_from_lev_env h str with
+ [ None ⇒ get_desc_env_aux t str | Some res' ⇒ Some ? res' ]
+ ].
definition check_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
- match get_desc_env_aux e (None ?) str with [ None ⇒ False | Some _ ⇒ True ].
+ match get_desc_env_aux e str with [ None ⇒ False | Some _ ⇒ True ].
definition checkb_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
- match get_desc_env_aux e (None ?) str with [ None ⇒ false | Some _ ⇒ true ].
+ match get_desc_env_aux e str with [ None ⇒ false | Some _ ⇒ true ].
lemma checkbdescenv_to_checkdescenv : ∀e,str.checkb_desc_env e str = true → check_desc_env e str.
unfold checkb_desc_env;
unfold check_desc_env;
intros;
- letin K ≝ (get_desc_env_aux e (None ?) str);
+ letin K ≝ (get_desc_env_aux e str);
elim K;
[ normalize; autobatch |
normalize; autobatch ]
qed.
definition get_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
- match get_desc_env_aux e (None ?) str with
+ match get_desc_env_aux e str with
[ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
definition check_not_already_def_env ≝ λe:aux_env_type.λstr:aux_str_type.
- match get_desc_from_lev_env (get_last_neList ? e) str with [ None ⇒ True | Some _ ⇒ False ].
+ match get_desc_from_lev_env (get_first_neList ? e) str with [ None ⇒ True | Some _ ⇒ False ].
definition checkb_not_already_def_env ≝ λe:aux_env_type.λstr:aux_str_type.
- match get_desc_from_lev_env (get_last_neList ? e) str with [ None ⇒ true | Some _ ⇒ false ].
+ match get_desc_from_lev_env (get_first_neList ? e) str with [ None ⇒ true | Some _ ⇒ false ].
lemma checkbnotalreadydefenv_to_checknotalreadydefenv : ∀e,str.checkb_not_already_def_env e str = true → check_not_already_def_env e str.
unfold checkb_not_already_def_env;
unfold check_not_already_def_env;
intros;
- letin K ≝ (get_desc_from_lev_env (get_last_neList ? e) str);
+ letin K ≝ (get_desc_from_lev_env (get_first_neList ? e) str);
elim K;
[ normalize; autobatch |
normalize; autobatch ]
qed.
-(* aggiungi descrittore ad ambiente globale *)
+(* aggiungi descrittore ad ambiente globale: in testa al primo ambiente *)
definition add_desc_env ≝
λe:aux_env_type.λstr:aux_str_type.λc:bool.λdesc:ast_type.
-let var ≝ VAR_ELEM str (DESC_ELEM c desc) in
+(*let var ≝ VAR_ELEM str (DESC_ELEM c desc) in*)
match e with
- [ ne_nil h ⇒ ne_nil ? (var::h)
- | ne_cons _ _ ⇒ (cut_last_neList ? e)&«(var::(get_last_neList ? e)) £ »
+ [ ne_nil h ⇒ ne_nil ? ((VAR_ELEM str (DESC_ELEM c desc))::h)
+ | ne_cons h tl ⇒ «£((VAR_ELEM str (DESC_ELEM c desc))::h)»&tl
].
+
+(* controllo e <= e' *)
+definition eq_env_elem ≝
+λe1,e2.match e1 with
+ [ VAR_ELEM s1 d1 ⇒ match e2 with
+ [ VAR_ELEM s2 d2 ⇒ (eqStr_str s1 s2)⊗(eqDesc_elem d1 d2) ]].
+
+lemma eq_to_eqenv : ∀e1,e2.e1 = e2 → eq_env_elem e1 e2 = true.
+ intros 3;
+ rewrite < H;
+ elim e1;
+ simplify;
+ rewrite > (eq_to_eqstr a a (refl_eq ??));
+ rewrite > (eq_to_eqdescelem d d (refl_eq ??));
+ reflexivity.
+qed.
+
+lemma eqenv_to_eq : ∀e1,e2.eq_env_elem e1 e2 = true → e1 = e2.
+ intros 2;
+ elim e1 0;
+ elim e2 0;
+ intros 4;
+ simplify;
+ intro;
+ rewrite > (eqstr_to_eq a1 a (andb_true_true ?? H));
+ rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
+ reflexivity.
+qed.
projects / helm.git / blobdiff