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

[helm.git] / helm / ocaml / tactics / metadataQuery.ml

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 1e7bbe690cc3ca52033d577965cd60e60fc1bbef..644e764ef56c18b927777d013cfc6a0dd8bebd3d 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -44,6 +44,7 @@ let sqlpat_of_shellglob =
             shellglob)))
 
 let nonvar s =
+  let s = UriManager.string_of_uri s in
   let len = String.length s in
   let suffix = String.sub s (len-4) 4 in
   not (suffix  = ".var")
@@ -59,13 +60,13 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
   let result = Mysql.exec dbd query in
   List.filter nonvar
     (Mysql.map result
-      (fun cols -> match cols.(0) with Some s -> s | _ -> assert false))
+      (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false))
 
 let match_term ~(dbd:Mysql.dbd) ty =
 (*   debug_print (CicPp.ppterm ty); *)
   let metadata = MetadataExtractor.compute ~body:None ~ty in
   let constants_no =
-    MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
+    MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty)
   in
   let full_card, diff =
     if CicUtil.is_meta_closed ty then
@@ -113,16 +114,16 @@ let signature_of_hypothesis context =
       | None -> set
       | Some (_, Cic.Decl t)
       | Some (_, Cic.Def (t, _)) ->
-          Constr.StringSet.union set (Constr.constants_of t))
-    Constr.StringSet.empty context
+          Constr.UriManagerSet.union set (Constr.constants_of t))
+    Constr.UriManagerSet.empty context
 
 let intersect uris siguris =
-  let set1 = List.fold_right Constr.StringSet.add uris Constr.StringSet.empty in
+  let set1 = List.fold_right Constr.UriManagerSet.add uris Constr.UriManagerSet.empty in
   let set2 =
-    List.fold_right Constr.StringSet.add siguris Constr.StringSet.empty
+    List.fold_right Constr.UriManagerSet.add siguris Constr.UriManagerSet.empty
   in
-  let inter = Constr.StringSet.inter set1 set2 in
-  List.filter (fun s -> Constr.StringSet.mem s inter) uris
+  let inter = Constr.UriManagerSet.inter set1 set2 in
+  List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
 
 let filter_uris_forward ~dbd (main, constants) uris =
   let main_uris =
@@ -131,7 +132,7 @@ let filter_uris_forward ~dbd (main, constants) uris =
     | Some (main, types) -> main :: types
   in
   let full_signature =
-    List.fold_right Constr.StringSet.add main_uris constants
+    List.fold_right Constr.UriManagerSet.add main_uris constants
   in
   List.filter (Constr.at_most ~dbd ~where:`Statement full_signature) uris
 
@@ -182,18 +183,18 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
   let types_constants =
     match main with
-    | None -> Constr.StringSet.empty
+    | None -> Constr.UriManagerSet.empty
     | Some (main, types) ->
-        List.fold_right Constr.StringSet.add (main :: types)
-          Constr.StringSet.empty
+        List.fold_right Constr.UriManagerSet.add (main :: types)
+          Constr.UriManagerSet.empty
   in
   let hyp_constants =
-    Constr.StringSet.diff (signature_of_hypothesis context) types_constants
+    Constr.UriManagerSet.diff (signature_of_hypothesis context) types_constants
   in
-(* Constr.StringSet.iter debug_print hyp_constants; *)
-  let other_constants = Constr.StringSet.union sig_constants hyp_constants in
+(* Constr.UriManagerSet.iter debug_print hyp_constants; *)
+  let other_constants = Constr.UriManagerSet.union sig_constants hyp_constants in
   let uris = 
-    let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
+    let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in
     if ((List.length uris < pow) or (pow <= 0))
     then begin
 (*       debug_print "MetadataQuery: large sig, falling back to old method"; *)
@@ -210,7 +211,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
 (*                debug_print ("STO APPLICANDO " ^ uri); *)
                PET.apply_tactic
                   (PrimitiveTactics.apply_tac
-                   ~term:(CicUtil.term_of_uri uri))
+                   ~term:(CicUtil.term_of_uri (UriManager.string_of_uri uri)))
                   status
               in
               let goal_list =
@@ -239,13 +240,13 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
     of the experimentation we shall make a choice. *)
 
 let close_with_types s metasenv context =
-  Constr.StringSet.fold 
+  Constr.UriManagerSet.fold 
     (fun e bag -> 
-      let t = CicUtil.term_of_uri e in
+      let t = CicUtil.term_of_uri (UriManager.string_of_uri e) in
       let ty, _ = 
         CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph  
       in
-      Constr.StringSet.union bag (Constr.constants_of ty)) 
+      Constr.UriManagerSet.union bag (Constr.constants_of ty)) 
     s s
 
 let experimental_hint 
@@ -263,40 +264,40 @@ let experimental_hint
   let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
   let types_constants =
     match main with
-    | None -> Constr.StringSet.empty
+    | None -> Constr.UriManagerSet.empty
     | Some (main, types) ->
-        List.fold_right Constr.StringSet.add (main :: types)
-          Constr.StringSet.empty
+        List.fold_right Constr.UriManagerSet.add (main :: types)
+          Constr.UriManagerSet.empty
   in
   let all_constants =
     let hyp_and_sug =
-      Constr.StringSet.union
+      Constr.UriManagerSet.union
         (signature_of_hypothesis context) 
         sig_constants
     in
     let main = 
       match main with
-      | None -> Constr.StringSet.empty
+      | None -> Constr.UriManagerSet.empty
       | Some (main,_) -> 
           let ty, _ = 
             CicTypeChecker.type_of_aux' 
-              metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
+              metasenv context (CicUtil.term_of_uri (UriManager.string_of_uri main)) CicUniv.empty_ugraph
           in
           Constr.constants_of ty
     in
-    Constr.StringSet.union main hyp_and_sug
+    Constr.UriManagerSet.union main hyp_and_sug
   in
-(* Constr.StringSet.iter debug_print hyp_constants; *)
+(* Constr.UriManagerSet.iter debug_print hyp_constants; *)
   let all_constants_closed = close_with_types all_constants metasenv context in
   let other_constants = 
-    Constr.StringSet.diff all_constants_closed types_constants
+    Constr.UriManagerSet.diff all_constants_closed types_constants
   in
   debug_print "all_constants_closed";
-  Constr.StringSet.iter debug_print all_constants_closed;
+  Constr.UriManagerSet.iter debug_print all_constants_closed;
   debug_print "other_constants";
-  Constr.StringSet.iter debug_print other_constants;
+  Constr.UriManagerSet.iter debug_print other_constants;
   let uris = 
-    let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
+    let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in
     if ((List.length uris < pow) or (pow <= 0))
     then begin
       debug_print "MetadataQuery: large sig, falling back to old method";
@@ -312,7 +313,7 @@ let experimental_hint
               let (subst,(proof, goal_list)) =
                   (* debug_print ("STO APPLICANDO" ^ uri); *)
                   PrimitiveTactics.apply_tac_verbose 
-                   ~term:(CicUtil.term_of_uri uri)
+                   ~term:(CicUtil.term_of_uri (UriManager.string_of_uri uri))
                   status
               in
               let goal_list =
@@ -366,13 +367,14 @@ let instance ~dbd t =
   let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in
   let no_full = MetadataDb.count_distinct `Statement metadata in
   let is_dummy = function
-    | `Obj(s, _) -> (String.sub s 0 10) <> "cic:/dummy" 
+    | `Obj(s, _) -> (String.sub (UriManager.string_of_uri s) 0 10) <> "cic:/dummy" 
          | _ -> true 
   in
   let rec look_for_dummy_main = function
          | [] -> None
     | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_ 
-      when ((String.sub s 0 10) = "cic:/dummy") -> 
+      when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") -> 
+      let s = UriManager.string_of_uri s in
       let len = String.length s in
             let dummy_index = int_of_string (String.sub s 11 (len-11)) in
       let dummy_type = List.nth types dummy_index in
@@ -496,7 +498,7 @@ let fwd_simpl ~dbd t =
    in
    let compare (_, x) (_, y) = compare x y in
    let filter n (uri, rank) =
-      if rank > 0 then Some uri else None
+      if rank > 0 then Some (UriManager.uri_of_string uri) else None
    in   
    match get_metadata t with
       | None                 -> []