X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcompiler%2Fast_type.ma;h=2d4eafdfb8df24570f7501709e318aa9e25bae7c;hb=34cdd4af2d7bdac3bab74a54123fbfcb02fa0403;hp=7f33aada2c27a7e67f6a31ce405c44f778e21be6;hpb=38fccc2b774e493a94eedef76342b56079c0e694;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 7f33aada2..2d4eafdfb 100755
--- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -88,26 +88,23 @@ nlet rec ast_type_rectex (P:ast_type → Type)
    ]
   ]. 
 
-ndefinition eq_ast_base_type ≝
+ndefinition eq_astbasetype ≝
 λt1,t2:ast_base_type.match t1 with
- [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with
-  [ AST_BASE_TYPE_BYTE8 ⇒ true | _ ⇒ false ]
- | AST_BASE_TYPE_WORD16 ⇒ match t2 with
-  [ AST_BASE_TYPE_WORD16 ⇒ true | _ ⇒ false ]
- | AST_BASE_TYPE_WORD32 ⇒ match t2 with
-  [ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ]
+ [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with [ AST_BASE_TYPE_BYTE8 ⇒ true | _ ⇒ false ]
+ | AST_BASE_TYPE_WORD16 ⇒ match t2 with [ AST_BASE_TYPE_WORD16 ⇒ true | _ ⇒ false ]
+ | AST_BASE_TYPE_WORD32 ⇒ match t2 with [ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ]
  ].
 
-nlet rec eq_ast_type (t1,t2:ast_type) on t1 ≝
+nlet rec eq_asttype (t1,t2:ast_type) on t1 ≝
  match t1 with
   [ AST_TYPE_BASE bType1 ⇒ match t2 with
-   [ AST_TYPE_BASE bType2 ⇒ eq_ast_base_type bType1 bType2
+   [ AST_TYPE_BASE bType2 ⇒ eq_astbasetype bType1 bType2
    | _ ⇒ false ]
   | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
-   [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eq_nat dim1 dim2)
+   [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_asttype subType1 subType2) ⊗ (eq_nat dim1 dim2)
    | _ ⇒ false ]
   | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
-   [ AST_TYPE_STRUCT nelSubType2 ⇒ bfold_right_neList2 ? (λx1,x2.eq_ast_type x1 x2) nelSubType1 nelSubType2
+   [ AST_TYPE_STRUCT nelSubType2 ⇒ bfold_right_neList2 ? (λx1,x2.eq_asttype x1 x2) nelSubType1 nelSubType2
    | _ ⇒ false
    ]
   ].
@@ -126,14 +123,14 @@ ndefinition isntb_ast_base_type ≝
 
 ndefinition eval_size_base_type ≝
 λast:ast_base_type.match ast with
- [ AST_BASE_TYPE_BYTE8 ⇒ 1
- | AST_BASE_TYPE_WORD16 ⇒ 2
- | AST_BASE_TYPE_WORD32 ⇒ 4
+ [ AST_BASE_TYPE_BYTE8 ⇒ nat1
+ | AST_BASE_TYPE_WORD16 ⇒ nat2
+ | AST_BASE_TYPE_WORD32 ⇒ nat4
  ].
 
 nlet rec eval_size_type (ast:ast_type) on ast ≝
  match ast with
   [ AST_TYPE_BASE b ⇒ eval_size_base_type b
-  | AST_TYPE_ARRAY sub_ast dim ⇒ (dim+1)*(eval_size_type sub_ast)
+  | AST_TYPE_ARRAY sub_ast dim ⇒ (dim + nat1)*(eval_size_type sub_ast)
   | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList … (λt,x.(eval_size_type t)+x) O nel_ast
   ].