Nuova implementazione di Auto "breadth-first".

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

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index edb69bf5025ba8ea6824190d27f51f07a66bf9d9..689102fe2439c982d94f756087375c2da6116c2e 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -124,28 +124,40 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
        MQIConn.MySQL_C conn -> conn
       | _ -> assert false in
   let result = Match_concl.cmatch conn ty in
+  (* Stampa il risultato della query 
   List.iter 
     (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) result;
+  *)
   let uris =
     List.map
       (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
+    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 +186,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*)
@@ -196,74 +209,6 @@ let choose_must list_of_must only =
    with _ -> 
      List.nth list_of_must 0 *)
 
-(* OLD CODE: TO BE REMOVED
-(*Funzione position prende una lista e un elemento e mi ritorna la posizione dell'elem nella lista*)
-(*Mi serve per ritornare la posizione del teo che produce meno subgoal*)
-
-exception NotInTheList;;
-
-
-let position n =
-        let rec aux k =
-         function
-             [] -> raise NotInTheList
-            | m::_ when m=n -> k
-            | _::tl -> aux (k+1) tl in
-        aux 1
-;;
-
-
-
-(*function taking a status and returning a new status after having searching a theorem to apply ,theorem which *)
-(*generate the less number of subgoals*)
-
-let  searchTheorem (proof,goal) =
-  let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
-  in
-    let mqi_handle = MQIC.init mqi_flags prerr_string
-in
-  let uris' =
-    matchConclusion
-      mqi_handle ~choose_must() (proof, goal)
-  in
-  let list_of_termin =
-    List.map
-    (function string ->
-    (MQueryMisc.term_of_cic_textual_parser_uri
-    (MQueryMisc.cic_textual_parser_uri_of_string string))
-    )
-    uris'
-  in
-  let list_proofgoal =
-    List.map
-    (function term ->
-      PrimitiveTactics.apply_tac ~term (proof,goal))
-    list_of_termin
-  in
-  let (list_of_subgoal: int  list list) =
-  List.map  snd list_proofgoal
-  in
-  let list_of_num =
-  List.map List.length list_of_subgoal
-  in
-  let list_sort =
-  List.sort Pervasives.compare list_of_num
-  in                                   (*ordino la lista in modo cresc*)
-  let min= List.nth  list_sort 0   (*prendo il minimo*)
-  in
-  let uri' =              (*cerco il teo di pos k*)
-  List.nth list_of_termin (position  min list_of_num)
-  in
-  (* let teo=
-    String.sub uri' 4 (String.length uri' - 4)
-
-  (* modifico la str in modo che sia accettata da apply*)
-  in*)
-  PrimitiveTactics.apply_tac ~term:uri' (proof,goal)
-;;
-*)
-
-
 let  searchTheorems mqi_handle (proof,goal) =
 (*prerr_endline "1";*)
   let subproofs =
@@ -279,9 +224,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
- 
-
 ;;