1 (* Copyright (C) 2000-2002, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
34 (******************************************************************************)
36 module MQI = MQueryInterpreter
38 module I = MQueryInterpreter
40 module G = MQueryGenerator
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
50 let must = choose_must list_of_must only in
54 (G.query_of_constraints
55 (Some CGMatchConclusion.universe)
56 (must,[],[]) (Some only,None,None)) in
61 MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
65 (* TODO ristretto per ragioni di efficienza *)
66 prerr_endline "STO FILTRANDO";
67 List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
69 prerr_endline "HO FILTRATO";
75 let tl',exc = filter_out tl in
78 let time = Unix.gettimeofday() in
81 (PrimitiveTactics.apply_tac
82 ~term:(MQueryMisc.term_of_cic_textual_parser_uri
83 (MQueryMisc.cic_textual_parser_uri_of_string uri))
85 let time1 = Unix.gettimeofday() in
86 prerr_endline (Printf.sprintf "%1.3f" (time1 -. time) );
88 with ProofEngineTypes.Fail _ ->
89 let time1 = Unix.gettimeofday() in
90 prerr_endline (Printf.sprintf "%1.3f" (time1 -. time)); false)
96 (ProofEngineTypes.Fail _) as e ->
98 "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
99 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
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>"
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
123 match mqi_handle.MQIConn.pgc with
124 MQIConn.MySQL_C conn -> conn
125 | _ -> assert false in
126 let result = Match_concl.cmatch conn ty in
128 (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) result;
132 (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u))
134 (* delete all .var uris *)
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 *)
142 (* TODO ristretto per ragioni di efficienza *)
143 List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
144 (* concl_cost are the costants in the conclusion of the proof
145 while hyp_const are the constants in the hypothesis *)
146 let (_,concl_const) = NewConstraints.constants_of ty in
147 prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
150 Some (_,Cic.Decl t) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
151 | Some (_,Cic.Def (t,_)) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
154 List.fold_right hyp ey NewConstraints.StringSet.empty in
155 prerr_endline (NewConstraints.pp_StringSet (NewConstraints.StringSet.union hyp_const concl_const));
156 (* uris with new constants in the proof are filtered *)
157 let uris = List.filter (Filter_auto.filter_new_constants conn (NewConstraints.StringSet.union hyp_const concl_const)) uris in
160 (* ristretto all cache *)
161 prerr_endline "SOLO CACHE";
163 (fun uri -> CicEnvironment.in_cache (UriManager.uri_of_string uri)) uris
165 prerr_endline "HO FILTRATO2";
172 let tl' = filter_out tl in
175 (prerr_endline ("STO APPLICANDO " ^ uri);
176 (PrimitiveTactics.apply_tac
177 ~term:(MQueryMisc.term_of_cic_textual_parser_uri
178 (MQueryMisc.cic_textual_parser_uri_of_string uri))
180 (* with ProofEngineTypes.Fail _ -> tl' *)
181 (* patch to cover CSC's exportation bug *)
184 prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
187 prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris'));
191 (*funzione che sceglie il penultimo livello di profondita' dei must*)
194 let choose_must list_of_must only=
195 let n = (List.length list_of_must) - 1 in
196 List.nth list_of_must n
199 (* questa prende solo il main *)
200 let choose_must list_of_must only =
201 List.nth list_of_must 0
204 let choose_must list_of_must only =
206 List.nth list_of_must 1
208 List.nth list_of_must 0 *)
210 (* OLD CODE: TO BE REMOVED
211 (*Funzione position prende una lista e un elemento e mi ritorna la posizione dell'elem nella lista*)
212 (*Mi serve per ritornare la posizione del teo che produce meno subgoal*)
214 exception NotInTheList;;
220 [] -> raise NotInTheList
222 | _::tl -> aux (k+1) tl in
228 (*function taking a status and returning a new status after having searching a theorem to apply ,theorem which *)
229 (*generate the less number of subgoals*)
231 let searchTheorem (proof,goal) =
232 let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
234 let mqi_handle = MQIC.init mqi_flags prerr_string
238 mqi_handle ~choose_must() (proof, goal)
243 (MQueryMisc.term_of_cic_textual_parser_uri
244 (MQueryMisc.cic_textual_parser_uri_of_string string))
251 PrimitiveTactics.apply_tac ~term (proof,goal))
254 let (list_of_subgoal: int list list) =
255 List.map snd list_proofgoal
258 List.map List.length list_of_subgoal
261 List.sort Pervasives.compare list_of_num
262 in (*ordino la lista in modo cresc*)
263 let min= List.nth list_sort 0 (*prendo il minimo*)
265 let uri' = (*cerco il teo di pos k*)
266 List.nth list_of_termin (position min list_of_num)
269 String.sub uri' 4 (String.length uri' - 4)
271 (* modifico la str in modo che sia accettata da apply*)
273 PrimitiveTactics.apply_tac ~term:uri' (proof,goal)
278 let searchTheorems mqi_handle (proof,goal) =
279 (*prerr_endline "1";*)
281 matchConclusion2 mqi_handle ~choose_must() (proof, goal) in
284 (fun (n1,(_,gl1)) (n2,(_,gl2)) ->
285 let l1 = List.length gl1 in
286 let l2 = List.length gl2 in
287 (* if the list of subgoals have the same lenght we use the
288 prefix tag, where higher tags have precedence *)
289 if l1 = l2 then n2 - n1
293 (* now we may drop the prefix tag *)