Snapshot.

[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 381ea92fb0387fe5e2d94a08c0fb353e32cabc23..79be3a54e09b2129d5c6704127cc19cd8e705e73 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
@@ -81,29 +81,72 @@ inductive ast_expr (e:aux_env_type) : ast_base_type → Type ≝
 | AST_EXPR_ID: ∀b:bool.∀t:ast_base_type.
                ast_var e b (AST_TYPE_BASE t) → ast_expr e t
 
-(* 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
-
 (* 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
-                 (* NB: l'index out of bound e' delegato a runtime? *)
 | 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_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 e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var 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 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.
+
+(* -------------------------- *)
+
+let rec aux_ast_init_type (t:ast_type) on t : Type ≝
+ match t with
+  [ AST_TYPE_BASE bType ⇒ match bType with
+   [ AST_BASE_TYPE_BYTE8 ⇒ byte8
+   | AST_BASE_TYPE_WORD16 ⇒ word16
+   | AST_BASE_TYPE_WORD32 ⇒ word32
+   ] 
+  | AST_TYPE_ARRAY subType dim ⇒
+   let T ≝ aux_ast_init_type subType in
+   let rec aux (n:nat) on n ≝
+    match n with
+     [ O ⇒ T
+     | S n' ⇒ Prod T (aux n')
+     ] in
+   aux dim 
+  | AST_TYPE_STRUCT nelSubType ⇒
+   let rec aux (nel:ne_list ast_type) on nel ≝
+    match nel with
+     [ ne_nil h ⇒ aux_ast_init_type h
+     | ne_cons h t ⇒ Prod (aux_ast_init_type h) (aux t)
+     ] in
+    aux nelSubType 
+  ].
+
+(*
+ inizializzatori: ammesse solo due forme, no ibridi
+  1) var1 = var2
+  2) var = ... valori ...
+*) 
+inductive ast_init (e:aux_env_type) : ast_type → Type ≝
+  AST_INIT_VAR: ∀b:bool.∀t:ast_type.
+                ast_var e b t → ast_init e t
+| AST_INIT_VAL: ∀t:ast_type.
+                aux_ast_init_type t → ast_init 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_base_type.
-               ast_var e false (AST_TYPE_BASE t) → ast_expr e t → ast_stm e
-| AST_STM_MEMCPY_ASG: ∀e:aux_env_type.∀b:bool.∀t:ast_type.
-                      (* D *) isnt_ast_base_type t → ast_var e false t → ast_var e b t → ast_stm e
+  AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
+               ast_var e false t → ast_right_expr e t → ast_stm e
 | AST_STM_WHILE: ∀e:aux_env_type.
                  ast_base_expr e → ast_decl e → ast_stm e
 | AST_STM_IF: ∀e:aux_env_type.
@@ -113,10 +156,8 @@ inductive ast_stm : aux_env_type → Type ≝
 with ast_decl : aux_env_type → Type ≝
   AST_NO_DECL: ∀e:aux_env_type.
                list (ast_stm e) → ast_decl e
-| AST_BASE_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_base_type.
-                 (* D *) (check_not_already_def_env e str) → option (ast_expr e t) → ast_decl (add_desc_env e str c (AST_TYPE_BASE t)) → 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) → (* D *) isnt_ast_base_type t → ast_decl (add_desc_env e str c t) → ast_decl e.
+            (* 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.
 
 (* -------------------------- *)