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 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "utility/ascii.ma".
24 include "utility/utility.ma".
26 (* ************************ *)
27 (* MANIPOLAZIONE DI STRINGA *)
28 (* ************************ *)
31 ndefinition aux_str_type ≝ list ascii.
34 ndefinition empty_str ≝ nil ascii.
37 ndefinition isNull_str ≝
38 λstr:aux_str_type.match str with
39 [ nil ⇒ true | cons _ _ ⇒ false ].
42 nlet rec eq_str (str,str':aux_str_type) ≝
44 [ nil ⇒ match str' with
47 | cons h t ⇒ match str' with
49 | cons h' t' ⇒ (eq_ascii h h')⊗(eq_str t t')
54 ndefinition strCat_str ≝
55 λstr,str':aux_str_type.str@str'.
58 ndefinition strLen_str ≝ len_list ascii.
65 ninductive aux_strId_type : Type ≝
66 STR_ID: aux_str_type → nat → aux_strId_type.
68 ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
69 λP:aux_strId_type → Prop.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
70 match a with [ STR_ID l n ⇒ f l n ].
72 ndefinition aux_strId_type_rec : ΠP:aux_strId_type → Set.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
73 λP:aux_strId_type → Set.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
74 match a with [ STR_ID l n ⇒ f l n ].
76 ndefinition aux_strId_type_rect : ΠP:aux_strId_type → Type.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
77 λP:aux_strId_type → Type.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
78 match a with [ STR_ID l n ⇒ f l n ].
81 ndefinition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
82 ndefinition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ].
85 ndefinition eq_strId ≝
86 λ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')).