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 d3ba1d2a3e1130ac9abc7e3d6a0071169fe8c2b1..689102fe2439c982d94f756087375c2da6116c2e 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -124,8 +124,10 @@ 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) -> 
@@ -140,7 +142,7 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
   (* delete all not "cic:/Coq" uris *)
   let uris =
     (* TODO ristretto per ragioni di efficienza *)
-    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
@@ -207,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 =
@@ -292,7 +226,5 @@ let  searchTheorems mqi_handle (proof,goal) =
  in
   (* now we may drop the prefix tag *)
  List.map snd res
- 
-
 ;;