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