First version of instance.

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 0e86d8ccecf56b8a9005cec598b0e5d585cd875b..49472ed7204f084cb160ac9fdb46378eae334b48 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -100,7 +100,7 @@ let match_term ~(dbd:Mysql.dbd) ty =
       None, diff
   in
   let constraints = List.map MetadataTypes.constr_of_metadata metadata in
-  Constr.at_least ~dbd ?full_card ?diff constraints
+    Constr.at_least ~dbd ?full_card ?diff constraints
 
 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
 
@@ -236,17 +236,38 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
     The cose is a cut and paste of the previous one: at the end 
     of the experimentation we shall make a choice. *)
 
+let close_with_types s metasenv context =
+  Constr.StringSet.fold 
+    (fun e bag -> 
+      let t = CicUtil.term_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)) 
+    s s
+
 let experimental_hint 
   ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let (_, metasenv, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+  let uris = 
+    if facts then
+      ["cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
+    else
+      ["cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
+       (* "cic:/Coq/Init/Logic/trans_eq.con"; *)
+       "cic:/Coq/Init/Logic/f_equal.con";
+       "cic:/Coq/Init/Logic/f_equal2.con";
+       "cic:/Coq/Init/Logic/f_equal3.con"] 
+  in
+  (* 
   let (uris, (main, sig_constants)) =
     match signature with
     | Some signature -> 
        (Constr.sigmatch ~dbd ~facts signature, signature)
     | None -> 
        (Constr.cmatch' ~dbd ~facts ty, Constr.signature_of ty)
-  in
+  in 
   let uris = List.filter nonvar (List.map snd uris) in
   let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
   let types_constants =
@@ -256,11 +277,33 @@ let experimental_hint
         List.fold_right Constr.StringSet.add (main :: types)
           Constr.StringSet.empty
   in
-  let hyp_constants =
-    Constr.StringSet.diff (signature_of_hypothesis context) types_constants
+  let all_constants =
+    let hyp_and_sug =
+      Constr.StringSet.union
+        (signature_of_hypothesis context) 
+        sig_constants
+    in
+    let main = 
+      match main with
+      | None -> Constr.StringSet.empty
+      | Some (main,_) -> 
+          let ty, _ = 
+            CicTypeChecker.type_of_aux' 
+              metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
+          in
+          Constr.constants_of ty
+    in
+    Constr.StringSet.union main hyp_and_sug
   in
 (* Constr.StringSet.iter prerr_endline hyp_constants; *)
-  let other_constants = Constr.StringSet.union sig_constants hyp_constants in
+  let all_constants_closed = close_with_types all_constants metasenv context in
+  let other_constants = 
+    Constr.StringSet.diff all_constants_closed types_constants
+  in
+  prerr_endline "all_constants_closed";
+  Constr.StringSet.iter prerr_endline all_constants_closed;
+  prerr_endline "other_constants";
+  Constr.StringSet.iter prerr_endline other_constants;
   let uris = 
     let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
     if ((List.length uris < pow) or (pow <= 0))
@@ -269,7 +312,7 @@ let experimental_hint
       filter_uris_forward ~dbd (main, other_constants) uris
     end else
       filter_uris_backward ~dbd ~facts (main, other_constants) uris
-  in
+  in *)
   let rec aux = function
     | [] -> []
     | uri :: tl ->
@@ -304,5 +347,34 @@ let elim ~dbd uri =
      `Obj (uri,[`InHypothesis]);
     ]
   in
-  MetadataConstraints.at_least ~dbd constraints
+  MetadataConstraints.at_least ~rating:`Hits ~dbd constraints
+
+
+let fill_with_dummy_constants t =
+  let rec aux i =
+    function
+       Cic.Lambda (n,s,t) -> 
+         let dummy_uri = 
+           UriManager.uri_of_string ("dummy_"^(string_of_int i)) in
+         (aux (i+1) (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
+      | t -> t
+  in aux 0 t
+      
+let instance ~dbd t =
+  let t' = fill_with_dummy_constants t in 
+  let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
+  let no_concl = MetadataDb.count_distinct `Conclusion metadata in
+  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 5) = "dummy" 
+       | _ -> false in
+  let metadata = List.filter is_dummy metadata in
+  let constraints = List.map MetadataTypes.constr_of_metadata metadata in
+  let concl_card = Some (MetadataConstraints.Eq no_concl) in
+  let full_card = Some (MetadataConstraints.Eq no_full) in
+  let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
+  Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints
+