1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
18 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
20 (* ********************************************************************** *)
22 include "string/string.ma".
23 include "freescale/word32.ma".
24 include "compiler/ast_type.ma".
26 (* ***************** *)
27 (* GESTIONE AMBIENTE *)
28 (* ***************** *)
30 (* descrittore: const + type *)
31 inductive desc_elem : Type ≝
32 DESC_ELEM: bool → ast_type → desc_elem.
34 (* elemento: name + desc *)
35 inductive var_elem : Type ≝
36 VAR_ELEM: aux_str_type → desc_elem → var_elem.
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).
43 definition defined_envList ≝
44 λd.λl:env_list d.match l with [ env_nil _ ⇒ False | env_cons _ _ _ ⇒ True ].
46 definition cut_first_envList : Πd.env_list d → ? → env_list (pred d) ≝
47 λd.λl:env_list d.λp:defined_envList ? l.
50 return λX.λY:env_list X.defined_envList X Y → env_list (pred X)
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
56 definition get_first_envList ≝
63 lemma defined_envList_S :
64 ∀d.∀l:env_list (S d).defined_envList (S d) l.
68 | intros; simplify; apply I
72 definition aux_env_type ≝ λd.env_list d.
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 ].
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')).
80 lemma eq_to_eqdescelem : ∀d,d'.d = d' → eqDesc_elem d d' = true.
85 rewrite > (eq_to_eqbool b b (refl_eq ??));
86 rewrite > (eq_to_eqasttype a a (refl_eq ??));
90 lemma eqdescelem_to_eq : ∀d,d'.eqDesc_elem d d' = true → d = d'.
97 rewrite > (eqbool_to_eq b1 b (andb_true_true ?? H));
98 rewrite > (eqasttype_to_eq a1 a (andb_true_true_r ?? H));
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 ].
106 definition empty_env ≝ env_nil [].
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 ??).
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 ≝
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 ]].
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 ≝
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' ]
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 ].
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 ].
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;
138 letin K ≝ (get_desc_env_aux d e str);
140 [ normalize; autobatch |
141 normalize; autobatch ]
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 ].
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 ].
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 ].
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;
158 letin K ≝ (get_desc_from_lev_env (get_first_envList d e) str);
160 [ normalize; autobatch |
161 normalize; autobatch ]
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*)
169 return λX.λe:aux_env_type X.aux_env_type X
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
175 (* controllo e <= e' *)
176 definition eq_env_elem ≝
178 [ VAR_ELEM s1 d1 ⇒ match e2 with
179 [ VAR_ELEM s2 d2 ⇒ (eqStr_str s1 s2)⊗(eqDesc_elem d1 d2) ]].
181 lemma eq_to_eqenv : ∀e1,e2.e1 = e2 → eq_env_elem e1 e2 = true.
186 rewrite > (eq_to_eqstr a a (refl_eq ??));
187 rewrite > (eq_to_eqdescelem d d (refl_eq ??));
191 lemma eqenv_to_eq : ∀e1,e2.eq_env_elem e1 e2 = true → e1 = e2.
198 rewrite > (eqstr_to_eq a1 a (andb_true_true ?? H));
199 rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));