Bug in the management of substitutions into auto corrected.

No significative loss in performance.
Comments commented.

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index bc999166482d2a1c9c763e52b573e0cc93656f09..ce700f2de5091c9f7532570453cc10401d4c62d6 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -54,7 +54,6 @@ let search_theorems_in_context status =
   let module S = CicSubstitution in
   let module PET = ProofEngineTypes in 
   let module PT = PrimitiveTactics in 
-  prerr_endline "Entro in search_context";
   let _,metasenv,_,_ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
   let rec find n = function 
@@ -76,7 +75,7 @@ let search_theorems_in_context status =
     []
 ;;     
 
-let depth = 4;;
+let depth = 6;;
 
 let new_search_theorems f proof goal depth gtl sign =
   let choices = f (proof,goal)
@@ -105,9 +104,11 @@ let rec auto dbd = function
       match meta_inf with
          Some (ey, ty) ->
             (* the goal is still there *)
+            (* 
            prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
            prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
            prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
+            *)
             (* if the goal contains metavariables we use the input
                signature for at_most constraints *)
             let is_meta_closed = CicUtil.is_meta_closed ty in
@@ -189,7 +190,6 @@ let search_theorems_in_context status =
   let module S = CicSubstitution in
   let module PET = ProofEngineTypes in 
   let module PT = PrimitiveTactics in 
-  prerr_endline "Entro in search_context";
   let _,metasenv,_,_ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
   let rec find n = function 
@@ -210,12 +210,13 @@ let search_theorems_in_context status =
     []
 ;;     
 
-let new_search_theorems f proof goal depth gtl sign =
+let new_search_theorems f proof goal depth subst sign =
   let choices = f (proof,goal)
   in 
   List.map 
-    (function (subst,(proof, goallist)) ->
-       (subst,(proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign)))
+    (function (local_subst,(proof, goallist)) ->
+       let new_subst t= local_subst (subst t) in
+       (new_subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
     choices 
 ;;
 
@@ -243,8 +244,10 @@ let rec auto_new dbd = function
            begin
             match exitus with
                Yes (bo,_) ->
+                  (*
                   prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
                  prerr_endline (CicPp.ppterm ty);
+                  *)
                   let subst_in =
                     (* if we just apply the subtitution, the type 
                        is irrelevant: we may use Implicit, since it will 
@@ -257,13 +260,18 @@ let rec auto_new dbd = function
                   let new_subst t = (subst_in (subst t)) in
                  auto_new dbd ((new_subst,(proof,gtl,sign))::tl)
               | No d when (d >= depth) -> 
+                  (*
                  prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
+                  *)
                  auto_new dbd tl
+               
              | No _ 
              | NotYetInspected -> 
+                  (*
                  prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
                  prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
                  prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
+                  *)
                  let sign, new_sign =
                    if is_meta_closed then
                      None, Some (MetadataConstraints.signature_of ty)
@@ -271,14 +279,14 @@ let rec auto_new dbd = function
                  let local_choices =
                    new_search_theorems 
                      search_theorems_in_context 
-                     proof goal (depth-1) [] new_sign in
+                     proof goal (depth-1) subst new_sign in
                  let global_choices =
                    new_search_theorems 
                      (fun status -> 
                         List.map snd 
                         (MetadataQuery.experimental_hint 
                            ~dbd ~facts:facts ?signature:sign status))
-                     proof goal (depth-1) [] new_sign in
+                     proof goal (depth-1) subst new_sign in
                  let all_choices =
                    local_choices@global_choices in
                  (match (auto_new dbd all_choices) 
@@ -288,7 +296,7 @@ let rec auto_new dbd = function
                            hastable *)
                         Hashtbl.add inspected_goals ty (No depth);
                         auto_new dbd tl
-                    | (local_subst,(proof,[],_))::tl1 -> 
+                    | (new_subst,(proof,[],_))::tl1 -> 
                         (* a proof for goal has been found:
                            in order to get the proof we apply subst to
                            Meta[goal] *)
@@ -297,11 +305,10 @@ let rec auto_new dbd = function
                             let irl = 
                               CicMkImplicit.identity_relocation_list_for_metavariable ey in
                             let meta_proof = 
-                              local_subst (Cic.Meta(goal,irl)) in
+                              new_subst (Cic.Meta(goal,irl)) in
                               Hashtbl.add inspected_goals 
                                 ty (Yes (meta_proof,depth));
                           end;
-                        let new_subst t = (local_subst (subst t)) in
                         let all_choices =
                           let gtl' = List.map fst gtl in
                             if (gtl = [] || is_meta_closed) then 

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index bb5594a35693f50917f86516419df44858e373b0..e5656b9b3f9aaa80e9e68c2b1169cad747ff7958 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -126,7 +126,6 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let hyp_constants =
     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
   in
-prerr_endline "HYP SIGNATURE";
 Constr.StringSet.iter prerr_endline hyp_constants;
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
@@ -144,7 +143,7 @@ Constr.StringSet.iter prerr_endline hyp_constants;
         (let status' =
             try
               let (proof, goal_list) =
-                prerr_endline ("STO APPLICANDO " ^ uri);
+(*                prerr_endline ("STO APPLICANDO " ^ uri); *)
                PET.apply_tactic
                   (PrimitiveTactics.apply_tac
                    ~term:(CicUtil.term_of_uri uri))
@@ -198,7 +197,6 @@ let experimental_hint
   let hyp_constants =
     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
   in
-prerr_endline "HYP SIGNATURE";
 Constr.StringSet.iter prerr_endline hyp_constants;
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
@@ -216,7 +214,7 @@ Constr.StringSet.iter prerr_endline hyp_constants;
         (let status' =
             try
               let (subst,(proof, goal_list)) =
-                  prerr_endline ("STO APPLICANDO" ^ uri);
+                  (* prerr_endline ("STO APPLICANDO" ^ uri); *)
                   PrimitiveTactics.apply_tac_verbose 
                    ~term:(CicUtil.term_of_uri uri)
                   status