(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
-include "utility/utility.ma".
-include "freescale/nat_lemmas.ma".
+include "common/list_utility.ma".
(* ************************* *)
(* dimensioni degli elementi *)
]
].
-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
]
].
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_STRUCT nel_ast ⇒ fold_right_neList ?? (λt,x.(eval_size_type t)+x) O nel_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
].