]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/tacticChaser.ml
New syntax.
[helm.git] / 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 result = Match_concl.cmatch conn ty in
125   (* Stampa il risultato della query 
126   List.iter 
127     (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) result;
128   *)
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   (*
142   let uris =
143     (* TODO ristretto per ragioni di efficienza *)
144     List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
145   *)
146   (* concl_cost are the costants in the conclusion of the proof 
147      while hyp_const are the constants in the hypothesis *)
148   let (_,concl_const) = NewConstraints.constants_of ty in
149   prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
150   let hyp t set =
151     match t with
152       Some (_,Cic.Decl t) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
153     | Some (_,Cic.Def (t,_)) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
154     | _ -> set in
155   let hyp_const =
156     List.fold_right hyp ey NewConstraints.StringSet.empty in
157   prerr_endline (NewConstraints.pp_StringSet (NewConstraints.StringSet.union hyp_const concl_const));
158   (* uris with new constants in the proof are filtered *)
159   let all_const = NewConstraints.StringSet.union hyp_const concl_const in
160   let uris = 
161     if (List.length uris < (Filter_auto.power 2 (List.length (NewConstraints.StringSet.elements all_const))))
162      then List.filter (Filter_auto.filter_new_constants conn all_const) uris 
163     else Filter_auto.filter_uris conn all_const uris in 
164 (*
165   let uris =
166     (* ristretto all cache *)
167     prerr_endline "SOLO CACHE";
168     List.filter 
169       (fun uri -> CicEnvironment.in_cache (UriManager.uri_of_string uri)) uris
170   in 
171   prerr_endline "HO FILTRATO2";
172 *)
173   let uris' =
174     let rec filter_out =
175      function
176         [] -> []
177       | (m,uri)::tl ->
178           let tl' = filter_out tl in
179             try
180               (m,
181                (prerr_endline ("STO APPLICANDO " ^ uri);
182                 (ProofEngineTypes.apply_tactic( PrimitiveTactics.apply_tac
183                    ~term:(MQueryMisc.term_of_cic_textual_parser_uri
184                             (MQueryMisc.cic_textual_parser_uri_of_string uri)))
185                    status)))::tl'
186             (* with ProofEngineTypes.Fail _ -> tl' *)
187             (* patch to cover CSC's exportation bug *)
188             with _ -> tl' 
189      in    
190      prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
191      filter_out uris
192    in
193      prerr_endline ("Ne sono rimasti " ^ 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) =  
237            let (_, ey ,ty) = CicUtil.lookup_meta goal1 metasenv in
238             (ey, ty) in
239    let (ey2, ty2) =  
240            let (_, ey ,ty) = CicUtil.lookup_meta goal2 metasenv in
241             (ey, ty) in 
242    let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
243    let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey1 ty2 in
244    let prop1 = if CicReduction.are_convertible 
245                    ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0
246                  else 1 in
247    let prop2 = if CicReduction.are_convertible 
248                    ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0
249                  else 1 in
250  prop1 - prop2 in
251  List.map (fun (level,(proof,goallist)) -> (proof, (List.stable_sort (order_goal_list proof) goallist))) res  
252 ;;
253