--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "utility/utility.ma".
+include "freescale/nat_lemmas.ma".
+
+(* ************************* *)
+(* dimensioni degli elementi *)
+(* ************************* *)
+
+(* usato per definire nell'ast *)
+ninductive ast_base_type : Type ≝
+ AST_BASE_TYPE_BYTE8: ast_base_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 ≝
+ 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)
+ ].
+
+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 ≝
+ 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_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)
+ ]
+ ].
+
+nlet rec ast_type_rec_aux (P:ast_type → Set)
+ (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)
+ ].
+
+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 ≝
+ 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_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)
+ ]
+ ].
+
+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
+ [ 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 ≝
+ match t1 with
+ [ AST_TYPE_BASE bType1 ⇒ match t2 with
+ [ AST_TYPE_BASE bType2 ⇒ eq_ast_base_type 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)
+ | _ ⇒ 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)))
+ | _ ⇒ false
+ ]
+ ].
+
+ndefinition is_ast_base_type ≝
+λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].
+
+ndefinition isb_ast_base_type ≝
+λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ true | _ ⇒ false ].
+
+ndefinition isnt_ast_base_type ≝
+λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ].
+
+ndefinition isntb_ast_base_type ≝
+λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ false | _ ⇒ true ].
+
+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
+ ].
+
+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
+ ].
projects / helm.git / blobdiff