X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnUriManager.ml;h=3e75751c61d5abba43203cbcce7a9d47d79d1359;hb=1df7f33eaed35696773168dedf9eb1c952a57c19;hp=95e3271b1344cc183a4b67b1227ac35f19ff0131;hpb=71303c30466f24b8953def22a80175c00dd975af;p=helm.git

diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml
index 95e3271b1..3e75751c6 100644
--- a/helm/software/components/ng_kernel/nUriManager.ml
+++ b/helm/software/components/ng_kernel/nUriManager.ml
@@ -23,18 +23,21 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(*                order, uri,      (which, constructor)        *)
-type uri = Uri of int *  string *  (int  * int option ) option
+exception IllFormedUri of string Lazy.t
+
+type spec = 
+ | Decl 
+ | Def
+ | Fix of int * int (* fixno, recparamno *)
+ | CoFix of int
+ | Ind of int
+ | Con of int * int (* indtyno, constrno *)
+
+type uri = Uri of int * string * spec
 
 let eq = (==);;
 
-let string_of_uri = function
-  | Uri (_,s,None) -> s
-  | Uri (_,s,Some (i,None)) -> 
-      s ^ "#xpointer(1/" ^ string_of_int (i+1) ^ ")"
-  | Uri (_,s,Some (i, Some k)) -> 
-      s ^ "#xpointer(1/" ^ string_of_int (i+1) ^ "/" ^ string_of_int (k+1) ^ ")"
-;;
+let string_of_uri (Uri (_,s,_)) = s;;
 
 module OrderedStrings =
  struct
@@ -47,35 +50,76 @@ module MapStringsToUri = Map.Make(OrderedStrings);;
 
 let set_of_uri = ref MapStringsToUri.empty;;
 
-let uri_of_string_aux =
-  let counter = ref 0 in fun s ->
-  incr counter;
-  try
-    let sharp = String.rindex s '#' in
-    let pre = String.sub s 0 sharp in
-    let ind = String.sub s (sharp+12) (String.length s - (sharp+13)) in
-    try
-      let slash = String.rindex ind '/' in
-      let indno = String.sub ind 0 slash in   
-      let constr = String.sub ind (slash+1) (String.length ind - (slash+1)) in
-      Uri(!counter,pre,Some(int_of_string indno-1,Some(int_of_string constr-1)))
-    with Not_found -> Uri (!counter,pre,Some (int_of_string ind-1, None))
-  with Not_found -> Uri (!counter,s,None)
-;;
+(* '.' not allowed in path and foo
+ *
+ * Decl                   cic:/path/foo.dec
+ * Def                    cic:/path/foo.def
+ * Fix of int * int       cic:/path/foo.fix(i,j)
+ * CoFix of int           cic:/path/foo.cfx(i)
+ * Ind of int             cic:/path/foo.ind(i)
+ * Con of int * int       cic:/path/foo.con(i,j)
+ *)
 
-let uri_of_string s =
-  try
-    MapStringsToUri.find s !set_of_uri
+let uri_of_string =
+  let counter = ref 0 in 
+  let c () = incr counter; !counter in 
+  let get2 s dot =
+    let comma = String.rindex s ',' in
+    let i = int_of_string (String.sub s (dot+5) (comma-dot-5)) in
+    let j = int_of_string (String.sub s (comma+1) (String.length s-comma-2)) in
+    i,j
+  in
+  let get1 s dot =
+    let i = int_of_string (String.sub s (dot+5) (String.length s-1)) in
+    i
+  in
+fun s ->
+  try MapStringsToUri.find s !set_of_uri
   with Not_found ->
-    let new_uri = uri_of_string_aux s in
+    let new_uri =
+      try
+        let dot = String.rindex s '.' in
+        let suffix = String.sub s (dot+1) 3 in
+        match suffix with
+        | "dec" -> Uri (c (), s, Decl)
+        | "def" -> Uri (c (), s, Def)
+        | "fix" -> let i,j = get2 s dot in Uri (c (), s, Fix (i,j))
+        | "cfx" -> let i = get1 s dot in Uri (c (), s, CoFix (i))
+        | "ind" -> let i = get1 s dot in Uri (c (), s, Ind (i))
+        | "con" -> let i,j = get2 s dot in Uri (c (), s, Con (i,j))
+        | _ -> raise Not_found
+      with Not_found -> raise (IllFormedUri (lazy s))
+    in
     set_of_uri := MapStringsToUri.add s new_uri !set_of_uri;
     new_uri
 ;;
 
 let nuri_of_ouri u indinfo =
-  uri_of_string (string_of_uri (Uri(0,UriManager.string_of_uri u,indinfo)))
+  let s = UriManager.string_of_uri u in
+  let dot = String.rindex s '.' in
+  let s2 = String.sub s 0 dot in
+  let ns = match indinfo with
+  | Decl ->  s2 ^ ".dec"
+  | Def -> s2 ^ ".def"
+  | Fix (i,j)  -> s2 ^ ".fix(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
+  | 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
 ;;
 
 let ouri_of_nuri u =
-  UriManager.uri_of_string (string_of_uri u)
+  let s = string_of_uri 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
+  let os =  
+    match suffix with
+    | "dec" 
+    | "def" -> prefix ^ ".con"
+    | "ind" 
+    | "con" -> prefix ^ ".ind"
+    | _ -> assert false
+  in
+  UriManager.uri_of_string os
 ;;