X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fast_to_astfe.ma;h=d6eadfdb82820b41bca28456742a59bdad6e9fb2;hb=55e5bef77f163b29feeb9ad4e83376c5aa301297;hp=528eeaa47eda0b6d3ade445ed9c26aa3f75d955e;hpb=5061952d0632ba8bc77be5cab11fab2f36e1e26f;p=helm.git diff --git a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma index 528eeaa47..d6eadfdb8 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma @@ -107,38 +107,31 @@ definition get_name_ast_id ≝ λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t. match ast with [ AST_ID s _ ⇒ s ]. -(* NB: avendo poi in input la dimostrazione "check_desc_env e (get_name_ast_id e b t ast)" ha senso *) -axiom ast_to_astfe_id_ax: - Πe:aux_env_type.Πb:bool.Πt:ast_type. Πast:ast_id e b t. Πfe:aux_flatEnv_type. - Πmap:aux_trasfMap_type e fe. - check_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)). - -(* -axiom ax2: - Πe:aux_env_type.Πb:bool.Πt:ast_type. Πast:ast_id e b t. Πfe:aux_flatEnv_type. - Πmap:aux_trasfMap_type e fe. - get_const_desc - (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))) - = b. - -axiom ax3: - Πe:aux_env_type.Πb:bool.Πt:ast_type. Πast:ast_id e b t. Πfe:aux_flatEnv_type. - Πmap:aux_trasfMap_type e fe. - get_type_desc - (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))) = t. -*) - -definition ast_to_astfe_id: +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) @@ -311,6 +304,117 @@ and ast_to_astfe_base_expr (e:aux_env_type) (ast:ast_base_expr e) (fe:aux_flatEn (λ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 @@ -327,19 +431,82 @@ definition ast_to_astfe_init : Πe.Πt.ast_init e t → Πfe.aux_trasfMap_type e | 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). @@ -348,13 +515,14 @@ lemma retype_map_to_id : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:(aux_env_ 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 @@ -370,12 +538,19 @@ let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) λ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 ⇒ @@ -386,28 +561,50 @@ let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) [ 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) @@ -417,13 +614,20 @@ let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) [ 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'')) ]]])]]]) ] (* @@ -433,32 +637,45 @@ let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e *) and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on ast - : Πmap:aux_trasfMap_type e fe.option (Σf.(Σ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 ? [] @@ -467,22 +684,31 @@ and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on (λ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')) ]]])) ]. @@ -494,17 +720,16 @@ definition ast_to_astfe : ast_root → (Σfe.astfe_root 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; @@ -521,20 +746,15 @@ include "compiler/preast_to_ast.ma".*) 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 [])) ) @@ -545,6 +765,10 @@ PREAST_ROOT ( 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 []))) ] @@ -552,7 +776,4 @@ PREAST_ROOT ( ) ) ). - -lemma provacheck : opt_map ?? (preast_to_ast prova) (λres.Some ? (ast_to_astfe res)) = None ?. -normalize; *)