X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fast_to_astfe.ma;h=90a59130a9e1064b1baaf6972ee175cd544892c9;hb=e1efca300fbaeb8c69a691a428a084d89a2c058f;hp=c6d859c4e207a65c653a3e883af602bdb2bca09a;hpb=5688b80cf330cc66038720e04cf7c0293630c163;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
index c6d859c4e..90a59130a 100755
--- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
@@ -36,12 +36,11 @@ lemma ast_to_astfe_id :
  ∀dimInv:env_to_flatEnv_inv d e m fe.
  astfe_id fe b t.
  intros 7;
- unfold env_to_flatEnv_inv;
  elim a 0;
  intros 3;
  lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?);
- [ apply (proj2 ?? (proj1 ?? (H1 a1 H)))
- | rewrite > (proj2 ?? (H1 a1 H));
+ [ apply (proj2 ?? (proj1 ?? ((env_to_flatEnv_inv_last ???? H1) a1 H)))
+ | rewrite > (proj2 ?? ((env_to_flatEnv_inv_last ???? H1) a1 H));
    apply Hletin
  ].
 qed.
@@ -53,7 +52,6 @@ lemma ast_to_astfe_retype_id :
  ∀dimLe:le_flatEnv fe fe' = true.
  astfe_id fe' b t.
  intros 8;
- unfold env_to_flatEnv_inv;
  elim a 0;
  intros 4;
  lapply (ASTFE_ID fe' a1 ?);
@@ -87,6 +85,12 @@ qed.
                 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 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_AND: ∀t:ast_base_type.
+                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_OR:  ∀t:ast_base_type.
+                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_XOR: ∀t:ast_base_type.
+                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_GT : ∀t:ast_base_type.
                 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)
@@ -148,6 +152,15 @@ let rec ast_to_astfe_expr d (e:aux_env_type d) t (ast:ast_expr d e t)
   | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒
    ASTFE_EXPR_SHL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
                            (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
+  | AST_EXPR_AND bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_AND fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_OR bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_OR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_XOR bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_XOR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 
   | AST_EXPR_GT bType sExpr1 sExpr2 ⇒
    ASTFE_EXPR_GT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
@@ -260,6 +273,15 @@ let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
   | ASTFE_EXPR_SHL bType sExpr1 sExpr2 ⇒
    ASTFE_EXPR_SHL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_AND bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_AND fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_OR bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_OR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_XOR bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_XOR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 
   | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒
    ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
@@ -579,8 +601,10 @@ let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux
 (*
   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.
-            (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
+| AST_CONST_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
+                  (check_not_already_def_env d e str) → ast_init d e t → ast_decl d (add_desc_env d e str true t) → ast_decl d e
+| AST_VAR_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
+                (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str false t) → ast_decl d e
 *)
 and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe.
                                                                        env_to_flatEnv_inv d e m fe →
@@ -613,40 +637,73 @@ and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_m
                               (env_map_flatEnv_addNil_aux sD sE resMap resFe resDimInv)
                               resDimLe resLStm ]
 
-   | AST_DECL sD sE sB sName sType sDim sOptInit sDecl ⇒
+   | AST_CONST_DECL sD sE sName sType sDim sInit sDecl ⇒
+    λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
+    match ast_to_astfe_decl sD (add_desc_env sD sE sName true sType) sDecl
+          (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+          (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+          (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv) with
+     [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+      AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
+                               ([ tripleT ??? sName true sType ]@resTrsf)
+                               (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
+                               (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe)
+                               ([ ASTFE_STM_INIT resFe true sType
+                                                 (* l'id e' sull'ambiente arricchito *)
+                                                 (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+                                                                         true sType
+                                                                         (ast_to_astfe_id sD (add_desc_env sD sE sName true sType)
+                                                                                          true sType
+                                                                                          (newid_from_init sD sE sName true sType)
+                                                                                          (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+                                                                                          (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+                                                                                          (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv))
+                                                                         sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE)
+                                                                         resMap resFe
+                                                                         (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
+                                                                         resDimLe)
+                                                 (* l'init e' sull'ambiente non arricchito *)
+                                                 (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType sInit m fe dimInv)
+                                                                           sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE)
+                                                                           resMap resFe
+                                                                           (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
+                                                                           (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe))
+                                ]@resLStm) ]
+
+   | AST_VAR_DECL sD sE sName sType sDim sOptInit sDecl ⇒
     λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
-    match ast_to_astfe_decl sD (add_desc_env sD sE sName sB sType) sDecl
-          (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
-          (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
-          (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv) with
+    match ast_to_astfe_decl sD (add_desc_env sD sE sName false sType) sDecl
+          (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+          (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+          (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv) with
      [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
       AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
-                               ([ tripleT ??? sName sB sType ]@resTrsf)
-                               (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
-                               (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe)
+                               ([ tripleT ??? sName false sType ]@resTrsf)
+                               (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
+                               (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe)
                                (match sOptInit with
                                 [ None ⇒ []
                                 | Some init ⇒
-                                 [ ASTFE_STM_INIT resFe sB sType
+                                 [ ASTFE_STM_INIT resFe false sType
                                                   (* l'id e' sull'ambiente arricchito *)
-                                                  (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
-                                                                          sB sType
-                                                                          (ast_to_astfe_id sD (add_desc_env sD sE sName sB sType)
-                                                                                           sB sType
-                                                                                           (newid_from_init sD sE sName sB sType)
-                                                                                           (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
-                                                                                           (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
-                                                                                           (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv))
-                                                                          sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE)
+                                                  (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+                                                                          false sType
+                                                                          (ast_to_astfe_id sD (add_desc_env sD sE sName false sType)
+                                                                                           false sType
+                                                                                           (newid_from_init sD sE sName false sType)
+                                                                                           (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+                                                                                           (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+                                                                                           (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv))
+                                                                          sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE)
                                                                           resMap resFe
-                                                                          (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
+                                                                          (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
                                                                           resDimLe)
                                                   (* l'init e' sull'ambiente non arricchito *)
                                                   (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType init m fe dimInv)
-                                                                            sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE)
+                                                                            sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE)
                                                                             resMap resFe
-                                                                            (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
-                                                                            (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe))
+                                                                            (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
+                                                                            (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe))
                                  ]]@resLStm) ]          
 
    ].