X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.ml;h=5851b1467e9e583863c9258d658fedc2d58cb52d;hb=3f00169098f1cd1cdecbbf20982f7c4c58f7d71d;hp=a4ce74bb51a118256452907dcd71758c7b22d369;hpb=f654787b2156ede958a1d35ca8daf239de1b7b89;p=helm.git

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index a4ce74bb5..5851b1467 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -40,7 +40,7 @@ module U = MQGUtil
 module G = MQueryGenerator
 
   (* search arguments on which Apply tactic doesn't fail *)
-let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() ~status =
+let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
  let ((_, metasenv, _, _), metano) = status in
  let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
   let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
@@ -48,11 +48,13 @@ match list_of_must with
   [] -> []
 |_ ->
   let must = choose_must list_of_must only in
+   prerr_endline "123";
   let result =
    I.execute mqi_handle 
       (G.query_of_constraints
         (Some CGMatchConclusion.universe)
         (must,[],[]) (Some only,None,None)) in 
+ prerr_endline "456";
   let uris =
    List.map
     (function uri,_ ->
@@ -64,7 +66,7 @@ match list_of_must with
     prerr_endline "STO FILTRANDO";
     List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
   in
-  prerr_endline "HO FILTRATO";
+     prerr_endline "HO FILTRATO";
   let uris',exc =
     let rec filter_out =
      function
@@ -78,7 +80,7 @@ match list_of_must with
               (PrimitiveTactics.apply_tac
                ~term:(MQueryMisc.term_of_cic_textual_parser_uri
                 (MQueryMisc.cic_textual_parser_uri_of_string uri))
-               ~status);
+               status);
              true
             with ProofEngineTypes.Fail _ -> false)
            then
@@ -108,6 +110,56 @@ match list_of_must with
 ;;
 
 
+(*matchConclusion modificata per evitare una doppia apply*)
+let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
+ let ((_, metasenv, _, _), metano) = status in
+ let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
+  let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
+match list_of_must with
+  [] -> []
+|_ ->
+  let must = choose_must list_of_must only in
+  let result =
+   I.execute mqi_handle 
+      (G.query_of_constraints
+        (Some CGMatchConclusion.universe)
+        (must,[],[]) (Some only,None,None)) in 
+  let uris =
+   List.map
+    (function uri,_ ->
+      MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
+    ) result
+  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 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
+  prerr_endline "HO FILTRATO2";
+  let uris' =
+    let rec filter_out =
+     function
+        [] -> []
+      | uri::tl ->
+         let tl' = filter_out tl in
+           try
+              ((PrimitiveTactics.apply_tac
+               ~term:(MQueryMisc.term_of_cic_textual_parser_uri
+                (MQueryMisc.cic_textual_parser_uri_of_string uri))
+               status)::tl')
+            with ProofEngineTypes.Fail _ -> tl'
+     in    
+     prerr_endline (string_of_int (List.length uris));
+     filter_out uris
+   in
+    uris'
+;;
+
 (*funzione che sceglie il penultimo livello di profondita' dei must*)
 
 (*
@@ -140,14 +192,14 @@ let position n =
 (*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 ~status:(proof,goal) =
+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() ~status:(proof, goal)
+      mqi_handle ~choose_must() (proof, goal)
   in
   let list_of_termin =
     List.map
@@ -160,7 +212,7 @@ in
   let list_proofgoal =
     List.map
     (function term ->
-      PrimitiveTactics.apply_tac ~term ~status:(proof,goal))
+      PrimitiveTactics.apply_tac ~term (proof,goal))
     list_of_termin
   in
   let (list_of_subgoal: int  list list) =
@@ -182,17 +234,18 @@ in
 
   (* modifico la str in modo che sia accettata da apply*)
   in*)
-  PrimitiveTactics.apply_tac ~term:uri' ~status:(proof,goal)
+  PrimitiveTactics.apply_tac ~term:uri' (proof,goal)
 ;;
 *)
 
 
-let  searchTheorems mqi_handle ~status:(proof,goal) =
-prerr_endline "1";
+let  searchTheorems mqi_handle (proof,goal) =
+(*prerr_endline "1";*)
   let uris' =
-    matchConclusion mqi_handle ~choose_must() ~status:(proof, goal) in
-prerr_endline "2";
-  let list_of_termin =
+    matchConclusion2 mqi_handle ~choose_must() (proof, goal) in
+prerr_endline (string_of_int (List.length uris'));
+(*prerr_endline "2";*)
+(*  let list_of_termin =
     List.map
       (function string ->
          (MQueryMisc.term_of_cic_textual_parser_uri
@@ -202,15 +255,15 @@ prerr_endline "3";
   let list_proofgoal =
     List.map
       (function term ->
-         PrimitiveTactics.apply_tac ~term ~status:(proof,goal)) list_of_termin in
-prerr_endline "4";
+         PrimitiveTactics.apply_tac ~term (proof,goal)) list_of_termin in*)
+(*prerr_endline "4";*)
 let res =
   List.sort 
     (fun (_,gl1) (_,gl2) -> 
         Pervasives.compare (List.length gl1) (List.length gl2)) 
-    list_proofgoal
+    uris'
     in
-prerr_endline "5";
+(*prerr_endline "5";*)
 res
 ;;