]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataDb.ml
many strings that are supposed to be URIs are now UriManager.uri
[helm.git] / helm / ocaml / metadata / metadataDb.ml
index d82894ed6f67ba9287a727c12b64df98b9f07389..51b432a4f5b843545a1e79eb6adf370d54cd956b 100644 (file)
@@ -74,27 +74,27 @@ let execute_insert dbd uri (sort_cols, rel_cols, obj_cols) =
   
     
 let count_distinct position l =
-  MetadataConstraints.StringSet.cardinal
+  MetadataConstraints.UriManagerSet.cardinal
   (List.fold_left (fun acc d -> 
     match position with
     | `Conclusion -> 
          (match d with
          | `Obj (name,`InConclusion) 
          | `Obj (name,`MainConclusion _ ) -> 
-             MetadataConstraints.StringSet.add name acc
+             MetadataConstraints.UriManagerSet.add name acc
          | _ -> acc)
     | `Hypothesis ->
         (match d with
         | `Obj (name,`InHypothesis) 
         | `Obj (name,`MainHypothesis _) -> 
-            MetadataConstraints.StringSet.add name acc
+            MetadataConstraints.UriManagerSet.add name acc
         | _ -> acc)
     | `Statement ->
         (match d with
         | `Obj (name,`InBody) -> acc
-        | `Obj (name,_) -> MetadataConstraints.StringSet.add name acc
+        | `Obj (name,_) -> MetadataConstraints.UriManagerSet.add name acc
         | _ -> acc)
-    ) MetadataConstraints.StringSet.empty l)
+    ) MetadataConstraints.UriManagerSet.empty l)
 (*    
 let insert_const_no dbd uri =
   let term = CicUtil.term_of_uri uri in 
@@ -119,13 +119,13 @@ let insert_const_no dbd (uri,metadata) =
   let no_full = count_distinct `Statement metadata in
   let insert = 
     sprintf "INSERT INTO %s VALUES (\"%s\", %d, %d, %d)" 
-      (count_tbl ()) uri no_concl no_hyp no_full
+      (count_tbl ()) (UriManager.string_of_uri uri) no_concl no_hyp no_full
   in
   ignore (Mysql.exec dbd insert)
   
 let insert_name ~dbd ~uri ~name =
   let query =
-    sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (name_tbl ()) uri name
+    sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (name_tbl ()) (UriManager.string_of_uri uri) name
   in
   ignore (Mysql.exec dbd query)