From 9b676d1df6d16c95e2b227c4ae0e353f6e2a308a Mon Sep 17 00:00:00 2001
From: Matteo Selmi <matteo.selmi@mail.polimi.it>
Date: Wed, 31 Mar 2004 20:21:56 +0000
Subject: [PATCH] tacticChaser modified to avoid double "apply" and to avoid to
 apply uris ".var" in tactic "auto".

---
 helm/ocaml/tactics/tacticChaser.ml | 71 ++++++++++++++++++++++++++----
 1 file changed, 62 insertions(+), 9 deletions(-)

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index a4ce74bb5..fe593a4f8 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -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
@@ -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*)
 
 (*
@@ -188,11 +240,12 @@ in
 
 
 let  searchTheorems mqi_handle ~status:(proof,goal) =
-prerr_endline "1";
+(*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() ~status:(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 ~status:(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
 ;;
 
-- 
2.39.2