X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.ml;h=5851b1467e9e583863c9258d658fedc2d58cb52d;hb=22f61c7bd18cd3652e886f6a765aab63eacac83c;hp=76a58091da7899dea84f55847538e6c383b16db9;hpb=a8f512296b650595549fe3e125930657d20bb99c;p=helm.git

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 76a58091d..5851b1467 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -33,74 +33,237 @@
 (*                                                                            *)
 (******************************************************************************)
 
+module MQI = MQueryInterpreter
+module MQIC = MQIConn
+module I = MQueryInterpreter
+module U = MQGUtil
+module G = MQueryGenerator
+
   (* search arguments on which Apply tactic doesn't fail *)
-let searchPattern 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) = List.find (function (m,_,_) -> m=metano) metasenv in
-  let list_of_must,only = MQueryLevels.out_restr metasenv ey ty 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 torigth_restriction (u,b) =
-   let p =
-    if b then
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" 
-    else
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
+   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,_ ->
+      MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
+    ) result
+  in
+  let uris =
+    (* TODO ristretto per ragioni di efficienza *)
+    prerr_endline "STO FILTRANDO";
+    List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
+  in
+     prerr_endline "HO FILTRATO";
+  let uris',exc =
+    let rec filter_out =
+     function
+        [] -> [],""
+      | uri::tl ->
+         let tl',exc = filter_out tl in
+          try
+           if
+            (try
+             ignore
+              (PrimitiveTactics.apply_tac
+               ~term:(MQueryMisc.term_of_cic_textual_parser_uri
+                (MQueryMisc.cic_textual_parser_uri_of_string uri))
+               status);
+             true
+            with ProofEngineTypes.Fail _ -> false)
+           then
+            uri::tl',exc
+           else
+            tl',exc
+          with
+           (ProofEngineTypes.Fail _) as e ->
+             let exc' =
+              "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
+               uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
+             in
+              tl',exc'
     in
-    (u,p,None)
+     filter_out uris
   in
-  let rigth_must = List.map torigth_restriction must in
-  let rigth_only = Some (List.map torigth_restriction only) in
+    let html' =
+     " <h1>Objects that can actually be applied: </h1> " ^
+     String.concat "<br>" uris' ^ exc ^
+     " <h1>Number of false matches: " ^
+      string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
+     " <h1>Number of good matches: " ^
+      string_of_int (List.length uris') ^ "</h1>"
+    in
+     output_html html' ;
+     uris'
+;;
+
+
+(*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 =
-	 MQueryInterpreter.execute mqi_handle 
-	    (MQueryGenerator.query_of_constraints
-        (Some
-          ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
-           "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"])
-        (rigth_must,[],[]) (rigth_only,None,None)) in 
-	let uris =
-	 List.map
-		(function uri,_ ->
-			MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
-		) result in
-	 let uris',exc =
-		let rec filter_out =
-		 function
-				[] -> [],""
-			| uri::tl ->
-				 let tl',exc = filter_out tl in
-					try
-					 if
-						(try
-						 ignore
-							(PrimitiveTactics.apply_tac
-							 ~term:(MQueryMisc.term_of_cic_textual_parser_uri
-								(MQueryMisc.cic_textual_parser_uri_of_string uri))
-							 ~status);
-						 true
-						with ProofEngineTypes.Fail _ -> false)
-					 then
-						uri::tl',exc
-					 else
-						tl',exc
-					with
-           (ProofEngineTypes.Fail _) as e ->
-						 let exc' =
-						  "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
-							 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
-						 in
-						  tl',exc'
-		in
-		 filter_out uris
-	 in
-		let html' =
-		 " <h1>Objects that can actually be applied: </h1> " ^
-		 String.concat "<br>" uris' ^ exc ^
-		 " <h1>Number of false matches: " ^
-			string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
-		 " <h1>Number of good matches: " ^
-			string_of_int (List.length uris') ^ "</h1>"
-		in
-		 output_html html' ;
-		 uris'
+   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*)
+
+(*
+let choose_must list_of_must only=
+let n = (List.length list_of_must) - 1 in
+   List.nth list_of_must n
+;;*)
+
+let choose_must list_of_must only =
+   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 uris' =
+    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
+         (MQueryMisc.cic_textual_parser_uri_of_string string)))
+    uris' in
+prerr_endline "3";
+  let list_proofgoal =
+    List.map
+      (function term ->
+         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)) 
+    uris'
+    in
+(*prerr_endline "5";*)
+res
 ;;