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