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   let result =
  52    I.execute mqi_handle
  53       (G.query_of_constraints
  54         (Some CGMatchConclusion.universe)
  55         (must,[],[]) (Some only,None,None)) in
  56   let uris =
  57    List.map
  58     (function uri,_ ->
  59       MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
  60     ) result
  61   in
  62   let uris =
  63     (* TODO ristretto per ragioni di efficienza *)
  64     prerr_endline "STO FILTRANDO";
  65     List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
  66   in
  67   prerr_endline "HO FILTRATO";
  68   let uris',exc =
  69     let rec filter_out =
  70      function
  71         [] -> [],""
  72       | uri::tl ->
  73          let tl',exc = filter_out tl in
  74           try
  75            if
  76             (try
  77              ignore
  78               (PrimitiveTactics.apply_tac
  79                ~term:(MQueryMisc.term_of_cic_textual_parser_uri
  80                 (MQueryMisc.cic_textual_parser_uri_of_string uri))
  81                ~status);
  82              true
  83             with ProofEngineTypes.Fail _ -> false)
  84            then
  85             uri::tl',exc
  86            else
  87             tl',exc
  88           with
  89            (ProofEngineTypes.Fail _) as e ->
  90              let exc' =
  91               "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
  92                uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
  93              in
  94               tl',exc'
  95     in
  96      filter_out uris
  97   in
  98     let html' =
  99      " <h1>Objects that can actually be applied: </h1> " ^
 100      String.concat "<br>" uris' ^ exc ^
 101      " <h1>Number of false matches: " ^
 102       string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
 103      " <h1>Number of good matches: " ^
 104       string_of_int (List.length uris') ^ "</h1>"
 105     in
 106      output_html html' ;
 107      uris'
 108 ;;
 109
 110
 111 (*funzione che sceglie il penultimo livello di profondita' dei must*)
 112
 113 (*
 114 let choose_must list_of_must only=
 115 let n = (List.length list_of_must) - 1 in
 116    List.nth list_of_must n
 117 ;;*)
 118
 119 let choose_must list_of_must only =
 120    List.nth list_of_must 0
 121
 122 (* OLD CODE: TO BE REMOVED
 123 (*Funzione position prende una lista e un elemento e mi ritorna la posizione dell'elem nella lista*)
 124 (*Mi serve per ritornare la posizione del teo che produce meno subgoal*)
 125
 126 exception NotInTheList;;
 127
 128
 129 let position n =
 130         let rec aux k =
 131          function
 132              [] -> raise NotInTheList
 133             | m::_ when m=n -> k
 134             | _::tl -> aux (k+1) tl in
 135         aux 1
 136 ;;
 137
 138
 139
 140 (*function taking a status and returning a new status after having searching a theorem to apply ,theorem which *)
 141 (*generate the less number of subgoals*)
 142
 143 let  searchTheorem ~status:(proof,goal) =
 144   let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
 145   in
 146     let mqi_handle = MQIC.init mqi_flags prerr_string
 147 in
 148   let uris' =
 149     matchConclusion
 150       mqi_handle ~choose_must() ~status:(proof, goal)
 151   in
 152   let list_of_termin =
 153     List.map
 154     (function string ->
 155     (MQueryMisc.term_of_cic_textual_parser_uri
 156     (MQueryMisc.cic_textual_parser_uri_of_string string))
 157     )
 158     uris'
 159   in
 160   let list_proofgoal =
 161     List.map
 162     (function term ->
 163       PrimitiveTactics.apply_tac ~term ~status:(proof,goal))
 164     list_of_termin
 165   in
 166   let (list_of_subgoal: int  list list) =
 167   List.map  snd list_proofgoal
 168   in
 169   let list_of_num =
 170   List.map List.length list_of_subgoal
 171   in
 172   let list_sort =
 173   List.sort Pervasives.compare list_of_num
 174   in                                   (*ordino la lista in modo cresc*)
 175   let min= List.nth  list_sort 0   (*prendo il minimo*)
 176   in
 177   let uri' =              (*cerco il teo di pos k*)
 178   List.nth list_of_termin (position  min list_of_num)
 179   in
 180   (* let teo=
 181     String.sub uri' 4 (String.length uri' - 4)
 182
 183   (* modifico la str in modo che sia accettata da apply*)
 184   in*)
 185   PrimitiveTactics.apply_tac ~term:uri' ~status:(proof,goal)
 186 ;;
 187 *)
 188
 189
 190 let  searchTheorems mqi_handle ~status:(proof,goal) =
 191 prerr_endline "1";
 192   let uris' =
 193     matchConclusion mqi_handle ~choose_must() ~status:(proof, goal) in
 194 prerr_endline "2";
 195   let list_of_termin =
 196     List.map
 197       (function string ->
 198          (MQueryMisc.term_of_cic_textual_parser_uri
 199          (MQueryMisc.cic_textual_parser_uri_of_string string)))
 200     uris' in
 201 prerr_endline "3";
 202   let list_proofgoal =
 203     List.map
 204       (function term ->
 205          PrimitiveTactics.apply_tac ~term ~status:(proof,goal)) list_of_termin in
 206 prerr_endline "4";
 207 let res =
 208   List.sort
 209     (fun (_,gl1) (_,gl2) ->
 210         Pervasives.compare (List.length gl1) (List.length gl2))
 211     list_proofgoal
 212     in
 213 prerr_endline "5";
 214 res
 215 ;;
 216