(* ********************************************************************** *)
include "compiler/astfe_tree.ma".
+include "compiler/sigma.ma".
(* ************************ *)
(* PASSO 2 : da AST a ASTFE *)
(* ************************ *)
(* operatore di cast *)
-definition ast_to_astfe_expr_check : Πt.astfe_expr t → Πt'.option (astfe_expr t') ≝
-λt:ast_type.λast:astfe_expr t.λt':ast_type.
+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 t) ast t' (eqasttype_to_eq ?? p))
+ 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 : Πt.astfe_init t → Πt'.option (astfe_init t') ≝
-λt:ast_type.λast:astfe_init t.λt':ast_type.
+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 t) ast t' (eqasttype_to_eq ?? p))
+ 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 : Πb.Πt.astfe_var b t → Πb'.option (astfe_var b' t) ≝
-λb:bool.λt:ast_type.λast:astfe_var b t.λb':bool.
+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 b t) ast b' (eqbool_to_eq ?? p))
+ 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 : Πb.Πt.astfe_var b t → Πt'.option (astfe_var b t') ≝
-λb:bool.λt:ast_type.λast:astfe_var b t.λt':ast_type.
+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 b t) ast t' (eqasttype_to_eq ?? p))
+ 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 : Πb.Πt.astfe_var b t → Πb'.Πt'.option (astfe_var b' t') ≝
-λb:bool.λt:ast_type.λast:astfe_var b t.λb':bool.λt':ast_type.
- opt_map ?? (ast_to_astfe_var_checkb b t ast b')
- (λres.opt_map ?? (ast_to_astfe_var_checkt b' t res 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 ast_to_astfe_id ≝
-λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.λmap:aux_trasfMap_type.match ast with
- [ AST_ID str _ ⇒ ASTFE_ID (name_to_nameId map str) b t ].
+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 ].
+
+(* 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_ax:
+ Π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.
+ check_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)).
+
+(*
+axiom ax2:
+ Π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.
+ get_const_desc
+ (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))
+ = b.
+
+axiom ax3:
+ Π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.
+ get_type_desc
+ (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))) = t.
+*)
+
+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)))).
+ apply
+ (λ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)) ?);
+ apply ast_to_astfe_id_ax.
+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) (map:aux_trasfMap_type) on ast : option (astfe_expr 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 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 val) t
- | AST_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 val) t
- | AST_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 val) t
+ [ 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 map)
- (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG bType res) t)
+ 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 map)
- (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT bType res) t)
+ 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 map)
- (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_COM bType res) t)
+ 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 map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
- (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD bType res1 res2) t))
+ 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 map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
- (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB bType res1 res2) t))
+ 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 map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
- (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL bType res1 res2) t))
+ 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 map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
- (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV bType res1 res2) t))
+ 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 map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 map)
- (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR bType res1 res2) t))
+ 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 map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 map)
- (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL bType res1 res2) t))
+ 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 map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
- (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT bType res1 res2) t))
+ 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 map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
- (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE bType res1 res2) t))
+ 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 map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
- (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT bType res1 res2) t))
+ 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 map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
- (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE bType res1 res2) t))
+ 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 map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
- (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ bType res1 res2) t))
+ 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 map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
- (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ bType res1 res2) t))
+ 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 map)
- (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 res) t)
+ 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 map)
- (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 res) t)
+ 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 map)
- (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 res) t)
+ 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 map)
- (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 res) t)
+ 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 map)
- (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 res) t)
+ 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 map)
- (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 res) t)
+ 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 map)
- (λres.ast_to_astfe_expr_check subType (ASTFE_EXPR_ID b subType res) t)
+ 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)
]
(*
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) (map:aux_trasfMap_type) on ast : option (astfe_var b t) ≝
+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 ⇒ ast_to_astfe_var_check subB subType (ASTFE_VAR_ID subB subType (ast_to_astfe_id e subB subType subId map)) b t
+ [ 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 map)
- (λresVar.opt_map ?? (ast_to_astfe_base_expr e expr map)
- (λresExpr.ast_to_astfe_var_check subB subType (ASTFE_VAR_ARRAY subB subType dim resVar resExpr) b t))
+ 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 map)
- (λres.ast_to_astfe_var_check subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT subB nelSubType field res) b t)
+ 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)
]
(*
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) (map:aux_trasfMap_type) on ast : option astfe_base_expr ≝
+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 map)
- (λres.Some ? (ASTFE_BASE_EXPR bType res))
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
+ (λres.Some ? (ASTFE_BASE_EXPR fe bType res))
].
(*
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 → aux_trasfMap_type → option (astfe_init t) ≝
-λe:aux_env_type.λt:ast_type.λast:ast_init e t.λmap:aux_trasfMap_type.match ast with
- [ AST_INIT_VAR subB subType var ⇒
- opt_map ?? (ast_to_astfe_var e subB subType var map)
- (λres.ast_to_astfe_init_check subType (ASTFE_INIT_VAR subB subType res) 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)
- | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check subType (ASTFE_INIT_VAL subType args) t
- ].
+ | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe subType (ASTFE_INIT_VAL fe subType args) t
+ ].
(*
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) (map:aux_trasfMap_type) (fe:aux_flatEnv_type) on ast : option (Prod3T astfe_stm aux_trasfMap_type aux_flatEnv_type) ≝
- match ast with
+(* NB: il lemma dovrebbe poi prendere in input la dimostrazione che fe <= fe', cosi' ha senso *)
+axiom retype_base_expr: ∀fe,fe'.astfe_base_expr fe → astfe_base_expr fe'.
+axiom retype_init: ∀t,fe,fe'.astfe_init fe t → astfe_init fe' t.
+axiom retype_list_decl: ∀fe,fe'.list (astfe_stm fe) → list (astfe_stm fe').
+axiom retype_neList_body: ∀fe,fe'.ne_list (Prod (astfe_base_expr fe) (astfe_body fe)) → ne_list (Prod (astfe_base_expr fe') (astfe_body fe')).
+
+(* 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.
+
+axiom how_to_build_it : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:aux_env_type → aux_env_type.∀map:aux_trasfMap_type (f e) fe.∀ll:list (astfe_stm fe).
+ (sigma (aux_env_type\to aux_env_type)
+ (\lambda f:(aux_env_type\to aux_env_type).
+ (sigma aux_flatEnv_type
+ (\lambda fe':aux_flatEnv_type.
+ (Prod (aux_trasfMap_type (f e) fe') (list (astfe_stm fe'))))))).
+
+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')) ≝
+ 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'))
+ with
[ AST_STM_ASG e' subType var expr ⇒
- opt_map ?? (ast_to_astfe_var e' false subType var map)
- (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr map)
- (λresExpr.Some ? (tripleT ??? (ASTFE_STM_ASG subType resVar resExpr) map fe)))
+ λ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 ⇒
- opt_map ?? (ast_to_astfe_base_expr e' expr map)
- (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl map fe)
- (λtripleRes.match tripleRes with
- [ tripleT resDecl map' fe' ⇒
- Some ? (tripleT ??? (ASTFE_STM_WHILE resExpr (ASTFE_BODY resDecl)) (rollback_map map' (build_snapshot map)) fe')
- ]))
+ λ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 (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
+ [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+ [ sigma_intro fe' mapAndStm ⇒ match mapAndStm with
+ [ pair map' resDecl ⇒
+ Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map)
+ (ASTFE_STM_WHILE fe' (retype_base_expr fe fe' resExpr) (ASTFE_BODY fe' resDecl))≫)
+ ]]]))
| AST_STM_IF e' nelExprDecl optDecl ⇒
- let rec aux (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e'))))
- (m:aux_trasfMap_type) (flatE:aux_flatEnv_type) on nel ≝
- match nel with
- [ ne_nil h ⇒
- opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) m)
- (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) m flatE)
- (λtripleRes.match tripleRes with
- [ tripleT resDecl m' flatE' ⇒
- Some ? (tripleT ??? « pair ?? resExpr (ASTFE_BODY resDecl) £» (rollback_map m' (build_snapshot m)) flatE')
- ]))
- | ne_cons h tl ⇒
- opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) m)
- (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) m flatE)
- (λtripleRes.match tripleRes with
- [ tripleT resDecl m' flatE' ⇒
- opt_map ?? (aux tl (rollback_map m' (build_snapshot m)) flatE')
- (λtripleRes'.match tripleRes' with
- [ tripleT tl' m'' flatE'' ⇒
- Some ? (tripleT ??? (« pair ?? resExpr (ASTFE_BODY resDecl) £»&tl') m'' flatE'')
- ])]))] in
- opt_map ?? (aux nelExprDecl map fe)
- (λtRes.match tRes with
- [ tripleT resNel resMap resFe ⇒
- match optDecl with
- [ None ⇒ Some ? (tripleT ??? (ASTFE_STM_IF resNel (None ?)) resMap resFe)
- | Some decl ⇒
- opt_map ?? (ast_to_astfe_decl (enter_env e') decl resMap resFe)
- (λtRes'.match tRes' with
- [ tripleT rDecl resMap' resFe' ⇒
- Some ? (tripleT ??? (ASTFE_STM_IF resNel (Some ? (ASTFE_BODY rDecl))) (rollback_map resMap' (build_snapshot resMap)) resFe')
- ])
- ]])
+ λ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 (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
+ [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+ [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
+ [ pair m' resDecl ⇒
+ Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m)
+ « pair ?? (retype_base_expr fenv fenv' resExpr) (ASTFE_BODY fenv' resDecl) £»≫)
+ ]]]))
+
+ | 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 (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
+ [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+ [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type (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' ⇒
+ Some ? (≪fenv'',pair ?? m''
+ (« pair ?? (retype_base_expr fenv fenv'' resExpr)
+ (ASTFE_BODY fenv'' (retype_list_decl fenv' fenv'' resDecl)) £»&tl')≫)
+ ]])]]]))
+ ] 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 (f' (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with
+ [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+ [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type (f (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with
+ [ pair (m'':aux_trasfMap_type (f (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒
+ 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'' (retype_neList_body fe' fe'' resNel) (Some ? (ASTFE_BODY fe'' resDecl)))≫)
+ ]]])]]])
]
(*
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) (map:aux_trasfMap_type) (fe:aux_flatEnv_type) on ast : option (Prod3T (list astfe_stm) aux_trasfMap_type aux_flatEnv_type) ≝
- match ast with
+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.(Σfe'.Prod (aux_trasfMap_type (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 (f e') fe') (list (astfe_stm fe'))))
+ with
[ AST_NO_DECL e' lStm ⇒
- let rec aux (ll:list (ast_stm e')) (m:aux_trasfMap_type) (flatE:aux_flatEnv_type) on ll ≝
- match ll with
- [ nil ⇒ Some ? (tripleT ??? [] m flatE)
- | cons h tl ⇒
- opt_map ?? (ast_to_astfe_stm e' h m flatE)
- (λtripleRes.match tripleRes with
- [ tripleT resStm m' flatE' ⇒
- opt_map ?? (aux tl m' flatE')
- (λtripleRes'.match tripleRes' with
- [ tripleT tl' m'' flatE'' ⇒
- Some ? (tripleT ??? ([ resStm ]@tl') m'' flatE'')
- ])])] in
- aux lStm map fe
+ λ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 (f e') fe') (list (astfe_stm fe')))) ≝
+ match ll with
+ [ nil ⇒ Some ? (how_to_build_it e' fenv (λx.x) (retype_map_to_id e' fenv (λx.x) m (refl_eq ??)) [])
+ | 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 (f e') fe') (list (astfe_stm fe')))).match sigmaRes' with
+ [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type (f e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
+ [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type (f e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with
+ [ pair m'' tl' ⇒
+ Some ? (how_to_build_it e' fenv'' f m''
+ ((retype_list_decl fenv' fenv'' [ resStm ])@tl'))
+ ]]])]])] in
+ aux lStm fe map
| AST_DECL e' b name t _ optInit subDecl ⇒
- opt_map ?? (match optInit with
- [ None ⇒ Some ? [] | Some init ⇒ opt_map ?? (ast_to_astfe_init e' t init map)
- (λresInit.Some ? [ ASTFE_STM_INIT b t (ASTFE_ID (name_to_nameId (add_maxcur_map map name) name) b t) resInit ])])
- (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl (add_maxcur_map map name) (add_desc_flatEnv fe (name_to_nameId (add_maxcur_map map name) name) b t))
- (λtripleRes.match tripleRes with
- [ tripleT tRes resMap resFe ⇒
- Some ? (tripleT ??? (hRes@tRes) resMap resFe)
- ]))
+ λ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)
+ (False_rect ? daemon))
+ b t)
+ (λresId.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
+ b t resId
+ (retype_init t fe (add_desc_flatEnv fe (next_nameId e' fe map name) b t) 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 (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 (f (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
+ [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type (f (add_desc_env e' name b t)) fe') (list (astfe_stm fe'))) ⇒ match mapAndStm with
+ [ pair map' tRes ⇒
+ Some ? (how_to_build_it e' fe' (λx.f (add_desc_env x name b t)) map'
+ ((retype_list_decl (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' hRes)@tRes))
+ ]]]))
].
(*
AST_ROOT: ast_decl empty_env → ast_root.
*)
-definition ast_to_astfe ≝
+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_trasfMap empty_flatEnv 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_astfe_prog
- | Some x ⇒ ASTFE_ROOT (thd3T ??? x) (ASTFE_BODY (fst3T ??? x))
- ]
- ].
+ [ None ⇒ ≪empty_flatEnv,empty_astfe_prog≫
+ | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (f empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with
+ [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+ [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type (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".
(* **************************** *)
(* id: accesso all'ambiente con stringa *)
-inductive astfe_id : bool → ast_type → Type ≝
- ASTFE_ID: ∀str:aux_strId_type.∀b:bool.∀t:ast_type.
- astfe_id b t.
+inductive astfe_id (e:aux_flatEnv_type) : bool → ast_type → Type ≝
+ ASTFE_ID: ∀str:aux_strId_type.
+ (* D *) check_desc_flatEnv e str → astfe_id e (get_const_desc (get_desc_flatEnv e str)) (get_type_desc (get_desc_flatEnv e str)).
(* -------------------------- *)
(* espressioni *)
-inductive astfe_expr : ast_type → Type ≝
- ASTFE_EXPR_BYTE8 : byte8 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
-| ASTFE_EXPR_WORD16: word16 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
-| ASTFE_EXPR_WORD32: word32 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+inductive astfe_expr (e:aux_flatEnv_type) : ast_type → Type ≝
+ ASTFE_EXPR_BYTE8 : byte8 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_WORD16: word16 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| ASTFE_EXPR_WORD32: word32 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
| ASTFE_EXPR_NEG: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
| ASTFE_EXPR_NOT: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
| ASTFE_EXPR_COM: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
| ASTFE_EXPR_ADD: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
| ASTFE_EXPR_SUB: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
| ASTFE_EXPR_MUL: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
| ASTFE_EXPR_DIV: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
| ASTFE_EXPR_SHR: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE t)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t)
| ASTFE_EXPR_SHL: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE t)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t)
| ASTFE_EXPR_GT : ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
| ASTFE_EXPR_GTE: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
| ASTFE_EXPR_LT : ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
| ASTFE_EXPR_LTE: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
| ASTFE_EXPR_EQ : ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
| ASTFE_EXPR_NEQ: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
-| ASTFE_EXPR_B8toW16 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
-| ASTFE_EXPR_B8toW32 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
-| ASTFE_EXPR_W16toB8 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
-| ASTFE_EXPR_W16toW32: astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
-| ASTFE_EXPR_W32toB8 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
-| ASTFE_EXPR_W32toW16: astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| ASTFE_EXPR_B8toW16 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| ASTFE_EXPR_B8toW32 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| ASTFE_EXPR_W16toB8 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_W16toW32: astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| ASTFE_EXPR_W32toB8 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_W32toW16: astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
| ASTFE_EXPR_ID: ∀b:bool.∀t:ast_type.
- astfe_var b t → astfe_expr t
+ astfe_var e b t → astfe_expr e t
(* variabile: modificatori di array/struct dell'id *)
with astfe_var : bool → ast_type → Type ≝
ASTFE_VAR_ID: ∀b:bool.∀t:ast_type.
- astfe_id b t → astfe_var b t
+ astfe_id e b t → astfe_var e b t
| ASTFE_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
- astfe_var b (AST_TYPE_ARRAY t n) → astfe_base_expr → astfe_var b t
+ astfe_var e b (AST_TYPE_ARRAY t n) → astfe_base_expr e → astfe_var e b t
| ASTFE_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
- astfe_var b (AST_TYPE_STRUCT nel) → astfe_var b (abs_nth_neList ? nel n)
+ astfe_var e b (AST_TYPE_STRUCT nel) → astfe_var e b (abs_nth_neList ? nel n)
(* espressioni generalizzate: anche non uniformi per tipo *)
with astfe_base_expr : Type ≝
ASTFE_BASE_EXPR: ∀t:ast_base_type.
- astfe_expr (AST_TYPE_BASE t) → astfe_base_expr.
+ astfe_expr e (AST_TYPE_BASE t) → astfe_base_expr e.
(* -------------------------- *)
1) var1 = var2
2) var = ... valori ...
*)
-inductive astfe_init : ast_type → Type ≝
+inductive astfe_init (e:aux_flatEnv_type) : ast_type → Type ≝
ASTFE_INIT_VAR: ∀b:bool.∀t:ast_type.
- astfe_var b t → astfe_init t
+ astfe_var e b t → astfe_init e t
| ASTFE_INIT_VAL: ∀t:ast_type.
- aux_ast_init_type t → astfe_init t.
+ aux_ast_init_type t → astfe_init e t.
(* -------------------------- *)
(* statement: assegnamento/while/if else if else + conversione di dichiarazione *)
-inductive astfe_stm : Type ≝
+inductive astfe_stm (e:aux_flatEnv_type) : Type ≝
ASTFE_STM_ASG: ∀t:ast_type.
- astfe_var false t → astfe_expr t → astfe_stm
+ astfe_var e false t → astfe_expr e t → astfe_stm e
| ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
- astfe_id b t → astfe_init t → astfe_stm
-| ASTFE_STM_WHILE: astfe_base_expr → astfe_body → astfe_stm
-| ASTFE_STM_IF: ne_list (Prod astfe_base_expr astfe_body) → option astfe_body → astfe_stm
+ 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
(* dichiarazioni *)
with astfe_body : Type ≝
- ASTFE_BODY: list astfe_stm → astfe_body.
+ ASTFE_BODY: list (astfe_stm e) → astfe_body e.
(* -------------------------- *)
(* programma *)
-inductive astfe_root : Type ≝
- ASTFE_ROOT: aux_flatEnv_type → astfe_body → astfe_root.
+inductive astfe_root (e:aux_flatEnv_type) : Type ≝
+ ASTFE_ROOT: astfe_body e → astfe_root e.
(* -------------------------- *)
(* programma vuoto *)
-definition empty_astfe_prog ≝ ASTFE_ROOT empty_flatEnv (ASTFE_BODY (nil ?)).
+definition empty_astfe_prog ≝ ASTFE_ROOT empty_flatEnv (ASTFE_BODY empty_flatEnv (nil ?)).
(* ambiente vuoto *)
definition empty_flatEnv ≝ nil flatVar_elem.
+(* 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 strCmp_strId str (get_nameId_flatVar h) with
+ [ true ⇒ Some ? (get_desc_flatVar h)
+ | false ⇒ get_desc_flatEnv_aux tl str ]].
+
+definition get_desc_flatEnv ≝
+λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux e 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 checkb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux e str with [ None ⇒ false | Some _ ⇒ true ].
+
+lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str = true → check_desc_flatEnv e str.
+ unfold checkb_desc_flatEnv;
+ unfold check_desc_flatEnv;
+ intros;
+ letin K ≝ (get_desc_flatEnv_aux e str);
+ elim K;
+ [ normalize; autobatch |
+ normalize; autobatch ]
+qed.
+
+(* aggiungi descrittore ad ambiente: in testa *)
+definition add_desc_flatEnv ≝
+λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
+ (VAR_FLAT_ELEM str (DESC_ELEM b t))::e.
+
(* STRUTTURA MAPPA TRASFORMAZIONE *)
-(* elemento: nome + max + cur *)
-inductive maxCur_elem : Type ≝
-MAX_CUR_ELEM: aux_str_type → nat → nat → maxCur_elem.
+(* 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.
(* tipo pubblico *)
-definition aux_trasfMap_type ≝ list maxCur_elem.
+definition aux_trasfMap_type ≝ λe,fe.list (maxCur_elem e fe).
(* getter *)
-definition get_name_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM n _ _ ⇒ n ].
-definition get_max_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM _ m _ ⇒ m ].
-definition get_cur_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM _ _ c ⇒ c ].
+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 ].
(* mappa di trasformazione vuota *)
-definition empty_trasfMap ≝ nil maxCur_elem.
+definition empty_trasfMap ≝ λe,fe.nil (maxCur_elem e fe).
(* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *)
(* recupera descrittore da mappa trasformazione : dummy se non esiste (impossibile) *)
-let rec get_maxcur_from_map_aux (map:aux_trasfMap_type) (str:aux_str_type) (dummy:option maxCur_elem) on map ≝
+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 ≝
match map with
- [ nil ⇒ dummy
- | cons h tl ⇒ match strCmp_str str (get_name_maxCur h) with
- [ true ⇒ Some ? h | false ⇒ get_maxcur_from_map_aux tl str dummy ]].
-
-definition get_maxcur_from_map ≝
-λmap:aux_trasfMap_type.λstr:aux_str_type.
- match get_maxcur_from_map_aux map str (None ?) with
- [ None ⇒ MAX_CUR_ELEM str 0 0 | Some x ⇒ x ].
-
-(* aggiungi/aggiorna descrittore mappa trasformazione *)
-let rec add_maxcur_map_aux (map:aux_trasfMap_type) (str:aux_str_type) (flag:bool) on map ≝
- match map with
- [ nil ⇒ match flag with
- [ true ⇒ []
- | false ⇒ [MAX_CUR_ELEM str 0 0]
- ]
- | cons h tl ⇒ match strCmp_str str (get_name_maxCur h) with
- [ true ⇒ [MAX_CUR_ELEM str (S (get_max_maxCur h)) (S (get_max_maxCur h))]@(add_maxcur_map_aux tl str true)
- | false ⇒ [h]@(add_maxcur_map_aux tl str flag)
- ]
+ [ nil ⇒ None ?
+ | cons h tl ⇒ match strCmp_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))
].
-definition add_maxcur_map ≝
-λmap:aux_trasfMap_type.λstr:aux_str_type.add_maxcur_map_aux map str false.
-
(* nome -> nome + id *)
definition name_to_nameId ≝
-λmap:aux_trasfMap_type.λstr:aux_str_type.
- STR_ID str (get_cur_maxCur (get_maxcur_from_map map str)).
-
-(* recupera descrittore da ambiente : dummy se non esiste (impossibile) *)
-let rec get_desc_from_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) (dummy:option desc_elem) on e ≝
-match e with
- [ nil ⇒ dummy
- | cons h tl ⇒ match strCmp_strId str (get_nameId_flatVar h) with
- [ true ⇒ Some ? (get_desc_flatVar h)
- | false ⇒ get_desc_from_flatEnv_aux tl str dummy ]].
-
-definition get_desc_from_flatEnv ≝
-λe:aux_flatEnv_type.λstr:aux_strId_type.
- match get_desc_from_flatEnv_aux e str (None ?) with
- [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
-
-(* aggiungi descrittore ad ambiente *)
-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) ].
-
-(* snapshot della mappa trasformazione *)
-let rec build_snapshot (map:aux_trasfMap_type) on map ≝
- match map with
- [ nil ⇒ []
- | cons h tl ⇒ [ STR_ID (get_name_maxCur h) (get_cur_maxCur h) ]@(build_snapshot tl)
+λ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)
].
-(* uscita da un blocco, rollback di cur in mappa di trasformazione *)
-let rec find_in_snapshot (snap:list aux_strId_type) (str:aux_str_type) on snap ≝
- match snap with
- [ nil ⇒ None ?
- | cons h tl ⇒ match strCmp_str str (get_name_strId h) with
- [ true ⇒ Some ? (get_id_strId h)
- | false ⇒ find_in_snapshot tl str
- ]
- ].
+(* 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)) →
+(strCmp_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)) →
+(strCmp_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))).
-let rec rollback_map (map:aux_trasfMap_type) (snap:list aux_strId_type) on map ≝
+(* 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 O O (False_rect ? daemon) ]
+ ]
+ | cons h tl ⇒ match h with
+ [ MAX_CUR_ELEM str' cur' max' dim' ⇒
+ match strCmp_str str' str return λx.(strCmp_str str' str = x) → ? with
+ [ true ⇒ λp:(strCmp_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:(strCmp_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 ? (strCmp_str str' str))
+ ]
+ ].
+
+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.
+
+(* NB: leave ... enter e' equivalente a e originale *)
+axiom retype_enter_leave_to_e: ∀e,fe,f. aux_trasfMap_type (leave_env (f (enter_env e))) fe → aux_trasfMap_type e fe.
+(* NB: enter non cambia fe *)
+axiom retype_e_to_enter: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (enter_env e) fe.
+(* NB: leave non cambia fe *)
+axiom retype_e_to_leave: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (leave_env e) fe.
+
+let rec rollback_map (e:aux_env_type) (fe,fe':aux_flatEnv_type) (f:aux_env_type → aux_env_type) (map:aux_trasfMap_type (leave_env (f (enter_env e))) fe')
+ (snap:aux_trasfMap_type e fe) on map : aux_trasfMap_type e fe' ≝
match map with
- [ nil ⇒ empty_trasfMap
- | cons h tl ⇒ match find_in_snapshot snap (get_name_maxCur h) with
- [ None ⇒ [h]
- | Some newCur ⇒ [ MAX_CUR_ELEM (get_name_maxCur h) (get_max_maxCur h) newCur ]
- ]@(rollback_map tl snap)
+ [ 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' f [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' f tl snap
].
(* sequenza di utilizzo:
| ...
*)
-(* mini test
+(* mini test
definition pippo ≝ [ ch_P ].
definition pluto ≝ [ ch_Q ].
-definition pippodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
-definition pippodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
-definition pippodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2).
-definition plutodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
-definition plutodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
-definition plutodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_WORD16) 2).
-
-definition map1 ≝ add_maxcur_map empty_trasfMap pippo.
-definition env1 ≝ add_desc_flatEnv empty_flatEnv (name_to_nameId map1 pippo) pippodesc1.
-definition map2 ≝ add_maxcur_map map1 pluto.
-definition env2 ≝ add_desc_flatEnv env1 (name_to_nameId map2 pluto) plutodesc1.
-
-definition snap1 ≝ build_snapshot map2.
-
-definition map3 ≝ add_maxcur_map map2 pippo.
-definition env3 ≝ add_desc_flatEnv env2 (name_to_nameId map3 pippo) pippodesc2.
-definition map4 ≝ add_maxcur_map map3 pluto.
-definition env4 ≝ add_desc_flatEnv env3 (name_to_nameId map4 pluto) plutodesc2.
-
-definition snap2 ≝ build_snapshot map4.
-
-definition map5 ≝ add_maxcur_map map4 pippo.
-definition env5 ≝ add_desc_flatEnv env4 (name_to_nameId map5 pippo) pippodesc3.
-definition map6 ≝ add_maxcur_map map5 pluto.
-definition env6 ≝ add_desc_flatEnv env5 (name_to_nameId map6 pluto) plutodesc3.
-
-definition map7 ≝ rollback_map map6 snap2.
-
-definition map8 ≝ rollback_map map7 snap1.
-
-lemma checkenv : None ? = Some ? env6.
-normalize; elim daemon.
-qed.
-
-lemma checkmap : None ? = Some ? map8.
-normalize; elim daemon.
-qed.
-
-lemma checksnap : None ? = Some ? snap2.
-normalize; elim daemon.
-qed.
+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 (λx.add_desc_env (add_desc_env x pippo false pippodesc3) pluto false plutodesc3) map6' map4.
+
+definition map7' ≝ retype_e_to_leave env4 fenv6 map7.
+
+definition map8 ≝ rollback_map env2 fenv2 fenv6 (λx.add_desc_env (add_desc_env x pippo true pippodesc2) pluto true plutodesc2) map7' map2.
*)
projects / helm.git / commitdiff