--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* *)
+(* Sviluppato da: *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "compiler/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)≫ ]].
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;
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;
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;
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;
[ 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 ???);
(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.
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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* *)
+(* Sviluppato da: *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "compiler/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).
projects / helm.git / commitdiff