From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 1 Sep 2004 07:24:22 +0000 (+0000)
Subject: Bug fixing: the call to MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
X-Git-Tag: moogle_mathql~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=584455a9f581cd2f0fa76a6720c5749b083db8bf;p=helm.git

Bug fixing: the call to MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
must be done after filter_new_constants (that compares uris).
---

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 831ccc6f4..2235670a0 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -23,15 +23,15 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 18/02/2003                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
+(*****************************************************************************)
+(*                                                                           *)
+(*                               PROJECT HELM                                *)
+(*                                                                           *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>              *)
+(*                                 18/02/2003                                *)
+(*                                                                           *)
+(*                                                                           *)
+(*****************************************************************************)
 
 module MQI = MQueryInterpreter
 module MQIC = MQIConn
@@ -121,16 +121,9 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
     match mqi_handle.MQIConn.pgc with
 	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
+  let uris = Match_concl.cmatch conn ty in
+  (* List.iter 
+    (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) uris; *)
   (* delete all .var uris *)
   let isvar (_,s) =
     let len = String.length s in
@@ -146,7 +139,7 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
   (* concl_cost are the costants in the conclusion of the proof 
      while hyp_const are the constants in the hypothesis *)
   let (main_concl,concl_const) = NewConstraints.mainandcons ty in
-  prerr_endline ("Ne sono rimasti 1 " ^ string_of_int (List.length uris));
+  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))
@@ -171,6 +164,11 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
   in 
   prerr_endline "HO FILTRATO2";
 *)
+  let uris =
+    List.map
+      (fun (n,u) -> 
+	 (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u)) 
+      uris in
   let uris' =
     let rec filter_out =
      function
@@ -179,14 +177,15 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
           let tl' = filter_out tl in
             try
 	           prerr_endline ("STO APPLICANDO " ^ uri);
-              (m,
+              let res = (m,
 		(ProofEngineTypes.apply_tactic( PrimitiveTactics.apply_tac
 		   ~term:(MQueryMisc.term_of_cic_textual_parser_uri
 			    (MQueryMisc.cic_textual_parser_uri_of_string uri)))
-		   status))::tl'
+		   status))::tl' in
+		prerr_endline ("OK");res
             (* with ProofEngineTypes.Fail _ -> tl' *)
             (* patch to cover CSC's exportation bug *)
-            with _ -> tl' 
+            with _ -> prerr_endline ("FAIL");tl' 
      in    
      prerr_endline ("Ne sono rimasti 2 " ^ string_of_int (List.length uris));
      filter_out uris