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 eqex_switch : ∀e1,e2.eq_ex e1 e2 = eq_ex e2 e1.
59 lemma eqb8_switch : ∀b1,b2.eq_b8 b1 b2 = eq_b8 b2 b1.
64 rewrite > eqex_switch in ⊢ (? ? % ?);
65 rewrite > eqex_switch in ⊢ (? ? (? ? %) ?);
69 lemma eqasciimin_switch : ∀a1,a2.eqAsciiMin a1 a2 = eqAsciiMin a2 a1.
72 rewrite > eqb8_switch in ⊢ (? ? % ?);
76 lemma eq_to_eqstr : ∀s,s'.s = s' → eqStr_str s s' = true.
83 rewrite > (eq_to_eqasciimin a a (refl_eq ??));
89 lemma eqstr_to_eq : ∀s,s'.eqStr_str s s' = true → s = s'.
104 lapply (andb_true_true ?? H2);
105 lapply (andb_true_true_r ?? H2);
106 rewrite > (H ? Hletin1);
107 rewrite > (eqasciimin_to_eq ?? Hletin);
114 definition strCat_str ≝
115 λstr,str':aux_str_type.str@str'.
118 definition strLen_str ≝ λstr:aux_str_type.len_list ? str.
125 inductive aux_strId_type : Type ≝
126 STR_ID: aux_str_type → nat → aux_strId_type.
129 definition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
130 definition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ].
133 definition eqStrId_str ≝
134 λsid,sid':aux_strId_type.(eqStr_str (get_name_strId sid) (get_name_strId sid'))⊗(eqb (get_id_strId sid) (get_id_strId sid')).
136 lemma eq_to_eqstrid : ∀s,s'.s = s' → eqStrId_str s s' = true.
141 rewrite > (eq_to_eqstr a a (refl_eq ??));
142 rewrite > (eq_to_eqb_true n n (refl_eq ??));
146 lemma eqstrid_to_eq : ∀s,s'.eqStrId_str s s' = true → s = s'.
153 rewrite > (eqstr_to_eq a1 a (andb_true_true ?? H));
154 rewrite > (eqb_true_to_eq n1 n (andb_true_true_r ?? H));