uses new at_least with criteria on constants number difference

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 8dcbcd08abd3e3d9d0d585c4aa390c46223e4e89..b6b360a813a9a3460cda2b39220fae443ac02842 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -60,20 +60,47 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
       (fun cols -> match cols.(0) with Some s -> s | _ -> assert false))
 
 let match_term ~(dbd:Mysql.dbd) ty =
+  prerr_endline (CicPp.ppterm ty);
   let metadata = MetadataExtractor.compute ~body:None ~ty in
   let constants_no =
     MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
   in
-  let full_card =
+  let full_card, diff =
     if CicUtil.is_meta_closed ty then
-      Some (MetadataConstraints.Eq constants_no)
+      Some (MetadataConstraints.Eq constants_no), None
     else
-      None  (* we already require a set of constants to appear, this additional
-             constraints is useless *)
-(*       MetadataConstraints.Gt (constants_no - 1) *)
+      let diff_no =
+        let (hyp_constants, concl_constants) =
+          (* collect different constants in hypotheses and conclusions *)
+          List.fold_left
+            (fun ((hyp, concl) as acc) metadata ->
+               match (metadata: MetadataTypes.metadata) with
+               | `Sort _ | `Rel _ -> acc
+               | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _)
+                 when not (List.mem uri concl) -> (hyp, uri :: concl)
+               | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _)
+                 when not (List.mem uri hyp) -> (uri :: hyp, concl)
+               | `Obj _ -> acc)
+            ([], [])
+            metadata
+        in
+        List.length hyp_constants - List.length concl_constants
+      in
+      let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in
+      let diff =
+        if MetadataExtractor.IntSet.equal concl_metas hyp_metas then
+          Some (MetadataConstraints.Eq diff_no)
+        else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then
+          Some (MetadataConstraints.Gt (diff_no - 1))
+        else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then
+          Some (MetadataConstraints.Lt (diff_no + 1))
+        else
+          None
+      in
+      None, diff
   in
   let constraints = List.map MetadataTypes.constr_of_metadata metadata in
-  Constr.at_least ~dbd ?full_card constraints
+  Constr.at_least ~dbd ?full_card ?diff constraints
 
 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))