From 1df7f33eaed35696773168dedf9eb1c952a57c19 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 31 Jan 2008 16:20:46 +0000 Subject: [PATCH] Transformation back and forth between old and new representation --- .../components/ng_kernel/nUriManager.ml | 26 +++++++++++++++++-- .../components/ng_kernel/nUriManager.mli | 2 +- 2 files changed, 25 insertions(+), 3 deletions(-) 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 -- 2.39.2