X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnReference.ml;h=5da330541997905447ae9341d41d16d566598e03;hb=18d8d7128c16b5d4dd589d75a2e7c026ac7d405d;hp=9d9ed88a6a4098b18c446d530bade36934e8171f;hpb=05e05dd130ec57395615de286ee50c6729d226ac;p=helm.git diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index 9d9ed88a6..5da330541 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,9 +113,22 @@ let string_of_reference (Ref (_,u,indinfo)) = | Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")" ;; +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 mk_fix i j = function + | Ref (d, u, Fix _) -> + reference_of_string (string_of_reference (Ref (d, u, Fix (i,j)))) + | _ -> assert false +;; + let reference_of_ouri u indinfo = let u = NUri.nuri_of_ouri u in - reference_of_string (string_of_reference (Ref (~-1,u,indinfo))) + reference_of_string (string_of_reference (Ref (max_int,u,indinfo))) ;; let ouri_of_reference (Ref (_,u,_)) = NUri.ouri_of_nuri u;; +