λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.
match ast with [ AST_ID s _ ⇒ s ].
-(* NB: avendo poi in input la dimostrazione "check_desc_env e (get_name_ast_id e b t ast)" ha senso *)
-axiom ast_to_astfe_id_ax:
- Πe:aux_env_type.Πb:bool.Πt:ast_type. Πast:ast_id e b t. Πfe:aux_flatEnv_type.
- Πmap:aux_trasfMap_type e fe.
- check_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)).
-
-(*
-axiom ax2:
- Πe:aux_env_type.Πb:bool.Πt:ast_type. Πast:ast_id e b t. Πfe:aux_flatEnv_type.
- Πmap:aux_trasfMap_type e fe.
- get_const_desc
- (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))
- = b.
-
-axiom ax3:
- Πe:aux_env_type.Πb:bool.Πt:ast_type. Πast:ast_id e b t. Πfe:aux_flatEnv_type.
- Πmap:aux_trasfMap_type e fe.
- get_type_desc
- (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))) = t.
-*)
-
-definition ast_to_astfe_id:
+definition ast_to_astfe_id :
Πe:aux_env_type.Πb:bool.Πt:ast_type.Πast:ast_id e b t.Πfe:aux_flatEnv_type.
Πmap:aux_trasfMap_type e fe.
astfe_id fe
(get_const_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))))
- (get_type_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))).
- apply
- (λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.λfe:aux_flatEnv_type.λmap:aux_trasfMap_type e fe.
- ASTFE_ID fe (name_to_nameId e fe map (get_name_ast_id e b t ast)) ?);
- apply ast_to_astfe_id_ax.
-qed.
+ (get_type_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))) ≝
+λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.λfe:aux_flatEnv_type.λmap:aux_trasfMap_type e fe.
+ ASTFE_ID fe (name_to_nameId e fe map (get_name_ast_id e b t ast))
+ (ast_to_astfe_id_aux e fe map (get_name_ast_id e b t ast)
+ (ast_id_ind e
+ (λHbeta3:bool.λHbeta2:ast_type.λHbeta1:ast_id e Hbeta3 Hbeta2.check_desc_env e (get_name_ast_id e Hbeta3 Hbeta2 Hbeta1))
+ (λa:aux_str_type.λH:check_desc_env e a.H) b t ast)).
+
+definition get_name_astfe_id ≝ λfe,b,t.λast:astfe_id fe b t.match ast with [ ASTFE_ID n _ ⇒ n ].
+
+definition retype_id
+: Πfe:aux_flatEnv_type.Πb:bool.Πt:ast_type.Πast:astfe_id fe b t.Πfe':aux_flatEnv_type.le_flatEnv fe fe' = true →
+ astfe_id fe'
+ (get_const_desc (get_desc_flatEnv fe' (get_name_astfe_id fe b t ast)))
+ (get_type_desc (get_desc_flatEnv fe' (get_name_astfe_id fe b t ast))) ≝
+λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
+ ASTFE_ID fe' (get_name_astfe_id fe b t ast)
+ (leflatenv_to_check fe fe' (get_name_astfe_id fe b t ast) dim (astfe_id_ind fe
+ (λHbeta3:bool.λHbeta2:ast_type.λHbeta1:astfe_id fe Hbeta3 Hbeta2.check_desc_flatEnv fe (get_name_astfe_id fe Hbeta3 Hbeta2 Hbeta1))
+ (λa:aux_strId_type.λH:check_desc_flatEnv fe a.H) b t ast)).
(*
AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
(λres.Some ? (ASTFE_BASE_EXPR fe bType res))
].
+let rec retype_expr (fe:aux_flatEnv_type) (t:ast_type) (ast:astfe_expr fe t) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_expr fe' t) ≝
+ match ast with
+ [ ASTFE_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' val) t
+ | ASTFE_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 fe' val) t
+ | ASTFE_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 fe' val) t
+
+ | ASTFE_EXPR_NEG bType subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG fe' bType res) t)
+ | ASTFE_EXPR_NOT bType subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT fe' bType res) t)
+ | ASTFE_EXPR_COM bType subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_COM fe' bType res) t)
+
+ | ASTFE_EXPR_ADD bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD fe' bType res1 res2) t))
+ | ASTFE_EXPR_SUB bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB fe' bType res1 res2) t))
+ | ASTFE_EXPR_MUL bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL fe' bType res1 res2) t))
+ | ASTFE_EXPR_DIV bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV fe' bType res1 res2) t))
+ | ASTFE_EXPR_SHR bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR fe' bType res1 res2) t))
+ | ASTFE_EXPR_SHL bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL fe' bType res1 res2) t))
+
+ | ASTFE_EXPR_LT bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT fe' bType res1 res2) t))
+ | ASTFE_EXPR_LTE bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE fe' bType res1 res2) t))
+ | ASTFE_EXPR_GT bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT fe' bType res1 res2) t))
+ | ASTFE_EXPR_GTE bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE fe' bType res1 res2) t))
+ | ASTFE_EXPR_EQ bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ fe' bType res1 res2) t))
+ | ASTFE_EXPR_NEQ bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ fe' bType res1 res2) t))
+
+ | ASTFE_EXPR_B8toW16 subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 fe' res) t)
+ | ASTFE_EXPR_B8toW32 subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 fe' res) t)
+ | ASTFE_EXPR_W16toB8 subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 fe' res) t)
+ | ASTFE_EXPR_W16toW32 subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 fe' res) t)
+ | ASTFE_EXPR_W32toB8 subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 fe' res) t)
+ | ASTFE_EXPR_W32toW16 subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 fe' res) t)
+
+ | ASTFE_EXPR_ID b subType var ⇒
+ opt_map ?? (retype_var fe b subType var fe' dim)
+ (λres.ast_to_astfe_expr_check fe' subType (ASTFE_EXPR_ID fe' b subType res) t)
+ ]
+and retype_var (fe:aux_flatEnv_type) (b:bool) (t:ast_type) (ast:astfe_var fe b t) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_var fe' b t) ≝
+ match ast with
+ [ ASTFE_VAR_ID subB subType subId ⇒
+ opt_map ?? (ast_to_astfe_id_check fe' ?? (retype_id fe subB subType subId fe' dim) subB subType)
+ (λresId.ast_to_astfe_var_check fe' subB subType (ASTFE_VAR_ID fe' subB subType resId) b t)
+
+ | ASTFE_VAR_ARRAY subB subType n var expr ⇒
+ opt_map ?? (retype_var fe subB (AST_TYPE_ARRAY subType n) var fe' dim)
+ (λresVar.opt_map ?? (retype_base_expr fe expr fe' dim)
+ (λresExpr.ast_to_astfe_var_check fe' subB subType (ASTFE_VAR_ARRAY fe' subB subType n resVar resExpr) b t))
+
+ | ASTFE_VAR_STRUCT subB nelSubType field var ⇒
+ opt_map ?? (retype_var fe subB (AST_TYPE_STRUCT nelSubType) var fe' dim)
+ (λres.ast_to_astfe_var_check fe' subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT fe' subB nelSubType field res) b t)
+ ]
+and retype_base_expr (fe:aux_flatEnv_type) (ast:astfe_base_expr fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_base_expr fe') ≝
+ match ast with
+ [ ASTFE_BASE_EXPR bType subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
+ (λres.Some ? (ASTFE_BASE_EXPR fe' bType res))
+ ].
+
(*
AST_INIT_VAR: ∀b:bool.∀t:ast_type.
ast_var e b t → ast_init e t
| AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe subType (ASTFE_INIT_VAL fe subType args) t
].
+definition retype_init ≝
+λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_init fe t.λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
+ match ast with
+ [ ASTFE_INIT_VAR subB subType var ⇒
+ opt_map ?? (retype_var fe subB subType var fe' dim)
+ (λres.ast_to_astfe_init_check fe' subType (ASTFE_INIT_VAR fe' subB subType res) t)
+
+ | ASTFE_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe' subType (ASTFE_INIT_VAL fe' subType args) t
+ ].
+
(*
- AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
- ast_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
+ 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 retype_stm (fe:aux_flatEnv_type) (ast:astfe_stm fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_stm fe') ≝
+ match ast with
+ [ ASTFE_STM_ASG subType var expr ⇒
+ opt_map ?? (retype_var fe false subType var fe' dim)
+ (λresVar.opt_map ?? (retype_expr fe subType expr fe' dim)
+ (λresExpr.Some ? (ASTFE_STM_ASG fe' subType resVar resExpr)))
+
+ | ASTFE_STM_INIT subB subType subId init ⇒
+ opt_map ?? (ast_to_astfe_id_check fe' ?? (retype_id fe subB subType subId fe' dim) subB subType)
+ (λresId.opt_map ?? (retype_init fe subType init fe' dim)
+ (λresInit.Some ? (ASTFE_STM_INIT fe' subB subType resId resInit)))
+
+ | ASTFE_STM_WHILE expr body ⇒
+ opt_map ?? (retype_base_expr fe expr fe' dim)
+ (λresExpr.opt_map ?? (retype_body fe body fe' dim)
+ (λresBody.Some ? (ASTFE_STM_WHILE fe' resExpr resBody)))
+
+ | ASTFE_STM_IF nelExprBody optBody ⇒
+ opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (retype_base_expr fe (fst ?? h) fe' dim)
+ (λresExpr.opt_map ?? (retype_body fe (snd ?? h) fe' dim)
+ (λresBody.opt_map ?? t
+ (λt'.Some ? («£(pair ?? resExpr resBody)»&t')))))
+ (Some ? (ne_nil ? (pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))))
+ nelExprBody)
+ (λres.match optBody with
+ [ None ⇒ Some ? (ASTFE_STM_IF fe' (cut_last_neList ? res) (None ?))
+ | Some body ⇒
+ opt_map ?? (retype_body fe body fe' dim)
+ (λresBody.Some ? (ASTFE_STM_IF fe' (cut_last_neList ? res) (Some ? resBody)))
+ ])
+ ]
+(*
+ ASTFE_BODY: list (astfe_stm e) → astfe_body e
*)
-(* 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')).
+and retype_body (fe:aux_flatEnv_type) (ast:astfe_body fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_body fe') ≝
+ match ast with
+ [ ASTFE_BODY lStm ⇒
+ opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (retype_stm fe h fe' dim)
+ (λh'.opt_map ?? t
+ (λt'.Some ? ([h']@t')))) (Some ? []) lStm)
+ (λresStm.Some ? (ASTFE_BODY fe' resStm))
+ ].
+
+definition retype_stm_list ≝
+λfe:aux_flatEnv_type.λast:list (astfe_stm fe).λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
+ fold_right_list ?? (λh,t.opt_map ?? (retype_stm fe h fe' dim)
+ (λh'.opt_map ?? t
+ (λt'.Some ? ([h']@t')))) (Some ? []) ast.
+
+definition retype_exprAndBody_neList ≝
+λfe:aux_flatEnv_type.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
+ opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (retype_base_expr fe (fst ?? h) fe' dim)
+ (λresExpr.opt_map ?? (retype_body fe (snd ?? h) fe' dim)
+ (λresBody.opt_map ?? t
+ (λt'.Some ? («£(pair ?? resExpr resBody)»&t')))))
+ (Some ? (ne_nil ? (pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))))
+ ast)
+ (λres.Some ? (cut_last_neList ? res)).
(* applicare l'identita' e' inifluente *)
lemma retype_map_to_id : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:(aux_env_type → aux_env_type).
apply (eq_rect ? e (λHbeta1:aux_env_type.aux_trasfMap_type Hbeta1 fe) a (f e) H);
qed.
-axiom how_to_build_it : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:aux_env_type → aux_env_type.∀map:aux_trasfMap_type (f e) fe.∀ll:list (astfe_stm fe).
- (sigma (aux_env_type\to aux_env_type)
- (\lambda f:(aux_env_type\to aux_env_type).
- (sigma aux_flatEnv_type
- (\lambda fe':aux_flatEnv_type.
- (Prod (aux_trasfMap_type (f e) fe') (list (astfe_stm fe'))))))).
-
+(*
+ 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
+*)
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
λ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
+ (λ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 ⇒
- 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))≫)
+ match le_flatEnv fe fe'
+ return λx.(le_flatEnv fe fe' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
+ with
+ [ true ⇒ λp:(le_flatEnv fe fe' = true).
+ opt_map ?? (retype_base_expr fe resExpr fe' p)
+ (λresExpr'.Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map)
+ (ASTFE_STM_WHILE fe' resExpr' (ASTFE_BODY fe' resDecl))≫))
+ | false ⇒ λp:(le_flatEnv fe fe' = false).None ?
+ ] (refl_eq ? (le_flatEnv fe fe'))
]]]))
| AST_STM_IF e' nelExprDecl optDecl ⇒
[ 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
+ (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
+ [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
[ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
[ pair m' resDecl ⇒
- 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) £»≫)
+ match le_flatEnv fenv fenv'
+ return λx.(le_flatEnv fenv fenv' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
+ with
+ [ true ⇒ λp:(le_flatEnv fenv fenv' = true).
+ opt_map ?? (retype_base_Expr fenv resExpr fenv' p)
+ (λresExpr'.Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m)
+ «£(pair ?? resExpr' (ASTFE_BODY fenv' resDecl))»≫))
+ | false ⇒ λp:(le_flatEnv fenv fenv' = false).None ?
+ ] (refl_eq ? (le_flatEnv fenv fenv'))
]]]))
| ne_cons h tl ⇒
opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
(λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
- (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (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
+ (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
+ [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+ [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fenv') (list (astfe_stm fenv'))) ⇒ match mapAndStm with
[ pair m' resDecl ⇒
opt_map ?? (aux fenv' (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) tl)
(λsigmaRes':(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes' with
[ sigma_intro fenv'' mapAndProd ⇒ match mapAndProd with
[ pair m'' tl' ⇒
+ match le_flatEnv fenv fenv''
+ return λx.(le_flatEnv fenv fenv'' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
+ with
+ [ true ⇒ λp:(le_flatEnv fenv fenv'' = true).
+ match le_flatEnv fenv' fenv''
+ return λy.(le_flatEnv fenv' fenv'' = y) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
+ with
+ [ true ⇒ λp':(le_flatEnv fenv' fenv'' = true).
+ opt_map ?? (retype_base_expr fenv resExpr fenv'' p)
+ (λresExpr'.opt_map ?? (retype_stm_list fenv' resDecl fenv'' p')
+ (λresDecl'.
Some ? (≪fenv'',pair ?? m''
- (« pair ?? (retype_base_expr fenv fenv'' resExpr)
- (ASTFE_BODY fenv'' (retype_list_decl fenv' fenv'' resDecl)) £»&tl')≫)
+ («£(pair ?? resExpr'
+ (ASTFE_BODY fenv'' resDecl'))»&tl')≫)))
+ | false ⇒ λp':(le_flatEnv fenv' fenv'' = false).None ?
+ ] (refl_eq ? (le_flatEnv fenv' fenv''))
+ | false ⇒ λp:(le_flatEnv fenv fenv'' = false).None ?
+ ] (refl_eq ? (le_flatEnv fenv fenv''))
]])]]]))
] in
opt_map ?? (aux fe map nelExprDecl)
[ 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)))≫)
+ (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with
+ [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+ [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with
+ [ pair (m'':aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒
+ match le_flatEnv fe' fe''
+ return λz.(le_flatEnv fe' fe'' = z) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
+ with
+ [ true ⇒ λp'':(le_flatEnv fe' fe'' = true).
+ opt_map ?? (retype_exprAndBody_neList fe' resNel fe'' p'')
+ (λresNel'.Some (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
+ (≪fe'',pair ?? (rollback_map e' fe' fe'' f (retype_e_to_leave ?? m'') m')
+ (ASTFE_STM_IF fe'' resNel' (Some ? (ASTFE_BODY fe'' resDecl)))≫))
+ | false ⇒ λp'':(le_flatEnv fe' fe'' = false).None ?
+ ] (refl_eq ? (le_flatEnv fe' fe''))
]]])]]])
]
(*
(check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e
*)
and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on ast
- : Πmap:aux_trasfMap_type e fe.option (Σf.(Σfe'.Prod (aux_trasfMap_type (f e) fe') (list (astfe_stm fe')))) ≝
+ : Πmap:aux_trasfMap_type e fe.option (Σf:aux_trasfEnv_type.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e) fe') (list (astfe_stm fe')))) ≝
match ast
- return λe':aux_env_type.λ_:ast_decl e'.aux_trasfMap_type e' fe → option (Σf.(Σfe'.Prod (aux_trasfMap_type (f e') fe') (list (astfe_stm fe'))))
+ return λe':aux_env_type.λ_:ast_decl e'.aux_trasfMap_type e' fe → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe'))))
with
[ AST_NO_DECL e' lStm ⇒
λmap:aux_trasfMap_type e' fe.
let rec aux (ll:list (ast_stm e')) (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) on ll
- : option (Σf.(Σfe'.Prod (aux_trasfMap_type (f e') fe') (list (astfe_stm fe')))) ≝
+ : option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv 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 ??)) [])
+ [ nil ⇒ let trsf ≝ []
+ in Some ? ≪trsf,≪fenv,pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fenv)
+ (list (astfe_stm fenv))
+ (retype_map_to_id e' fenv (build_trasfEnv trsf) m (refl_eq ? e')) []≫≫
+
| cons h tl ⇒
opt_map ?? (ast_to_astfe_stm e' h fenv m)
(λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')).match sigmaRes with
[ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
[ pair m' resStm ⇒
opt_map ?? (aux tl fenv' m')
- (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type (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
+ (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))).match sigmaRes' with
+ [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
+ [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type ((build_trasfEnv f) e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with
[ pair m'' tl' ⇒
- Some ? (how_to_build_it e' fenv'' f m''
- ((retype_list_decl fenv' fenv'' [ resStm ])@tl'))
+ match le_flatEnv fenv' fenv''
+ return λx.(le_flatEnv fenv' fenv'' = x) → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe'))))
+ with
+ [ true ⇒ λp:(le_flatEnv fenv' fenv'' = true).
+ opt_map ?? (retype_stm_list fenv' [resStm] fenv'' p)
+ (λresStm'.Some ? ≪f,≪fenv'',pair (aux_trasfMap_type ((build_trasfEnv f) e') fenv'')
+ (list (astfe_stm fenv''))
+ m''
+ (resStm'@tl')≫≫)
+ | false ⇒ λp:(le_flatEnv fenv' fenv'' = false).None ?
+ ] (refl_eq ? (le_flatEnv fenv' fenv''))
]]])]])] in
aux lStm fe map
- | AST_DECL e' b name t _ optInit subDecl ⇒
+ | AST_DECL e' b name t dim optInit subDecl ⇒
λmap:aux_trasfMap_type e' fe.
opt_map ?? (match optInit with
[ None ⇒ Some ? []
(λ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))
+ (ast_to_astfe_dec_aux e' name b t fe map dim))
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)
- ])))
+ (λresId.opt_map ?? (retype_init fe t resInit (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
+ (adddescflatenv_to_leflatenv fe (next_nameId e' fe map name) b t))
+ (λresInit'.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t) b t resId resInit' ]))))
])
(λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl
(add_desc_flatEnv fe (next_nameId e' fe map name) b t)
(add_maxcur_map e' fe map map name b t))
- (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (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))
+ (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))).match sigmaRes with
+ [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
+ [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe'))) ⇒ match mapAndStm with
+ [ pair (map':aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') tRes ⇒
+ match le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'
+ return λx.(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = x) → option (Σf'.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f') e') fe') (list (astfe_stm fe'))))
+ with
+ [ true ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = true).
+ opt_map ?? (retype_stm_list (add_desc_flatEnv fe (next_nameId e' fe map name) b t) hRes fe' p)
+ (λhRes'.let trsf ≝ [ tripleT ??? name b t ]@f
+ in Some ? ≪trsf,≪fe',pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fe')
+ (list (astfe_stm fe'))
+ map'
+ (hRes'@tRes)≫≫)
+ | false ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = false).None ?
+ ] (refl_eq ? (le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'))
]]]))
].
[ AST_ROOT 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
+ | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with
+ [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+ [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe) (list (astfe_stm fe))) ⇒ match mapAndStm with
[ pair map resStm ⇒ ≪fe,(ASTFE_ROOT fe (ASTFE_BODY fe resStm))≫
]]]]].
-(* mini test *)
-(*include "compiler/preast_tree.ma".
-include "compiler/preast_to_ast.ma".*)
+(* mini test
+include "compiler/preast_tree.ma".
+include "compiler/preast_to_ast.ma".
-(*
{ const byte8 a;
const byte8[3] b={0,1,2};
byte8[3] c=b;
else
{ const byte8 a=a; }
}
-*)
-(*
+
definition prova ≝
PREAST_ROOT (
PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) (
- PREAST_DECL true [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAL (PREAST_INIT_VAL_ARRAY «(PREAST_INIT_VAL_BYTE8 〈x0,x2〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)»))) (
+ PREAST_DECL true [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAL (PREAST_INIT_VAL_ARRAY «(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x2〉)»))) (
PREAST_DECL false [ch_C] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_B]))) (
PREAST_NO_DECL [
PREAST_STM_IF «
(pair ??
- (PREAST_EXPR_BYTE8 〈xF,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 []))
)
PREAST_DECL false [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_C]))) (PREAST_NO_DECL [])
))
])
+ )
+ £ (pair ??
+ (PREAST_EXPR_BYTE8 〈xF,x2〉)
+ (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ARRAY (PREAST_VAR_ID [ch_B]) (PREAST_EXPR_BYTE8 〈x0,x0〉)))) (PREAST_NO_DECL []))
)
» (Some ? (PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL [])))
]
)
)
).
-
-lemma provacheck : opt_map ?? (preast_to_ast prova) (λres.Some ? (ast_to_astfe res)) = None ?.
-normalize;
*)
projects / helm.git / blobdiff