From: Claudio Sacerdoti Coen Date: Fri, 12 Dec 2008 14:32:23 +0000 (+0000) Subject: 1. new expressions AND, OR, XOR X-Git-Tag: make_still_working~4409 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=be527f5bd4acaf530d8843b23e6849fd5211e1fc;p=helm.git 1. new expressions AND, OR, XOR 2. constants must be initialized 3. bug fixed: the size n of an array means that the array has (n+1) elements. Thus the last valid index is n. --- diff --git a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma index c6d859c4e..5d7a6a622 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma @@ -87,6 +87,12 @@ qed. ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t) | AST_EXPR_SHL: ∀t:ast_base_type. ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_AND: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_OR: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_XOR: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) | AST_EXPR_GT : ∀t:ast_base_type. ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) @@ -148,6 +154,15 @@ let rec ast_to_astfe_expr d (e:aux_env_type d) t (ast:ast_expr d e t) | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒ ASTFE_EXPR_SHL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv) (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv) + | AST_EXPR_AND bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_AND fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv) + (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv) + | AST_EXPR_OR bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_OR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv) + (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv) + | AST_EXPR_XOR bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_XOR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv) + (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv) | AST_EXPR_GT bType sExpr1 sExpr2 ⇒ ASTFE_EXPR_GT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv) @@ -260,6 +275,15 @@ let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t) | ASTFE_EXPR_SHL bType sExpr1 sExpr2 ⇒ ASTFE_EXPR_SHL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe) + | ASTFE_EXPR_AND bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_AND fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) + | ASTFE_EXPR_OR bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_OR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) + | ASTFE_EXPR_XOR bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_XOR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒ ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) @@ -579,8 +603,10 @@ let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux (* AST_NO_DECL: ∀d.∀e:aux_env_type d. list (ast_stm d e) → ast_decl d e -| AST_DECL: ∀d.∀e:aux_env_type d.∀c:bool.∀str:aux_str_type.∀t:ast_type. - (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str c t) → ast_decl d e +| AST_CONST_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type. + (check_not_already_def_env d e str) → ast_init d e t → ast_decl d (add_desc_env d e str true t) → ast_decl d e +| AST_VAR_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type. + (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str false t) → ast_decl d e *) and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe. env_to_flatEnv_inv d e m fe → @@ -613,40 +639,73 @@ and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_m (env_map_flatEnv_addNil_aux sD sE resMap resFe resDimInv) resDimLe resLStm ] - | AST_DECL sD sE sB sName sType sDim sOptInit sDecl ⇒ + | AST_CONST_DECL sD sE sName sType sDim sInit sDecl ⇒ + λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. + match ast_to_astfe_decl sD (add_desc_env sD sE sName true sType) sDecl + (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe))) + (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv) with + [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ + AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe + ([ tripleT ??? sName true sType ]@resTrsf) + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv) + (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe) + ([ ASTFE_STM_INIT resFe true sType + (* l'id e' sull'ambiente arricchito *) + (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe))) + true sType + (ast_to_astfe_id sD (add_desc_env sD sE sName true sType) + true sType + (newid_from_init sD sE sName true sType) + (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe))) + (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv)) + sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE) + resMap resFe + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv) + resDimLe) + (* l'init e' sull'ambiente non arricchito *) + (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType sInit m fe dimInv) + sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE) + resMap resFe + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv) + (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe)) + ]@resLStm) ] + + | AST_VAR_DECL sD sE sName sType sDim sOptInit sDecl ⇒ λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. - match ast_to_astfe_decl sD (add_desc_env sD sE sName sB sType) sDecl - (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe))) - (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe))) - (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv) with + match ast_to_astfe_decl sD (add_desc_env sD sE sName false sType) sDecl + (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe))) + (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv) with [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe - ([ tripleT ??? sName sB sType ]@resTrsf) - (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv) - (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe) + ([ tripleT ??? sName false sType ]@resTrsf) + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv) + (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe) (match sOptInit with [ None ⇒ [] | Some init ⇒ - [ ASTFE_STM_INIT resFe sB sType + [ ASTFE_STM_INIT resFe false sType (* l'id e' sull'ambiente arricchito *) - (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe))) - sB sType - (ast_to_astfe_id sD (add_desc_env sD sE sName sB sType) - sB sType - (newid_from_init sD sE sName sB sType) - (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe))) - (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe))) - (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv)) - sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE) + (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe))) + false sType + (ast_to_astfe_id sD (add_desc_env sD sE sName false sType) + false sType + (newid_from_init sD sE sName false sType) + (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe))) + (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv)) + sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE) resMap resFe - (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv) + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv) resDimLe) (* l'init e' sull'ambiente non arricchito *) (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType init m fe dimInv) - sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE) + sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE) resMap resFe - (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv) - (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe)) + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv) + (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe)) ]]@resLStm) ] ]. diff --git a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma index 553991bd7..8ee77aeb1 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma @@ -57,6 +57,12 @@ inductive ast_expr (d:nat) (e:aux_env_type d) : ast_type → Type ≝ ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t) | AST_EXPR_SHL: ∀t:ast_base_type. ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_AND: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_OR: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_XOR: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) | AST_EXPR_GT : ∀t:ast_base_type. ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) @@ -147,8 +153,10 @@ inductive ast_stm : Πd:nat.aux_env_type d → Type ≝ with ast_decl : Πd:nat.aux_env_type d → Type ≝ AST_NO_DECL: ∀d.∀e:aux_env_type d. list (ast_stm d e) → ast_decl d e -| AST_DECL: ∀d.∀e:aux_env_type d.∀c:bool.∀str:aux_str_type.∀t:ast_type. - (* D *) (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str c t) → ast_decl d e. +| AST_CONST_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type. + (* D *) (check_not_already_def_env d e str) → ast_init d e t → ast_decl d (add_desc_env d e str true t) → ast_decl d e +| AST_VAR_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type. + (* D *) (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str false t) → ast_decl d e. (* -------------------------- *) diff --git a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma index 2690b2466..626248685 100755 --- a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma +++ b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma @@ -57,6 +57,12 @@ inductive astfe_expr (e:aux_flatEnv_type) : ast_type → Type ≝ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_SHL: ∀t:ast_base_type. astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_AND: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_OR: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_XOR: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_GT : ∀t:ast_base_type. astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 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 a5db9536b..d12999168 100755 --- a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma +++ b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma @@ -102,6 +102,9 @@ definition preast_to_ast_var_check ≝ 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_AND: preast_expr → preast_expr → preast_expr + PREAST_EXPR_OR: preast_expr → preast_expr → preast_expr + PREAST_EXPR_XOR: 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 @@ -208,6 +211,36 @@ let rec preast_to_ast_expr (preast:preast_expr) (d:nat) (e:aux_env_type d) on pr (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)) (λres2.Some ? ≪?,(AST_EXPR_SHL d e ? res1 res2)≫)) | _ ⇒ None ? ])) + | PREAST_EXPR_AND subExpr1 subExpr2 ⇒ + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). + match (sigmaFst ?? sigmaRes1) with + [ AST_TYPE_BASE bType ⇒ + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_AND d e ? res1 res2)≫)) + | _ ⇒ None ? ])) + | PREAST_EXPR_OR subExpr1 subExpr2 ⇒ + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). + match (sigmaFst ?? sigmaRes1) with + [ AST_TYPE_BASE bType ⇒ + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_OR d e ? res1 res2)≫)) + | _ ⇒ None ? ])) + | PREAST_EXPR_XOR subExpr1 subExpr2 ⇒ + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). + match (sigmaFst ?? sigmaRes1) with + [ AST_TYPE_BASE bType ⇒ + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_XOR d e ? res1 res2)≫)) + | _ ⇒ None ? ])) | PREAST_EXPR_GT subExpr1 subExpr2 ⇒ opt_map ?? (preast_to_ast_expr subExpr1 d e) @@ -338,9 +371,9 @@ and preast_to_ast_var (preast:preast_var) (d:nat) (e:aux_env_type d) on preast : OUT_OF_BOUND sara' fatto a run time *) match (match expr with - [ 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) + [ 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 d e) @@ -528,7 +561,8 @@ let rec preast_to_ast_stm (preast:preast_stm) (d:nat) (e:aux_env_type d) on prea ] (* PREAST_NO_DECL: list preast_stm → preast_decl - PREAST_DECL: bool → aux_str_type → ast_type → option preast_init → preast_decl → preast_decl + PREAST_CONST_DECL: aux_str_type → ast_type → preast_init → preast_decl → preast_decl + PREAST_VAR_DECL: aux_str_type → ast_type → option preast_init → preast_decl → preast_decl *) and preast_to_ast_decl (preast:preast_decl) (d:nat) (e:aux_env_type d) on preast : option (ast_decl d e) ≝ match preast with @@ -538,20 +572,33 @@ and preast_to_ast_decl (preast:preast_decl) (d:nat) (e:aux_env_type d) on preast (λt'.Some ? ([h']@t')))) (Some ? (nil ?)) lPreastStm) (λres.Some ? (AST_NO_DECL d e res)) - | PREAST_DECL constFlag decName decType optInitExpr subPreastDecl ⇒ + | PREAST_CONST_DECL decName decType initExpr subPreastDecl ⇒ + match checkb_not_already_def_env d e decName + return λx.(checkb_not_already_def_env d e decName = x) → option (ast_decl d e) + with + [ true ⇒ λp:(checkb_not_already_def_env d e decName = true). + opt_map ?? (preast_to_ast_decl subPreastDecl d (add_desc_env d e decName true decType)) + (λdecl.opt_map ?? (preast_to_ast_init initExpr d e) + (λsigmaRes:(Σt:ast_type.ast_init d e t).opt_map ?? (preast_to_ast_init_check d e sigmaRes decType) + (λresInit.Some ? (AST_CONST_DECL d e decName decType + (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) resInit decl)))) + | false ⇒ λp:(checkb_not_already_def_env d e decName = false).None ? + ] (refl_eq ? (checkb_not_already_def_env d e decName)) + + | PREAST_VAR_DECL decName decType optInitExpr subPreastDecl ⇒ match checkb_not_already_def_env d e decName return λx.(checkb_not_already_def_env d e decName = x) → option (ast_decl d e) with [ true ⇒ λp:(checkb_not_already_def_env d e decName = true). - opt_map ?? (preast_to_ast_decl subPreastDecl d (add_desc_env d e decName constFlag decType)) + opt_map ?? (preast_to_ast_decl subPreastDecl d (add_desc_env d e decName false decType)) (λdecl.match optInitExpr with - [ None ⇒ Some ? (AST_DECL d e constFlag decName decType - (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (None ?) decl) + [ None ⇒ Some ? (AST_VAR_DECL d e decName decType + (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (None ?) decl) | Some initExpr ⇒ opt_map ?? (preast_to_ast_init initExpr d e) (λsigmaRes:(Σt:ast_type.ast_init d e t).opt_map ?? (preast_to_ast_init_check d e sigmaRes decType) - (λresInit.Some ? (AST_DECL d e constFlag decName decType - (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (Some ? resInit) decl)))]) + (λresInit.Some ? (AST_VAR_DECL d e decName decType + (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (Some ? resInit) decl)))]) | false ⇒ λp:(checkb_not_already_def_env d e decName = false).None ? ] (refl_eq ? (checkb_not_already_def_env d e decName)) ]. diff --git a/helm/software/matita/contribs/assembly/compiler/preast_tree.ma b/helm/software/matita/contribs/assembly/compiler/preast_tree.ma index 9a463d1b6..6ad8c3d62 100755 --- a/helm/software/matita/contribs/assembly/compiler/preast_tree.ma +++ b/helm/software/matita/contribs/assembly/compiler/preast_tree.ma @@ -42,6 +42,9 @@ inductive preast_expr : Type ≝ | 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_AND: preast_expr → preast_expr → preast_expr +| PREAST_EXPR_OR: preast_expr → preast_expr → preast_expr +| PREAST_EXPR_XOR: preast_expr → preast_expr → preast_expr | PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr | PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr @@ -95,7 +98,8 @@ inductive preast_stm : Type ≝ (* dichiarazioni *) with preast_decl : Type ≝ PREAST_NO_DECL: list preast_stm → preast_decl -| PREAST_DECL: bool → aux_str_type → ast_type → option preast_init → preast_decl → preast_decl. +| PREAST_CONST_DECL: aux_str_type → ast_type → preast_init → preast_decl → preast_decl +| PREAST_VAR_DECL: aux_str_type → ast_type → option preast_init → preast_decl → preast_decl. (* -------------------------- *)