1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
18 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
20 (* ********************************************************************** *)
22 include "string/ascii_min.ma".
23 include "compiler/utility.ma".
25 (* ************************ *)
26 (* MANIPOLAZIONE DI STRINGA *)
27 (* ************************ *)
30 definition aux_str_type ≝ list ascii_min.
33 definition empty_str ≝ nil ascii_min.
36 definition isNull_str ≝
37 λstr:aux_str_type.match str with
38 [ nil ⇒ true | cons _ _ ⇒ false ].
41 let rec eqStr_str (str,str':aux_str_type) ≝
43 [ nil ⇒ match str' with
46 | cons h t ⇒ match str' with
48 | cons h' t' ⇒ (eqAsciiMin h h')⊗(eqStr_str t t')
52 lemma eq_to_eqstr : ∀s,s'.s = s' → eqStr_str s s' = true.
59 rewrite > (eq_to_eqasciimin a a (refl_eq ??));
65 lemma eqstr_to_eq : ∀s,s'.eqStr_str s s' = true → s = s'.
80 lapply (andb_true_true ?? H2);
81 lapply (andb_true_true_r ?? H2);
82 rewrite > (H ? Hletin1);
83 rewrite > (eqasciimin_to_eq ?? Hletin);
90 definition strCat_str ≝
91 λstr,str':aux_str_type.str@str'.
94 definition strLen_str ≝ λstr:aux_str_type.len_list ? str.
101 inductive aux_strId_type : Type ≝
102 STR_ID: aux_str_type → nat → aux_strId_type.
105 definition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
106 definition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ].
109 definition eqStrId_str ≝
110 λsid,sid':aux_strId_type.(eqStr_str (get_name_strId sid) (get_name_strId sid'))⊗(eqb (get_id_strId sid) (get_id_strId sid')).
112 lemma eq_to_eqstrid : ∀s,s'.s = s' → eqStrId_str s s' = true.
117 rewrite > (eq_to_eqstr a a (refl_eq ??));
118 rewrite > (eq_to_eqb_true n n (refl_eq ??));
122 lemma eqstrid_to_eq : ∀s,s'.eqStrId_str s s' = true → s = s'.
129 rewrite > (eqstr_to_eq a1 a (andb_true_true ?? H));
130 rewrite > (eqb_true_to_eq n1 n (andb_true_true_r ?? H));