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
53 (G.query_of_constraints
54 (Some CGMatchConclusion.universe)
55 (must,[],[]) (Some only,None,None)) in
59 MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
63 (* TODO ristretto per ragioni di efficienza *)
64 prerr_endline "STO FILTRANDO";
65 List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
67 prerr_endline "HO FILTRATO";
73 let tl',exc = filter_out tl in
78 (PrimitiveTactics.apply_tac
79 ~term:(MQueryMisc.term_of_cic_textual_parser_uri
80 (MQueryMisc.cic_textual_parser_uri_of_string uri))
83 with ProofEngineTypes.Fail _ -> false)
89 (ProofEngineTypes.Fail _) as e ->
91 "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
92 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
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>"
111 (*funzione che sceglie il penultimo livello di profondita' dei must*)
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
119 let choose_must list_of_must only =
120 List.nth list_of_must 0
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*)
126 exception NotInTheList;;
132 [] -> raise NotInTheList
134 | _::tl -> aux (k+1) tl in
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*)
143 let searchTheorem ~status:(proof,goal) =
144 let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
146 let mqi_handle = MQIC.init mqi_flags prerr_string
150 mqi_handle ~choose_must() ~status:(proof, goal)
155 (MQueryMisc.term_of_cic_textual_parser_uri
156 (MQueryMisc.cic_textual_parser_uri_of_string string))
163 PrimitiveTactics.apply_tac ~term ~status:(proof,goal))
166 let (list_of_subgoal: int list list) =
167 List.map snd list_proofgoal
170 List.map List.length list_of_subgoal
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*)
177 let uri' = (*cerco il teo di pos k*)
178 List.nth list_of_termin (position min list_of_num)
181 String.sub uri' 4 (String.length uri' - 4)
183 (* modifico la str in modo che sia accettata da apply*)
185 PrimitiveTactics.apply_tac ~term:uri' ~status:(proof,goal)
190 let searchTheorems mqi_handle ~status:(proof,goal) =
193 matchConclusion mqi_handle ~choose_must() ~status:(proof, goal) in
198 (MQueryMisc.term_of_cic_textual_parser_uri
199 (MQueryMisc.cic_textual_parser_uri_of_string string)))
205 PrimitiveTactics.apply_tac ~term ~status:(proof,goal)) list_of_termin in
209 (fun (_,gl1) (_,gl2) ->
210 Pervasives.compare (List.length gl1) (List.length gl2))