From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Apr 2005 13:34:27 +0000 (+0000)
Subject: main constants set is closed with constants types
X-Git-Tag: single_binding~130
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb1c54e2c68e87998c1c9b09221b64fb63adaa7a;p=helm.git

main constants set is closed with constants types
---

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 3bc3c566e..5afd37a9a 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -236,6 +236,16 @@ 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
@@ -256,11 +266,32 @@ 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))