helm/software/matita/contribs/assembly/compiler/environment.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 "string/string.ma".
  23 include "freescale/word32.ma".
  24 include "compiler/ast_type.ma".
  25
  26 (* ***************** *)
  27 (* GESTIONE AMBIENTE *)
  28 (* ***************** *)
  29
  30 (* descrittore: const + type *)
  31 inductive desc_elem : Type ≝
  32 DESC_ELEM: bool → ast_type → desc_elem.
  33
  34 (* elemento: name + desc *)
  35 inductive var_elem : Type ≝
  36 VAR_ELEM: aux_str_type → desc_elem → var_elem.
  37
  38 (* ambiente globale: (ambiente base + ambienti annidati) *)
  39 definition aux_env_type ≝ ne_list (list var_elem).
  40
  41 (* getter *)
  42 definition get_const_desc ≝ λd:desc_elem.match d with [ DESC_ELEM c _ ⇒ c ].
  43 definition get_type_desc ≝ λd:desc_elem.match d with [ DESC_ELEM _ t ⇒ t ].
  44
  45 definition get_name_var ≝ λv:var_elem.match v with [ VAR_ELEM n _ ⇒ n ].
  46 definition get_desc_var ≝ λv:var_elem.match v with [ VAR_ELEM _ d ⇒ d ].
  47
  48 (* ambiente vuoto *)
  49 definition empty_env ≝ ne_nil ? (nil var_elem ).
  50
  51 (* setter *)
  52 definition enter_env ≝ λe:aux_env_type.e&empty_env.
  53 definition leave_env ≝ λe:aux_env_type.cut_last_neList ? e.
  54
  55 (* recupera descrittore da ambiente *)
  56 let rec get_desc_from_lev_env (env:list var_elem ) (str:aux_str_type) on env ≝
  57 match env with
  58  [ nil ⇒ None ?
  59  | cons h t ⇒ match strCmp_str str (get_name_var h) with
  60   [ true ⇒ Some ? (get_desc_var h)
  61   | false ⇒ get_desc_from_lev_env t str ]].
  62
  63 (* recupera descrittore da ambiente globale *)
  64 let rec get_desc_env_aux (env:aux_env_type) (res:option desc_elem) (str:aux_str_type) on env ≝
  65  match env with
  66   [ ne_nil h ⇒ match get_desc_from_lev_env h str with
  67                [ None ⇒ res | Some res' ⇒ Some ? res' ]
  68   | ne_cons h t ⇒ get_desc_env_aux t (match get_desc_from_lev_env h str with
  69                                       [ None ⇒ res | Some res' ⇒ Some ? res' ]) str ].
  70
  71 definition check_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
  72  match get_desc_env_aux e (None ?) str with [ None ⇒ False | Some _ ⇒ True ].
  73
  74 definition checkb_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
  75  match get_desc_env_aux e (None ?) str with [ None ⇒ false | Some _ ⇒ true ].
  76
  77 lemma checkbdescenv_to_checkdescenv : ∀e,str.checkb_desc_env e str = true → check_desc_env e str.
  78  unfold checkb_desc_env;
  79  unfold check_desc_env;
  80  intros;
  81  letin K ≝ (get_desc_env_aux e (None ?) str);
  82  elim K;
  83  [ normalize; autobatch |
  84    normalize; autobatch ]
  85 qed.
  86
  87 definition get_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
  88  match get_desc_env_aux e (None ?) str with
  89   [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
  90
  91 definition check_not_already_def_env ≝ λe:aux_env_type.λstr:aux_str_type.
  92  match get_desc_from_lev_env (get_last_neList ? e) str with [ None ⇒ True | Some _ ⇒ False ].
  93
  94 definition checkb_not_already_def_env ≝ λe:aux_env_type.λstr:aux_str_type.
  95  match get_desc_from_lev_env (get_last_neList ? e) str with [ None ⇒ true | Some _ ⇒ false ].
  96
  97 lemma checkbnotalreadydefenv_to_checknotalreadydefenv : ∀e,str.checkb_not_already_def_env e str = true → check_not_already_def_env e str.
  98  unfold checkb_not_already_def_env;
  99  unfold check_not_already_def_env;
 100  intros;
 101  letin K ≝ (get_desc_from_lev_env (get_last_neList ? e) str);
 102  elim K;
 103  [ normalize; autobatch |
 104    normalize; autobatch ]
 105 qed.
 106
 107 (* aggiungi descrittore ad ambiente globale *)
 108 definition add_desc_env ≝
 109 λe:aux_env_type.λstr:aux_str_type.λc:bool.λdesc:ast_type.
 110 let var ≝ VAR_ELEM str (DESC_ELEM c desc) in
 111  match e with
 112   [ ne_nil h ⇒ ne_nil ? (var::h)
 113   | ne_cons _ _ ⇒ (cut_last_neList ? e)&«(var::(get_last_neList ? e)) £ »
 114   ].