Added a filter for uris in tactic "auto".

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

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index edb69bf5025ba8ea6824190d27f51f07a66bf9d9..d3ba1d2a3e1130ac9abc7e3d6a0071169fe8c2b1 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -131,21 +131,31 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
       (fun (n,u) -> 
         (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u)) 
       result in
+  (* delete all .var uris *)
   let isvar (_,s) =
     let len = String.length s in
     let suffix = String.sub s (len-4) 4 in
       not (suffix  = ".var") in
   let uris = List.filter isvar uris in
+  (* delete all not "cic:/Coq" uris *)
   let uris =
     (* TODO ristretto per ragioni di efficienza *)
-    prerr_endline "STO FILTRANDO2";
     List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
+  (* concl_cost are the costants in the conclusion of the proof 
+     while hyp_const are the constants in the hypothesis *)
+  let (_,concl_const) = NewConstraints.constants_of ty in
+  prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
+  let hyp t set =
+    match t with
+      Some (_,Cic.Decl t) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
+    | Some (_,Cic.Def (t,_)) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
+    | _ -> set in
+  let hyp_const =
+    List.fold_right hyp ey NewConstraints.StringSet.empty in
+  prerr_endline (NewConstraints.pp_StringSet (NewConstraints.StringSet.union hyp_const concl_const));
+  (* uris with new constants in the proof are filtered *)
+  let uris = List.filter (Filter_auto.filter_new_constants conn (NewConstraints.StringSet.union hyp_const concl_const)) uris in 
 (*
-  let uris =
-    (* TODO ristretto per ragioni di efficienza *)
-    prerr_endline "STO FILTRANDO2";
-    List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
-  in
   let uris =
     (* ristretto all cache *)
     prerr_endline "SOLO CACHE";
@@ -174,7 +184,8 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
      prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
      filter_out uris
    in
-    uris'
+     prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris'));
+     uris'
 ;;
 
 (*funzione che sceglie il penultimo livello di profondita' dei must*)
@@ -279,7 +290,7 @@ let  searchTheorems mqi_handle (proof,goal) =
        else l1 - l2)
     subproofs
  in
- (* now we may drop the prefix tag *)
+  (* now we may drop the prefix tag *)
  List.map snd res