1 (* Copyright (C) 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 (* Da rimuovere, solo per debug*)
27 let print_context ctx =
31 | Cic.Anonymous -> "_"
34 (fun i (output,context) ->
35 let (newoutput,context') =
37 Some (n,Cic.Decl t) ->
38 print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
39 | Some (n,Cic.Def (t,None)) ->
40 print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
42 "_ ?= _\n", None::context
43 | Some (_,Cic.Def (_,Some _)) -> assert false
45 output^newoutput,context'
50 let search_theorems_in_context status =
51 let (proof, goal) = status in
53 let module R = CicReduction in
54 let module S = CicSubstitution in
55 let module PET = ProofEngineTypes in
56 let module PT = PrimitiveTactics in
57 let _,metasenv,_,_ = proof in
58 let _,context,ty = CicUtil.lookup_meta goal metasenv in
59 let rec find n = function
64 Some (PET.apply_tactic
65 (PT.apply_tac ~term:(C.Rel n)) status )
69 Some res -> res::(find (n+1) tl)
70 | None -> find (n+1) tl)
80 let new_search_theorems f proof goal depth gtl sign =
81 let choices = f (proof,goal)
84 (function (proof, goallist) ->
85 (proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign))
89 exception NoOtherChoices;;
90 let rec auto dbd = function
92 | (proof, [], sign)::tl -> (proof, [], sign)::tl
93 | (proof, (goal,0)::_, _)::tl -> auto dbd tl
94 | (proof, (((goal,depth)::gtl) as allg), sign)::tl ->
95 (* first we check if the metavariable has not been already
96 closed as a side effect by some other application *)
97 let facts = (depth = 1) in
98 let name,metasenv,p,statement = proof in
101 let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
106 (* the goal is still there *)
108 prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
109 prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
110 prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
112 (* if the goal contains metavariables we use the input
113 signature for at_most constraints *)
114 let is_meta_closed = CicUtil.is_meta_closed ty in
116 if is_meta_closed then
117 None, Some (MetadataConstraints.signature_of ty)
118 else sign,sign in (* maybe the union ? *)
121 search_theorems_in_context
122 proof goal (depth-1) [] new_sign in
128 ~dbd ~facts:facts ?signature:sign status))
129 proof goal (depth-1) [] new_sign in
130 (* we proceed depth-first on the current goal. This is
131 a MAJOR optimization, since in case of success, and
132 if the goal is meta_closed, we may just drop the alternatives
133 tl1, avoiding useless backtracking. *)
135 local_choices@global_choices in
136 (match (auto dbd all_choices)
139 | (proof,[],_)::tl1 ->
141 let gtl' = List.map fst gtl in
142 if (gtl = [] || is_meta_closed) then
147 (function (p,l,s) -> (p,l@gtl,s)) tl1)
149 (proof,gtl,sign)::tl2@tl in
152 | None -> auto dbd ((proof,gtl,sign)::tl)
156 let auto_tac ~(dbd:Mysql.dbd) =
157 let auto_tac dbh (proof,goal) =
158 prerr_endline "Entro in Auto";
159 match (auto dbd [(proof, [(goal,depth)],None)]) with
160 [] -> prerr_endline("Auto failed");
161 raise (ProofEngineTypes.Fail "No Applicable theorem")
163 prerr_endline "AUTO_TAC HA FINITO";
167 ProofEngineTypes.mk_tactic (auto_tac dbd)
171 (************************** EXPERIMENTAL VERSION ****************************)
173 (* In this versions of auto_tac we maintain an hash table of all inspected
174 goals. We assume that the context is invariant for application.
175 To this aim, it is essential to sall hint_verbose, that in turns calls
181 | Yes of Cic.term * int
184 let inspected_goals = Hashtbl.create 503;;
186 let search_theorems_in_context status =
187 let (proof, goal) = status in
188 let module C = Cic in
189 let module R = CicReduction in
190 let module S = CicSubstitution in
191 let module PET = ProofEngineTypes in
192 let module PT = PrimitiveTactics in
193 let _,metasenv,_,_ = proof in
194 let _,context,ty = CicUtil.lookup_meta goal metasenv in
195 let rec find n = function
200 Some (PT.apply_tac_verbose ~term:(C.Rel n) status )
202 PET.Fail _ -> None in
204 Some res -> res::(find (n+1) tl)
205 | None -> find (n+1) tl)
213 let new_search_theorems f proof goal depth subst sign =
214 let choices = f (proof,goal)
217 (function (local_subst,(proof, goallist)) ->
218 let new_subst t= local_subst (subst t) in
219 (new_subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
223 exception NoOtherChoices;;
224 let rec auto_new dbd = function
226 | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
227 | (subst,(proof, (goal,0)::_, _))::tl -> auto_new dbd tl
228 | (subst,(proof, (((goal,depth)::gtl) as allg), sign))::tl ->
229 let facts = (depth = 1) in
230 let name,metasenv,p,statement = proof in
233 let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
238 (* first of all we check if the goal has been already
241 try Hashtbl.find inspected_goals ty
242 with Not_found -> NotYetInspected in
243 let is_meta_closed = CicUtil.is_meta_closed ty in
248 prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
249 prerr_endline (CicPp.ppterm ty);
252 (* if we just apply the subtitution, the type
253 is irrelevant: we may use Implicit, since it will
255 CicMetaSubst.apply_subst
256 [(goal,(ey, bo, Cic.Implicit None))] in
258 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
259 proof goal subst_in metasenv in
260 let new_subst t = (subst_in (subst t)) in
261 auto_new dbd ((new_subst,(proof,gtl,sign))::tl)
262 | No d when (d >= depth) ->
264 prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
271 prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
272 prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
273 prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
276 if is_meta_closed then
277 None, Some (MetadataConstraints.signature_of ty)
278 else sign,sign in (* maybe the union ? *)
281 search_theorems_in_context
282 proof goal (depth-1) subst new_sign in
287 (MetadataQuery.experimental_hint
288 ~dbd ~facts:facts ?signature:sign status))
289 proof goal (depth-1) subst new_sign in
291 local_choices@global_choices in
292 (match (auto_new dbd all_choices)
295 (* no proof has been found; we update the
297 Hashtbl.add inspected_goals ty (No depth);
299 | (new_subst,(proof,[],_))::tl1 ->
300 (* a proof for goal has been found:
301 in order to get the proof we apply subst to
303 if is_meta_closed then
306 CicMkImplicit.identity_relocation_list_for_metavariable ey in
308 new_subst (Cic.Meta(goal,irl)) in
309 Hashtbl.add inspected_goals
310 ty (Yes (meta_proof,depth));
313 let gtl' = List.map fst gtl in
314 if (gtl = [] || is_meta_closed) then
315 (new_subst,(proof,gtl,sign))::tl
319 (function (f,(p,l,s))
320 -> (f,(p,l@gtl,s))) tl1)
322 (new_subst,(proof,gtl,sign))::tl2@tl in
323 auto_new dbd all_choices
326 | None -> auto_new dbd ((subst,(proof,gtl,sign))::tl)
330 let auto_tac_new ~(dbd:Mysql.dbd) =
331 let auto_tac dbd (proof,goal) =
332 Hashtbl.clear inspected_goals;
333 prerr_endline "Entro in Auto";
335 match (auto_new dbd [id,(proof, [(goal,depth)],None)]) with
336 [] -> prerr_endline("Auto failed");
337 raise (ProofEngineTypes.Fail "No Applicable theorem")
338 | (_,(proof,[],_))::_ ->
339 prerr_endline "AUTO_TAC HA FINITO";
343 ProofEngineTypes.mk_tactic (auto_tac dbd)