freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / compiler / environment.ma

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
new file mode 100755 (executable)
index 0000000..73a2c8a
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
@@ -0,0 +1,72 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                                                                        *)
+(* Sviluppato da:                                                         *)
+(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "common/string.ma".
+include "compiler/ast_type.ma".
+
+(* ***************** *)
+(* GESTIONE AMBIENTE *)
+(* ***************** *)
+
+(* elemento: name + const + type *)
+nrecord envDsc : Type ≝
+ {
+ nameDsc: aux_str_type;
+ constDsc: bool;
+ typeDsc: ast_type
+ }.
+
+(* ambiente globale: (ambiente base + ambienti annidati) *)
+ninductive env_list : nat → Type ≝
+  env_nil: list envDsc → env_list O
+| env_cons: ∀n.list envDsc → env_list n → env_list (S n).
+
+(* sto cercando di emulare "inversion e" *)
+nlemma inv_envList :
+ ∀n.∀e:env_list n.∀P:Prop.
+ (n = (match e with [ env_nil _ ⇒ O | env_cons n' _ _ ⇒ S n' ]) → P) → P.
+ #n; #e;
+ ncases e;
+ nnormalize;
+ ##[ ##1: #x; #P; #H;
+ ##| ##2: #x; #y; #z; #P; #H;
+ ##]
+ napply (H (refl_eq …)).
+nqed.
+
+ndefinition defined_envList ≝
+λd.λl:env_list d.match l with [ env_nil _ ⇒ False | env_cons _ _ _ ⇒ True ].
+
+(* bisogna dimostrare "defined_envList (S ...)"
+   impossibile anche cercando di usare l'emulazione di inversion
+*)
+ndefinition cut_first_envList_aux : Πd.env_list (S d) → env_list d ≝
+λd.λl:env_list (S d).
+  match l
+   return λX.λY:env_list X.defined_envList X Y → env_list (pred X)
+  with
+   [ env_nil h ⇒ λp:defined_envList O (env_nil h).False_rect_Type0 ? p
+   | env_cons n h t ⇒ λp:defined_envList (S n) (env_cons n h t).t
+   ] ?.
+ napply (inv_envList ? l …);
+ (* se apro l, a ritroso modifica il suo parametro destro d e non dimostro piu' nulla *)
+ (* io pensavo di ottenere per env_nil l'assurdo S d = O ... *)
+ ncases l;