AST to ASTFE completed up to a few computational (!!!) axioms.

[helm.git] / helm / software / matita / contribs / assembly / compiler / environment.ma

diff --git a/helm/software/matita/contribs/assembly/compiler/environment.ma b/helm/software/matita/contribs/assembly/compiler/environment.ma
index 363716ae8c87a369e72daaf93f2eb2c4926a6651..326ed1d2031cf7b0e0581cbe0861e5fd2d9a586f 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/environment.ma
+++ b/helm/software/matita/contribs/assembly/compiler/environment.ma
@@ -48,11 +48,35 @@ definition get_desc_var ≝ λv:var_elem.match v with [ VAR_ELEM _ d ⇒ d ].
 (* ambiente vuoto *)
 definition empty_env ≝ ne_nil ? (nil var_elem ).
 
+(* confronto *)
+let rec eq_aux_env_type_aux (subE,subE':list var_elem) on subE ≝
+ match subE with
+  [ nil ⇒ match subE' with
+   [ nil ⇒ true | cons _ _ ⇒ false ]
+  | cons h tl ⇒ match subE' with
+   [ nil ⇒ false | cons h' tl' ⇒ (strCmp_str (get_name_var h) (get_name_var h'))⊗
+                                 (eq_bool (get_const_desc (get_desc_var h)) (get_const_desc (get_desc_var h')))⊗
+                                 (eq_ast_type (get_type_desc (get_desc_var h)) (get_type_desc (get_desc_var h')))⊗   
+                                 (eq_aux_env_type_aux tl tl') ]
+  ].
+
+axiom eqbauxenvtypeaux_to_eq : ∀e,e'.eq_aux_env_type_aux e e' = true → e = e'.
+
+let rec eq_aux_env_type (e,e':aux_env_type) on e ≝
+ match e with
+  [ ne_nil h ⇒ match e' with
+   [ ne_nil h' ⇒ eq_aux_env_type_aux h h' | ne_cons _ _ ⇒ false ]
+  | ne_cons h tl ⇒ match e' with
+   [ ne_nil h' ⇒ false | ne_cons h' tl' ⇒ (eq_aux_env_type_aux h h')⊗(eq_aux_env_type tl tl') ]
+  ].
+
+axiom eqbauxenvtype_to_eq : ∀e,e':aux_env_type.eq_aux_env_type e e' = true → e = e'.
+
 (* 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 ?
@@ -60,55 +84,55 @@ match env 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
   ].