--- /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/astfe_tree.ma".
+
+(* ************************ *)
+(* PASSO 2 : da AST a ASTFE *)
+(* ************************ *)
+
+(* operatore di cast *)
+definition ast_to_astfe_expr_check : Πt.astfe_expr t → Πt'.option (astfe_expr t') ≝
+λt:ast_type.λast:astfe_expr t.λt':ast_type.
+ match eq_ast_type t t'
+ return λx.(eq_ast_type t t' = x) → ?
+ with
+ [ true ⇒ λp:(eq_ast_type t t' = true).
+ Some ? (eq_rect ? t (λt.astfe_expr t) ast t' (eqasttype_to_eq ?? p))
+ | false ⇒ λp:(eq_ast_type t t' = false).None ?
+ ] (refl_eq ? (eq_ast_type t t')).
+
+definition ast_to_astfe_init_check : Πt.astfe_init t → Πt'.option (astfe_init t') ≝
+λt:ast_type.λast:astfe_init t.λt':ast_type.
+ match eq_ast_type t t'
+ return λx.(eq_ast_type t t' = x) → ?
+ with
+ [ true ⇒ λp:(eq_ast_type t t' = true).
+ Some ? (eq_rect ? t (λt.astfe_init t) ast t' (eqasttype_to_eq ?? p))
+ | false ⇒ λp:(eq_ast_type t t' = false).None ?
+ ] (refl_eq ? (eq_ast_type t t')).
+
+definition ast_to_astfe_var_checkb : Πb.Πt.astfe_var b t → Πb'.option (astfe_var b' t) ≝
+λb:bool.λt:ast_type.λast:astfe_var b t.λb':bool.
+ match eq_bool b b'
+ return λx.(eq_bool b b' = x) → ?
+ with
+ [ true ⇒ λp:(eq_bool b b' = true).
+ Some ? (eq_rect ? b (λb.astfe_var b t) ast b' (eqbool_to_eq ?? p))
+ | false ⇒ λp:(eq_bool b b' = false).None ?
+ ] (refl_eq ? (eq_bool b b')).
+
+definition ast_to_astfe_var_checkt : Πb.Πt.astfe_var b t → Πt'.option (astfe_var b t') ≝
+λb:bool.λt:ast_type.λast:astfe_var b t.λt':ast_type.
+ match eq_ast_type t t'
+ return λx.(eq_ast_type t t' = x) → ?
+ with
+ [ true ⇒ λp:(eq_ast_type t t' = true).
+ Some ? (eq_rect ? t (λt.astfe_var b t) ast t' (eqasttype_to_eq ?? p))
+ | false ⇒ λp:(eq_ast_type t t' = false).None ?
+ ] (refl_eq ? (eq_ast_type t t')).
+
+definition ast_to_astfe_var_check : Πb.Πt.astfe_var b t → Πb'.Πt'.option (astfe_var b' t') ≝
+λb:bool.λt:ast_type.λast:astfe_var b t.λb':bool.λt':ast_type.
+ opt_map ?? (ast_to_astfe_var_checkb b t ast b')
+ (λres.opt_map ?? (ast_to_astfe_var_checkt b' t res t')
+ (λres'.Some ? res')).
+
+(*
+ AST_ID: ∀str:aux_str_type.
+ (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str)))
+*)
+definition ast_to_astfe_id ≝
+λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.λmap:aux_trasfMap_type.match ast with
+ [ AST_ID str _ ⇒ ASTFE_ID (name_to_nameId map str) b t ].
+
+(*
+ AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+ AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+
+ AST_EXPR_NEG: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ AST_EXPR_NOT: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ AST_EXPR_COM: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+
+ AST_EXPR_ADD: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ AST_EXPR_SUB: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ AST_EXPR_MUL: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ AST_EXPR_DIV: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
+ AST_EXPR_SHR: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
+ AST_EXPR_SHL: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
+
+ AST_EXPR_GT : ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ AST_EXPR_GTE: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ AST_EXPR_LT : ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ AST_EXPR_LTE: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ AST_EXPR_EQ : ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ AST_EXPR_NEQ: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+
+ AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+ AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+ AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+ AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+
+ AST_EXPR_ID: ∀b:bool.∀t:ast_type.
+ ast_var e b t → ast_expr e t
+*)
+let rec ast_to_astfe_expr (e:aux_env_type) (t:ast_type) (ast:ast_expr e t) (map:aux_trasfMap_type) on ast : option (astfe_expr t) ≝
+ match ast with
+ [ AST_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 val) t
+ | AST_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 val) t
+ | AST_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 val) t
+
+ | AST_EXPR_NEG bType subExpr ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr map)
+ (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG bType res) t)
+ | AST_EXPR_NOT bType subExpr ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr map)
+ (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT bType res) t)
+ | AST_EXPR_COM bType subExpr ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr map)
+ (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_COM bType res) t)
+
+ | AST_EXPR_ADD bType subExpr1 subExpr2 ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
+ (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
+ (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD bType res1 res2) t))
+ | AST_EXPR_SUB bType subExpr1 subExpr2 ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
+ (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
+ (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB bType res1 res2) t))
+ | AST_EXPR_MUL bType subExpr1 subExpr2 ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
+ (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
+ (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL bType res1 res2) t))
+ | AST_EXPR_DIV bType subExpr1 subExpr2 ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
+ (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
+ (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV bType res1 res2) t))
+ | AST_EXPR_SHR bType subExpr1 subExpr2 ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
+ (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 map)
+ (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR bType res1 res2) t))
+ | AST_EXPR_SHL bType subExpr1 subExpr2 ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
+ (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 map)
+ (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL bType res1 res2) t))
+
+ | AST_EXPR_LT bType subExpr1 subExpr2 ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
+ (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
+ (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT bType res1 res2) t))
+ | AST_EXPR_LTE bType subExpr1 subExpr2 ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
+ (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
+ (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE bType res1 res2) t))
+ | AST_EXPR_GT bType subExpr1 subExpr2 ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
+ (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
+ (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT bType res1 res2) t))
+ | AST_EXPR_GTE bType subExpr1 subExpr2 ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
+ (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
+ (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE bType res1 res2) t))
+ | AST_EXPR_EQ bType subExpr1 subExpr2 ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
+ (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
+ (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ bType res1 res2) t))
+ | AST_EXPR_NEQ bType subExpr1 subExpr2 ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
+ (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
+ (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ bType res1 res2) t))
+
+ | AST_EXPR_B8toW16 subExpr ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr map)
+ (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 res) t)
+ | AST_EXPR_B8toW32 subExpr ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr map)
+ (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 res) t)
+ | AST_EXPR_W16toB8 subExpr ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr map)
+ (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 res) t)
+ | AST_EXPR_W16toW32 subExpr ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr map)
+ (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 res) t)
+ | AST_EXPR_W32toB8 subExpr ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr map)
+ (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 res) t)
+ | AST_EXPR_W32toW16 subExpr ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr map)
+ (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 res) t)
+
+ | AST_EXPR_ID b subType var ⇒
+ opt_map ?? (ast_to_astfe_var e b subType var map)
+ (λres.ast_to_astfe_expr_check subType (ASTFE_EXPR_ID b subType res) t)
+ ]
+(*
+ AST_VAR_ID: ∀b:bool.∀t:ast_type.
+ ast_id e b t → ast_var e b t
+ AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
+ ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
+ AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
+ ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
+*)
+and ast_to_astfe_var (e:aux_env_type) (b:bool) (t:ast_type) (ast:ast_var e b t) (map:aux_trasfMap_type) on ast : option (astfe_var b t) ≝
+ match ast with
+ [ AST_VAR_ID subB subType subId ⇒ ast_to_astfe_var_check subB subType (ASTFE_VAR_ID subB subType (ast_to_astfe_id e subB subType subId map)) b t
+
+ | AST_VAR_ARRAY subB subType dim var expr ⇒
+ opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_ARRAY subType dim) var map)
+ (λresVar.opt_map ?? (ast_to_astfe_base_expr e expr map)
+ (λresExpr.ast_to_astfe_var_check subB subType (ASTFE_VAR_ARRAY subB subType dim resVar resExpr) b t))
+
+ | AST_VAR_STRUCT subB nelSubType field var _ ⇒
+ opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_STRUCT nelSubType) var map)
+ (λres.ast_to_astfe_var_check subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT subB nelSubType field res) b t)
+ ]
+(*
+ AST_BASE_EXPR: ∀t:ast_base_type.
+ ast_expr e (AST_TYPE_BASE t) → ast_base_expr e
+*)
+and ast_to_astfe_base_expr (e:aux_env_type) (ast:ast_base_expr e) (map:aux_trasfMap_type) on ast : option astfe_base_expr ≝
+ match ast with
+ [ AST_BASE_EXPR bType subExpr ⇒
+ opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr map)
+ (λres.Some ? (ASTFE_BASE_EXPR bType res))
+ ].
+
+(*
+ AST_INIT_VAR: ∀b:bool.∀t:ast_type.
+ ast_var e b t → ast_init e t
+ AST_INIT_VAL: ∀t:ast_type.
+ aux_ast_init_type t → ast_init e t
+*)
+definition ast_to_astfe_init : Πe.Πt.ast_init e t → aux_trasfMap_type → option (astfe_init t) ≝
+λe:aux_env_type.λt:ast_type.λast:ast_init e t.λmap:aux_trasfMap_type.match ast with
+ [ AST_INIT_VAR subB subType var ⇒
+ opt_map ?? (ast_to_astfe_var e subB subType var map)
+ (λres.ast_to_astfe_init_check subType (ASTFE_INIT_VAR subB subType res) t)
+
+ | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check subType (ASTFE_INIT_VAL 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
+*)
+let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (map:aux_trasfMap_type) (fe:aux_flatEnv_type) on ast : option (Prod3T astfe_stm aux_trasfMap_type aux_flatEnv_type) ≝
+ match ast with
+ [ AST_STM_ASG e' subType var expr ⇒
+ opt_map ?? (ast_to_astfe_var e' false subType var map)
+ (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr map)
+ (λresExpr.Some ? (tripleT ??? (ASTFE_STM_ASG subType resVar resExpr) map fe)))
+
+ | AST_STM_WHILE e' expr decl ⇒
+ opt_map ?? (ast_to_astfe_base_expr e' expr map)
+ (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl map fe)
+ (λtripleRes.match tripleRes with
+ [ tripleT resDecl map' fe' ⇒
+ Some ? (tripleT ??? (ASTFE_STM_WHILE resExpr (ASTFE_BODY resDecl)) (rollback_map map' (build_snapshot map)) fe')
+ ]))
+
+ | AST_STM_IF e' nelExprDecl optDecl ⇒
+ let rec aux (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e'))))
+ (m:aux_trasfMap_type) (flatE:aux_flatEnv_type) on nel ≝
+ match nel with
+ [ ne_nil h ⇒
+ opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) m)
+ (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) m flatE)
+ (λtripleRes.match tripleRes with
+ [ tripleT resDecl m' flatE' ⇒
+ Some ? (tripleT ??? « pair ?? resExpr (ASTFE_BODY resDecl) £» (rollback_map m' (build_snapshot m)) flatE')
+ ]))
+ | ne_cons h tl ⇒
+ opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) m)
+ (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) m flatE)
+ (λtripleRes.match tripleRes with
+ [ tripleT resDecl m' flatE' ⇒
+ opt_map ?? (aux tl (rollback_map m' (build_snapshot m)) flatE')
+ (λtripleRes'.match tripleRes' with
+ [ tripleT tl' m'' flatE'' ⇒
+ Some ? (tripleT ??? (« pair ?? resExpr (ASTFE_BODY resDecl) £»&tl') m'' flatE'')
+ ])]))] in
+ opt_map ?? (aux nelExprDecl map fe)
+ (λtRes.match tRes with
+ [ tripleT resNel resMap resFe ⇒
+ match optDecl with
+ [ None ⇒ Some ? (tripleT ??? (ASTFE_STM_IF resNel (None ?)) resMap resFe)
+ | Some decl ⇒
+ opt_map ?? (ast_to_astfe_decl (enter_env e') decl resMap resFe)
+ (λtRes'.match tRes' with
+ [ tripleT rDecl resMap' resFe' ⇒
+ Some ? (tripleT ??? (ASTFE_STM_IF resNel (Some ? (ASTFE_BODY rDecl))) (rollback_map resMap' (build_snapshot resMap)) resFe')
+ ])
+ ]])
+ ]
+(*
+ AST_NO_DECL: ∀e:aux_env_type.
+ list (ast_stm e) → ast_decl e
+ AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
+ (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e
+*)
+and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (map:aux_trasfMap_type) (fe:aux_flatEnv_type) on ast : option (Prod3T (list astfe_stm) aux_trasfMap_type aux_flatEnv_type) ≝
+ match ast with
+ [ AST_NO_DECL e' lStm ⇒
+ let rec aux (ll:list (ast_stm e')) (m:aux_trasfMap_type) (flatE:aux_flatEnv_type) on ll ≝
+ match ll with
+ [ nil ⇒ Some ? (tripleT ??? [] m flatE)
+ | cons h tl ⇒
+ opt_map ?? (ast_to_astfe_stm e' h m flatE)
+ (λtripleRes.match tripleRes with
+ [ tripleT resStm m' flatE' ⇒
+ opt_map ?? (aux tl m' flatE')
+ (λtripleRes'.match tripleRes' with
+ [ tripleT tl' m'' flatE'' ⇒
+ Some ? (tripleT ??? ([ resStm ]@tl') m'' flatE'')
+ ])])] in
+ aux lStm map fe
+
+ | AST_DECL e' b name t _ optInit subDecl ⇒
+ opt_map ?? (match optInit with
+ [ None ⇒ Some ? [] | Some init ⇒ opt_map ?? (ast_to_astfe_init e' t init map)
+ (λresInit.Some ? [ ASTFE_STM_INIT b t (ASTFE_ID (name_to_nameId (add_maxcur_map map name) name) b t) resInit ])])
+ (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl (add_maxcur_map map name) (add_desc_flatEnv fe (name_to_nameId (add_maxcur_map map name) name) b t))
+ (λtripleRes.match tripleRes with
+ [ tripleT tRes resMap resFe ⇒
+ Some ? (tripleT ??? (hRes@tRes) resMap resFe)
+ ]))
+ ].
+
+(*
+ AST_ROOT: ast_decl empty_env → ast_root.
+*)
+definition ast_to_astfe ≝
+λast:ast_root.match ast with
+ [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_trasfMap empty_flatEnv with
+ (* impossibile: dummy *)
+ [ None ⇒ empty_astfe_prog
+ | Some x ⇒ ASTFE_ROOT (thd3T ??? x) (ASTFE_BODY (fst3T ??? x))
+ ]
+ ].
+
+(* 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;
+
+ if(0xF0)
+ { byte8 a=a; }
+ else if(0xF1)
+ {
+ while(0x10)
+ { byte8[3] b=c; }
+ }
+ else if(0xF2)
+ { byte8 a=b[0]; }
+ else
+ { const byte8 a=a; }
+}
+*)
+(*
+definition prova ≝
+PREAST_ROOT (
+ PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) (
+ PREAST_DECL true [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAL (PREAST_INIT_VAL_ARRAY «(PREAST_INIT_VAL_BYTE8 〈x0,x2〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)»))) (
+ PREAST_DECL false [ch_C] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_B]))) (
+ PREAST_NO_DECL [
+ PREAST_STM_IF «
+ (pair ??
+ (PREAST_EXPR_BYTE8 〈xF,x2〉)
+ (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ARRAY (PREAST_VAR_ID [ch_B]) (PREAST_EXPR_BYTE8 〈x0,x0〉)))) (PREAST_NO_DECL []))
+ )
+ £ (pair ??
+ (PREAST_EXPR_BYTE8 〈xF,x0〉)
+ (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL []))
+ )
+ ; (pair ??
+ (PREAST_EXPR_BYTE8 〈xF,x1〉)
+ (PREAST_NO_DECL [
+ (PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x1,x0〉) (
+ PREAST_DECL false [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_C]))) (PREAST_NO_DECL [])
+ ))
+ ])
+ )
+ » (Some ? (PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL [])))
+ ]
+ )
+ )
+ )
+).
+
+lemma provacheck : opt_map ?? (preast_to_ast prova) (λres.Some ? (ast_to_astfe res)) = None ?.
+normalize;
+*)
projects / helm.git / blobdiff