From a8ad55eb789b38c85c5581089308e349e4b0f1a3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 23 Jul 2008 09:53:56 +0000 Subject: [PATCH] Update. --- .../assembly/compiler/ast_to_astfe.ma | 425 ++++++++++++++++++ .../contribs/assembly/compiler/ast_tree.ma | 71 ++- .../contribs/assembly/compiler/astfe_tree.ma | 140 ++++++ .../assembly/compiler/env_to_flatenv.ma | 213 +++++++++ .../assembly/compiler/preast_to_ast.ma | 384 +++++++++------- .../software/matita/contribs/assembly/depends | 60 +-- .../matita/contribs/assembly/string/string.ma | 16 + 7 files changed, 1090 insertions(+), 219 deletions(-) create mode 100755 helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma create mode 100755 helm/software/matita/contribs/assembly/compiler/astfe_tree.ma create mode 100755 helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma diff --git a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma new file mode 100755 index 000000000..054aeedc2 --- /dev/null +++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma @@ -0,0 +1,425 @@ +(**************************************************************************) +(* ___ *) +(* ||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; +*) diff --git a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma index 6fa1b3ffd..6ba41f18c 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma @@ -33,53 +33,53 @@ inductive ast_id (e:aux_env_type) : bool → ast_type → Type ≝ (* -------------------------- *) (* 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 ≝ @@ -93,16 +93,7 @@ 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. (* -------------------------- *) @@ -146,11 +137,11 @@ inductive ast_init (e:aux_env_type) : ast_type → Type ≝ (* 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 ≝ diff --git a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma new file mode 100755 index 000000000..82666acf3 --- /dev/null +++ b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma @@ -0,0 +1,140 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ?)). diff --git a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma new file mode 100755 index 000000000..4d3a092c1 --- /dev/null +++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma @@ -0,0 +1,213 @@ +(**************************************************************************) +(* ___ *) +(* ||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. +*) diff --git a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma index 27c1e5477..141544c33 100755 --- a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma +++ b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma @@ -27,25 +27,25 @@ include "compiler/sigma.ma". (* 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)) ]. @@ -62,7 +62,7 @@ definition preast_to_ast_init_check ≝ ]. 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) @@ -73,7 +73,7 @@ definition preast_to_ast_var_checkb ≝ ]. 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) @@ -84,7 +84,7 @@ definition preast_to_ast_var_checkt ≝ ]. 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)). @@ -116,134 +116,203 @@ definition preast_to_ast_var_check ≝ 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 @@ -255,12 +324,12 @@ and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option ( | 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' @@ -269,21 +338,24 @@ and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option ( 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 @@ -291,7 +363,7 @@ and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option ( 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)≫≫ @@ -316,43 +388,43 @@ 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) ≝ +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 ? @@ -362,29 +434,29 @@ let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option ( ] 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 ? ]]])) @@ -395,17 +467,17 @@ let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option ( 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))≫) ]. (* @@ -413,54 +485,44 @@ definition preast_to_ast_init : preast_init → Πe.option (Σt:ast_type.ast_ini 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))) ]) ] @@ -501,3 +563,23 @@ definition preast_to_ast ≝ λ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; +*) diff --git a/helm/software/matita/contribs/assembly/depends b/helm/software/matita/contribs/assembly/depends index 8038c648e..9e0caab22 100644 --- a/helm/software/matita/contribs/assembly/depends +++ b/helm/software/matita/contribs/assembly/depends @@ -1,40 +1,44 @@ -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 diff --git a/helm/software/matita/contribs/assembly/string/string.ma b/helm/software/matita/contribs/assembly/string/string.ma index 0a81fb6e6..4c4862928 100755 --- a/helm/software/matita/contribs/assembly/string/string.ma +++ b/helm/software/matita/contribs/assembly/string/string.ma @@ -54,3 +54,19 @@ definition strCat_str ≝ (* 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')). -- 2.39.2