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             (try
  79              ignore
  80               (PrimitiveTactics.apply_tac
  81                ~term:(MQueryMisc.term_of_cic_textual_parser_uri
  82                 (MQueryMisc.cic_textual_parser_uri_of_string uri))
  83                status);
  84              true
  85             with ProofEngineTypes.Fail _ -> false)
  86            then
  87             uri::tl',exc
  88            else
  89             tl',exc
  90           with
  91            (ProofEngineTypes.Fail _) as e ->
  92              let exc' =
  93               "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
  94                uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
  95              in
  96               tl',exc'
  97     in
  98      filter_out uris
  99   in
 100     let html' =
 101      " <h1>Objects that can actually be applied: </h1> " ^
 102      String.concat "<br>" uris' ^ exc ^
 103      " <h1>Number of false matches: " ^
 104       string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
 105      " <h1>Number of good matches: " ^
 106       string_of_int (List.length uris') ^ "</h1>"
 107     in
 108      output_html html' ;
 109      uris'
 110 ;;
 111
 112
 113 (*matchConclusion modificata per evitare una doppia apply*)
 114 let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
 115  let ((_, metasenv, _, _), metano) = status in
 116  let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
 117   let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
 118 match list_of_must with
 119   [] -> []
 120 |_ ->
 121   let must = choose_must list_of_must only in
 122   let result =
 123    I.execute mqi_handle
 124       (G.query_of_constraints
 125         (Some CGMatchConclusion.universe)
 126         (must,[],[]) (Some only,None,None)) in
 127   let uris =
 128    List.map
 129     (function uri,_ ->
 130       MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
 131     ) result
 132   in
 133   let uris =
 134     (* TODO ristretto per ragioni di efficienza *)
 135     prerr_endline "STO FILTRANDO2";
 136     List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
 137   in
 138   let isvar s =
 139       let len = String.length s in
 140       let suffix = String.sub s (len-4) 4 in
 141       not (suffix  = ".var") in
 142    let uris = List.filter isvar uris in
 143   prerr_endline "HO FILTRATO2";
 144   let uris' =
 145     let rec filter_out =
 146      function
 147         [] -> []
 148       | uri::tl ->
 149          let tl' = filter_out tl in
 150            try
 151               ((PrimitiveTactics.apply_tac
 152                ~term:(MQueryMisc.term_of_cic_textual_parser_uri
 153                 (MQueryMisc.cic_textual_parser_uri_of_string uri))
 154                status)::tl')
 155             with ProofEngineTypes.Fail _ -> tl'
 156      in
 157      prerr_endline (string_of_int (List.length uris));
 158      filter_out uris
 159    in
 160     uris'
 161 ;;
 162
 163 (*funzione che sceglie il penultimo livello di profondita' dei must*)
 164
 165 (*
 166 let choose_must list_of_must only=
 167 let n = (List.length list_of_must) - 1 in
 168    List.nth list_of_must n
 169 ;;*)
 170
 171 let choose_must list_of_must only =
 172    List.nth list_of_must 0
 173
 174 (* OLD CODE: TO BE REMOVED
 175 (*Funzione position prende una lista e un elemento e mi ritorna la posizione dell'elem nella lista*)
 176 (*Mi serve per ritornare la posizione del teo che produce meno subgoal*)
 177
 178 exception NotInTheList;;
 179
 180
 181 let position n =
 182         let rec aux k =
 183          function
 184              [] -> raise NotInTheList
 185             | m::_ when m=n -> k
 186             | _::tl -> aux (k+1) tl in
 187         aux 1
 188 ;;
 189
 190
 191
 192 (*function taking a status and returning a new status after having searching a theorem to apply ,theorem which *)
 193 (*generate the less number of subgoals*)
 194
 195 let  searchTheorem (proof,goal) =
 196   let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
 197   in
 198     let mqi_handle = MQIC.init mqi_flags prerr_string
 199 in
 200   let uris' =
 201     matchConclusion
 202       mqi_handle ~choose_must() (proof, goal)
 203   in
 204   let list_of_termin =
 205     List.map
 206     (function string ->
 207     (MQueryMisc.term_of_cic_textual_parser_uri
 208     (MQueryMisc.cic_textual_parser_uri_of_string string))
 209     )
 210     uris'
 211   in
 212   let list_proofgoal =
 213     List.map
 214     (function term ->
 215       PrimitiveTactics.apply_tac ~term (proof,goal))
 216     list_of_termin
 217   in
 218   let (list_of_subgoal: int  list list) =
 219   List.map  snd list_proofgoal
 220   in
 221   let list_of_num =
 222   List.map List.length list_of_subgoal
 223   in
 224   let list_sort =
 225   List.sort Pervasives.compare list_of_num
 226   in                                   (*ordino la lista in modo cresc*)
 227   let min= List.nth  list_sort 0   (*prendo il minimo*)
 228   in
 229   let uri' =              (*cerco il teo di pos k*)
 230   List.nth list_of_termin (position  min list_of_num)
 231   in
 232   (* let teo=
 233     String.sub uri' 4 (String.length uri' - 4)
 234
 235   (* modifico la str in modo che sia accettata da apply*)
 236   in*)
 237   PrimitiveTactics.apply_tac ~term:uri' (proof,goal)
 238 ;;
 239 *)
 240
 241
 242 let  searchTheorems mqi_handle (proof,goal) =
 243 (*prerr_endline "1";*)
 244   let uris' =
 245     matchConclusion2 mqi_handle ~choose_must() (proof, goal) in
 246 prerr_endline (string_of_int (List.length uris'));
 247 (*prerr_endline "2";*)
 248 (*  let list_of_termin =
 249     List.map
 250       (function string ->
 251          (MQueryMisc.term_of_cic_textual_parser_uri
 252          (MQueryMisc.cic_textual_parser_uri_of_string string)))
 253     uris' in
 254 prerr_endline "3";
 255   let list_proofgoal =
 256     List.map
 257       (function term ->
 258          PrimitiveTactics.apply_tac ~term (proof,goal)) list_of_termin in*)
 259 (*prerr_endline "4";*)
 260 let res =
 261   List.sort
 262     (fun (_,gl1) (_,gl2) ->
 263         Pervasives.compare (List.length gl1) (List.length gl2))
 264     uris'
 265     in
 266 (*prerr_endline "5";*)
 267 res
 268 ;;
 269