--- /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;
+*)
(* -------------------------- *)
(* espressioni *)
-inductive ast_expr (e:aux_env_type) : ast_base_type → Type ≝
- AST_EXPR_BYTE8 : byte8 → ast_expr e AST_BASE_TYPE_BYTE8
-| AST_EXPR_WORD16: word16 → ast_expr e AST_BASE_TYPE_WORD16
-| AST_EXPR_WORD32: word32 → ast_expr e AST_BASE_TYPE_WORD32
+inductive ast_expr (e:aux_env_type) : ast_type → Type ≝
+ 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 t → ast_expr e t
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
| AST_EXPR_NOT: ∀t:ast_base_type.
- ast_expr e t → ast_expr e t
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
| AST_EXPR_COM: ∀t:ast_base_type.
- ast_expr e t → ast_expr e t
+ ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
| AST_EXPR_ADD: ∀t:ast_base_type.
- ast_expr e t → ast_expr e t → ast_expr e t
+ 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 t → ast_expr e t → ast_expr e t
+ 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 t → ast_expr e t → ast_expr e t
+ 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 t → ast_expr e t → ast_expr e t
+ 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 t → ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e t
+ 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 t → ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e t
+ 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 t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+ 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 t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+ 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 t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+ 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 t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+ 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 t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+ 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 t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+ 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_BASE_TYPE_BYTE8 → ast_expr e AST_BASE_TYPE_WORD16
-| AST_EXPR_B8toW32 : ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e AST_BASE_TYPE_WORD32
-| AST_EXPR_W16toB8 : ast_expr e AST_BASE_TYPE_WORD16 → ast_expr e AST_BASE_TYPE_BYTE8
-| AST_EXPR_W16toW32: ast_expr e AST_BASE_TYPE_WORD16 → ast_expr e AST_BASE_TYPE_WORD32
-| AST_EXPR_W32toB8 : ast_expr e AST_BASE_TYPE_WORD32 → ast_expr e AST_BASE_TYPE_BYTE8
-| AST_EXPR_W32toW16: ast_expr e AST_BASE_TYPE_WORD32 → ast_expr e AST_BASE_TYPE_WORD16
+| 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_base_type.
- ast_var e b (AST_TYPE_BASE t) → ast_expr e t
+| AST_EXPR_ID: ∀b:bool.∀t:ast_type.
+ ast_var e b t → ast_expr e t
(* variabile: modificatori di array/struct dell'id *)
with ast_var : bool → ast_type → Type ≝
(* espressioni generalizzate: anche non uniformi per tipo *)
with ast_base_expr : Type ≝
AST_BASE_EXPR: ∀t:ast_base_type.
- ast_expr e t → ast_base_expr e.
-
-(* -------------------------- *)
-
-(* espressioni destre di assegnamento *)
-inductive ast_right_expr (e:aux_env_type) : ast_type → Type ≝
- AST_RIGHT_EXPR_BASE: ∀t:ast_base_type.
- ast_expr e t → ast_right_expr e (AST_TYPE_BASE t)
-| AST_RIGHT_EXPR_VAR: ∀b:bool.∀t:ast_type.
- ast_var e b t → ast_right_expr e t.
+ ast_expr e (AST_TYPE_BASE t) → ast_base_expr e.
(* -------------------------- *)
(* statement: assegnamento/while/if else if else *)
inductive ast_stm : aux_env_type → Type ≝
AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
- ast_var e false t → ast_right_expr e t → ast_stm e
+ 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 e → ast_stm e
+ 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 e)) → option (ast_decl e) → ast_stm e
+ ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
(* dichiarazioni *)
with ast_decl : aux_env_type → Type ≝
--- /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 "string/string.ma".
+include "compiler/utility.ma".
+include "freescale/word32.ma".
+include "compiler/ast_type.ma".
+include "compiler/env_to_flatenv.ma".
+include "compiler/ast_tree.ma".
+
+(* **************************** *)
+(* ALBERO DI TOKEN CON FLAT ENV *)
+(* **************************** *)
+
+(* id: accesso all'ambiente con stringa *)
+inductive astfe_id : bool → ast_type → Type ≝
+ ASTFE_ID: ∀str:aux_strId_type.∀b:bool.∀t:ast_type.
+ astfe_id b t.
+
+(* -------------------------- *)
+
+(* espressioni *)
+inductive astfe_expr : ast_type → Type ≝
+ ASTFE_EXPR_BYTE8 : byte8 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_WORD16: word16 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| ASTFE_EXPR_WORD32: word32 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+
+| ASTFE_EXPR_NEG: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_NOT: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_COM: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+
+| ASTFE_EXPR_ADD: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_SUB: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_MUL: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_DIV: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_SHR: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_SHL: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE t)
+
+| ASTFE_EXPR_GT : ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_GTE: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_LT : ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_LTE: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_EQ : ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_NEQ: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+
+| ASTFE_EXPR_B8toW16 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| ASTFE_EXPR_B8toW32 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| ASTFE_EXPR_W16toB8 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_W16toW32: astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| ASTFE_EXPR_W32toB8 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_W32toW16: astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+
+| ASTFE_EXPR_ID: ∀b:bool.∀t:ast_type.
+ astfe_var b t → astfe_expr t
+
+(* variabile: modificatori di array/struct dell'id *)
+with astfe_var : bool → ast_type → Type ≝
+ ASTFE_VAR_ID: ∀b:bool.∀t:ast_type.
+ astfe_id b t → astfe_var b t
+| ASTFE_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
+ astfe_var b (AST_TYPE_ARRAY t n) → astfe_base_expr → astfe_var b t
+| ASTFE_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
+ astfe_var b (AST_TYPE_STRUCT nel) → astfe_var b (abs_nth_neList ? nel n)
+
+(* espressioni generalizzate: anche non uniformi per tipo *)
+with astfe_base_expr : Type ≝
+ ASTFE_BASE_EXPR: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_base_expr.
+
+(* -------------------------- *)
+
+(*
+ inizializzatori: ammesse solo due forme, no ibridi
+ 1) var1 = var2
+ 2) var = ... valori ...
+*)
+inductive astfe_init : ast_type → Type ≝
+ ASTFE_INIT_VAR: ∀b:bool.∀t:ast_type.
+ astfe_var b t → astfe_init t
+| ASTFE_INIT_VAL: ∀t:ast_type.
+ aux_ast_init_type t → astfe_init t.
+
+(* -------------------------- *)
+
+(* statement: assegnamento/while/if else if else + conversione di dichiarazione *)
+inductive astfe_stm : Type ≝
+ ASTFE_STM_ASG: ∀t:ast_type.
+ astfe_var false t → astfe_expr t → astfe_stm
+| ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
+ astfe_id b t → astfe_init t → astfe_stm
+| ASTFE_STM_WHILE: astfe_base_expr → astfe_body → astfe_stm
+| ASTFE_STM_IF: ne_list (Prod astfe_base_expr astfe_body) → option astfe_body → astfe_stm
+
+(* dichiarazioni *)
+with astfe_body : Type ≝
+ ASTFE_BODY: list astfe_stm → astfe_body.
+
+(* -------------------------- *)
+
+(* programma *)
+inductive astfe_root : Type ≝
+ ASTFE_ROOT: aux_flatEnv_type → astfe_body → astfe_root.
+
+(* -------------------------- *)
+
+(* programma vuoto *)
+definition empty_astfe_prog ≝ ASTFE_ROOT empty_flatEnv (ASTFE_BODY (nil ?)).
--- /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 *)
+(* ********************** *)
+
+(* STRUTTURA AMBIENTE FLAT *)
+
+(* elemento: name + desc *)
+inductive flatVar_elem : Type ≝
+VAR_FLAT_ELEM: aux_strId_type → desc_elem → flatVar_elem.
+
+(* tipo pubblico *)
+definition aux_flatEnv_type ≝ list flatVar_elem.
+
+(* getter *)
+definition get_nameId_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
+definition get_desc_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
+
+(* ambiente vuoto *)
+definition empty_flatEnv ≝ nil flatVar_elem.
+
+(* STRUTTURA MAPPA TRASFORMAZIONE *)
+
+(* elemento: nome + max + cur *)
+inductive maxCur_elem : Type ≝
+MAX_CUR_ELEM: aux_str_type → nat → nat → maxCur_elem.
+
+(* tipo pubblico *)
+definition aux_trasfMap_type ≝ list maxCur_elem.
+
+(* getter *)
+definition get_name_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM n _ _ ⇒ n ].
+definition get_max_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM _ m _ ⇒ m ].
+definition get_cur_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM _ _ c ⇒ c ].
+
+(* mappa di trasformazione vuota *)
+definition empty_trasfMap ≝ nil maxCur_elem.
+
+(* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *)
+
+(* recupera descrittore da mappa trasformazione : dummy se non esiste (impossibile) *)
+let rec get_maxcur_from_map_aux (map:aux_trasfMap_type) (str:aux_str_type) (dummy:option maxCur_elem) on map ≝
+ match map with
+ [ nil ⇒ dummy
+ | cons h tl ⇒ match strCmp_str str (get_name_maxCur h) with
+ [ true ⇒ Some ? h | false ⇒ get_maxcur_from_map_aux tl str dummy ]].
+
+definition get_maxcur_from_map ≝
+λmap:aux_trasfMap_type.λstr:aux_str_type.
+ match get_maxcur_from_map_aux map str (None ?) with
+ [ None ⇒ MAX_CUR_ELEM str 0 0 | Some x ⇒ x ].
+
+(* aggiungi/aggiorna descrittore mappa trasformazione *)
+let rec add_maxcur_map_aux (map:aux_trasfMap_type) (str:aux_str_type) (flag:bool) on map ≝
+ match map with
+ [ nil ⇒ match flag with
+ [ true ⇒ []
+ | false ⇒ [MAX_CUR_ELEM str 0 0]
+ ]
+ | cons h tl ⇒ match strCmp_str str (get_name_maxCur h) with
+ [ true ⇒ [MAX_CUR_ELEM str (S (get_max_maxCur h)) (S (get_max_maxCur h))]@(add_maxcur_map_aux tl str true)
+ | false ⇒ [h]@(add_maxcur_map_aux tl str flag)
+ ]
+ ].
+
+definition add_maxcur_map ≝
+λmap:aux_trasfMap_type.λstr:aux_str_type.add_maxcur_map_aux map str false.
+
+(* nome -> nome + id *)
+definition name_to_nameId ≝
+λmap:aux_trasfMap_type.λstr:aux_str_type.
+ STR_ID str (get_cur_maxCur (get_maxcur_from_map map str)).
+
+(* recupera descrittore da ambiente : dummy se non esiste (impossibile) *)
+let rec get_desc_from_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) (dummy:option desc_elem) on e ≝
+match e with
+ [ nil ⇒ dummy
+ | cons h tl ⇒ match strCmp_strId str (get_nameId_flatVar h) with
+ [ true ⇒ Some ? (get_desc_flatVar h)
+ | false ⇒ get_desc_from_flatEnv_aux tl str dummy ]].
+
+definition get_desc_from_flatEnv ≝
+λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_from_flatEnv_aux e str (None ?) with
+ [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
+
+(* aggiungi descrittore ad ambiente *)
+definition add_desc_flatEnv ≝
+λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
+ e@[ VAR_FLAT_ELEM str (DESC_ELEM b t) ].
+
+(* snapshot della mappa trasformazione *)
+let rec build_snapshot (map:aux_trasfMap_type) on map ≝
+ match map with
+ [ nil ⇒ []
+ | cons h tl ⇒ [ STR_ID (get_name_maxCur h) (get_cur_maxCur h) ]@(build_snapshot tl)
+ ].
+
+(* uscita da un blocco, rollback di cur in mappa di trasformazione *)
+let rec find_in_snapshot (snap:list aux_strId_type) (str:aux_str_type) on snap ≝
+ match snap with
+ [ nil ⇒ None ?
+ | cons h tl ⇒ match strCmp_str str (get_name_strId h) with
+ [ true ⇒ Some ? (get_id_strId h)
+ | false ⇒ find_in_snapshot tl str
+ ]
+ ].
+
+let rec rollback_map (map:aux_trasfMap_type) (snap:list aux_strId_type) on map ≝
+ match map with
+ [ nil ⇒ empty_trasfMap
+ | cons h tl ⇒ match find_in_snapshot snap (get_name_maxCur h) with
+ [ None ⇒ [h]
+ | Some newCur ⇒ [ MAX_CUR_ELEM (get_name_maxCur h) (get_max_maxCur h) newCur ]
+ ]@(rollback_map tl snap)
+ ].
+
+(* sequenza di utilizzo:
+
+[BLOCCO ESTERNO]
+
+|DICHIARAZIONE "pippo":
+| -) MAP1 <- add_maxcur_map MAP0 "pippo"
+| -) ENV1 <- add_desc_flatEnv ENV0 (name_to_nameId MAP1 "pippo") DESC
+|
+|ACCESSO "pippo":
+| -) name_to_nameId MAP1 "pippo"
+|
+|PREPARAZIONE ENTRATA BLOCCO INTERNO:
+| -) SNAP <- build_snapshot MAP1
+
+ |[BLOCCO INTERNO]
+ |
+ |DICHIARAZIONE "pippo":
+ | -) MAP2 <- add_maxcur_map MAP1 "pippo"
+ | -) ENV2 <- add_desc_flatEnv ENV (name_to_nameId MAP2 "pippo") DESC
+ |
+ |ACCESSO "pippo":
+ | -) name_to_nameId MAP2 "pippo"
+ |
+ |PREPARAZIONE USCITA BLOCCO INTERNO:
+ | -) MAP3 <- rollback_map MAP2 SNAP
+
+| ...
+*)
+
+(* mini test
+definition pippo ≝ [ ch_P ].
+definition pluto ≝ [ ch_Q ].
+definition pippodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
+definition pippodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
+definition pippodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2).
+definition plutodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
+definition plutodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
+definition plutodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_WORD16) 2).
+
+definition map1 ≝ add_maxcur_map empty_trasfMap pippo.
+definition env1 ≝ add_desc_flatEnv empty_flatEnv (name_to_nameId map1 pippo) pippodesc1.
+definition map2 ≝ add_maxcur_map map1 pluto.
+definition env2 ≝ add_desc_flatEnv env1 (name_to_nameId map2 pluto) plutodesc1.
+
+definition snap1 ≝ build_snapshot map2.
+
+definition map3 ≝ add_maxcur_map map2 pippo.
+definition env3 ≝ add_desc_flatEnv env2 (name_to_nameId map3 pippo) pippodesc2.
+definition map4 ≝ add_maxcur_map map3 pluto.
+definition env4 ≝ add_desc_flatEnv env3 (name_to_nameId map4 pluto) plutodesc2.
+
+definition snap2 ≝ build_snapshot map4.
+
+definition map5 ≝ add_maxcur_map map4 pippo.
+definition env5 ≝ add_desc_flatEnv env4 (name_to_nameId map5 pippo) pippodesc3.
+definition map6 ≝ add_maxcur_map map5 pluto.
+definition env6 ≝ add_desc_flatEnv env5 (name_to_nameId map6 pluto) plutodesc3.
+
+definition map7 ≝ rollback_map map6 snap2.
+
+definition map8 ≝ rollback_map map7 snap1.
+
+lemma checkenv : None ? = Some ? env6.
+normalize; elim daemon.
+qed.
+
+lemma checkmap : None ? = Some ? map8.
+normalize; elim daemon.
+qed.
+
+lemma checksnap : None ? = Some ? snap2.
+normalize; elim daemon.
+qed.
+*)
(* PASSO 1 : da PREAST a AST *)
(* ************************* *)
+(* NB: ASSERTO
+ al parser spetta il compito di rigettare le condizioni statiche verificabili
+ - divisione per valore 0
+ al parser spetta il compito di collassare le espressioni statiche
+ - val1+val2 -> val3, ...
+ al parser spetta il compito di collassare gli statement con condizioni statiche
+ - if(true) { b1 } else { b2 } -> b1, ...
+ al parser spetta il compito di individuare divergenza e dead code
+ - while(true) { b1 } -> loop infinito, ...
+*)
+
(* operatore di cast *)
definition preast_to_ast_expr_check ≝
-λe:aux_env_type.λsig:Σt'.ast_expr e t'.λt:ast_base_type.
- match sig with [ sigma_intro t' expr ⇒
- match eq_ast_base_type t' t
- return λx.eq_ast_base_type t' t = x → option (ast_expr e t)
- with
- [ true ⇒ λp:(eq_ast_base_type t' t = true).Some ? (eq_rect ? t' (λt.ast_expr e t) expr t (eqastbasetype_to_eq ?? p))
- | false ⇒ λp:(eq_ast_base_type t' t = false).None ?
- ] (refl_eq ? (eq_ast_base_type t' t))
- ].
-
-definition preast_to_ast_right_expr_check ≝
-λe:aux_env_type.λsig:Σt'.ast_right_expr e t'.λt:ast_type.
+λe:aux_env_type.λsig:(Σt'.ast_expr e t').λt:ast_type.
match sig with [ sigma_intro t' expr ⇒
match eq_ast_type t' t
- return λx.eq_ast_type t' t = x → option (ast_right_expr e t)
+ return λx.eq_ast_type t' t = x → option (ast_expr e t)
with
- [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_right_expr e t) expr t (eqasttype_to_eq ?? p))
+ [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_expr e t) expr t (eqasttype_to_eq ?? p))
| false ⇒ λp:(eq_ast_type t' t = false).None ?
] (refl_eq ? (eq_ast_type t' t))
].
].
definition preast_to_ast_var_checkb ≝
-λe:aux_env_type.λt:ast_type.λsig:Σb'.ast_var e b' t.λb:bool.
+λe:aux_env_type.λt:ast_type.λsig:(Σb'.ast_var e b' t).λb:bool.
match sig with [ sigma_intro b' var ⇒
match eq_bool b' b
return λx.eq_bool b' b = x → option (ast_var e b t)
].
definition preast_to_ast_var_checkt ≝
-λe:aux_env_type.λb:bool.λsig:Σt'.ast_var e b t'.λt:ast_type.
+λe:aux_env_type.λb:bool.λsig:(Σt'.ast_var e b t').λt:ast_type.
match sig with [ sigma_intro t' var ⇒
match eq_ast_type t' t
return λx.eq_ast_type t' t = x → option (ast_var e b t)
].
definition preast_to_ast_var_check ≝
-λe:aux_env_type.λsig:Σb'.(Σt'.ast_var e b' t').λb:bool.λt:ast_type.
+λe:aux_env_type.λsig:(Σb'.(Σt'.ast_var e b' t')).λb:bool.λt:ast_type.
opt_map ?? (preast_to_ast_var_checkt e (sigmaFst ?? sig) (sigmaSnd ?? sig) t)
(λres1.opt_map ?? (preast_to_ast_var_checkb e t ≪(sigmaFst ?? sig),res1≫ b)
(λres2.Some ? res2)).
PREAST_EXPR_W32toW16: preast_expr → preast_expr
PREAST_EXPR_ID: preast_var → preast_expr
*)
-let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) on preast : option (Σt:ast_base_type.ast_expr e t) ≝
+let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) on preast : option (Σt.ast_expr e t) ≝
match preast with
- [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_BYTE8 e val)≫
- | PREAST_EXPR_WORD16 val ⇒ Some ? ≪AST_BASE_TYPE_WORD16,(AST_EXPR_WORD16 e val)≫
- | PREAST_EXPR_WORD32 val ⇒ Some ? ≪AST_BASE_TYPE_WORD32,(AST_EXPR_WORD32 e val)≫
+ [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪?,(AST_EXPR_BYTE8 e val)≫
+ | PREAST_EXPR_WORD16 val ⇒ Some ? ≪?,(AST_EXPR_WORD16 e val)≫
+ | PREAST_EXPR_WORD32 val ⇒ Some ? ≪?,(AST_EXPR_WORD32 e val)≫
| PREAST_EXPR_NEG subExpr ⇒
opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:Σt:ast_base_type.ast_expr e t.
- Some ? ≪(sigmaFst ?? sigmaRes),(AST_EXPR_NEG e (sigmaFst ?? sigmaRes) (sigmaSnd ?? sigmaRes))≫)
+ (λsigmaRes:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType))
+ (λres.Some ? ≪?,(AST_EXPR_NEG e ? res)≫)
+ | _ ⇒ None ? ])
| PREAST_EXPR_NOT subExpr ⇒
opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:Σt:ast_base_type.ast_expr e t.
- Some ? ≪(sigmaFst ?? sigmaRes),(AST_EXPR_NOT e (sigmaFst ?? sigmaRes) (sigmaSnd ?? sigmaRes))≫)
+ (λsigmaRes:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType))
+ (λres.Some ? ≪?,(AST_EXPR_NOT e ? res)≫)
+ | _ ⇒ None ? ])
| PREAST_EXPR_COM subExpr ⇒
opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:Σt:ast_base_type.ast_expr e t.
- Some ? ≪(sigmaFst ?? sigmaRes),(AST_EXPR_COM e (sigmaFst ?? sigmaRes) (sigmaSnd ?? sigmaRes))≫)
+ (λsigmaRes:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType))
+ (λres.Some ? ≪?,(AST_EXPR_COM e ? res)≫)
+ | _ ⇒ None ? ])
| PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
- (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_ADD e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_ADD e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
| PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
- (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_SUB e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_SUB e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
| PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
- (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_MUL e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_MUL e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
| PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
- (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_DIV e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_DIV e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
| PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 AST_BASE_TYPE_BYTE8)
- (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_SHR e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres2.Some ? ≪?,(AST_EXPR_SHR e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
| PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 AST_BASE_TYPE_BYTE8)
- (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_SHL e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres2.Some ? ≪?,(AST_EXPR_SHL e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
| PREAST_EXPR_GT subExpr1 subExpr2 ⇒
opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
- (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_GT e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_GT e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
| PREAST_EXPR_GTE subExpr1 subExpr2 ⇒
opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
- (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_GTE e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_GTE e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
| PREAST_EXPR_LT subExpr1 subExpr2 ⇒
opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
- (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_LT e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_LT e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
| PREAST_EXPR_LTE subExpr1 subExpr2 ⇒
opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
- (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_LTE e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_LTE e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
| PREAST_EXPR_EQ subExpr1 subExpr2 ⇒
opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
- (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_EQ e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_EQ e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
| PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒
opt_map ?? (preast_to_ast_expr subExpr1 e)
- (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
- (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
- (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_NEQ e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_NEQ e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
| PREAST_EXPR_B8toW16 subExpr ⇒
opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr_check e sigmaRes AST_BASE_TYPE_BYTE8)
- (λres.Some ? ≪AST_BASE_TYPE_WORD16,(AST_EXPR_B8toW16 e res)≫))
+ (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres.Some ? ≪?,(AST_EXPR_B8toW16 e res)≫))
| PREAST_EXPR_B8toW32 subExpr ⇒
opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr_check e sigmaRes AST_BASE_TYPE_BYTE8)
- (λres.Some ? ≪AST_BASE_TYPE_WORD32,(AST_EXPR_B8toW32 e res)≫))
+ (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres.Some ? ≪?,(AST_EXPR_B8toW32 e res)≫))
| PREAST_EXPR_W16toB8 subExpr ⇒
opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr_check e sigmaRes AST_BASE_TYPE_WORD16)
- (λres.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_W16toB8 e res)≫))
+ (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
+ (λres.Some ? ≪?,(AST_EXPR_W16toB8 e res)≫))
| PREAST_EXPR_W16toW32 subExpr ⇒
opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr_check e sigmaRes AST_BASE_TYPE_WORD16)
- (λres.Some ? ≪AST_BASE_TYPE_WORD32,(AST_EXPR_W16toW32 e res)≫))
+ (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
+ (λres.Some ? ≪?,(AST_EXPR_W16toW32 e res)≫))
| PREAST_EXPR_W32toB8 subExpr ⇒
opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr_check e sigmaRes AST_BASE_TYPE_WORD32)
- (λres.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_W32toB8 e res)≫))
+ (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
+ (λres.Some ? ≪?,(AST_EXPR_W32toB8 e res)≫))
| PREAST_EXPR_W32toW16 subExpr ⇒
opt_map ?? (preast_to_ast_expr subExpr e)
- (λsigmaRes:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr_check e sigmaRes AST_BASE_TYPE_WORD32)
- (λres.Some ? ≪AST_BASE_TYPE_WORD16,(AST_EXPR_W32toW16 e res)≫))
+ (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
+ (λres.Some ? ≪?,(AST_EXPR_W32toW16 e res)≫))
- | PREAST_EXPR_ID var ⇒
+ | PREAST_EXPR_ID var ⇒
opt_map ?? (preast_to_ast_var var e)
- (λsigmaRes:(Σb:bool.(Σt:ast_type.ast_var e b t)).
+ (λsigmaRes:(Σb.(Σt.ast_var e b t)).
match sigmaRes with [ sigma_intro b sigmaRes' ⇒
match sigmaRes' with [ sigma_intro t _ ⇒
- match t with
- [ AST_TYPE_BASE bType ⇒
- opt_map ?? (preast_to_ast_var_check e sigmaRes b (AST_TYPE_BASE bType))
- (λres.Some ? ≪bType,(AST_EXPR_ID e b bType res)≫)
- | _ ⇒ None ? ]]])
+ opt_map ?? (preast_to_ast_var_check e sigmaRes b t)
+ (λres.Some ? ≪?,(AST_EXPR_ID e ?? res)≫)]])
]
(*
PREAST_VAR_ID: aux_str_type → preast_var
PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
PREAST_VAR_STRUCT: preast_var → nat → preast_var
*)
-and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option (Σb:bool.(Σt:ast_type.ast_var e b t)) ≝
+and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option (Σb.(Σt.ast_var e b t)) ≝
match preast with
[ PREAST_VAR_ID name ⇒
match checkb_desc_env e name
- return λx.checkb_desc_env e name = x → option (Σb:bool.(Σt:ast_type.ast_var e b t))
+ return λx.checkb_desc_env e name = x → option (Σb.(Σt.ast_var e b t))
with
[ true ⇒ λp:(checkb_desc_env e name = true).
let desc ≝ get_desc_env e name in
| PREAST_VAR_ARRAY subVar expr ⇒
opt_map ?? (preast_to_ast_var subVar e)
- (λsigmaRes:(Σb:bool.(Σt:ast_type.ast_var e b t)).
- match sigmaRes with [ sigma_intro b sigmaRes' ⇒
- match sigmaRes' with [ sigma_intro t _ ⇒
+ (λsigmaResV:(Σb.(Σt.ast_var e b t)).
+ match sigmaResV with [ sigma_intro b sigmaResV' ⇒
+ match sigmaResV' with [ sigma_intro t _ ⇒
match t with
[ AST_TYPE_ARRAY subType dim ⇒
- opt_map ?? (preast_to_ast_var_check e sigmaRes b (AST_TYPE_ARRAY subType dim))
+ opt_map ?? (preast_to_ast_var_check e sigmaResV b (AST_TYPE_ARRAY subType dim))
(λresVar.
(* ASSERTO:
1) se l'indice e' un'espressione riducibile ad un valore deve essere gia'
OUT_OF_BOUND sara' fatto a run time
*)
match (match expr with
- [ PREAST_EXPR_BYTE8 val ⇒ (λx.leb (nat_of_byte8 val) dim)
- | PREAST_EXPR_WORD16 val ⇒ (λx.leb (nat_of_word16 val) dim)
- | PREAST_EXPR_WORD32 val ⇒ (λx.leb (nat_of_word32 val) dim)
+ [ PREAST_EXPR_BYTE8 val ⇒ (λx.ltb (nat_of_byte8 val) dim)
+ | PREAST_EXPR_WORD16 val ⇒ (λx.ltb (nat_of_word16 val) dim)
+ | PREAST_EXPR_WORD32 val ⇒ (λx.ltb (nat_of_word32 val) dim)
| _ ⇒ (λx.true) ]) expr with
[ true ⇒
opt_map ?? (preast_to_ast_expr expr e)
- (λsigmaRes:Σt:ast_base_type.ast_expr e t.
- match sigmaRes with [ sigma_intro t resExpr ⇒
- Some ? ≪b,≪subType,(AST_VAR_ARRAY e b subType dim resVar (AST_BASE_EXPR e t resExpr))≫≫ ])
+ (λsigmaResE:(Σt.ast_expr e t).
+ match sigmaFst ?? sigmaResE with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaResE (AST_TYPE_BASE bType))
+ (λresExpr.Some ? ≪b,≪subType,(AST_VAR_ARRAY e b subType dim resVar (AST_BASE_EXPR e bType resExpr))≫≫)
+ | _ ⇒ None ? ])
| false ⇒ None ? ])
| _ ⇒ None ? ]]])
| PREAST_VAR_STRUCT subVar field ⇒
opt_map ?? (preast_to_ast_var subVar e)
- (λsigmaRes:(Σb:bool.(Σt:ast_type.ast_var e b t)).
+ (λsigmaRes:(Σb.(Σt.ast_var e b t)).
match sigmaRes with [ sigma_intro b sigmaRes' ⇒
match sigmaRes' with [ sigma_intro t _ ⇒
match t with
opt_map ?? (preast_to_ast_var_check e sigmaRes b (AST_TYPE_STRUCT nelSubType))
(λresVar.
match ltb field (len_neList ? nelSubType)
- return λx.(ltb field (len_neList ? nelSubType) = x) → option (Σb:bool.(Σt:ast_type.ast_var e b t))
+ return λx.(ltb field (len_neList ? nelSubType) = x) → option (Σb.(Σt.ast_var e b t))
with
[ true ⇒ λp:(ltb field (len_neList ? nelSubType) = true).
Some ? ≪b,≪(abs_nth_neList ? nelSubType field),(AST_VAR_STRUCT e b nelSubType field resVar p)≫≫
Π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:ast_type.aux_ast_init_type t) ≝
+let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (Σt.aux_ast_init_type t) ≝
match preast with
[ PREAST_INIT_VAL_BYTE8 val ⇒
- Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_BYTE8),val≫
+ Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_BYTE8),val≫
| PREAST_INIT_VAL_WORD16 val ⇒
- Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD16),val≫
+ Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD16),val≫
| PREAST_INIT_VAL_WORD32 val ⇒
- Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD32),val≫
+ Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD32),val≫
| PREAST_INIT_VAL_ARRAY nelSubVal ⇒
- let rec aux (nel:ne_list preast_init_val) on nel : option (Σt:ast_type.aux_ast_init_type t) ≝
+ let rec aux (nel:ne_list preast_init_val) on nel : option (Σt.aux_ast_init_type t) ≝
match nel with
[ ne_nil h ⇒
opt_map ?? (preast_to_ast_init_val_aux h)
(λsigmaRes.match sigmaRes with [ sigma_intro t res ⇒
- Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_ARRAY t 0),res≫ ])
+ Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_ARRAY t 0),res≫ ])
| ne_cons h tl ⇒
opt_map ?? (preast_to_ast_init_val_aux h)
- (λsigmaRes1:(Σt:ast_type.aux_ast_init_type t).opt_map ?? (aux tl)
- (λsigmaRes2:(Σt:ast_type.aux_ast_init_type t).
+ (λsigmaRes1:(Σt.aux_ast_init_type t).opt_map ?? (aux tl)
+ (λsigmaRes2:(Σt.aux_ast_init_type t).
match sigmaRes1 with [ sigma_intro t1 res1 ⇒
match sigmaRes2 with [ sigma_intro t2 res2 ⇒
match t2 with
[ AST_TYPE_ARRAY bType dim ⇒
match eq_ast_type t1 bType
- return λx.(eq_ast_type t1 bType = x) → option (Σt:ast_type.aux_ast_init_type t)
+ return λx.(eq_ast_type t1 bType = x) → option (Σt.aux_ast_init_type t)
with
[ true ⇒ λp:(eq_ast_type t1 bType = true).
match eq_ast_type t2 (AST_TYPE_ARRAY bType dim)
- return λy.(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = y) → option (Σt:ast_type.aux_ast_init_type t)
+ return λy.(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = y) → option (Σt.aux_ast_init_type t)
with
[ true ⇒ λp':(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = true).
- Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_ARRAY bType (S dim)),
- (preast_to_ast_init_val_aux_array bType dim
- (pair (aux_ast_init_type bType) (aux_ast_init_type (AST_TYPE_ARRAY bType dim))
- (eq_rect ? t1 (λw.aux_ast_init_type w) res1 bType (eqasttype_to_eq ?? p))
- (eq_rect ? t2 (λz.aux_ast_init_type z) res2 (AST_TYPE_ARRAY bType dim) (eqasttype_to_eq ?? p'))))≫
+ Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_ARRAY bType (S dim)),
+ (preast_to_ast_init_val_aux_array bType dim
+ (pair (aux_ast_init_type bType) (aux_ast_init_type (AST_TYPE_ARRAY bType dim))
+ (eq_rect ? t1 (λw.aux_ast_init_type w) res1 bType (eqasttype_to_eq ?? p))
+ (eq_rect ? t2 (λz.aux_ast_init_type z) res2 (AST_TYPE_ARRAY bType dim) (eqasttype_to_eq ?? p'))))≫
| false ⇒ λp':(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = false).None ?
] (refl_eq ? (eq_ast_type t2 (AST_TYPE_ARRAY bType dim)))
| false ⇒ λp:(eq_ast_type t1 bType = false).None ?
] in aux nelSubVal
| PREAST_INIT_VAL_STRUCT nelSubVal ⇒
- let rec aux (nel:ne_list preast_init_val) on nel : option (Σt:ast_type.aux_ast_init_type t) ≝
+ let rec aux (nel:ne_list preast_init_val) on nel : option (Σt.aux_ast_init_type t) ≝
match nel with
[ ne_nil h ⇒
opt_map ?? (preast_to_ast_init_val_aux h)
- (λsigmaRes:(Σt:ast_type.aux_ast_init_type t).match sigmaRes with [ sigma_intro t res ⇒
- Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_STRUCT (« t £»)),res≫ ])
+ (λ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≫ ])
| ne_cons h tl ⇒
opt_map ?? (preast_to_ast_init_val_aux h)
- (λsigmaRes1:(Σt:ast_type.aux_ast_init_type t).opt_map ?? (aux tl)
- (λsigmaRes2:(Σt:ast_type.aux_ast_init_type t).
+ (λsigmaRes1:(Σt.aux_ast_init_type t).opt_map ?? (aux tl)
+ (λsigmaRes2:(Σt.aux_ast_init_type t).
match sigmaRes1 with [ sigma_intro t1 res1 ⇒
match sigmaRes2 with [ sigma_intro t2 res2 ⇒
match t2 with
[ AST_TYPE_STRUCT nelSubType ⇒
match eq_ast_type t2 (AST_TYPE_STRUCT nelSubType)
- return λx.(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = x) → option (Σt:ast_type.aux_ast_init_type t)
+ 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:ast_type.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
- (eq_rect ? t2 (λy.aux_ast_init_type y) res2 (AST_TYPE_STRUCT nelSubType) (eqasttype_to_eq ?? p))))≫
+ 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
+ (eq_rect ? t2 (λy.aux_ast_init_type y) res2 (AST_TYPE_STRUCT nelSubType) (eqasttype_to_eq ?? p))))≫
| false ⇒ λp:(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = false).None ?
] (refl_eq ? (eq_ast_type t2 (AST_TYPE_STRUCT nelSubType)))
| _ ⇒ None ? ]]]))
PREAST_INIT_VAR: preast_var → preast_init
PREAST_INIT_VAL: preast_init_val → preast_init
*)
-definition preast_to_ast_init : preast_init → Πe.option (Σt:ast_type.ast_init e t) ≝
+definition preast_to_ast_init : preast_init → Πe.option (Σt.ast_init e t) ≝
λpreast:preast_init.λe:aux_env_type.match preast with
[ PREAST_INIT_VAR var ⇒
opt_map ?? (preast_to_ast_var var e)
- (λsigmaRes:(Σb:bool.(Σt:ast_type.ast_var e b t)).
- Some (Σt:ast_type.ast_init e t) ≪?,(AST_INIT_VAR e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫)
+ (λsigmaRes:(Σb.(Σt.ast_var e b t)).
+ Some ? ≪?,(AST_INIT_VAR e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫)
| PREAST_INIT_VAL val ⇒
opt_map ?? (preast_to_ast_init_val_aux val)
- (λsigmaRes:(Σt:ast_type.aux_ast_init_type t).
- Some (Σt:ast_type.ast_init e t) ≪?,(AST_INIT_VAL e ? (sigmaSnd ?? sigmaRes))≫)
+ (λsigmaRes:(Σt.aux_ast_init_type t).
+ Some ? ≪?,(AST_INIT_VAL e ? (sigmaSnd ?? sigmaRes))≫)
].
(*
PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
*)
-definition preast_to_ast_right_expr : preast_expr → Πe.option (Σt:ast_type.ast_right_expr e t) ≝
-λpreast:preast_expr.λe:aux_env_type.match preast with
- (* NB: PREAST_EXPR_ID viene sempre tradotto come AST_RIGHT_EXPR_VAR *)
- [ PREAST_EXPR_ID var ⇒
- opt_map ?? (preast_to_ast_var var e)
- (λsigmaRes:(Σb:bool.(Σt:ast_type.ast_var e b t)).
- Some (Σt:ast_type.ast_right_expr e t) ≪?,(AST_RIGHT_EXPR_VAR e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫)
-
- | _ ⇒
- opt_map ?? (preast_to_ast_expr preast e)
- (λsigmaRes:(Σt:ast_base_type.ast_expr e t).
- Some (Σt:ast_type.ast_right_expr e t) ≪ (AST_TYPE_BASE ?),(AST_RIGHT_EXPR_BASE e ? (sigmaSnd ?? sigmaRes))≫)
- ].
-
definition preast_to_ast_base_expr : preast_expr → Πe.option (ast_base_expr e) ≝
λpreast:preast_expr.λe:aux_env_type.
opt_map ?? (preast_to_ast_expr preast e)
- (λsigmaRes:(Σt:ast_base_type.ast_expr e t).
- Some (ast_base_expr e) (AST_BASE_EXPR e ? (sigmaSnd ?? sigmaRes))).
+ (λsigmaRes:(Σt.ast_expr e t).
+ match sigmaFst ?? sigmaRes with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType))
+ (λres.Some ? (AST_BASE_EXPR e ? res))
+ | _ ⇒ None ? ]).
let rec preast_to_ast_stm (preast:preast_stm) (e:aux_env_type) on preast : option (ast_stm e) ≝
match preast with
[ PREAST_STM_ASG var expr ⇒
opt_map ?? (preast_to_ast_var var e)
- (λsigmaResV:(Σb:bool.(Σt:ast_type.ast_var e b t)).
+ (λsigmaResV:(Σb.(Σt.ast_var e b t)).
match sigmaResV with [ sigma_intro _ sigmaResV' ⇒
match sigmaResV' with [ sigma_intro t _ ⇒
opt_map ?? (preast_to_ast_var_check e sigmaResV false t)
- (λresVar.opt_map ?? (preast_to_ast_right_expr expr e)
- (λsigmaResE:(Σt:ast_type.ast_right_expr e t).opt_map ?? (preast_to_ast_right_expr_check e sigmaResE t)
+ (λresVar.opt_map ?? (preast_to_ast_expr expr e)
+ (λsigmaResE:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaResE t)
(λresExpr.Some ? (AST_STM_ASG e t resVar resExpr)
)))]])
| PREAST_STM_WHILE expr decl ⇒
opt_map ?? (preast_to_ast_base_expr expr e)
- (λresExpr.opt_map ?? (preast_to_ast_decl decl e)
+ (λresExpr.opt_map ?? (preast_to_ast_decl decl (enter_env e))
(λresDecl.Some ? (AST_STM_WHILE e resExpr resDecl)))
-
+
| PREAST_STM_IF nelExprDecl optDecl ⇒
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) e)
+ (λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) (enter_env e))
(λresDecl.opt_map ?? 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 e (nil ?)))))
+ (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
[ None ⇒ Some ? (AST_STM_IF e (cut_last_neList ? res) (None ?))
- | Some decl ⇒ opt_map ?? (preast_to_ast_decl decl e)
+ | Some decl ⇒ opt_map ?? (preast_to_ast_decl decl (enter_env e))
(λresDecl.Some ? (AST_STM_IF e (cut_last_neList ? res) (Some ? resDecl)))
])
]
λpreast:preast_root.match preast with
[ PREAST_ROOT decl ⇒ opt_map ?? (preast_to_ast_decl decl empty_env)
(λres.Some ? (AST_ROOT res)) ].
+
+(* mini test
+definition prova ≝
+PREAST_ROOT (
+ 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_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〉)))
+ ]
+ )
+ )
+ ]
+ )
+).
+
+lemma checkprova : None ? = preast_to_ast prova.
+normalize;
+*)
-string/ascii_min.ma freescale/byte8.ma
-string/string.ma compiler/utility.ma string/ascii_min.ma
-compiler/ast_tree.ma compiler/environment.ma
compiler/preast_tree.ma compiler/ast_type.ma compiler/utility.ma freescale/word32.ma string/string.ma
-compiler/environment.ma compiler/ast_type.ma freescale/word32.ma string/string.ma
-compiler/utility.ma freescale/extra.ma
-compiler/ast_type.ma compiler/utility.ma freescale/word32.ma
-compiler/preast_to_ast.ma compiler/ast_tree.ma compiler/preast_tree.ma
+compiler/astfe_tree.ma compiler/ast_tree.ma compiler/ast_type.ma compiler/env_to_flatenv.ma compiler/utility.ma freescale/word32.ma string/string.ma
+freescale/exadecim.ma freescale/extra.ma
+freescale/memory_struct.ma freescale/translation.ma
+string/ascii_min.ma freescale/byte8.ma
+freescale/memory_bits.ma freescale/memory_trees.ma
+freescale/opcode.ma freescale/aux_bases.ma
freescale/extra.ma datatypes/constructors.ma list/list.ma logic/connectives.ma nat/div_and_mod.ma nat/primes.ma
-freescale/table_RS08_tests.ma freescale/table_RS08.ma
+freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma
+compiler/env_to_flatenv.ma compiler/environment.ma
+freescale/table_RS08.ma freescale/opcode.ma
+freescale/memory_trees.ma freescale/memory_struct.ma
freescale/table_HC05_tests.ma freescale/table_HC05.ma
-freescale/load_write.ma freescale/model.ma
-freescale/byte8.ma freescale/exadecim.ma
+freescale/aux_bases.ma freescale/word16.ma
+string/string.ma compiler/utility.ma string/ascii_min.ma
freescale/table_HCS08.ma freescale/opcode.ma
-freescale/multivm.ma freescale/load_write.ma
-freescale/translation.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma
-freescale/model.ma freescale/status.ma
-freescale/medium_tests_lemmas.ma freescale/medium_tests_tools.ma
+freescale/table_HC08_tests.ma freescale/table_HC08.ma
+freescale/table_RS08_tests.ma freescale/table_RS08.ma
freescale/medium_tests.ma freescale/medium_tests_lemmas.ma
-freescale/table_HC08.ma freescale/opcode.ma
-freescale/opcode.ma freescale/aux_bases.ma
-freescale/memory_trees.ma freescale/memory_struct.ma
-freescale/table_HCS08_tests.ma freescale/table_HCS08.ma
-freescale/exadecim.ma freescale/extra.ma
-freescale/word16.ma freescale/byte8.ma
freescale/medium_tests_tools.ma freescale/multivm.ma
+compiler/ast_tree.ma compiler/environment.ma
+freescale/table_HCS08_tests.ma freescale/table_HCS08.ma
+freescale/medium_tests_lemmas.ma freescale/medium_tests_tools.ma
+freescale/table_HC05.ma freescale/opcode.ma
freescale/status.ma freescale/memory_abs.ma
-freescale/memory_func.ma freescale/memory_struct.ma
-freescale/memory_bits.ma freescale/memory_trees.ma
-freescale/table_HC08_tests.ma freescale/table_HC08.ma
freescale/micro_tests.ma freescale/multivm.ma
-freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma
-freescale/table_RS08.ma freescale/opcode.ma
-freescale/table_HC05.ma freescale/opcode.ma
-freescale/aux_bases.ma freescale/word16.ma
-freescale/memory_struct.ma freescale/translation.ma
+freescale/word16.ma freescale/byte8.ma
+freescale/model.ma freescale/status.ma
+freescale/table_HC08.ma freescale/opcode.ma
+freescale/multivm.ma freescale/load_write.ma
+compiler/environment.ma compiler/ast_type.ma freescale/word32.ma string/string.ma
+freescale/load_write.ma freescale/model.ma
+compiler/sigma.ma
+compiler/ast_to_astfe.ma compiler/astfe_tree.ma
+compiler/utility.ma freescale/extra.ma
+compiler/ast_type.ma compiler/utility.ma freescale/word32.ma
+compiler/preast_to_ast.ma compiler/ast_tree.ma compiler/preast_tree.ma compiler/sigma.ma
+freescale/translation.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma
+freescale/byte8.ma freescale/exadecim.ma
freescale/word32.ma freescale/word16.ma
+freescale/memory_func.ma freescale/memory_struct.ma
datatypes/constructors.ma
list/list.ma
logic/connectives.ma
(* strlen *)
definition strLen_str ≝ λstr:aux_str_type.len_list ? str.
+
+(* ************ *)
+(* STRINGA + ID *)
+(* ************ *)
+
+(* tipo pubblico *)
+inductive aux_strId_type : Type ≝
+ STR_ID: aux_str_type → nat → aux_strId_type.
+
+(* getter *)
+definition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
+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')).
projects / helm.git / commitdiff