(* ********************************************************************** *)
include "compiler/astfe_tree1.ma".
-include "compiler/sigma.ma".
(* ************************ *)
(* PASSO 2 : da AST a ASTFE *)
*)
lemma ast_to_astfe_id :
∀e,b,t.∀ast:ast_id e b t.
- ∀d.∀m:aux_map_type d.∀fe,fe'.
- ∀dimInv:env_to_flatEnv_inv d e m fe'.
- ∀dimLe:le_flatEnv fe fe' = true.
- ∀emfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
- astfe_id fe' b t .
- intros 8;
+ ∀d.∀m:aux_map_type d.∀fe.
+ ∀dimInv:env_to_flatEnv_inv d e m fe.
+ astfe_id fe b t .
+ intros 7;
unfold env_to_flatEnv_inv;
elim a 0;
- intros 5;
- lapply (ASTFE_ID fe' (STR_ID a1 (get_id_map d m a1)) ?);
- [ apply (proj2 ?? (proj1 ?? (dimInv a1 H)))
- | rewrite > (proj2 ?? (dimInv a1 H));
+ intros 3;
+ lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?);
+ [ apply (proj2 ?? (proj1 ?? (H1 a1 H)))
+ | rewrite > (proj2 ?? (H1 a1 H));
apply Hletin
].
qed.
∀d.∀e.∀m:aux_map_type d.∀fe'.
∀dimInv:env_to_flatEnv_inv d e m fe'.
∀dimLe:le_flatEnv fe fe' = true.
- ∀emfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
astfe_id fe' b t.
intros 8;
unfold env_to_flatEnv_inv;
elim a 0;
- intros 5;
+ intros 4;
lapply (ASTFE_ID fe' a1 ?);
- [ apply (leflatenv_to_check fe fe' a1 dimLe H)
- | rewrite > (leflatenv_to_get fe fe' a1 dimLe H);
+ [ apply (leflatenv_to_check fe fe' a1 H2 H)
+ | rewrite > (leflatenv_to_get fe fe' a1 H2 H);
apply Hletin
].
qed.
ast_var e b t → ast_expr e t
*)
let rec ast_to_astfe_expr e t (ast:ast_expr e t)
- d (m:aux_map_type d) fe fe'
- (dimInv:env_to_flatEnv_inv d e m fe')
- (dimLe:le_flatEnv fe fe' = true)
- (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_expr fe' t ≝
+ d (m:aux_map_type d) fe
+ (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_expr fe t ≝
match ast
- return λW.λa:ast_expr e W.astfe_expr fe' W
+ return λW.λa:ast_expr e W.astfe_expr fe W
with
[ AST_EXPR_BYTE8 val ⇒
- ASTFE_EXPR_BYTE8 fe' val
+ ASTFE_EXPR_BYTE8 fe val
| AST_EXPR_WORD16 val ⇒
- ASTFE_EXPR_WORD16 fe' val
+ ASTFE_EXPR_WORD16 fe val
| AST_EXPR_WORD32 val ⇒
- ASTFE_EXPR_WORD32 fe' val
+ ASTFE_EXPR_WORD32 fe val
| AST_EXPR_NEG bType sExpr ⇒
- ASTFE_EXPR_NEG fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_NEG fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv)
| AST_EXPR_NOT bType sExpr ⇒
- ASTFE_EXPR_NOT fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_NOT fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv)
| AST_EXPR_COM bType sExpr ⇒
- ASTFE_EXPR_COM fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_COM fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv)
| AST_EXPR_ADD bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_ADD fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_ADD fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
+ (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
| AST_EXPR_SUB bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_SUB fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_SUB fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
+ (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
| AST_EXPR_MUL bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_MUL fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_MUL fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
+ (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
| AST_EXPR_DIV bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_DIV fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_DIV fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
+ (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
| AST_EXPR_SHR bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_SHR fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_SHR fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
+ (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe dimInv)
| AST_EXPR_SHL bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_SHL fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_SHL fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
+ (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe dimInv)
| AST_EXPR_GT bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_GT fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_GT fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
+ (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
| AST_EXPR_GTE bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_GTE fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_GTE fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
+ (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
| AST_EXPR_LT bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_LT fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_LT fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
+ (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
| AST_EXPR_LTE bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_LTE fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_LTE fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
+ (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
| AST_EXPR_EQ bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_EQ fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_EQ fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
+ (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
| AST_EXPR_NEQ bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_NEQ fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_NEQ fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv)
+ (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv)
| AST_EXPR_B8toW16 sExpr ⇒
- ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_B8toW16 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe dimInv)
| AST_EXPR_B8toW32 sExpr ⇒
- ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_B8toW32 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe dimInv)
| AST_EXPR_W16toB8 sExpr ⇒
- ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_W16toB8 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe dimInv)
| AST_EXPR_W16toW32 sExpr ⇒
- ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_W16toW32 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe dimInv)
| AST_EXPR_W32toB8 sExpr ⇒
- ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_W32toB8 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe dimInv)
| AST_EXPR_W32toW16 sExpr ⇒
- ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_W32toW16 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe dimInv)
| AST_EXPR_ID b sType var ⇒
- ASTFE_EXPR_ID fe' b sType (ast_to_astfe_var e b sType var d m fe fe' dimInv dimLe emfe)
+ ASTFE_EXPR_ID fe b sType (ast_to_astfe_var e b sType var d m fe dimInv)
]
(*
ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
*)
and ast_to_astfe_var e b t (ast:ast_var e b t)
- d (m:aux_map_type d) fe fe'
- (dimInv:env_to_flatEnv_inv d e m fe')
- (dimLe:le_flatEnv fe fe' = true)
- (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_var fe' b t ≝
+ d (m:aux_map_type d) fe
+ (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_var fe b t ≝
match ast
- return λW,X.λa:ast_var e W X.astfe_var fe' W X
+ return λW,X.λa:ast_var e W X.astfe_var fe W X
with
[ AST_VAR_ID sB sType sId ⇒
- ASTFE_VAR_ID fe' sB sType (ast_to_astfe_id e sB sType sId d m fe fe' dimInv dimLe emfe)
+ ASTFE_VAR_ID fe sB sType (ast_to_astfe_id e sB sType sId d m fe dimInv)
| AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒
- ASTFE_VAR_ARRAY fe' sB sType sDim (ast_to_astfe_var e sB (AST_TYPE_ARRAY sType sDim) sVar d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_base_expr e sExpr d m fe fe' dimInv dimLe emfe)
+ ASTFE_VAR_ARRAY fe sB sType sDim (ast_to_astfe_var e sB (AST_TYPE_ARRAY sType sDim) sVar d m fe dimInv)
+ (ast_to_astfe_base_expr e sExpr d m fe dimInv)
| AST_VAR_STRUCT sB sType sField sVar sLtb ⇒
- ASTFE_VAR_STRUCT fe' sB sType sField (ast_to_astfe_var e sB (AST_TYPE_STRUCT sType) sVar d m fe fe' dimInv dimLe emfe)
+ ASTFE_VAR_STRUCT fe sB sType sField (ast_to_astfe_var e sB (AST_TYPE_STRUCT sType) sVar d m fe dimInv)
]
(*
AST_BASE_EXPR: ∀t:ast_base_type.
ast_expr e (AST_TYPE_BASE t) → ast_base_expr e
*)
and ast_to_astfe_base_expr e (ast:ast_base_expr e)
- d (m:aux_map_type d) fe fe'
- (dimInv:env_to_flatEnv_inv d e m fe')
- (dimLe:le_flatEnv fe fe' = true)
- (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_base_expr fe' ≝
+ d (m:aux_map_type d) fe
+ (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_base_expr fe ≝
match ast
- return λa:ast_base_expr e.astfe_base_expr fe'
+ return λa:ast_base_expr e.astfe_base_expr fe
with
[ AST_BASE_EXPR bType sExpr ⇒
- ASTFE_BASE_EXPR fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe)
+ ASTFE_BASE_EXPR fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv)
].
let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
d e (m:aux_map_type d) fe'
(dimInv:env_to_flatEnv_inv d e m fe')
- (dimLe:le_flatEnv fe fe' = true)
- (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_expr fe' t ≝
+ (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_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 emfe)
+ 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 emfe)
+ 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 emfe)
+ 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 emfe)
- (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
+ 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 emfe)
- (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
+ 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 emfe)
- (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
+ 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 emfe)
- (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
+ 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 emfe)
- (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe emfe)
+ 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 emfe)
- (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe emfe)
+ ASTFE_EXPR_SHL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
| ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒
- ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
- (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
+ 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 emfe)
- (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
+ 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 emfe)
- (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
+ 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 emfe)
- (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
+ 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 emfe)
- (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
+ 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 emfe)
- (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
+ 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 emfe)
+ 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 emfe)
+ 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 emfe)
+ 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 emfe)
+ 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 emfe)
+ 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 emfe)
+ 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 emfe)
+ ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe)
]
and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t)
d e (m:aux_map_type d) fe'
(dimInv:env_to_flatEnv_inv d e m fe')
- (dimLe:le_flatEnv fe fe' = true)
- (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_var fe' b t ≝
+ (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 emfe)
+ 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 emfe)
- (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe emfe)
+ 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 emfe)
+ ASTFE_VAR_STRUCT fe' sB sType sField (ast_to_astfe_retype_var fe sB (AST_TYPE_STRUCT sType) sVar d e m fe' dimInv dimLe)
]
and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe)
d e (m:aux_map_type d) fe'
(dimInv:env_to_flatEnv_inv d e m fe')
- (dimLe:le_flatEnv fe fe' = true)
- (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_base_expr 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 emfe)
+ ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
].
(*
*)
definition ast_to_astfe_init ≝
λe,t.λast:ast_init e t.
-λd.λm:aux_map_type d.λfe,fe'.
-λdimInv:env_to_flatEnv_inv d e m fe'.
-λdimLe:le_flatEnv fe fe' = true.
-λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
+λd.λm:aux_map_type d.λfe.
+λdimInv:env_to_flatEnv_inv d e m fe.
match ast
- return λW.λa:ast_init e W.astfe_init fe' W
+ return λW.λa:ast_init e W.astfe_init fe W
with
[ AST_INIT_VAR sB sType sVar ⇒
- ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_var e sB sType sVar d m fe fe' dimInv dimLe emfe)
+ ASTFE_INIT_VAR fe sB sType (ast_to_astfe_var e sB sType sVar d m fe dimInv)
| AST_INIT_VAL sType sArgs ⇒
- ASTFE_INIT_VAL fe' sType sArgs
+ ASTFE_INIT_VAL fe sType sArgs
].
λd.λe.λm:aux_map_type d.λfe'.
λdimInv:env_to_flatEnv_inv d e m fe'.
λdimLe:le_flatEnv fe fe' = true.
-λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
match ast
return λW.λa:astfe_init fe W.astfe_init fe' W
with
[ ASTFE_INIT_VAR sB sType sVar ⇒
- ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe emfe)
+ ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe)
| ASTFE_INIT_VAL sType sArgs ⇒
ASTFE_INIT_VAL fe' sType sArgs
].
+(*
+ ASTFE_STM_ASG: ∀t:ast_type.
+ astfe_var e false t → astfe_expr e t → astfe_stm e
+ ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
+ astfe_id e b t → astfe_init e t → astfe_stm e
+ ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
+ ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
+*)
+let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe) d e m fe' dimInv dimLe on ast : astfe_stm fe' ≝
+ match ast with
+ [ ASTFE_STM_ASG sType sVar sExpr ⇒
+ ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe)
+
+ | ASTFE_STM_INIT sB sType sId sInit ⇒
+ ASTFE_STM_INIT fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe)
+
+ | ASTFE_STM_WHILE sExpr sBody ⇒
+ ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)
+
+ | ASTFE_STM_IF sNelExprBody sOptBody ⇒
+ ASTFE_STM_IF fe' (cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
+ )»&t)
+ «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
+ sNelExprBody))
+ (opt_map ?? sOptBody
+ (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)))
+ ]
+(*
+ ASTFE_BODY: list (astfe_stm e) → astfe_body e
+*)
+and ast_to_astfe_retype_body fe (ast:astfe_body fe) d e m fe' dimInv dimLe on ast : astfe_body fe' ≝
+ match ast with
+ [ ASTFE_BODY sLStm ⇒
+ ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] sLStm)
+ ].
+
+definition ast_to_astfe_retype_stm_list ≝
+λfe.λast:list (astfe_stm fe).λd,e,m,fe',dimInv,dimLe.
+ fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] ast.
+
+definition ast_to_astfe_retype_exprBody_neList ≝
+λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).λd,e,m,fe',dimInv,dimLe.
+ cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
+ )»&t)
+ «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
+ ast).
+
(*
AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
ast_var e false t → ast_expr e t → ast_stm e
AST_STM_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
*)
-(*lemma ast_to_astfe_stm_aux :
- ∀d,e.∀m:aux_map_type d.∀fe,fe',dimInv,dimLe.
- ∀emfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
- ∀ast:astfe_stm fe'.
- (ΣD.(ΣE.(ΣM.(ΣFE.(ΣFE'.(ΣDIMINV.(ΣDIMLE.Prod (env_map_flatEnv D E M FE FE' DIMINV DIMLE) (astfe_stm FE')))))))).
- elim daemon.
-qed.*)
-inductive ast_to_astfe_stm_res (d:nat) : Type ≝
-AST_TO_ASTFE_STM_RES:
- ∀e.∀m:aux_map_type d.∀fe,fe'.
- ∀dimInv:env_to_flatEnv_inv d e m fe'.
- ∀dimLe:le_flatEnv fe fe' = true.
- ∀trsf:Prod3T aux_str_type bool ast_type.
- env_map_flatEnv d e m fe fe' dimInv dimLe → astfe_stm fe' → ast_to_astfe_stm_res d.
-
-let rec ast_to_astfe_stm e (ast:ast_stm e) on ast ≝
+inductive ast_to_astfe_stm_record (d:nat) (e:aux_env_type) (fe:aux_flatEnv_type) : Type ≝
+AST_TO_ASTFE_STM_RECORD: ∀m:aux_map_type d.∀fe'.
+ env_to_flatEnv_inv d e m fe' →
+ le_flatEnv fe fe' = true →
+ astfe_stm fe' →
+ ast_to_astfe_stm_record d e fe.
+
+inductive ast_to_astfe_if_record (d:nat) (e:aux_env_type) (fe:aux_flatEnv_type) : Type ≝
+AST_TO_ASTFE_IF_RECORD: ∀m:aux_map_type d.∀fe'.
+ env_to_flatEnv_inv d e m fe' →
+ le_flatEnv fe fe' = true →
+ ne_list (Prod (astfe_base_expr fe') (astfe_body fe')) →
+ ast_to_astfe_if_record d e fe.
+
+inductive ast_to_astfe_decl_record (d:nat) (e:aux_env_type) (m:aux_map_type d) (fe:aux_flatEnv_type) : Type ≝
+AST_TO_ASTFE_DECL_RECORD: ∀trsf:list (Prod3T aux_str_type bool ast_type).
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env trsf e)
+ (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe)))
+ (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) →
+ le_flatEnv fe (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) = true →
+ list (astfe_stm (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe)))) →
+ ast_to_astfe_decl_record d e m fe.
+
+let rec ast_to_astfe_stm e (ast:ast_stm e) on ast : Πd.Πm:aux_map_type d.Πfe.Πfe'.
+ env_to_flatEnv_inv d e m fe' →
+ le_flatEnv fe fe' = true →
+ ast_to_astfe_stm_record d e fe ≝
match ast
return λX.λast:ast_stm X.
- Πd.Πm:aux_map_type d.Πfe.Πfe'.ΠdimInv:env_to_flatEnv_inv d X m fe'.
- ΠdimLe:le_flatEnv fe fe' = true.env_map_flatEnv d X m fe fe' dimInv dimLe →
- ast_to_astfe_stm_res d
+ Πd.Πm:aux_map_type d.Πfe.Πfe'.
+ env_to_flatEnv_inv d X m fe' → le_flatEnv fe fe' = true → ast_to_astfe_stm_record d X fe
with
[ AST_STM_ASG sE sType sVar sExpr ⇒
- λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.
- λdimLe:le_flatEnv fe fe' = true.λemfe:env_map_flatEnv d sE m fe fe' dimInv dimLe.
- AST_TO_ASTFE_STM_RES d sE m fe fe' dimInv dimLe emfe []
- (ASTFE_STM_ASG fe' sType (ast_to_astfe_var sE false sType sVar d m fe fe' dimInv dimLe emfe)
- (ast_to_astfe_expr sE sType sExpr d m fe fe' dimInv dimLe emfe))
-
- | _ ⇒ False_rect ? daemon
+ λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true.
+ AST_TO_ASTFE_STM_RECORD d sE fe m fe' dimInv dimLe
+ (ASTFE_STM_ASG fe' sType (ast_to_astfe_var sE false sType sVar d m fe' dimInv)
+ (ast_to_astfe_expr sE sType sExpr d m fe' dimInv))
+
+ | AST_STM_WHILE sE sExpr sDecl ⇒
+ λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true.
+ (* in sostanza
+ 1) eseguo decl su ENTER dell'invariante
+ 2) decl restituisce ADD+ENTER dell'invariante
+ 3) eseguo base_expr sull'invariante
+ 4) retipo base_expr su LEAVE+ADD+ENTER dell'invariante
+ 5) retituisco su LEAVE+ADD+ENTER dell'invariante *)
+ match ast_to_astfe_decl (enter_env sE) sDecl (S d) (enter_map d m) fe fe' (env_map_flatEnv_enter_aux d sE m fe' dimInv) dimLe with
+ [ AST_TO_ASTFE_DECL_RECORD resTrsf resDimInv resDimLe resLStm ⇒
+ AST_TO_ASTFE_STM_RECORD d sE fe
+ (* m'' *)
+ (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))))
+ (* fe'' *)
+ (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe')))
+ (* leave_add_enter(dimInv) *)
+ (env_map_flatEnv_leave_aux d sE m fe' resTrsf resDimInv)
+ (* fe ≤ fe' ∧ fe' ≤ fe'' → fe ≤ fe'' *)
+ (leflatenv_trans ??? dimLe resDimLe)
+ (* risultato su fe'' *)
+ (ASTFE_STM_WHILE (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe')))
+ (ast_to_astfe_retype_base_expr fe' (ast_to_astfe_base_expr sE sExpr d m fe' dimInv)
+ d sE
+ (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))))
+ (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe')))
+ (env_map_flatEnv_leave_aux d sE m fe' resTrsf resDimInv)
+ resDimLe)
+ (ASTFE_BODY (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))) resLStm)) ]
+
+ | AST_STM_IF sE sExprDecl sOptDecl ⇒
+ λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true.
+ let rec aux (nel:ne_list (Prod (ast_base_expr sE) (ast_decl (enter_env sE))))
+ (pMap:aux_map_type d) (pFe,pFe':aux_flatEnv_type)
+ (pDimInv:env_to_flatEnv_inv d sE pMap pFe')
+ (pDimLe:le_flatEnv pFe pFe' = true) on nel : ast_to_astfe_if_record d sE pFe ≝
+ match nel with
+ [ ne_nil h ⇒
+ match ast_to_astfe_decl (enter_env sE) (snd ?? h) (S d) (enter_map d pMap) pFe pFe' (env_map_flatEnv_enter_aux d sE pMap pFe' pDimInv) pDimLe with
+ [ AST_TO_ASTFE_DECL_RECORD resTrsf resDimInv resDimLe resLStm ⇒
+ AST_TO_ASTFE_IF_RECORD d sE pFe
+ (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))))
+ (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe')))
+ (env_map_flatEnv_leave_aux d sE pMap pFe' resTrsf resDimInv)
+ (leflatenv_trans ??? pDimLe resDimLe)
+ «£(pair ?? (ast_to_astfe_retype_base_expr pFe' (ast_to_astfe_base_expr sE (fst ?? h) d pMap pFe' pDimInv)
+ d sE
+ (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))))
+ (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe')))
+ (env_map_flatEnv_leave_aux d sE pMap pFe' resTrsf resDimInv)
+ resDimLe)
+ (ASTFE_BODY (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))) resLStm))» ]
+
+ | ne_cons h t ⇒ (False_rect ? daemon)
+ (*match ast_to_astfe_decl (enter_env sE) (snd ?? h) (S d) (enter_map d pMap) pFe pFe' (env_map_flatEnv_enter_aux d sE pMap pFe' pDimInv) pDimLe with
+ [ AST_TO_ASTFE_DECL_RECORD resTrsf resDimInv resDimLe resLStm ⇒
+ match aux t (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))))
+ pFe (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe')))
+ (env_map_flatEnv_leave_aux d sE pMap pFe' resTrsf resDimInv)
+ (leflatenv_trans ??? pDimLe resDimLe) with
+ [ AST_TO_ASTFE_IF_RECORD iMap iFe' iDimInv iDimLe iNelExprDecl ⇒
+ AST_TO_ASTFE_IF_RECORD d sE pFe iMap iFe' iDimInv iDimLe
+ (False_rect ? daemon) ]]*)
+
+
+ ] in (False_rect ? daemon)
- ].
+ ]
+and ast_to_astfe_decl e (ast:ast_decl e) on ast : Πd.Πm:aux_map_type d.Πfe.Πfe'.
+ env_to_flatEnv_inv d e m fe' →
+ le_flatEnv fe fe' = true →
+ ast_to_astfe_decl_record d e m fe' ≝
+ match ast
+ return λX.λast:ast_decl X.
+ Πd.Πm:aux_map_type d.Πfe.Πfe'.
+ env_to_flatEnv_inv d X m fe' → le_flatEnv fe fe' = true → ast_to_astfe_decl_record d X m fe'
+ with
+ [ AST_NO_DECL sE sLStm ⇒
+ λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true.
+ False_rect ? daemon
+ | _ ⇒ False_rect ? daemon
+ ].
-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 ⇒
- λmap:aux_trasfMap_type e' fe.
- opt_map ?? (ast_to_astfe_var e' false subType var fe map)
- (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr fe map)
- (λresExpr.Some ? (≪fe,(pair ?? map (ASTFE_STM_ASG fe subType resVar resExpr))≫)))
-
- | AST_STM_WHILE e' expr decl ⇒
- λmap:aux_trasfMap_type e' fe.
- opt_map ?? (ast_to_astfe_base_expr e' expr fe map)
- (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe (retype_e_to_enter e' fe map))
- (λsigmaRes:(Σf.(Σfe'. Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
- [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
- [ sigma_intro fe' mapAndStm ⇒ match mapAndStm with
- [ pair map' resDecl ⇒
- match le_flatEnv fe fe'
- return λx.(le_flatEnv fe fe' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
- with
- [ true ⇒ λp:(le_flatEnv fe fe' = true).
- opt_map ?? (retype_base_expr fe resExpr fe' p)
- (λresExpr'.Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map)
- (ASTFE_STM_WHILE fe' resExpr' (ASTFE_BODY fe' resDecl))≫))
- | false ⇒ λp:(le_flatEnv fe fe' = false).None ?
- ] (refl_eq ? (le_flatEnv fe fe'))
- ]]]))
+FINQUI
| AST_STM_IF e' nelExprDecl optDecl ⇒
λmap:aux_trasfMap_type e' fe.
)
).
*)
-
-
-
-
-
-
-
-
-
-
-
-
-(*
- ASTFE_STM_ASG: ∀t:ast_type.
- astfe_var e false t → astfe_expr e t → astfe_stm e
- ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
- astfe_id e b t → astfe_init e t → astfe_stm e
- ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
- ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
-*)
-let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe) d e m fe' dimInv dimLe (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_stm fe' ≝
- match ast with
- [ ASTFE_STM_ASG sType sVar sExpr ⇒
- ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe emfe)
- (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe emfe)
-
- | 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 emfe)
- (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe emfe)
-
- | ASTFE_STM_WHILE sExpr sBody ⇒
- ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe emfe)
- (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe emfe)
-
- | 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 emfe)
- (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe emfe)
- )»&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 emfe)))
- ]
-(*
- ASTFE_BODY: list (astfe_stm e) → astfe_body e
-*)
-and ast_to_astfe_retype_body fe (ast:astfe_body fe) d e m fe' dimInv dimLe (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_body fe' ≝
- match ast with
- [ ASTFE_BODY sLStm ⇒
- ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe emfe ]@t) [] sLStm)
- ].
-
-definition ast_to_astfe_retype_stm_list ≝
-λfe.λast:list (astfe_stm fe).λd,e,m,fe',dimInv,dimLe.λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
- fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe emfe]@t) [] ast.
-
-definition ast_to_astfe_retype_exprBody_neList ≝
-λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).λd,e,m,fe',dimInv,dimLe.λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
- cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe emfe)
- (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe emfe)
- )»&t)
- «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
- ast).
-
-
-
-
-
-
-
projects / helm.git / commitdiff