helm/ocaml/tactics/tacticChaser.ml

   1 (* Copyright (C) 2000-2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 18/02/2003                                 *)
  32 (*                                                                            *)
  33 (*                                                                            *)
  34 (******************************************************************************)
  35
  36 module MQI = MQueryInterpreter
  37 module MQIC = MQIConn
  38 module I = MQueryInterpreter
  39 module U = MQGUtil
  40 module G = MQueryGenerator
  41
  42   (* search arguments on which Apply tactic doesn't fail *)
  43 let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
  44  let ((_, metasenv, _, _), metano) = status in
  45  let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
  46   let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
  47 match list_of_must with
  48   [] -> []
  49 |_ ->
  50   let must = choose_must list_of_must only in
  51    prerr_endline "123";
  52   let result =
  53    I.execute mqi_handle
  54       (G.query_of_constraints
  55         (Some CGMatchConclusion.universe)
  56         (must,[],[]) (Some only,None,None)) in
  57  prerr_endline "456";
  58   let uris =
  59    List.map
  60     (function uri,_ ->
  61       MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
  62     ) result
  63   in
  64   let uris =
  65     (* TODO ristretto per ragioni di efficienza *)
  66     prerr_endline "STO FILTRANDO";
  67     List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
  68   in
  69      prerr_endline "HO FILTRATO";
  70   let uris',exc =
  71     let rec filter_out =
  72      function
  73         [] -> [],""
  74       | uri::tl ->
  75          let tl',exc = filter_out tl in
  76           try
  77            if
  78              let time = Unix.gettimeofday() in
  79             (try
  80              ignore
  81                (PrimitiveTactics.apply_tac
  82                   ~term:(MQueryMisc.term_of_cic_textual_parser_uri
  83                            (MQueryMisc.cic_textual_parser_uri_of_string uri))
  84                   status);
  85                let time1 = Unix.gettimeofday() in
  86                  prerr_endline (Printf.sprintf "%1.3f" (time1 -. time) );
  87                true
  88             with ProofEngineTypes.Fail _ ->
  89               let time1 = Unix.gettimeofday() in
  90               prerr_endline (Printf.sprintf "%1.3f" (time1 -. time)); false)
  91            then
  92             uri::tl',exc
  93            else
  94             tl',exc
  95           with
  96            (ProofEngineTypes.Fail _) as e ->
  97              let exc' =
  98               "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
  99                uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
 100              in
 101               tl',exc'
 102     in
 103      filter_out uris
 104   in
 105     let html' =
 106      " <h1>Objects that can actually be applied: </h1> " ^
 107      String.concat "<br>" uris' ^ exc ^
 108      " <h1>Number of false matches: " ^
 109       string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
 110      " <h1>Number of good matches: " ^
 111       string_of_int (List.length uris') ^ "</h1>"
 112     in
 113      output_html html' ;
 114      uris'
 115 ;;
 116
 117
 118 (*matchConclusion modificata per evitare una doppia apply*)
 119 let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
 120   let ((_, metasenv, _, _), metano) = status in
 121   let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
 122   let conn =
 123     match mqi_handle.MQIConn.pgc with
 124         MQIConn.MySQL_C conn -> conn
 125       | _ -> assert false in
 126   let result = Match_concl.cmatch conn ty in
 127   List.iter
 128     (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) result;
 129   let uris =
 130     List.map
 131       (fun (n,u) ->
 132          (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u))
 133       result in
 134   (* delete all .var uris *)
 135   let isvar (_,s) =
 136     let len = String.length s in
 137     let suffix = String.sub s (len-4) 4 in
 138       not (suffix  = ".var") in
 139   let uris = List.filter isvar uris in
 140   (* delete all not "cic:/Coq" uris *)
 141   let uris =
 142     (* TODO ristretto per ragioni di efficienza *)
 143     List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
 144   (* concl_cost are the costants in the conclusion of the proof
 145      while hyp_const are the constants in the hypothesis *)
 146   let (_,concl_const) = NewConstraints.constants_of ty in
 147   prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
 148   let hyp t set =
 149     match t with
 150       Some (_,Cic.Decl t) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
 151     | Some (_,Cic.Def (t,_)) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
 152     | _ -> set in
 153   let hyp_const =
 154     List.fold_right hyp ey NewConstraints.StringSet.empty in
 155   prerr_endline (NewConstraints.pp_StringSet (NewConstraints.StringSet.union hyp_const concl_const));
 156   (* uris with new constants in the proof are filtered *)
 157   let uris = List.filter (Filter_auto.filter_new_constants conn (NewConstraints.StringSet.union hyp_const concl_const)) uris in
 158 (*
 159   let uris =
 160     (* ristretto all cache *)
 161     prerr_endline "SOLO CACHE";
 162     List.filter
 163       (fun uri -> CicEnvironment.in_cache (UriManager.uri_of_string uri)) uris
 164   in
 165   prerr_endline "HO FILTRATO2";
 166 *)
 167   let uris' =
 168     let rec filter_out =
 169      function
 170         [] -> []
 171       | (m,uri)::tl ->
 172           let tl' = filter_out tl in
 173             try
 174               (m,
 175                (prerr_endline ("STO APPLICANDO " ^ uri);
 176                 (PrimitiveTactics.apply_tac
 177                    ~term:(MQueryMisc.term_of_cic_textual_parser_uri
 178                             (MQueryMisc.cic_textual_parser_uri_of_string uri))
 179                    status)))::tl'
 180             (* with ProofEngineTypes.Fail _ -> tl' *)
 181             (* patch to cover CSC's exportation bug *)
 182             with _ -> tl'
 183      in
 184      prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
 185      filter_out uris
 186    in
 187      prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris'));
 188      uris'
 189 ;;
 190
 191 (*funzione che sceglie il penultimo livello di profondita' dei must*)
 192
 193 (*
 194 let choose_must list_of_must only=
 195 let n = (List.length list_of_must) - 1 in
 196    List.nth list_of_must n
 197 ;;*)
 198
 199 (* questa prende solo il main *)
 200 let choose_must list_of_must only =
 201    List.nth list_of_must 0
 202
 203 (* livello 1
 204 let choose_must list_of_must only =
 205    try
 206      List.nth list_of_must 1
 207    with _ ->
 208      List.nth list_of_must 0 *)
 209
 210 (* OLD CODE: TO BE REMOVED
 211 (*Funzione position prende una lista e un elemento e mi ritorna la posizione dell'elem nella lista*)
 212 (*Mi serve per ritornare la posizione del teo che produce meno subgoal*)
 213
 214 exception NotInTheList;;
 215
 216
 217 let position n =
 218         let rec aux k =
 219          function
 220              [] -> raise NotInTheList
 221             | m::_ when m=n -> k
 222             | _::tl -> aux (k+1) tl in
 223         aux 1
 224 ;;
 225
 226
 227
 228 (*function taking a status and returning a new status after having searching a theorem to apply ,theorem which *)
 229 (*generate the less number of subgoals*)
 230
 231 let  searchTheorem (proof,goal) =
 232   let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
 233   in
 234     let mqi_handle = MQIC.init mqi_flags prerr_string
 235 in
 236   let uris' =
 237     matchConclusion
 238       mqi_handle ~choose_must() (proof, goal)
 239   in
 240   let list_of_termin =
 241     List.map
 242     (function string ->
 243     (MQueryMisc.term_of_cic_textual_parser_uri
 244     (MQueryMisc.cic_textual_parser_uri_of_string string))
 245     )
 246     uris'
 247   in
 248   let list_proofgoal =
 249     List.map
 250     (function term ->
 251       PrimitiveTactics.apply_tac ~term (proof,goal))
 252     list_of_termin
 253   in
 254   let (list_of_subgoal: int  list list) =
 255   List.map  snd list_proofgoal
 256   in
 257   let list_of_num =
 258   List.map List.length list_of_subgoal
 259   in
 260   let list_sort =
 261   List.sort Pervasives.compare list_of_num
 262   in                                   (*ordino la lista in modo cresc*)
 263   let min= List.nth  list_sort 0   (*prendo il minimo*)
 264   in
 265   let uri' =              (*cerco il teo di pos k*)
 266   List.nth list_of_termin (position  min list_of_num)
 267   in
 268   (* let teo=
 269     String.sub uri' 4 (String.length uri' - 4)
 270
 271   (* modifico la str in modo che sia accettata da apply*)
 272   in*)
 273   PrimitiveTactics.apply_tac ~term:uri' (proof,goal)
 274 ;;
 275 *)
 276
 277
 278 let  searchTheorems mqi_handle (proof,goal) =
 279 (*prerr_endline "1";*)
 280   let subproofs =
 281     matchConclusion2 mqi_handle ~choose_must() (proof, goal) in
 282  let res =
 283   List.sort
 284     (fun (n1,(_,gl1)) (n2,(_,gl2)) ->
 285        let l1 = List.length gl1 in
 286        let l2 = List.length gl2 in
 287        (* if the list of subgoals have the same lenght we use the
 288           prefix tag, where higher tags have precedence *)
 289        if l1 = l2 then n2 - n1
 290        else l1 - l2)
 291     subproofs
 292  in
 293   (* now we may drop the prefix tag *)
 294  List.map snd res
 295
 296
 297 ;;
 298