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 let debug_print = prerr_endline
28 (* let debug_print = fun _ -> () *)
30 let search_theorems_in_context status =
31 let (proof, goal) = status in
33 let module R = CicReduction in
34 let module S = CicSubstitution in
35 let module PET = ProofEngineTypes in
36 let module PT = PrimitiveTactics in
37 let _,metasenv,_,_ = proof in
38 let _,context,ty = CicUtil.lookup_meta goal metasenv in
39 let rec find n = function
44 Some (PET.apply_tactic
45 (PT.apply_tac ~term:(C.Rel n)) status )
49 Some res -> res::(find (n+1) tl)
50 | None -> find (n+1) tl)
61 let new_search_theorems f proof goal depth gtl sign =
62 let choices = f (proof,goal)
65 (function (proof, goallist) ->
66 (proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign))
70 exception NoOtherChoices;;
71 let rec auto dbd = function
73 | (proof, [], sign)::tl -> (proof, [], sign)::tl
74 | (proof, (goal,0)::_, _)::tl -> auto dbd tl
75 | (proof, (((goal,depth)::gtl) as allg), sign)::tl ->
76 (* first we check if the metavariable has not been already
77 closed as a side effect by some other application *)
78 let facts = (depth = 1) in
79 let name,metasenv,p,statement = proof in
82 let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
87 (* the goal is still there *)
89 debug_print ("CURRENT GOAL = " ^ CicPp.ppterm ty);
90 debug_print ("CURRENT PROOF = " ^ CicPp.ppterm p);
91 debug_print ("CURRENT HYP = " ^ CicPp.ppcontext ey);
93 (* if the goal contains metavariables we use the input
94 signature for at_most constraints *)
95 let is_meta_closed = CicUtil.is_meta_closed ty in
97 if is_meta_closed then
98 None, Some (MetadataConstraints.signature_of ty)
99 else sign,sign in (* maybe the union ? *)
102 search_theorems_in_context
103 proof goal (depth-1) [] new_sign in
109 ~dbd ~facts:facts ?signature:sign status))
110 proof goal (depth-1) [] new_sign in
111 (* we proceed depth-first on the current goal. This is
112 a MAJOR optimization, since in case of success, and
113 if the goal is meta_closed, we may just drop the alternatives
114 tl1, avoiding useless backtracking. *)
116 local_choices@global_choices in
117 (match (auto dbd all_choices)
120 | (proof,[],_)::tl1 ->
122 let gtl' = List.map fst gtl in
123 if (gtl = [] || is_meta_closed) then
128 (function (p,l,s) -> (p,l@gtl,s)) tl1)
130 (proof,gtl,sign)::tl2@tl in
133 | None -> auto dbd ((proof,gtl,sign)::tl)
137 let auto_tac ?num dbd =
138 let auto_tac dbh (proof,goal) =
139 debug_print "Entro in Auto";
140 match (auto dbd [(proof, [(goal,depth)],None)]) with
141 [] -> debug_print("Auto failed");
142 raise (ProofEngineTypes.Fail "No Applicable theorem")
144 debug_print "AUTO_TAC HA FINITO";
148 ProofEngineTypes.mk_tactic (auto_tac dbd)
152 (************************** EXPERIMENTAL VERSION ****************************)
154 (* In this versions of auto_tac we maintain an hash table of all inspected
155 goals. We assume that the context is invariant for application.
156 To this aim, it is essential to sall hint_verbose, that in turns calls
163 | Yes of Cic.term * int
166 let inspected_goals = Hashtbl.create 503;;
168 let search_theorems_in_context status =
169 let (proof, goal) = status in
170 let module C = Cic in
171 let module R = CicReduction in
172 let module S = CicSubstitution in
173 let module PET = ProofEngineTypes in
174 let module PT = PrimitiveTactics in
175 let _,metasenv,_,_ = proof in
176 let _,context,ty = CicUtil.lookup_meta goal metasenv in
177 let rec find n = function
182 let (subst,(proof, goal_list)) =
183 PT.apply_tac_verbose ~term:(C.Rel n) status in
186 List.stable_sort (compare_goal_list proof) goal_list in
188 Some (subst,(proof, goal_list))
190 PET.Fail _ -> None in
192 Some res -> res::(find (n+1) tl)
193 | None -> find (n+1) tl)
202 let compare_goals proof goal1 goal2 =
203 let _,metasenv,_,_ = proof in
204 let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
205 let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
206 let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1
207 CicUniv.empty_ugraph in
208 let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2
209 CicUniv.empty_ugraph in
211 let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1
212 CicUniv.empty_ugraph in
216 let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2
217 CicUniv.empty_ugraph in
223 let new_search_theorems f dbd proof goal depth sign =
224 let choices = f (proof,goal)
227 (function (subst,(proof, goallist)) ->
228 (* let goallist = reorder_goals dbd sign proof goallist in *)
229 let goallist = List.sort (compare_goals proof) goallist in
230 (subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
234 exception NoOtherChoices;;
236 let is_in_metasenv goal metasenv =
239 CicUtil.lookup_meta goal metasenv in
243 let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
245 if depth = 0 then [] else
246 if List.mem ty already_seen_goals then [] else
247 let already_seen_goals = ty::already_seen_goals in
248 let facts = (depth = 1) in
249 let _,metasenv,p,_ = proof in
250 (* first of all we check if the goal has been already
252 assert (is_in_metasenv goal metasenv);
254 try Hashtbl.find inspected_goals ty
255 with Not_found -> NotYetInspected in
256 let is_meta_closed = CicUtil.is_meta_closed ty in
261 debug_print "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
262 debug_print (CicPp.ppterm ty);
265 (* if we just apply the subtitution, the type
266 is irrelevant: we may use Implicit, since it will
268 CicMetaSubst.apply_subst
269 [(goal,(ey, bo, Cic.Implicit None))] in
271 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
272 proof goal subst_in metasenv in
273 [(subst_in,(proof,[],sign))]
274 | No d when (d >= depth) ->
275 (* debug_print "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *)
276 [] (* the empty list means no choices, i.e. failure *)
279 debug_print ("CURRENT GOAL = " ^ CicPp.ppterm ty);
280 debug_print ("CURRENT PROOF = " ^ CicPp.ppterm p);
281 debug_print ("CURRENT HYP = " ^ CicPp.ppcontext ey);
283 if is_meta_closed then
284 None, Some (MetadataConstraints.signature_of ty)
285 else sign,sign in (* maybe the union ? *)
288 search_theorems_in_context dbd
289 proof goal (depth-1) new_sign in
294 (MetadataQuery.experimental_hint
295 ~dbd ~facts:facts ?signature:sign status))
296 dbd proof goal (depth-1) new_sign in
298 local_choices@global_choices in
301 (fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
303 (List.length goals1) (List.length goals2))
305 (match (auto_new dbd width already_seen_goals sorted_choices)
308 (* no proof has been found; we update the
310 (* if is_meta_closed then *)
311 Hashtbl.add inspected_goals ty (No depth);
313 | (subst,(proof,[],sign))::tl1 ->
314 (* a proof for goal has been found:
315 in order to get the proof we apply subst to
317 if is_meta_closed then
320 CicMkImplicit.identity_relocation_list_for_metavariable ey in
322 subst (Cic.Meta(goal,irl)) in
323 Hashtbl.add inspected_goals
324 ty (Yes (meta_proof,depth));
328 CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph
330 if not (cty = ty) then
332 debug_print ("ty = "^CicPp.ppterm ty);
333 debug_print ("cty = "^CicPp.ppterm cty);
336 Hashtbl.add inspected_goals
337 ty (Yes (meta_proof,depth));
341 (subst,(proof,[],sign))::tl1
345 and auto_new dbd width already_seen_goals = function
347 | (subst,(proof, goals, sign))::tl ->
348 let _,metasenv,_,_ = proof in
349 let is_in_metasenv (goal, _) =
352 CicUtil.lookup_meta goal metasenv in
355 let goals'= List.filter is_in_metasenv goals in
356 auto_new_aux dbd width already_seen_goals
357 ((subst,(proof, goals', sign))::tl)
359 and auto_new_aux dbd width already_seen_goals = function
361 | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
362 | (subst,(proof, (goal,0)::_, _))::tl ->
363 auto_new dbd width already_seen_goals tl
364 | (subst,(proof, goals, _))::tl when
365 (List.length goals) > width ->
366 auto_new dbd width already_seen_goals tl
367 | (subst,(proof, (goal,depth)::gtl, sign))::tl ->
368 let _,metasenv,p,_ = proof in
369 let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
370 match (auto_single dbd proof goal ey ty depth
371 (width - (List.length gtl)) sign already_seen_goals)
373 [] -> auto_new dbd width already_seen_goals tl
374 | (local_subst,(proof,[],sign))::tl1 ->
375 let new_subst f t = f (subst t) in
376 let is_meta_closed = CicUtil.is_meta_closed ty in
378 if is_meta_closed then
379 (new_subst local_subst,(proof,gtl,sign))::tl
383 (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
385 (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
386 auto_new dbd width already_seen_goals all_choices
390 let default_depth = 5
391 let default_width = 3
393 let auto_tac_new ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
396 let auto_tac dbd (proof,goal) =
397 Hashtbl.clear inspected_goals;
398 debug_print "Entro in Auto";
400 match (auto_new dbd width [] [id,(proof, [(goal,depth)],None)]) with
401 [] -> debug_print("Auto failed");
402 raise (ProofEngineTypes.Fail "No Applicable theorem")
403 | (_,(proof,[],_))::_ ->
404 debug_print "AUTO_TAC HA FINITO";
405 let _,_,p,_ = proof in
406 debug_print (CicPp.ppterm p);
410 ProofEngineTypes.mk_tactic (auto_tac dbd)