X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcompiler%2Fast_type.ma;h=1fa93ce72fc55c6f173c03d369da4610603dfcc4;hb=dc74ed7c4af1aa9b90fc5d2f0a86bd7825696e71;hp=d972fe0bae891b3de5e6a7949eb0dd42c37aca28;hpb=7b60729bcdcdd820ae78e32a68b59e56e11f1c02;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
index d972fe0ba..1fa93ce72 100755
--- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
@@ -33,107 +33,62 @@ ninductive ast_base_type : Type ≝
 | AST_BASE_TYPE_WORD16: ast_base_type
 | AST_BASE_TYPE_WORD32: ast_base_type.
 
-(*ndefinition ast_base_type_ind
- : ΠP:ast_base_type → Prop.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 →
-   Πa:ast_base_type.P a ≝
-λP:ast_base_type → Prop.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
-λa:ast_base_type.
- match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ].
-
-ndefinition ast_base_type_rec
- : ΠP:ast_base_type → Set.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 →
-   Πa:ast_base_type.P a ≝
-λP:ast_base_type → Set.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
-λa:ast_base_type.
- match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ].
-
-ndefinition ast_base_type_rect
- : ΠP:ast_base_type → Type.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 →
-   Πa:ast_base_type.P a ≝
-λP:ast_base_type → Type.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
-λa:ast_base_type.
- match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ].
-*)
 ninductive ast_type : Type ≝
   AST_TYPE_BASE: ast_base_type → ast_type
 | AST_TYPE_ARRAY: ast_type → nat → ast_type
 | AST_TYPE_STRUCT: ne_list ast_type → ast_type.
 
-nlet rec ast_type_ind_aux (P:ast_type → Prop)
-                          (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
-                          (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
-                          (f2:Πt.P t)
-                          (t:ne_list ast_type) on t ≝
+(* principio di eliminazione arricchito *)
+nlet rec ast_type_index_aux (P:ast_type → Prop)
+                            (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
+                            (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
+                            (f2:Πt.P t)
+                            (t:ne_list ast_type) on t ≝
  match t return λt.P (AST_TYPE_STRUCT t) with
   [ ne_nil h ⇒ f h (f2 h)
-  | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_ind_aux P f f1 f2 t)
+  | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_index_aux P f f1 f2 t)
   ].
 
-(*nlet rec ast_type_ind (P:ast_type → Prop)
-                      (f:Πb.P (AST_TYPE_BASE b))
-                      (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
-                      (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
-                      (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
-                      (t:ast_type) on t : P t ≝
+nlet rec ast_type_index (P:ast_type → Prop)
+                        (f:Πb.P (AST_TYPE_BASE b))
+                        (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
+                        (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
+                        (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
+                        (t:ast_type) on t : P t ≝
  match t return λt.P t with
   [ AST_TYPE_BASE b ⇒ f b
-  | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_ind P f f1 f2 f3 t')
+  | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_index P f f1 f2 f3 t')
   | AST_TYPE_STRUCT nl ⇒ match nl with
-   [ ne_nil h ⇒ f2 h (ast_type_ind P f f1 f2 f3 h)
-   | ne_cons h t ⇒ f3 h t (ast_type_ind P f f1 f2 f3 h) (ast_type_ind_aux P f2 f3 (ast_type_ind P f f1 f2 f3) t)
+   [ ne_nil h ⇒ f2 h (ast_type_index P f f1 f2 f3 h)
+   | ne_cons h t ⇒ f3 h t (ast_type_index P f f1 f2 f3 h) (ast_type_index_aux P f2 f3 (ast_type_index P f f1 f2 f3) t)
    ]
   ]. 
 
-nlet rec ast_type_rec_aux (P:ast_type → Type[0])
-                          (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
-                          (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
-                          (f2:Πt.P t)
-                          (t:ne_list ast_type) on t ≝
+nlet rec ast_type_rectex_aux (P:ast_type → Type)
+                             (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
+                             (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
+                             (f2:Πt.P t)
+                             (t:ne_list ast_type) on t ≝
  match t return λt.P (AST_TYPE_STRUCT t) with
   [ ne_nil h ⇒ f h (f2 h)
-  | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rec_aux P f f1 f2 t)
+  | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rectex_aux P f f1 f2 t)
   ].
 
-nlet rec ast_type_rec (P:ast_type → Set)
-                      (f:Πb.P (AST_TYPE_BASE b))
-                      (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
-                      (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
-                      (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
-                      (t:ast_type) on t : P t ≝
+nlet rec ast_type_rectex (P:ast_type → Type)
+                         (f:Πb.P (AST_TYPE_BASE b))
+                         (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
+                         (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
+                         (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
+                         (t:ast_type) on t : P t ≝
  match t return λt.P t with
   [ AST_TYPE_BASE b ⇒ f b
-  | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rec P f f1 f2 f3 t')
+  | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rectex P f f1 f2 f3 t')
   | AST_TYPE_STRUCT nl ⇒ match nl with
-   [ ne_nil h ⇒ f2 h (ast_type_rec P f f1 f2 f3 h)
-   | ne_cons h t ⇒ f3 h t (ast_type_rec P f f1 f2 f3 h) (ast_type_rec_aux P f2 f3 (ast_type_rec P f f1 f2 f3) t)
+   [ ne_nil h ⇒ f2 h (ast_type_rectex P f f1 f2 f3 h)
+   | ne_cons h t ⇒ f3 h t (ast_type_rectex P f f1 f2 f3 h) (ast_type_rectex_aux P f2 f3 (ast_type_rectex P f f1 f2 f3) t)
    ]
   ]. 
 
-nlet rec ast_type_rect_aux (P:ast_type → Type)
-                           (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
-                           (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
-                           (f2:Πt.P t)
-                           (t:ne_list ast_type) on t ≝
- match t return λt.P (AST_TYPE_STRUCT t) with
-  [ ne_nil h ⇒ f h (f2 h)
-  | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rect_aux P f f1 f2 t)
-  ].
-
-nlet rec ast_type_rect (P:ast_type → Type)
-                       (f:Πb.P (AST_TYPE_BASE b))
-                       (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
-                       (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
-                       (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
-                       (t:ast_type) on t : P t ≝
- match t return λt.P t with
-  [ AST_TYPE_BASE b ⇒ f b
-  | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rect P f f1 f2 f3 t')
-  | AST_TYPE_STRUCT nl ⇒ match nl with
-   [ ne_nil h ⇒ f2 h (ast_type_rect P f f1 f2 f3 h)
-   | ne_cons h t ⇒ f3 h t (ast_type_rect P f f1 f2 f3 h) (ast_type_rect_aux P f2 f3 (ast_type_rect P f f1 f2 f3) t)
-   ]
-  ]. 
-*)
 ndefinition eq_ast_base_type ≝
 λt1,t2:ast_base_type.match t1 with
  [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with
@@ -153,16 +108,7 @@ nlet rec eq_ast_type (t1,t2:ast_type) on t1 ≝
    [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eq_nat dim1 dim2)
    | _ ⇒ false ]
   | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
-   [ AST_TYPE_STRUCT nelSubType2 ⇒
-    match eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2)
-     return λx.eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = x → bool
-    with
-     [ true ⇒ λp:(eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = true).
-      fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
-                         true nelSubType1 nelSubType2
-                         (eqnat_to_eq (len_neList ? nelSubType1) (len_neList ? nelSubType2) p)
-     | false ⇒ λp:(eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = false).false
-     ] (refl_eq ? (eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2)))
+   [ AST_TYPE_STRUCT nelSubType2 ⇒ bfold_right_neList2 ? (λx1,x2.eq_ast_type x1 x2) nelSubType1 nelSubType2
    | _ ⇒ false
    ]
   ].