added mk_fix i j r that given an r of a fix generated another fix on i and j

[helm.git] / helm / software / components / ng_kernel / nReference.ml

diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml
index bcdd4713ea6ab1041247526e83bd5a30a98cd625..5da330541997905447ae9341d41d16d566598e03 100644 (file)
--- a/helm/software/components/ng_kernel/nReference.ml
+++ b/helm/software/components/ng_kernel/nReference.ml
@@ -33,12 +33,10 @@ type spec =
  | Ind of int
  | Con of int * int (* indtyno, constrno *)
 
-type reference = Ref of int * string * spec
+type reference = Ref of int * NUri.uri * spec
 
 let eq = (==);;
 
-let string_of_reference (Ref (_,s,_)) = s;;
-
 module OrderedStrings =
  struct
   type t = string
@@ -46,9 +44,9 @@ module OrderedStrings =
  end
 ;;
 
-module MapStringsToUri = Map.Make(OrderedStrings);;
+module MapStringsToReference = Map.Make(OrderedStrings);;
 
-let set_of_reference = ref MapStringsToUri.empty;;
+let set_of_reference = ref MapStringsToReference.empty;;
 
 (* '.' not allowed in path and foo
  *
@@ -60,6 +58,12 @@ let set_of_reference = ref MapStringsToUri.empty;;
  * Con of int * int       cic:/path/foo.con(i,j)
  *)
 
+let uri_suffix_of_ref_suffix = function
+    | "dec" | "fix" | "cfx" | "def" -> "con"
+    | "ind" | "con" -> "ind"
+    | x -> prerr_endline (x ^ " not a valid suffix"); assert false
+;;
+
 let reference_of_string =
   let counter = ref 0 in 
   let c () = incr counter; !counter in 
@@ -70,56 +74,61 @@ 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 ->
-  try MapStringsToUri.find s !set_of_reference
+  try MapStringsToReference.find s !set_of_reference
   with Not_found ->
     let new_reference =
       try
         let dot = String.rindex s '.' in
+        let prefix = String.sub s 0 (dot+1) in
         let suffix = String.sub s (dot+1) 3 in
+        let u = NUri.uri_of_string (prefix ^ uri_suffix_of_ref_suffix suffix) in
         match suffix with
-        | "dec" -> Ref (c (), s, Decl)
-        | "def" -> Ref (c (), s, Def)
-        | "fix" -> let i,j = get2 s dot in Ref (c (), s, Fix (i,j))
-        | "cfx" -> let i = get1 s dot in Ref (c (), s, CoFix (i))
-        | "ind" -> let i = get1 s dot in Ref (c (), s, Ind (i))
-        | "con" -> let i,j = get2 s dot in Ref (c (), s, Con (i,j))
+        | "dec" -> Ref (c (), u, Decl)
+        | "def" -> Ref (c (), u, Def)
+        | "fix" -> let i,j = get2 s dot in Ref (c (), u, Fix (i,j))
+        | "cfx" -> let i = get1 s dot in Ref (c (), u, CoFix (i))
+        | "ind" -> let i = get1 s dot in Ref (c (), u, Ind (i))
+        | "con" -> let i,j = get2 s dot in Ref (c (), u, Con (i,j))
         | _ -> raise Not_found
       with Not_found -> raise (IllFormedReference (lazy s))
     in
-    set_of_reference := MapStringsToUri.add s new_reference !set_of_reference;
+    set_of_reference := MapStringsToReference.add s new_reference !set_of_reference;
     new_reference
 ;;
 
-let reference_of_ouri u indinfo =
-  let s = UriManager.string_of_uri u in
+let string_of_reference (Ref (_,u,indinfo)) =
+  let s = NUri.string_of_uri u in
   let dot = String.rindex s '.' in
   let s2 = String.sub s 0 dot in
-  let ns = match indinfo with
+  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 reference_of_string ns
 ;;
 
-let ouri_of_reference u =
-  let s = string_of_reference 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
+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 (max_int,u,indinfo)))
+;;
+
+let ouri_of_reference (Ref (_,u,_)) = NUri.ouri_of_nuri u;;
+