include "utility/ascii.ma".
include "freescale/theory.ma".
include "freescale/nat.ma".
+include "utility/utility.ma".
(* ************************ *)
(* MANIPOLAZIONE DI STRINGA *)
ndefinition aux_str_type ≝ list ascii.
(* strcmp *)
-nlet rec eq_str (str,str':aux_str_type) ≝
- match str with
- [ nil ⇒ match str' with
- [ nil => true
- | cons _ _ => false ]
- | cons h t ⇒ match str' with
- [ nil ⇒ false
- | cons h' t' ⇒ (eq_ascii h h')⊗(eq_str t t')
- ]
- ].
+ndefinition eq_str ≝
+ bfold_right_list2 ascii (λx,y.eq_ascii x y).
(* ************ *)
(* STRINGA + ID *)
(* ************ *)
(* tipo pubblico *)
-ninductive aux_strId_type : Type ≝
- STR_ID: aux_str_type → nat → aux_strId_type.
-
-(*ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
-λP:aux_strId_type → Prop.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
- match a with [ STR_ID l n ⇒ f l n ].
-
-ndefinition aux_strId_type_rec : ΠP:aux_strId_type → Set.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
-λP:aux_strId_type → Set.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
- match a with [ STR_ID l n ⇒ f l n ].
-
-ndefinition aux_strId_type_rect : ΠP:aux_strId_type → Type.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
-λP:aux_strId_type → Type.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
- match a with [ STR_ID l n ⇒ f l n ].*)
-
-(* getter *)
-ndefinition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
-ndefinition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ].
+nrecord strId : Type ≝
+ {
+ str_elem: aux_str_type;
+ id_elem: nat
+ }.
(* confronto *)
ndefinition eq_strId ≝
-λsid,sid':aux_strId_type.(eq_str (get_name_strId sid) (get_name_strId sid'))⊗(eq_nat (get_id_strId sid) (get_id_strId sid')).
+λsid,sid':strId.
+ (eq_str (str_elem sid) (str_elem sid'))⊗
+ (eq_nat (id_elem sid) (id_elem sid')).