From: Enrico Tassi Date: Tue, 5 Feb 2008 15:20:38 +0000 (+0000) Subject: uri -> reference X-Git-Tag: make_still_working~5633 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3f5fd615a881e80716b35f4f0084934850555a55;p=helm.git uri -> reference --- diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 6466912a1..9221ba8d4 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -43,10 +43,10 @@ and term = | Prod of name * term * term (* binder, source, target *) | Lambda of name * term * term (* binder, source, target *) | LetIn of name * term * term * term (* binder, type, term, body *) - | Const of NUriManager.uri (* uri contains indtypeno/constrno *) + | Const of NUriManager.reference (* reference contains indtypeno/constrno *) | Sort of sort (* sort *) | Implicit of implicit_annotation (* ... *) - | MutCase of NUriManager.uri * (* ind. uri, *) + | MutCase of NUriManager.reference * (* ind. reference, *) term * term * (* outtype, ind. term *) term list (* patterns *) diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml index 3e75751c6..745f9359c 100644 --- a/helm/software/components/ng_kernel/nUriManager.ml +++ b/helm/software/components/ng_kernel/nUriManager.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -exception IllFormedUri of string Lazy.t +exception IllFormedReference of string Lazy.t type spec = | Decl @@ -33,11 +33,11 @@ type spec = | Ind of int | Con of int * int (* indtyno, constrno *) -type uri = Uri of int * string * spec +type reference = Ref of int * string * spec let eq = (==);; -let string_of_uri (Uri (_,s,_)) = s;; +let string_of_reference (Uri (_,s,_)) = s;; module OrderedStrings = struct @@ -48,7 +48,7 @@ module OrderedStrings = module MapStringsToUri = Map.Make(OrderedStrings);; -let set_of_uri = ref MapStringsToUri.empty;; +let set_of_reference = ref MapStringsToUri.empty;; (* '.' not allowed in path and foo * @@ -60,7 +60,7 @@ let set_of_uri = ref MapStringsToUri.empty;; * Con of int * int cic:/path/foo.con(i,j) *) -let uri_of_string = +let reference_of_string = let counter = ref 0 in let c () = incr counter; !counter in let get2 s dot = @@ -74,9 +74,9 @@ let uri_of_string = i in fun s -> - try MapStringsToUri.find s !set_of_uri + try MapStringsToUri.find s !set_of_reference with Not_found -> - let new_uri = + let new_reference = try let dot = String.rindex s '.' in let suffix = String.sub s (dot+1) 3 in @@ -90,11 +90,11 @@ fun s -> | _ -> raise Not_found with Not_found -> raise (IllFormedUri (lazy s)) in - set_of_uri := MapStringsToUri.add s new_uri !set_of_uri; - new_uri + set_of_reference := MapStringsToUri.add s new_reference !set_of_reference; + new_reference ;; -let nuri_of_ouri u indinfo = +let reference_of_ouri u indinfo = let s = UriManager.string_of_uri u in let dot = String.rindex s '.' in let s2 = String.sub s 0 dot in @@ -105,11 +105,11 @@ let nuri_of_ouri u indinfo = | CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")" | Ind i -> s2 ^ ".ind(" ^ string_of_int i ^ ")" | Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")" - in uri_of_string ns + in reference_of_string ns ;; -let ouri_of_nuri u = - let s = string_of_uri u in +let ouri_of_reference u = + let s = string_of_reference u in let dot = String.rindex s '.' in let prefix = String.sub s 0 dot in let suffix = String.sub s (dot+1) 3 in diff --git a/helm/software/components/ng_kernel/nUriManager.mli b/helm/software/components/ng_kernel/nUriManager.mli index ae8f793e6..116e30ac9 100644 --- a/helm/software/components/ng_kernel/nUriManager.mli +++ b/helm/software/components/ng_kernel/nUriManager.mli @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -exception IllFormedUri of string Lazy.t +exception IllFormedReference of string Lazy.t type spec = | Decl @@ -33,12 +33,12 @@ type spec = | Ind of int | Con of int * int (* indtyno, constrno *) -type uri = Uri of int * string * spec +type reference = Ref of int * string * spec -val eq: uri -> uri -> bool -val string_of_uri: uri -> string +val eq: reference -> reference -> bool +val string_of_reference: reference -> string (* CACCA *) -val nuri_of_ouri: UriManager.uri -> spec -> uri -val ouri_of_nuri: uri -> UriManager.uri +val reference_of_ouri: UriManager.uri -> spec -> reference +val ouri_of_reference: reference -> UriManager.uri