Wrong invariant: Hypothesis (i.e. lambda-abstractions) can have no

[helm.git] / helm / software / components / metadata / metadataConstraints.ml

diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml
index 07fcc738b0b2fee951580106307200b4823f505c..d7192bd7e75e12c65f1c0d12922ec6e5e3f31673 100644 (file)
--- a/helm/software/components/metadata/metadataConstraints.ml
+++ b/helm/software/components/metadata/metadataConstraints.ml
@@ -29,7 +29,7 @@ open Printf
 open MetadataTypes 
 
 let critical_value = 7
-let just_factor = 3
+let just_factor = 1
 
 module UriManagerSet = UriManager.UriSet
 module SetSet = Set.Make (UriManagerSet)
@@ -174,17 +174,21 @@ let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
 let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables
   (metadata: MetadataTypes.constr list)
 =
-  let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables 
-  in
+  let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables in
   if (metadata = []) && concl_card = None && full_card = None then
-    failwith "MetadataQuery.at_least: no constraints given";
-  let (n,from,where) =
-    List.fold_left (add_constraint ~tables) (0,[],[]) metadata
-  in
-  let (n,from,where) =
-    add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
-  in
-  exec ~dbd ?rating (n,from,where)
+    begin
+      HLog.warn "MetadataConstraints.at_least: no constraints given";
+      []
+    end
+  else
+    let (n,from,where) =
+      List.fold_left (add_constraint ~tables) (0,[],[]) metadata
+    in
+    let (n,from,where) =
+      add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
+    in
+    exec ~dbd ?rating (n,from,where)
+;;
     
 let at_least  
   ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating
@@ -384,7 +388,7 @@ let rec signature_of = function
       Some (u, []), add l
   | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
       let suri = UriManager.uri_of_uriref u t None in
-      if u = HelmLibraryObjects.Logic.eq_URI then
+       if LibraryObjects.is_eq_URI u then 
          (* equality is handled in a special way: in particular, 
              the type, if defined, is always added to the prefix, 
             and n is not decremented - it should have been n-2 *)
@@ -400,7 +404,7 @@ let rec signature_of = function
             let suri1 = UriManager.uri_of_uriref u1 t1 (Some c1) in
            let inconcl =  UriManagerSet.remove suri1 (add l1) in
             Some (suri, [suri1]), inconcl
-       | _ :: _ -> Some (suri, []), UriManagerSet.empty
+       | _ :: tl -> Some (suri, []), add tl
        | _ -> assert false (* args number must be > 0 *)
       else
        Some (suri, []), add l
@@ -541,8 +545,13 @@ let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
             List.map (fun uri -> (card, uri)) res))
           maximal_prefixes)
     in
-    Printf.fprintf stderr "all: %d\n" (List.length all);flush_all ();
-    List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
+(*     Printf.fprintf stderr "all: %d\n" (List.length all);flush_all (); *)
+(*
+    List.filter (function (_,uri) -> 
+      at_most ~dbd ~where constants uri) 
+*)
+    all 
+    in
   let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
     greater_than @ equal_to
 
@@ -617,23 +626,28 @@ let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
       let subsets = power_upto just_factor constants in
       (* let _ = prerr_endline (("subsets: ")^
         (string_of_int (List.length subsets))) in *)
-      let types_no = List.length types in
-      List.map (function (n,l) -> (n+types_no,types@l)) subsets
+      let types_no = List.length types in 
+       if types_no > 0 then  
+          List.map (function (n,l) -> (n+types_no,types@l)) subsets
+       else subsets
     in
+    prerr_endline ("critical_value exceded..." ^ string_of_int constants_no);
     let all_constants = 
      let all = match main with None -> types | Some m -> m::types in
       List.fold_right UriManagerSet.add all constants
     in
      compute_with_only ~dbd ~where main subsets all_constants
   else
+    (prerr_endline ("all subsets..." ^ string_of_int constants_no);
     let subsets = 
       let subsets = power constants in
       let types_no = List.length types in
        if types_no > 0 then  
         (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
        else subsets
-      in
-       compute_exactly ~dbd ~facts ~where main subsets
+    in
+       prerr_endline "fine1";
+       compute_exactly ~dbd ~facts ~where main subsets)
 
   (* match query wrappers *)