include "compiler/preast_tree.ma".
include "compiler/ast_tree.ma".
+include "compiler/sigma.ma".
-(* *********************** *)
-(* PASSO 1 DI COMPILAZIONE *)
-(* *********************** *)
+(* ************************* *)
+(* PASSO 1 : da PREAST a AST *)
+(* ************************* *)
-(*
- PREAST_VAR_ID: aux_str_type → preast_var
- PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
- PREAST_VAR_STRUCT: ne_list preast_var → nat → preast_var.
-*)
-let rec evaluate_var_type (preast:preast_var) (e:aux_env_type) on preast : option (Prod bool ast_type) ≝
- match preast with
- [ PREAST_VAR_ID name ⇒
- opt_map ?? (get_desc_env_aux e (None ?) name)
- (λdesc.Some ? (pair ?? (get_const_desc desc) (get_type_desc desc)))
- | PREAST_VAR_ARRAY subVar expr ⇒
- opt_map ?? (evaluate_var_type subVar e)
- (λcDesc.match snd ?? cDesc with
- [ AST_TYPE_ARRAY subType dim ⇒ Some ? (pair ?? (fst ?? cDesc) subType)
- | _ ⇒ None ? ])
- | PREAST_VAR_STRUCT subVar field ⇒
- opt_map ?? (evaluate_var_type subVar e)
- (λcDesc.match snd ?? cDesc with
- [ AST_TYPE_STRUCT nelSubType ⇒
- opt_map ?? (nth_neList ? nelSubType field)
- (λsubType.Some ? (pair ?? (fst ?? cDesc) subType))
- | _ ⇒ None ? ])
+(* 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.
+ 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)
+ 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))
+ | false ⇒ λp:(eq_ast_type t' t = false).None ?
+ ] (refl_eq ? (eq_ast_type t' t))
+ ].
+
+definition preast_to_ast_init_check ≝
+λe:aux_env_type.λsig:Σt'.ast_init 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_init e t)
+ with
+ [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_init 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.
+ 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)
+ with
+ [ true ⇒ λp:(eq_bool b' b = true).Some ? (eq_rect ? b' (λb.ast_var e b t) var b (eqbool_to_eq ?? p))
+ | false ⇒ λp:(eq_bool b' b = false).None ?
+ ] (refl_eq ? (eq_bool b' b))
+ ].
+
+definition preast_to_ast_var_checkt ≝
+λ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)
+ with
+ [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_var e b t) var 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_check ≝
+λ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_BYTE8 : byte8 → preast_expr
PREAST_EXPR_WORD16: word16 → preast_expr
PREAST_EXPR_W32toW16: preast_expr → preast_expr
PREAST_EXPR_ID: preast_var → preast_expr
*)
-let rec evaluate_expr_type (preast:preast_expr) (e:aux_env_type) on preast : option ast_base_type ≝
+let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) on preast : option (Σt:ast_base_type.ast_expr e t) ≝
match preast with
- [ PREAST_EXPR_BYTE8 _ ⇒ Some ? AST_BASE_TYPE_BYTE8
- | PREAST_EXPR_WORD16 _ ⇒ Some ? AST_BASE_TYPE_WORD16
- | PREAST_EXPR_WORD32 _ ⇒ Some ? AST_BASE_TYPE_WORD32
- | PREAST_EXPR_NEG subExpr ⇒ evaluate_expr_type subExpr e
- | PREAST_EXPR_NOT subExpr ⇒ evaluate_expr_type subExpr e
- | PREAST_EXPR_COM subExpr ⇒ evaluate_expr_type subExpr e
+ [ 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_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))≫)
+ | 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))≫)
+ | 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))≫)
+
| PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
+ 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)≫)))
| PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
+ 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)≫)))
| PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
+ 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)≫)))
| PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
+ 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)≫)))
+
| PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t2 AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
+ 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)≫)))
| PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t2 AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
+ 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)≫)))
+
| PREAST_EXPR_GT subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
+ 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)≫)))
| PREAST_EXPR_GTE subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
+ 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)≫)))
| PREAST_EXPR_LT subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
+ 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)≫)))
| PREAST_EXPR_LTE subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
+ 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)≫)))
| PREAST_EXPR_EQ subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
+ 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)≫)))
| PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
+ 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)≫)))
+
| PREAST_EXPR_B8toW16 subExpr ⇒
- opt_map ?? (evaluate_expr_type subExpr e)
- (λt.match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? AST_BASE_TYPE_WORD16 | false ⇒ None ? ])
+ 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)≫))
| PREAST_EXPR_B8toW32 subExpr ⇒
- opt_map ?? (evaluate_expr_type subExpr e)
- (λt.match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? AST_BASE_TYPE_WORD32 | false ⇒ None ? ])
+ 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)≫))
| PREAST_EXPR_W16toB8 subExpr ⇒
- opt_map ?? (evaluate_expr_type subExpr e)
- (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD16 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ])
+ 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)≫))
| PREAST_EXPR_W16toW32 subExpr ⇒
- opt_map ?? (evaluate_expr_type subExpr e)
- (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD16 with [ true ⇒ Some ? AST_BASE_TYPE_WORD32 | false ⇒ None ? ])
+ 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)≫))
| PREAST_EXPR_W32toB8 subExpr ⇒
- opt_map ?? (evaluate_expr_type subExpr e)
- (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD32 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ])
+ 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)≫))
| PREAST_EXPR_W32toW16 subExpr ⇒
- opt_map ?? (evaluate_expr_type subExpr e)
- (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD32 with [ true ⇒ Some ? AST_BASE_TYPE_WORD16 | false ⇒ None ? ])
- | PREAST_EXPR_ID var ⇒
- opt_map ?? (evaluate_var_type var e)
- (λcDesc.match snd ?? cDesc with [ AST_TYPE_BASE bType ⇒ Some ? bType | _ ⇒ None ? ])
- ].
+ 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)≫))
-(*
- PREAST_EXPR_BYTE8 : byte8 → preast_expr
- PREAST_EXPR_WORD16: word16 → preast_expr
- PREAST_EXPR_WORD32: word32 → preast_expr
- PREAST_EXPR_NEG: preast_expr → preast_expr
- PREAST_EXPR_NOT: preast_expr → preast_expr
- PREAST_EXPR_COM: preast_expr → preast_expr
- PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
- PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
- PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
- PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_B8toW16 : preast_expr → preast_expr
- PREAST_EXPR_B8toW32 : preast_expr → preast_expr
- PREAST_EXPR_W16toB8 : preast_expr → preast_expr
- PREAST_EXPR_W16toW32: preast_expr → preast_expr
- PREAST_EXPR_W32toB8 : preast_expr → preast_expr
- 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) (t:ast_base_type) on preast : option (ast_expr e t) ≝
- (*match preast
- return λpr:preast_expr.λen:aux_env_type.λtp:ast_base_type.(match pr with
- [ PREAST_EXPR_BYTE8 _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_WORD16 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD16)
- | PREAST_EXPR_WORD32 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD32)
- | PREAST_EXPR_NEG _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_NOT _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_COM _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_ADD _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_SUB _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_MUL _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_DIV _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_SHR _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_SHL _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_GT _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_GTE _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_LT _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_LTE _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_EQ _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_NEQ _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_B8toW16 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD16)
- | PREAST_EXPR_B8toW32 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD32)
- | PREAST_EXPR_W16toB8 _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_W16toW32 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD32)
- | PREAST_EXPR_W32toB8 _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_W32toW16 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD16)
- | PREAST_EXPR_ID _ ⇒ option (ast_expr en tp)
- | _ ⇒ option (ast_expr en tp)
- ])
- with
- [ PREAST_EXPR_BYTE8 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
- [ true ⇒ Some ? (AST_EXPR_BYTE8 e val) | false ⇒ None ? ]
- | PREAST_EXPR_WORD16 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
- [ true ⇒ Some ? (AST_EXPR_WORD16 e val) | false ⇒ None ? ]
- | PREAST_EXPR_WORD32 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD32 with
- [ true ⇒ Some ? (AST_EXPR_WORD32 e val) | false ⇒ None ? ]
- | PREAST_EXPR_NEG subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e t)
- (λres.Some ? (AST_EXPR_NEG e t res))
- | PREAST_EXPR_NOT subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e t)
- (λres.Some ? (AST_EXPR_NOT e t res))
- | PREAST_EXPR_COM subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e t)
- (λres.Some ? (AST_EXPR_COM e t res))
- | PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e t)
- (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
- (λres2.Some ? (AST_EXPR_ADD e t res1 res2)))
- | PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e t)
- (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
- (λres2.Some ? (AST_EXPR_SUB e t res1 res2)))
- | PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e t)
- (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
- (λres2.Some ? (AST_EXPR_MUL e t res1 res2)))
- | PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e t)
- (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
- (λres2.Some ? (AST_EXPR_DIV e t res1 res2)))
- | PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e t)
- (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e AST_BASE_TYPE_BYTE8)
- (λres2.Some ? (AST_EXPR_SHR e t res1 res2)))
- | PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
- opt_map ?? (preast_to_ast_expr subExpr1 e t)
- (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e AST_BASE_TYPE_BYTE8)
- (λres2.Some ? (AST_EXPR_SHL e t res1 res2)))
- | PREAST_EXPR_GT subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
- [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
- (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
- (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
- (λres2.Some ? (AST_EXPR_GT e resType res1 res2))))
- | false ⇒ None ? ]
- | PREAST_EXPR_GTE subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
- [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
- (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
- (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
- (λres2.Some ? (AST_EXPR_GTE e resType res1 res2))))
- | false ⇒ None ? ]
- | PREAST_EXPR_LT subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
- [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
- (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
- (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
- (λres2.Some ? (AST_EXPR_LT e resType res1 res2))))
- | false ⇒ None ? ]
- | PREAST_EXPR_LTE subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
- [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
- (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
- (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
- (λres2.Some ? (AST_EXPR_LTE e resType res1 res2))))
- | false ⇒ None ? ]
- | PREAST_EXPR_EQ subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
- [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
- (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
- (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
- (λres2.Some ? (AST_EXPR_EQ e resType res1 res2))))
- | false ⇒ None ? ]
- | PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
- [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
- (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
- (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
- (λres2.Some ? (AST_EXPR_NEQ e resType res1 res2))))
- | false ⇒ None ? ]
- | PREAST_EXPR_B8toW16 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
- [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_BYTE8)
- (λres.Some ? (AST_EXPR_B8toW16 e res))
- | false ⇒ None ? ]
- | PREAST_EXPR_B8toW32 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD32 with
- [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_BYTE8)
- (λres.Some ? (AST_EXPR_B8toW32 e res))
- | false ⇒ None ? ]
- | PREAST_EXPR_W16toB8 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
- [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD16)
- (λres.Some ? (AST_EXPR_W16toB8 e res))
- | false ⇒ None ? ]
- | PREAST_EXPR_W16toW32 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD32 with
- [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD16)
- (λres.Some ? (AST_EXPR_W16toW32 e res))
- | false ⇒ None ? ]
- | PREAST_EXPR_W32toB8 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
- [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD32)
- (λres.Some ? (AST_EXPR_W32toB8 e res))
- | false ⇒ None ? ]
- | PREAST_EXPR_W32toW16 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
- [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD32)
- (λres.Some ? (AST_EXPR_W32toW16 e res))
- | false ⇒ None ? ]
| PREAST_EXPR_ID var ⇒
- opt_map ?? (evaluate_var_type var e)
- (λcDesc.opt_map ?? (preast_to_ast_var var e (fst ?? cDesc) (AST_TYPE_BASE t))
- (λres.Some ? (AST_EXPR_ID e (fst ?? cDesc) t res)))
- ]*)
- None (ast_expr e t)
+ opt_map ?? (preast_to_ast_var var 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 _ ⇒
+ 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 ? ]]])
+ ]
(*
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.
+ PREAST_VAR_STRUCT: preast_var → nat → preast_var
*)
-and preast_to_ast_var (preast:preast_var) (e:aux_env_type) (c:bool) (t:ast_type) on preast : option (ast_var e c t) ≝
- None (ast_var e c t)
+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)) ≝
+ 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))
+ with
+ [ true ⇒ λp:(checkb_desc_env e name = true).
+ let desc ≝ get_desc_env e name in
+ let b ≝ get_const_desc desc in
+ let t ≝ get_type_desc desc in
+ Some ? ≪b,≪t,(AST_VAR_ID e b t (AST_ID e name (checkbdescenv_to_checkdescenv e name p)))≫≫
+ | false ⇒ λp:(checkb_desc_env e name = false).None ?
+ ] (refl_eq ? (checkb_desc_env e name))
+
+ | 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 _ ⇒
+ match t with
+ [ AST_TYPE_ARRAY subType dim ⇒
+ opt_map ?? (preast_to_ast_var_check e sigmaRes b (AST_TYPE_ARRAY subType dim))
+ (λresVar.
+ (* ASSERTO:
+ 1) se l'indice e' un'espressione riducibile ad un valore deve essere gia'
+ stato fatto dal parser, e qui controllo la condizione OUT_OF_BOUND
+ 2) se l'indice non e' un'espressione riducibile ad un valore il controllo
+ 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)
+ | _ ⇒ (λ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))≫≫ ])
+ | 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)).
+ match sigmaRes with [ sigma_intro b sigmaRes' ⇒
+ match sigmaRes' with [ sigma_intro t _ ⇒
+ match t with
+ [ AST_TYPE_STRUCT nelSubType ⇒
+ 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))
+ 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)≫≫
+ | false ⇒ λp:(ltb field (len_neList ? nelSubType) = false).None ?
+ ] (refl_eq ? (ltb field (len_neList ? nelSubType)))
+ )
+ | _ ⇒ None ? ]]])
+ ].
+
(*
- PREAST_EXPR_BYTE8 : byte8 → preast_expr
- PREAST_EXPR_WORD16: word16 → preast_expr
- PREAST_EXPR_WORD32: word32 → preast_expr
- PREAST_EXPR_NEG: preast_expr → preast_expr
- PREAST_EXPR_NOT: preast_expr → preast_expr
- PREAST_EXPR_COM: preast_expr → preast_expr
- PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
- PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
- PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
- PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_B8toW16 : preast_expr → preast_expr
- PREAST_EXPR_B8toW32 : preast_expr → preast_expr
- PREAST_EXPR_W16toB8 : preast_expr → preast_expr
- PREAST_EXPR_W16toW32: preast_expr → preast_expr
- PREAST_EXPR_W32toB8 : preast_expr → preast_expr
- PREAST_EXPR_W32toW16: preast_expr → preast_expr
- PREAST_EXPR_ID: preast_var → preast_expr
+ PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val
+ PREAST_INIT_VAL_WORD16: word16 → preast_init_val
+ PREAST_INIT_VAL_WORD32: word32 → preast_init_val
+ PREAST_INIT_VAL_ARRAY: ne_list preast_init_val → preast_init_val
+ PREAST_INIT_VAL_STRUCT: ne_list preast_init_val → preast_init_val
+*)
+definition preast_to_ast_init_val_aux_array :
+Πt.Πn.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_ARRAY t n)) → (aux_ast_init_type (AST_TYPE_ARRAY t (S n))) ≝
+λt:ast_type.λn:nat.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_ARRAY t n)).x.
+
+definition preast_to_ast_init_val_aux_struct :
+Πt.Πnel.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)) → (aux_ast_init_type (AST_TYPE_STRUCT («t£»&nel))) ≝
+λt: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) ≝
+ 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≫
+ | PREAST_INIT_VAL_WORD16 val ⇒
+ Some (Σt:ast_type.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≫
+
+ | 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) ≝
+ 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≫ ])
+ | 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).
+ 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)
+ 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)
+ 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'))))≫
+ | 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 ?
+ ] (refl_eq ? (eq_ast_type t1 bType))
+ | _ ⇒ 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) ≝
+ 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≫ ])
+ | 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).
+ 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)
+ 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))))≫
+ | false ⇒ λp:(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = false).None ?
+ ] (refl_eq ? (eq_ast_type t2 (AST_TYPE_STRUCT nelSubType)))
+ | _ ⇒ None ? ]]]))
+ ] in aux nelSubVal
+ ].
+
+(*
+ PREAST_INIT_VAR: preast_var → preast_init
+ PREAST_INIT_VAL: preast_init_val → preast_init
*)
-and preast_to_ast_base_expr (preast:preast_expr) (e:aux_env_type) on preast : option (ast_base_expr e) ≝
- None (ast_base_expr e).
+definition preast_to_ast_init : preast_init → Πe.option (Σt:ast_type.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)))≫)
+
+ | 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))≫)
+ ].
(*
PREAST_STM_ASG: preast_var → preast_expr → preast_stm
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))).
+
let rec preast_to_ast_stm (preast:preast_stm) (e:aux_env_type) on preast : option (ast_stm e) ≝
match preast with
- (* (A) assegnamento *)
[ PREAST_STM_ASG var expr ⇒
- opt_map ?? (evaluate_var_type var e)
- (λcDesc.match fst ?? cDesc with
- (* NO: left non deve essere read only *)
- [ true ⇒ None ?
- (* OK: left e' read write *)
- | false ⇒
- match isntb_ast_base_type (snd ?? cDesc)
- return λx.(isntb_ast_base_type (snd ?? cDesc)) = x → option (ast_stm e)
- with
- (* (A.1) memcpy *)
- [ true ⇒ λp:(isntb_ast_base_type (snd ?? cDesc)) = true.match expr with
- (* OK: right deve essere una var *)
- [ PREAST_EXPR_ID subVar ⇒ opt_map ?? (evaluate_var_type subVar e)
- (λcDesc'.opt_map ?? (preast_to_ast_var var e false (snd ?? cDesc))
- (λresVar.opt_map ?? (preast_to_ast_var subVar e (fst ?? cDesc') (snd ?? cDesc))
- (λresVar'.Some ? (AST_STM_MEMCPY_ASG e (fst ?? cDesc') (snd ?? cDesc)
- (isntbastbasetype_to_isntastbasetype (snd ?? cDesc) p)
- resVar resVar'))))
- (* NO: right non e' una var *)
- | _ ⇒ None ? ]
- (* (A.2) variabile *)
- | false ⇒ λp:(isntb_ast_base_type (snd ?? cDesc)) = false.match snd ?? cDesc with
- [ AST_TYPE_BASE bType ⇒ opt_map ?? (preast_to_ast_expr expr e bType)
- (λresExpr.opt_map ?? (preast_to_ast_var var e false (AST_TYPE_BASE bType))
- (λresVar.Some ? (AST_STM_ASG e bType resVar resExpr)))
- | _ ⇒ None ? ]] (refl_eq ? (isntb_ast_base_type (snd ?? cDesc)))
- ])
+ opt_map ?? (preast_to_ast_var var e)
+ (λsigmaResV:(Σb:bool.(Σt:ast_type.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)
+ (λresExpr.Some ? (AST_STM_ASG e t resVar resExpr)
+ )))]])
- (* (B) while *)
| PREAST_STM_WHILE expr decl ⇒
opt_map ?? (preast_to_ast_base_expr expr e)
(λresExpr.opt_map ?? (preast_to_ast_decl decl e)
(λresDecl.Some ? (AST_STM_WHILE e resExpr resDecl)))
-
- (* (C) if *)
+
| 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)
]
(*
PREAST_NO_DECL: list preast_stm → preast_decl
- PREAST_DECL: bool → aux_str_type → ast_type → option preast_expr → preast_decl → preast_decl.
+ PREAST_DECL: bool → aux_str_type → ast_type → option preast_init → preast_decl → preast_decl
*)
and preast_to_ast_decl (preast:preast_decl) (e:aux_env_type) on preast : option (ast_decl e) ≝
match preast with
- (* (A) nessuna dichiarazione, solo statement *)
[ PREAST_NO_DECL lPreastStm ⇒
- opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (preast_to_ast_stm h e)
- (λh'.opt_map ?? t
- (λt'.Some ? ([h']@t')))) (Some ? (nil ?)) lPreastStm)
- (λres.Some ? (AST_NO_DECL e res))
+ opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (preast_to_ast_stm h e)
+ (λh'.opt_map ?? t
+ (λt'.Some ? ([h']@t')))) (Some ? (nil ?)) lPreastStm)
+ (λres.Some ? (AST_NO_DECL e res))
- (* (B) dichiarazione *)
| PREAST_DECL constFlag decName decType optInitExpr subPreastDecl ⇒
- match checkb_not_already_def_env e decName
- return λx.(checkb_not_already_def_env e decName) = x → option (ast_decl e)
+ match checkb_not_already_def_env e decName
+ return λx.(checkb_not_already_def_env e decName = x) → option (ast_decl e)
with
- (* OK: non era gia' dichiarata *)
- [ true ⇒ λp:(checkb_not_already_def_env e decName) = true.
- match decType with
- (* (B.1) dichiarazione tipo base *)
- [ AST_TYPE_BASE decBaseType ⇒ match optInitExpr with
- (* (B.1.1) tipo base senza inizializzazione *)
- [ None ⇒ opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag (AST_TYPE_BASE decBaseType)))
- (λsubRes.Some ? (AST_BASE_DECL e constFlag decName decBaseType
- (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p)
- (None ?) subRes))
- (* (B.1.2) tipo base con inizializzazione *)
- | Some initExpr ⇒ opt_map ?? (preast_to_ast_expr initExpr e decBaseType)
- (λinitRes.opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag (AST_TYPE_BASE decBaseType)))
- (λsubRes.Some ? (AST_BASE_DECL e constFlag decName decBaseType
- (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p)
- (None ?) subRes)))
- ]
- (* (B.2) dichiarazione record/struttura *)
- | _ ⇒ match optInitExpr with
- (* OK: senza inizializzazione *)
- [ None ⇒ match isntb_ast_base_type decType
- return λy.(isntb_ast_base_type decType) = y → option (ast_decl e)
- with
- [ true ⇒ λp':(isntb_ast_base_type decType) = true.
- opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag decType))
- (λsubRes.Some ? (AST_DECL e constFlag decName decType
- (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p)
- (isntbastbasetype_to_isntastbasetype decType p')
- subRes))
- | false ⇒ λp':(isntb_ast_base_type decType) = false.None ?
- ] (refl_eq ? (isntb_ast_base_type decType))
- (* NO: con inizializzazione *)
- | Some _ ⇒ None ?
- ]
- ]
- (* NO: era gia' dichiarata *)
- | false ⇒ λp:(checkb_not_already_def_env e decName) = false.None ?
- ] (refl_eq ? (checkb_not_already_def_env e decName))
+ [ true ⇒ λp:(checkb_not_already_def_env e decName = true).
+ opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag decType))
+ (λdecl.match optInitExpr with
+ [ None ⇒ Some ? (AST_DECL e constFlag decName decType
+ (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p) (None ?) decl)
+ | Some initExpr ⇒
+ opt_map ?? (preast_to_ast_init initExpr e)
+ (λsigmaRes:(Σt:ast_type.ast_init e t).opt_map ?? (preast_to_ast_init_check e sigmaRes decType)
+ (λresInit.Some ? (AST_DECL e constFlag decName decType
+ (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p) (Some ? resInit) decl)))])
+ | false ⇒ λp:(checkb_not_already_def_env e decName = false).None ?
+ ] (refl_eq ? (checkb_not_already_def_env e decName))
].
(*
- PREAST_ROOT: preast_decl → preast_root.
+ PREAST_ROOT: preast_decl → preast_root
*)
definition preast_to_ast ≝
λpreast:preast_root.match preast with
projects / helm.git / blobdiff