From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 31 Jan 2008 15:27:47 +0000 (+0000)
Subject: snapshot
X-Git-Tag: make_still_working~5643
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eac47b8c4a4e136507d82f2cc16b2d0c5093d710;p=helm.git

snapshot
---

diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml
index 86cae6b6b..40b669845 100644
--- 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,35 +52,44 @@ 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
 ;;
diff --git a/helm/software/components/ng_kernel/nUriManager.mli b/helm/software/components/ng_kernel/nUriManager.mli
index 911a1849b..1e8a08cbd 100644
--- a/helm/software/components/ng_kernel/nUriManager.mli
+++ b/helm/software/components/ng_kernel/nUriManager.mli
@@ -23,13 +23,15 @@
  * 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