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 inductive env_list : nat → Type ≝
  40   env_nil: list var_elem → env_list O
  41 | env_cons: ∀n.list var_elem → env_list n → env_list (S n).
  42
  43 definition defined_envList ≝
  44 λd.λl:env_list d.match l with [ env_nil _ ⇒ False | env_cons _ _ _ ⇒ True ].
  45
  46 definition cut_first_envList : Πd.env_list d → ? → env_list (pred d) ≝
  47 λd.λl:env_list d.λp:defined_envList ? l.
  48  let value ≝
  49   match l
  50    return λX.λY:env_list X.defined_envList X Y → env_list (pred X)
  51   with
  52    [ env_nil h ⇒ λp:defined_envList O (env_nil h).False_rect ? p
  53    | env_cons n h t ⇒ λp:defined_envList (S n) (env_cons n h t).t
  54    ] p in value.
  55
  56 definition get_first_envList ≝
  57 λd.λl:env_list d.
  58  match l with
  59   [ env_nil h ⇒ h
  60   | env_cons _ h _ ⇒ h
  61   ].
  62
  63 lemma defined_envList_S :
  64 ∀d.∀l:env_list (S d).defined_envList (S d) l.
  65  intros;
  66  inversion l;
  67   [ intros; destruct H
  68   | intros; simplify; apply I
  69   ]
  70 qed.
  71
  72 definition aux_env_type ≝ λd.env_list d.
  73
  74 (* getter *)
  75 definition get_const_desc ≝ λd:desc_elem.match d with [ DESC_ELEM c _ ⇒ c ].
  76 definition get_type_desc ≝ λd:desc_elem.match d with [ DESC_ELEM _ t ⇒ t ].
  77
  78 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')).
  79
  80 lemma eq_to_eqdescelem : ∀d,d'.d = d' → eqDesc_elem d d' = true.
  81  intros 3;
  82  rewrite < H;
  83  elim d;
  84  simplify;
  85  rewrite > (eq_to_eqbool b b (refl_eq ??));
  86  rewrite > (eq_to_eqasttype a a (refl_eq ??));
  87  reflexivity.
  88 qed.
  89
  90 lemma eqdescelem_to_eq : ∀d,d'.eqDesc_elem d d' = true → d = d'.
  91  intros 2;
  92  elim d 0;
  93  elim d' 0;
  94  intros 4;
  95  simplify;
  96  intro;
  97  rewrite > (eqbool_to_eq b1 b (andb_true_true ?? H));
  98  rewrite > (eqasttype_to_eq a1 a (andb_true_true_r ?? H));
  99  reflexivity.
 100 qed.
 101
 102 definition get_name_var ≝ λv:var_elem.match v with [ VAR_ELEM n _ ⇒ n ].
 103 definition get_desc_var ≝ λv:var_elem.match v with [ VAR_ELEM _ d ⇒ d ].
 104
 105 (* ambiente vuoto *)
 106 definition empty_env ≝ env_nil [].
 107
 108 (* setter *)
 109 definition enter_env ≝ λd.λe:aux_env_type d.env_cons d [] e.
 110 definition leave_env ≝ λd.λe:aux_env_type (S d).cut_first_envList (S d) e (defined_envList_S ??).
 111
 112 (* recupera descrittore da ambiente: il primo trovato, ma e' anche l'unico *)
 113 let rec get_desc_from_lev_env (env:list var_elem) (str:aux_str_type) on env ≝
 114 match env with
 115  [ nil ⇒ None ?
 116  | cons h t ⇒ match eqStr_str str (get_name_var h) with
 117   [ true ⇒ Some ? (get_desc_var h)
 118   | false ⇒ get_desc_from_lev_env t str ]].
 119
 120 (* recupera descrittore da ambiente globale: il primo trovato *)
 121 let rec get_desc_env_aux d (env:aux_env_type d) (str:aux_str_type) on env ≝
 122  match env with
 123   [ env_nil h ⇒ get_desc_from_lev_env h str
 124   | env_cons n h t ⇒  match get_desc_from_lev_env h str with
 125    [ None ⇒ get_desc_env_aux n t str | Some res' ⇒ Some ? res' ]
 126   ].
 127
 128 definition check_desc_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
 129  match get_desc_env_aux d e str with [ None ⇒ False | Some _ ⇒ True ].
 130
 131 definition checkb_desc_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
 132  match get_desc_env_aux d e str with [ None ⇒ false | Some _ ⇒ true ].
 133
 134 lemma checkbdescenv_to_checkdescenv : ∀d.∀e:aux_env_type d.∀str.checkb_desc_env d e str = true → check_desc_env d e str.
 135  unfold checkb_desc_env;
 136  unfold check_desc_env;
 137  intros;
 138  letin K ≝ (get_desc_env_aux d e str);
 139  elim K;
 140  [ normalize; autobatch |
 141    normalize; autobatch ]
 142 qed.
 143
 144 definition get_desc_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
 145  match get_desc_env_aux d e str with
 146   [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
 147
 148 definition check_not_already_def_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
 149  match get_desc_from_lev_env (get_first_envList d e) str with [ None ⇒ True | Some _ ⇒ False ].
 150
 151 definition checkb_not_already_def_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type.
 152  match get_desc_from_lev_env (get_first_envList d e) str with [ None ⇒ true | Some _ ⇒ false ].
 153
 154 lemma checkbnotalreadydefenv_to_checknotalreadydefenv : ∀d.∀e:aux_env_type d.∀str.checkb_not_already_def_env d e str = true → check_not_already_def_env d e str.
 155  unfold checkb_not_already_def_env;
 156  unfold check_not_already_def_env;
 157  intros;
 158  letin K ≝ (get_desc_from_lev_env (get_first_envList d e) str);
 159  elim K;
 160  [ normalize; autobatch |
 161    normalize; autobatch ]
 162 qed.
 163
 164 (* aggiungi descrittore ad ambiente globale: in testa al primo ambiente *)
 165 definition add_desc_env ≝
 166 λd.λe:aux_env_type d.λstr:aux_str_type.λc:bool.λdesc:ast_type.
 167 (*let var ≝ VAR_ELEM str (DESC_ELEM c desc) in*)
 168  match e
 169   return λX.λe:aux_env_type X.aux_env_type X
 170  with
 171   [ env_nil h ⇒ env_nil ((VAR_ELEM str (DESC_ELEM c desc))::h)
 172   | env_cons n h t ⇒ env_cons n ((VAR_ELEM str (DESC_ELEM c desc))::h) t
 173   ].
 174
 175 (* controllo e <= e' *)
 176 definition eq_env_elem ≝
 177 λe1,e2.match e1 with
 178  [ VAR_ELEM s1 d1 ⇒ match e2 with
 179   [ VAR_ELEM s2 d2 ⇒ (eqStr_str s1 s2)⊗(eqDesc_elem d1 d2) ]].
 180
 181 lemma eq_to_eqenv : ∀e1,e2.e1 = e2 → eq_env_elem e1 e2 = true.
 182  intros 3;
 183  rewrite < H;
 184  elim e1;
 185  simplify;
 186  rewrite > (eq_to_eqstr a a (refl_eq ??));
 187  rewrite > (eq_to_eqdescelem d d (refl_eq ??));
 188  reflexivity.
 189 qed.
 190
 191 lemma eqenv_to_eq : ∀e1,e2.eq_env_elem e1 e2 = true → e1 = e2.
 192  intros 2;
 193  elim e1 0;
 194  elim e2 0;
 195  intros 4;
 196  simplify;
 197  intro;
 198  rewrite > (eqstr_to_eq a1 a (andb_true_true ?? H));
 199  rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
 200  reflexivity.
 201 qed.