From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 31 Jan 2008 16:20:46 +0000 (+0000)
Subject: Transformation back and forth between old and new representation
X-Git-Tag: make_still_working~5642
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1df7f33eaed35696773168dedf9eb1c952a57c19;p=helm.git

Transformation back and forth between old and new representation
---

diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml
index 40b669845..3e75751c6 100644
--- a/helm/software/components/ng_kernel/nUriManager.ml
+++ b/helm/software/components/ng_kernel/nUriManager.ml
@@ -95,9 +95,31 @@ fun s ->
 ;;
 
 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
 ;;
diff --git a/helm/software/components/ng_kernel/nUriManager.mli b/helm/software/components/ng_kernel/nUriManager.mli
index 1e8a08cbd..ae8f793e6 100644
--- a/helm/software/components/ng_kernel/nUriManager.mli
+++ b/helm/software/components/ng_kernel/nUriManager.mli
@@ -40,5 +40,5 @@ val string_of_uri: uri -> string
 
 
 (* CACCA *)
-val nuri_of_ouri: UriManager.uri -> (int * int option ) option -> uri
+val nuri_of_ouri: UriManager.uri -> spec ->  uri
 val ouri_of_nuri: uri -> UriManager.uri