]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/ng_assembly2/compiler/environment.ma
milestone update in ground
[helm.git] / matitaB / matita / contribs / ng_assembly2 / 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 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "common/string.ma".
24 include "compiler/ast_type.ma".
25
26 (* ***************** *)
27 (* GESTIONE AMBIENTE *)
28 (* ***************** *)
29
30 (* elemento: name + const + type *)
31 nrecord envDsc : Type ≝
32  {
33  nameDsc: aux_str_type;
34  constDsc: bool;
35  typeDsc: ast_type
36  }.
37
38 (* ambiente globale: (ambiente base + ambienti annidati) *)
39 ninductive env_list : nat → Type ≝
40   env_nil: list envDsc → env_list O
41 | env_cons: ∀n.list envDsc → env_list n → env_list (S n).
42
43 ndefinition defined_envList ≝
44 λd.λl:env_list d.match l with [ env_nil _ ⇒ False | env_cons _ _ _ ⇒ True ].
45
46 (* bisogna bypassare la carenza di inversion *)
47 nlemma defined_envList_S : ∀d.∀l:env_list (S d).defined_envList (S d) l.
48  #d; #l;
49  ngeneralize in match (refl_eq ? (S d));
50  ncases l in ⊢ (? ? % ? → %);
51  ##[ ##1: #dsc; #H; ndestruct (*nelim (nat_destruct_0_S … H)*)
52  ##| ##2: #n; #dsc; #sub; #H;
53           nnormalize;
54           napply I
55  ##]
56 nqed.
57
58 ndefinition cut_first_envList_aux : Πd.env_list (S d) → env_list d ≝
59 λd.λl:env_list (S d).
60   match l
61    return λX.λY:env_list X.defined_envList X Y → env_list (pred X)
62   with
63    [ env_nil h ⇒ λp:defined_envList O (env_nil h).False_rect_Type0 ? p
64    | env_cons n h t ⇒ λp:defined_envList (S n) (env_cons n h t).t
65    ] (defined_envList_S d l).