X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.ml;h=de356a3d1f52860237a9582bb57b0ddc991e271f;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=831ccc6f4bedaf2cc4f32d77f4067aa25486948b;hpb=6c3a5a7adc3f37ddfb99a69b050fbf324e95e583;p=helm.git

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 831ccc6f4..de356a3d1 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,22 +121,11 @@ 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
-    let suffix = String.sub s (len-4) 4 in
-      not (suffix  = ".var") in
-  let uris = List.filter isvar uris in 
+  let uris = List.filter UriManager.is_var uris in 
   (* delete all not "cic:/Coq" uris *)
   (*
   let uris =
@@ -146,7 +135,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 +160,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 +173,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
@@ -239,21 +234,24 @@ let  searchTheorems mqi_handle (proof,goal) =
 (*
    prerr_endline "PRIMA DELLA PRIMA TYPE OF " ;
 *)
-   let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
+   let ty_sort1,u = (*TASSI: FIXME *)
+     CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph in
 (*
    prerr_endline (Printf.sprintf "PRIMA DELLA SECONDA TYPE OF %s \n### %s @@@%s " (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppcontext [] ey2) (CicMetaSubst.ppterm [] ty2));
 *)
-   let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 in
+   let ty_sort2,u1 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 u in
 (*
    prerr_endline "DOPO LA SECONDA TYPE OF " ;
 *)
-   let prop1 = if CicReduction.are_convertible 
-	 	   ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0
-		 else 1 in
-   let prop2 = if CicReduction.are_convertible 
-	 	   ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0
-		 else 1 in
- prop1 - prop2 in
- List.map (fun (level,(proof,goallist)) -> (proof, (List.stable_sort (order_goal_list proof) goallist))) res  
+   let b,u2 = 
+     CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 u1 in
+   let prop1 = if b then 0 else 1 in
+   let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 u2 in
+   let prop2 = if b then 0 else 1 in
+     prop1 - prop2 in
+   List.map (
+     fun (level,(proof,goallist)) -> 
+       (proof, (List.stable_sort (order_goal_list proof) goallist))
+   ) res  
 ;;