X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fenvironment.ma;h=590a98d1f390d277f6bc89d3240640be6fe16599;hb=11e495dda047bcdfa4267c06cad2d074fcffe3e3;hp=8131570820a1538c390d4f192a7cfd7e5525737d;hpb=55e5bef77f163b29feeb9ad4e83376c5aa301297;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/environment.ma b/helm/software/matita/contribs/assembly/compiler/environment.ma
index 813157082..590a98d1f 100755
--- a/helm/software/matita/contribs/assembly/compiler/environment.ma
+++ b/helm/software/matita/contribs/assembly/compiler/environment.ma
@@ -20,7 +20,6 @@
 (* ********************************************************************** *)
 
 include "string/string.ma".
-include "freescale/word32.ma".
 include "compiler/ast_type.ma".
 
 (* ***************** *)
@@ -36,7 +35,40 @@ inductive var_elem : Type ≝
 VAR_ELEM: aux_str_type → desc_elem → var_elem.
 
 (* ambiente globale: (ambiente base + ambienti annidati) *)
-definition aux_env_type ≝ ne_list (list var_elem).
+inductive env_list : nat → Type ≝
+  env_nil: list var_elem → env_list O
+| env_cons: ∀n.list var_elem → env_list n → env_list (S n).
+
+definition defined_envList ≝
+λd.λl:env_list d.match l with [ env_nil _ ⇒ False | env_cons _ _ _ ⇒ True ].
+
+definition cut_first_envList : Πd.env_list d → ? → env_list (pred d) ≝
+λd.λl:env_list d.λp:defined_envList ? l.
+ let value ≝
+  match l
+   return λX.λY:env_list X.defined_envList X Y → env_list (pred X)
+  with
+   [ env_nil h ⇒ λp:defined_envList O (env_nil h).False_rect ? p
+   | env_cons n h t ⇒ λp:defined_envList (S n) (env_cons n h t).t
+   ] p in value.
+
+definition get_first_envList ≝
+λd.λl:env_list d.
+ match l with
+  [ env_nil h ⇒ h
+  | env_cons _ h _ ⇒ h
+  ].
+
+lemma defined_envList_S :
+∀d.∀l:env_list (S d).defined_envList (S d) l.
+ intros;
+ inversion l;
+  [ intros; destruct H
+  | intros; simplify; apply I
+  ]
+qed.
+
+definition aux_env_type ≝ λd.env_list d.
 
 (* getter *)
 definition get_const_desc ≝ λd:desc_elem.match d with [ DESC_ELEM c _ ⇒ c ].
@@ -70,14 +102,14 @@ 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 ].
 
 (* ambiente vuoto *)
-definition empty_env ≝ ne_nil ? (nil var_elem ).
+definition empty_env ≝ env_nil [].
 
 (* setter *)
-definition enter_env ≝ λe:aux_env_type.empty_env&e.
-definition leave_env ≝ λe:aux_env_type.cut_first_neList ? e.
+definition enter_env ≝ λd.λe:aux_env_type d.env_cons d [] e.
+definition leave_env ≝ λd.λe:aux_env_type (S d).cut_first_envList (S d) e (defined_envList_S ??).
 
 (* 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 ≝
+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 eqStr_str str (get_name_var h) with
@@ -85,44 +117,44 @@ match env with
   | false ⇒ get_desc_from_lev_env t str ]].
 
 (* recupera descrittore da ambiente globale: il primo trovato *)
-let rec get_desc_env_aux (env:aux_env_type) (str:aux_str_type) on env ≝
+let rec get_desc_env_aux d (env:aux_env_type d) (str:aux_str_type) on env ≝
  match env with
-  [ 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' ]
+  [ env_nil h ⇒ get_desc_from_lev_env h str 
+  | env_cons n h t ⇒  match get_desc_from_lev_env h str with 
+   [ None ⇒ get_desc_env_aux n t str | Some res' ⇒ Some ? res' ]
   ].
 
-definition check_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
- match get_desc_env_aux e str with [ None ⇒ False | Some _ ⇒ True ].
+definition check_desc_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
+ match get_desc_env_aux d 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 str with [ None ⇒ false | Some _ ⇒ true ].
+definition checkb_desc_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
+ match get_desc_env_aux d e str with [ None ⇒ false | Some _ ⇒ true ].
 
-lemma checkbdescenv_to_checkdescenv : ∀e,str.checkb_desc_env e str = true → check_desc_env e str.
+lemma checkbdescenv_to_checkdescenv : ∀d.∀e:aux_env_type d.∀str.checkb_desc_env d e str = true → check_desc_env d e str.
  unfold checkb_desc_env;
  unfold check_desc_env;
  intros;
- letin K ≝ (get_desc_env_aux e str);
+ letin K ≝ (get_desc_env_aux d 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 str with
+definition get_desc_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
+ match get_desc_env_aux d 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_first_neList ? e) str with [ None ⇒ True | Some _ ⇒ False ].
+definition check_not_already_def_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
+ match get_desc_from_lev_env (get_first_envList d 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_first_neList ? e) str with [ None ⇒ true | Some _ ⇒ false ].
+definition checkb_not_already_def_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
+ match get_desc_from_lev_env (get_first_envList d 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.
+lemma checkbnotalreadydefenv_to_checknotalreadydefenv : ∀d.∀e:aux_env_type d.∀str.checkb_not_already_def_env d e str = true → check_not_already_def_env d e str.
  unfold checkb_not_already_def_env;
  unfold check_not_already_def_env;
  intros;
- letin K ≝ (get_desc_from_lev_env (get_first_neList ? e) str);
+ letin K ≝ (get_desc_from_lev_env (get_first_envList d e) str);
  elim K;
  [ normalize; autobatch |
    normalize; autobatch ]
@@ -130,11 +162,13 @@ qed.
 
 (* 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.
+λd.λe:aux_env_type d.λstr:aux_str_type.λc:bool.λdesc:ast_type.
 (*let var ≝ VAR_ELEM str (DESC_ELEM c desc) in*)
- match e with
-  [ 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
+ match e
+  return λX.λe:aux_env_type X.aux_env_type X
+ with
+  [ env_nil h ⇒ env_nil ((VAR_ELEM str (DESC_ELEM c desc))::h)
+  | env_cons n h t ⇒ env_cons n ((VAR_ELEM str (DESC_ELEM c desc))::h) t
   ].
 
 (* controllo e <= e' *)