Transformation back and forth between old and new representation

[helm.git] / helm / software / components / ng_kernel / nUriManager.ml

diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml
index 86cae6b6ba4984d59c18f725c9de170a02b78ae9..3e75751c61d5abba43203cbcce7a9d47d79d1359 100644 (file)
--- a/helm/software/components/ng_kernel/nUriManager.ml
+++ b/helm/software/components/ng_kernel/nUriManager.ml
@@ -23,19 +23,21 @@
  * http://cs.unibo.it/helm/.
  *)
 
+exception IllFormedUri of string Lazy.t
+
 type spec = 
  | Decl 
  | Def
  | Fix of int * int (* fixno, recparamno *)
  | CoFix of int
  | Ind of int
- | IConstr of int * int (* indtyno, constrno *)
+ | Con of int * int (* indtyno, constrno *)
 
-type uri = Uri of int *  string * spec
+type uri = Uri of int * string * spec
 
 let eq = (==);;
 
-let string_of_uri (Uri (_,s,_)) = s ;;
+let string_of_uri (Uri (_,s,_)) = s;;
 
 module OrderedStrings =
  struct
@@ -50,43 +52,74 @@ let set_of_uri = ref MapStringsToUri.empty;;
 
 (* '.' not allowed in path and foo
  *
- * Decl                   cic:/path/foo.decl
+ * 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.cofix(i)
+ * CoFix of int           cic:/path/foo.cfx(i)
  * Ind of int             cic:/path/foo.ind(i)
- * Constr of int * int    cic:/path/foo.constr(i,j)
+ * Con of int * int       cic:/path/foo.con(i,j)
  *)
 
-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)
-;;
-
-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
 ;;