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 "common/string.ma".
23 include "compiler/ast_type.ma".
25 (* ***************** *)
26 (* GESTIONE AMBIENTE *)
27 (* ***************** *)
29 (* elemento: name + const + type *)
30 nrecord envDsc : Type ≝
32 nameDsc: aux_str_type;
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).
42 ndefinition defined_envList ≝
43 λd.λl:env_list d.match l with [ env_nil _ ⇒ False | env_cons _ _ _ ⇒ True ].
45 (* bisogna bypassare la carenza di inversion *)
46 nlemma defined_envList_S : ∀d.∀l:env_list (S d).defined_envList (S d) l.
48 ngeneralize in match (refl_eq ? (S d));
49 (* S d = S d → ? e' in realta' eq nat (S d) (S d) ... *)
50 ncases l in ⊢ (? ? % ? → %);
51 ##[ ##1: #dsc; #H; nelim (nat_destruct_0_S … H)
52 ##| ##2: #n; #dsc; #sub; #H;
58 ndefinition cut_first_envList_aux : Πd.env_list (S d) → env_list d ≝
61 return λX.λY:env_list X.defined_envList X Y → env_list (pred X)
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).