First attempts at the third phase.

[helm.git] / helm / software / matita / contribs / assembly / compiler / astfe_to_linearfe.ma

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 (executable)
index 0000000..07b38ee
--- /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)≫ ]].