(* 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 ].
-
-(* 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.
+ AST_ID: ∀str:aux_str_type.
+ (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)))
*)
+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;
+ elim a 0;
+ intros 3;
+ lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?);
+ [ apply (proj2 ?? (proj1 ?? ((env_to_flatEnv_inv_last ???? H1) a1 H)))
+ | rewrite > (proj2 ?? ((env_to_flatEnv_inv_last ???? H1) a1 H));
+ apply Hletin
+ ].
+qed.
-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.
+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;
+ 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
+ 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 d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_NOT: ∀t:ast_base_type.
+ 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 d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+
+| AST_EXPR_ADD: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_SUB: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_MUL: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_DIV: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_SHR: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_SHL: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_AND: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_OR: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_XOR: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+
+| AST_EXPR_GT : ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_GTE: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_LT : ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_LTE: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_EQ : ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_NEQ: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+
+| AST_EXPR_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 d e b t → ast_expr d 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_AND bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_AND fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_OR bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_OR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_XOR bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_XOR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+
+ | AST_EXPR_GT bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_GT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (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_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)
+ AST_VAR_ID: ∀b:bool.∀t:ast_type.
+ ast_id d e b t → ast_var d e b t
+| AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
+ 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 d e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var d 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
+ AST_BASE_EXPR: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d 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)
].
-(*
- 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_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)
+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_AND bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_AND fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_OR bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_OR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_XOR bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_XOR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+
+ | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_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)
- | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe subType (ASTFE_INIT_VAL fe subType args) 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 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_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
+ AST_INIT_VAR: ∀b:bool.∀t:ast_type.
+ ast_var d e b t → ast_init d e t
+| AST_INIT_VAL: ∀t:ast_type.
+ aux_ast_init_type t → ast_init d e t
*)
-(* 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.
+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)
-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'))))))).
+ | AST_INIT_VAL sType sArgs ⇒
+ ASTFE_INIT_VAL fe sType sArgs
-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')) ≝
+ ].
+
+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 λe':aux_env_type.λ_:ast_stm e'.aux_trasfMap_type e' fe → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
+ return λW.λa:astfe_init fe W.astfe_init fe' W
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 (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 ⇒
- λ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)))≫)
- ]]])]]])
+ [ 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: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_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)))
]
(*
- 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
+ ASTFE_BODY: list (astfe_stm e) → astfe_body 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.(Σ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 ⇒
- λ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 ⇒
- λ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))
- ]]]))
+and ast_to_astfe_retype_body fe (ast:astfe_body 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_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: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.
+ 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:aux_map_type d.λfe'.
+λdimInv:env_to_flatEnv_inv d e m fe'.
+λdimLe:le_flatEnv fe fe' = true.
+ 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).
+
+(* multi-sigma per incapsulare i risultati della trasformazione sugli stm/decl *)
+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.
+
(*
- AST_ROOT: ast_decl empty_env → ast_root.
+ 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
*)
-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 (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".
-include "compiler/preast_to_ast.ma".*)
+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.
+ env_to_flatEnv_inv d e m fe →
+ ast_to_astfe_stm_record d e fe ≝
+ match ast
+ return λD.λE.λast:ast_stm D E.
+ Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_stm_record D E fe
+ with
+ [ AST_STM_ASG sD sE sType sVar sExpr ⇒
+ λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
+ AST_TO_ASTFE_STM_RECORD sD sE fe m fe dimInv
+ (eq_to_leflatenv ?? (refl_eq ??))
+ (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.λdimInv:env_to_flatEnv_inv sD sE m fe.
+ match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD m) fe
+ (env_map_flatEnv_enter_aux sD sE m fe dimInv) 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)
+ 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.λdimInv:env_to_flatEnv_inv sD sE m fe.
+ 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:aux_flatEnv_type)
+ (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) 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
+ (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) 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)
+ 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
+ (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with
+ [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+ match aux t (leave_map sD resMap) 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)) with
+ [ AST_TO_ASTFE_IF_RECORD resMap' resFe' resDimInv' resDimLe' resExprBody ⇒
+ AST_TO_ASTFE_IF_RECORD sD sE pFe resMap' resFe' resDimInv'
+ (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 dimInv 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
+ (env_map_flatEnv_enter_aux sD sE resMap resFe resDimInv) 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) ]]]
+ ]
(*
-{ 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; }
-}
+ AST_NO_DECL: ∀d.∀e:aux_env_type d.
+ list (ast_stm d e) → ast_decl d e
+| AST_CONST_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
+ (check_not_already_def_env d e str) → ast_init d e t → ast_decl d (add_desc_env d e str true t) → ast_decl d e
+| AST_VAR_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
+ (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str false t) → ast_decl d e
*)
+and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe.
+ env_to_flatEnv_inv d e m fe →
+ ast_to_astfe_decl_record d e fe ≝
+ match ast
+ return λD.λE.λast:ast_decl D E.
+ Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_decl_record D E fe
+ with
+ [ AST_NO_DECL sD sE sLStm ⇒
+ λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
+ let rec aux (l:list (ast_stm sD sE)) (pMap:aux_map_type sD) (pFe:aux_flatEnv_type)
+ (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) 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 (eq_to_leflatenv ?? (refl_eq ??)) []
+
+ | cons h t ⇒
+ match ast_to_astfe_stm sD sE h pMap pFe pDimInv with
+ [ AST_TO_ASTFE_STM_RECORD resMap resFe resDimInv resDimLe resStm ⇒
+ match aux t resMap resFe resDimInv 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 ??? resDimLe resDimLe')
+ ([ ast_to_astfe_retype_stm resFe resStm sD sE resMap' resFe' resDimInv' resDimLe' ]@resLStm) ]]
+
+ ] in
+ match aux sLStm m fe dimInv 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_CONST_DECL sD sE sName sType sDim sInit sDecl ⇒
+ λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
+ match ast_to_astfe_decl sD (add_desc_env sD sE sName true sType) sDecl
+ (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+ (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+ (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv) with
+ [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+ AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
+ ([ tripleT ??? sName true sType ]@resTrsf)
+ (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
+ (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe)
+ ([ ASTFE_STM_INIT resFe true sType
+ (* l'id e' sull'ambiente arricchito *)
+ (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+ true sType
+ (ast_to_astfe_id sD (add_desc_env sD sE sName true sType)
+ true sType
+ (newid_from_init sD sE sName true sType)
+ (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+ (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+ (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv))
+ sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE)
+ resMap resFe
+ (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
+ resDimLe)
+ (* l'init e' sull'ambiente non arricchito *)
+ (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType sInit m fe dimInv)
+ sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE)
+ resMap resFe
+ (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
+ (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe))
+ ]@resLStm) ]
+
+ | AST_VAR_DECL sD sE sName sType sDim sOptInit sDecl ⇒
+ λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
+ match ast_to_astfe_decl sD (add_desc_env sD sE sName false sType) sDecl
+ (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+ (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+ (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv) with
+ [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+ AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
+ ([ tripleT ??? sName false sType ]@resTrsf)
+ (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
+ (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe)
+ (match sOptInit with
+ [ None ⇒ []
+ | Some init ⇒
+ [ ASTFE_STM_INIT resFe false sType
+ (* l'id e' sull'ambiente arricchito *)
+ (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+ false sType
+ (ast_to_astfe_id sD (add_desc_env sD sE sName false sType)
+ false sType
+ (newid_from_init sD sE sName false sType)
+ (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+ (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+ (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv))
+ sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE)
+ resMap resFe
+ (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
+ resDimLe)
+ (* l'init e' sull'ambiente non arricchito *)
+ (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType init m fe dimInv)
+ sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE)
+ resMap resFe
+ (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
+ (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe))
+ ]]@resLStm) ]
+
+ ].
+
(*
-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,x2〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)»))) (
- 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,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 []))
- )
- £ (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 [])
- ))
- ])
- )
- » (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 [])))
- ]
- )
- )
- )
-).
-
-lemma provacheck : opt_map ?? (preast_to_ast prova) (λres.Some ? (ast_to_astfe res)) = None ?.
-normalize;
+ AST_ROOT: ast_decl O 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 O empty_env decl empty_map empty_flatEnv env_map_flatEnv_empty_aux with
+ [ AST_TO_ASTFE_DECL_RECORD _ resFe _ _ _ resLStm ⇒ ≪resFe,ASTFE_ROOT resFe (ASTFE_BODY resFe resLStm)≫ ]].
projects / helm.git / blobdiff