mod change (-x)

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

diff --git a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma
old mode 100755 (executable)
new mode 100644 (file)
index 82666ac..6262486
--- a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma
+++ b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma
@@ -19,86 +19,87 @@
 (*                                                                        *)
 (* ********************************************************************** *)
 
-include "string/string.ma".
-include "compiler/utility.ma".
-include "freescale/word32.ma".
-include "compiler/ast_type.ma".
 include "compiler/env_to_flatenv.ma".
-include "compiler/ast_tree.ma".
 
 (* **************************** *)
 (* ALBERO DI TOKEN CON FLAT ENV *)
 (* **************************** *)
 
 (* id: accesso all'ambiente con stringa *)
-inductive astfe_id : bool → ast_type → Type ≝
-  ASTFE_ID: ∀str:aux_strId_type.∀b:bool.∀t:ast_type.
-            astfe_id b t.
+inductive astfe_id (e:aux_flatEnv_type) : bool → ast_type → Type ≝
+  ASTFE_ID: ∀str:aux_strId_type.
+            (* D *) check_desc_flatEnv e str → astfe_id e (get_const_desc (get_desc_flatEnv e str)) (get_type_desc (get_desc_flatEnv e str)).
 
 (* -------------------------- *)
 
 (* espressioni *)
-inductive astfe_expr : ast_type → Type ≝
-  ASTFE_EXPR_BYTE8 : byte8 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
-| ASTFE_EXPR_WORD16: word16 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
-| ASTFE_EXPR_WORD32: word32 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+inductive astfe_expr (e:aux_flatEnv_type) : ast_type → Type ≝
+  ASTFE_EXPR_BYTE8 : byte8 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_WORD16: word16 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| ASTFE_EXPR_WORD32: word32 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
 
 | ASTFE_EXPR_NEG: ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
 | ASTFE_EXPR_NOT: ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
 | ASTFE_EXPR_COM: ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
 
 | ASTFE_EXPR_ADD: ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
 | ASTFE_EXPR_SUB: ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
 | ASTFE_EXPR_MUL: ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
 | ASTFE_EXPR_DIV: ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
 | ASTFE_EXPR_SHR: ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE t)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t)
 | ASTFE_EXPR_SHL: ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE t)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t)
+| ASTFE_EXPR_AND: ∀t:ast_base_type.
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
+| ASTFE_EXPR_OR:  ∀t:ast_base_type.
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
+| ASTFE_EXPR_XOR: ∀t:ast_base_type.
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
 
 | ASTFE_EXPR_GT : ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 | ASTFE_EXPR_GTE: ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 | ASTFE_EXPR_LT : ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 | ASTFE_EXPR_LTE: ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 | ASTFE_EXPR_EQ : ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 | ASTFE_EXPR_NEQ: ∀t:ast_base_type.
-                  astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 
-| ASTFE_EXPR_B8toW16 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
-| ASTFE_EXPR_B8toW32 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
-| ASTFE_EXPR_W16toB8 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
-| ASTFE_EXPR_W16toW32: astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
-| ASTFE_EXPR_W32toB8 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
-| ASTFE_EXPR_W32toW16: astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| ASTFE_EXPR_B8toW16 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| ASTFE_EXPR_B8toW32 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| ASTFE_EXPR_W16toB8 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_W16toW32: astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| ASTFE_EXPR_W32toB8 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_W32toW16: astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
 
 | ASTFE_EXPR_ID: ∀b:bool.∀t:ast_type.
-                 astfe_var b t → astfe_expr t
+                 astfe_var e b t → astfe_expr e t
 
 (* variabile: modificatori di array/struct dell'id *)
 with astfe_var : bool → ast_type → Type ≝
   ASTFE_VAR_ID: ∀b:bool.∀t:ast_type.
-                astfe_id b t → astfe_var b t
+                astfe_id e b t → astfe_var e b t
 | ASTFE_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
-                   astfe_var b (AST_TYPE_ARRAY t n) → astfe_base_expr → astfe_var b t
+                   astfe_var e b (AST_TYPE_ARRAY t n) → astfe_base_expr e → astfe_var e b t
 | ASTFE_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
-                    astfe_var b (AST_TYPE_STRUCT nel) → astfe_var b (abs_nth_neList ? nel n)
+                    astfe_var e b (AST_TYPE_STRUCT nel) → astfe_var e b (abs_nth_neList ? nel n)
 
 (* espressioni generalizzate: anche non uniformi per tipo *)
 with astfe_base_expr : Type ≝
   ASTFE_BASE_EXPR: ∀t:ast_base_type.
-                   astfe_expr (AST_TYPE_BASE t) → astfe_base_expr.
+                   astfe_expr e (AST_TYPE_BASE t) → astfe_base_expr e.
 
 (* -------------------------- *)
 
@@ -107,34 +108,34 @@ with astfe_base_expr : Type ≝
   1) var1 = var2
   2) var = ... valori ...
 *) 
-inductive astfe_init : ast_type → Type ≝
+inductive astfe_init (e:aux_flatEnv_type) : ast_type → Type ≝
   ASTFE_INIT_VAR: ∀b:bool.∀t:ast_type.
-                  astfe_var b t → astfe_init t
+                  astfe_var e b t → astfe_init e t
 | ASTFE_INIT_VAL: ∀t:ast_type.
-                  aux_ast_init_type t → astfe_init t.
+                  aux_ast_init_type t → astfe_init e t.
 
 (* -------------------------- *)
 
 (* statement: assegnamento/while/if else if else + conversione di dichiarazione *)
-inductive astfe_stm : Type ≝
+inductive astfe_stm (e:aux_flatEnv_type) : Type ≝
   ASTFE_STM_ASG: ∀t:ast_type.
-                 astfe_var false t → astfe_expr t → astfe_stm
+                 astfe_var e false t → astfe_expr e t → astfe_stm e
 | ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
-                  astfe_id b t → astfe_init t → astfe_stm
-| ASTFE_STM_WHILE: astfe_base_expr → astfe_body → astfe_stm
-| ASTFE_STM_IF: ne_list (Prod astfe_base_expr astfe_body) → option astfe_body → astfe_stm
+                  astfe_id e b t → astfe_init e t → astfe_stm e
+| ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
+| ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
 
 (* dichiarazioni *)
 with astfe_body : Type ≝
-  ASTFE_BODY: list astfe_stm → astfe_body.
+  ASTFE_BODY: list (astfe_stm e) → astfe_body e.
 
 (* -------------------------- *)
 
 (* programma *)
-inductive astfe_root : Type ≝
-  ASTFE_ROOT: aux_flatEnv_type → astfe_body → astfe_root.
+inductive astfe_root (e:aux_flatEnv_type) : Type ≝
+  ASTFE_ROOT: astfe_body e → astfe_root e.
 
 (* -------------------------- *)
 
 (* programma vuoto *)
-definition empty_astfe_prog ≝ ASTFE_ROOT empty_flatEnv (ASTFE_BODY (nil ?)).
+definition empty_astfe_prog ≝ ASTFE_ROOT empty_flatEnv (ASTFE_BODY empty_flatEnv (nil ?)).