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 eqDesc_elem ≝ λd,d'.(eq_bool (get_const_desc d) (get_const_desc d'))⊗(eq_ast_type (get_type_desc d) (get_type_desc d')).
  46
  47 lemma eq_to_eqdescelem : ∀d,d'.d = d' → eqDesc_elem d d' = true.
  48  intros 3;
  49  rewrite < H;
  50  elim d;
  51  simplify;
  52  rewrite > (eq_to_eqbool b b (refl_eq ??));
  53  rewrite > (eq_to_eqasttype a a (refl_eq ??));
  54  reflexivity.
  55 qed.
  56
  57 lemma eqdescelem_to_eq : ∀d,d'.eqDesc_elem d d' = true → d = d'.
  58  intros 2;
  59  elim d 0;
  60  elim d' 0;
  61  intros 4;
  62  simplify;
  63  intro;
  64  rewrite > (eqbool_to_eq b1 b (andb_true_true ?? H));
  65  rewrite > (eqasttype_to_eq a1 a (andb_true_true_r ?? H));
  66  reflexivity.
  67 qed.
  68
  69 definition get_name_var ≝ λv:var_elem.match v with [ VAR_ELEM n _ ⇒ n ].
  70 definition get_desc_var ≝ λv:var_elem.match v with [ VAR_ELEM _ d ⇒ d ].
  71
  72 (* ambiente vuoto *)
  73 definition empty_env ≝ ne_nil ? (nil var_elem ).
  74
  75 (* setter *)
  76 definition enter_env ≝ λe:aux_env_type.empty_env&e.
  77 definition leave_env ≝ λe:aux_env_type.cut_first_neList ? e.
  78
  79 (* recupera descrittore da ambiente: il primo trovato, ma e' anche l'unico *)
  80 let rec get_desc_from_lev_env (env:list var_elem ) (str:aux_str_type) on env ≝
  81 match env with
  82  [ nil ⇒ None ?
  83  | cons h t ⇒ match eqStr_str str (get_name_var h) with
  84   [ true ⇒ Some ? (get_desc_var h)
  85   | false ⇒ get_desc_from_lev_env t str ]].
  86
  87 (* recupera descrittore da ambiente globale: il primo trovato *)
  88 let rec get_desc_env_aux (env:aux_env_type) (str:aux_str_type) on env ≝
  89  match env with
  90   [ ne_nil h ⇒ get_desc_from_lev_env h str
  91   | ne_cons h t ⇒  match get_desc_from_lev_env h str with
  92    [ None ⇒ get_desc_env_aux t str | Some res' ⇒ Some ? res' ]
  93   ].
  94
  95 definition check_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
  96  match get_desc_env_aux e str with [ None ⇒ False | Some _ ⇒ True ].
  97
  98 definition checkb_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
  99  match get_desc_env_aux e str with [ None ⇒ false | Some _ ⇒ true ].
 100
 101 lemma checkbdescenv_to_checkdescenv : ∀e,str.checkb_desc_env e str = true → check_desc_env e str.
 102  unfold checkb_desc_env;
 103  unfold check_desc_env;
 104  intros;
 105  letin K ≝ (get_desc_env_aux e str);
 106  elim K;
 107  [ normalize; autobatch |
 108    normalize; autobatch ]
 109 qed.
 110
 111 definition get_desc_env ≝ λe:aux_env_type.λstr:aux_str_type.
 112  match get_desc_env_aux e str with
 113   [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
 114
 115 definition check_not_already_def_env ≝ λe:aux_env_type.λstr:aux_str_type.
 116  match get_desc_from_lev_env (get_first_neList ? e) str with [ None ⇒ True | Some _ ⇒ False ].
 117
 118 definition checkb_not_already_def_env ≝ λe:aux_env_type.λstr:aux_str_type.
 119  match get_desc_from_lev_env (get_first_neList ? e) str with [ None ⇒ true | Some _ ⇒ false ].
 120
 121 lemma checkbnotalreadydefenv_to_checknotalreadydefenv : ∀e,str.checkb_not_already_def_env e str = true → check_not_already_def_env e str.
 122  unfold checkb_not_already_def_env;
 123  unfold check_not_already_def_env;
 124  intros;
 125  letin K ≝ (get_desc_from_lev_env (get_first_neList ? e) str);
 126  elim K;
 127  [ normalize; autobatch |
 128    normalize; autobatch ]
 129 qed.
 130
 131 (* aggiungi descrittore ad ambiente globale: in testa al primo ambiente *)
 132 definition add_desc_env ≝
 133 λe:aux_env_type.λstr:aux_str_type.λc:bool.λdesc:ast_type.
 134 (*let var ≝ VAR_ELEM str (DESC_ELEM c desc) in*)
 135  match e with
 136   [ ne_nil h ⇒ ne_nil ? ((VAR_ELEM str (DESC_ELEM c desc))::h)
 137   | ne_cons h tl ⇒ «£((VAR_ELEM str (DESC_ELEM c desc))::h)»&tl
 138   ].
 139
 140 (* controllo e <= e' *)
 141 definition eq_env_elem ≝
 142 λe1,e2.match e1 with
 143  [ VAR_ELEM s1 d1 ⇒ match e2 with
 144   [ VAR_ELEM s2 d2 ⇒ (eqStr_str s1 s2)⊗(eqDesc_elem d1 d2) ]].
 145
 146 lemma eq_to_eqenv : ∀e1,e2.e1 = e2 → eq_env_elem e1 e2 = true.
 147  intros 3;
 148  rewrite < H;
 149  elim e1;
 150  simplify;
 151  rewrite > (eq_to_eqstr a a (refl_eq ??));
 152  rewrite > (eq_to_eqdescelem d d (refl_eq ??));
 153  reflexivity.
 154 qed.
 155
 156 lemma eqenv_to_eq : ∀e1,e2.eq_env_elem e1 e2 = true → e1 = e2.
 157  intros 2;
 158  elim e1 0;
 159  elim e2 0;
 160  intros 4;
 161  simplify;
 162  intro;
 163  rewrite > (eqstr_to_eq a1 a (andb_true_true ?? H));
 164  rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
 165  reflexivity.
 166 qed.