λ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;
*)
destruct H.
qed.
+lemma eq_to_eqastbasetype : ∀t1,t2.t1 = t2 → eq_ast_base_type t1 t2 = true.
+ do 2 intro;
+ elim t1 0;
+ elim t2 0;
+ normalize;
+ intro;
+ try destruct H;
+ reflexivity.
+qed.
+
+definition eq_ast_type_aux ≝
+λT:Type.λf:T → T → bool.
+ let rec aux (nl1,nl2:ne_list T) on nl1 ≝
+ match nl1 with
+ [ ne_nil h ⇒ match nl2 with
+ [ ne_nil h' ⇒ f h h'
+ | ne_cons h' _ ⇒ false
+ ]
+ | ne_cons h t ⇒ match nl2 with
+ [ ne_nil h' ⇒ false
+ | ne_cons h' t' ⇒ (f h h') ⊗ (aux t t')
+ ]
+ ] in aux.
+
let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
match t1 with
[ AST_TYPE_BASE bType1 ⇒ match t2 with
| AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
[ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eqb dim1 dim2) | _ ⇒ false ]
| AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
- [ AST_TYPE_STRUCT nelSubType2 ⇒
- fst ?? (fold_right_neList ?? (λh,t.match fst ?? t with
- [ true ⇒ match nth_neList ? nelSubType2 ((len_neList ? nelSubType2)-(snd ?? t)-1) with
- [ None ⇒ pair ?? false (S (snd ?? t))
- | Some cfr ⇒ match eq_ast_type h cfr with
- [ true ⇒ pair ?? true (S (snd ?? t))
- | false ⇒ pair ?? false (S (snd ?? t)) ]]
- | false ⇒ t]) (pair ?? true O) nelSubType1)
+ [ AST_TYPE_STRUCT nelSubType2 ⇒ eq_ast_type_aux ? eq_ast_type nelSubType1 nelSubType2
| _ ⇒ false ]
].
+lemma eq_ast_type_elim :
+ ∀P:ast_type → Prop.
+ (∀x.P (AST_TYPE_BASE x)) →
+ (∀t:ast_type.∀n.(P t) → (P (AST_TYPE_ARRAY t n))) →
+ (∀x.(P x) → (P (AST_TYPE_STRUCT (ne_nil ? x)))) →
+ (∀x,l.(P x) → (P (AST_TYPE_STRUCT l)) → (P (AST_TYPE_STRUCT (ne_cons ? x l)))) →
+ (∀t.(P t)).
+ intros;
+ apply
+ (let rec aux t ≝
+ match t
+ return λt.P t
+ with
+ [ AST_TYPE_BASE b ⇒ H b
+ | AST_TYPE_ARRAY t n ⇒ H1 t n (aux t)
+ | AST_TYPE_STRUCT l ⇒
+ let rec aux_l (l:ne_list ast_type ) ≝
+ match l
+ return λl.P (AST_TYPE_STRUCT l)
+ with
+ [ ne_nil t => H2 t (aux t)
+ | ne_cons hd tl => H3 hd tl (aux hd) (aux_l tl)
+ ] in aux_l l
+ ] in aux t);
+qed.
+
lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2).
intro;
- elim t1 0; [1,3:intros 2 | intros 4] elim t2;
- [ 2,5,7,9: normalize in H1; destruct H1;
- | 3,4: normalize in H; destruct H;
- | 1: simplify in H;
- apply (eq_f ?? (λx.? x) a a1 (eqastbasetype_to_eq a a1 H))
- | 8: simplify in H2;
- lapply (andb_true_true ? ? H2);
- lapply (andb_true_true_r ? ? H2); clear H2;
- rewrite > (H ? Hletin);
- rewrite > (eqb_true_to_eq ?? Hletin1);
- reflexivity
- | 6: elim daemon;
+ elim t1 using eq_ast_type_elim 0;
+ [ 1: intros 2;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: intros;
+ simplify in H;
+ rewrite > (eqastbasetype_to_eq ?? H);
+ reflexivity
+ | 2: simplify;
+ intros;
+ destruct H1
+ | 3: simplify;
+ intros;
+ destruct H1
+ | 4: simplify;
+ intros;
+ destruct H2
+ ]
+ | 2: intros 4;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H1
+ | 2: simplify;
+ intros;
+ lapply (andb_true_true ?? H2) as H3;
+ lapply (andb_true_true_r ?? H2) as H4;
+ rewrite > (H ? H3);
+ rewrite > (eqb_true_to_eq ?? H4);
+ reflexivity
+ | 3: simplify;
+ intros;
+ destruct H2
+ | 4: simplify;
+ intros;
+ destruct H3
+ ]
+ | 3: intros 3;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H1
+ | 2: simplify;
+ intros;
+ destruct H2
+ | 3: intros;
+ simplify in H2;
+ rewrite > (H x1);
+ [ reflexivity
+ | apply H2
+ ]
+ | 4: intros;
+ simplify in H3;
+ destruct H3
+ ]
+ | 4: intros 5;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H2
+ | 2: simplify;
+ intros;
+ destruct H3
+ | 3: simplify;
+ intros;
+ destruct H3
+ | 4: intros;
+ simplify in H4;
+ lapply (andb_true_true ?? H4) as H5;
+ lapply (andb_true_true_r ?? H4) as H6;
+ rewrite > (H ? H5);
+ lapply depth=0 (H1 (AST_TYPE_STRUCT l1)) as K;
+ destruct (K ?);
+ [ apply H6
+ | reflexivity
+ ]
+ ]
+ ].
+qed.
+
+lemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_ast_type t1 t2 = true.
+ intro;
+ elim t1 using eq_ast_type_elim 0;
+ [ 1: intros 2;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H;
+ apply (eq_to_eqastbasetype x x (refl_eq ??))
+ | 2: simplify;
+ intros;
+ destruct H1
+ | 3: simplify;
+ intros;
+ destruct H1
+ | 4: simplify;
+ intros;
+ destruct H2
+ ]
+ | 2: intros 4;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H1
+ | 2: intros;
+ simplify;
+ destruct H2;
+ rewrite > (H t (refl_eq ??));
+ rewrite > (eq_to_eqb_true n n (refl_eq ??));
+ reflexivity
+ | 3: simplify;
+ intros;
+ destruct H2
+ | 4: simplify;
+ intros;
+ destruct H3
+ ]
+ | 3: intros 3;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H1
+ | 2: simplify;
+ intros;
+ destruct H2
+ | 3: intros;
+ simplify;
+ destruct H2;
+ rewrite > (H x (refl_eq ??));
+ reflexivity
+ | 4: simplify;
+ intros;
+ destruct H3
+ ]
+ | 4: intros 5;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H2
+ | 2: simplify;
+ intros;
+ destruct H3
+ | 3: simplify;
+ intros;
+ destruct H3
+ | 4: intros;
+ simplify;
+ destruct H4;
+ rewrite > (H x (refl_eq ??));
+ rewrite > (H1 (AST_TYPE_STRUCT l) (refl_eq ??));
+ reflexivity
+ ]
].
qed.
let rec get_desc_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) on e ≝
match e with
[ nil ⇒ None ?
- | cons h tl ⇒ match strCmp_strId str (get_nameId_flatVar h) with
+ | cons h tl ⇒ match eqStrId_str str (get_nameId_flatVar h) with
[ true ⇒ Some ? (get_desc_flatVar h)
| false ⇒ get_desc_flatEnv_aux tl str ]].
normalize; autobatch ]
qed.
-(* aggiungi descrittore ad ambiente: in testa *)
+(* aggiungi descrittore ad ambiente: in coda *)
definition add_desc_flatEnv ≝
λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
- (VAR_FLAT_ELEM str (DESC_ELEM b t))::e.
+ e@[VAR_FLAT_ELEM str (DESC_ELEM b t)].
+
+(* controllo fe <= fe' *)
+definition eq_flatEnv_elem ≝
+λe1,e2.match e1 with
+ [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
+ [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
+
+lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
+ intros 3;
+ rewrite < H;
+ elim e1;
+ simplify;
+ rewrite > (eq_to_eqstrid a a (refl_eq ??));
+ rewrite > (eq_to_eqdescelem d d (refl_eq ??));
+ reflexivity.
+qed.
+
+lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
+ intros 2;
+ elim e1 0;
+ elim e2 0;
+ intros 4;
+ simplify;
+ intro;
+ rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
+ rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
+ reflexivity.
+qed.
+
+let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
+match fe with
+ [ nil ⇒ true
+ | cons h tl ⇒ match fe' with
+ [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
+ ].
+
+lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
+ intro;
+ elim fe 0;
+ [ intros; exists; [ apply fe' | reflexivity ]
+ | intros 4; elim fe';
+ [ simplify in H1:(%); destruct H1
+ | simplify in H2:(%);
+ rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
+ cases (H l1 (andb_true_true_r ?? H2));
+ simplify;
+ rewrite < H3;
+ exists; [ apply x | reflexivity ]
+ ]
+ ].
+qed.
+
+lemma leflatenv_to_check : ∀fe,fe',str.
+ (le_flatEnv fe fe' = true) →
+ (check_desc_flatEnv fe str) →
+ (check_desc_flatEnv fe' str).
+ intros 4;
+ cases (leflatEnv_to_le fe fe' H);
+ rewrite < H1;
+ elim fe 0;
+ [ intro; simplify in H2:(%); elim H2;
+ | intros 3;
+ simplify;
+ cases (eqStrId_str str (get_nameId_flatVar a));
+ [ simplify; intro; apply H3
+ | simplify;
+ apply H2
+ ]
+ ].
+qed.
+
+lemma adddescflatenv_to_leflatenv : ∀fe,n,b,t.le_flatEnv fe (add_desc_flatEnv fe n b t) = true.
+intros;
+ change in ⊢ (? ? (? ? %) ?) with (fe@[VAR_FLAT_ELEM n (DESC_ELEM b t)]);
+ elim fe 0;
+ [ 1: reflexivity
+ | 2: do 3 intro;
+ unfold le_flatEnv;
+ change in ⊢ (? ? % ?) with ((eq_flatEnv_elem a a)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)])));
+ unfold eq_flatEnv_elem;
+ elim a;
+ change in ⊢ (? ? % ?) with ((eqStrId_str a1 a1)⊗(eqDesc_elem d d)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)])));
+ rewrite > (eq_to_eqstrid a1 a1 (refl_eq ??));
+ rewrite > (eq_to_eqdescelem d d (refl_eq ??));
+ rewrite > H;
+ reflexivity
+ ].
+qed.
(* STRUTTURA MAPPA TRASFORMAZIONE *)
let rec get_maxcur_map (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) (str:aux_str_type) on map ≝
match map with
[ nil ⇒ None ?
- | cons h tl ⇒ match strCmp_str str (get_name_maxCur e fe h) with
+ | cons h tl ⇒ match eqStr_str str (get_name_maxCur e fe h) with
[ true ⇒ Some ? h | false ⇒ get_maxcur_map e fe tl str ]].
(* prossimo nome *)
axiom add_maxcur_map_aux_false : ∀e,fe,str,cur,str',b',desc',map.
(check_desc_env e str →
get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
-(strCmp_str str str' = false) →
+(eqStr_str str str' = false) →
(check_desc_env (add_desc_env e str' b' desc') str →
get_desc_env (add_desc_env e str' b' desc') str =
get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str cur)).
axiom add_maxcur_map_aux_true : ∀e,fe,str,cur,max,str',b',desc',map.
(check_desc_env e str →
get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
-(strCmp_str str str' = true) →
+(eqStr_str str str' = true) →
(check_desc_env (add_desc_env e str' b' desc') str →
get_desc_env (add_desc_env e str' b' desc') str =
get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str (S max))).
+axiom add_maxcur_map_aux_new : ∀e,fe,str,b,desc,map.
+ check_desc_env (add_desc_env e str b desc) str →
+ get_desc_env (add_desc_env e str b desc) str =
+ get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str) b desc) (STR_ID str 0).
+
+(* 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_aux : ∀e,fe.∀map:aux_trasfMap_type e fe.∀str.
+ check_desc_env e str → check_desc_flatEnv fe (name_to_nameId e fe map str).
+
+axiom ast_to_astfe_dec_aux : ∀e,str,b,t,fe,map.
+ check_not_already_def_env e str →
+ check_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str) b t) (next_nameId e fe map str).
+
(* aggiungi/aggiorna descrittore mappa trasformazione *)
let rec add_maxcur_map_aux (e:aux_env_type) (fe:aux_flatEnv_type) (map,fMap:aux_trasfMap_type e fe)
(str:aux_str_type) (b:bool) (desc:ast_type) (flag:bool) on map
[ true ⇒ []
| false ⇒
[ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
- str O O (False_rect ? daemon) ]
+ str 0 0 (add_maxcur_map_aux_new e fe str b desc fMap) ]
]
| cons h tl ⇒ match h with
[ MAX_CUR_ELEM str' cur' max' dim' ⇒
- match strCmp_str str' str return λx.(strCmp_str str' str = x) → ? with
- [ true ⇒ λp:(strCmp_str str' str = true).
+ match eqStr_str str' str return λx.(eqStr_str str' str = x) → ? with
+ [ true ⇒ λp:(eqStr_str str' str = true).
[ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
str' (S max') (S max')
(add_maxcur_map_aux_true e fe str' cur' max' str b desc fMap dim' p)
]@(add_maxcur_map_aux e fe tl fMap str b desc true)
- | false ⇒ λp:(strCmp_str str' str = false).
+ | false ⇒ λp:(eqStr_str str' str = false).
[ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
str' cur' max'
(add_maxcur_map_aux_false e fe str' cur' str b desc fMap dim' p)
]@(add_maxcur_map_aux e fe tl fMap str b desc flag)
- ] (refl_eq ? (strCmp_str str' str))
+ ] (refl_eq ? (eqStr_str str' str))
]
].
λe:aux_env_type.λfe:aux_flatEnv_type.λmap,fMap:aux_trasfMap_type e fe.λstr:aux_str_type.λb:bool.λdesc:ast_type.
add_maxcur_map_aux e fe map fMap str b desc false.
+(* composizione di funzioni generata da una lista di nome x const x tipo *)
+definition aux_trasfEnv_type ≝ list (Prod3T aux_str_type bool ast_type).
+
+let rec build_trasfEnv (trasf:aux_trasfEnv_type) on trasf : aux_env_type → aux_env_type ≝
+ match trasf with
+ [ nil ⇒ (λx.x)
+ | cons h tl ⇒ (λx.(build_trasfEnv tl) (add_desc_env x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
+ ].
+
+lemma build_trasfEnv_exists_aux : ∀a.∀trsf:aux_trasfEnv_type.∀c.
+ ∃b.build_trasfEnv trsf (c§§a) = (b§§a).
+ intros 2;
+ elim trsf;
+ [ simplify; exists; [apply c | reflexivity]
+ | simplify; apply H; ]
+qed.
+
+lemma eq_enter_leave : ∀e,trsf.leave_env (build_trasfEnv trsf (enter_env e)) = e.
+ intros;
+ change in ⊢ (? ? (? (? ? %)) ?) with ([]§§e);
+ cases (build_trasfEnv_exists_aux e trsf []);
+ rewrite > H;
+ reflexivity.
+qed.
+
(* NB: leave ... enter e' equivalente a e originale *)
-axiom retype_enter_leave_to_e: ∀e,fe,f. aux_trasfMap_type (leave_env (f (enter_env e))) fe → aux_trasfMap_type e fe.
+lemma retype_enter_leave_to_e_aux : ∀e,fe,str,cur,trsf.
+ (check_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str →
+ get_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str = get_desc_flatEnv fe (STR_ID str cur)) →
+ (check_desc_env e str →
+ get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)).
+ intros 5;
+ rewrite > (eq_enter_leave e trsf);
+ intros;
+ apply H;
+ apply H1.
+qed.
+
+let rec retype_enter_leave_to_e (e:aux_env_type) (fe:aux_flatEnv_type) (trsf:aux_trasfEnv_type)
+ (map:aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe) on map : aux_trasfMap_type e fe ≝
+ match map with
+ [ nil ⇒ []
+ | cons h tl ⇒ match h with
+ [ MAX_CUR_ELEM str cur max dim ⇒
+ [MAX_CUR_ELEM e fe str cur max (retype_enter_leave_to_e_aux e fe str cur trsf dim)]@(retype_enter_leave_to_e e fe trsf tl)
+ ]].
+
+lemma retype_e_to_enter_leave_aux : ∀e,fe,str,cur,trsf.
+ (check_desc_env e str →
+ get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
+ (check_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str →
+ get_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str = get_desc_flatEnv fe (STR_ID str cur)).
+ intros 5;
+ rewrite < (eq_enter_leave e trsf) in ⊢ ((? % ?→?)→?);
+ rewrite < (eq_enter_leave e trsf) in ⊢ ((?→? ? (? % ?) ?)→?);
+ intros;
+ apply H;
+ apply H1.
+qed.
+
+let rec retype_e_to_enter_leave (e:aux_env_type) (fe:aux_flatEnv_type) (trsf:aux_trasfEnv_type)
+ (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe ≝
+ match map with
+ [ nil ⇒ []
+ | cons h tl ⇒ match h with
+ [ MAX_CUR_ELEM str cur max dim ⇒
+ [MAX_CUR_ELEM (leave_env ((build_trasfEnv trsf) (enter_env e))) fe str cur max (retype_e_to_enter_leave_aux e fe str cur trsf dim)]@(retype_e_to_enter_leave e fe trsf tl)
+ ]].
+
(* NB: enter non cambia fe *)
-axiom retype_e_to_enter: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (enter_env e) fe.
+lemma retype_e_to_enter_aux : ∀e,fe,str,cur.
+ (check_desc_env e str →
+ get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
+ (check_desc_env (enter_env e) str →
+ get_desc_env (enter_env e) str = get_desc_flatEnv fe (STR_ID str cur)).
+ intros 6;
+ rewrite > H;
+ [ reflexivity
+ | apply H1
+ ].
+qed.
+
+let rec retype_e_to_enter (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (enter_env e) fe ≝
+ match map with
+ [ nil ⇒ []
+ | cons h tl ⇒ match h with
+ [ MAX_CUR_ELEM str cur max dim ⇒
+ [MAX_CUR_ELEM (enter_env e) fe str cur max (retype_e_to_enter_aux e fe str cur dim)]@(retype_e_to_enter e fe tl)
+ ]].
+
(* NB: leave non cambia fe *)
-axiom retype_e_to_leave: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (leave_env e) fe.
+axiom retype_e_to_leave_aux : ∀e,fe,str,cur.
+ (check_desc_env e str →
+ get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
+ (check_desc_env (leave_env e) str →
+ get_desc_env (leave_env e) str = get_desc_flatEnv fe (STR_ID str cur)).
+
+let rec retype_e_to_leave (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (leave_env e) fe ≝
+ match map with
+ [ nil ⇒ []
+ | cons h tl ⇒ match h with
+ [ MAX_CUR_ELEM str cur max dim ⇒
+ [MAX_CUR_ELEM (leave_env e) fe str cur max (retype_e_to_leave_aux e fe str cur dim)]@(retype_e_to_leave e fe tl)
+ ]].
-let rec rollback_map (e:aux_env_type) (fe,fe':aux_flatEnv_type) (f:aux_env_type → aux_env_type) (map:aux_trasfMap_type (leave_env (f (enter_env e))) fe')
+let rec rollback_map (e:aux_env_type) (fe,fe':aux_flatEnv_type) (trsf:aux_trasfEnv_type) (map:aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe')
(snap:aux_trasfMap_type e fe) on map : aux_trasfMap_type e fe' ≝
match map with
[ nil ⇒ empty_trasfMap e fe'
| cons h tl ⇒
match get_maxcur_map e fe snap (get_name_maxCur ?? h) with
- [ None ⇒ retype_enter_leave_to_e e fe' f [h]
+ [ None ⇒ retype_enter_leave_to_e e fe' trsf [h]
| Some new ⇒
[ MAX_CUR_ELEM ?? (get_name_maxCur ?? h) (get_cur_maxCur ?? new)
(get_max_maxCur ?? h) (False_rect ? daemon) ]
- ] @ rollback_map e fe fe' f tl snap
+ ] @ rollback_map e fe fe' trsf tl snap
].
(* sequenza di utilizzo:
| ...
*)
-(* mini test
+(* mini test
definition pippo ≝ [ ch_P ].
definition pluto ≝ [ ch_Q ].
definition pippodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
definition map6' ≝ retype_e_to_leave env6 fenv6 map6.
-definition map7 ≝ rollback_map env4 fenv4 fenv6 (λx.add_desc_env (add_desc_env x pippo false pippodesc3) pluto false plutodesc3) map6' map4.
+definition map7 ≝ rollback_map env4 fenv4 fenv6 [ tripleT ??? pluto false plutodesc3 ; tripleT ??? pippo false pippodesc3 ] map6' map4.
definition map7' ≝ retype_e_to_leave env4 fenv6 map7.
-definition map8 ≝ rollback_map env2 fenv2 fenv6 (λx.add_desc_env (add_desc_env x pippo true pippodesc2) pluto true plutodesc2) map7' map2.
+definition map8 ≝ rollback_map env2 fenv2 fenv6 [ tripleT ??? pluto true plutodesc2 ; tripleT ??? pippo true pippodesc2 ] map7' map2.
*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* *)
+(* Sviluppato da: *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "compiler/environment.ma".
+
+(* ********************** *)
+(* GESTIONE AMBIENTE FLAT *)
+(* ********************** *)
+
+(* elemento: name + nel curId + nel desc *)
+inductive var_flatElem : Type ≝
+VAR_FLAT_ELEM: aux_str_type → ne_list (option nat) → ne_list desc_elem → var_flatElem.
+
+definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ _ ⇒ n ].
+definition get_cur_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ c _ ⇒ c ].
+definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ _ d ⇒ d ].
+
+(* ambiente globale: descrittori *)
+definition aux_flatEnv_type ≝ Prod nat (list var_flatElem).
+
+(* ambiente vuoto *)
+definition empty_flatEnv ≝ pair ?? O (nil var_flatElem).
+
+definition get_depth_flatEnv ≝ λenv:aux_flatEnv_type.match env with [ pair d _ ⇒ d ].
+definition get_subEnv_flatEnv ≝ λenv:aux_flatEnv_type.match env with [ pair _ s ⇒ s ].
+
+(* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
+let rec enter_flatEnv_aux (subEnv:list var_flatElem) on subEnv ≝
+ match subEnv with
+ [ nil ⇒ []
+ | cons h t ⇒ (VAR_FLAT_ELEM (get_name_flatVar h)
+ ((get_first_neList ? (get_cur_flatVar h))§§(get_cur_flatVar h))
+ (get_desc_flatVar h))::(enter_flatEnv_aux t)
+ ].
+
+definition enter_flatEnv ≝
+λenv.pair ?? (get_depth_flatEnv env) (enter_flatEnv_aux (get_subEnv_flatEnv env)).
+
+(* leave: elimina la testa (il "cur" corrente) *)
+let rec leave_flatEnv_aux (subEnv:list var_flatElem) on subEnv ≝
+ match subEnv with
+ [ nil ⇒ []
+ | cons h t ⇒ (VAR_FLAT_ELEM (get_name_flatVar h)
+ (cut_first_neList ? (get_cur_flatVar h))
+ (get_desc_flatVar h))::(leave_flatEnv_aux t)
+ ].
+
+definition leave_flatEnv ≝
+λenv.pair ?? (get_depth_flatEnv env) (leave_flatEnv_aux (get_subEnv_flatEnv env)).
+
+(* get_id *)
+let rec get_id_flatEnv_aux (subEnv:list var_flatElem) (name:aux_str_type) on subEnv ≝
+ match subEnv with
+ [ nil ⇒ None ?
+ | cons h t ⇒
+ match (match eqStr_str name (get_name_flatVar h) with
+ [ true ⇒ get_first_neList ? (get_cur_flatVar h)
+ | false ⇒ None ?
+ ]) with
+ [ None ⇒ get_id_flatEnv_aux t name
+ | Some x ⇒ Some ? x
+ ]
+ ].
+
+definition get_id_flatEnv ≝
+λe:aux_flatEnv_type.λstr:aux_str_type.
+ match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with
+ [ None ⇒ O | Some x ⇒ x ].
+
+(* get_desc *)
+let rec get_desc_flatEnv_aux (subEnv:list var_flatElem) (name:aux_strId_type) on subEnv ≝
+ match subEnv with
+ [ nil ⇒ None ?
+ | cons h t ⇒
+ match (match (eqStr_str (get_name_strId name) (get_name_flatVar h))⊗
+ (leb (S (get_id_strId name)) (len_neList ? (get_desc_flatVar h))) with
+ [ true ⇒ nth_neList ? (get_desc_flatVar h) (get_id_strId name)
+ | false ⇒ None ?
+ ]) with
+ [ None ⇒ get_desc_flatEnv_aux t name
+ | Some x ⇒ Some ? x
+ ]
+ ].
+
+definition get_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with
+ [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
+
+(* check_id *)
+definition check_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type.
+ match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ False | Some _ ⇒ True ].
+
+definition checkb_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type.
+ match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ false | Some _ ⇒ true ].
+
+lemma checkbidflatenv_to_checkidflatenv : ∀e,str.checkb_id_flatEnv e str = true → check_id_flatEnv e str.
+ unfold checkb_id_flatEnv;
+ unfold check_id_flatEnv;
+ intros;
+ letin K ≝ (get_id_flatEnv_aux (get_subEnv_flatEnv e) str);
+ elim K;
+ [ normalize; autobatch |
+ normalize; autobatch ]
+qed.
+
+definition checknot_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type.
+ match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ True | Some _ ⇒ False ].
+
+definition checknotb_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type.
+ match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ true | Some _ ⇒ false ].
+
+lemma checknotbidflatenv_to_checknotidflatenv : ∀e,str.checknotb_id_flatEnv e str = true → checknot_id_flatEnv e str.
+ unfold checknotb_id_flatEnv;
+ unfold checknot_id_flatEnv;
+ intros;
+ letin K ≝ (get_id_flatEnv_aux (get_subEnv_flatEnv e) str);
+ elim K;
+ [ normalize; autobatch |
+ normalize; autobatch ]
+qed.
+
+(* check_desc *)
+definition check_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ False | Some _ ⇒ True ].
+
+definition checkb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ false | Some _ ⇒ true ].
+
+lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str = true → check_desc_flatEnv e str.
+ unfold checkb_desc_flatEnv;
+ unfold check_desc_flatEnv;
+ intros;
+ letin K ≝ (get_desc_flatEnv_aux (get_subEnv_flatEnv e) str);
+ elim K;
+ [ normalize; autobatch |
+ normalize; autobatch ]
+qed.
+
+definition checknot_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ True | Some _ ⇒ False ].
+
+definition checknotb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ true | Some _ ⇒ false ].
+
+lemma checknotbdescflatenv_to_checknotdescflatenv : ∀e,str.checknotb_desc_flatEnv e str = true → checknot_desc_flatEnv e str.
+ unfold checknotb_desc_flatEnv;
+ unfold checknot_desc_flatEnv;
+ intros;
+ letin K ≝ (get_desc_flatEnv_aux (get_subEnv_flatEnv e) str);
+ elim K;
+ [ normalize; autobatch |
+ normalize; autobatch ]
+qed.
+
+(* aggiungi descrittore : in testa al primo ambiente *)
+let rec previous_cur_from_depth (depth:nat) on depth ≝
+ match depth with
+ [ O ⇒ «£(Some ? O)»
+ | S n ⇒ (previous_cur_from_depth n)&«£(None ?)»
+ ].
+
+let rec add_desc_flatEnv_aux (subEnv:list var_flatElem) (str:aux_str_type) (c:bool) (desc:ast_type) (depth:nat) (flag:bool) on subEnv ≝
+ match subEnv with
+ [ nil ⇒ match flag with
+ [ true ⇒ []
+ | false ⇒ [ VAR_FLAT_ELEM str (previous_cur_from_depth depth) «£(DESC_ELEM c desc)» ]
+ ]
+ | cons h t ⇒ (match eqStr_str str (get_name_flatVar h) with
+ [ true ⇒ VAR_FLAT_ELEM (get_name_flatVar h)
+ («£(Some ? (len_neList ? (get_desc_flatVar h)))»&(cut_first_neList ? (get_cur_flatVar h)))
+ ((get_desc_flatVar h)&«£(DESC_ELEM c desc)»)
+ | false ⇒ h
+ ])::(add_desc_flatEnv_aux t str c desc depth ((eqStr_str str (get_name_flatVar h)⊕flag)))
+ ].
+
+definition add_desc_flatEnv ≝ λenv,str,c,desc.add_desc_flatEnv_aux (get_subEnv_flatEnv env) str c desc (get_depth_flatEnv env) false.
+
+(* equivalenza *)
+definition env_to_flatEnv ≝
+ λe,fe.∀str.
+ check_desc_env e str →
+ check_id_flatEnv fe str →
+ check_desc_flatEnv fe (STR_ID str (get_id_flatEnv fe str)) →
+ get_desc_env e str = get_desc_flatEnv fe (STR_ID str (get_id_flatEnv fe str)).
+
+lemma empty_env_to_flatEnv : env_to_flatEnv empty_env empty_flatEnv.
+ unfold env_to_flatEnv;
+ unfold empty_env;
+ unfold empty_flatEnv;
+ simplify;
+ intros;
+ reflexivity.
+qed.
+
+lemma getdescenv_to_enter : ∀e,str.get_desc_env e str = get_desc_env (enter_env e) str.
+ intros 2;
+ elim e;
+ reflexivity.
+qed.
+
+lemma enter_env_to_flatEnv :
+ ∀e,fe.env_to_flatEnv e fe → env_to_flatEnv (enter_env e) (enter_flatEnv fe).
+ intros 2;
+ unfold env_to_flatEnv;
+ intros;
+ lapply (H str H1);
+ [ rewrite < (getdescenv_to_enter e str);
+ rewrite > Hletin;
+
+
+
+
+
+
+
+
+
+
definition get_const_desc ≝ λd:desc_elem.match d with [ DESC_ELEM c _ ⇒ c ].
definition get_type_desc ≝ λd:desc_elem.match d with [ DESC_ELEM _ t ⇒ t ].
+definition eqDesc_elem ≝ λd,d'.(eq_bool (get_const_desc d) (get_const_desc d'))⊗(eq_ast_type (get_type_desc d) (get_type_desc d')).
+
+lemma eq_to_eqdescelem : ∀d,d'.d = d' → eqDesc_elem d d' = true.
+ intros 3;
+ rewrite < H;
+ elim d;
+ simplify;
+ rewrite > (eq_to_eqbool b b (refl_eq ??));
+ rewrite > (eq_to_eqasttype a a (refl_eq ??));
+ reflexivity.
+qed.
+
+lemma eqdescelem_to_eq : ∀d,d'.eqDesc_elem d d' = true → d = d'.
+ intros 2;
+ elim d 0;
+ elim d' 0;
+ intros 4;
+ simplify;
+ intro;
+ rewrite > (eqbool_to_eq b1 b (andb_true_true ?? H));
+ rewrite > (eqasttype_to_eq a1 a (andb_true_true_r ?? H));
+ reflexivity.
+qed.
+
definition get_name_var ≝ λv:var_elem.match v with [ VAR_ELEM n _ ⇒ n ].
definition get_desc_var ≝ λv:var_elem.match v with [ VAR_ELEM _ d ⇒ d ].
(* ambiente vuoto *)
definition empty_env ≝ ne_nil ? (nil var_elem ).
-(* confronto *)
-let rec eq_aux_env_type_aux (subE,subE':list var_elem) on subE ≝
- match subE with
- [ nil ⇒ match subE' with
- [ nil ⇒ true | cons _ _ ⇒ false ]
- | cons h tl ⇒ match subE' with
- [ nil ⇒ false | cons h' tl' ⇒ (strCmp_str (get_name_var h) (get_name_var h'))⊗
- (eq_bool (get_const_desc (get_desc_var h)) (get_const_desc (get_desc_var h')))⊗
- (eq_ast_type (get_type_desc (get_desc_var h)) (get_type_desc (get_desc_var h')))⊗
- (eq_aux_env_type_aux tl tl') ]
- ].
-
-axiom eqbauxenvtypeaux_to_eq : ∀e,e'.eq_aux_env_type_aux e e' = true → e = e'.
-
-let rec eq_aux_env_type (e,e':aux_env_type) on e ≝
- match e with
- [ ne_nil h ⇒ match e' with
- [ ne_nil h' ⇒ eq_aux_env_type_aux h h' | ne_cons _ _ ⇒ false ]
- | ne_cons h tl ⇒ match e' with
- [ ne_nil h' ⇒ false | ne_cons h' tl' ⇒ (eq_aux_env_type_aux h h')⊗(eq_aux_env_type tl tl') ]
- ].
-
-axiom eqbauxenvtype_to_eq : ∀e,e':aux_env_type.eq_aux_env_type e e' = true → e = e'.
-
(* setter *)
definition enter_env ≝ λe:aux_env_type.empty_env&e.
definition leave_env ≝ λe:aux_env_type.cut_first_neList ? e.
let rec get_desc_from_lev_env (env:list var_elem ) (str:aux_str_type) on env ≝
match env with
[ nil ⇒ None ?
- | cons h t ⇒ match strCmp_str str (get_name_var h) with
+ | cons h t ⇒ match eqStr_str str (get_name_var h) with
[ true ⇒ Some ? (get_desc_var h)
| false ⇒ get_desc_from_lev_env t str ]].
(*let var ≝ VAR_ELEM str (DESC_ELEM c desc) in*)
match e with
[ ne_nil h ⇒ ne_nil ? ((VAR_ELEM str (DESC_ELEM c desc))::h)
- | ne_cons h tl ⇒ «((VAR_ELEM str (DESC_ELEM c desc))::h) £ »&tl
+ | ne_cons h tl ⇒ «£((VAR_ELEM str (DESC_ELEM c desc))::h)»&tl
].
+
+(* controllo e <= e' *)
+definition eq_env_elem ≝
+λe1,e2.match e1 with
+ [ VAR_ELEM s1 d1 ⇒ match e2 with
+ [ VAR_ELEM s2 d2 ⇒ (eqStr_str s1 s2)⊗(eqDesc_elem d1 d2) ]].
+
+lemma eq_to_eqenv : ∀e1,e2.e1 = e2 → eq_env_elem e1 e2 = true.
+ intros 3;
+ rewrite < H;
+ elim e1;
+ simplify;
+ rewrite > (eq_to_eqstr a a (refl_eq ??));
+ rewrite > (eq_to_eqdescelem d d (refl_eq ??));
+ reflexivity.
+qed.
+
+lemma eqenv_to_eq : ∀e1,e2.eq_env_elem e1 e2 = true → e1 = e2.
+ intros 2;
+ elim e1 0;
+ elim e2 0;
+ intros 4;
+ simplify;
+ intro;
+ rewrite > (eqstr_to_eq a1 a (andb_true_true ?? H));
+ rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
+ reflexivity.
+qed.
λt:ast_type.λn:nat.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_ARRAY t n)).x.
definition preast_to_ast_init_val_aux_struct :
-Πt.Πnel.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)) → (aux_ast_init_type (AST_TYPE_STRUCT («t£»&nel))) ≝
+Πt.Πnel.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)) → (aux_ast_init_type (AST_TYPE_STRUCT («£t»&nel))) ≝
λt:ast_type.λnel:ne_list ast_type.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)).x.
let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (Σt.aux_ast_init_type t) ≝
[ ne_nil h ⇒
opt_map ?? (preast_to_ast_init_val_aux h)
(λsigmaRes:(Σt.aux_ast_init_type t).match sigmaRes with [ sigma_intro t res ⇒
- Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT (« t £»)),res≫ ])
+ Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («£t»)),res≫ ])
| ne_cons h tl ⇒
opt_map ?? (preast_to_ast_init_val_aux h)
(λsigmaRes1:(Σt.aux_ast_init_type t).opt_map ?? (aux tl)
return λx.(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = x) → option (Σt.aux_ast_init_type t)
with
[ true ⇒ λp:(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = true).
- Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («t1£»&nelSubType)),
+ Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («£t1»&nelSubType)),
(preast_to_ast_init_val_aux_struct ??
(pair (aux_ast_init_type t1) (aux_ast_init_type (AST_TYPE_STRUCT nelSubType))
res1
opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (preast_to_ast_base_expr (fst ?? h) e)
(λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) (enter_env e))
(λresDecl.opt_map ?? t
- (λt'.Some ? («(pair ?? resExpr resDecl)£»&t')))))
+ (λt'.Some ? («£(pair ?? resExpr resDecl)»&t')))))
(Some ? (ne_nil ? (pair ?? (AST_BASE_EXPR e AST_BASE_TYPE_BYTE8 (AST_EXPR_BYTE8 e 〈x0,x0〉)) (AST_NO_DECL (enter_env e) (nil ?)))))
nelExprDecl)
(λres.match optDecl with
PREAST_DECL true [ ch_Q ] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (None ?) (
PREAST_NO_DECL [
PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x0,x0〉) (
- PREAST_DECL false [ ch_P ] (AST_TYPE_STRUCT «(AST_TYPE_BASE AST_BASE_TYPE_BYTE8)£(AST_TYPE_BASE AST_BASE_TYPE_WORD16)») (None ?) (
+ PREAST_DECL false [ ch_P ] (AST_TYPE_STRUCT «(AST_TYPE_BASE AST_BASE_TYPE_WORD16)£(AST_TYPE_BASE AST_BASE_TYPE_BYTE8)») (None ?) (
PREAST_NO_DECL [
PREAST_STM_ASG (PREAST_VAR_STRUCT (PREAST_VAR_ID [ ch_P ]) 1) (PREAST_EXPR_ID (PREAST_VAR_ARRAY (PREAST_VAR_ID [ ch_Q ]) (PREAST_EXPR_BYTE8 〈x0,x1〉)))
]
right associative with precedence 46
for @{'ne_cons $hd $tl}.
-notation "« y break £ list0 x sep ; break »"
+notation "« list0 x sep ; break £ y break »"
non associative with precedence 90
for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}.
match p_l with [ ne_nil h ⇒ [h] | ne_cons h t ⇒ [h]@neList_to_list T t ].
let rec list_to_neList (T:Type) (p_l:list T) on p_l ≝
- match p_l with [ nil ⇒ None (ne_list T) | cons h t ⇒ match list_to_neList T t with [ None ⇒ Some ? «h£» | Some t' ⇒ Some ? («h£»&t') ]].
+ match p_l with [ nil ⇒ None (ne_list T) | cons h t ⇒ match list_to_neList T t with [ None ⇒ Some ? «£h» | Some t' ⇒ Some ? («£h»&t') ]].
(* listlen *)
-let rec len_list_aux (T:Type) (p_l:list T) (c:nat) on p_l ≝
- match p_l with [ nil ⇒ c | cons _ t ⇒ len_list_aux T t (S c) ].
+let rec len_list (T:Type) (p_l:list T) on p_l ≝
+ match p_l with [ nil ⇒ O | cons _ t ⇒ S (len_list T t) ].
-definition len_list ≝ λT:Type.λl:list T.len_list_aux T l O.
-
-let rec len_neList_aux (T:Type) (p_l:ne_list T) (c:nat) on p_l ≝
- match p_l with [ ne_nil _ ⇒ (S c) | ne_cons _ t ⇒ len_neList_aux T t (S c) ].
-
-definition len_neList ≝ λT:Type.λl:ne_list T.len_neList_aux T l O.
+let rec len_neList (T:Type) (p_l:ne_list T) on p_l ≝
+ match p_l with [ ne_nil _ ⇒ 1 | ne_cons _ t ⇒ S (len_neList T t) ].
(* nth elem *)
let rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
normalize; autobatch ]
qed.
+lemma isempty_to_eq : ∀T,l.isb_empty_list T l = true → l = [].
+ do 2 intro;
+ elim l 0;
+ [ 1: intro; reflexivity
+ | 2: intros; normalize in H1:(%); destruct H1
+ ].
+qed.
+
+lemma eq_to_isempty : ∀T,l.l = [] → isb_empty_list T l = true.
+ do 2 intro;
+ elim l 0;
+ [ 1: intro; reflexivity
+ | 2: intros; destruct H1
+ ]
+qed.
+
(* ******** *)
(* naturali *)
(* ******** *)
[ true ⇒ b2
| false ⇒ not_bool b2 ].
+lemma eqbool_switch : ∀b1,b2.eq_bool b1 b2 = eq_bool b2 b1.
+ do 2 intro;
+ elim b1; elim b2;
+ reflexivity.
+qed.
+
+lemma andbool_switch : ∀b1,b2.and_bool b1 b2 = and_bool b2 b1.
+ do 2 intro;
+ elim b1; elim b2;
+ reflexivity.
+qed.
+
+lemma orbool_switch : ∀b1,b2.or_bool b1 b2 = or_bool b2 b1.
+ do 2 intro;
+ elim b1; elim b2;
+ reflexivity.
+qed.
+
+lemma xorbool_switch : ∀b1,b2.xor_bool b1 b2 = xor_bool b2 b1.
+ do 2 intro;
+ elim b1; elim b2;
+ reflexivity.
+qed.
+
lemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
unfold eq_bool;
intros;
destruct H.
qed.
+lemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
+ do 2 intro;
+ elim b1 0;
+ elim b2 0;
+ intro;
+ normalize in H:(%);
+ try destruct H;
+ reflexivity.
+qed.
+
(* \ominus *)
notation "hvbox(⊖ a)" non associative with precedence 36
for @{ 'not_bool $a }.
(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
-include "freescale/medium_tests_lemmas.ma".
+(* include "freescale/medium_tests_tools.ma" *)
+include "freescale/medium_tests_tools.ma".
(* ************************ *)
(* HCS08GB60 String Reverse *)
(MSB_w16 〈bhigh:blow〉))
false)
(filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3))).
-
- intros;
+elim daemon.
+(* intros;
whd in ⊢ (? ? % ?);
whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
rewrite > H;
rewrite > (set_set_clk_desc HCS08 t (set_pc_reg HCS08 t (setweak_v_flag HCS08 t (setweak_n_flag HCS08 t (set_z_flag HCS08 t (set_alu HCS08 t s (set_indX_16_reg_HC08 (alu HCS08 t s) 〈bhigh:blow〉)) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈bhigh:blow〉)) false) (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3)) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (None ?));
rewrite > (set_clk_f_set_clk_desc HCS08 t s (λtmps.set_pc_reg HCS08 t (setweak_v_flag HCS08 t (setweak_n_flag HCS08 t (set_z_flag HCS08 t (set_alu HCS08 t tmps (set_indX_16_reg_HC08 (alu HCS08 t tmps) 〈bhigh:blow〉)) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈bhigh:blow〉)) false) (filtered_plus_w16 HCS08 t tmps (get_pc_reg HCS08 t tmps) 3))) in ⊢ (? ? (? ? %) ?);
[2: elim H; reflexivity ]
- reflexivity.
+ reflexivity.*)
qed.
definition execute_HCS08_STHX_maSP1_aux ≝
(succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)) =
array_8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE) →
(execute HCS08 MEM_TREE (TickOK ? s) 5 = execute_HCS08_STHX_maSP1_aux s blow).
-
- intros;
+elim daemon.
+(* intros;
whd in ⊢ (? ? % ?);
whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
rewrite > H;
rewrite > (set_clk_f_set_clk_desc HCS08 MEM_TREE s (λs.set_pc_reg HCS08 MEM_TREE (setweak_v_flag HCS08 MEM_TREE (setweak_n_flag HCS08 MEM_TREE (set_z_flag HCS08 MEM_TREE (set_mem_desc HCS08 MEM_TREE s (mt_update byte8 (mt_update byte8 (get_mem_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉) (indX_high_reg_HC08 (alu HCS08 MEM_TREE s))) (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)) (indX_low_reg_HC08 (alu HCS08 MEM_TREE s)))) (eq_w16 〈(indX_high_reg_HC08 (alu HCS08 MEM_TREE s)):(indX_low_reg_HC08 (alu HCS08 MEM_TREE s))〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_b8 (indX_high_reg_HC08 (alu HCS08 MEM_TREE s)))) false) (filtered_plus_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s) 3)))
in ⊢ (? ? (? ? %) ?);
[2: elim H; reflexivity ]
- reflexivity.
+ reflexivity.*)
qed.
(* setter forte della ALU *)
definition set_alu ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.match s with
- [ mk_any_status _ mem chk clk ⇒ mk_any_status m t alu' mem chk clk ].
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
+ mk_any_status m t alu' (get_mem_desc m t s) (get_chk_desc m t s) (get_clk_desc m t s).
(* setter forte della memoria *)
definition set_mem_desc ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.match s with
- [ mk_any_status alu _ chk clk ⇒ mk_any_status m t alu mem' chk clk ].
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
+ mk_any_status m t (get_alu m t s) mem' (get_chk_desc m t s) (get_clk_desc m t s).
(* setter forte del descrittore *)
definition set_chk_desc ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.match s with
- [ mk_any_status alu mem _ clk ⇒ mk_any_status m t alu mem chk' clk ].
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
+ mk_any_status m t (get_alu m t s) (get_mem_desc m t s) chk' (get_clk_desc m t s).
(* setter forte del clik *)
definition set_clk_desc ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.
-λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).match s with
- [ mk_any_status alu mem chk _ ⇒ mk_any_status m t alu mem chk clk' ].
+λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
+ mk_any_status m t (get_alu m t s) (get_mem_desc m t s) (get_chk_desc m t s) clk'.
(* REGISTRO A *)
(* setter specifico HC05 di A *)
definition set_acc_8_low_reg_HC05 ≝
-λalu.λacclow':byte8.match alu with
- [ mk_alu_HC05 _ indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC05 acclow' indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
+λalu.λacclow':byte8.
+ mk_alu_HC05
+ acclow'
+ (indX_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
(* setter specifico HC08/HCS08 di A *)
definition set_acc_8_low_reg_HC08 ≝
-λalu.λacclow':byte8.match alu with
- [ mk_alu_HC08 _ indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC08 acclow' indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ].
+λalu.λacclow':byte8.
+ mk_alu_HC08
+ acclow'
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
(* setter specifico RS08 di A *)
definition set_acc_8_low_reg_RS08 ≝
-λalu.λacclow':byte8.match alu with
- [ mk_alu_RS08 _ pc pcm spc xm psm zfl cfl ⇒
- mk_alu_RS08 acclow' pc pcm spc xm psm zfl cfl ].
+λalu.λacclow':byte8.
+ mk_alu_RS08
+ acclow'
+ (pc_reg_RS08 alu)
+ (pc_mask_RS08 alu)
+ (spc_reg_RS08 alu)
+ (x_map_RS08 alu)
+ (ps_map_RS08 alu)
+ (z_flag_RS08 alu)
+ (c_flag_RS08 alu).
(* setter forte di A *)
definition set_acc_8_low_reg ≝
(* setter specifico HC05 di X *)
definition set_indX_8_low_reg_HC05 ≝
-λalu.λindxlow':byte8.match alu with
- [ mk_alu_HC05 acclow _ sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC05 acclow indxlow' sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
+λalu.λindxlow':byte8.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ indxlow'
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
(* setter specifico HC08/HCS08 di X *)
definition set_indX_8_low_reg_HC08 ≝
-λalu.λindxlow':byte8.match alu with
- [ mk_alu_HC08 acclow _ indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC08 acclow indxlow' indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ].
+λalu.λindxlow':byte8.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ indxlow'
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
(* setter forte di X *)
definition set_indX_8_low_reg ≝
(* setter specifico HC08/HCS08 di H *)
definition set_indX_8_high_reg_HC08 ≝
-λalu.λindxhigh':byte8.match alu with
- [ mk_alu_HC08 acclow indxlow _ sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC08 acclow indxlow indxhigh' sp pc vfl hfl ifl nfl zfl cfl irqfl ].
+λalu.λindxhigh':byte8.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ indxhigh'
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
(* setter forte di H *)
definition set_indX_8_high_reg ≝
(* setter specifico HC08/HCS08 di H:X *)
definition set_indX_16_reg_HC08 ≝
-λalu.λindx16:word16.match alu with
- [ mk_alu_HC08 acclow _ _ sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC08 acclow (w16l indx16) (w16h indx16) sp pc vfl hfl ifl nfl zfl cfl irqfl ].
+λalu.λindx16:word16.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (w16l indx16)
+ (w16h indx16)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
(* setter forte di H:X *)
definition set_indX_16_reg ≝
(* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
definition set_sp_reg_HC05 ≝
-λalu.λsp':word16.match alu with
- [ mk_alu_HC05 acclow indxlow _ spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC05 acclow indxlow (or_w16 (and_w16 sp' spm) spf) spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
+λalu.λsp':word16.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indx_low_reg_HC05 alu)
+ (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
(* setter specifico HC08/HCS08 di SP *)
definition set_sp_reg_HC08 ≝
-λalu.λsp':word16.match alu with
- [ mk_alu_HC08 acclow indxlow indxhigh _ pc vfl hfl ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC08 acclow indxlow indxhigh sp' pc vfl hfl ifl nfl zfl cfl irqfl ].
+λalu.λsp':word16.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ sp'
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
(* setter forte di SP *)
definition set_sp_reg ≝
(* setter specifico HC05 di PC, effettua PC∧mask *)
definition set_pc_reg_HC05 ≝
-λalu.λpc':word16.match alu with
- [ mk_alu_HC05 acclow indxlow sp spm spf _ pcm hfl ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC05 acclow indxlow sp spm spf (and_w16 pc' pcm) pcm hfl ifl nfl zfl cfl irqfl ].
+λalu.λpc':word16.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indx_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (and_w16 pc' (pc_mask_HC05 alu))
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
(* setter specifico HC08/HCS08 di PC *)
definition set_pc_reg_HC08 ≝
-λalu.λpc':word16.match alu with
- [ mk_alu_HC08 acclow indxlow indxhigh sp _ vfl hfl ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC08 acclow indxlow indxhigh sp pc' vfl hfl ifl nfl zfl cfl irqfl ].
+λalu.λpc':word16.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ pc'
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
(* setter specifico RS08 di PC, effettua PC∧mask *)
definition set_pc_reg_RS08 ≝
-λalu.λpc':word16.match alu with
- [ mk_alu_RS08 acclow _ pcm spc xm psm zfl cfl ⇒
- mk_alu_RS08 acclow (and_w16 pc' pcm) pcm spc xm psm zfl cfl ].
+λalu.λpc':word16.
+ mk_alu_RS08
+ (acc_low_reg_RS08 alu)
+ (and_w16 pc' (pc_mask_RS08 alu))
+ (pc_mask_RS08 alu)
+ (spc_reg_RS08 alu)
+ (x_map_RS08 alu)
+ (ps_map_RS08 alu)
+ (z_flag_RS08 alu)
+ (c_flag_RS08 alu).
(* setter forte di PC *)
definition set_pc_reg ≝
(* setter specifico RS08 di SPC, effettua SPC∧mask *)
definition set_spc_reg_RS08 ≝
-λalu.λspc':word16.match alu with
- [ mk_alu_RS08 acclow pc pcm _ xm psm zfl cfl ⇒
- mk_alu_RS08 acclow pc pcm (and_w16 spc' pcm) xm psm zfl cfl ].
+λalu.λspc':word16.
+ mk_alu_RS08
+ (acc_low_reg_RS08 alu)
+ (pc_reg_RS08 alu)
+ (pc_mask_RS08 alu)
+ (and_w16 spc' (pc_mask_RS08 alu))
+ (x_map_RS08 alu)
+ (ps_map_RS08 alu)
+ (z_flag_RS08 alu)
+ (c_flag_RS08 alu).
(* setter forte di SPC *)
definition set_spc_reg ≝
(* setter specifico RS08 di memory mapped X *)
definition set_x_map_RS08 ≝
-λalu.λxm':byte8.match alu with
- [ mk_alu_RS08 acclow pc pcm spc _ psm zfl cfl ⇒
- mk_alu_RS08 acclow pc pcm spc xm' psm zfl cfl ].
+λalu.λxm':byte8.
+ mk_alu_RS08
+ (acc_low_reg_RS08 alu)
+ (pc_reg_RS08 alu)
+ (pc_mask_RS08 alu)
+ (spc_reg_RS08 alu)
+ xm'
+ (ps_map_RS08 alu)
+ (z_flag_RS08 alu)
+ (c_flag_RS08 alu).
(* setter forte di memory mapped X *)
definition set_x_map ≝
(* setter specifico RS08 di memory mapped PS *)
definition set_ps_map_RS08 ≝
-λalu.λpsm':byte8.match alu with
- [ mk_alu_RS08 acclow pc pcm spc xm _ zfl cfl ⇒
- mk_alu_RS08 acclow pc pcm spc xm psm' zfl cfl ].
+λalu.λpsm':byte8.
+ mk_alu_RS08
+ (acc_low_reg_RS08 alu)
+ (pc_reg_RS08 alu)
+ (pc_mask_RS08 alu)
+ (spc_reg_RS08 alu)
+ (x_map_RS08 alu)
+ psm'
+ (z_flag_RS08 alu)
+ (c_flag_RS08 alu).
(* setter forte di memory mapped PS *)
definition set_ps_map ≝
(* setter specifico HC08/HCS08 di V *)
definition set_v_flag_HC08 ≝
-λalu.λvfl':bool.match alu with
- [ mk_alu_HC08 acclow indxlow indxhigh sp pc _ hfl ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC08 acclow indxlow indxhigh sp pc vfl' hfl ifl nfl zfl cfl irqfl ].
+λalu.λvfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ vfl'
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
(* setter forte di V *)
definition set_v_flag ≝
(* setter specifico HC05 di H *)
definition set_h_flag_HC05 ≝
-λalu.λhfl':bool.match alu with
- [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm _ ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl' ifl nfl zfl cfl irqfl ].
+λalu.λhfl':bool.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indx_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ hfl'
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
(* setter specifico HC08/HCS08 di H *)
definition set_h_flag_HC08 ≝
-λalu.λhfl':bool.match alu with
- [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl _ ifl nfl zfl cfl irqfl ⇒
- mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl' ifl nfl zfl cfl irqfl ].
+λalu.λhfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ hfl'
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
(* setter forte di H *)
definition set_h_flag ≝
(* setter specifico HC05 di I *)
definition set_i_flag_HC05 ≝
-λalu.λifl':bool.match alu with
- [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl _ nfl zfl cfl irqfl ⇒
- mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl' nfl zfl cfl irqfl ].
+λalu.λifl':bool.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indx_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ ifl'
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
(* setter specifico HC08/HCS08 di I *)
definition set_i_flag_HC08 ≝
-λalu.λifl':bool.match alu with
- [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl _ nfl zfl cfl irqfl ⇒
- mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl' nfl zfl cfl irqfl ].
+λalu.λifl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ ifl'
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
(* setter forte di I *)
definition set_i_flag ≝
(* setter specifico HC05 di N *)
definition set_n_flag_HC05 ≝
-λalu.λnfl':bool.match alu with
- [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl _ zfl cfl irqfl ⇒
- mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl' zfl cfl irqfl ].
+λalu.λnfl':bool.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indx_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ nfl'
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
(* setter specifico HC08/HCS08 di N *)
definition set_n_flag_HC08 ≝
-λalu.λnfl':bool.match alu with
- [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl _ zfl cfl irqfl ⇒
- mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl' zfl cfl irqfl ].
+λalu.λnfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ nfl'
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
(* setter forte di N *)
definition set_n_flag ≝
(* setter specifico HC05 di Z *)
definition set_z_flag_HC05 ≝
-λalu.λzfl':bool.match alu with
- [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl _ cfl irqfl ⇒
- mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl' cfl irqfl ].
+λalu.λzfl':bool.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indx_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ zfl'
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
(* setter specifico HC08/HCS08 di Z *)
definition set_z_flag_HC08 ≝
-λalu.λzfl':bool.match alu with
- [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl _ cfl irqfl ⇒
- mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl' cfl irqfl ].
+λalu.λzfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ zfl'
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
(* setter sprcifico RS08 di Z *)
definition set_z_flag_RS08 ≝
-λalu.λzfl':bool.match alu with
- [ mk_alu_RS08 acclow pc pcm spc xm psm _ cfl ⇒
- mk_alu_RS08 acclow pc pcm spc xm psm zfl' cfl ].
+λalu.λzfl':bool.
+ mk_alu_RS08
+ (acc_low_reg_RS08 alu)
+ (pc_reg_RS08 alu)
+ (pc_mask_RS08 alu)
+ (spc_reg_RS08 alu)
+ (x_map_RS08 alu)
+ (ps_map_RS08 alu)
+ zfl'
+ (c_flag_RS08 alu).
(* setter forte di Z *)
definition set_z_flag ≝
(* setter specifico HC05 di C *)
definition set_c_flag_HC05 ≝
-λalu.λcfl':bool.match alu with
- [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl _ irqfl ⇒
- mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl' irqfl ].
+λalu.λcfl':bool.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indx_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ cfl'
+ (irq_flag_HC05 alu).
(* setter specifico HC08/HCS08 di C *)
definition set_c_flag_HC08 ≝
-λalu.λcfl':bool.match alu with
- [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl _ irqfl ⇒
- mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl' irqfl ].
+λalu.λcfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ cfl'
+ (irq_flag_HC08 alu).
(* setter specifico RS08 di C *)
definition set_c_flag_RS08 ≝
-λalu.λcfl':bool.match alu with
- [ mk_alu_RS08 acclow pc pcm spc xm psm zfl _ ⇒
- mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl' ].
+λalu.λcfl':bool.
+ mk_alu_RS08
+ (acc_low_reg_RS08 alu)
+ (pc_reg_RS08 alu)
+ (pc_mask_RS08 alu)
+ (spc_reg_RS08 alu)
+ (x_map_RS08 alu)
+ (ps_map_RS08 alu)
+ (z_flag_RS08 alu)
+ cfl'.
(* setter forte di C *)
definition set_c_flag ≝
(* setter specifico HC05 di IRQ *)
definition set_irq_flag_HC05 ≝
-λalu.λirqfl':bool.match alu with
- [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl _ ⇒
- mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl' ].
+λalu.λirqfl':bool.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indx_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ irqfl'.
(* setter specifico HC08/HCS08 di IRQ *)
definition set_irq_flag_HC08 ≝
-λalu.λirqfl':bool.match alu with
- [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl _ ⇒
- mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl' ].
+λalu.λirqfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ irqfl'.
(* setter forte di IRQ *)
definition set_irq_flag ≝
(* confronto fra ascii_min *)
definition eqAsciiMin ≝
λc,c':ascii_min.(eq_b8 (magic_of_ascii_min c) (magic_of_ascii_min c')).
+
+lemma eq_to_eqasciimin : ∀a1,a2.a1 = a2 → eqAsciiMin a1 a2 = true.
+ do 3 intro;
+ unfold eqAsciiMin;
+ rewrite > H;
+ elim a2;
+ reflexivity.
+qed.
+
+(* 63^2 casi... *)
+lemma eqasciimin_to_eq_00 : ∀a.eqAsciiMin ch_0 a = true → ch_0 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_01 : ∀a.eqAsciiMin ch_1 a = true → ch_1 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_02 : ∀a.eqAsciiMin ch_2 a = true → ch_2 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_03 : ∀a.eqAsciiMin ch_3 a = true → ch_3 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_04 : ∀a.eqAsciiMin ch_4 a = true → ch_4 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_05 : ∀a.eqAsciiMin ch_5 a = true → ch_5 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_06 : ∀a.eqAsciiMin ch_6 a = true → ch_6 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_07 : ∀a.eqAsciiMin ch_7 a = true → ch_7 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_08 : ∀a.eqAsciiMin ch_8 a = true → ch_8 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_09 : ∀a.eqAsciiMin ch_9 a = true → ch_9 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_10 : ∀a.eqAsciiMin ch__ a = true → ch__ = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_11 : ∀a.eqAsciiMin ch_A a = true → ch_A = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_12 : ∀a.eqAsciiMin ch_B a = true → ch_B = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_13 : ∀a.eqAsciiMin ch_C a = true → ch_C = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_14 : ∀a.eqAsciiMin ch_D a = true → ch_D = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_15 : ∀a.eqAsciiMin ch_E a = true → ch_E = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_16 : ∀a.eqAsciiMin ch_F a = true → ch_F = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_17 : ∀a.eqAsciiMin ch_G a = true → ch_G = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_18 : ∀a.eqAsciiMin ch_H a = true → ch_H = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_19 : ∀a.eqAsciiMin ch_I a = true → ch_I = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_20 : ∀a.eqAsciiMin ch_J a = true → ch_J = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_21 : ∀a.eqAsciiMin ch_K a = true → ch_K = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_22 : ∀a.eqAsciiMin ch_L a = true → ch_L = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_23 : ∀a.eqAsciiMin ch_M a = true → ch_M = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_24 : ∀a.eqAsciiMin ch_N a = true → ch_N = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_25 : ∀a.eqAsciiMin ch_O a = true → ch_O = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_26 : ∀a.eqAsciiMin ch_P a = true → ch_P = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_27 : ∀a.eqAsciiMin ch_Q a = true → ch_Q = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_28 : ∀a.eqAsciiMin ch_R a = true → ch_R = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_29 : ∀a.eqAsciiMin ch_S a = true → ch_S = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_30 : ∀a.eqAsciiMin ch_T a = true → ch_T = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_31 : ∀a.eqAsciiMin ch_U a = true → ch_U = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_32 : ∀a.eqAsciiMin ch_V a = true → ch_V = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_33 : ∀a.eqAsciiMin ch_W a = true → ch_W = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_34 : ∀a.eqAsciiMin ch_X a = true → ch_X = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_35 : ∀a.eqAsciiMin ch_Y a = true → ch_Y = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_36 : ∀a.eqAsciiMin ch_Z a = true → ch_Z = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_37 : ∀a.eqAsciiMin ch_a a = true → ch_a = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_38 : ∀a.eqAsciiMin ch_b a = true → ch_b = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_39 : ∀a.eqAsciiMin ch_c a = true → ch_c = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_40 : ∀a.eqAsciiMin ch_d a = true → ch_d = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_41 : ∀a.eqAsciiMin ch_e a = true → ch_e = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_42 : ∀a.eqAsciiMin ch_f a = true → ch_f = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_43 : ∀a.eqAsciiMin ch_g a = true → ch_g = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_44 : ∀a.eqAsciiMin ch_h a = true → ch_h = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_45 : ∀a.eqAsciiMin ch_i a = true → ch_i = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_46 : ∀a.eqAsciiMin ch_j a = true → ch_j = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_47 : ∀a.eqAsciiMin ch_k a = true → ch_k = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_48 : ∀a.eqAsciiMin ch_l a = true → ch_l = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_49 : ∀a.eqAsciiMin ch_m a = true → ch_m = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_50 : ∀a.eqAsciiMin ch_n a = true → ch_n = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_51 : ∀a.eqAsciiMin ch_o a = true → ch_o = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_52 : ∀a.eqAsciiMin ch_p a = true → ch_p = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_53 : ∀a.eqAsciiMin ch_q a = true → ch_q = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_54 : ∀a.eqAsciiMin ch_r a = true → ch_r = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_55 : ∀a.eqAsciiMin ch_s a = true → ch_s = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_56 : ∀a.eqAsciiMin ch_t a = true → ch_t = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_57 : ∀a.eqAsciiMin ch_u a = true → ch_u = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_58 : ∀a.eqAsciiMin ch_v a = true → ch_v = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_59 : ∀a.eqAsciiMin ch_w a = true → ch_w = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_60 : ∀a.eqAsciiMin ch_x a = true → ch_x = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_61 : ∀a.eqAsciiMin ch_y a = true → ch_y = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_62 : ∀a.eqAsciiMin ch_z a = true → ch_z = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+
+lemma eqasciimin_to_eq : ∀a1.∀a2.eqAsciiMin a1 a2 = true → a1 = a2.
+ do 1 intro;
+ elim a1 0;
+ [ 1: apply eqasciimin_to_eq_00 | 2: apply eqasciimin_to_eq_01 | 3: apply eqasciimin_to_eq_02 | 4: apply eqasciimin_to_eq_03
+ | 5: apply eqasciimin_to_eq_04 | 6: apply eqasciimin_to_eq_05 | 7: apply eqasciimin_to_eq_06 | 8: apply eqasciimin_to_eq_07
+ | 9: apply eqasciimin_to_eq_08 | 10: apply eqasciimin_to_eq_09 | 11: apply eqasciimin_to_eq_10 | 12: apply eqasciimin_to_eq_11
+ | 13: apply eqasciimin_to_eq_12 | 14: apply eqasciimin_to_eq_13 | 15: apply eqasciimin_to_eq_14 | 16: apply eqasciimin_to_eq_15
+ | 17: apply eqasciimin_to_eq_16 | 18: apply eqasciimin_to_eq_17 | 19: apply eqasciimin_to_eq_18 | 20: apply eqasciimin_to_eq_19
+ | 21: apply eqasciimin_to_eq_20 | 22: apply eqasciimin_to_eq_21 | 23: apply eqasciimin_to_eq_22 | 24: apply eqasciimin_to_eq_23
+ | 25: apply eqasciimin_to_eq_24 | 26: apply eqasciimin_to_eq_25 | 27: apply eqasciimin_to_eq_26 | 28: apply eqasciimin_to_eq_27
+ | 29: apply eqasciimin_to_eq_28 | 30: apply eqasciimin_to_eq_29 | 31: apply eqasciimin_to_eq_30 | 32: apply eqasciimin_to_eq_31
+ | 33: apply eqasciimin_to_eq_32 | 34: apply eqasciimin_to_eq_33 | 35: apply eqasciimin_to_eq_34 | 36: apply eqasciimin_to_eq_35
+ | 37: apply eqasciimin_to_eq_36 | 38: apply eqasciimin_to_eq_37 | 39: apply eqasciimin_to_eq_38 | 40: apply eqasciimin_to_eq_39
+ | 41: apply eqasciimin_to_eq_40 | 42: apply eqasciimin_to_eq_41 | 43: apply eqasciimin_to_eq_42 | 44: apply eqasciimin_to_eq_43
+ | 45: apply eqasciimin_to_eq_44 | 46: apply eqasciimin_to_eq_45 | 47: apply eqasciimin_to_eq_46 | 48: apply eqasciimin_to_eq_47
+ | 49: apply eqasciimin_to_eq_48 | 50: apply eqasciimin_to_eq_49 | 51: apply eqasciimin_to_eq_50 | 52: apply eqasciimin_to_eq_51
+ | 53: apply eqasciimin_to_eq_52 | 54: apply eqasciimin_to_eq_53 | 55: apply eqasciimin_to_eq_54 | 56: apply eqasciimin_to_eq_55
+ | 57: apply eqasciimin_to_eq_56 | 58: apply eqasciimin_to_eq_57 | 59: apply eqasciimin_to_eq_58 | 60: apply eqasciimin_to_eq_59
+ | 61: apply eqasciimin_to_eq_60 | 62: apply eqasciimin_to_eq_61 | 63: apply eqasciimin_to_eq_62 ].
+qed.
[ nil ⇒ true | cons _ _ ⇒ false ].
(* strcmp *)
-let rec strCmp_str (str,str':aux_str_type) ≝
+let rec eqStr_str (str,str':aux_str_type) ≝
match str with
[ nil ⇒ match str' with
- [ nil ⇒ true | cons _ _ ⇒ false ]
+ [ nil => true
+ | cons _ _ => false ]
| cons h t ⇒ match str' with
[ nil ⇒ false
- | cons h' t' ⇒ match eqAsciiMin h h' with
- [ true ⇒ strCmp_str t t' | false ⇒ false ]
- ]].
+ | cons h' t' ⇒ (eqAsciiMin h h')⊗(eqStr_str t t')
+ ]
+ ].
-axiom eqbstrcmpstr_to_eq : ∀s,s'.strCmp_str s s' = true → s = s'.
+lemma eq_to_eqstr : ∀s,s'.s = s' → eqStr_str s s' = true.
+ do 2 intro;
+ intro;
+ rewrite < H;
+ elim s;
+ [ 1: reflexivity
+ | 2: simplify;
+ rewrite > (eq_to_eqasciimin a a (refl_eq ??));
+ rewrite > H1;
+ reflexivity
+ ].
+qed.
+
+lemma eqstr_to_eq : ∀s,s'.eqStr_str s s' = true → s = s'.
+ intros 1;
+ elim s 0;
+ intros;
+ [ simplify in H:(%);
+ cases s' in H;
+ simplify;
+ intros;
+ [ reflexivity
+ | destruct H
+ ]
+ | elim s' in H1;
+ [ simplify in H1;
+ destruct H1
+ | simplify in H2;
+ lapply (andb_true_true ?? H2);
+ lapply (andb_true_true_r ?? H2);
+ rewrite > (H ? Hletin1);
+ rewrite > (eqasciimin_to_eq ?? Hletin);
+ reflexivity
+ ]
+ ].
+qed.
(* strcat *)
definition strCat_str ≝
definition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ].
(* confronto *)
-definition strCmp_strId ≝
-λsid,sid':aux_strId_type.(strCmp_str (get_name_strId sid) (get_name_strId sid'))⊗(eqb (get_id_strId sid) (get_id_strId sid')).
+definition eqStrId_str ≝
+λsid,sid':aux_strId_type.(eqStr_str (get_name_strId sid) (get_name_strId sid'))⊗(eqb (get_id_strId sid) (get_id_strId sid')).
+
+lemma eq_to_eqstrid : ∀s,s'.s = s' → eqStrId_str s s' = true.
+ intros 3;
+ rewrite < H;
+ elim s;
+ simplify;
+ rewrite > (eq_to_eqstr a a (refl_eq ??));
+ rewrite > (eq_to_eqb_true n n (refl_eq ??));
+ reflexivity.
+qed.
+
+lemma eqstrid_to_eq : ∀s,s'.eqStrId_str s s' = true → s = s'.
+ intros 2;
+ elim s 0;
+ elim s' 0;
+ intros 4;
+ simplify;
+ intro;
+ rewrite > (eqstr_to_eq a1 a (andb_true_true ?? H));
+ rewrite > (eqb_true_to_eq n1 n (andb_true_true_r ?? H));
+ reflexivity.
+qed.
projects / helm.git / commitdiff