matita/matita/contribs/ng_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 (*                          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).