From: Claudio Sacerdoti Coen Date: Thu, 6 Nov 2008 17:56:57 +0000 (+0000) Subject: First attempts at the third phase. X-Git-Tag: make_still_working~4586 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=92c1b82f32dd0db6af3cb1f56af23b78144fae9a;p=helm.git First attempts at the third phase. --- diff --git a/helm/software/matita/contribs/assembly/compiler/astfe_to_linearfe.ma b/helm/software/matita/contribs/assembly/compiler/astfe_to_linearfe.ma new file mode 100755 index 000000000..07b38ee2c --- /dev/null +++ b/helm/software/matita/contribs/assembly/compiler/astfe_to_linearfe.ma @@ -0,0 +1,96 @@ +(**************************************************************************) +(* ___ *) +(* ||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/linearfe.ma". + +(* ***************************** *) +(* PASSO 3 : da ASTFE a LINEARFE *) +(* ***************************** *) + +(* + ASTFE_STM_ASG: ∀t:ast_type. + astfe_var e false t → astfe_expr e t → astfe_stm e +| ASTFE_STM_INIT: ∀b:bool.∀t:ast_type. + astfe_id e b t → astfe_init e t → astfe_stm e +| ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e +| ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e +*) +inductive astfe_to_linearfe_stm_record (fe:aux_flatEnv_type) : Type ≝ + ASTFE_TO_LINEARFE_STM_RECORD_SINGLE: linearfe_stm fe → astfe_to_linearfe_stm_record fe +| ASTFE_TO_LINEARFE_STM_RECORD_MULTI: nat → jumpBlock fe → linearfe_prog fe → astfe_to_linearfe_stm_record fe. + +let rec astfe_to_linearfe_stm fe (ast:astfe_stm fe) (nextL:nat) on ast + : astfe_to_linearfe_stm_record fe ≝ + match ast with + [ ASTFE_STM_ASG sType sVar sExpr ⇒ + ASTFE_TO_LINEARFE_STM_RECORD_SINGLE fe (LINEARFE_STM_ASG fe sType sVar sExpr) + + | ASTFE_STM_INIT sB sType sId sInit ⇒ + ASTFE_TO_LINEARFE_STM_RECORD_SINGLE fe (LINEARFE_STM_INIT fe sB sType sId sInit) + + | ASTFE_STM_WHILE sExpr sBody ⇒ False_rect ? daemon + + | ASTFE_STM_IF sNelExprBody sOptBody ⇒ False_rect ? daemon + + ] +(* + ASTFE_BODY: list (astfe_stm e) → astfe_body e +*) +and astfe_to_linearfe_body fe (ast:list (astfe_stm fe)) (res:list (linearfe_stm fe)) + (beginL:jumpLabel) (endJump:jumpBlock fe) (nextL:nat) on ast + : Prod nat (linearfe_prog fe) ≝ + match ast with + [ nil ⇒ + pair ?? nextL [ LINEARFE_ELEM fe beginL res endJump ] + | cons h t ⇒ + + ]. + + + + let rec aux (pLStm:list (astfe_stm fe)) (pRes:list (linearfe_stm fe)) + on pLStm : Prod nat (linearfe_prog fe) ≝ + match pLStm with + [ nil ⇒ + pair ?? nextL [ LINEARFE_ELEM fe beginL pRes endJump ] + + | cons h t ⇒ + match astfe_to_linearfe_stm fe h nextL with + [ ASTFE_TO_LINEARFE_STM_RECORD_SINGLE resStm ⇒ aux t (pRes@[ resStm ]) + + | ASTFE_TO_LINEARFE_STM_RECORD_MULTI resNextL resJumpBlock resProg ⇒ + match astfe_to_linearfe_body fe (ASTFE_BODY fe (*t*)[]) (*N_LABEL nextL*)beginL endJump (*resNextL*)1 with + [ pair resNextL' resProg' ⇒ + (*pair ?? resNextL' ([ LINEARFE_ELEM fe beginL pRes resJumpBlock ]@resProg)*)False_rect ? daemon + ] + + ] in aux ast [] + + + + +(* + AST_ROOT: ast_decl O empty_env → ast_root +*) +definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝ +λast:ast_root.match ast with + [ AST_ROOT decl ⇒ match ast_to_astfe_decl O empty_env decl empty_map empty_flatEnv env_map_flatEnv_empty_aux with + [ AST_TO_ASTFE_DECL_RECORD _ resFe _ _ _ resLStm ⇒ ≪resFe,ASTFE_ROOT resFe (ASTFE_BODY resFe resLStm)≫ ]]. diff --git a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma index 156d9a8bd..1339f4f9d 100755 --- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma +++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma @@ -125,7 +125,9 @@ definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ]. -lemma checkbidmap_to_checkidmap : ∀d.∀map:aux_map_type d.∀name.checkb_id_map d map name = true → check_id_map d map name. +lemma checkbidmap_to_checkidmap : + ∀d.∀map:aux_map_type d.∀name. + checkb_id_map d map name = true → check_id_map d map name. unfold checkb_id_map; unfold check_id_map; intros 3; @@ -141,7 +143,9 @@ definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. definition checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ]. -lemma checknotbidmap_to_checknotidmap : ∀d.∀map:aux_map_type d.∀name.checknotb_id_map d map name = true → checknot_id_map d map name. +lemma checknotbidmap_to_checknotidmap : + ∀d.∀map:aux_map_type d.∀name. + checknotb_id_map d map name = true → checknot_id_map d map name. unfold checknotb_id_map; unfold checknot_id_map; intros 3; @@ -171,7 +175,8 @@ definition check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. definition checkb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. match get_desc_flatEnv_aux fe str with [ None ⇒ false | Some _ ⇒ true ]. -lemma checkbdescflatenv_to_checkdescflatenv : ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str. +lemma checkbdescflatenv_to_checkdescflatenv : + ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str. unfold checkb_desc_flatEnv; unfold check_desc_flatEnv; intros 2; @@ -187,7 +192,8 @@ definition checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. definition checknotb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. match get_desc_flatEnv_aux fe str with [ None ⇒ true | Some _ ⇒ false ]. -lemma checknotbdescflatenv_to_checknotdescflatenv : ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str. +lemma checknotbdescflatenv_to_checknotdescflatenv : + ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str. unfold checknotb_desc_flatEnv; unfold checknot_desc_flatEnv; intros 2; @@ -535,7 +541,7 @@ lemma env_map_flatEnv_enter_aux : [ split; [ rewrite < (checkenvmapalign_to_enter ???); apply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1)))))) - | (* TO DO !!! *) elim daemon; + | (* TO DO !!! *) elim daemon ] | unfold check_id_map; rewrite > (getidmap_to_enter ???); @@ -596,14 +602,15 @@ let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_ty (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))) ]. -(* TO DO !!! *) -axiom env_map_flatEnv_add_aux : +lemma env_map_flatEnv_add_aux : ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf. env_to_flatEnv_inv d e map fe → env_to_flatEnv_inv d (build_trasfEnv_env d trsf e) (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))). + (* TO DO !!! *) elim daemon. +qed. lemma env_map_flatEnv_addNil_aux : ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe. @@ -736,11 +743,12 @@ lemma leave_add_enter_env : reflexivity. qed. -(* TO DO !!! *) -axiom env_map_flatEnv_leave_aux : +lemma env_map_flatEnv_leave_aux : ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf. env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe → env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe. + (* TO DO !!! *) elim daemon. +qed. lemma newid_from_init : ∀d.∀e:aux_env_type d.∀name,const,desc. diff --git a/helm/software/matita/contribs/assembly/compiler/linearfe.ma b/helm/software/matita/contribs/assembly/compiler/linearfe.ma new file mode 100755 index 000000000..1f264398b --- /dev/null +++ b/helm/software/matita/contribs/assembly/compiler/linearfe.ma @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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/env_to_flatenv.ma". +include "compiler/astfe_tree.ma". + +(* ************************************************ *) +(* SUCCESSIONE APPIATITA DI ASSEGNAMENTI SU FLATENV *) +(* ************************************************ *) + +inductive jumpLabel : Type ≝ + BEGIN_LABEL: jumpLabel +| N_LABEL: nat → jumpLabel +| END_LABEL: jumpLabel. + +(* + L1 := goto L1 + EXPR L1 L2 := if(EXPR) then { goto L1; } else { goto L2; } +*) +inductive jumpBlock (e:aux_flatEnv_type) : Type ≝ + JUMPBLOCK_ABS: jumpLabel → jumpBlock e +| JUMPBLOCK_COND: astfe_base_expr e → jumpLabel → jumpLabel → jumpBlock e. + +inductive linearfe_stm (e:aux_flatEnv_type) : Type ≝ + LINEARFE_STM_ASG: ∀t:ast_type. + astfe_var e false t → astfe_expr e t → linearfe_stm e +| LINEARFE_STM_INIT: ∀b:bool.∀t:ast_type. + astfe_id e b t → astfe_init e t → linearfe_stm e. + +(* LABEL + [ init/assegnamenti ] + if(EXPR) then { goto LABEL; } else { goto LABEL; } *) +inductive linearfe_elem (e:aux_flatEnv_type) : Type ≝ + LINEARFE_ELEM: jumpLabel → list (linearfe_stm e) → jumpBlock e → linearfe_elem e. + +(* -------------------------- *) + +definition linearfe_prog ≝ λe.list (linearfe_elem e). + +(* -------------------------- *) + +(* programma vuoto *) +definition empty_linearfe_prog ≝ nil (linearfe_elem empty_flatEnv).