Update.

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

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
index 6fa1b3ffdb500083e97de231190b4d1e1cc1825b..6ba41f18c5a4144edffef898cb365d3e36ae10fb 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
@@ -33,53 +33,53 @@ inductive ast_id (e:aux_env_type) : bool → ast_type → Type ≝
 (* -------------------------- *)
 
 (* espressioni *)
-inductive ast_expr (e:aux_env_type) : ast_base_type → Type ≝
-  AST_EXPR_BYTE8 : byte8 → ast_expr e AST_BASE_TYPE_BYTE8
-| AST_EXPR_WORD16: word16 → ast_expr e AST_BASE_TYPE_WORD16
-| AST_EXPR_WORD32: word32 → ast_expr e AST_BASE_TYPE_WORD32
+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)
 
 | AST_EXPR_NEG: ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t
+                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 | AST_EXPR_NOT: ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t
+                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 | AST_EXPR_COM: ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t
+                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 
 | AST_EXPR_ADD: ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t → ast_expr e t
+                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 | AST_EXPR_SUB: ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t → ast_expr e t
+                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 | AST_EXPR_MUL: ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t → ast_expr e t
+                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 | AST_EXPR_DIV: ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t → ast_expr e t
+                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 | AST_EXPR_SHR: ∀t:ast_base_type.
-                ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e t
+                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_SHL: ∀t:ast_base_type.
-                ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e t
+                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_GT : ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+                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_GTE: ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+                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_LT : ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+                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_LTE: ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+                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_EQ : ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+                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_NEQ: ∀t:ast_base_type.
-                ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+                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_B8toW16 : ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e AST_BASE_TYPE_WORD16
-| AST_EXPR_B8toW32 : ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e AST_BASE_TYPE_WORD32
-| AST_EXPR_W16toB8 : ast_expr e AST_BASE_TYPE_WORD16 → ast_expr e AST_BASE_TYPE_BYTE8
-| AST_EXPR_W16toW32: ast_expr e AST_BASE_TYPE_WORD16 → ast_expr e AST_BASE_TYPE_WORD32
-| AST_EXPR_W32toB8 : ast_expr e AST_BASE_TYPE_WORD32 → ast_expr e AST_BASE_TYPE_BYTE8
-| AST_EXPR_W32toW16: ast_expr e AST_BASE_TYPE_WORD32 → ast_expr e AST_BASE_TYPE_WORD16
+| 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_ID: ∀b:bool.∀t:ast_base_type.
-               ast_var e b (AST_TYPE_BASE t) → ast_expr e t
+| AST_EXPR_ID: ∀b:bool.∀t:ast_type.
+               ast_var e b t → ast_expr e t
 
 (* variabile: modificatori di array/struct dell'id *)
 with ast_var : bool → ast_type → Type ≝
@@ -93,16 +93,7 @@ with ast_var : bool → ast_type → Type ≝
 (* espressioni generalizzate: anche non uniformi per tipo *)
 with ast_base_expr : Type ≝
   AST_BASE_EXPR: ∀t:ast_base_type.
-                 ast_expr e t → ast_base_expr e.
-
-(* -------------------------- *)
-
-(* espressioni destre di assegnamento *)
-inductive ast_right_expr (e:aux_env_type) : ast_type → Type ≝
-  AST_RIGHT_EXPR_BASE: ∀t:ast_base_type.
-                       ast_expr e t → ast_right_expr e (AST_TYPE_BASE t)
-| AST_RIGHT_EXPR_VAR: ∀b:bool.∀t:ast_type.
-                      ast_var e b t → ast_right_expr e t.
+                 ast_expr e (AST_TYPE_BASE t) → ast_base_expr e.
 
 (* -------------------------- *)
 
@@ -146,11 +137,11 @@ inductive ast_init (e:aux_env_type) : ast_type → Type ≝
 (* 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_right_expr e t → ast_stm e
+               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 e → ast_stm e
+                 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 e)) → option (ast_decl e) → ast_stm e
+              ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
 
 (* dichiarazioni *)
 with ast_decl : aux_env_type → Type ≝