helm/software/matita/contribs/assembly/compiler/astfe_to_linearfe.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                                                                        *)
  17 (* Sviluppato da:                                                         *)
  18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  19 (*                                                                        *)
  20 (* ********************************************************************** *)
  21
  22 include "compiler/linearfe.ma".
  23
  24 (* ***************************** *)
  25 (* PASSO 3 : da ASTFE a LINEARFE *)
  26 (* ***************************** *)
  27
  28 (*
  29   ASTFE_STM_ASG: ∀t:ast_type.
  30                  astfe_var e false t → astfe_expr e t → astfe_stm e
  31 | ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
  32                   astfe_id e b t → astfe_init e t → astfe_stm e
  33 | ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
  34 | ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
  35 *)
  36 inductive astfe_to_linearfe_stm_record (fe:aux_flatEnv_type) : Type ≝
  37   ASTFE_TO_LINEARFE_STM_RECORD_SINGLE: linearfe_stm fe → astfe_to_linearfe_stm_record fe
  38 | ASTFE_TO_LINEARFE_STM_RECORD_MULTI: nat → jumpBlock fe → linearfe_prog fe → astfe_to_linearfe_stm_record fe.
  39
  40 let rec astfe_to_linearfe_stm fe (ast:astfe_stm fe) (nextL:nat) on ast
  41  : astfe_to_linearfe_stm_record fe ≝
  42  match ast with
  43   [ ASTFE_STM_ASG sType sVar sExpr ⇒
  44    ASTFE_TO_LINEARFE_STM_RECORD_SINGLE fe (LINEARFE_STM_ASG fe sType sVar sExpr)
  45
  46   | ASTFE_STM_INIT sB sType sId sInit ⇒
  47    ASTFE_TO_LINEARFE_STM_RECORD_SINGLE fe (LINEARFE_STM_INIT fe sB sType sId sInit)
  48
  49   | ASTFE_STM_WHILE sExpr sBody ⇒ False_rect ? daemon
  50
  51   | ASTFE_STM_IF sNelExprBody sOptBody ⇒ False_rect ? daemon
  52
  53   ]
  54 (*
  55   ASTFE_BODY: list (astfe_stm e) → astfe_body e
  56 *)
  57 and astfe_to_linearfe_body fe (ast:list (astfe_stm fe)) (res:list (linearfe_stm fe))
  58                               (beginL:jumpLabel) (endJump:jumpBlock fe) (nextL:nat) on ast
  59                               : Prod nat (linearfe_prog fe) ≝
  60  match ast with
  61   [ nil ⇒
  62    pair ?? nextL [ LINEARFE_ELEM fe beginL res endJump ]
  63   | cons h t ⇒
  64
  65   ].
  66
  67
  68
  69    let rec aux (pLStm:list (astfe_stm fe)) (pRes:list (linearfe_stm fe))
  70                 on pLStm : Prod nat (linearfe_prog fe) ≝
  71     match pLStm with
  72     [ nil ⇒
  73      pair ?? nextL [ LINEARFE_ELEM fe beginL pRes endJump ]
  74
  75     | cons h t ⇒
  76      match astfe_to_linearfe_stm fe h nextL with
  77       [ ASTFE_TO_LINEARFE_STM_RECORD_SINGLE resStm ⇒ aux t (pRes@[ resStm ])
  78
  79       | ASTFE_TO_LINEARFE_STM_RECORD_MULTI resNextL resJumpBlock resProg ⇒
  80        match astfe_to_linearfe_body fe (ASTFE_BODY fe (*t*)[]) (*N_LABEL nextL*)beginL endJump (*resNextL*)1 with
  81         [ pair resNextL' resProg' ⇒
  82          (*pair ?? resNextL' ([ LINEARFE_ELEM fe beginL pRes resJumpBlock ]@resProg)*)False_rect ? daemon
  83         ]
  84
  85       ] in aux ast []
  86
  87
  88
  89
  90 (*
  91   AST_ROOT: ast_decl O empty_env → ast_root
  92 *)
  93 definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
  94 λast:ast_root.match ast with
  95  [ AST_ROOT decl ⇒ match ast_to_astfe_decl O empty_env decl empty_map empty_flatEnv env_map_flatEnv_empty_aux with
  96   [ AST_TO_ASTFE_DECL_RECORD _ resFe _ _ _ resLStm ⇒ ≪resFe,ASTFE_ROOT resFe (ASTFE_BODY resFe resLStm)≫ ]].