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              let time = Unix.gettimeofday() in
  77             (try
  78              ignore(ProofEngineTypes.apply_tactic
  79                (PrimitiveTactics.apply_tac
  80                   ~term:(MQueryMisc.term_of_cic_textual_parser_uri
  81                            (MQueryMisc.cic_textual_parser_uri_of_string uri)))
  82                   status);
  83                let time1 = Unix.gettimeofday() in
  84                  prerr_endline (Printf.sprintf "%1.3f" (time1 -. time) );
  85                true
  86             with ProofEngineTypes.Fail _ ->
  87               let time1 = Unix.gettimeofday() in
  88               prerr_endline (Printf.sprintf "%1.3f" (time1 -. time)); false)
  89            then
  90             uri::tl',exc
  91            else
  92             tl',exc
  93           with
  94            (ProofEngineTypes.Fail _) as e ->
  95              let exc' =
  96               "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
  97                uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
  98              in
  99               tl',exc'
 100     in
 101      filter_out uris
 102   in
 103     let html' =
 104      " <h1>Objects that can actually be applied: </h1> " ^
 105      String.concat "<br>" uris' ^ exc ^
 106      " <h1>Number of false matches: " ^
 107       string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
 108      " <h1>Number of good matches: " ^
 109       string_of_int (List.length uris') ^ "</h1>"
 110     in
 111      output_html html' ;
 112      uris'
 113 ;;
 114
 115
 116 (*matchConclusion modificata per evitare una doppia apply*)
 117 let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
 118   let ((_, metasenv, _, _), metano) = status in
 119   let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
 120   let conn =
 121     match mqi_handle.MQIConn.pgc with
 122         MQIConn.MySQL_C conn -> conn
 123       | _ -> assert false in
 124   let uris = Match_concl.cmatch conn ty in
 125   (* List.iter
 126     (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) uris; *)
 127   (* delete all .var uris *)
 128   let isvar (_,s) =
 129     let len = String.length s in
 130     let suffix = String.sub s (len-4) 4 in
 131       not (suffix  = ".var") in
 132   let uris = List.filter isvar uris in
 133   (* delete all not "cic:/Coq" uris *)
 134   (*
 135   let uris =
 136     (* TODO ristretto per ragioni di efficienza *)
 137     List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
 138   *)
 139   (* concl_cost are the costants in the conclusion of the proof
 140      while hyp_const are the constants in the hypothesis *)
 141   let (main_concl,concl_const) = NewConstraints.mainandcons ty in
 142   prerr_endline ("Ne sono rimasti" ^ string_of_int (List.length uris));
 143   let hyp t set =
 144     match t with
 145       Some (_,Cic.Decl t) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
 146     | Some (_,Cic.Def (t,_)) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
 147     | _ -> set in
 148   let hyp_const =
 149     List.fold_right hyp ey NewConstraints.StringSet.empty in
 150   prerr_endline (NewConstraints.pp_StringSet (NewConstraints.StringSet.union hyp_const concl_const));
 151   (* uris with new constants in the proof are filtered *)
 152   let all_const = NewConstraints.StringSet.union hyp_const concl_const in
 153   let uris =
 154     if (List.length uris < (Filter_auto.power 2 (List.length (NewConstraints.StringSet.elements all_const))))
 155      then
 156      (prerr_endline("metodo vecchio");List.filter (Filter_auto.filter_new_constants conn all_const) uris)
 157     else Filter_auto.filter_uris conn all_const uris main_concl 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     List.map
 169       (fun (n,u) ->
 170          (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u))
 171       uris in
 172   let uris' =
 173     let rec filter_out =
 174      function
 175         [] -> []
 176       | (m,uri)::tl ->
 177           let tl' = filter_out tl in
 178             try
 179                    prerr_endline ("STO APPLICANDO " ^ uri);
 180               let res = (m,
 181                 (ProofEngineTypes.apply_tactic( PrimitiveTactics.apply_tac
 182                    ~term:(MQueryMisc.term_of_cic_textual_parser_uri
 183                             (MQueryMisc.cic_textual_parser_uri_of_string uri)))
 184                    status))::tl' in
 185                 prerr_endline ("OK");res
 186             (* with ProofEngineTypes.Fail _ -> tl' *)
 187             (* patch to cover CSC's exportation bug *)
 188             with _ -> prerr_endline ("FAIL");tl'
 189      in
 190      prerr_endline ("Ne sono rimasti 2 " ^ string_of_int (List.length uris));
 191      filter_out uris
 192    in
 193      prerr_endline ("Ne sono rimasti 3 " ^ string_of_int (List.length uris'));
 194
 195      uris'
 196 ;;
 197
 198 (*funzione che sceglie il penultimo livello di profondita' dei must*)
 199
 200 (*
 201 let choose_must list_of_must only=
 202 let n = (List.length list_of_must) - 1 in
 203    List.nth list_of_must n
 204 ;;*)
 205
 206 (* questa prende solo il main *)
 207 let choose_must list_of_must only =
 208    List.nth list_of_must 0
 209
 210 (* livello 1
 211 let choose_must list_of_must only =
 212    try
 213      List.nth list_of_must 1
 214    with _ ->
 215      List.nth list_of_must 0 *)
 216
 217 let  searchTheorems mqi_handle (proof,goal) =
 218   let subproofs =
 219     matchConclusion2 mqi_handle ~choose_must() (proof, goal) in
 220  let res =
 221   List.sort
 222     (fun (n1,(_,gl1)) (n2,(_,gl2)) ->
 223        let l1 = List.length gl1 in
 224        let l2 = List.length gl2 in
 225        (* if the list of subgoals have the same lenght we use the
 226           prefix tag, where higher tags have precedence *)
 227        if l1 = l2 then n2 - n1
 228        else l1 - l2)
 229     subproofs
 230  in
 231   (* now we may drop the prefix tag *)
 232  (*let res' =
 233    List.map snd res in*)
 234  let order_goal_list proof goal1 goal2 =
 235    let _,metasenv,_,_ = proof in
 236    let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
 237    let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
 238 (*
 239    prerr_endline "PRIMA DELLA PRIMA TYPE OF " ;
 240 *)
 241    let ty_sort1,u = (*TASSI: FIXME *)
 242      CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph in
 243 (*
 244    prerr_endline (Printf.sprintf "PRIMA DELLA SECONDA TYPE OF %s \n### %s @@@%s " (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppcontext [] ey2) (CicMetaSubst.ppterm [] ty2));
 245 *)
 246    let ty_sort2,u1 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 u in
 247 (*
 248    prerr_endline "DOPO LA SECONDA TYPE OF " ;
 249 *)
 250    let b,u2 =
 251      CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 u1 in
 252    let prop1 = if b then 0 else 1 in
 253    let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 u2 in
 254    let prop2 = if b then 0 else 1 in
 255      prop1 - prop2 in
 256    List.map (
 257      fun (level,(proof,goallist)) ->
 258        (proof, (List.stable_sort (order_goal_list proof) goallist))
 259    ) res
 260 ;;
 261