One Obj.magic implemented, trust changed to false.

[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 de7116cb1a7dbcfa3ec329441106fa082a545c38..3e75751c61d5abba43203cbcce7a9d47d79d1359 100644 (file)
--- a/helm/software/components/ng_kernel/nUriManager.ml
+++ b/helm/software/components/ng_kernel/nUriManager.ml
@@ -23,18 +23,103 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception IllFormedUri of string Lazy.t;;
+exception IllFormedUri of string Lazy.t
 
-(*                        order, uri,      (type, constructor)        *)
-type uri = private Uri of int *  string *  (int * int option ) option
+type spec = 
+ | Decl 
+ | Def
+ | Fix of int * int (* fixno, recparamno *)
+ | CoFix of int
+ | Ind of int
+ | Con of int * int (* indtyno, constrno *)
 
-let eq (Uri(_,x1,x2)) (Uri(_,y1,y2)) = x1 = y1 && x2 = y2;;
+type uri = Uri of int * string * spec
 
-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 ^ ")"
+let eq = (==);;
+
+let string_of_uri (Uri (_,s,_)) = s;;
+
+module OrderedStrings =
+ struct
+  type t = string
+  let compare (s1 : t) (s2 : t) = compare s1 s2
+ end
+;;
+
+module MapStringsToUri = Map.Make(OrderedStrings);;
+
+let set_of_uri = ref MapStringsToUri.empty;;
+
+(* '.' 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 =
+  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 =
+      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 =
+  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 =
+  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
+;;