New implementation of experimental_hint/auto (called new_experimental_hint) that

[helm.git] / helm / ocaml / metadata / metadataConstraints.ml

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index 74b15015ce9dc5750d7378238f0c015faad19888..d18663fadcaea3998f1267915967827c0ce83611 100644 (file)
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -350,7 +350,9 @@ and signature_concl =
     | Cic.Meta _                     
     | Cic.Sort _ 
     | Cic.Implicit _ -> UriManagerSet.empty 
-    | Cic.Var (u,exp_named_subst) -> UriManagerSet.empty
+    | Cic.Var (u,exp_named_subst) ->
+       (*CSC: TODO if the var has a body it must be processed *)
+       UriManagerSet.empty
     | Cic.Const (u,exp_named_subst) -> 
         UriManagerSet.singleton u
     | Cic.MutInd (u, t, exp_named_subst) -> 
@@ -421,8 +423,12 @@ let must_of_prefix ?(where = `Conclusion) m s =
     | `Conclusion -> [`InConclusion]
     | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
   in
+  let positions =
+   if m = None then `MainConclusion None :: positions else positions in
   let s' = List.map (fun (u:UriManager.uri) -> `Obj (u, positions)) s in
-  `Obj (m, [`MainConclusion None]) :: s'
+   match m with
+      None -> s'
+    | Some m -> `Obj (m, [`MainConclusion None]) :: s'
 
 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
 
@@ -477,17 +483,29 @@ let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
   List.concat
     (List.map 
       (fun (m,s) -> 
-        if ((m = 0) && (UriManager.eq main (UriManager.uri_of_string (HelmLibraryObjects.Logic.eq_XURI)))) then
+        let is_eq,card =
+         match main with
+            None -> false,m
+          | Some main ->
+             (m = 0 &&
+              UriManager.eq main
+               (UriManager.uri_of_string (HelmLibraryObjects.Logic.eq_XURI))),
+             m+1
+        in
+        if m = 0 && is_eq then
           (if facts then myspeciallist_of_facts
           else myspeciallist)
         else
           let res =
+           (* this gets rid of the ~750 objects of type Set/Prop/Type *)
+           if card = 0 then []
+           else
             let must = must_of_prefix ~where main s in
             match where with
-            | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
-            | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
+            | `Conclusion -> at_least ~dbd ~concl_card:(Eq card) must
+            | `Statement -> at_least ~dbd ~full_card:(Eq card) must
           in
-          List.map (fun uri -> (m, uri)) res)
+          List.map (fun uri -> (card, uri)) res)
       prefixes)
 
   (* critical value reached, fallback to "only" constraints *)
@@ -510,14 +528,15 @@ let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion)
       union
         (List.map 
           (fun (m,s) -> 
+            let card = if main = None then m else m + 1 in
             let must = must_of_prefix ~where main s in
             (let res = 
               match where with
-              | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
-              | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
+              | `Conclusion -> at_least ~dbd ~concl_card:(Gt card) must
+              | `Statement -> at_least ~dbd ~full_card:(Gt card) must
             in
             (* we tag the uri with m+1, for sorting purposes *)
-            List.map (fun uri -> (m+1, uri)) res))
+            List.map (fun uri -> (card, uri)) res))
           maximal_prefixes)
     in
     List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
@@ -541,7 +560,7 @@ let cmatch ~(dbd:Mysql.dbd)  ?(facts=false) t =
             let all_constants = 
               List.fold_right UriManagerSet.add types (UriManagerSet.add main constants)
             in
-            compute_with_only ~dbd ~facts main all_concl all_constants
+            compute_with_only ~dbd ~facts (Some main) all_concl all_constants
          | _, _ -> [])
       else
         (* in this case we compute all prefixes, and we do not need
@@ -557,15 +576,7 @@ let cmatch ~(dbd:Mysql.dbd)  ?(facts=false) t =
         in
         (match prefixes with
            Some main, all_concl ->
-            compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl
-(*
-             List.concat
-               (List.map 
-                  (fun (m,s) -> 
-                    let must = must_of_prefix ~where:`Conclusion main s in
-                    let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
-                    List.map (fun uri -> (m, uri)) res)
-                  all_concl) *)
+           compute_exactly ~dbd ~facts ~where:`Conclusion (Some main) all_concl
          | _, _ -> [])
 
 let power_upto upto consts =
@@ -586,31 +597,35 @@ let power consts =
 
 type where = [ `Conclusion | `Statement ]
 
-let sigmatch ~(dbd:Mysql.dbd) 
-  ?(facts=false) ?(where = `Conclusion) (main, constants) =
-  match main with
-    None -> []
-  | Some (main, types) ->
-      let constants_no = UriManagerSet.cardinal constants in
-      if (constants_no > critical_value) then 
-        let subsets = 
-          let subsets = power_upto just_factor constants in
-          let types_no = List.length types in
-          List.map (function (n,l) -> (n+types_no,types@l)) subsets
-        in
-        let all_constants = 
-          List.fold_right UriManagerSet.add types (UriManagerSet.add main constants)
-        in
-        compute_with_only ~dbd ~where main subsets all_constants
-      else
-        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
+let sigmatch ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion)
+ (main, constants)
+=
+ let main,types =
+   match main with
+     None -> None,[]
+   | Some (main, types) -> Some main,types
+ in
+  let constants_no = UriManagerSet.cardinal constants in
+  if (constants_no > critical_value) then 
+    let subsets = 
+      let subsets = power_upto just_factor constants in
+      let types_no = List.length types in
+      List.map (function (n,l) -> (n+types_no,types@l)) subsets
+    in
+    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
+    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
 
   (* match query wrappers *)