(* PASSO 2 : da AST a ASTFE *)
(* ************************ *)
-(* operatore di cast *)
-definition ast_to_astfe_expr_check : Πfe.Πt.astfe_expr fe t → Πt'.option (astfe_expr fe t') ≝
-λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_expr fe t.λt':ast_type.
- match eq_ast_type t t'
- return λx.(eq_ast_type t t' = x) → ?
- with
- [ true ⇒ λp:(eq_ast_type t t' = true).
- Some ? (eq_rect ? t (λt.astfe_expr fe t) ast t' (eqasttype_to_eq ?? p))
- | false ⇒ λp:(eq_ast_type t t' = false).None ?
- ] (refl_eq ? (eq_ast_type t t')).
-
-definition ast_to_astfe_init_check : Πfe.Πt.astfe_init fe t → Πt'.option (astfe_init fe t') ≝
-λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_init fe t.λt':ast_type.
- match eq_ast_type t t'
- return λx.(eq_ast_type t t' = x) → ?
- with
- [ true ⇒ λp:(eq_ast_type t t' = true).
- Some ? (eq_rect ? t (λt.astfe_init fe t) ast t' (eqasttype_to_eq ?? p))
- | false ⇒ λp:(eq_ast_type t t' = false).None ?
- ] (refl_eq ? (eq_ast_type t t')).
-
-definition ast_to_astfe_var_checkb : Πfe.Πb.Πt.astfe_var fe b t → Πb'.option (astfe_var fe b' t) ≝
-λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_var fe b t.λb':bool.
- match eq_bool b b'
- return λx.(eq_bool b b' = x) → ?
- with
- [ true ⇒ λp:(eq_bool b b' = true).
- Some ? (eq_rect ? b (λb.astfe_var fe b t) ast b' (eqbool_to_eq ?? p))
- | false ⇒ λp:(eq_bool b b' = false).None ?
- ] (refl_eq ? (eq_bool b b')).
-
-definition ast_to_astfe_var_checkt : Πfe.Πb.Πt.astfe_var fe b t → Πt'.option (astfe_var fe b t') ≝
-λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_var fe b t.λt':ast_type.
- match eq_ast_type t t'
- return λx.(eq_ast_type t t' = x) → ?
- with
- [ true ⇒ λp:(eq_ast_type t t' = true).
- Some ? (eq_rect ? t (λt.astfe_var fe b t) ast t' (eqasttype_to_eq ?? p))
- | false ⇒ λp:(eq_ast_type t t' = false).None ?
- ] (refl_eq ? (eq_ast_type t t')).
-
-definition ast_to_astfe_var_check : Πfe.Πb.Πt.astfe_var fe b t → Πb'.Πt'.option (astfe_var fe b' t') ≝
-λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_var fe b t.λb':bool.λt':ast_type.
- opt_map ?? (ast_to_astfe_var_checkb fe b t ast b')
- (λres.opt_map ?? (ast_to_astfe_var_checkt fe b' t res t')
- (λres'.Some ? res')).
-
-definition ast_to_astfe_id_checkb : Πfe.Πb.Πt.astfe_id fe b t → Πb'.option (astfe_id fe b' t) ≝
-λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λb':bool.
- match eq_bool b b'
- return λx.(eq_bool b b' = x) → ?
- with
- [ true ⇒ λp:(eq_bool b b' = true).
- Some ? (eq_rect ? b (λb.astfe_id fe b t) ast b' (eqbool_to_eq ?? p))
- | false ⇒ λp:(eq_bool b b' = false).None ?
- ] (refl_eq ? (eq_bool b b')).
-
-definition ast_to_astfe_id_checkt : Πfe.Πb.Πt.astfe_id fe b t → Πt'.option (astfe_id fe b t') ≝
-λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λt':ast_type.
- match eq_ast_type t t'
- return λx.(eq_ast_type t t' = x) → ?
- with
- [ true ⇒ λp:(eq_ast_type t t' = true).
- Some ? (eq_rect ? t (λt.astfe_id fe b t) ast t' (eqasttype_to_eq ?? p))
- | false ⇒ λp:(eq_ast_type t t' = false).None ?
- ] (refl_eq ? (eq_ast_type t t')).
-
-definition ast_to_astfe_id_check : Πfe.Πb.Πt.astfe_id fe b t → Πb'.Πt'.option (astfe_id fe b' t') ≝
-λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λb':bool.λt':ast_type.
- opt_map ?? (ast_to_astfe_id_checkb fe b t ast b')
- (λres.opt_map ?? (ast_to_astfe_id_checkt fe b' t res t')
- (λres'.Some ? res')).
-
(*
AST_ID: ∀str:aux_str_type.
(check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str)))
*)
-definition get_name_ast_id ≝
-λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.
- match ast with [ AST_ID s _ ⇒ s ].
-
-definition ast_to_astfe_id :
- Πe:aux_env_type.Πb:bool.Πt:ast_type.Πast:ast_id e b t.Πfe:aux_flatEnv_type.
- Πmap:aux_trasfMap_type e fe.
- astfe_id fe
- (get_const_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))))
- (get_type_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))) ≝
-λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.λfe:aux_flatEnv_type.λmap:aux_trasfMap_type e fe.
- ASTFE_ID fe (name_to_nameId e fe map (get_name_ast_id e b t ast))
- (ast_to_astfe_id_aux e fe map (get_name_ast_id e b t ast)
- (ast_id_ind e
- (λHbeta3:bool.λHbeta2:ast_type.λHbeta1:ast_id e Hbeta3 Hbeta2.check_desc_env e (get_name_ast_id e Hbeta3 Hbeta2 Hbeta1))
- (λa:aux_str_type.λH:check_desc_env e a.H) b t ast)).
-
-definition get_name_astfe_id ≝ λfe,b,t.λast:astfe_id fe b t.match ast with [ ASTFE_ID n _ ⇒ n ].
-
-definition retype_id
-: Πfe:aux_flatEnv_type.Πb:bool.Πt:ast_type.Πast:astfe_id fe b t.Πfe':aux_flatEnv_type.le_flatEnv fe fe' = true →
- astfe_id fe'
- (get_const_desc (get_desc_flatEnv fe' (get_name_astfe_id fe b t ast)))
- (get_type_desc (get_desc_flatEnv fe' (get_name_astfe_id fe b t ast))) ≝
-λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
- ASTFE_ID fe' (get_name_astfe_id fe b t ast)
- (leflatenv_to_check fe fe' (get_name_astfe_id fe b t ast) dim (astfe_id_ind fe
- (λHbeta3:bool.λHbeta2:ast_type.λHbeta1:astfe_id fe Hbeta3 Hbeta2.check_desc_flatEnv fe (get_name_astfe_id fe Hbeta3 Hbeta2 Hbeta1))
- (λa:aux_strId_type.λH:check_desc_flatEnv fe a.H) b t ast)).
+lemma ast_to_astfe_id :
+ ∀d.∀e:aux_env_type d.∀b,t.∀ast:ast_id d e b t.
+ ∀m:aux_map_type d.∀fe.
+ ∀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 Hletin
+ ].
+qed.
+
+lemma ast_to_astfe_retype_id :
+ ∀fe,b,t.∀ast:astfe_id fe b t.
+ ∀d.∀e:aux_env_type d.∀m:aux_map_type d.∀fe'.
+ ∀dimInv:env_to_flatEnv_inv d e m fe'.
+ ∀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 ?);
+ [ apply (leflatenv_to_check fe fe' a1 H2 H)
+ | rewrite > (leflatenv_to_get fe fe' a1 H2 H);
+ apply Hletin
+ ].
+qed.
(*
AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
AST_EXPR_ID: ∀b:bool.∀t:ast_type.
ast_var e b t → ast_expr e t
*)
-let rec ast_to_astfe_expr (e:aux_env_type) (t:ast_type) (ast:ast_expr e t) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on ast : option (astfe_expr fe t) ≝
- match ast with
- [ AST_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe val) t
- | AST_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 fe val) t
- | AST_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 fe val) t
-
- | AST_EXPR_NEG bType subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG fe bType res) t)
- | AST_EXPR_NOT bType subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT fe bType res) t)
- | AST_EXPR_COM bType subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_COM fe bType res) t)
-
- | AST_EXPR_ADD bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD fe bType res1 res2) t))
- | AST_EXPR_SUB bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB fe bType res1 res2) t))
- | AST_EXPR_MUL bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL fe bType res1 res2) t))
- | AST_EXPR_DIV bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV fe bType res1 res2) t))
- | AST_EXPR_SHR bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR fe bType res1 res2) t))
- | AST_EXPR_SHL bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL fe bType res1 res2) t))
-
- | AST_EXPR_LT bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT fe bType res1 res2) t))
- | AST_EXPR_LTE bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE fe bType res1 res2) t))
- | AST_EXPR_GT bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT fe bType res1 res2) t))
- | AST_EXPR_GTE bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE fe bType res1 res2) t))
- | AST_EXPR_EQ bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ fe bType res1 res2) t))
- | AST_EXPR_NEQ bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ fe bType res1 res2) t))
-
- | AST_EXPR_B8toW16 subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 fe res) t)
- | AST_EXPR_B8toW32 subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 fe res) t)
- | AST_EXPR_W16toB8 subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 fe res) t)
- | AST_EXPR_W16toW32 subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 fe res) t)
- | AST_EXPR_W32toB8 subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 fe res) t)
- | AST_EXPR_W32toW16 subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 fe res) t)
-
- | AST_EXPR_ID b subType var ⇒
- opt_map ?? (ast_to_astfe_var e b subType var fe map)
- (λres.ast_to_astfe_expr_check fe subType (ASTFE_EXPR_ID fe b subType res) t)
+let rec ast_to_astfe_expr d (e:aux_env_type d) t (ast:ast_expr d e t)
+ (m:aux_map_type d) fe
+ (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_expr fe t ≝
+ match ast
+ return λW.λa:ast_expr d e W.astfe_expr fe W
+ with
+ [ AST_EXPR_BYTE8 val ⇒
+ ASTFE_EXPR_BYTE8 fe val
+ | AST_EXPR_WORD16 val ⇒
+ ASTFE_EXPR_WORD16 fe val
+ | AST_EXPR_WORD32 val ⇒
+ ASTFE_EXPR_WORD32 fe val
+
+ | AST_EXPR_NEG bType sExpr ⇒
+ ASTFE_EXPR_NEG fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
+ | AST_EXPR_NOT bType sExpr ⇒
+ ASTFE_EXPR_NOT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
+ | AST_EXPR_COM bType sExpr ⇒
+ ASTFE_EXPR_COM fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
+
+ | AST_EXPR_ADD bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_ADD 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_SUB bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_SUB 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_MUL bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_MUL 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_DIV bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_DIV 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_SHR bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_SHR 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_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_GT bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_GT 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_GTE bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_GTE 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_LT bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_LT 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_LTE bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_LTE 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_EQ bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_EQ 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_NEQ bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_NEQ 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_B8toW16 sExpr ⇒
+ ASTFE_EXPR_B8toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
+ | AST_EXPR_B8toW32 sExpr ⇒
+ ASTFE_EXPR_B8toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
+ | AST_EXPR_W16toB8 sExpr ⇒
+ ASTFE_EXPR_W16toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
+ | AST_EXPR_W16toW32 sExpr ⇒
+ ASTFE_EXPR_W16toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
+ | AST_EXPR_W32toB8 sExpr ⇒
+ ASTFE_EXPR_W32toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
+ | AST_EXPR_W32toW16 sExpr ⇒
+ ASTFE_EXPR_W32toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
+
+ | AST_EXPR_ID b sType var ⇒
+ ASTFE_EXPR_ID fe b sType (ast_to_astfe_var d e b sType var m fe dimInv)
+
]
(*
AST_VAR_ID: ∀b:bool.∀t:ast_type.
AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
*)
-and ast_to_astfe_var (e:aux_env_type) (b:bool) (t:ast_type) (ast:ast_var e b t) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on ast : option (astfe_var fe b t) ≝
- match ast with
- [ AST_VAR_ID subB subType subId ⇒
- opt_map ?? (ast_to_astfe_id_check fe ?? (ast_to_astfe_id e subB subType subId fe map) subB subType)
- (λresId.ast_to_astfe_var_check fe subB subType (ASTFE_VAR_ID fe subB subType resId) b t)
-
- | AST_VAR_ARRAY subB subType dim var expr ⇒
- opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_ARRAY subType dim) var fe map)
- (λresVar.opt_map ?? (ast_to_astfe_base_expr e expr fe map)
- (λresExpr.ast_to_astfe_var_check fe subB subType (ASTFE_VAR_ARRAY fe subB subType dim resVar resExpr) b t))
-
- | AST_VAR_STRUCT subB nelSubType field var _ ⇒
- opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_STRUCT nelSubType) var fe map)
- (λres.ast_to_astfe_var_check fe subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT fe subB nelSubType field res) b t)
+and ast_to_astfe_var d (e:aux_env_type d) b t (ast:ast_var d e b t)
+ (m:aux_map_type d) fe
+ (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_var fe b t ≝
+ match ast
+ return λW,X.λa:ast_var d e W X.astfe_var fe W X
+ with
+ [ AST_VAR_ID sB sType sId ⇒
+ ASTFE_VAR_ID fe sB sType (ast_to_astfe_id d e sB sType sId m fe dimInv)
+
+ | AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒
+ ASTFE_VAR_ARRAY fe sB sType sDim (ast_to_astfe_var d e sB (AST_TYPE_ARRAY sType sDim) sVar m fe dimInv)
+ (ast_to_astfe_base_expr d e sExpr m fe dimInv)
+
+ | AST_VAR_STRUCT sB sType sField sVar sLtb ⇒
+ ASTFE_VAR_STRUCT fe sB sType sField (ast_to_astfe_var d e sB (AST_TYPE_STRUCT sType) sVar m fe dimInv)
]
(*
AST_BASE_EXPR: ∀t:ast_base_type.
ast_expr e (AST_TYPE_BASE t) → ast_base_expr e
*)
-and ast_to_astfe_base_expr (e:aux_env_type) (ast:ast_base_expr e) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on ast : option (astfe_base_expr fe) ≝
- match ast with
- [ AST_BASE_EXPR bType subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
- (λres.Some ? (ASTFE_BASE_EXPR fe bType res))
+and ast_to_astfe_base_expr d (e:aux_env_type d) (ast:ast_base_expr d e)
+ (m:aux_map_type d) fe
+ (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_base_expr fe ≝
+ match ast
+ return λa:ast_base_expr d e.astfe_base_expr fe
+ with
+ [ AST_BASE_EXPR bType sExpr ⇒
+ ASTFE_BASE_EXPR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
].
-let rec retype_expr (fe:aux_flatEnv_type) (t:ast_type) (ast:astfe_expr fe t) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_expr fe' t) ≝
- match ast with
- [ ASTFE_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' val) t
- | ASTFE_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 fe' val) t
- | ASTFE_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 fe' val) t
-
- | ASTFE_EXPR_NEG bType subExpr ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
- (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG fe' bType res) t)
- | ASTFE_EXPR_NOT bType subExpr ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
- (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT fe' bType res) t)
- | ASTFE_EXPR_COM bType subExpr ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
- (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_COM fe' bType res) t)
-
- | ASTFE_EXPR_ADD bType subExpr1 subExpr2 ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
- (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
- (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD fe' bType res1 res2) t))
- | ASTFE_EXPR_SUB bType subExpr1 subExpr2 ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
- (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
- (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB fe' bType res1 res2) t))
- | ASTFE_EXPR_MUL bType subExpr1 subExpr2 ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
- (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
- (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL fe' bType res1 res2) t))
- | ASTFE_EXPR_DIV bType subExpr1 subExpr2 ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
- (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
- (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV fe' bType res1 res2) t))
- | ASTFE_EXPR_SHR bType subExpr1 subExpr2 ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
- (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe' dim)
- (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR fe' bType res1 res2) t))
- | ASTFE_EXPR_SHL bType subExpr1 subExpr2 ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
- (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe' dim)
- (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL fe' bType res1 res2) t))
-
- | ASTFE_EXPR_LT bType subExpr1 subExpr2 ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
- (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
- (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT fe' bType res1 res2) t))
- | ASTFE_EXPR_LTE bType subExpr1 subExpr2 ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
- (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
- (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE fe' bType res1 res2) t))
- | ASTFE_EXPR_GT bType subExpr1 subExpr2 ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
- (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
- (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT fe' bType res1 res2) t))
- | ASTFE_EXPR_GTE bType subExpr1 subExpr2 ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
- (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
- (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE fe' bType res1 res2) t))
- | ASTFE_EXPR_EQ bType subExpr1 subExpr2 ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
- (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
- (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ fe' bType res1 res2) t))
- | ASTFE_EXPR_NEQ bType subExpr1 subExpr2 ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
- (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
- (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ fe' bType res1 res2) t))
-
- | ASTFE_EXPR_B8toW16 subExpr ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe' dim)
- (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 fe' res) t)
- | ASTFE_EXPR_B8toW32 subExpr ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe' dim)
- (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 fe' res) t)
- | ASTFE_EXPR_W16toB8 subExpr ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe' dim)
- (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 fe' res) t)
- | ASTFE_EXPR_W16toW32 subExpr ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe' dim)
- (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 fe' res) t)
- | ASTFE_EXPR_W32toB8 subExpr ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe' dim)
- (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 fe' res) t)
- | ASTFE_EXPR_W32toW16 subExpr ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe' dim)
- (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 fe' res) t)
-
- | ASTFE_EXPR_ID b subType var ⇒
- opt_map ?? (retype_var fe b subType var fe' dim)
- (λres.ast_to_astfe_expr_check fe' subType (ASTFE_EXPR_ID fe' b subType res) t)
+let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
+ d (e:aux_env_type d) (m:aux_map_type d) fe'
+ (dimInv:env_to_flatEnv_inv d e m fe')
+ (dimLe:le_flatEnv fe fe' = true) on ast : astfe_expr fe' t ≝
+ match ast
+ return λW.λa:astfe_expr fe W.astfe_expr fe' W
+ with
+ [ ASTFE_EXPR_BYTE8 val ⇒
+ ASTFE_EXPR_BYTE8 fe' val
+ | ASTFE_EXPR_WORD16 val ⇒
+ ASTFE_EXPR_WORD16 fe' val
+ | ASTFE_EXPR_WORD32 val ⇒
+ ASTFE_EXPR_WORD32 fe' val
+
+ | ASTFE_EXPR_NEG bType sExpr ⇒
+ ASTFE_EXPR_NEG fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_NOT bType sExpr ⇒
+ ASTFE_EXPR_NOT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_COM bType sExpr ⇒
+ ASTFE_EXPR_COM fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
+
+ | ASTFE_EXPR_ADD bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_ADD 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_SUB bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_SUB 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_MUL bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_MUL 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_DIV bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_DIV 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_SHR bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_SHR 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_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_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_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_GTE bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_GTE 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_LT bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_LT 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_LTE bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_LTE 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_EQ bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_EQ 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_NEQ bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_NEQ 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_B8toW16 sExpr ⇒
+ ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_B8toW32 sExpr ⇒
+ ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_W16toB8 sExpr ⇒
+ ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_W16toW32 sExpr ⇒
+ ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_W32toB8 sExpr ⇒
+ ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_W32toW16 sExpr ⇒
+ ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
+
+ | ASTFE_EXPR_ID b sType var ⇒
+ ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe)
+
]
-and retype_var (fe:aux_flatEnv_type) (b:bool) (t:ast_type) (ast:astfe_var fe b t) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_var fe' b t) ≝
- match ast with
- [ ASTFE_VAR_ID subB subType subId ⇒
- opt_map ?? (ast_to_astfe_id_check fe' ?? (retype_id fe subB subType subId fe' dim) subB subType)
- (λresId.ast_to_astfe_var_check fe' subB subType (ASTFE_VAR_ID fe' subB subType resId) b t)
-
- | ASTFE_VAR_ARRAY subB subType n var expr ⇒
- opt_map ?? (retype_var fe subB (AST_TYPE_ARRAY subType n) var fe' dim)
- (λresVar.opt_map ?? (retype_base_expr fe expr fe' dim)
- (λresExpr.ast_to_astfe_var_check fe' subB subType (ASTFE_VAR_ARRAY fe' subB subType n resVar resExpr) b t))
-
- | ASTFE_VAR_STRUCT subB nelSubType field var ⇒
- opt_map ?? (retype_var fe subB (AST_TYPE_STRUCT nelSubType) var fe' dim)
- (λres.ast_to_astfe_var_check fe' subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT fe' subB nelSubType field res) b t)
+and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t)
+ d (e:aux_env_type d) (m:aux_map_type d) fe'
+ (dimInv:env_to_flatEnv_inv d e m fe')
+ (dimLe:le_flatEnv fe fe' = true) on ast : astfe_var fe' b t ≝
+ match ast
+ return λW,X.λa:astfe_var fe W X.astfe_var fe' W X
+ with
+ [ ASTFE_VAR_ID sB sType sId ⇒
+ ASTFE_VAR_ID fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
+
+ | ASTFE_VAR_ARRAY sB sType sDim sVar sExpr ⇒
+ ASTFE_VAR_ARRAY fe' sB sType sDim (ast_to_astfe_retype_var fe sB (AST_TYPE_ARRAY sType sDim) sVar d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
+
+ | ASTFE_VAR_STRUCT sB sType sField sVar ⇒
+ ASTFE_VAR_STRUCT fe' sB sType sField (ast_to_astfe_retype_var fe sB (AST_TYPE_STRUCT sType) sVar d e m fe' dimInv dimLe)
]
-and retype_base_expr (fe:aux_flatEnv_type) (ast:astfe_base_expr fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_base_expr fe') ≝
- match ast with
- [ ASTFE_BASE_EXPR bType subExpr ⇒
- opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
- (λres.Some ? (ASTFE_BASE_EXPR fe' bType res))
+and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe)
+ d (e:aux_env_type d) (m:aux_map_type d) fe'
+ (dimInv:env_to_flatEnv_inv d e m fe')
+ (dimLe:le_flatEnv fe fe' = true) on ast : astfe_base_expr fe' ≝
+ match ast
+ return λa:astfe_base_expr fe.astfe_base_expr fe'
+ with
+ [ ASTFE_BASE_EXPR bType sExpr ⇒
+ ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
].
(*
AST_INIT_VAL: ∀t:ast_type.
aux_ast_init_type t → ast_init e t
*)
-definition ast_to_astfe_init : Πe.Πt.ast_init e t → Πfe.aux_trasfMap_type e fe → option (astfe_init fe t) ≝
-λe:aux_env_type.λt:ast_type.λast:ast_init e t.λfe:aux_flatEnv_type.λmap:aux_trasfMap_type e fe.
- match ast with
- [ AST_INIT_VAR subB subType var ⇒
- opt_map ?? (ast_to_astfe_var e subB subType var fe map)
- (λres.ast_to_astfe_init_check fe subType (ASTFE_INIT_VAR fe subB subType res) t)
+definition ast_to_astfe_init ≝
+λd.λe:aux_env_type d.λt.λast:ast_init d e t.
+λm:aux_map_type d.λfe.
+λdimInv:env_to_flatEnv_inv d e m fe.
+ match ast
+ return λW.λa:ast_init d e W.astfe_init fe W
+ with
+ [ AST_INIT_VAR sB sType sVar ⇒
+ ASTFE_INIT_VAR fe sB sType (ast_to_astfe_var d e sB sType sVar m fe dimInv)
+
+ | AST_INIT_VAL sType sArgs ⇒
+ ASTFE_INIT_VAL fe sType sArgs
- | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe subType (ASTFE_INIT_VAL fe subType args) t
].
-definition retype_init ≝
-λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_init fe t.λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
- match ast with
- [ ASTFE_INIT_VAR subB subType var ⇒
- opt_map ?? (retype_var fe subB subType var fe' dim)
- (λres.ast_to_astfe_init_check fe' subType (ASTFE_INIT_VAR fe' subB subType res) t)
+definition ast_to_astfe_retype_init ≝
+λfe,t.λast:astfe_init fe t.
+λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
+λdimInv:env_to_flatEnv_inv d e m fe'.
+λdimLe:le_flatEnv fe fe' = true.
+ match ast
+ return λW.λa:astfe_init fe W.astfe_init fe' W
+ with
+ [ ASTFE_INIT_VAR sB sType sVar ⇒
+ ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe)
+
+ | ASTFE_INIT_VAL sType sArgs ⇒
+ ASTFE_INIT_VAL fe' sType sArgs
- | ASTFE_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe' subType (ASTFE_INIT_VAL fe' subType args) t
].
(*
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
*)
-let rec retype_stm (fe:aux_flatEnv_type) (ast:astfe_stm fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_stm fe') ≝
+let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe) d (e:aux_env_type d) m fe' dimInv dimLe on ast : astfe_stm fe' ≝
match ast with
- [ ASTFE_STM_ASG subType var expr ⇒
- opt_map ?? (retype_var fe false subType var fe' dim)
- (λresVar.opt_map ?? (retype_expr fe subType expr fe' dim)
- (λresExpr.Some ? (ASTFE_STM_ASG fe' subType resVar resExpr)))
-
- | ASTFE_STM_INIT subB subType subId init ⇒
- opt_map ?? (ast_to_astfe_id_check fe' ?? (retype_id fe subB subType subId fe' dim) subB subType)
- (λresId.opt_map ?? (retype_init fe subType init fe' dim)
- (λresInit.Some ? (ASTFE_STM_INIT fe' subB subType resId resInit)))
-
- | ASTFE_STM_WHILE expr body ⇒
- opt_map ?? (retype_base_expr fe expr fe' dim)
- (λresExpr.opt_map ?? (retype_body fe body fe' dim)
- (λresBody.Some ? (ASTFE_STM_WHILE fe' resExpr resBody)))
-
- | ASTFE_STM_IF nelExprBody optBody ⇒
- opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (retype_base_expr fe (fst ?? h) fe' dim)
- (λresExpr.opt_map ?? (retype_body fe (snd ?? h) fe' dim)
- (λresBody.opt_map ?? t
- (λt'.Some ? («£(pair ?? resExpr resBody)»&t')))))
- (Some ? (ne_nil ? (pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))))
- nelExprBody)
- (λres.match optBody with
- [ None ⇒ Some ? (ASTFE_STM_IF fe' (cut_last_neList ? res) (None ?))
- | Some body ⇒
- opt_map ?? (retype_body fe body fe' dim)
- (λresBody.Some ? (ASTFE_STM_IF fe' (cut_last_neList ? res) (Some ? resBody)))
- ])
+ [ ASTFE_STM_ASG sType sVar sExpr ⇒
+ ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe)
+
+ | ASTFE_STM_INIT sB sType sId sInit ⇒
+ ASTFE_STM_INIT fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe)
+
+ | ASTFE_STM_WHILE sExpr sBody ⇒
+ ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)
+
+ | ASTFE_STM_IF sNelExprBody sOptBody ⇒
+ ASTFE_STM_IF fe' (cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
+ )»&t)
+ «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
+ sNelExprBody))
+ (opt_map ?? sOptBody
+ (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)))
]
(*
ASTFE_BODY: list (astfe_stm e) → astfe_body e
*)
-and retype_body (fe:aux_flatEnv_type) (ast:astfe_body fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_body fe') ≝
+and ast_to_astfe_retype_body fe (ast:astfe_body fe) d (e:aux_env_type d) m fe' dimInv dimLe on ast : astfe_body fe' ≝
match ast with
- [ ASTFE_BODY lStm ⇒
- opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (retype_stm fe h fe' dim)
- (λh'.opt_map ?? t
- (λt'.Some ? ([h']@t')))) (Some ? []) lStm)
- (λresStm.Some ? (ASTFE_BODY fe' resStm))
+ [ ASTFE_BODY sLStm ⇒
+ ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] sLStm)
].
-definition retype_stm_list ≝
-λfe:aux_flatEnv_type.λast:list (astfe_stm fe).λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
- fold_right_list ?? (λh,t.opt_map ?? (retype_stm fe h fe' dim)
- (λh'.opt_map ?? t
- (λt'.Some ? ([h']@t')))) (Some ? []) ast.
-
-definition retype_exprAndBody_neList ≝
-λfe:aux_flatEnv_type.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
- opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (retype_base_expr fe (fst ?? h) fe' dim)
- (λresExpr.opt_map ?? (retype_body fe (snd ?? h) fe' dim)
- (λresBody.opt_map ?? t
- (λt'.Some ? («£(pair ?? resExpr resBody)»&t')))))
- (Some ? (ne_nil ? (pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))))
- ast)
- (λres.Some ? (cut_last_neList ? res)).
-
-(* applicare l'identita' e' inifluente *)
-lemma retype_map_to_id : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:(aux_env_type → aux_env_type).
- aux_trasfMap_type e fe → e = f e → aux_trasfMap_type (f e) fe.
- intros;
- apply (eq_rect ? e (λHbeta1:aux_env_type.aux_trasfMap_type Hbeta1 fe) a (f e) H);
-qed.
+definition ast_to_astfe_retype_stm_list ≝
+λfe.λast:list (astfe_stm fe).λd.λe:aux_env_type d.λm,fe',dimInv,dimLe.
+ fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] ast.
+
+definition ast_to_astfe_retype_exprBody_neList ≝
+λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).λd.λe:aux_env_type d.λm,fe',dimInv,dimLe.
+ cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
+ )»&t)
+ «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
+ ast).
(*
AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
AST_STM_IF: ∀e:aux_env_type.
ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
*)
-let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) on ast
- : Πmap:aux_trasfMap_type e fe.option (Σfe'.Prod (aux_trasfMap_type e fe') (astfe_stm fe')) ≝
+inductive ast_to_astfe_stm_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
+AST_TO_ASTFE_STM_RECORD: ∀m:aux_map_type d.∀fe'.
+ env_to_flatEnv_inv d e m fe' →
+ le_flatEnv fe fe' = true →
+ astfe_stm fe' →
+ ast_to_astfe_stm_record d e fe.
+
+inductive ast_to_astfe_if_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
+AST_TO_ASTFE_IF_RECORD: ∀m:aux_map_type d.∀fe'.
+ env_to_flatEnv_inv d e m fe' →
+ le_flatEnv fe fe' = true →
+ ne_list (Prod (astfe_base_expr fe') (astfe_body fe')) →
+ ast_to_astfe_if_record d e fe.
+
+inductive ast_to_astfe_decl_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
+AST_TO_ASTFE_DECL_RECORD: ∀m:aux_map_type d.∀fe'.∀trsf:list (Prod3T aux_str_type bool ast_type).
+ env_to_flatEnv_inv d (build_trasfEnv_env d trsf e) m fe' →
+ le_flatEnv fe fe' = true →
+ list (astfe_stm fe') →
+ ast_to_astfe_decl_record d e fe.
+
+inductive ast_to_astfe_decl_aux_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
+AST_TO_ASTFE_DECL_AUX_RECORD: ∀m:aux_map_type d.∀fe'.
+ env_to_flatEnv_inv d e m fe' →
+ le_flatEnv fe fe' = true →
+ list (astfe_stm fe') →
+ ast_to_astfe_decl_aux_record d e fe.
+
+let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux_map_type d.Πfe.Πfe'.
+ env_to_flatEnv_inv d e m fe' →
+ le_flatEnv fe fe' = true →
+ ast_to_astfe_stm_record d e fe ≝
match ast
- return λe':aux_env_type.λ_:ast_stm e'.aux_trasfMap_type e' fe → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
+ return λD.λE.λast:ast_stm D E.
+ Πm:aux_map_type D.Πfe.Πfe'.
+ env_to_flatEnv_inv D E m fe' → le_flatEnv fe fe' = true → ast_to_astfe_stm_record D E fe
with
- [ AST_STM_ASG e' subType var expr ⇒
- λmap:aux_trasfMap_type e' fe.
- opt_map ?? (ast_to_astfe_var e' false subType var fe map)
- (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr fe map)
- (λresExpr.Some ? (≪fe,(pair ?? map (ASTFE_STM_ASG fe subType resVar resExpr))≫)))
-
- | AST_STM_WHILE e' expr decl ⇒
- λmap:aux_trasfMap_type e' fe.
- opt_map ?? (ast_to_astfe_base_expr e' expr fe map)
- (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe (retype_e_to_enter e' fe map))
- (λsigmaRes:(Σf.(Σfe'. Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
- [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
- [ sigma_intro fe' mapAndStm ⇒ match mapAndStm with
- [ pair map' resDecl ⇒
- match le_flatEnv fe fe'
- return λx.(le_flatEnv fe fe' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
- with
- [ true ⇒ λp:(le_flatEnv fe fe' = true).
- opt_map ?? (retype_base_expr fe resExpr fe' p)
- (λresExpr'.Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map)
- (ASTFE_STM_WHILE fe' resExpr' (ASTFE_BODY fe' resDecl))≫))
- | false ⇒ λp:(le_flatEnv fe fe' = false).None ?
- ] (refl_eq ? (le_flatEnv fe fe'))
- ]]]))
-
- | AST_STM_IF e' nelExprDecl optDecl ⇒
- λmap:aux_trasfMap_type e' fe.
- let rec aux (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv)
- (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e')))) on nel ≝
- match nel with
- [ ne_nil h ⇒
- opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
- (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
- (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
- [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
- [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
- [ pair m' resDecl ⇒
- match le_flatEnv fenv fenv'
- return λx.(le_flatEnv fenv fenv' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
- with
- [ true ⇒ λp:(le_flatEnv fenv fenv' = true).
- opt_map ?? (retype_base_Expr fenv resExpr fenv' p)
- (λresExpr'.Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m)
- «£(pair ?? resExpr' (ASTFE_BODY fenv' resDecl))»≫))
- | false ⇒ λp:(le_flatEnv fenv fenv' = false).None ?
- ] (refl_eq ? (le_flatEnv fenv fenv'))
- ]]]))
-
- | ne_cons h tl ⇒
- opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
- (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
- (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
- [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
- [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fenv') (list (astfe_stm fenv'))) ⇒ match mapAndStm with
- [ pair m' resDecl ⇒
- opt_map ?? (aux fenv' (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) tl)
- (λsigmaRes':(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes' with
- [ sigma_intro fenv'' mapAndProd ⇒ match mapAndProd with
- [ pair m'' tl' ⇒
- match le_flatEnv fenv fenv''
- return λx.(le_flatEnv fenv fenv'' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
- with
- [ true ⇒ λp:(le_flatEnv fenv fenv'' = true).
- match le_flatEnv fenv' fenv''
- return λy.(le_flatEnv fenv' fenv'' = y) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
- with
- [ true ⇒ λp':(le_flatEnv fenv' fenv'' = true).
- opt_map ?? (retype_base_expr fenv resExpr fenv'' p)
- (λresExpr'.opt_map ?? (retype_stm_list fenv' resDecl fenv'' p')
- (λresDecl'.
- Some ? (≪fenv'',pair ?? m''
- («£(pair ?? resExpr'
- (ASTFE_BODY fenv'' resDecl'))»&tl')≫)))
- | false ⇒ λp':(le_flatEnv fenv' fenv'' = false).None ?
- ] (refl_eq ? (le_flatEnv fenv' fenv''))
- | false ⇒ λp:(le_flatEnv fenv fenv'' = false).None ?
- ] (refl_eq ? (le_flatEnv fenv fenv''))
- ]])]]]))
- ] in
- opt_map ?? (aux fe map nelExprDecl)
- (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes with
- [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) ⇒ match mapAndStm with
- [ pair (m':aux_trasfMap_type e' fe') resNel ⇒ match optDecl with
- [ None ⇒ Some ? (≪fe',pair ?? m' (ASTFE_STM_IF fe' resNel (None ?))≫)
- | Some decl ⇒
- opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe' (retype_e_to_enter e' fe' m'))
- (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with
- [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
- [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with
- [ pair (m'':aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒
- match le_flatEnv fe' fe''
- return λz.(le_flatEnv fe' fe'' = z) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
- with
- [ true ⇒ λp'':(le_flatEnv fe' fe'' = true).
- opt_map ?? (retype_exprAndBody_neList fe' resNel fe'' p'')
- (λresNel'.Some (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
- (≪fe'',pair ?? (rollback_map e' fe' fe'' f (retype_e_to_leave ?? m'') m')
- (ASTFE_STM_IF fe'' resNel' (Some ? (ASTFE_BODY fe'' resDecl)))≫))
- | false ⇒ λp'':(le_flatEnv fe' fe'' = false).None ?
- ] (refl_eq ? (le_flatEnv fe' fe''))
- ]]])]]])
+ [ AST_STM_ASG sD sE sType sVar sExpr ⇒
+ λm:aux_map_type sD.λfe,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true.
+ AST_TO_ASTFE_STM_RECORD sD sE fe m fe' dimInv dimLe
+ (ASTFE_STM_ASG fe' sType (ast_to_astfe_var sD sE false sType sVar m fe' dimInv)
+ (ast_to_astfe_expr sD sE sType sExpr m fe' dimInv))
+
+ | AST_STM_WHILE sD sE sExpr sDecl ⇒
+ λm:aux_map_type sD.λfe,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true.
+ match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD m) fe' fe'
+ (env_map_flatEnv_enter_aux sD sE m fe' dimInv)
+ (eq_to_leflatenv ?? (refl_eq ??)) with
+ [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+ eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+ (λenv.ast_to_astfe_stm_record sD env fe)
+ (AST_TO_ASTFE_STM_RECORD sD
+ (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+ fe
+ (leave_map sD resMap)
+ resFe
+ (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
+ (leflatenv_trans ??? dimLe resDimLe)
+ (ASTFE_STM_WHILE resFe
+ (ast_to_astfe_retype_base_expr fe' (ast_to_astfe_base_expr sD sE sExpr m fe' dimInv)
+ sD
+ (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+ (leave_map sD resMap)
+ resFe
+ (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
+ resDimLe)
+ (ASTFE_BODY resFe resLStm)))
+ sE (leave_add_enter_env sD sE resTrsf) ]
+
+ | AST_STM_IF sD sE sExprDecl sOptDecl ⇒
+ λm:aux_map_type sD.λfe,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true.
+ let rec aux (nel:ne_list (Prod (ast_base_expr sD sE) (ast_decl (S sD) (enter_env sD sE))))
+ (pMap:aux_map_type sD) (pFe,pFe':aux_flatEnv_type)
+ (pDimInv:env_to_flatEnv_inv sD sE pMap pFe')
+ (pDimLe:le_flatEnv pFe pFe' = true) on nel : ast_to_astfe_if_record sD sE pFe ≝
+ match nel with
+ [ ne_nil h ⇒
+ match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe' pFe'
+ (env_map_flatEnv_enter_aux sD sE pMap pFe' pDimInv)
+ (eq_to_leflatenv ?? (refl_eq ??)) with
+ [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+ eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+ (λenv.ast_to_astfe_if_record sD env pFe)
+ (AST_TO_ASTFE_IF_RECORD sD
+ (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+ pFe
+ (leave_map sD resMap)
+ resFe
+ (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
+ (leflatenv_trans ??? pDimLe resDimLe)
+ «£(pair ?? (ast_to_astfe_retype_base_expr pFe' (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe' pDimInv)
+ sD
+ (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+ (leave_map sD resMap)
+ resFe
+ (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
+ resDimLe)
+ (ASTFE_BODY resFe resLStm))»)
+ sE (leave_add_enter_env sD sE resTrsf) ]
+
+ | ne_cons h t ⇒
+ match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe' pFe'
+ (env_map_flatEnv_enter_aux sD sE pMap pFe' pDimInv)
+ (eq_to_leflatenv ?? (refl_eq ??)) with
+ [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+ match aux t (leave_map sD resMap) resFe resFe
+ (eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+ (λenv.env_to_flatEnv_inv sD env (leave_map sD resMap) resFe)
+ (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
+ sE (leave_add_enter_env sD sE resTrsf))
+ (eq_to_leflatenv ?? (refl_eq ??)) with
+ [ AST_TO_ASTFE_IF_RECORD resMap' resFe' resDimInv' resDimLe' resExprBody ⇒
+ AST_TO_ASTFE_IF_RECORD sD sE pFe resMap' resFe' resDimInv'
+ (leflatenv_trans ??? pDimLe (leflatenv_trans ??? resDimLe resDimLe'))
+ («£(pair ?? (ast_to_astfe_retype_base_expr pFe' (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe' pDimInv)
+ sD sE resMap' resFe' resDimInv'
+ (leflatenv_trans ??? resDimLe resDimLe'))
+ (ast_to_astfe_retype_body resFe (ASTFE_BODY resFe resLStm)
+ sD sE resMap' resFe' resDimInv' resDimLe'))»&resExprBody) ]]
+
+ ] in
+ match aux sExprDecl m fe fe' dimInv dimLe with
+ [ AST_TO_ASTFE_IF_RECORD resMap resFe resDimInv resDimLe resExprBody ⇒
+ match sOptDecl with
+ [ None ⇒
+ AST_TO_ASTFE_STM_RECORD sD sE fe resMap resFe resDimInv resDimLe (ASTFE_STM_IF resFe resExprBody (None ?))
+
+ | Some sDecl ⇒
+ match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD resMap) resFe resFe
+ (env_map_flatEnv_enter_aux sD sE resMap resFe resDimInv)
+ (eq_to_leflatenv ?? (refl_eq ??)) with
+ [ AST_TO_ASTFE_DECL_RECORD resMap' resFe' resTrsf resDimInv' resDimLe' resLStm ⇒
+ eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+ (λenv.ast_to_astfe_stm_record sD env fe)
+ (AST_TO_ASTFE_STM_RECORD sD
+ (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+ fe
+ (leave_map sD resMap')
+ resFe'
+ (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv')
+ (leflatenv_trans ??? resDimLe resDimLe')
+ (ASTFE_STM_IF resFe'
+ (ast_to_astfe_retype_exprBody_neList resFe resExprBody
+ sD
+ (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+ (leave_map sD resMap')
+ resFe'
+ (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv')
+ resDimLe')
+ (Some ? (ASTFE_BODY resFe' resLStm))))
+ sE (leave_add_enter_env sD sE resTrsf) ]]]
]
(*
AST_NO_DECL: ∀e:aux_env_type.
AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
(check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e
*)
-and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on ast
- : Πmap:aux_trasfMap_type e fe.option (Σf:aux_trasfEnv_type.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e) fe') (list (astfe_stm fe')))) ≝
+and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe.Πfe'.
+ env_to_flatEnv_inv d e m fe' →
+ le_flatEnv fe fe' = true →
+ ast_to_astfe_decl_record d e fe ≝
match ast
- return λe':aux_env_type.λ_:ast_decl e'.aux_trasfMap_type e' fe → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe'))))
- with
- [ AST_NO_DECL e' lStm ⇒
- λmap:aux_trasfMap_type e' fe.
- let rec aux (ll:list (ast_stm e')) (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) on ll
- : option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ≝
- match ll with
- [ nil ⇒ let trsf ≝ []
- in Some ? ≪trsf,≪fenv,pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fenv)
- (list (astfe_stm fenv))
- (retype_map_to_id e' fenv (build_trasfEnv trsf) m (refl_eq ? e')) []≫≫
-
- | cons h tl ⇒
- opt_map ?? (ast_to_astfe_stm e' h fenv m)
- (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')).match sigmaRes with
- [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
- [ pair m' resStm ⇒
- opt_map ?? (aux tl fenv' m')
- (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))).match sigmaRes' with
- [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
- [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type ((build_trasfEnv f) e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with
- [ pair m'' tl' ⇒
- match le_flatEnv fenv' fenv''
- return λx.(le_flatEnv fenv' fenv'' = x) → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe'))))
- with
- [ true ⇒ λp:(le_flatEnv fenv' fenv'' = true).
- opt_map ?? (retype_stm_list fenv' [resStm] fenv'' p)
- (λresStm'.Some ? ≪f,≪fenv'',pair (aux_trasfMap_type ((build_trasfEnv f) e') fenv'')
- (list (astfe_stm fenv''))
- m''
- (resStm'@tl')≫≫)
- | false ⇒ λp:(le_flatEnv fenv' fenv'' = false).None ?
- ] (refl_eq ? (le_flatEnv fenv' fenv''))
- ]]])]])] in
- aux lStm fe map
-
- | AST_DECL e' b name t dim optInit subDecl ⇒
- λmap:aux_trasfMap_type e' fe.
- opt_map ?? (match optInit with
- [ None ⇒ Some ? []
- | Some init ⇒
- opt_map ?? (ast_to_astfe_init e' t init fe map)
- (λresInit.opt_map ?? (ast_to_astfe_id_check (add_desc_flatEnv fe (next_nameId e' fe map name) b t) ??
- (ASTFE_ID (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
- (next_nameId e' fe map name)
- (ast_to_astfe_dec_aux e' name b t fe map dim))
- b t)
- (λresId.opt_map ?? (retype_init fe t resInit (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
- (adddescflatenv_to_leflatenv fe (next_nameId e' fe map name) b t))
- (λresInit'.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t) b t resId resInit' ]))))
- ])
- (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl
- (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
- (add_maxcur_map e' fe map map name b t))
- (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))).match sigmaRes with
- [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
- [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe'))) ⇒ match mapAndStm with
- [ pair (map':aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') tRes ⇒
- match le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'
- return λx.(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = x) → option (Σf'.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f') e') fe') (list (astfe_stm fe'))))
- with
- [ true ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = true).
- opt_map ?? (retype_stm_list (add_desc_flatEnv fe (next_nameId e' fe map name) b t) hRes fe' p)
- (λhRes'.let trsf ≝ [ tripleT ??? name b t ]@f
- in Some ? ≪trsf,≪fe',pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fe')
- (list (astfe_stm fe'))
- map'
- (hRes'@tRes)≫≫)
- | false ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = false).None ?
- ] (refl_eq ? (le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'))
- ]]]))
- ].
+ return λD.λE.λast:ast_decl D E.
+ Πm:aux_map_type D.Πfe.Πfe'.
+ env_to_flatEnv_inv D E m fe' → le_flatEnv fe fe' = true → ast_to_astfe_decl_record D E fe
+ with
+ [ AST_NO_DECL sD sE sLStm ⇒
+ λm:aux_map_type sD.λfe,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true.
+ let rec aux (l:list (ast_stm sD sE)) (pMap:aux_map_type sD) (pFe,pFe':aux_flatEnv_type)
+ (pDimInv:env_to_flatEnv_inv sD sE pMap pFe')
+ (pDimLe:le_flatEnv pFe pFe' = true) on l : ast_to_astfe_decl_aux_record sD sE pFe ≝
+ match l with
+ [ nil ⇒
+ AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe pMap pFe' pDimInv pDimLe []
+
+ | cons h t ⇒
+ match ast_to_astfe_stm sD sE h pMap pFe' pFe' pDimInv (eq_to_leflatenv ?? (refl_eq ??)) with
+ [ AST_TO_ASTFE_STM_RECORD resMap resFe resDimInv resDimLe resStm ⇒
+ match aux t resMap resFe resFe resDimInv (eq_to_leflatenv ?? (refl_eq ??)) with
+ [ AST_TO_ASTFE_DECL_AUX_RECORD resMap' resFe' resDimInv' resDimLe' resLStm ⇒
+ AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe resMap' resFe' resDimInv'
+ (leflatenv_trans ??? pDimLe (leflatenv_trans ??? resDimLe resDimLe'))
+ ([ ast_to_astfe_retype_stm resFe resStm sD sE resMap' resFe' resDimInv' resDimLe' ]@resLStm) ]]
+
+ ] in
+ match aux sLStm m fe fe' dimInv dimLe with
+ [ AST_TO_ASTFE_DECL_AUX_RECORD resMap resFe resDimInv resDimLe resLStm ⇒
+ AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe []
+ (env_map_flatEnv_addNil_aux sD sE resMap resFe resDimInv)
+ resDimLe resLStm ]
+
+ | AST_DECL sD sE sB sName sType sDim sOptInit sDecl ⇒
+ λm:aux_map_type sD.λfe,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true.
+ 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')))
+ (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)
+ (eq_to_leflatenv ?? (refl_eq ??)) 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 ??? dimLe (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe' [ tripleT ??? sName sB sType ]) resDimLe))
+ (match sOptInit with
+ [ None ⇒ []
+ | Some init ⇒
+ [ ASTFE_STM_INIT resFe sB 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)
+ resMap resFe
+ (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB 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)
+ 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))
+ ]]@resLStm) ]
+
+ ].
(*
AST_ROOT: ast_decl empty_env → ast_root.
*)
definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
λast:ast_root.match ast with
- [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_flatEnv (empty_trasfMap empty_env empty_flatEnv) with
- (* impossibile: dummy *)
- [ None ⇒ ≪empty_flatEnv,empty_astfe_prog≫
- | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with
- [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
- [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe) (list (astfe_stm fe))) ⇒ match mapAndStm with
- [ pair map resStm ⇒ ≪fe,(ASTFE_ROOT fe (ASTFE_BODY fe resStm))≫
- ]]]]].
-
-(* mini test
-include "compiler/preast_tree.ma".
-include "compiler/preast_to_ast.ma".
-
-{ const byte8 a;
- const byte8[3] b={0,1,2};
- byte8[3] c=b;
-
- if(0xF0)
- { byte8 a=a; }
- else if(0xF1)
- {
- while(0x10)
- { byte8[3] b=c; }
- }
- else if(0xF2)
- { byte8 a=b[0]; }
- else
- { const byte8 a=a; }
-}
-
-definition prova ≝
-PREAST_ROOT (
- PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) (
- PREAST_DECL true [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAL (PREAST_INIT_VAL_ARRAY «(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x2〉)»))) (
- PREAST_DECL false [ch_C] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_B]))) (
- PREAST_NO_DECL [
- PREAST_STM_IF «
- (pair ??
- (PREAST_EXPR_BYTE8 〈xF,x0〉)
- (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL []))
- )
- ; (pair ??
- (PREAST_EXPR_BYTE8 〈xF,x1〉)
- (PREAST_NO_DECL [
- (PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x1,x0〉) (
- PREAST_DECL false [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_C]))) (PREAST_NO_DECL [])
- ))
- ])
- )
- £ (pair ??
- (PREAST_EXPR_BYTE8 〈xF,x2〉)
- (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ARRAY (PREAST_VAR_ID [ch_B]) (PREAST_EXPR_BYTE8 〈x0,x0〉)))) (PREAST_NO_DECL []))
- )
- » (Some ? (PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL [])))
- ]
- )
- )
- )
-).
-*)
+ [ AST_ROOT decl ⇒ match ast_to_astfe_decl O empty_env decl empty_map empty_flatEnv empty_flatEnv env_map_flatEnv_empty_aux (eq_to_leflatenv ?? (refl_eq ??)) with
+ [ AST_TO_ASTFE_DECL_RECORD _ resFe _ _ _ resLStm ⇒ ≪resFe,ASTFE_ROOT resFe (ASTFE_BODY resFe resLStm)≫ ]].
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* *)
-(* Sviluppato da: *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* *)
-(* ********************************************************************** *)
-
-include "compiler/astfe_tree1.ma".
-
-(* ************************ *)
-(* PASSO 2 : da AST a ASTFE *)
-(* ************************ *)
-
-(*
- AST_ID: ∀str:aux_str_type.
- (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str)))
-*)
-lemma ast_to_astfe_id :
- ∀e,b,t.∀ast:ast_id e b t.
- ∀d.∀m:aux_map_type d.∀fe.
- ∀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 Hletin
- ].
-qed.
-
-lemma ast_to_astfe_retype_id :
- ∀fe,b,t.∀ast:astfe_id fe b t.
- ∀d.∀e.∀m:aux_map_type d.∀fe'.
- ∀dimInv:env_to_flatEnv_inv d e m fe'.
- ∀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 ?);
- [ apply (leflatenv_to_check fe fe' a1 H2 H)
- | rewrite > (leflatenv_to_get fe fe' a1 H2 H);
- apply Hletin
- ].
-qed.
-
-(*
- 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 (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
- AST_EXPR_NOT: ∀t:ast_base_type.
- ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
- AST_EXPR_COM: ∀t:ast_base_type.
- ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
-
- AST_EXPR_ADD: ∀t:ast_base_type.
- 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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_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_type.
- ast_var e b t → ast_expr e t
-*)
-let rec ast_to_astfe_expr e t (ast:ast_expr e t)
- d (m:aux_map_type d) fe
- (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_expr fe t ≝
- match ast
- return λW.λa:ast_expr e W.astfe_expr fe W
- with
- [ AST_EXPR_BYTE8 val ⇒
- ASTFE_EXPR_BYTE8 fe val
- | AST_EXPR_WORD16 val ⇒
- ASTFE_EXPR_WORD16 fe val
- | AST_EXPR_WORD32 val ⇒
- ASTFE_EXPR_WORD32 fe val
-
- | AST_EXPR_NEG bType sExpr ⇒
- ASTFE_EXPR_NEG fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv)
- | AST_EXPR_NOT bType sExpr ⇒
- ASTFE_EXPR_NOT fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv)
- | AST_EXPR_COM bType sExpr ⇒
- ASTFE_EXPR_COM fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv)
-
- | AST_EXPR_ADD bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_ADD fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
- | AST_EXPR_SUB bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_SUB fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
- | AST_EXPR_MUL bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_MUL fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
- | AST_EXPR_DIV bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_DIV fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
- | AST_EXPR_SHR bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_SHR fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
- (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe dimInv)
- | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_SHL fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
- (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe dimInv)
-
- | AST_EXPR_GT bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_GT fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
- | AST_EXPR_GTE bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_GTE fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
- | AST_EXPR_LT bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_LT fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
- | AST_EXPR_LTE bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_LTE fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
- | AST_EXPR_EQ bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_EQ fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
- | AST_EXPR_NEQ bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_NEQ fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
-
- | AST_EXPR_B8toW16 sExpr ⇒
- ASTFE_EXPR_B8toW16 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe dimInv)
- | AST_EXPR_B8toW32 sExpr ⇒
- ASTFE_EXPR_B8toW32 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe dimInv)
- | AST_EXPR_W16toB8 sExpr ⇒
- ASTFE_EXPR_W16toB8 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe dimInv)
- | AST_EXPR_W16toW32 sExpr ⇒
- ASTFE_EXPR_W16toW32 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe dimInv)
- | AST_EXPR_W32toB8 sExpr ⇒
- ASTFE_EXPR_W32toB8 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe dimInv)
- | AST_EXPR_W32toW16 sExpr ⇒
- ASTFE_EXPR_W32toW16 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe dimInv)
-
- | AST_EXPR_ID b sType var ⇒
- ASTFE_EXPR_ID fe b sType (ast_to_astfe_var e b sType var d m fe dimInv)
-
- ]
-(*
- AST_VAR_ID: ∀b:bool.∀t:ast_type.
- ast_id e b t → ast_var e b t
- 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) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
-*)
-and ast_to_astfe_var e b t (ast:ast_var e b t)
- d (m:aux_map_type d) fe
- (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_var fe b t ≝
- match ast
- return λW,X.λa:ast_var e W X.astfe_var fe W X
- with
- [ AST_VAR_ID sB sType sId ⇒
- ASTFE_VAR_ID fe sB sType (ast_to_astfe_id e sB sType sId d m fe dimInv)
-
- | AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒
- ASTFE_VAR_ARRAY fe sB sType sDim (ast_to_astfe_var e sB (AST_TYPE_ARRAY sType sDim) sVar d m fe dimInv)
- (ast_to_astfe_base_expr e sExpr d m fe dimInv)
-
- | AST_VAR_STRUCT sB sType sField sVar sLtb ⇒
- ASTFE_VAR_STRUCT fe sB sType sField (ast_to_astfe_var e sB (AST_TYPE_STRUCT sType) sVar d m fe dimInv)
- ]
-(*
- AST_BASE_EXPR: ∀t:ast_base_type.
- ast_expr e (AST_TYPE_BASE t) → ast_base_expr e
-*)
-and ast_to_astfe_base_expr e (ast:ast_base_expr e)
- d (m:aux_map_type d) fe
- (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_base_expr fe ≝
- match ast
- return λa:ast_base_expr e.astfe_base_expr fe
- with
- [ AST_BASE_EXPR bType sExpr ⇒
- ASTFE_BASE_EXPR fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv)
- ].
-
-let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
- d e (m:aux_map_type d) fe'
- (dimInv:env_to_flatEnv_inv d e m fe')
- (dimLe:le_flatEnv fe fe' = true) on ast : astfe_expr fe' t ≝
- match ast
- return λW.λa:astfe_expr fe W.astfe_expr fe' W
- with
- [ ASTFE_EXPR_BYTE8 val ⇒
- ASTFE_EXPR_BYTE8 fe' val
- | ASTFE_EXPR_WORD16 val ⇒
- ASTFE_EXPR_WORD16 fe' val
- | ASTFE_EXPR_WORD32 val ⇒
- ASTFE_EXPR_WORD32 fe' val
-
- | ASTFE_EXPR_NEG bType sExpr ⇒
- ASTFE_EXPR_NEG fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
- | ASTFE_EXPR_NOT bType sExpr ⇒
- ASTFE_EXPR_NOT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
- | ASTFE_EXPR_COM bType sExpr ⇒
- ASTFE_EXPR_COM fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
-
- | ASTFE_EXPR_ADD bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_ADD 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_SUB bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_SUB 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_MUL bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_MUL 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_DIV bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_DIV 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_SHR bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_SHR 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_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_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_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
- | ASTFE_EXPR_GTE bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_GTE 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_LT bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_LT 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_LTE bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_LTE 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_EQ bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_EQ 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_NEQ bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_NEQ 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_B8toW16 sExpr ⇒
- ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
- | ASTFE_EXPR_B8toW32 sExpr ⇒
- ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
- | ASTFE_EXPR_W16toB8 sExpr ⇒
- ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
- | ASTFE_EXPR_W16toW32 sExpr ⇒
- ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
- | ASTFE_EXPR_W32toB8 sExpr ⇒
- ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
- | ASTFE_EXPR_W32toW16 sExpr ⇒
- ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
-
- | ASTFE_EXPR_ID b sType var ⇒
- ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe)
-
- ]
-and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t)
- d e (m:aux_map_type d) fe'
- (dimInv:env_to_flatEnv_inv d e m fe')
- (dimLe:le_flatEnv fe fe' = true) on ast : astfe_var fe' b t ≝
- match ast
- return λW,X.λa:astfe_var fe W X.astfe_var fe' W X
- with
- [ ASTFE_VAR_ID sB sType sId ⇒
- ASTFE_VAR_ID fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
-
- | ASTFE_VAR_ARRAY sB sType sDim sVar sExpr ⇒
- ASTFE_VAR_ARRAY fe' sB sType sDim (ast_to_astfe_retype_var fe sB (AST_TYPE_ARRAY sType sDim) sVar d e m fe' dimInv dimLe)
- (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
-
- | ASTFE_VAR_STRUCT sB sType sField sVar ⇒
- ASTFE_VAR_STRUCT fe' sB sType sField (ast_to_astfe_retype_var fe sB (AST_TYPE_STRUCT sType) sVar d e m fe' dimInv dimLe)
- ]
-and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe)
- d e (m:aux_map_type d) fe'
- (dimInv:env_to_flatEnv_inv d e m fe')
- (dimLe:le_flatEnv fe fe' = true) on ast : astfe_base_expr fe' ≝
- match ast
- return λa:astfe_base_expr fe.astfe_base_expr fe'
- with
- [ ASTFE_BASE_EXPR bType sExpr ⇒
- ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
- ].
-
-(*
- 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
-*)
-definition ast_to_astfe_init ≝
-λe,t.λast:ast_init e t.
-λd.λm:aux_map_type d.λfe.
-λdimInv:env_to_flatEnv_inv d e m fe.
- match ast
- return λW.λa:ast_init e W.astfe_init fe W
- with
- [ AST_INIT_VAR sB sType sVar ⇒
- ASTFE_INIT_VAR fe sB sType (ast_to_astfe_var e sB sType sVar d m fe dimInv)
-
- | AST_INIT_VAL sType sArgs ⇒
- ASTFE_INIT_VAL fe sType sArgs
-
- ].
-
-definition ast_to_astfe_retype_init ≝
-λfe,t.λast:astfe_init fe t.
-λd.λe.λm:aux_map_type d.λfe'.
-λdimInv:env_to_flatEnv_inv d e m fe'.
-λdimLe:le_flatEnv fe fe' = true.
- match ast
- return λW.λa:astfe_init fe W.astfe_init fe' W
- with
- [ ASTFE_INIT_VAR sB sType sVar ⇒
- ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe)
-
- | ASTFE_INIT_VAL sType sArgs ⇒
- ASTFE_INIT_VAL fe' sType sArgs
-
- ].
-
-(*
- ASTFE_STM_ASG: ∀t:ast_type.
- astfe_var e false t → astfe_expr e t → astfe_stm e
- ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
- 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
-*)
-let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe) d e m fe' dimInv dimLe on ast : astfe_stm fe' ≝
- match ast with
- [ ASTFE_STM_ASG sType sVar sExpr ⇒
- ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe)
- (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe)
-
- | ASTFE_STM_INIT sB sType sId sInit ⇒
- ASTFE_STM_INIT fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
- (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe)
-
- | ASTFE_STM_WHILE sExpr sBody ⇒
- ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
- (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)
-
- | ASTFE_STM_IF sNelExprBody sOptBody ⇒
- ASTFE_STM_IF fe' (cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe)
- (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
- )»&t)
- «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
- sNelExprBody))
- (opt_map ?? sOptBody
- (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)))
- ]
-(*
- ASTFE_BODY: list (astfe_stm e) → astfe_body e
-*)
-and ast_to_astfe_retype_body fe (ast:astfe_body fe) d e m fe' dimInv dimLe on ast : astfe_body fe' ≝
- match ast with
- [ ASTFE_BODY sLStm ⇒
- ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] sLStm)
- ].
-
-definition ast_to_astfe_retype_stm_list ≝
-λfe.λast:list (astfe_stm fe).λd,e,m,fe',dimInv,dimLe.
- fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] ast.
-
-definition ast_to_astfe_retype_exprBody_neList ≝
-λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).λd,e,m,fe',dimInv,dimLe.
- cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe)
- (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
- )»&t)
- «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
- ast).
-
-(*
- AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
- 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 (enter_env e) → ast_stm e
- AST_STM_IF: ∀e:aux_env_type.
- ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
-*)
-inductive ast_to_astfe_stm_record (d:nat) (e:aux_env_type) (fe:aux_flatEnv_type) : Type ≝
-AST_TO_ASTFE_STM_RECORD: ∀m:aux_map_type d.∀fe'.
- env_to_flatEnv_inv d e m fe' →
- le_flatEnv fe fe' = true →
- astfe_stm fe' →
- ast_to_astfe_stm_record d e fe.
-
-inductive ast_to_astfe_if_record (d:nat) (e:aux_env_type) (fe:aux_flatEnv_type) : Type ≝
-AST_TO_ASTFE_IF_RECORD: ∀m:aux_map_type d.∀fe'.
- env_to_flatEnv_inv d e m fe' →
- le_flatEnv fe fe' = true →
- ne_list (Prod (astfe_base_expr fe') (astfe_body fe')) →
- ast_to_astfe_if_record d e fe.
-
-inductive ast_to_astfe_decl_record (d:nat) (e:aux_env_type) (m:aux_map_type d) (fe:aux_flatEnv_type) : Type ≝
-AST_TO_ASTFE_DECL_RECORD: ∀trsf:list (Prod3T aux_str_type bool ast_type).
- env_to_flatEnv_inv d
- (build_trasfEnv_env trsf e)
- (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe)))
- (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) →
- le_flatEnv fe (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) = true →
- list (astfe_stm (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe)))) →
- ast_to_astfe_decl_record d e m fe.
-
-let rec ast_to_astfe_stm e (ast:ast_stm e) on ast : Πd.Πm:aux_map_type d.Πfe.Πfe'.
- env_to_flatEnv_inv d e m fe' →
- le_flatEnv fe fe' = true →
- ast_to_astfe_stm_record d e fe ≝
- match ast
- return λX.λast:ast_stm X.
- Πd.Πm:aux_map_type d.Πfe.Πfe'.
- env_to_flatEnv_inv d X m fe' → le_flatEnv fe fe' = true → ast_to_astfe_stm_record d X fe
- with
- [ AST_STM_ASG sE sType sVar sExpr ⇒
- λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true.
- AST_TO_ASTFE_STM_RECORD d sE fe m fe' dimInv dimLe
- (ASTFE_STM_ASG fe' sType (ast_to_astfe_var sE false sType sVar d m fe' dimInv)
- (ast_to_astfe_expr sE sType sExpr d m fe' dimInv))
-
- | AST_STM_WHILE sE sExpr sDecl ⇒
- λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true.
- (* in sostanza
- 1) eseguo decl su ENTER dell'invariante
- 2) decl restituisce ADD+ENTER dell'invariante
- 3) eseguo base_expr sull'invariante
- 4) retipo base_expr su LEAVE+ADD+ENTER dell'invariante
- 5) retituisco su LEAVE+ADD+ENTER dell'invariante *)
- match ast_to_astfe_decl (enter_env sE) sDecl (S d) (enter_map d m) fe fe' (env_map_flatEnv_enter_aux d sE m fe' dimInv) dimLe with
- [ AST_TO_ASTFE_DECL_RECORD resTrsf resDimInv resDimLe resLStm ⇒
- AST_TO_ASTFE_STM_RECORD d sE fe
- (* m'' *)
- (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))))
- (* fe'' *)
- (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe')))
- (* leave_add_enter(dimInv) *)
- (env_map_flatEnv_leave_aux d sE m fe' resTrsf resDimInv)
- (* fe ≤ fe' ∧ fe' ≤ fe'' → fe ≤ fe'' *)
- (leflatenv_trans ??? dimLe resDimLe)
- (* risultato su fe'' *)
- (ASTFE_STM_WHILE (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe')))
- (ast_to_astfe_retype_base_expr fe' (ast_to_astfe_base_expr sE sExpr d m fe' dimInv)
- d sE
- (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))))
- (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe')))
- (env_map_flatEnv_leave_aux d sE m fe' resTrsf resDimInv)
- resDimLe)
- (ASTFE_BODY (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))) resLStm)) ]
-
- | AST_STM_IF sE sExprDecl sOptDecl ⇒
- λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true.
- let rec aux (nel:ne_list (Prod (ast_base_expr sE) (ast_decl (enter_env sE))))
- (pMap:aux_map_type d) (pFe,pFe':aux_flatEnv_type)
- (pDimInv:env_to_flatEnv_inv d sE pMap pFe')
- (pDimLe:le_flatEnv pFe pFe' = true) on nel : ast_to_astfe_if_record d sE pFe ≝
- match nel with
- [ ne_nil h ⇒
- match ast_to_astfe_decl (enter_env sE) (snd ?? h) (S d) (enter_map d pMap) pFe pFe' (env_map_flatEnv_enter_aux d sE pMap pFe' pDimInv) pDimLe with
- [ AST_TO_ASTFE_DECL_RECORD resTrsf resDimInv resDimLe resLStm ⇒
- AST_TO_ASTFE_IF_RECORD d sE pFe
- (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))))
- (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe')))
- (env_map_flatEnv_leave_aux d sE pMap pFe' resTrsf resDimInv)
- (leflatenv_trans ??? pDimLe resDimLe)
- «£(pair ?? (ast_to_astfe_retype_base_expr pFe' (ast_to_astfe_base_expr sE (fst ?? h) d pMap pFe' pDimInv)
- d sE
- (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))))
- (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe')))
- (env_map_flatEnv_leave_aux d sE pMap pFe' resTrsf resDimInv)
- resDimLe)
- (ASTFE_BODY (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))) resLStm))» ]
-
- | ne_cons h t ⇒ (False_rect ? daemon)
- (*match ast_to_astfe_decl (enter_env sE) (snd ?? h) (S d) (enter_map d pMap) pFe pFe' (env_map_flatEnv_enter_aux d sE pMap pFe' pDimInv) pDimLe with
- [ AST_TO_ASTFE_DECL_RECORD resTrsf resDimInv resDimLe resLStm ⇒
- match aux t (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))))
- pFe (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe')))
- (env_map_flatEnv_leave_aux d sE pMap pFe' resTrsf resDimInv)
- (leflatenv_trans ??? pDimLe resDimLe) with
- [ AST_TO_ASTFE_IF_RECORD iMap iFe' iDimInv iDimLe iNelExprDecl ⇒
- AST_TO_ASTFE_IF_RECORD d sE pFe iMap iFe' iDimInv iDimLe
- (False_rect ? daemon) ]]*)
-
-
- ] in (False_rect ? daemon)
-
- ]
-and ast_to_astfe_decl e (ast:ast_decl e) on ast : Πd.Πm:aux_map_type d.Πfe.Πfe'.
- env_to_flatEnv_inv d e m fe' →
- le_flatEnv fe fe' = true →
- ast_to_astfe_decl_record d e m fe' ≝
- match ast
- return λX.λast:ast_decl X.
- Πd.Πm:aux_map_type d.Πfe.Πfe'.
- env_to_flatEnv_inv d X m fe' → le_flatEnv fe fe' = true → ast_to_astfe_decl_record d X m fe'
- with
- [ AST_NO_DECL sE sLStm ⇒
- λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true.
- False_rect ? daemon
-
- | _ ⇒ False_rect ? daemon
-
- ].
-
-FINQUI
-
- | AST_STM_IF e' nelExprDecl optDecl ⇒
- λmap:aux_trasfMap_type e' fe.
- let rec aux (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv)
- (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e')))) on nel ≝
- match nel with
- [ ne_nil h ⇒
- opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
- (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
- (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
- [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
- [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
- [ pair m' resDecl ⇒
- match le_flatEnv fenv fenv'
- return λx.(le_flatEnv fenv fenv' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
- with
- [ true ⇒ λp:(le_flatEnv fenv fenv' = true).
- opt_map ?? (retype_base_Expr fenv resExpr fenv' p)
- (λresExpr'.Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m)
- «£(pair ?? resExpr' (ASTFE_BODY fenv' resDecl))»≫))
- | false ⇒ λp:(le_flatEnv fenv fenv' = false).None ?
- ] (refl_eq ? (le_flatEnv fenv fenv'))
- ]]]))
-
- | ne_cons h tl ⇒
- opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
- (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
- (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
- [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
- [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fenv') (list (astfe_stm fenv'))) ⇒ match mapAndStm with
- [ pair m' resDecl ⇒
- opt_map ?? (aux fenv' (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) tl)
- (λsigmaRes':(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes' with
- [ sigma_intro fenv'' mapAndProd ⇒ match mapAndProd with
- [ pair m'' tl' ⇒
- match le_flatEnv fenv fenv''
- return λx.(le_flatEnv fenv fenv'' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
- with
- [ true ⇒ λp:(le_flatEnv fenv fenv'' = true).
- match le_flatEnv fenv' fenv''
- return λy.(le_flatEnv fenv' fenv'' = y) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
- with
- [ true ⇒ λp':(le_flatEnv fenv' fenv'' = true).
- opt_map ?? (retype_base_expr fenv resExpr fenv'' p)
- (λresExpr'.opt_map ?? (retype_stm_list fenv' resDecl fenv'' p')
- (λresDecl'.
- Some ? (≪fenv'',pair ?? m''
- («£(pair ?? resExpr'
- (ASTFE_BODY fenv'' resDecl'))»&tl')≫)))
- | false ⇒ λp':(le_flatEnv fenv' fenv'' = false).None ?
- ] (refl_eq ? (le_flatEnv fenv' fenv''))
- | false ⇒ λp:(le_flatEnv fenv fenv'' = false).None ?
- ] (refl_eq ? (le_flatEnv fenv fenv''))
- ]])]]]))
- ] in
- opt_map ?? (aux fe map nelExprDecl)
- (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes with
- [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) ⇒ match mapAndStm with
- [ pair (m':aux_trasfMap_type e' fe') resNel ⇒ match optDecl with
- [ None ⇒ Some ? (≪fe',pair ?? m' (ASTFE_STM_IF fe' resNel (None ?))≫)
- | Some decl ⇒
- opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe' (retype_e_to_enter e' fe' m'))
- (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with
- [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
- [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with
- [ pair (m'':aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒
- match le_flatEnv fe' fe''
- return λz.(le_flatEnv fe' fe'' = z) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
- with
- [ true ⇒ λp'':(le_flatEnv fe' fe'' = true).
- opt_map ?? (retype_exprAndBody_neList fe' resNel fe'' p'')
- (λresNel'.Some (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
- (≪fe'',pair ?? (rollback_map e' fe' fe'' f (retype_e_to_leave ?? m'') m')
- (ASTFE_STM_IF fe'' resNel' (Some ? (ASTFE_BODY fe'' resDecl)))≫))
- | false ⇒ λp'':(le_flatEnv fe' fe'' = false).None ?
- ] (refl_eq ? (le_flatEnv fe' fe''))
- ]]])]]])
- ]
-(*
- AST_NO_DECL: ∀e:aux_env_type.
- list (ast_stm e) → ast_decl e
- AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
- (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e
-*)
-and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on ast
- : Πmap:aux_trasfMap_type e fe.option (Σf:aux_trasfEnv_type.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e) fe') (list (astfe_stm fe')))) ≝
- match ast
- return λe':aux_env_type.λ_:ast_decl e'.aux_trasfMap_type e' fe → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe'))))
- with
- [ AST_NO_DECL e' lStm ⇒
- λmap:aux_trasfMap_type e' fe.
- let rec aux (ll:list (ast_stm e')) (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) on ll
- : option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ≝
- match ll with
- [ nil ⇒ let trsf ≝ []
- in Some ? ≪trsf,≪fenv,pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fenv)
- (list (astfe_stm fenv))
- (retype_map_to_id e' fenv (build_trasfEnv trsf) m (refl_eq ? e')) []≫≫
-
- | cons h tl ⇒
- opt_map ?? (ast_to_astfe_stm e' h fenv m)
- (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')).match sigmaRes with
- [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
- [ pair m' resStm ⇒
- opt_map ?? (aux tl fenv' m')
- (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))).match sigmaRes' with
- [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
- [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type ((build_trasfEnv f) e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with
- [ pair m'' tl' ⇒
- match le_flatEnv fenv' fenv''
- return λx.(le_flatEnv fenv' fenv'' = x) → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe'))))
- with
- [ true ⇒ λp:(le_flatEnv fenv' fenv'' = true).
- opt_map ?? (retype_stm_list fenv' [resStm] fenv'' p)
- (λresStm'.Some ? ≪f,≪fenv'',pair (aux_trasfMap_type ((build_trasfEnv f) e') fenv'')
- (list (astfe_stm fenv''))
- m''
- (resStm'@tl')≫≫)
- | false ⇒ λp:(le_flatEnv fenv' fenv'' = false).None ?
- ] (refl_eq ? (le_flatEnv fenv' fenv''))
- ]]])]])] in
- aux lStm fe map
-
- | AST_DECL e' b name t dim optInit subDecl ⇒
- λmap:aux_trasfMap_type e' fe.
- opt_map ?? (match optInit with
- [ None ⇒ Some ? []
- | Some init ⇒
- opt_map ?? (ast_to_astfe_init e' t init fe map)
- (λresInit.opt_map ?? (ast_to_astfe_id_check (add_desc_flatEnv fe (next_nameId e' fe map name) b t) ??
- (ASTFE_ID (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
- (next_nameId e' fe map name)
- (ast_to_astfe_dec_aux e' name b t fe map dim))
- b t)
- (λresId.opt_map ?? (retype_init fe t resInit (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
- (adddescflatenv_to_leflatenv fe (next_nameId e' fe map name) b t))
- (λresInit'.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t) b t resId resInit' ]))))
- ])
- (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl
- (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
- (add_maxcur_map e' fe map map name b t))
- (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))).match sigmaRes with
- [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
- [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe'))) ⇒ match mapAndStm with
- [ pair (map':aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') tRes ⇒
- match le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'
- return λx.(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = x) → option (Σf'.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f') e') fe') (list (astfe_stm fe'))))
- with
- [ true ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = true).
- opt_map ?? (retype_stm_list (add_desc_flatEnv fe (next_nameId e' fe map name) b t) hRes fe' p)
- (λhRes'.let trsf ≝ [ tripleT ??? name b t ]@f
- in Some ? ≪trsf,≪fe',pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fe')
- (list (astfe_stm fe'))
- map'
- (hRes'@tRes)≫≫)
- | false ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = false).None ?
- ] (refl_eq ? (le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'))
- ]]]))
- ].
-
-(*
- AST_ROOT: ast_decl empty_env → ast_root.
-*)
-definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
-λast:ast_root.match ast with
- [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_flatEnv (empty_trasfMap empty_env empty_flatEnv) with
- (* impossibile: dummy *)
- [ None ⇒ ≪empty_flatEnv,empty_astfe_prog≫
- | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with
- [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
- [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe) (list (astfe_stm fe))) ⇒ match mapAndStm with
- [ pair map resStm ⇒ ≪fe,(ASTFE_ROOT fe (ASTFE_BODY fe resStm))≫
- ]]]]].
-
-(* mini test
-include "compiler/preast_tree.ma".
-include "compiler/preast_to_ast.ma".
-
-{ const byte8 a;
- const byte8[3] b={0,1,2};
- byte8[3] c=b;
-
- if(0xF0)
- { byte8 a=a; }
- else if(0xF1)
- {
- while(0x10)
- { byte8[3] b=c; }
- }
- else if(0xF2)
- { byte8 a=b[0]; }
- else
- { const byte8 a=a; }
-}
-
-definition prova ≝
-PREAST_ROOT (
- PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) (
- PREAST_DECL true [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAL (PREAST_INIT_VAL_ARRAY «(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x2〉)»))) (
- PREAST_DECL false [ch_C] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_B]))) (
- PREAST_NO_DECL [
- PREAST_STM_IF «
- (pair ??
- (PREAST_EXPR_BYTE8 〈xF,x0〉)
- (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL []))
- )
- ; (pair ??
- (PREAST_EXPR_BYTE8 〈xF,x1〉)
- (PREAST_NO_DECL [
- (PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x1,x0〉) (
- PREAST_DECL false [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_C]))) (PREAST_NO_DECL [])
- ))
- ])
- )
- £ (pair ??
- (PREAST_EXPR_BYTE8 〈xF,x2〉)
- (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ARRAY (PREAST_VAR_ID [ch_B]) (PREAST_EXPR_BYTE8 〈x0,x0〉)))) (PREAST_NO_DECL []))
- )
- » (Some ? (PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL [])))
- ]
- )
- )
- )
-).
-*)
(* *************** *)
(* id: accesso all'ambiente con stringa *)
-inductive ast_id (e:aux_env_type) : bool → ast_type → Type ≝
+inductive ast_id (d:nat) (e:aux_env_type d) : bool → ast_type → Type ≝
AST_ID: ∀str:aux_str_type.
- (* D *) (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str))).
+ (* D *) (check_desc_env d e str) → (ast_id d e (get_const_desc (get_desc_env d e str)) (get_type_desc (get_desc_env d e str))).
(* -------------------------- *)
(* espressioni *)
-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)
+inductive ast_expr (d:nat) (e:aux_env_type d) : ast_type → Type ≝
+ AST_EXPR_BYTE8 : byte8 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_WORD16: word16 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| AST_EXPR_WORD32: word32 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
| AST_EXPR_NEG: ∀t:ast_base_type.
- ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
| AST_EXPR_NOT: ∀t:ast_base_type.
- ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
| AST_EXPR_COM: ∀t:ast_base_type.
- ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
| AST_EXPR_ADD: ∀t:ast_base_type.
- ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ 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_SUB: ∀t:ast_base_type.
- ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ 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_MUL: ∀t:ast_base_type.
- ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ 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_DIV: ∀t:ast_base_type.
- ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ 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_SHR: ∀t:ast_base_type.
- 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 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr 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 d e (AST_TYPE_BASE t)
| AST_EXPR_GT : ∀t:ast_base_type.
- 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 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_GTE: ∀t:ast_base_type.
- 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 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_LT : ∀t:ast_base_type.
- 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 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_LTE: ∀t:ast_base_type.
- 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 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_EQ : ∀t:ast_base_type.
- 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 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_NEQ: ∀t:ast_base_type.
- 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 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_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_B8toW16 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| AST_EXPR_B8toW32 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| AST_EXPR_W16toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_W16toW32: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| AST_EXPR_W32toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_W32toW16: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
| AST_EXPR_ID: ∀b:bool.∀t:ast_type.
- ast_var e b t → ast_expr e t
+ ast_var d e b t → ast_expr d e t
(* 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
+ ast_id d e b t → ast_var d e b t
| 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 d e b (AST_TYPE_ARRAY t n) → ast_base_expr d e → ast_var d 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 d e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var d 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 (AST_TYPE_BASE t) → ast_base_expr e.
+ ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d e.
(* -------------------------- *)
1) var1 = var2
2) var = ... valori ...
*)
-inductive ast_init (e:aux_env_type) : ast_type → Type ≝
+inductive ast_init (d:nat) (e:aux_env_type d) : ast_type → Type ≝
AST_INIT_VAR: ∀b:bool.∀t:ast_type.
- ast_var e b t → ast_init e t
+ ast_var d e b t → ast_init d e t
| AST_INIT_VAL: ∀t:ast_type.
- aux_ast_init_type t → ast_init e t.
+ aux_ast_init_type t → ast_init d 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_type.
- 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 (enter_env e) → ast_stm e
-| AST_STM_IF: ∀e:aux_env_type.
- ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
+inductive ast_stm : Πd:nat.aux_env_type d → Type ≝
+ AST_STM_ASG: ∀d.∀e:aux_env_type d.∀t:ast_type.
+ ast_var d e false t → ast_expr d e t → ast_stm d e
+| AST_STM_WHILE: ∀d.∀e:aux_env_type d.
+ ast_base_expr d e → ast_decl (S d) (enter_env d e) → ast_stm d e
+| AST_STM_IF: ∀d.∀e:aux_env_type d.
+ ne_list (Prod (ast_base_expr d e) (ast_decl (S d) (enter_env d e))) → option (ast_decl (S d) (enter_env d e)) → ast_stm d e
(* dichiarazioni *)
-with ast_decl : aux_env_type → Type ≝
- AST_NO_DECL: ∀e:aux_env_type.
- list (ast_stm e) → 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) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e.
+with ast_decl : Πd:nat.aux_env_type d → Type ≝
+ 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.
+ (* D *) (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.
(* -------------------------- *)
(* programma *)
inductive ast_root : Type ≝
- AST_ROOT: ast_decl empty_env → ast_root.
+ AST_ROOT: ast_decl O empty_env → ast_root.
(* -------------------------- *)
(* programma vuoto *)
-definition empty_ast_prog ≝ AST_ROOT (AST_NO_DECL empty_env (nil ?)).
+definition empty_ast_prog ≝ AST_ROOT (AST_NO_DECL O empty_env (nil ?)).
(* ********************************************************************** *)
include "compiler/environment.ma".
+include "compiler/ast_tree.ma".
(* ********************** *)
(* GESTIONE AMBIENTE FLAT *)
(* ********************** *)
-(* STRUTTURA AMBIENTE FLAT *)
+(* ambiente flat *)
+inductive var_flatElem : Type ≝
+VAR_FLAT_ELEM: aux_strId_type → desc_elem → var_flatElem.
-(* elemento: name + desc *)
-inductive flatVar_elem : Type ≝
-VAR_FLAT_ELEM: aux_strId_type → desc_elem → flatVar_elem.
+definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
+definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
-(* tipo pubblico *)
-definition aux_flatEnv_type ≝ list flatVar_elem.
+definition aux_flatEnv_type ≝ list var_flatElem.
-(* getter *)
-definition get_nameId_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
-definition get_desc_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
+definition empty_flatEnv ≝ nil var_flatElem.
-(* ambiente vuoto *)
-definition empty_flatEnv ≝ nil flatVar_elem.
+(* mappa: nome + max + cur *)
+inductive map_list : nat → Type ≝
+ map_nil: map_list O
+| map_cons: ∀n.option nat → map_list n → map_list (S n).
-(* recupera descrittore da ambiente : dummy se non esiste (impossibile) *)
-let rec get_desc_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) on e ≝
-match e with
- [ nil ⇒ None ?
- | cons h tl ⇒ match eqStrId_str str (get_nameId_flatVar h) with
- [ true ⇒ Some ? (get_desc_flatVar h)
- | false ⇒ get_desc_flatEnv_aux tl str ]].
+definition defined_mapList ≝
+λd.λl:map_list d.match l with [ map_nil ⇒ False | map_cons _ _ _ ⇒ True ].
-definition get_desc_flatEnv ≝
-λe:aux_flatEnv_type.λstr:aux_strId_type.
- match get_desc_flatEnv_aux e str with
+definition cut_first_mapList : Πd.map_list d → ? → map_list (pred d) ≝
+λd.λl:map_list d.λp:defined_mapList ? l.
+ let value ≝
+ match l
+ return λX.λY:map_list X.defined_mapList X Y → map_list (pred X)
+ with
+ [ map_nil ⇒ λp:defined_mapList O map_nil.False_rect ? p
+ | map_cons n h t ⇒ λp:defined_mapList (S n) (map_cons n h t).t
+ ] p in value.
+
+definition get_first_mapList : Πd.map_list d → ? → option nat ≝
+λd.λl:map_list d.λp:defined_mapList ? l.
+ let value ≝
+ match l
+ return λX.λY:map_list X.defined_mapList X Y → option nat
+ with
+ [ map_nil ⇒ λp:defined_mapList O map_nil.False_rect ? p
+ | map_cons n h t ⇒ λp:defined_mapList (S n) (map_cons n h t).h
+ ] p in value.
+
+inductive map_elem (d:nat) : Type ≝
+MAP_ELEM: aux_str_type → nat → map_list (S d) → map_elem d.
+
+definition get_name_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM n _ _ ⇒ n ].
+definition get_max_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ m _ ⇒ m ].
+definition get_cur_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ _ c ⇒ c ].
+
+definition aux_map_type ≝ λd.list (map_elem d).
+
+definition empty_map ≝ nil (map_elem O).
+
+lemma defined_mapList_S_to_true :
+∀d.∀l:map_list (S d).defined_mapList (S d) l = True.
+ intros;
+ inversion l;
+ [ intros; destruct H
+ | intros; simplify; reflexivity
+ ]
+qed.
+
+lemma defined_mapList_get :
+ ∀d.∀h:map_elem d.defined_mapList (S d) (get_cur_mapElem d h).
+ intros 2;
+ rewrite > (defined_mapList_S_to_true ? (get_cur_mapElem d h));
+ apply I.
+qed.
+
+(* get_id *)
+let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝
+ match map with
+ [ nil ⇒ None ?
+ | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
+ [ true ⇒ get_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??)
+ | false ⇒ get_id_map_aux d t name
+ ]
+ ].
+
+definition get_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
+
+(* get_max *)
+let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝
+ match map with
+ [ nil ⇒ None ?
+ | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
+ [ true ⇒ Some ? (get_max_mapElem d h)
+ | false ⇒ get_max_map_aux d t name
+ ]
+ ].
+
+definition get_max_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_max_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
+
+(* check_id *)
+definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ False | Some _ ⇒ True ].
+
+definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ].
+
+lemma checkbidmap_to_checkidmap : ∀d.∀map:aux_map_type d.∀name.checkb_id_map d map name = true → check_id_map d map name.
+ unfold checkb_id_map;
+ unfold check_id_map;
+ intros 3;
+ elim (get_id_map_aux d map name) 0;
+ [ simplify; intro; destruct H
+ | simplify; intros; apply I
+ ].
+qed.
+
+definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ True | Some _ ⇒ False ].
+
+definition checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ].
+
+lemma checknotbidmap_to_checknotidmap : ∀d.∀map:aux_map_type d.∀name.checknotb_id_map d map name = true → checknot_id_map d map name.
+ unfold checknotb_id_map;
+ unfold checknot_id_map;
+ intros 3;
+ elim (get_id_map_aux d map name) 0;
+ [ simplify; intro; apply I
+ | simplify; intros; destruct H
+ ].
+qed.
+
+(* get_desc *)
+let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝
+ match fe with
+ [ nil ⇒ None ?
+ | cons h t ⇒ match eqStrId_str name (get_name_flatVar h) with
+ [ true ⇒ Some ? (get_desc_flatVar h)
+ | false ⇒ get_desc_flatEnv_aux t name
+ ]
+ ].
+
+definition get_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux fe str with
[ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
-definition check_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
- match get_desc_flatEnv_aux e str with [ None ⇒ False | Some _ ⇒ True ].
+definition check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux fe str with [ None ⇒ False | Some _ ⇒ True ].
-definition checkb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
- match get_desc_flatEnv_aux e str with [ None ⇒ false | Some _ ⇒ true ].
+definition checkb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux fe str with [ None ⇒ false | Some _ ⇒ true ].
-lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str = true → check_desc_flatEnv e str.
+lemma checkbdescflatenv_to_checkdescflatenv : ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str.
unfold checkb_desc_flatEnv;
unfold check_desc_flatEnv;
- intros;
- letin K ≝ (get_desc_flatEnv_aux e str);
- elim K;
- [ normalize; autobatch |
- normalize; autobatch ]
+ intros 2;
+ elim (get_desc_flatEnv_aux fe str) 0;
+ [ simplify; intro; destruct H
+ | simplify; intros; apply I
+ ].
qed.
-(* aggiungi descrittore ad ambiente: in coda *)
-definition add_desc_flatEnv ≝
-λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
- e@[VAR_FLAT_ELEM str (DESC_ELEM b t)].
+definition checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux fe str with [ None ⇒ True | Some _ ⇒ False ].
+
+definition checknotb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux fe str with [ None ⇒ true | Some _ ⇒ false ].
-(* controllo fe <= fe' *)
+lemma checknotbdescflatenv_to_checknotdescflatenv : ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str.
+ unfold checknotb_desc_flatEnv;
+ unfold checknot_desc_flatEnv;
+ intros 2;
+ elim (get_desc_flatEnv_aux fe str) 0;
+ [ simplify; intro; apply I
+ | simplify; intros; destruct H
+ ].
+qed.
+
+(* fe <= fe' *)
definition eq_flatEnv_elem ≝
λe1,e2.match e1 with
[ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
[ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
].
-lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
+lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true.
+ intros 3;
+ rewrite < H;
+ elim e1;
+ [ reflexivity
+ | simplify;
+ rewrite > (eq_to_eqflatenv a a (refl_eq ??));
+ rewrite > H1;
+ reflexivity
+ ].
+qed.
+
+lemma leflatenv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
intro;
elim fe 0;
[ intros; exists; [ apply fe' | reflexivity ]
].
qed.
+lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
+ intros;
+ elim fe;
+ [ simplify;
+ reflexivity
+ | simplify;
+ rewrite > (eq_to_eqflatenv a a (refl_eq ??));
+ rewrite > H;
+ reflexivity
+ ].
+qed.
+
lemma leflatenv_to_check : ∀fe,fe',str.
(le_flatEnv fe fe' = true) →
(check_desc_flatEnv fe str) →
(check_desc_flatEnv fe' str).
intros 4;
- cases (leflatEnv_to_le fe fe' H);
+ cases (leflatenv_to_le fe fe' H);
rewrite < H1;
elim fe 0;
[ intro; simplify in H2:(%); elim H2;
| intros 3;
simplify;
- cases (eqStrId_str str (get_nameId_flatVar a));
+ cases (eqStrId_str str (get_name_flatVar a));
[ simplify; intro; apply H3
- | simplify;
- apply H2
+ | simplify; apply H2
]
].
qed.
-lemma adddescflatenv_to_leflatenv : ∀fe,n,b,t.le_flatEnv fe (add_desc_flatEnv fe n b t) = true.
-intros;
- change in ⊢ (? ? (? ? %) ?) with (fe@[VAR_FLAT_ELEM n (DESC_ELEM b t)]);
+lemma leflatenv_to_get : ∀fe,fe',str.
+ (le_flatEnv fe fe' = true) →
+ (check_desc_flatEnv fe str) →
+ (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
+ intros 4;
+ cases (leflatenv_to_le fe fe' H);
+ rewrite < H1;
elim fe 0;
- [ 1: reflexivity
- | 2: do 3 intro;
- unfold le_flatEnv;
- change in ⊢ (? ? % ?) with ((eq_flatEnv_elem a a)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)])));
- unfold eq_flatEnv_elem;
- elim a;
- change in ⊢ (? ? % ?) with ((eqStrId_str a1 a1)⊗(eqDesc_elem d d)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)])));
- rewrite > (eq_to_eqstrid a1 a1 (refl_eq ??));
- rewrite > (eq_to_eqdescelem d d (refl_eq ??));
- rewrite > H;
- reflexivity
+ [ intro;
+ simplify in H2:(%);
+ elim H2
+ | simplify;
+ intros 2;
+ cases (eqStrId_str str (get_name_flatVar a));
+ [ simplify;
+ intros;
+ reflexivity
+ | simplify;
+ unfold check_desc_flatEnv;
+ unfold get_desc_flatEnv;
+ cases (get_desc_flatEnv_aux l str);
+ [ simplify; intros; elim H3
+ | simplify; intros; rewrite < (H2 H3); reflexivity
+ ]
+ ]
].
qed.
-(* STRUTTURA MAPPA TRASFORMAZIONE *)
+(* controllo di coerenza env <-> map *)
+let rec check_map_env_align_auxEnv (d:nat) (e:aux_env_type d) (str:aux_str_type) (res:nat) on e ≝
+ match e with
+ [ env_nil h ⇒ λf.f h
+ | env_cons d' h t ⇒ λf.check_map_env_align_auxEnv d' t str (f h)
+ ] (λx.match get_desc_from_lev_env x str with [ None ⇒ S res | Some _ ⇒ O ]).
+
+let rec check_map_env_align_auxMap (d:nat) (map:map_list d) (res:nat) on map ≝
+ match map with
+ [ map_nil ⇒ eqb res O
+ | map_cons d' h t ⇒ match eqb res O with
+ [ true ⇒ match h with
+ [ None ⇒ check_map_env_align_auxMap d' t O | Some _ ⇒ false ]
+ | false ⇒ match h with
+ [ None ⇒ false | Some _ ⇒ check_map_env_align_auxMap d' t (pred res) ]
+ ]
+ ].
-(* elemento: nome + cur + max + dimostrazione *)
-inductive maxCur_elem (e:aux_env_type) (fe:aux_flatEnv_type) : Type ≝
-MAX_CUR_ELEM: ∀str:aux_str_type.∀cur:nat.nat → (check_desc_env e str → get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) → maxCur_elem e fe.
+(* esprimendolo in lingua umana il vincolo che controlla e':
+ ∀name ϵ map.
+ la map_list "cur" deve avere la seguente struttura
+ - Some _ ; ... ; Some _ ; None ; ... None
+ - il numero di Some _ deve essere pari a (d + 1 - x) con x
+ ricavato scandendo in avanti tutti gli ambienti e
+ numerando quanti ambienti CONSECUTIVI non contengono la definizione di name
+
+ ex: scandendo e in avanti si trova la seguente sequenza di check per il nome "pippo"
+ no si no si NO NO
+ quindi sapendo che d=5 (6 partendo da 0) e che check_env_align_aux ha restituito 2
+ sappiamo che la mappa alla voce "pippo" deve avere la seguente struttura scandita in avanti
+ Some _ ; Some _ ; Some _ ; Some _ ; None ; None
+ cioe' 5+1-2 Some seguiti da solo None
+
+ NB: e' solo meta' perche' cosi' si asserisce map ≤ env
+
+*)
+let rec check_map_env_align (d:nat) (e:aux_env_type d) (map:aux_map_type d) on map ≝
+ match map with
+ [ nil ⇒ true
+ | cons h t ⇒ (check_map_env_align_auxMap (S d) (get_cur_mapElem d h) (d + 1 - (check_map_env_align_auxEnv d e (get_name_mapElem d h) O)))⊗
+ (check_map_env_align d e t)
+ ].
-(* tipo pubblico *)
-definition aux_trasfMap_type ≝ λe,fe.list (maxCur_elem e fe).
+let rec check_env_map_align_aux (d:nat) (map:aux_map_type d) (le:list var_elem) on le ≝
+ match le with
+ [ nil ⇒ true
+ | cons h t ⇒ match get_id_map_aux d map (get_name_var h) with
+ [ None ⇒ false | Some _ ⇒ check_env_map_align_aux d map t ]
+ ].
-(* getter *)
-definition get_name_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM n _ _ _ ⇒ n ].
-definition get_cur_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM _ c _ _ ⇒ c ].
-definition get_max_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM _ _ m _ ⇒ m ].
+(* esprimendolo in lingua umana il vincolo che controlla e':
+ ∀name ϵ e.name ϵ map
+
+ NB: e' l'altra meta' perche' cosi' asserisce env ≤ map
+*)
+let rec check_env_map_align (de:nat) (e:aux_env_type de) (dm:nat) (map:aux_map_type dm) on e ≝
+ match e with
+ [ env_nil h ⇒ check_env_map_align_aux dm map h
+ | env_cons d' h t ⇒ (check_env_map_align_aux dm map h)⊗(check_env_map_align d' t dm map)
+ ].
-(* mappa di trasformazione vuota *)
-definition empty_trasfMap ≝ λe,fe.nil (maxCur_elem e fe).
+(* invariante *)
+definition env_to_flatEnv_inv ≝
+ λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type.
+ ∀str.
+ check_desc_env d e str →
+ (((check_env_map_align d e d map)⊗(check_map_env_align d e map)) = true ∧
+ check_id_map d map str ∧
+ check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
+ get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
+
+lemma inv_to_checkdescflatenv :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
+ env_to_flatEnv_inv d e map fe →
+ (∀str.check_desc_env d e str → check_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
+ intros 7;
+ unfold env_to_flatEnv_inv in H:(%);
+ lapply (H str H1);
+ apply (proj2 ?? (proj1 ?? Hletin));
+qed.
-(* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *)
+lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
+ unfold env_to_flatEnv_inv;
+ unfold empty_env;
+ unfold empty_map;
+ unfold empty_flatEnv;
+ simplify;
+ intros;
+ elim H.
+qed.
-(* recupera descrittore da mappa trasformazione : dummy se non esiste (impossibile) *)
-let rec get_maxcur_map (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) (str:aux_str_type) on map ≝
+lemma leflatenv_to_inv :
+ ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
+ le_flatEnv fe fe' = true →
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv d e map fe'.
+ intros 6;
+ unfold env_to_flatEnv_inv;
+ intros;
+ split;
+ [ split;
+ [ lapply (H1 str H2);
+ apply (proj1 ?? (proj1 ?? Hletin))
+ | lapply (H1 str H2);
+ apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
+ ]
+ | lapply (H1 str H2);
+ rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
+ apply (proj2 ?? Hletin)
+ ].
+qed.
+
+lemma leflatenv_trans :
+ ∀fe,fe',fe''.
+ le_flatEnv fe fe' = true →
+ le_flatEnv fe' fe'' = true →
+ le_flatEnv fe fe'' = true.
+ intros 4;
+ cases (leflatenv_to_le fe ? H);
+ rewrite < H1;
+ intro;
+ cases (leflatenv_to_le (fe@x) fe'' H2);
+ rewrite < H3;
+ rewrite > associative_append;
+ apply (le_to_leflatenv fe ?).
+qed.
+
+(* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
+let rec enter_map d (map:aux_map_type d) on map ≝
match map with
- [ nil ⇒ None ?
- | cons h tl ⇒ match eqStr_str str (get_name_maxCur e fe h) with
- [ true ⇒ Some ? h | false ⇒ get_maxcur_map e fe tl str ]].
-
-(* prossimo nome *)
-definition next_nameId ≝
-λe,fe.λmap:aux_trasfMap_type e fe.λstr:aux_str_type.
- match get_maxcur_map e fe map str with
- [ None ⇒ STR_ID str 0
- | Some maxcur ⇒ STR_ID str (S (get_max_maxCur e fe maxcur))
+ [ nil ⇒ []
+ | cons h t ⇒
+ (MAP_ELEM (S d)
+ (get_name_mapElem d h)
+ (get_max_mapElem d h)
+ (map_cons (S d)
+ (get_first_mapList ? (get_cur_mapElem d h) (defined_mapList_get ??))
+ (get_cur_mapElem d h))
+ )::(enter_map d t)
].
-(* nome -> nome + id *)
-definition name_to_nameId ≝
-λe,fe.λmap:aux_trasfMap_type e fe.λstr:aux_str_type.
- match get_maxcur_map e fe map str with
- [ None ⇒ STR_ID str 0
- | Some maxcur ⇒ STR_ID str (get_cur_maxCur e fe maxcur)
+lemma getidmap_to_enter :
+ ∀d.∀m:aux_map_type d.∀str.
+ get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
+ intros;
+ elim m;
+ [ simplify; reflexivity
+ | simplify; rewrite > H; reflexivity
+ ]
+qed.
+
+(* leave: elimina la testa (il "cur" corrente) *)
+let rec leave_map d (map:aux_map_type (S d)) on map ≝
+ match map with
+ [ nil ⇒ []
+ | cons h t ⇒
+ (MAP_ELEM d
+ (get_name_mapElem (S d) h)
+ (get_max_mapElem (S d) h)
+ (cut_first_mapList ? (get_cur_mapElem (S d) h) (defined_mapList_get ??))
+ )::(leave_map d t)
].
-(* NB: se cerco qualcos'altro il risultato e' invariato *)
-axiom add_maxcur_map_aux_false : ∀e,fe,str,cur,str',b',desc',map.
-(check_desc_env e str →
- get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
-(eqStr_str str str' = false) →
-(check_desc_env (add_desc_env e str' b' desc') str →
- get_desc_env (add_desc_env e str' b' desc') str =
- get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str cur)).
-
-(* NB: se cerco cio' che e' appena stato aggiunto, deve essere uguale *)
-axiom add_maxcur_map_aux_true : ∀e,fe,str,cur,max,str',b',desc',map.
-(check_desc_env e str →
- get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
-(eqStr_str str str' = true) →
-(check_desc_env (add_desc_env e str' b' desc') str →
- get_desc_env (add_desc_env e str' b' desc') str =
- get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str (S max))).
-
-axiom add_maxcur_map_aux_new : ∀e,fe,str,b,desc,map.
- check_desc_env (add_desc_env e str b desc) str →
- get_desc_env (add_desc_env e str b desc) str =
- get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str) b desc) (STR_ID str 0).
-
-(* NB: avendo poi in input la dimostrazione "check_desc_env e (get_name_ast_id e b t ast)" ha senso *)
-axiom ast_to_astfe_id_aux : ∀e,fe.∀map:aux_trasfMap_type e fe.∀str.
- check_desc_env e str → check_desc_flatEnv fe (name_to_nameId e fe map str).
-
-axiom ast_to_astfe_dec_aux : ∀e,str,b,t,fe,map.
- check_not_already_def_env e str →
- check_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str) b t) (next_nameId e fe map str).
-
-(* aggiungi/aggiorna descrittore mappa trasformazione *)
-let rec add_maxcur_map_aux (e:aux_env_type) (fe:aux_flatEnv_type) (map,fMap:aux_trasfMap_type e fe)
- (str:aux_str_type) (b:bool) (desc:ast_type) (flag:bool) on map
- : aux_trasfMap_type (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc) ≝
-match map with
- [ nil ⇒
- match flag with
- [ true ⇒ []
- | false ⇒
- [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
- str 0 0 (add_maxcur_map_aux_new e fe str b desc fMap) ]
- ]
- | cons h tl ⇒ match h with
- [ MAX_CUR_ELEM str' cur' max' dim' ⇒
- match eqStr_str str' str return λx.(eqStr_str str' str = x) → ? with
- [ true ⇒ λp:(eqStr_str str' str = true).
- [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
- str' (S max') (S max')
- (add_maxcur_map_aux_true e fe str' cur' max' str b desc fMap dim' p)
- ]@(add_maxcur_map_aux e fe tl fMap str b desc true)
- | false ⇒ λp:(eqStr_str str' str = false).
- [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
- str' cur' max'
- (add_maxcur_map_aux_false e fe str' cur' str b desc fMap dim' p)
- ]@(add_maxcur_map_aux e fe tl fMap str b desc flag)
- ] (refl_eq ? (eqStr_str str' str))
- ]
- ].
+(* aggiungi descrittore *)
+let rec new_map_elem_from_depth_aux (d:nat) on d ≝
+ match d
+ return λd.map_list d
+ with
+ [ O ⇒ map_nil
+ | S n ⇒ map_cons n (None ?) (new_map_elem_from_depth_aux n)
+ ].
-definition add_maxcur_map ≝
-λe:aux_env_type.λfe:aux_flatEnv_type.λmap,fMap:aux_trasfMap_type e fe.λstr:aux_str_type.λb:bool.λdesc:ast_type.
-add_maxcur_map_aux e fe map fMap str b desc false.
+let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
+ match map with
+ [ nil ⇒ []
+ | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
+ [ true ⇒ MAP_ELEM d name max (map_cons d (Some ? max) (cut_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??)))
+ | false ⇒ h
+ ]::(new_max_map_aux d t name max)
+ ].
-(* composizione di funzioni generata da una lista di nome x const x tipo *)
-definition aux_trasfEnv_type ≝ list (Prod3T aux_str_type bool ast_type).
+definition add_desc_env_flatEnv_map ≝
+λd.λmap:aux_map_type d.λstr.
+ match get_max_map_aux d map str with
+ [ None ⇒ map@[ MAP_ELEM d str O (map_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ]
+ | Some x ⇒ new_max_map_aux d map str (S x)
+ ].
-let rec build_trasfEnv (trasf:aux_trasfEnv_type) on trasf : aux_env_type → aux_env_type ≝
- match trasf with
+definition add_desc_env_flatEnv_fe ≝
+λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
+ fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
+ (DESC_ELEM c desc) ].
+
+let rec build_trasfEnv_env (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf : aux_env_type d → aux_env_type d ≝
+ match trsf with
[ nil ⇒ (λx.x)
- | cons h tl ⇒ (λx.(build_trasfEnv tl) (add_desc_env x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
+ | cons h t ⇒ (λx.(build_trasfEnv_env d t) (add_desc_env d x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
].
-lemma build_trasfEnv_exists_aux : ∀a.∀trsf:aux_trasfEnv_type.∀c.
- ∃b.build_trasfEnv trsf (c§§a) = (b§§a).
- intros 2;
- elim trsf;
- [ simplify; exists; [apply c | reflexivity]
- | simplify; apply H; ]
+let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf :
+ Prod (aux_map_type d) aux_flatEnv_type → Prod (aux_map_type d) aux_flatEnv_type ≝
+ match trsf with
+ [ nil ⇒ (λx.x)
+ | cons h t ⇒ (λx.(build_trasfEnv_mapFe d t)
+ (pair ?? (add_desc_env_flatEnv_map d (fst ?? x) (fst3T ??? h))
+ (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))))
+ ].
+
+(* avanzamento dell'invariante *)
+axiom env_map_flatEnv_enter_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe.
+
+axiom env_map_flatEnv_add_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env d trsf e)
+ (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
+
+lemma env_map_flatEnv_addNil_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env d [] e)
+ (fst ?? (build_trasfEnv_mapFe d [] (pair ?? map fe)))
+ (snd ?? (build_trasfEnv_mapFe d [] (pair ?? map fe))).
+ intros;
+ simplify;
+ apply H.
qed.
-lemma eq_enter_leave : ∀e,trsf.leave_env (build_trasfEnv trsf (enter_env e)) = e.
+lemma env_map_flatEnv_addSingle_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀name,const,desc.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv d
+ (add_desc_env d e name const desc)
+ (fst ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe)))
+ (snd ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe))).
intros;
- change in ⊢ (? ? (? (? ? %)) ?) with ([]§§e);
- cases (build_trasfEnv_exists_aux e trsf []);
- rewrite > H;
- reflexivity.
+ apply (env_map_flatEnv_add_aux d e map fe [ tripleT ??? name const desc ]);
+ apply H.
qed.
-(* NB: leave ... enter e' equivalente a e originale *)
-lemma retype_enter_leave_to_e_aux : ∀e,fe,str,cur,trsf.
- (check_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str →
- get_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str = get_desc_flatEnv fe (STR_ID str cur)) →
- (check_desc_env e str →
- get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)).
- intros 5;
- rewrite > (eq_enter_leave e trsf);
+lemma env_map_flatEnv_addJoin_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe:aux_flatEnv_type.∀name,const,desc,trsf.
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env d trsf (add_desc_env d e name const desc))
+ map fe →
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env d ([ tripleT ??? name const desc ]@trsf) e)
+ map fe.
intros;
- apply H;
- apply H1.
+ simplify;
+ apply H.
qed.
-let rec retype_enter_leave_to_e (e:aux_env_type) (fe:aux_flatEnv_type) (trsf:aux_trasfEnv_type)
- (map:aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe) on map : aux_trasfMap_type e fe ≝
- match map with
- [ nil ⇒ []
- | cons h tl ⇒ match h with
- [ MAX_CUR_ELEM str cur max dim ⇒
- [MAX_CUR_ELEM e fe str cur max (retype_enter_leave_to_e_aux e fe str cur trsf dim)]@(retype_enter_leave_to_e e fe trsf tl)
- ]].
-
-lemma retype_e_to_enter_leave_aux : ∀e,fe,str,cur,trsf.
- (check_desc_env e str →
- get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
- (check_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str →
- get_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str = get_desc_flatEnv fe (STR_ID str cur)).
- intros 5;
- rewrite < (eq_enter_leave e trsf) in ⊢ ((? % ?→?)→?);
- rewrite < (eq_enter_leave e trsf) in ⊢ ((?→? ? (? % ?) ?)→?);
+lemma env_map_flatEnv_add_aux_fe_al :
+ ∀trsf.∀d.∀m:aux_map_type d.∀a,l.
+ snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m (a::l))) =
+ a::(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l))).
+ intro;
+ elim trsf;
+ [ simplify; reflexivity
+ | simplify;
+ elim a;
+ simplify;
+ rewrite > (H ????);
+ reflexivity
+ ].
+qed.
+
+lemma env_map_flatEnv_add_aux_fe_l :
+ ∀trsf.∀d.∀m:aux_map_type d.∀l.
+ snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l)) =
+ l@(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m []))).
intros;
- apply H;
- apply H1.
+ elim l;
+ [ simplify; reflexivity
+ | rewrite > (env_map_flatEnv_add_aux_fe_al ????);
+ rewrite > H;
+ reflexivity
+ ].
qed.
-let rec retype_e_to_enter_leave (e:aux_env_type) (fe:aux_flatEnv_type) (trsf:aux_trasfEnv_type)
- (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe ≝
- match map with
- [ nil ⇒ []
- | cons h tl ⇒ match h with
- [ MAX_CUR_ELEM str cur max dim ⇒
- [MAX_CUR_ELEM (leave_env ((build_trasfEnv trsf) (enter_env e))) fe str cur max (retype_e_to_enter_leave_aux e fe str cur trsf dim)]@(retype_e_to_enter_leave e fe trsf tl)
- ]].
-
-(* NB: enter non cambia fe *)
-lemma retype_e_to_enter_aux : ∀e,fe,str,cur.
- (check_desc_env e str →
- get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
- (check_desc_env (enter_env e) str →
- get_desc_env (enter_env e) str = get_desc_flatEnv fe (STR_ID str cur)).
- intros 6;
- rewrite > H;
- [ reflexivity
- | apply H1
+lemma env_map_flatEnv_add_aux_fe :
+ ∀d.∀map:aux_map_type d.∀fe,trsf.
+ ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
+ intros 3;
+ elim fe 0;
+ [ simplify;
+ intro;
+ exists;
+ [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
+ | reflexivity
+ ]
+ | intros 4;
+ exists;
+ [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
+ | rewrite > (env_map_flatEnv_add_aux_fe_al trsf d map a l);
+ rewrite > (env_map_flatEnv_add_aux_fe_l trsf d map l);
+ rewrite < (cons_append_commute ????);
+ reflexivity
+ ]
].
qed.
-let rec retype_e_to_enter (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (enter_env e) fe ≝
- match map with
- [ nil ⇒ []
- | cons h tl ⇒ match h with
- [ MAX_CUR_ELEM str cur max dim ⇒
- [MAX_CUR_ELEM (enter_env e) fe str cur max (retype_e_to_enter_aux e fe str cur dim)]@(retype_e_to_enter e fe tl)
- ]].
-
-(* NB: leave non cambia fe *)
-axiom retype_e_to_leave_aux : ∀e,fe,str,cur.
- (check_desc_env e str →
- get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
- (check_desc_env (leave_env e) str →
- get_desc_env (leave_env e) str = get_desc_flatEnv fe (STR_ID str cur)).
-
-let rec retype_e_to_leave (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (leave_env e) fe ≝
- match map with
- [ nil ⇒ []
- | cons h tl ⇒ match h with
- [ MAX_CUR_ELEM str cur max dim ⇒
- [MAX_CUR_ELEM (leave_env e) fe str cur max (retype_e_to_leave_aux e fe str cur dim)]@(retype_e_to_leave e fe tl)
- ]].
+lemma buildtrasfenvadd_to_le :
+ ∀d.∀m:aux_map_type d.∀fe,trsf.
+ le_flatEnv fe (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m fe))) = true.
+ intros 4;
+ cases (env_map_flatEnv_add_aux_fe d m fe trsf);
+ rewrite < H;
+ rewrite > (le_to_leflatenv fe x);
+ reflexivity.
+qed.
-let rec rollback_map (e:aux_env_type) (fe,fe':aux_flatEnv_type) (trsf:aux_trasfEnv_type) (map:aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe')
- (snap:aux_trasfMap_type e fe) on map : aux_trasfMap_type e fe' ≝
- match map with
- [ nil ⇒ empty_trasfMap e fe'
- | cons h tl ⇒
- match get_maxcur_map e fe snap (get_name_maxCur ?? h) with
- [ None ⇒ retype_enter_leave_to_e e fe' trsf [h]
- | Some new ⇒
- [ MAX_CUR_ELEM ?? (get_name_maxCur ?? h) (get_cur_maxCur ?? new)
- (get_max_maxCur ?? h) (False_rect ? daemon) ]
- ] @ rollback_map e fe fe' trsf tl snap
- ].
+axiom env_map_flatEnv_leave_aux :
+ ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf.
+ env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe →
+ env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe.
-(* sequenza di utilizzo:
-
-[BLOCCO ESTERNO]
-
-|DICHIARAZIONE "pippo":
-| -) MAP1 <- add_maxcur_map MAP0 "pippo"
-| -) ENV1 <- add_desc_flatEnv ENV0 (name_to_nameId MAP1 "pippo") DESC
-|
-|ACCESSO "pippo":
-| -) name_to_nameId MAP1 "pippo"
-|
-|PREPARAZIONE ENTRATA BLOCCO INTERNO:
-| -) SNAP <- build_snapshot MAP1
-
- |[BLOCCO INTERNO]
- |
- |DICHIARAZIONE "pippo":
- | -) MAP2 <- add_maxcur_map MAP1 "pippo"
- | -) ENV2 <- add_desc_flatEnv ENV (name_to_nameId MAP2 "pippo") DESC
- |
- |ACCESSO "pippo":
- | -) name_to_nameId MAP2 "pippo"
- |
- |PREPARAZIONE USCITA BLOCCO INTERNO:
- | -) MAP3 <- rollback_map MAP2 SNAP
-
-| ...
-*)
+lemma leave_add_enter_env_aux :
+ ∀d.∀a:aux_env_type d.∀trsf.∀c.
+ ∃b.build_trasfEnv_env (S d) trsf (env_cons d c a) = (env_cons d b a).
+ intros 3;
+ elim trsf;
+ [ simplify; exists; [ apply c | reflexivity ]
+ | simplify; apply H
+ ].
+qed.
-(* mini test
-definition pippo ≝ [ ch_P ].
-definition pluto ≝ [ ch_Q ].
-definition pippodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
-definition pippodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
-definition pippodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32).
-definition plutodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
-definition plutodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
-definition plutodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32).
-
-definition map1 ≝ add_maxcur_map empty_env empty_flatEnv (empty_trasfMap ??) (empty_trasfMap ??) pippo false pippodesc1.
-definition env1 ≝ add_desc_env empty_env pippo false pippodesc1.
-definition fenv1 ≝ add_desc_flatEnv empty_flatEnv (next_nameId empty_env empty_flatEnv (empty_trasfMap ??) pippo) false pippodesc1.
-definition map2 ≝ add_maxcur_map env1 fenv1 map1 map1 pluto false plutodesc1.
-definition env2 ≝ add_desc_env env1 pluto false plutodesc1.
-definition fenv2 ≝ add_desc_flatEnv fenv1 (next_nameId ?? map1 pluto) false plutodesc1.
-
-definition env2' ≝ enter_env env2.
-definition map2' ≝ retype_e_to_enter env2 fenv2 map2.
-
-definition map3 ≝ add_maxcur_map env2' fenv2 map2' map2' pippo true pippodesc2.
-definition env3 ≝ add_desc_env env2' pippo true pippodesc2.
-definition fenv3 ≝ add_desc_flatEnv fenv2 (next_nameId ?? map2' pippo) true pippodesc2.
-definition map4 ≝ add_maxcur_map env3 fenv3 map3 map3 pluto true plutodesc2.
-definition env4 ≝ add_desc_env env3 pluto true plutodesc2.
-definition fenv4 ≝ add_desc_flatEnv fenv3 (next_nameId ?? map3 pluto) true plutodesc2.
-
-definition env4' ≝ enter_env env4.
-definition map4' ≝ retype_e_to_enter env4 fenv4 map4.
-
-definition map5 ≝ add_maxcur_map env4' fenv4 map4' map4' pippo false pippodesc3.
-definition env5 ≝ add_desc_env env4' pippo false pippodesc3.
-definition fenv5 ≝ add_desc_flatEnv fenv4 (next_nameId ?? map4' pippo) false pippodesc3.
-definition map6 ≝ add_maxcur_map env5 fenv5 map5 map5 pluto false plutodesc3.
-definition env6 ≝ add_desc_env env5 pluto false plutodesc3.
-definition fenv6 ≝ add_desc_flatEnv fenv5 (next_nameId ?? map5 pluto) false plutodesc3.
-
-definition map6' ≝ retype_e_to_leave env6 fenv6 map6.
-
-definition map7 ≝ rollback_map env4 fenv4 fenv6 [ tripleT ??? pluto false plutodesc3 ; tripleT ??? pippo false pippodesc3 ] map6' map4.
-
-definition map7' ≝ retype_e_to_leave env4 fenv6 map7.
-
-definition map8 ≝ rollback_map env2 fenv2 fenv6 [ tripleT ??? pluto true plutodesc2 ; tripleT ??? pippo true pippodesc2 ] map7' map2.
-*)
+lemma leave_add_enter_env :
+ ∀d.∀e:aux_env_type d.∀trsf.
+ leave_env d (build_trasfEnv_env (S d) trsf (enter_env d e)) = e.
+ intros;
+ unfold enter_env;
+ lapply (leave_add_enter_env_aux d e trsf []);
+ cases Hletin;
+ rewrite > H;
+ simplify;
+ reflexivity.
+qed.
+
+lemma newid_from_init :
+ ∀d.∀e:aux_env_type d.∀name,const,desc.
+ ast_id d (add_desc_env d e name const desc) const desc.
+ intros;
+ lapply (AST_ID d (add_desc_env d e name const desc) name ?);
+ [ elim e;
+ simplify;
+ rewrite > (eq_to_eqstr ?? (refl_eq ??));
+ simplify;
+ apply I
+ | cut (const = get_const_desc (get_desc_env d (add_desc_env d e name const desc) name) ∧
+ desc = get_type_desc (get_desc_env d (add_desc_env d e name const desc) name));
+ [ rewrite > (proj1 ?? Hcut) in ⊢ (? ? ? % ?);
+ rewrite > (proj2 ?? Hcut) in ⊢ (? ? ? ? %);
+ apply Hletin
+ | split;
+ [ elim e;
+ simplify;
+ rewrite > (eq_to_eqstr ?? (refl_eq ??));
+ simplify;
+ reflexivity
+ | elim e;
+ simplify;
+ rewrite > (eq_to_eqstr ?? (refl_eq ??));
+ simplify;
+ reflexivity
+ ]
+ ]
+ ].
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* *)
-(* Sviluppato da: *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* *)
-(* ********************************************************************** *)
-
-include "compiler/environment.ma".
-
-(* ********************** *)
-(* GESTIONE AMBIENTE FLAT *)
-(* ********************** *)
-
-(* ambiente flat *)
-inductive var_flatElem : Type ≝
-VAR_FLAT_ELEM: aux_strId_type → desc_elem → var_flatElem.
-
-definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
-definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
-
-definition aux_flatEnv_type ≝ list var_flatElem.
-
-definition empty_flatEnv ≝ nil var_flatElem.
-
-(* mappa: nome + max + cur *)
-inductive n_list : nat → Type ≝
- n_nil: n_list O
-| n_cons: ∀n.option nat → n_list n → n_list (S n).
-
-definition defined_nList ≝
-λd.λl:n_list d.match l with [ n_nil ⇒ False | n_cons _ _ _ ⇒ True ].
-
-definition cut_first_nList : Πd.n_list d → ? → n_list (pred d) ≝
-λd.λl:n_list d.λp:defined_nList ? l.
- let value ≝
- match l
- return λX.λY:n_list X.defined_nList X Y → n_list (pred X)
- with
- [ n_nil ⇒ λp:defined_nList O n_nil.False_rect ? p
- | n_cons n h t ⇒ λp:defined_nList (S n) (n_cons n h t).t
- ] p in value.
-
-definition get_first_nList : Πd.n_list d → ? → option nat ≝
-λd.λl:n_list d.λp:defined_nList ? l.
- let value ≝
- match l
- return λX.λY:n_list X.defined_nList X Y → option nat
- with
- [ n_nil ⇒ λp:defined_nList O n_nil.False_rect ? p
- | n_cons n h t ⇒ λp:defined_nList (S n) (n_cons n h t).h
- ] p in value.
-
-inductive map_elem (d:nat) : Type ≝
-MAP_ELEM: aux_str_type → nat → n_list (S d) → map_elem d.
-
-definition get_name_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM n _ _ ⇒ n ].
-definition get_max_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ m _ ⇒ m ].
-definition get_cur_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ _ c ⇒ c ].
-
-definition aux_map_type ≝ λd.list (map_elem d).
-
-definition empty_map ≝ nil (map_elem O).
-
-lemma defined_nList_S_to_true :
-∀d.∀l:n_list (S d).defined_nList (S d) l = True.
- intros;
- inversion l;
- [ intros; destruct H
- | intros; simplify; reflexivity
- ]
-qed.
-
-lemma defined_get_id :
- ∀d.∀h:map_elem d.defined_nList (S d) (get_cur_mapElem d h).
- intros 2;
- rewrite > (defined_nList_S_to_true ? (get_cur_mapElem d h));
- apply I.
-qed.
-
-(* get_id *)
-let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝
- match map with
- [ nil ⇒ None ?
- | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
- [ true ⇒ get_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ??)
- | false ⇒ get_id_map_aux d t name
- ]
- ].
-
-definition get_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
- match get_id_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
-
-(* get_max *)
-let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝
- match map with
- [ nil ⇒ None ?
- | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
- [ true ⇒ Some ? (get_max_mapElem d h)
- | false ⇒ get_max_map_aux d t name
- ]
- ].
-
-definition get_max_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
- match get_max_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
-
-(* check_id *)
-definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
- match get_id_map_aux d map name with [ None ⇒ False | Some _ ⇒ True ].
-
-definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
- match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ].
-
-lemma checkbidmap_to_checkidmap : ∀d.∀map:aux_map_type d.∀name.checkb_id_map d map name = true → check_id_map d map name.
- unfold checkb_id_map;
- unfold check_id_map;
- intros 3;
- elim (get_id_map_aux d map name) 0;
- [ simplify; intro; destruct H
- | simplify; intros; apply I
- ].
-qed.
-
-definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
- match get_id_map_aux d map name with [ None ⇒ True | Some _ ⇒ False ].
-
-definition checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
- match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ].
-
-lemma checknotbidmap_to_checknotidmap : ∀d.∀map:aux_map_type d.∀name.checknotb_id_map d map name = true → checknot_id_map d map name.
- unfold checknotb_id_map;
- unfold checknot_id_map;
- intros 3;
- elim (get_id_map_aux d map name) 0;
- [ simplify; intro; apply I
- | simplify; intros; destruct H
- ].
-qed.
-
-(* get_desc *)
-let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝
- match fe with
- [ nil ⇒ None ?
- | cons h t ⇒ match eqStrId_str name (get_name_flatVar h) with
- [ true ⇒ Some ? (get_desc_flatVar h)
- | false ⇒ get_desc_flatEnv_aux t name
- ]
- ].
-
-definition get_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
- match get_desc_flatEnv_aux fe str with
- [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
-
-definition check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
- match get_desc_flatEnv_aux fe str with [ None ⇒ False | Some _ ⇒ True ].
-
-definition checkb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
- match get_desc_flatEnv_aux fe str with [ None ⇒ false | Some _ ⇒ true ].
-
-lemma checkbdescflatenv_to_checkdescflatenv : ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str.
- unfold checkb_desc_flatEnv;
- unfold check_desc_flatEnv;
- intros 2;
- elim (get_desc_flatEnv_aux fe str) 0;
- [ simplify; intro; destruct H
- | simplify; intros; apply I
- ].
-qed.
-
-definition checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
- match get_desc_flatEnv_aux fe str with [ None ⇒ True | Some _ ⇒ False ].
-
-definition checknotb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
- match get_desc_flatEnv_aux fe str with [ None ⇒ true | Some _ ⇒ false ].
-
-lemma checknotbdescflatenv_to_checknotdescflatenv : ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str.
- unfold checknotb_desc_flatEnv;
- unfold checknot_desc_flatEnv;
- intros 2;
- elim (get_desc_flatEnv_aux fe str) 0;
- [ simplify; intro; apply I
- | simplify; intros; destruct H
- ].
-qed.
-
-(* fe <= fe' *)
-definition eq_flatEnv_elem ≝
-λe1,e2.match e1 with
- [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
- [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
-
-lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
- intros 3;
- rewrite < H;
- elim e1;
- simplify;
- rewrite > (eq_to_eqstrid a a (refl_eq ??));
- rewrite > (eq_to_eqdescelem d d (refl_eq ??));
- reflexivity.
-qed.
-
-lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
- intros 2;
- elim e1 0;
- elim e2 0;
- intros 4;
- simplify;
- intro;
- rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
- rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
- reflexivity.
-qed.
-
-let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
-match fe with
- [ nil ⇒ true
- | cons h tl ⇒ match fe' with
- [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
- ].
-
-lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true.
- intros 3;
- rewrite < H;
- elim e1;
- [ reflexivity
- | simplify;
- rewrite > (eq_to_eqflatenv a a (refl_eq ??));
- rewrite > H1;
- reflexivity
- ].
-qed.
-
-lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
- intro;
- elim fe 0;
- [ intros; exists; [ apply fe' | reflexivity ]
- | intros 4; elim fe';
- [ simplify in H1:(%); destruct H1
- | simplify in H2:(%);
- rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
- cases (H l1 (andb_true_true_r ?? H2));
- simplify;
- rewrite < H3;
- exists; [ apply x | reflexivity ]
- ]
- ].
-qed.
-
-lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
- intros;
- elim fe;
- [ simplify;
- reflexivity
- | simplify;
- rewrite > (eq_to_eqflatenv a a (refl_eq ??));
- rewrite > H;
- reflexivity
- ].
-qed.
-
-lemma leflatenv_to_check : ∀fe,fe',str.
- (le_flatEnv fe fe' = true) →
- (check_desc_flatEnv fe str) →
- (check_desc_flatEnv fe' str).
- intros 4;
- cases (leflatEnv_to_le fe fe' H);
- rewrite < H1;
- elim fe 0;
- [ intro; simplify in H2:(%); elim H2;
- | intros 3;
- simplify;
- cases (eqStrId_str str (get_name_flatVar a));
- [ simplify; intro; apply H3
- | simplify; apply H2
- ]
- ].
-qed.
-
-lemma leflatenv_to_get : ∀fe,fe',str.
- (le_flatEnv fe fe' = true) →
- (check_desc_flatEnv fe str) →
- (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
- intros 4;
- cases (leflatEnv_to_le fe fe' H);
- rewrite < H1;
- elim fe 0;
- [ intro;
- simplify in H2:(%);
- elim H2
- | simplify;
- intros 2;
- cases (eqStrId_str str (get_name_flatVar a));
- [ simplify;
- intros;
- reflexivity
- | simplify;
- unfold check_desc_flatEnv;
- unfold get_desc_flatEnv;
- cases (get_desc_flatEnv_aux l str);
- [ simplify; intros; elim H3
- | simplify; intros; rewrite < (H2 H3); reflexivity
- ]
- ]
- ].
-qed.
-
-(* invariante *)
-definition env_to_flatEnv_inv ≝
- λd.λe:aux_env_type.λmap:aux_map_type d.λfe:aux_flatEnv_type.
- ∀str.
- check_desc_env e str →
- (check_id_map d map str ∧
- check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
- get_desc_env e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
-
-lemma inv_to_checkdescflatenv :
- ∀d.∀e.∀map:aux_map_type d.∀fe.
- env_to_flatEnv_inv d e map fe →
- (∀str.check_desc_env e str → check_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
- intros 7;
- unfold env_to_flatEnv_inv in H:(%);
- lapply (H str H1);
- apply (proj2 ?? (proj1 ?? Hletin));
-qed.
-
-lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
- unfold env_to_flatEnv_inv;
- unfold empty_env;
- unfold empty_map;
- unfold empty_flatEnv;
- simplify;
- intros;
- split;
- [ split; apply H | reflexivity ].
-qed.
-
-lemma leflatenv_to_inv :
- ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
- le_flatEnv fe fe' = true →
- env_to_flatEnv_inv d e map fe →
- env_to_flatEnv_inv d e map fe'.
- intros 6;
- unfold env_to_flatEnv_inv;
- intros;
- split;
- [ split;
- [ lapply (H1 str H2);
- apply (proj1 ?? (proj1 ?? Hletin))
- | lapply (H1 str H2);
- apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
- ]
- | lapply (H1 str H2);
- rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
- apply (proj2 ?? Hletin)
- ].
-qed.
-
-lemma leflatenv_trans :
- ∀fe,fe',fe''.
- le_flatEnv fe fe' = true →
- le_flatEnv fe' fe'' = true →
- le_flatEnv fe fe'' = true.
- intros 4;
- cases (leflatenv_to_le fe ? H);
- rewrite < H1;
- intro;
- cases (leflatenv_to_le (fe@x) fe'' H2);
- rewrite < H3;
- rewrite > associative_append;
- apply (le_to_leflatenv fe ?).
-qed.
-
-(* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
-let rec enter_map d (map:aux_map_type d) on map ≝
- match map with
- [ nil ⇒ []
- | cons h t ⇒
- (MAP_ELEM (S d)
- (get_name_mapElem d h)
- (get_max_mapElem d h)
- (n_cons (S d)
- (get_first_nList ? (get_cur_mapElem d h) (defined_get_id ??))
- (get_cur_mapElem d h))
- )::(enter_map d t)
- ].
-
-lemma getidmap_to_enter :
- ∀d.∀m:aux_map_type d.∀str.
- get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
- intros;
- elim m;
- [ simplify; reflexivity
- | simplify; rewrite > H; reflexivity
- ]
-qed.
-
-lemma env_map_flatEnv_enter_aux :
- ∀d.∀e.∀map:aux_map_type d.∀fe.
- env_to_flatEnv_inv d e map fe → env_to_flatEnv_inv (S d) (enter_env e) (enter_map d map) fe.
- intros 3;
- unfold enter_env;
- unfold empty_env;
- unfold env_to_flatEnv_inv;
- simplify;
- elim e 0;
- [ elim map 0;
- [ simplify; intros; split;
- [ apply (proj1 ?? (H str H1)) | apply (proj2 ?? (H str H1)); ]
- | simplify; intros; split;
- [ rewrite > (getidmap_to_enter d l str); apply (proj1 ?? (H1 str H2))
- | rewrite > (getidmap_to_enter d l str); apply (proj2 ?? (H1 str H2))
- ]
- ]
- | elim map 0;
- [ simplify; intros; split;
- [ apply (proj1 ?? (H1 str H2)) | apply (proj2 ?? (H1 str H2)) ]
- | simplify; intros; split;
- [ rewrite > (getidmap_to_enter d l str); apply (proj1 ?? (H2 str H3))
- | rewrite > (getidmap_to_enter d l str); apply (proj2 ?? (H2 str H3))
- ]
- ]
- ].
-qed.
-
-(* leave: elimina la testa (il "cur" corrente) *)
-let rec leave_map d (map:aux_map_type (S d)) on map ≝
- match map with
- [ nil ⇒ []
- | cons h t ⇒
- (MAP_ELEM d
- (get_name_mapElem (S d) h)
- (get_max_mapElem (S d) h)
- (cut_first_nList ? (get_cur_mapElem (S d) h) (defined_get_id ??))
- )::(leave_map d t)
- ].
-
-(* aggiungi descrittore *)
-let rec new_map_elem_from_depth_aux (d:nat) on d ≝
- match d
- return λd.n_list d
- with
- [ O ⇒ n_nil
- | S n ⇒ n_cons n (None ?) (new_map_elem_from_depth_aux n)
- ].
-
-let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
- match map with
- [ nil ⇒ []
- | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
- [ true ⇒ MAP_ELEM d name max (n_cons d (Some ? max) (cut_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ??)))
- | false ⇒ h
- ]::(new_max_map_aux d t name max)
- ].
-
-definition add_desc_env_flatEnv_map ≝
-λd.λmap:aux_map_type d.λstr.
- match get_max_map_aux d map str with
- [ None ⇒ map@[ MAP_ELEM d str O (n_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ]
- | Some x ⇒ new_max_map_aux d map str (S x)
- ].
-
-definition add_desc_env_flatEnv_fe ≝
-λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
- fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
- (DESC_ELEM c desc) ].
-
-let rec build_trasfEnv_env (trsf:list (Prod3T aux_str_type bool ast_type)) e on trsf ≝
- match trsf with
- [ nil ⇒ e
- | cons h t ⇒ build_trasfEnv_env t (add_desc_env e (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))
- ].
-
-let rec build_trasfEnv_mapFe (trasf:list ?) d (mfe:Prod (aux_map_type d) aux_flatEnv_type) on trasf ≝
- match trasf with
- [ nil ⇒ mfe
- | cons h t ⇒
- build_trasfEnv_mapFe t d (pair ?? (add_desc_env_flatEnv_map d (fst ?? mfe) (fst3T ??? h))
- (add_desc_env_flatEnv_fe d (fst ?? mfe) (snd ?? mfe) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
- ].
-
-(* avanzamento delle dimostrazioni *)
-axiom env_map_flatEnv_add_aux :
- ∀d.∀e.∀map:aux_map_type d.∀fe.∀trsf.
- env_to_flatEnv_inv d e map fe →
- env_to_flatEnv_inv d
- (build_trasfEnv_env trsf e)
- (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe)))
- (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))).
-
-axiom env_map_flatEnv_add_aux_fe :
- ∀d.∀map:aux_map_type d.∀fe,trsf.
- ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))).
-
-lemma buildtrasfenvadd_to_le :
- ∀d.∀m:aux_map_type d.∀fe,trsf.
- le_flatEnv fe (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) = true.
- intros 4;
- cases (env_map_flatEnv_add_aux_fe d m fe trsf);
- rewrite < H;
- rewrite > (le_to_leflatenv fe x);
- reflexivity.
-qed.
-
-axiom env_map_flatEnv_leave_aux :
- ∀d.∀e.∀map:aux_map_type d.∀fe.∀trsf.
- env_to_flatEnv_inv (S d)
- (build_trasfEnv_env trsf (enter_env e))
- (fst ?? (build_trasfEnv_mapFe trsf (S d) (pair ?? (enter_map d map) fe)))
- (snd ?? (build_trasfEnv_mapFe trsf (S d) (pair ?? (enter_map d map) fe))) →
- env_to_flatEnv_inv d
- e
- (leave_map d (fst ?? (build_trasfEnv_mapFe trsf (S d) (pair ?? (enter_map d map) fe))))
- (snd ?? (build_trasfEnv_mapFe trsf (S d) (pair ?? (enter_map d map) fe))).
VAR_ELEM: aux_str_type → desc_elem → var_elem.
(* ambiente globale: (ambiente base + ambienti annidati) *)
-definition aux_env_type ≝ ne_list (list var_elem).
+inductive env_list : nat → Type ≝
+ env_nil: list var_elem → env_list O
+| env_cons: ∀n.list var_elem → env_list n → env_list (S n).
+
+definition defined_envList ≝
+λd.λl:env_list d.match l with [ env_nil _ ⇒ False | env_cons _ _ _ ⇒ True ].
+
+definition cut_first_envList : Πd.env_list d → ? → env_list (pred d) ≝
+λd.λl:env_list d.λp:defined_envList ? l.
+ let value ≝
+ match l
+ return λX.λY:env_list X.defined_envList X Y → env_list (pred X)
+ with
+ [ env_nil h ⇒ λp:defined_envList O (env_nil h).False_rect ? p
+ | env_cons n h t ⇒ λp:defined_envList (S n) (env_cons n h t).t
+ ] p in value.
+
+definition get_first_envList ≝
+λd.λl:env_list d.
+ match l with
+ [ env_nil h ⇒ h
+ | env_cons _ h _ ⇒ h
+ ].
+
+lemma defined_envList_S :
+∀d.∀l:env_list (S d).defined_envList (S d) l.
+ intros;
+ inversion l;
+ [ intros; destruct H
+ | intros; simplify; apply I
+ ]
+qed.
+
+definition aux_env_type ≝ λd.env_list d.
(* getter *)
definition get_const_desc ≝ λd:desc_elem.match d with [ DESC_ELEM c _ ⇒ c ].
definition get_desc_var ≝ λv:var_elem.match v with [ VAR_ELEM _ d ⇒ d ].
(* ambiente vuoto *)
-definition empty_env ≝ ne_nil ? (nil var_elem ).
+definition empty_env ≝ env_nil [].
(* setter *)
-definition enter_env ≝ λe:aux_env_type.empty_env&e.
-definition leave_env ≝ λe:aux_env_type.cut_first_neList ? e.
+definition enter_env ≝ λd.λe:aux_env_type d.env_cons d [] e.
+definition leave_env ≝ λd.λe:aux_env_type (S d).cut_first_envList (S d) e (defined_envList_S ??).
(* recupera descrittore da ambiente: il primo trovato, ma e' anche l'unico *)
-let rec get_desc_from_lev_env (env:list var_elem ) (str:aux_str_type) on env ≝
+let rec get_desc_from_lev_env (env:list var_elem) (str:aux_str_type) on env ≝
match env with
[ nil ⇒ None ?
| cons h t ⇒ match eqStr_str str (get_name_var h) with
| false ⇒ get_desc_from_lev_env t str ]].
(* recupera descrittore da ambiente globale: il primo trovato *)
-let rec get_desc_env_aux (env:aux_env_type) (str:aux_str_type) on env ≝
+let rec get_desc_env_aux d (env:aux_env_type d) (str:aux_str_type) on env ≝
match env with
- [ ne_nil h ⇒ get_desc_from_lev_env h str
- | ne_cons h t ⇒ match get_desc_from_lev_env h str with
- [ None ⇒ get_desc_env_aux t str | Some res' ⇒ Some ? res' ]
+ [ env_nil h ⇒ get_desc_from_lev_env h str
+ | env_cons n h t ⇒ match get_desc_from_lev_env h str with
+ [ None ⇒ get_desc_env_aux n t str | Some res' ⇒ Some ? res' ]
].
-definition check_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
- match get_desc_env_aux e str with [ None ⇒ False | Some _ ⇒ True ].
+definition check_desc_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
+ match get_desc_env_aux d e str with [ None ⇒ False | Some _ ⇒ True ].
-definition checkb_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
- match get_desc_env_aux e str with [ None ⇒ false | Some _ ⇒ true ].
+definition checkb_desc_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
+ match get_desc_env_aux d e str with [ None ⇒ false | Some _ ⇒ true ].
-lemma checkbdescenv_to_checkdescenv : ∀e,str.checkb_desc_env e str = true → check_desc_env e str.
+lemma checkbdescenv_to_checkdescenv : ∀d.∀e:aux_env_type d.∀str.checkb_desc_env d e str = true → check_desc_env d e str.
unfold checkb_desc_env;
unfold check_desc_env;
intros;
- letin K ≝ (get_desc_env_aux e str);
+ letin K ≝ (get_desc_env_aux d e str);
elim K;
[ normalize; autobatch |
normalize; autobatch ]
qed.
-definition get_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
- match get_desc_env_aux e str with
+definition get_desc_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
+ match get_desc_env_aux d e str with
[ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
-definition check_not_already_def_env ≝ λe:aux_env_type.λstr:aux_str_type.
- match get_desc_from_lev_env (get_first_neList ? e) str with [ None ⇒ True | Some _ ⇒ False ].
+definition check_not_already_def_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
+ match get_desc_from_lev_env (get_first_envList d e) str with [ None ⇒ True | Some _ ⇒ False ].
-definition checkb_not_already_def_env ≝ λe:aux_env_type.λstr:aux_str_type.
- match get_desc_from_lev_env (get_first_neList ? e) str with [ None ⇒ true | Some _ ⇒ false ].
+definition checkb_not_already_def_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
+ match get_desc_from_lev_env (get_first_envList d e) str with [ None ⇒ true | Some _ ⇒ false ].
-lemma checkbnotalreadydefenv_to_checknotalreadydefenv : ∀e,str.checkb_not_already_def_env e str = true → check_not_already_def_env e str.
+lemma checkbnotalreadydefenv_to_checknotalreadydefenv : ∀d.∀e:aux_env_type d.∀str.checkb_not_already_def_env d e str = true → check_not_already_def_env d e str.
unfold checkb_not_already_def_env;
unfold check_not_already_def_env;
intros;
- letin K ≝ (get_desc_from_lev_env (get_first_neList ? e) str);
+ letin K ≝ (get_desc_from_lev_env (get_first_envList d e) str);
elim K;
[ normalize; autobatch |
normalize; autobatch ]
(* aggiungi descrittore ad ambiente globale: in testa al primo ambiente *)
definition add_desc_env ≝
-λe:aux_env_type.λstr:aux_str_type.λc:bool.λdesc:ast_type.
+λd.λe:aux_env_type d.λstr:aux_str_type.λc:bool.λdesc:ast_type.
(*let var ≝ VAR_ELEM str (DESC_ELEM c desc) in*)
- match e with
- [ ne_nil h ⇒ ne_nil ? ((VAR_ELEM str (DESC_ELEM c desc))::h)
- | ne_cons h tl ⇒ «£((VAR_ELEM str (DESC_ELEM c desc))::h)»&tl
+ match e
+ return λX.λe:aux_env_type X.aux_env_type X
+ with
+ [ env_nil h ⇒ env_nil ((VAR_ELEM str (DESC_ELEM c desc))::h)
+ | env_cons n h t ⇒ env_cons n ((VAR_ELEM str (DESC_ELEM c desc))::h) t
].
(* controllo e <= e' *)
(* operatore di cast *)
definition preast_to_ast_expr_check ≝
-λe:aux_env_type.λsig:(Σt'.ast_expr e t').λt:ast_type.
+λd.λe:aux_env_type d.λsig:(Σt'.ast_expr d e t').λt:ast_type.
match sig with [ sigma_intro t' expr ⇒
match eq_ast_type t' t
- return λx.eq_ast_type t' t = x → option (ast_expr e t)
+ return λx.eq_ast_type t' t = x → option (ast_expr d e t)
with
- [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_expr e t) expr t (eqasttype_to_eq ?? p))
+ [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_expr d e t) expr t (eqasttype_to_eq ?? p))
| false ⇒ λp:(eq_ast_type t' t = false).None ?
] (refl_eq ? (eq_ast_type t' t))
].
definition preast_to_ast_init_check ≝
-λe:aux_env_type.λsig:Σt'.ast_init e t'.λt:ast_type.
+λd.λe:aux_env_type d.λsig:Σt'.ast_init d e t'.λt:ast_type.
match sig with [ sigma_intro t' expr ⇒
match eq_ast_type t' t
- return λx.eq_ast_type t' t = x → option (ast_init e t)
+ return λx.eq_ast_type t' t = x → option (ast_init d e t)
with
- [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_init e t) expr t (eqasttype_to_eq ?? p))
+ [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_init d e t) expr t (eqasttype_to_eq ?? p))
| false ⇒ λp:(eq_ast_type t' t = false).None ?
] (refl_eq ? (eq_ast_type t' t))
].
definition preast_to_ast_var_checkb ≝
-λe:aux_env_type.λt:ast_type.λsig:(Σb'.ast_var e b' t).λb:bool.
+λd.λe:aux_env_type d.λt:ast_type.λsig:(Σb'.ast_var d e b' t).λb:bool.
match sig with [ sigma_intro b' var ⇒
match eq_bool b' b
- return λx.eq_bool b' b = x → option (ast_var e b t)
+ return λx.eq_bool b' b = x → option (ast_var d e b t)
with
- [ true ⇒ λp:(eq_bool b' b = true).Some ? (eq_rect ? b' (λb.ast_var e b t) var b (eqbool_to_eq ?? p))
+ [ true ⇒ λp:(eq_bool b' b = true).Some ? (eq_rect ? b' (λb.ast_var d e b t) var b (eqbool_to_eq ?? p))
| false ⇒ λp:(eq_bool b' b = false).None ?
] (refl_eq ? (eq_bool b' b))
].
definition preast_to_ast_var_checkt ≝
-λe:aux_env_type.λb:bool.λsig:(Σt'.ast_var e b t').λt:ast_type.
+λd.λe:aux_env_type d.λb:bool.λsig:(Σt'.ast_var d e b t').λt:ast_type.
match sig with [ sigma_intro t' var ⇒
match eq_ast_type t' t
- return λx.eq_ast_type t' t = x → option (ast_var e b t)
+ return λx.eq_ast_type t' t = x → option (ast_var d e b t)
with
- [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_var e b t) var t (eqasttype_to_eq ?? p))
+ [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_var d e b t) var t (eqasttype_to_eq ?? p))
| false ⇒ λp:(eq_ast_type t' t = false).None ?
] (refl_eq ? (eq_ast_type t' t))
].
definition preast_to_ast_var_check ≝
-λe:aux_env_type.λsig:(Σb'.(Σt'.ast_var e b' t')).λb:bool.λt:ast_type.
- opt_map ?? (preast_to_ast_var_checkt e (sigmaFst ?? sig) (sigmaSnd ?? sig) t)
- (λres1.opt_map ?? (preast_to_ast_var_checkb e t ≪(sigmaFst ?? sig),res1≫ b)
+λd.λe:aux_env_type d.λsig:(Σb'.(Σt'.ast_var d e b' t')).λb:bool.λt:ast_type.
+ opt_map ?? (preast_to_ast_var_checkt d e (sigmaFst ?? sig) (sigmaSnd ?? sig) t)
+ (λres1.opt_map ?? (preast_to_ast_var_checkb d e t ≪(sigmaFst ?? sig),res1≫ b)
(λres2.Some ? res2)).
(*
PREAST_EXPR_W32toW16: preast_expr → preast_expr
PREAST_EXPR_ID: preast_var → preast_expr
*)
-let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) on preast : option (Σt.ast_expr e t) ≝
+let rec preast_to_ast_expr (preast:preast_expr) (d:nat) (e:aux_env_type d) on preast : option (Σt.ast_expr d e t) ≝
match preast with
- [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪?,(AST_EXPR_BYTE8 e val)≫
- | PREAST_EXPR_WORD16 val ⇒ Some ? ≪?,(AST_EXPR_WORD16 e val)≫
- | PREAST_EXPR_WORD32 val ⇒ Some ? ≪?,(AST_EXPR_WORD32 e val)≫
+ [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪?,(AST_EXPR_BYTE8 d e val)≫
+ | PREAST_EXPR_WORD16 val ⇒ Some ? ≪?,(AST_EXPR_WORD16 d e val)≫
+ | PREAST_EXPR_WORD32 val ⇒ Some ? ≪?,(AST_EXPR_WORD32 d e val)≫
| PREAST_EXPR_NEG subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType))
- (λres.Some ? ≪?,(AST_EXPR_NEG e ? res)≫)
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType))
+ (λres.Some ? ≪?,(AST_EXPR_NEG d e ? res)≫)
| _ ⇒ None ? ])
| PREAST_EXPR_NOT subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType))
- (λres.Some ? ≪?,(AST_EXPR_NOT e ? res)≫)
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType))
+ (λres.Some ? ≪?,(AST_EXPR_NOT d e ? res)≫)
| _ ⇒ None ? ])
| PREAST_EXPR_COM subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType))
- (λres.Some ? ≪?,(AST_EXPR_COM e ? res)≫)
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType))
+ (λres.Some ? ≪?,(AST_EXPR_COM d e ? res)≫)
| _ ⇒ None ? ])
| PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes1) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
- (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
- (λres2.Some ? ≪?,(AST_EXPR_ADD e ? res1 res2)≫))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_ADD d e ? res1 res2)≫))
| _ ⇒ None ? ]))
| PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes1) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
- (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
- (λres2.Some ? ≪?,(AST_EXPR_SUB e ? res1 res2)≫))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_SUB d e ? res1 res2)≫))
| _ ⇒ None ? ]))
| PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes1) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
- (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
- (λres2.Some ? ≪?,(AST_EXPR_MUL e ? res1 res2)≫))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_MUL d e ? res1 res2)≫))
| _ ⇒ None ? ]))
| PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes1) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
- (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
- (λres2.Some ? ≪?,(AST_EXPR_DIV e ? res1 res2)≫))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_DIV d e ? res1 res2)≫))
| _ ⇒ None ? ]))
| PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes1) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
- (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
- (λres2.Some ? ≪?,(AST_EXPR_SHR e ? res1 res2)≫))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres2.Some ? ≪?,(AST_EXPR_SHR d e ? res1 res2)≫))
| _ ⇒ None ? ]))
| PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes1) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
- (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
- (λres2.Some ? ≪?,(AST_EXPR_SHL e ? res1 res2)≫))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres2.Some ? ≪?,(AST_EXPR_SHL d e ? res1 res2)≫))
| _ ⇒ None ? ]))
| PREAST_EXPR_GT subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes1) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
- (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
- (λres2.Some ? ≪?,(AST_EXPR_GT e ? res1 res2)≫))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_GT d e ? res1 res2)≫))
| _ ⇒ None ? ]))
| PREAST_EXPR_GTE subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes1) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
- (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
- (λres2.Some ? ≪?,(AST_EXPR_GTE e ? res1 res2)≫))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_GTE d e ? res1 res2)≫))
| _ ⇒ None ? ]))
| PREAST_EXPR_LT subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes1) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
- (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
- (λres2.Some ? ≪?,(AST_EXPR_LT e ? res1 res2)≫))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_LT d e ? res1 res2)≫))
| _ ⇒ None ? ]))
| PREAST_EXPR_LTE subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes1) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
- (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
- (λres2.Some ? ≪?,(AST_EXPR_LTE e ? res1 res2)≫))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_LTE d e ? res1 res2)≫))
| _ ⇒ None ? ]))
| PREAST_EXPR_EQ subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes1) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
- (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
- (λres2.Some ? ≪?,(AST_EXPR_EQ e ? res1 res2)≫))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_EQ d e ? res1 res2)≫))
| _ ⇒ None ? ]))
| PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
match (sigmaFst ?? sigmaRes1) with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
- (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
- (λres2.Some ? ≪?,(AST_EXPR_NEQ e ? res1 res2)≫))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_NEQ d e ? res1 res2)≫))
| _ ⇒ None ? ]))
| PREAST_EXPR_B8toW16 subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
- (λres.Some ? ≪?,(AST_EXPR_B8toW16 e res)≫))
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres.Some ? ≪?,(AST_EXPR_B8toW16 d e res)≫))
| PREAST_EXPR_B8toW32 subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
- (λres.Some ? ≪?,(AST_EXPR_B8toW32 e res)≫))
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres.Some ? ≪?,(AST_EXPR_B8toW32 d e res)≫))
| PREAST_EXPR_W16toB8 subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
- (λres.Some ? ≪?,(AST_EXPR_W16toB8 e res)≫))
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
+ (λres.Some ? ≪?,(AST_EXPR_W16toB8 d e res)≫))
| PREAST_EXPR_W16toW32 subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
- (λres.Some ? ≪?,(AST_EXPR_W16toW32 e res)≫))
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
+ (λres.Some ? ≪?,(AST_EXPR_W16toW32 d e res)≫))
| PREAST_EXPR_W32toB8 subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
- (λres.Some ? ≪?,(AST_EXPR_W32toB8 e res)≫))
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
+ (λres.Some ? ≪?,(AST_EXPR_W32toB8 d e res)≫))
| PREAST_EXPR_W32toW16 subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
- (λres.Some ? ≪?,(AST_EXPR_W32toW16 e res)≫))
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
+ (λres.Some ? ≪?,(AST_EXPR_W32toW16 d e res)≫))
| PREAST_EXPR_ID var ⇒
- opt_map ?? (preast_to_ast_var var e)
- (λsigmaRes:(Σb.(Σt.ast_var e b t)).
+ opt_map ?? (preast_to_ast_var var d e)
+ (λsigmaRes:(Σb.(Σt.ast_var d e b t)).
match sigmaRes with [ sigma_intro b sigmaRes' ⇒
match sigmaRes' with [ sigma_intro t _ ⇒
- opt_map ?? (preast_to_ast_var_check e sigmaRes b t)
- (λres.Some ? ≪?,(AST_EXPR_ID e ?? res)≫)]])
+ opt_map ?? (preast_to_ast_var_check d e sigmaRes b t)
+ (λres.Some ? ≪?,(AST_EXPR_ID d e ?? res)≫)]])
]
(*
PREAST_VAR_ID: aux_str_type → preast_var
PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
PREAST_VAR_STRUCT: preast_var → nat → preast_var
*)
-and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option (Σb.(Σt.ast_var e b t)) ≝
+and preast_to_ast_var (preast:preast_var) (d:nat) (e:aux_env_type d) on preast : option (Σb.(Σt.ast_var d e b t)) ≝
match preast with
[ PREAST_VAR_ID name ⇒
- match checkb_desc_env e name
- return λx.checkb_desc_env e name = x → option (Σb.(Σt.ast_var e b t))
+ match checkb_desc_env d e name
+ return λx.checkb_desc_env d e name = x → option (Σb.(Σt.ast_var d e b t))
with
- [ true ⇒ λp:(checkb_desc_env e name = true).
- let desc ≝ get_desc_env e name in
+ [ true ⇒ λp:(checkb_desc_env d e name = true).
+ let desc ≝ get_desc_env d e name in
let b ≝ get_const_desc desc in
let t ≝ get_type_desc desc in
- Some ? ≪b,≪t,(AST_VAR_ID e b t (AST_ID e name (checkbdescenv_to_checkdescenv e name p)))≫≫
- | false ⇒ λp:(checkb_desc_env e name = false).None ?
- ] (refl_eq ? (checkb_desc_env e name))
+ Some ? ≪b,≪t,(AST_VAR_ID d e b t (AST_ID d e name (checkbdescenv_to_checkdescenv d e name p)))≫≫
+ | false ⇒ λp:(checkb_desc_env d e name = false).None ?
+ ] (refl_eq ? (checkb_desc_env d e name))
| PREAST_VAR_ARRAY subVar expr ⇒
- opt_map ?? (preast_to_ast_var subVar e)
- (λsigmaResV:(Σb.(Σt.ast_var e b t)).
+ opt_map ?? (preast_to_ast_var subVar d e)
+ (λsigmaResV:(Σb.(Σt.ast_var d e b t)).
match sigmaResV with [ sigma_intro b sigmaResV' ⇒
match sigmaResV' with [ sigma_intro t _ ⇒
match t with
[ AST_TYPE_ARRAY subType dim ⇒
- opt_map ?? (preast_to_ast_var_check e sigmaResV b (AST_TYPE_ARRAY subType dim))
+ opt_map ?? (preast_to_ast_var_check d e sigmaResV b (AST_TYPE_ARRAY subType dim))
(λresVar.
(* ASSERTO:
1) se l'indice e' un'espressione riducibile ad un valore deve essere gia'
| PREAST_EXPR_WORD32 val ⇒ (λx.ltb (nat_of_word32 val) dim)
| _ ⇒ (λx.true) ]) expr with
[ true ⇒
- opt_map ?? (preast_to_ast_expr expr e)
- (λsigmaResE:(Σt.ast_expr e t).
+ opt_map ?? (preast_to_ast_expr expr d e)
+ (λsigmaResE:(Σt.ast_expr d e t).
match sigmaFst ?? sigmaResE with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaResE (AST_TYPE_BASE bType))
- (λresExpr.Some ? ≪b,≪subType,(AST_VAR_ARRAY e b subType dim resVar (AST_BASE_EXPR e bType resExpr))≫≫)
+ opt_map ?? (preast_to_ast_expr_check d e sigmaResE (AST_TYPE_BASE bType))
+ (λresExpr.Some ? ≪b,≪subType,(AST_VAR_ARRAY d e b subType dim resVar (AST_BASE_EXPR d e bType resExpr))≫≫)
| _ ⇒ None ? ])
| false ⇒ None ? ])
| _ ⇒ None ? ]]])
| PREAST_VAR_STRUCT subVar field ⇒
- opt_map ?? (preast_to_ast_var subVar e)
- (λsigmaRes:(Σb.(Σt.ast_var e b t)).
+ opt_map ?? (preast_to_ast_var subVar d e)
+ (λsigmaRes:(Σb.(Σt.ast_var d e b t)).
match sigmaRes with [ sigma_intro b sigmaRes' ⇒
match sigmaRes' with [ sigma_intro t _ ⇒
match t with
[ AST_TYPE_STRUCT nelSubType ⇒
- opt_map ?? (preast_to_ast_var_check e sigmaRes b (AST_TYPE_STRUCT nelSubType))
+ opt_map ?? (preast_to_ast_var_check d e sigmaRes b (AST_TYPE_STRUCT nelSubType))
(λresVar.
match ltb field (len_neList ? nelSubType)
- return λx.(ltb field (len_neList ? nelSubType) = x) → option (Σb.(Σt.ast_var e b t))
+ return λx.(ltb field (len_neList ? nelSubType) = x) → option (Σb.(Σt.ast_var d e b t))
with
[ true ⇒ λp:(ltb field (len_neList ? nelSubType) = true).
- Some ? ≪b,≪(abs_nth_neList ? nelSubType field),(AST_VAR_STRUCT e b nelSubType field resVar p)≫≫
+ Some ? ≪b,≪(abs_nth_neList ? nelSubType field),(AST_VAR_STRUCT d e b nelSubType field resVar p)≫≫
| false ⇒ λp:(ltb field (len_neList ? nelSubType) = false).None ?
] (refl_eq ? (ltb field (len_neList ? nelSubType)))
)
PREAST_INIT_VAR: preast_var → preast_init
PREAST_INIT_VAL: preast_init_val → preast_init
*)
-definition preast_to_ast_init : preast_init → Πe.option (Σt.ast_init e t) ≝
-λpreast:preast_init.λe:aux_env_type.match preast with
+definition preast_to_ast_init : preast_init → Πd.Πe:aux_env_type d.option (Σt.ast_init d e t) ≝
+λpreast:preast_init.λd.λe:aux_env_type d.match preast with
[ PREAST_INIT_VAR var ⇒
- opt_map ?? (preast_to_ast_var var e)
- (λsigmaRes:(Σb.(Σt.ast_var e b t)).
- Some ? ≪?,(AST_INIT_VAR e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫)
+ opt_map ?? (preast_to_ast_var var d e)
+ (λsigmaRes:(Σb.(Σt.ast_var d e b t)).
+ Some ? ≪?,(AST_INIT_VAR d e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫)
| PREAST_INIT_VAL val ⇒
opt_map ?? (preast_to_ast_init_val_aux val)
(λsigmaRes:(Σt.aux_ast_init_type t).
- Some ? ≪?,(AST_INIT_VAL e ? (sigmaSnd ?? sigmaRes))≫)
+ Some ? ≪?,(AST_INIT_VAL d e ? (sigmaSnd ?? sigmaRes))≫)
].
(*
PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
*)
-definition preast_to_ast_base_expr : preast_expr → Πe.option (ast_base_expr e) ≝
-λpreast:preast_expr.λe:aux_env_type.
- opt_map ?? (preast_to_ast_expr preast e)
- (λsigmaRes:(Σt.ast_expr e t).
+definition preast_to_ast_base_expr : preast_expr → Πd.Πe:aux_env_type d.option (ast_base_expr d e) ≝
+λpreast:preast_expr.λd.λe:aux_env_type d.
+ opt_map ?? (preast_to_ast_expr preast d e)
+ (λsigmaRes:(Σt.ast_expr d e t).
match sigmaFst ?? sigmaRes with
[ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType))
- (λres.Some ? (AST_BASE_EXPR e ? res))
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType))
+ (λres.Some ? (AST_BASE_EXPR d e ? res))
| _ ⇒ None ? ]).
-let rec preast_to_ast_stm (preast:preast_stm) (e:aux_env_type) on preast : option (ast_stm e) ≝
+let rec preast_to_ast_stm (preast:preast_stm) (d:nat) (e:aux_env_type d) on preast : option (ast_stm d e) ≝
match preast with
[ PREAST_STM_ASG var expr ⇒
- opt_map ?? (preast_to_ast_var var e)
- (λsigmaResV:(Σb.(Σt.ast_var e b t)).
+ opt_map ?? (preast_to_ast_var var d e)
+ (λsigmaResV:(Σb.(Σt.ast_var d e b t)).
match sigmaResV with [ sigma_intro _ sigmaResV' ⇒
match sigmaResV' with [ sigma_intro t _ ⇒
- opt_map ?? (preast_to_ast_var_check e sigmaResV false t)
- (λresVar.opt_map ?? (preast_to_ast_expr expr e)
- (λsigmaResE:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaResE t)
- (λresExpr.Some ? (AST_STM_ASG e t resVar resExpr)
+ opt_map ?? (preast_to_ast_var_check d e sigmaResV false t)
+ (λresVar.opt_map ?? (preast_to_ast_expr expr d e)
+ (λsigmaResE:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaResE t)
+ (λresExpr.Some ? (AST_STM_ASG d e t resVar resExpr)
)))]])
| PREAST_STM_WHILE expr decl ⇒
- opt_map ?? (preast_to_ast_base_expr expr e)
- (λresExpr.opt_map ?? (preast_to_ast_decl decl (enter_env e))
- (λresDecl.Some ? (AST_STM_WHILE e resExpr resDecl)))
+ opt_map ?? (preast_to_ast_base_expr expr d e)
+ (λresExpr.opt_map ?? (preast_to_ast_decl decl (S d) (enter_env d e))
+ (λresDecl.Some ? (AST_STM_WHILE d e resExpr resDecl)))
| PREAST_STM_IF nelExprDecl optDecl ⇒
- opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (preast_to_ast_base_expr (fst ?? h) e)
- (λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) (enter_env e))
+ opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (preast_to_ast_base_expr (fst ?? h) d e)
+ (λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) (S d) (enter_env d e))
(λresDecl.opt_map ?? t
(λt'.Some ? («£(pair ?? resExpr resDecl)»&t')))))
- (Some ? (ne_nil ? (pair ?? (AST_BASE_EXPR e AST_BASE_TYPE_BYTE8 (AST_EXPR_BYTE8 e 〈x0,x0〉)) (AST_NO_DECL (enter_env e) (nil ?)))))
+ (Some ? (ne_nil ? (pair ?? (AST_BASE_EXPR d e AST_BASE_TYPE_BYTE8 (AST_EXPR_BYTE8 d e 〈x0,x0〉)) (AST_NO_DECL (S d) (enter_env d e) (nil ?)))))
nelExprDecl)
(λres.match optDecl with
- [ None ⇒ Some ? (AST_STM_IF e (cut_last_neList ? res) (None ?))
- | Some decl ⇒ opt_map ?? (preast_to_ast_decl decl (enter_env e))
- (λresDecl.Some ? (AST_STM_IF e (cut_last_neList ? res) (Some ? resDecl)))
+ [ None ⇒ Some ? (AST_STM_IF d e (cut_last_neList ? res) (None ?))
+ | Some decl ⇒ opt_map ?? (preast_to_ast_decl decl (S d) (enter_env d e))
+ (λresDecl.Some ? (AST_STM_IF d e (cut_last_neList ? res) (Some ? resDecl)))
])
]
(*
PREAST_NO_DECL: list preast_stm → preast_decl
PREAST_DECL: bool → aux_str_type → ast_type → option preast_init → preast_decl → preast_decl
*)
-and preast_to_ast_decl (preast:preast_decl) (e:aux_env_type) on preast : option (ast_decl e) ≝
+and preast_to_ast_decl (preast:preast_decl) (d:nat) (e:aux_env_type d) on preast : option (ast_decl d e) ≝
match preast with
[ PREAST_NO_DECL lPreastStm ⇒
- opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (preast_to_ast_stm h e)
+ opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (preast_to_ast_stm h d e)
(λh'.opt_map ?? t
(λt'.Some ? ([h']@t')))) (Some ? (nil ?)) lPreastStm)
- (λres.Some ? (AST_NO_DECL e res))
+ (λres.Some ? (AST_NO_DECL d e res))
| PREAST_DECL constFlag decName decType optInitExpr subPreastDecl ⇒
- match checkb_not_already_def_env e decName
- return λx.(checkb_not_already_def_env e decName = x) → option (ast_decl e)
+ match checkb_not_already_def_env d e decName
+ return λx.(checkb_not_already_def_env d e decName = x) → option (ast_decl d e)
with
- [ true ⇒ λp:(checkb_not_already_def_env e decName = true).
- opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag decType))
+ [ true ⇒ λp:(checkb_not_already_def_env d e decName = true).
+ opt_map ?? (preast_to_ast_decl subPreastDecl d (add_desc_env d e decName constFlag decType))
(λdecl.match optInitExpr with
- [ None ⇒ Some ? (AST_DECL e constFlag decName decType
- (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p) (None ?) decl)
+ [ None ⇒ Some ? (AST_DECL d e constFlag decName decType
+ (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (None ?) decl)
| Some initExpr ⇒
- opt_map ?? (preast_to_ast_init initExpr e)
- (λsigmaRes:(Σt:ast_type.ast_init e t).opt_map ?? (preast_to_ast_init_check e sigmaRes decType)
- (λresInit.Some ? (AST_DECL e constFlag decName decType
- (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p) (Some ? resInit) decl)))])
- | false ⇒ λp:(checkb_not_already_def_env e decName = false).None ?
- ] (refl_eq ? (checkb_not_already_def_env e decName))
+ opt_map ?? (preast_to_ast_init initExpr d e)
+ (λsigmaRes:(Σt:ast_type.ast_init d e t).opt_map ?? (preast_to_ast_init_check d e sigmaRes decType)
+ (λresInit.Some ? (AST_DECL d e constFlag decName decType
+ (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (Some ? resInit) decl)))])
+ | false ⇒ λp:(checkb_not_already_def_env d e decName = false).None ?
+ ] (refl_eq ? (checkb_not_already_def_env d e decName))
].
(*
*)
definition preast_to_ast ≝
λpreast:preast_root.match preast with
- [ PREAST_ROOT decl ⇒ opt_map ?? (preast_to_ast_decl decl empty_env)
+ [ PREAST_ROOT decl ⇒ opt_map ?? (preast_to_ast_decl decl O empty_env)
(λres.Some ? (AST_ROOT res)) ].
-
-(* mini test
-definition prova ≝
-PREAST_ROOT (
- PREAST_DECL true [ ch_Q ] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (None ?) (
- PREAST_NO_DECL [
- PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x0,x0〉) (
- PREAST_DECL false [ ch_P ] (AST_TYPE_STRUCT «(AST_TYPE_BASE AST_BASE_TYPE_WORD16)£(AST_TYPE_BASE AST_BASE_TYPE_BYTE8)») (None ?) (
- PREAST_NO_DECL [
- PREAST_STM_ASG (PREAST_VAR_STRUCT (PREAST_VAR_ID [ ch_P ]) 1) (PREAST_EXPR_ID (PREAST_VAR_ARRAY (PREAST_VAR_ID [ ch_Q ]) (PREAST_EXPR_BYTE8 〈x0,x1〉)))
- ]
- )
- )
- ]
- )
-).
-
-lemma checkprova : None ? = preast_to_ast prova.
-normalize;
-*)
projects / helm.git / commitdiff