uri and references(uri)

diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend
index 497730e2b556790812b2b6370283e1b574801c4d..5fb3278edbc64d5abdc9d1c56083d5234eaf597c 100644 (file)
--- a/helm/software/components/ng_kernel/.depend
+++ b/helm/software/components/ng_kernel/.depend
@@ -1,13 +1,16 @@
 nCicEnvironment.cmi: nReference.cmi nCic.cmo 
 nCicTypeChecker.cmi: nCic.cmo 
+nReference.cmi: nUri.cmi 
 oCic2NCic.cmi: nCic.cmo 
-nCicEnvironment.cmo: oCic2NCic.cmi nCicEnvironment.cmi 
-nCicEnvironment.cmx: oCic2NCic.cmx nCicEnvironment.cmi 
+nCicEnvironment.cmo: oCic2NCic.cmi nReference.cmi nCicEnvironment.cmi 
+nCicEnvironment.cmx: oCic2NCic.cmx nReference.cmx nCicEnvironment.cmi 
 nCicTypeChecker.cmo: nCicTypeChecker.cmi 
 nCicTypeChecker.cmx: nCicTypeChecker.cmi 
-nReference.cmo: nReference.cmi 
-nReference.cmx: nReference.cmi 
+nReference.cmo: nUri.cmi nReference.cmi 
+nReference.cmx: nUri.cmx nReference.cmi 
 oCicTypeChecker.cmo: oCic2NCic.cmi nCicTypeChecker.cmi oCicTypeChecker.cmi 
 oCicTypeChecker.cmx: oCic2NCic.cmx nCicTypeChecker.cmx oCicTypeChecker.cmi 
 oCic2NCic.cmo: oCic2NCic.cmi 
 oCic2NCic.cmx: oCic2NCic.cmi 
+nUri.cmo: nUri.cmi 
+nUri.cmx: nUri.cmi 

diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile
index 20917028861e2084bb0ded1e57d1bccf3fb08c0d..65c0ab906597f92c8d904ffeef08b4ce5f01d9f4 100644 (file)
--- a/helm/software/components/ng_kernel/Makefile
+++ b/helm/software/components/ng_kernel/Makefile
@@ -2,7 +2,7 @@ PACKAGE = ng_kernel
 PREDICATES =
 
 INTERFACE_FILES = \
-       nCicEnvironment.mli nCicTypeChecker.mli nReference.mli oCicTypeChecker.mli oCic2NCic.mli
+       nCicEnvironment.mli nCicTypeChecker.mli nReference.mli oCicTypeChecker.mli oCic2NCic.mli nUri.mli
 IMPLEMENTATION_FILES = \
   nCic.ml $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL = 

diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml
index bcdd4713ea6ab1041247526e83bd5a30a98cd625..ad93584fbc2a7ed3281df5018e13368e6cc6fda3 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,14 @@ 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" 
+    | "def" -> "con"
+    | "ind" 
+    | "con" -> "ind"
+    | _ -> assert false
+;;
+
 let reference_of_string =
   let counter = ref 0 in 
   let c () = incr counter; !counter in 
@@ -74,52 +80,46 @@ let reference_of_string =
     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 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 ouri_of_reference (Ref (_,u,_)) =
+  UriManager.uri_of_string (NUri.string_of_uri u)
 ;;

diff --git a/helm/software/components/ng_kernel/nReference.mli b/helm/software/components/ng_kernel/nReference.mli
index 116e30ac95bce6610147b2288383d1c692569979..1904f99c941a80fd9ff488df61d670c4c78a1bbd 100644 (file)
--- a/helm/software/components/ng_kernel/nReference.mli
+++ b/helm/software/components/ng_kernel/nReference.mli
@@ -33,7 +33,7 @@ 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
 
 val eq: reference -> reference -> bool
 val string_of_reference: reference -> string 

diff --git a/helm/software/components/ng_kernel/nUri.ml b/helm/software/components/ng_kernel/nUri.ml
new file mode 100644 (file)
index 0000000..1b7d519
--- /dev/null
+++ b/helm/software/components/ng_kernel/nUri.ml
@@ -0,0 +1,37 @@
+type uri = int * string (* shareno, URI *)
+
+let string_of_uri (_, uri) = uri;;
+
+module OrderedStrings =
+ struct
+  type t = string
+  let compare (s1 : t) (s2 : t) = compare s1 s2
+ end
+;;
+
+module MapStringsToUri = Map.Make(OrderedStrings);;
+
+let set_of_uri = ref MapStringsToUri.empty;;
+
+let uri_of_string = 
+  let counter = ref 0 in 
+  let c () = incr counter; !counter in 
+fun s ->
+  try MapStringsToUri.find s !set_of_uri
+  with Not_found ->
+    let new_uri = c(), s in
+    set_of_uri := MapStringsToUri.add s new_uri !set_of_uri;
+    new_uri
+;;
+
+let eq = (==);;
+let compare (n1,_) (n2,_) = n2 - n1;;
+
+module HT = struct
+        type t = uri
+        let equal = eq
+        let compare = compare
+        let hash (n,_) = n;;
+end;;
+
+module UriHash = Hashtbl.Make(HT);;

diff --git a/helm/software/components/ng_kernel/nUri.mli b/helm/software/components/ng_kernel/nUri.mli
new file mode 100644 (file)
index 0000000..d0dcb72
--- /dev/null
+++ b/helm/software/components/ng_kernel/nUri.mli
@@ -0,0 +1,7 @@
+type uri
+
+val string_of_uri: uri -> string
+val uri_of_string: string -> uri
+val eq: uri -> uri -> bool
+
+module UriHash: Hashtbl.S with type key = uri