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 prerr_endline "Entro in search_context";
58 let _,metasenv,_,_ = proof in
59 let _,context,ty = CicUtil.lookup_meta goal metasenv in
60 let rec find n = function
65 Some (PET.apply_tactic
66 (PT.apply_tac ~term:(C.Rel n)) status )
70 Some res -> res::(find (n+1) tl)
71 | None -> find (n+1) tl)
81 let new_search_theorems f proof goal depth gtl sign =
82 let choices = f (proof,goal)
85 (function (proof, goallist) ->
86 (proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign))
90 exception NoOtherChoices;;
91 let rec auto dbd = function
93 | (proof, [], sign)::tl -> (proof, [], sign)::tl
94 | (proof, (goal,0)::_, _)::tl -> auto dbd tl
95 | (proof, (((goal,depth)::gtl) as allg), sign)::tl ->
96 (* first we check if the metavariable has not been already
97 closed as a side effect by some other application *)
98 let facts = (depth = 1) in
99 let name,metasenv,p,statement = proof in
102 let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
107 (* 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)));
111 (* if the goal contains metavariables we use the input
112 signature for at_most constraints *)
113 let is_meta_closed = CicUtil.is_meta_closed ty in
115 if is_meta_closed then
116 None, Some (MetadataConstraints.signature_of ty)
117 else sign,sign in (* maybe the union ? *)
120 search_theorems_in_context
121 proof goal (depth-1) [] new_sign in
127 ~dbd ~facts:facts ?signature:sign status))
128 proof goal (depth-1) [] new_sign in
129 (* we proceed depth-first on the current goal. This is
130 a MAJOR optimization, since in case of success, and
131 if the goal is meta_closed, we may just drop the alternatives
132 tl1, avoiding useless backtracking. *)
134 local_choices@global_choices in
135 (match (auto dbd all_choices)
138 | (proof,[],_)::tl1 ->
140 let gtl' = List.map fst gtl in
141 if (gtl = [] || is_meta_closed) then
146 (function (p,l,s) -> (p,l@gtl,s)) tl1)
148 (proof,gtl,sign)::tl2@tl in
151 | None -> auto dbd ((proof,gtl,sign)::tl)
155 let auto_tac ~(dbd:Mysql.dbd) =
156 let auto_tac dbh (proof,goal) =
157 prerr_endline "Entro in Auto";
158 match (auto dbd [(proof, [(goal,depth)],None)]) with
159 [] -> prerr_endline("Auto failed");
160 raise (ProofEngineTypes.Fail "No Applicable theorem")
162 prerr_endline "AUTO_TAC HA FINITO";
166 ProofEngineTypes.mk_tactic (auto_tac dbd)
170 (************************** EXPERIMENTAL VERSION ****************************)
172 (* In this versions of auto_tac we maintain an hash table of all inspected
173 goals. We assume that the context is invariant for application.
174 To this aim, it is essential to sall hint_verbose, that in turns calls
180 | Yes of Cic.term * int
183 let inspected_goals = Hashtbl.create 503;;
185 let search_theorems_in_context status =
186 let (proof, goal) = status in
187 let module C = Cic in
188 let module R = CicReduction in
189 let module S = CicSubstitution in
190 let module PET = ProofEngineTypes in
191 let module PT = PrimitiveTactics in
192 prerr_endline "Entro in search_context";
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 gtl sign =
214 let choices = f (proof,goal)
217 (function (subst,(proof, goallist)) ->
218 (subst,(proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign)))
222 exception NoOtherChoices;;
223 let rec auto_new dbd = function
225 | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
226 | (subst,(proof, (goal,0)::_, _))::tl -> auto_new dbd tl
227 | (subst,(proof, (((goal,depth)::gtl) as allg), sign))::tl ->
228 let facts = (depth = 1) in
229 let name,metasenv,p,statement = proof in
232 let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
237 (* first of all we check if the goal has been already
240 try Hashtbl.find inspected_goals ty
241 with Not_found -> NotYetInspected in
242 let is_meta_closed = CicUtil.is_meta_closed ty in
246 prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
247 prerr_endline (CicPp.ppterm ty);
249 (* if we just apply the subtitution, the type
250 is irrelevant: we may use Implicit, since it will
252 CicMetaSubst.apply_subst
253 [(goal,(ey, bo, Cic.Implicit None))] in
255 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
256 proof goal subst_in metasenv in
257 let new_subst t = (subst_in (subst t)) in
258 auto_new dbd ((new_subst,(proof,gtl,sign))::tl)
259 | No d when (d >= depth) ->
260 prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
264 prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
265 prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
266 prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
268 if is_meta_closed then
269 None, Some (MetadataConstraints.signature_of ty)
270 else sign,sign in (* maybe the union ? *)
273 search_theorems_in_context
274 proof goal (depth-1) [] new_sign in
279 (MetadataQuery.experimental_hint
280 ~dbd ~facts:facts ?signature:sign status))
281 proof goal (depth-1) [] new_sign in
283 local_choices@global_choices in
284 (match (auto_new dbd all_choices)
287 (* no proof has been found; we update the
289 Hashtbl.add inspected_goals ty (No depth);
291 | (local_subst,(proof,[],_))::tl1 ->
292 (* a proof for goal has been found:
293 in order to get the proof we apply subst to
295 if is_meta_closed then
298 CicMkImplicit.identity_relocation_list_for_metavariable ey in
300 local_subst (Cic.Meta(goal,irl)) in
301 Hashtbl.add inspected_goals
302 ty (Yes (meta_proof,depth));
304 let new_subst t = (local_subst (subst t)) in
306 let gtl' = List.map fst gtl in
307 if (gtl = [] || is_meta_closed) then
308 (new_subst,(proof,gtl,sign))::tl
312 (function (f,(p,l,s))
313 -> (f,(p,l@gtl,s))) tl1)
315 (new_subst,(proof,gtl,sign))::tl2@tl in
316 auto_new dbd all_choices
319 | None -> auto_new dbd ((subst,(proof,gtl,sign))::tl)
323 let auto_tac_new ~(dbd:Mysql.dbd) =
324 let auto_tac dbd (proof,goal) =
325 Hashtbl.clear inspected_goals;
326 prerr_endline "Entro in Auto";
328 match (auto_new dbd [id,(proof, [(goal,depth)],None)]) with
329 [] -> prerr_endline("Auto failed");
330 raise (ProofEngineTypes.Fail "No Applicable theorem")
331 | (_,(proof,[],_))::_ ->
332 prerr_endline "AUTO_TAC HA FINITO";
336 ProofEngineTypes.mk_tactic (auto_tac dbd)