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 strCmp_str (str,str':aux_str_type) ≝
43 [ nil ⇒ match str' with
44 [ nil ⇒ true | cons _ _ ⇒ false ]
45 | cons h t ⇒ match str' with
47 | cons h' t' ⇒ match eqAsciiMin h h' with
48 [ true ⇒ strCmp_str t t' | false ⇒ false ]
51 axiom eqbstrcmpstr_to_eq : ∀s,s'.strCmp_str s s' = true → s = s'.
54 definition strCat_str ≝
55 λstr,str':aux_str_type.str@str'.
58 definition strLen_str ≝ λstr:aux_str_type.len_list ? str.
65 inductive aux_strId_type : Type ≝
66 STR_ID: aux_str_type → nat → aux_strId_type.
69 definition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
70 definition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ].
73 definition strCmp_strId ≝
74 λsid,sid':aux_strId_type.(strCmp_str (get_name_strId sid) (get_name_strId sid'))⊗(eqb (get_id_strId sid) (get_id_strId sid')).