renamed Http_client to Http_user_agent to avoid clashes with Gerd's

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index cbca9a9c270304d6feb62fee26b580e39da551cf..3fdecb8c5850a55f700c333557d03892354c053f 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -27,25 +27,29 @@ open Printf
 
 module Constr = MetadataConstraints
 
-let locate ~(dbh:Dbi.connection) name =
+let nonvar s =
+  let len = String.length s in
+  let suffix = String.sub s (len-4) 4 in
+  not (suffix  = ".var")
+
+let locate ~(dbh:Dbi.connection) ?(vars = false) name =
   let query =
     dbh#prepare (sprintf "SELECT source FROM %s WHERE value = \"%s\""
       MetadataTypes.name_tbl name)
   in
   query#execute [];
-  List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ())
+  List.filter nonvar
+    (List.map (function [`String s] -> s | _ -> assert false)
+      (query#fetchall ()))
 
 let match_term ~(dbh:Dbi.connection) ty =
-  let constraints =
-    List.map MetadataTypes.constr_of_metadata
-      (MetadataExtractor.compute ~body:None ~ty)
+  let metadata = MetadataExtractor.compute ~body:None ~ty in
+  let constants_no =
+    MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
   in
-  Constr.at_least ~dbh constraints
-
-let nonvar s =
-  let len = String.length s in
-  let suffix = String.sub s (len-4) 4 in
-  not (suffix  = ".var")
+  let constraints = List.map MetadataTypes.constr_of_metadata metadata in
+  Constr.at_least ~dbh ~full_card:(MetadataConstraints.Eq constants_no)
+    constraints
 
 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
 
@@ -59,10 +63,13 @@ let signature_of_hypothesis context =
           Constr.StringSet.union set (Constr.constants_of t))
     Constr.StringSet.empty context
 
-let intersect l1 l2 =
-  let set1 = List.fold_right Constr.StringSet.add l1 Constr.StringSet.empty in
-  let set2 = List.fold_right Constr.StringSet.add l2 Constr.StringSet.empty in
-  Constr.StringSet.elements (Constr.StringSet.inter set1 set2)
+let intersect uris siguris =
+  let set1 = List.fold_right Constr.StringSet.add uris Constr.StringSet.empty in
+  let set2 =
+    List.fold_right Constr.StringSet.add siguris Constr.StringSet.empty
+  in
+  let inter = Constr.StringSet.inter set1 set2 in
+  List.filter (fun s -> Constr.StringSet.mem s inter) uris
 
 let filter_uris_forward ~dbh (main, constants) uris =
   let main_uris =
@@ -126,8 +133,6 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
     end else
       filter_uris_backward ~dbh (main, other_constants) uris
   in
-prerr_endline "URIS";
-List.iter prerr_endline uris;
   let rec aux = function
     | [] -> []
     | uri :: tl ->
@@ -150,5 +155,18 @@ List.iter prerr_endline uris;
               prerr_endline ("HO APPLICATO " ^ uri);
               status' :: aux tl)
   in
-  aux uris
+  List.stable_sort
+    (fun (_, (_, goals1)) (_, (_, goals2)) ->
+      Pervasives.compare (List.length goals1) (List.length goals2))
+    (aux uris)
+
+let elim ~dbh uri =
+  let constraints =
+    [`Rel [`MainConclusion None];
+     `Sort (Cic.Prop,[`MainHypothesis (Some 1)]);
+     `Obj (uri,[`MainHypothesis (Some 0)]);
+     `Obj (uri,[`InHypothesis]);
+    ]
+  in
+  MetadataConstraints.at_least ~dbh constraints