many strings that are supposed to be URIs are now UriManager.uri

[helm.git] / helm / ocaml / metadata / metadataExtractor.ml

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index a1c24d9c624e9b5a6f53c6ef4f6eea69936ae710..5a7522b90eb6f5c3c017bcecd15d915f5d21d8ac 100644 (file)
--- a/helm/ocaml/metadata/metadataExtractor.ml
+++ b/helm/ocaml/metadata/metadataExtractor.ml
@@ -56,7 +56,7 @@ module OrderedMetadata =
   end
 
 module MetadataSet = Set.Make (OrderedMetadata)
-module StringSet = Set.Make (String)
+module UriManagerSet = UriManager.UriSet
 
 module S = MetadataSet
 
@@ -72,6 +72,9 @@ let var_has_body uri =
   | Cic.Variable (_, Some body, _, _, _), _ -> true
   | _ -> false
 
+let string_of_uriref s =
+ UriManager.uri_of_string (UriManager.string_of_uriref s)
+
 let compute_term pos term =
   let rec aux (pos: position) set = function
     | Cic.Var (uri, subst) when var_has_body uri ->
@@ -130,17 +133,17 @@ let compute_term pos term =
           (fun set term -> aux (next_pos pos) set term)
           set tl
     | Cic.Const (uri, subst) ->
-        let set = S.add (`Obj (string_of_uri uri, pos)) set in
+        let set = S.add (`Obj (uri, pos)) set in
         List.fold_left
           (fun set (_, term) -> aux (next_pos pos) set term)
           set subst
     | Cic.MutInd (uri, typeno, subst) ->
-        let uri = UriManager.string_of_uriref (uri, [typeno]) in
+        let uri = string_of_uriref (uri, [typeno]) in
         let set = S.add (`Obj (uri, pos)) set in
         List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
           set subst
     | Cic.MutConstruct (uri, typeno, consno, subst) ->
-        let uri = UriManager.string_of_uriref (uri, [typeno; consno]) in
+        let uri = string_of_uriref (uri, [typeno; consno]) in
         let set = S.add (`Obj (uri, pos)) set in
         List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
           set subst
@@ -241,13 +244,13 @@ let compute_metas term =
 let compute_type pos uri typeno (name, _, ty, constructors) =
   let consno = ref 0 in
   let type_metadata =
-    (UriManager.string_of_uriref (uri, [typeno]), name, (compute_term pos ty))
+    (string_of_uriref (uri, [typeno]), name, (compute_term pos ty))
   in
   let constructors_metadata =
     List.map
       (fun (name, term) ->
         incr consno;
-        let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in
+        let uri = string_of_uriref (uri, [typeno; !consno]) in
         (uri, name, (compute_term pos term)))
       constructors
   in
@@ -268,14 +271,14 @@ let compute (pos:position) ~body ~ty =
     S.fold
       (fun metadata uris ->
         match metadata with
-        | `Obj (uri, _) -> StringSet.add uri uris
+        | `Obj (uri, _) -> UriManagerSet.add uri uris
         | _ -> uris)
-      type_metadata StringSet.empty
+      type_metadata UriManagerSet.empty
   in
   S.union
     (S.filter
       (function
-        | `Obj (uri, _) when StringSet.mem uri uris -> false
+        | `Obj (uri, _) when UriManagerSet.mem uri uris -> false
         | _ -> true)
       body_metadata)
     type_metadata
@@ -321,7 +324,7 @@ let compute_obj uri =
           S.empty
           params
       in
-      [ UriManager.string_of_uri uri, 
+      [ uri, 
         UriManager.name_of_uri uri,
         S.union metadata var_metadata ]
   | Cic.InductiveDefinition (types, params, _, _) ->