X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fast_tree.ma;h=553991bd79c53c5b08bd04f61b1dc25ee31af9f6;hb=db1552c8344acc3de1f0596d999170046eb0c8fa;hp=6ba41f18c5a4144edffef898cb365d3e36ae10fb;hpb=a8ad55eb789b38c85c5581089308e349e4b0f1a3;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
index 6ba41f18c..553991bd7 100755
--- a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
@@ -26,74 +26,74 @@ include "compiler/environment.ma".
 (* *************** *)
 
 (* id: accesso all'ambiente con stringa *)
-inductive ast_id (e:aux_env_type) : bool → ast_type → Type ≝
+inductive ast_id (d:nat) (e:aux_env_type d) : bool → ast_type → Type ≝
   AST_ID: ∀str:aux_str_type.
-          (* D *) (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str))).
+          (* D *) (check_desc_env d e str) → (ast_id d e (get_const_desc (get_desc_env d e str)) (get_type_desc (get_desc_env d e str))).
 
 (* -------------------------- *)
 
 (* espressioni *)
-inductive ast_expr (e:aux_env_type) : ast_type → Type ≝
-  AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
-| AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
-| AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+inductive ast_expr (d:nat) (e:aux_env_type d) : ast_type → Type ≝
+  AST_EXPR_BYTE8 : byte8 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_WORD16: word16 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| AST_EXPR_WORD32: word32 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
 
 | AST_EXPR_NEG: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
 | AST_EXPR_NOT: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
 | AST_EXPR_COM: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
 
 | AST_EXPR_ADD: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
 | AST_EXPR_SUB: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
 | AST_EXPR_MUL: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
 | AST_EXPR_DIV: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
 | AST_EXPR_SHR: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
 | AST_EXPR_SHL: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
 
 | AST_EXPR_GT : ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 | AST_EXPR_GTE: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 | AST_EXPR_LT : ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 | AST_EXPR_LTE: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 | AST_EXPR_EQ : ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 | AST_EXPR_NEQ: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 
-| AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
-| AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
-| AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
-| AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
-| AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
-| AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| AST_EXPR_B8toW16 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| AST_EXPR_B8toW32 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| AST_EXPR_W16toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_W16toW32: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| AST_EXPR_W32toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_W32toW16: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
 
 | AST_EXPR_ID: ∀b:bool.∀t:ast_type.
-               ast_var e b t → ast_expr e t
+               ast_var d e b t → ast_expr d e t
 
 (* variabile: modificatori di array/struct dell'id *)
 with ast_var : bool → ast_type → Type ≝
   AST_VAR_ID: ∀b:bool.∀t:ast_type.
-              ast_id e b t → ast_var e b t
+              ast_id d e b t → ast_var d e b t
 | AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
-                 ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
+                 ast_var d e b (AST_TYPE_ARRAY t n) → ast_base_expr d e → ast_var d e b t
 | AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
-                  ast_var e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
+                  ast_var d e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var d e b (abs_nth_neList ? nel n)
 
 (* espressioni generalizzate: anche non uniformi per tipo *)
 with ast_base_expr : Type ≝
   AST_BASE_EXPR: ∀t:ast_base_type.
-                 ast_expr e (AST_TYPE_BASE t) → ast_base_expr e.
+                 ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d e.
 
 (* -------------------------- *)
 
@@ -126,37 +126,37 @@ let rec aux_ast_init_type (t:ast_type) on t : Type ≝
   1) var1 = var2
   2) var = ... valori ...
 *) 
-inductive ast_init (e:aux_env_type) : ast_type → Type ≝
+inductive ast_init (d:nat) (e:aux_env_type d) : ast_type → Type ≝
   AST_INIT_VAR: ∀b:bool.∀t:ast_type.
-                ast_var e b t → ast_init e t
+                ast_var d e b t → ast_init d e t
 | AST_INIT_VAL: ∀t:ast_type.
-                aux_ast_init_type t → ast_init e t.
+                aux_ast_init_type t → ast_init d e t.
 
 (* -------------------------- *)
 
 (* statement: assegnamento/while/if else if else *)
-inductive ast_stm : aux_env_type → Type ≝
-  AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
-               ast_var e false t → ast_expr e t → ast_stm e
-| AST_STM_WHILE: ∀e:aux_env_type.
-                 ast_base_expr e → ast_decl (enter_env e) → ast_stm e
-| AST_STM_IF: ∀e:aux_env_type.
-              ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
+inductive ast_stm : Πd:nat.aux_env_type d → Type ≝
+  AST_STM_ASG: ∀d.∀e:aux_env_type d.∀t:ast_type.
+               ast_var d e false t → ast_expr d e t → ast_stm d e
+| AST_STM_WHILE: ∀d.∀e:aux_env_type d.
+                 ast_base_expr d e → ast_decl (S d) (enter_env d e) → ast_stm d e
+| AST_STM_IF: ∀d.∀e:aux_env_type d.
+              ne_list (Prod (ast_base_expr d e) (ast_decl (S d) (enter_env d e))) → option (ast_decl (S d) (enter_env d e)) → ast_stm d e
 
 (* dichiarazioni *)
-with ast_decl : aux_env_type → Type ≝
-  AST_NO_DECL: ∀e:aux_env_type.
-               list (ast_stm e) → ast_decl e
-| AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
-            (* D *) (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e.
+with ast_decl : Πd:nat.aux_env_type d → Type ≝
+  AST_NO_DECL: ∀d.∀e:aux_env_type d.
+               list (ast_stm d e) → ast_decl d e
+| AST_DECL: ∀d.∀e:aux_env_type d.∀c:bool.∀str:aux_str_type.∀t:ast_type.
+            (* D *) (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str c t) → ast_decl d e.
 
 (* -------------------------- *)
 
 (* programma *)
 inductive ast_root : Type ≝
-  AST_ROOT: ast_decl empty_env → ast_root.
+  AST_ROOT: ast_decl O empty_env → ast_root.
 
 (* -------------------------- *)
 
 (* programma vuoto *)
-definition empty_ast_prog ≝ AST_ROOT (AST_NO_DECL empty_env (nil ?)).
+definition empty_ast_prog ≝ AST_ROOT (AST_NO_DECL O empty_env (nil ?)).