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)
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 *)
109 prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
110 prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
111 prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
113 (* if the goal contains metavariables we use the input
114 signature for at_most constraints *)
115 let is_meta_closed = CicUtil.is_meta_closed ty in
117 if is_meta_closed then
118 None, Some (MetadataConstraints.signature_of ty)
119 else sign,sign in (* maybe the union ? *)
122 search_theorems_in_context
123 proof goal (depth-1) [] new_sign in
129 ~dbd ~facts:facts ?signature:sign status))
130 proof goal (depth-1) [] new_sign in
131 (* we proceed depth-first on the current goal. This is
132 a MAJOR optimization, since in case of success, and
133 if the goal is meta_closed, we may just drop the alternatives
134 tl1, avoiding useless backtracking. *)
136 local_choices@global_choices in
137 (match (auto dbd all_choices)
140 | (proof,[],_)::tl1 ->
142 let gtl' = List.map fst gtl in
143 if (gtl = [] || is_meta_closed) then
148 (function (p,l,s) -> (p,l@gtl,s)) tl1)
150 (proof,gtl,sign)::tl2@tl in
153 | None -> auto dbd ((proof,gtl,sign)::tl)
157 let auto_tac ?num ~(dbd:Mysql.dbd) =
158 let auto_tac dbh (proof,goal) =
159 prerr_endline "Entro in Auto";
160 match (auto dbd [(proof, [(goal,depth)],None)]) with
161 [] -> prerr_endline("Auto failed");
162 raise (ProofEngineTypes.Fail "No Applicable theorem")
164 prerr_endline "AUTO_TAC HA FINITO";
168 ProofEngineTypes.mk_tactic (auto_tac dbd)
172 (************************** EXPERIMENTAL VERSION ****************************)
174 (* In this versions of auto_tac we maintain an hash table of all inspected
175 goals. We assume that the context is invariant for application.
176 To this aim, it is essential to sall hint_verbose, that in turns calls
183 | Yes of Cic.term * int
186 let inspected_goals = Hashtbl.create 503;;
188 let search_theorems_in_context status =
189 let (proof, goal) = status in
190 let module C = Cic in
191 let module R = CicReduction in
192 let module S = CicSubstitution in
193 let module PET = ProofEngineTypes in
194 let module PT = PrimitiveTactics in
195 let _,metasenv,_,_ = proof in
196 let _,context,ty = CicUtil.lookup_meta goal metasenv in
197 let rec find n = function
202 let (subst,(proof, goal_list)) =
203 PT.apply_tac_verbose ~term:(C.Rel n) status in
206 List.stable_sort (compare_goal_list proof) goal_list in
208 Some (subst,(proof, goal_list))
210 PET.Fail _ -> None in
212 Some res -> res::(find (n+1) tl)
213 | None -> find (n+1) tl)
221 (** splits a list of goals in three groups: closed propositional goals,
222 open propositional goals and non proposotional goals *)
225 let _,metasenv,_,_ = proof in
229 let (_, ey, ty) = CicUtil.lookup_meta g metasenv in
231 CicTypeChecker.type_of_aux' metasenv ey ty CicUniv.empty_ugraph in
233 CicReduction.are_convertible ey (Cic.Sort Cic.Prop) ty_sort u in
235 (if CicUtil.is_meta_closed ty then
241 CicUtil.Meta_not_found _ -> (c,o,g::z,n)
246 let my_weight dbd sign proof g =
248 search_theorems_in_context (proof,g) in
250 (List.map snd (MetadataQuery.experimental_hint
251 ~dbd ~facts:false ?signature:sign (proof,g))) in *)
253 (fun n (_,(_,l)) -> n+(List.length l)+1)
257 let add_weight dbd sign proof =
258 List.map (function g -> (g,my_weight dbd sign proof g))
263 (* let reorder_goals dbd sign proof goals =
266 (* let reorder_goals dbd sign proof goals =
267 let (c,o,z,n) = split proof goals
270 let reorder_goals dbd sign proof goals =
271 let (c,o,z,n) = split proof goals in
276 let l' = add_weight dbd sign proof l in
277 c@(List.map fst (List.sort (fun (_,x) (_,y) -> x - y) l'))@n@z
279 let compare_goals proof goal1 goal2 =
280 let _,metasenv,_,_ = proof in
281 let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
282 let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
283 let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1
284 CicUniv.empty_ugraph in
285 let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2
286 CicUniv.empty_ugraph in
288 let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1
289 CicUniv.empty_ugraph in
293 let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2
294 CicUniv.empty_ugraph in
300 let new_search_theorems f dbd proof goal depth sign =
301 let choices = f (proof,goal)
304 (function (subst,(proof, goallist)) ->
305 (* let goallist = reorder_goals dbd sign proof goallist in *)
306 let goallist = List.sort (compare_goals proof) goallist in
307 (subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
311 exception NoOtherChoices;;
313 let is_in_metasenv goal metasenv =
316 CicUtil.lookup_meta goal metasenv in
320 let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
322 if depth = 0 then [] else
323 if List.mem ty already_seen_goals then [] else
324 let already_seen_goals = ty::already_seen_goals in
325 let facts = (depth = 1) in
326 let _,metasenv,p,_ = proof in
327 (* first of all we check if the goal has been already
329 assert (is_in_metasenv goal metasenv);
331 try Hashtbl.find inspected_goals ty
332 with Not_found -> NotYetInspected in
333 let is_meta_closed = CicUtil.is_meta_closed ty in
338 prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
339 prerr_endline (CicPp.ppterm ty);
342 (* if we just apply the subtitution, the type
343 is irrelevant: we may use Implicit, since it will
345 CicMetaSubst.apply_subst
346 [(goal,(ey, bo, Cic.Implicit None))] in
348 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
349 proof goal subst_in metasenv in
350 [(subst_in,(proof,[],sign))]
351 | No d when (d >= depth) ->
352 (* prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *)
353 [] (* the empty list means no choices, i.e. failure *)
357 prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
358 prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
359 prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
362 if is_meta_closed then
363 None, Some (MetadataConstraints.signature_of ty)
364 else sign,sign in (* maybe the union ? *)
367 search_theorems_in_context dbd
368 proof goal (depth-1) new_sign in
369 let global_choices = [] in
374 (MetadataQuery.experimental_hint
375 ~dbd ~facts:facts ?signature:sign status))
376 dbd proof goal (depth-1) new_sign in *)
378 local_choices@global_choices in
381 (fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
383 (List.length goals1) (List.length goals2))
385 (match (auto_new dbd width already_seen_goals sorted_choices)
388 (* no proof has been found; we update the
390 (* if is_meta_closed then *)
391 Hashtbl.add inspected_goals ty (No depth);
393 | (subst,(proof,[],sign))::tl1 ->
394 (* a proof for goal has been found:
395 in order to get the proof we apply subst to
397 if is_meta_closed then
400 CicMkImplicit.identity_relocation_list_for_metavariable ey in
402 subst (Cic.Meta(goal,irl)) in
403 Hashtbl.add inspected_goals
404 ty (Yes (meta_proof,depth));
408 CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph
410 if not (cty = ty) then
412 prerr_endline ("ty = "^CicPp.ppterm ty);
413 prerr_endline ("cty = "^CicPp.ppterm cty);
416 Hashtbl.add inspected_goals
417 ty (Yes (meta_proof,depth));
421 (subst,(proof,[],sign))::tl1
425 and auto_new dbd width already_seen_goals = function
427 | (subst,(proof, goals, sign))::tl ->
428 let _,metasenv,_,_ = proof in
429 let is_in_metasenv (goal, _) =
432 CicUtil.lookup_meta goal metasenv in
435 let goals'= List.filter is_in_metasenv goals in
436 auto_new_aux dbd width already_seen_goals
437 ((subst,(proof, goals', sign))::tl)
439 and auto_new_aux dbd width already_seen_goals = function
441 | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
442 | (subst,(proof, (goal,0)::_, _))::tl ->
443 auto_new dbd width already_seen_goals tl
444 | (subst,(proof, goals, _))::tl when
445 (List.length goals) > width+1 ->
446 auto_new dbd width already_seen_goals tl
447 | (subst,(proof, (goal,depth)::gtl, sign))::tl ->
448 let maxdepthgoals,othergoals =
451 (g,d)::l when d=depth -> aux (g::acc) l
454 let _,metasenv,p,_ = proof in
455 let len1 = List.length maxdepthgoals in
456 let maxdepthgoals = reorder_goals dbd sign proof maxdepthgoals in
457 let len2 = List.length maxdepthgoals in
458 match maxdepthgoals with
460 ("caso sospetto " ^ (string_of_int (List.length othergoals)) ^ " " ^ string_of_int depth);
462 width already_seen_goals((subst,(proof, othergoals, sign))::tl)
464 let gtl = (List.map (fun x->(x,depth)) tgs)@othergoals in
469 CicUtil.lookup_meta goal metasenv in
476 match (auto_single dbd proof goal ey ty depth
477 (width - (List.length gtl) - (len1-len2)) sign already_seen_goals)
479 [] -> auto_new dbd width already_seen_goals tl
480 | (local_subst,(proof,[],sign))::tl1 ->
481 let new_subst f t = f (subst t) in
482 let is_meta_closed = CicUtil.is_meta_closed ty in
484 if is_meta_closed then
485 (new_subst local_subst,(proof,gtl,sign))::tl
489 (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
491 (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
492 auto_new dbd width already_seen_goals all_choices
495 | None -> prerr_endline "caso none";
497 dbd width already_seen_goals ((subst,(proof, gtl, sign))::tl)
502 let auto_tac_new ~(dbd:Mysql.dbd) =
503 let auto_tac dbd (proof,goal) =
504 Hashtbl.clear inspected_goals;
505 prerr_endline "Entro in Auto";
507 match (auto_new dbd width [] [id,(proof, [(goal,depth)],None)]) with
508 [] -> prerr_endline("Auto failed");
509 raise (ProofEngineTypes.Fail "No Applicable theorem")
510 | (_,(proof,[],_))::_ ->
511 prerr_endline "AUTO_TAC HA FINITO";
512 let _,_,p,_ = proof in
513 prerr_endline (CicPp.ppterm p);
517 ProofEngineTypes.mk_tactic (auto_tac dbd)