From: Enrico Tassi <enrico.tassi@inria.fr>
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