]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/tacticChaser.ml
Trick: the refiner always subst-expands the outtype, so that the beta-redex
[helm.git] / helm / software / components / 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 (* $Id$ *)
37
38 module MQI = MQueryInterpreter
39 module MQIC = MQIConn
40 module I = MQueryInterpreter
41 module U = MQGUtil
42 module G = MQueryGenerator
43
44   (* search arguments on which Apply tactic doesn't fail *)
45 let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
46  let ((_, metasenv, _, _), metano) = status in
47  let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
48   let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
49 match list_of_must with
50   [] -> []
51 |_ ->
52   let must = choose_must list_of_must only in
53   let result =
54    I.execute mqi_handle 
55       (G.query_of_constraints
56         (Some CGMatchConclusion.universe)
57         (must,[],[]) (Some only,None,None)) in 
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(ProofEngineTypes.apply_tactic 
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 uris = Match_concl.cmatch conn ty in
127   (* List.iter 
128     (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) uris; *)
129   (* delete all .var uris *)
130   let uris = List.filter UriManager.is_var uris in 
131   (* delete all not "cic:/Coq" uris *)
132   (*
133   let uris =
134     (* TODO ristretto per ragioni di efficienza *)
135     List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
136   *)
137   (* concl_cost are the costants in the conclusion of the proof 
138      while hyp_const are the constants in the hypothesis *)
139   let (main_concl,concl_const) = NewConstraints.mainandcons ty in
140   prerr_endline ("Ne sono rimasti" ^ string_of_int (List.length uris));
141   let hyp t set =
142     match t with
143       Some (_,Cic.Decl t) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
144     | Some (_,Cic.Def (t,_)) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
145     | _ -> set in
146   let hyp_const =
147     List.fold_right hyp ey NewConstraints.StringSet.empty in
148   prerr_endline (NewConstraints.pp_StringSet (NewConstraints.StringSet.union hyp_const concl_const));
149   (* uris with new constants in the proof are filtered *)
150   let all_const = NewConstraints.StringSet.union hyp_const concl_const in
151   let uris = 
152     if (List.length uris < (Filter_auto.power 2 (List.length (NewConstraints.StringSet.elements all_const))))
153      then 
154      (prerr_endline("metodo vecchio");List.filter (Filter_auto.filter_new_constants conn all_const) uris)
155     else Filter_auto.filter_uris conn all_const uris main_concl in 
156 (*
157   let uris =
158     (* ristretto all cache *)
159     prerr_endline "SOLO CACHE";
160     List.filter 
161       (fun uri -> CicEnvironment.in_cache (UriManager.uri_of_string uri)) uris
162   in 
163   prerr_endline "HO FILTRATO2";
164 *)
165   let uris =
166     List.map
167       (fun (n,u) -> 
168          (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u)) 
169       uris in
170   let uris' =
171     let rec filter_out =
172      function
173         [] -> []
174       | (m,uri)::tl ->
175           let tl' = filter_out tl in
176             try
177                    prerr_endline ("STO APPLICANDO " ^ uri);
178               let res = (m,
179                 (ProofEngineTypes.apply_tactic( PrimitiveTactics.apply_tac
180                    ~term:(MQueryMisc.term_of_cic_textual_parser_uri
181                             (MQueryMisc.cic_textual_parser_uri_of_string uri)))
182                    status))::tl' in
183                 prerr_endline ("OK");res
184             (* with ProofEngineTypes.Fail _ -> tl' *)
185             (* patch to cover CSC's exportation bug *)
186             with _ -> prerr_endline ("FAIL");tl' 
187      in    
188      prerr_endline ("Ne sono rimasti 2 " ^ string_of_int (List.length uris));
189      filter_out uris
190    in
191      prerr_endline ("Ne sono rimasti 3 " ^ string_of_int (List.length uris'));
192    
193      uris'
194 ;;
195
196 (*funzione che sceglie il penultimo livello di profondita' dei must*)
197
198 (* 
199 let choose_must list_of_must only=
200 let n = (List.length list_of_must) - 1 in
201    List.nth list_of_must n
202 ;;*)
203
204 (* questa prende solo il main *) 
205 let choose_must list_of_must only =
206    List.nth list_of_must 0 
207  
208 (* livello 1
209 let choose_must list_of_must only =
210    try 
211      List.nth list_of_must 1
212    with _ -> 
213      List.nth list_of_must 0 *)
214
215 let  searchTheorems mqi_handle (proof,goal) =
216   let subproofs =
217     matchConclusion2 mqi_handle ~choose_must() (proof, goal) in
218  let res =
219   List.sort 
220     (fun (n1,(_,gl1)) (n2,(_,gl2)) -> 
221        let l1 = List.length gl1 in
222        let l2 = List.length gl2 in
223        (* if the list of subgoals have the same lenght we use the
224           prefix tag, where higher tags have precedence *)
225        if l1 = l2 then n2 - n1
226        else l1 - l2)
227     subproofs
228  in
229   (* now we may drop the prefix tag *)
230  (*let res' =
231    List.map snd res in*)
232  let order_goal_list proof goal1 goal2 =
233    let _,metasenv,_,_ = proof in
234    let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
235    let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
236 (*
237    prerr_endline "PRIMA DELLA PRIMA TYPE OF " ;
238 *)
239    let ty_sort1,u = (*TASSI: FIXME *)
240      CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph in
241 (*
242    prerr_endline (Printf.sprintf "PRIMA DELLA SECONDA TYPE OF %s \n### %s @@@%s " (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppcontext [] ey2) (CicMetaSubst.ppterm [] ty2));
243 *)
244    let ty_sort2,u1 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 u in
245 (*
246    prerr_endline "DOPO LA SECONDA TYPE OF " ;
247 *)
248    let b,u2 = 
249      CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 u1 in
250    let prop1 = if b then 0 else 1 in
251    let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 u2 in
252    let prop2 = if b then 0 else 1 in
253      prop1 - prop2 in
254    List.map (
255      fun (level,(proof,goallist)) -> 
256        (proof, (List.stable_sort (order_goal_list proof) goallist))
257    ) res  
258 ;;
259