(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
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
].