∀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.
∀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 ?);
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)
| 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)
| 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)
(*
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 →
(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) ]
].