X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnReference.ml;h=2692075e02796a5c3958e066854513d2de720059;hb=c25986cdbd05f0c06d93f850453b5f82695b7814;hp=ad93584fbc2a7ed3281df5018e13368e6cc6fda3;hpb=813025418906707f7bbbf43732fc0e8d5cfc6943;p=helm.git diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index ad93584fb..2692075e0 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -59,11 +59,9 @@ let set_of_reference = ref MapStringsToReference.empty;; *) let uri_suffix_of_ref_suffix = function - | "dec" - | "def" -> "con" - | "ind" - | "con" -> "ind" - | _ -> assert false + | "dec" | "fix" | "cfx" | "def" -> "con" + | "ind" | "con" -> "ind" + | x -> prerr_endline (x ^ " not a valid suffix"); assert false ;; let reference_of_string = @@ -76,7 +74,7 @@ let reference_of_string = i,j in let get1 s dot = - let i = int_of_string (String.sub s (dot+5) (String.length s-1)) in + let i = int_of_string (String.sub s (dot+5) (String.length s-1-dot-5)) in i in fun s -> @@ -115,11 +113,16 @@ let string_of_reference (Ref (_,u,indinfo)) = | Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")" ;; -let reference_of_ouri u indinfo = - let u = NUri.uri_of_string (UriManager.string_of_uri u) in - reference_of_string (string_of_reference (Ref (~-1,u,indinfo))) +let mk_constructor j = function + | Ref (d, u, Ind i) -> + reference_of_string (string_of_reference (Ref (d, u, Con (i,j)))) + | _ -> assert false ;; -let ouri_of_reference (Ref (_,u,_)) = - UriManager.uri_of_string (NUri.string_of_uri u) +let reference_of_ouri u indinfo = + let u = NUri.nuri_of_ouri u in + reference_of_string (string_of_reference (Ref (max_int,u,indinfo))) ;; + +let ouri_of_reference (Ref (_,u,_)) = NUri.ouri_of_nuri u;; +