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 definition aux_env_type ≝ ne_list (list var_elem).
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 ].
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 ].
49 definition empty_env ≝ ne_nil ? (nil var_elem ).
52 definition enter_env ≝ λe:aux_env_type.e&empty_env.
53 definition leave_env ≝ λe:aux_env_type.cut_last_neList ? e.
55 (* recupera descrittore da ambiente *)
56 let rec get_desc_from_lev_env (env:list var_elem ) (str:aux_str_type) on env ≝
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 ]].
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 ≝
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 ].
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 ].
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 ].
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;
81 letin K ≝ (get_desc_env_aux e (None ?) str);
83 [ normalize; autobatch |
84 normalize; autobatch ]
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 ].
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 ].
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 ].
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;
101 letin K ≝ (get_desc_from_lev_env (get_last_neList ? e) str);
103 [ normalize; autobatch |
104 normalize; autobatch ]
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
112 [ ne_nil h ⇒ ne_nil ? (var::h)
113 | ne_cons _ _ ⇒ (cut_last_neList ? e)&«(var::(get_last_neList ? e)) £ »