2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
17 let debug_print ?(depth=0) s =
18 if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
19 let debug_do f = if !debug then f () else ()
21 open Continuationals.Stack
23 module Ast = CicNotationPt
25 (* =================================== paramod =========================== *)
26 let auto_paramod ~params:(l,_) status goal =
27 let gty = get_goalty status goal in
28 let n,h,metasenv,subst,o = status#obj in
29 let status,t = term_of_cic_term status gty (ctx_of gty) in
33 let status, t = disambiguate status (ctx_of gty) t None in
34 let status, ty = typeof status (ctx_of t) t in
35 let status, t = term_of_cic_term status t (ctx_of gty) in
36 let status, ty = term_of_cic_term status ty (ctx_of ty) in
37 (status, (t,ty) :: l))
41 NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
43 | [] -> raise (Error (lazy "no proof found",None))
44 | (pt, _, metasenv, subst)::_ ->
45 let status = status#set_obj (n,h,metasenv,subst,o) in
46 instantiate status goal (mk_cic_term (ctx_of gty) pt)
49 let auto_paramod_tac ~params status =
50 NTactics.distribute_tac (auto_paramod ~params) status
53 (* =================================== auto =========================== *)
54 (****************** AUTO ********************
56 let calculate_timeout flags =
57 if flags.timeout = 0. then
58 (debug_print (lazy "AUTO WITH NO TIMEOUT");
59 {flags with timeout = infinity})
63 let is_equational_case goalty flags =
64 let ensure_equational t =
65 if is_an_equational_goal t then true
68 (flags.use_paramod && is_an_equational_goal goalty) ||
69 (flags.use_only_paramod && ensure_equational goalty)
72 type menv = Cic.metasenv
73 type subst = Cic.substitution
74 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
75 let candidate_no = ref 0;;
76 type candidate = int * Cic.term Lazy.t
77 type cache = AutoCache.cache
80 (* the goal (mainly for depth) and key of the goal *)
81 goal * AutoCache.cache_key
83 (* goal has to be proved *)
85 (* goal has to be cached as a success obtained using candidate as the first
87 | S of goal * AutoCache.cache_key * candidate * int
89 (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
90 menv * subst * int * op list * op list * fail list
92 (* list of computations that may lead to the solution: all op list will
93 * end with the same (S(g,_)) *)
96 (* menv, subst, alternatives, tables, cache *)
97 | Proved of menv * subst * elem list * AutomationCache.tables * cache
98 | Gaveup of AutomationCache.tables * cache
101 (* the status exported to the external observer *)
103 (* context, (goal,candidate) list, and_list, history *)
104 Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
105 (int * Cic.term * int) list * Cic.term Lazy.t list
108 let rec aux acc = function
109 | (D g)::tl -> aux (acc@[g]) tl
115 let calculate_goal_ty (goalno,_,_) s m =
117 let _,cc,goalty = CicUtil.lookup_meta goalno m in
118 (* XXX applicare la subst al contesto? *)
119 Some (cc, CicMetaSubst.apply_subst s goalty)
120 with CicUtil.Meta_not_found i when i = goalno -> None
123 let calculate_closed_goal_ty (goalno,_,_) s =
125 let cc,_,goalty = List.assoc goalno s in
126 (* XXX applicare la subst al contesto? *)
127 Some (cc, CicMetaSubst.apply_subst s goalty)
132 let pp_status ctx status =
134 let names = Utils.names_of_context ctx in
137 ProofEngineReduction.replace
138 ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
139 ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
143 let string_of_do m s (gi,_,_ as g) d =
144 match calculate_goal_ty g s m with
145 | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
146 | None -> Printf.sprintf "D(%d, _, %d)" gi d
148 let string_of_s m su k (ci,ct) gi =
149 Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
151 let string_of_ol m su l =
155 | D (g,d,s) -> string_of_do m su (g,d,s) d
156 | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
159 let string_of_fl m s fl =
161 (List.map (fun ((i,_,_),ty) ->
162 Printf.sprintf "(%d, %s)" i (pp ty)) fl)
164 let rec aux = function
166 | (m,s,_,_,ol,fl)::tl ->
167 Printf.eprintf "< [%s] ;;; [%s]>\n"
168 (string_of_ol m s ol) (string_of_fl m s fl);
171 Printf.eprintf "-------------------------- status -------------------\n";
173 Printf.eprintf "-----------------------------------------------------\n";
176 let auto_status = ref [] ;;
177 let auto_context = ref [];;
178 let in_pause = ref false;;
179 let pause b = in_pause := b;;
180 let cond = Condition.create ();;
181 let mutex = Mutex.create ();;
182 let hint = ref None;;
183 let prune_hint = ref [];;
185 let step _ = Condition.signal cond;;
186 let give_hint n = hint := Some n;;
187 let give_prune_hint hint =
188 prune_hint := hint :: !prune_hint
195 Condition.wait cond mutex;
200 let get_auto_status _ =
201 let status = !auto_status in
202 let and_list,elems,last =
205 | (m,s,_,don,gl,fail)::tl ->
208 (fun (id,d,_ as g) ->
209 match calculate_goal_ty g s m with
210 | Some (_,x) -> Some (id,x,d) | None -> None)
214 (* these are the S goalsin the or list *)
217 (fun (m,s,_,don,gl,fail) ->
219 (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
223 (* this function eats id from a list l::[id,x] returning x, l *)
224 let eat_tail_if_eq id l =
225 let rec aux (s, l) = function
227 | ((id1,_,_),k1,c)::tl when id = id1 ->
229 | None -> aux (Some c,l) tl
230 | Some _ -> assert false)
231 | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
233 let c, l = aux (None, []) l in
236 let eat_in_parallel id l =
237 let rec aux (b,eaten, new_l as acc) l =
241 match eat_tail_if_eq id l with
242 | None, l -> aux (b@[false], eaten, new_l@[l]) tl
243 | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
247 let rec eat_all rows l =
251 match List.rev elem with
252 | ((to_eat,depth,_),k,_)::next_lunch ->
253 let b, eaten, l = eat_in_parallel to_eat l in
254 let eaten = HExtlib.list_uniq eaten in
255 let eaten = List.rev eaten in
256 let b = true (* List.hd (List.rev b) *) in
257 let rows = rows @ [to_eat,k,b,depth,eaten] in
259 | [] -> eat_all rows or_list
261 eat_all [] (List.rev orlist)
265 (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
268 (* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
269 and_list, rows, history
271 !auto_context, elems, and_list, last
274 (* Works if there is no dependency over proofs *)
275 let is_a_green_cut goalty =
276 CicUtil.is_meta_closed goalty
278 let rec first_s = function
279 | (D _)::tl -> first_s tl
280 | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
283 let list_union l1 l2 =
284 (* TODO ottimizzare compare *)
285 HExtlib.list_uniq (List.sort compare (l1 @ l1))
287 let rec eq_todo l1 l2 =
289 | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
290 | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
291 when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
292 if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
296 let eat_head todo id fl orlist =
297 let rec aux acc = function
299 | (m, s, _, _, todo1, fl1)::tl as orlist ->
301 match first_s todo1 with
302 | None -> orlist, acc
303 | Some (((gno,_,_),_,_,_), todo11) ->
304 (* TODO confronto tra todo da ottimizzare *)
305 if gno = id && eq_todo todo11 todo then
306 aux (list_union fl1 acc) tl
314 let close_proof p ty menv context =
316 List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
318 let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
319 naif_closure p menv context
321 (* XXX capire bene quando aggiungere alla cache *)
322 let add_to_cache_and_del_from_orlist_if_green_cut
323 g s m cache key todo orlist fl ctx size minsize
325 let cache = cache_remove_underinspection cache key in
326 (* prima per fare la irl usavamo il contesto vero e proprio e non quello
328 match calculate_closed_goal_ty g s with
329 | None -> assert false
330 | Some (canonical_ctx , gty) ->
331 let goalno,depth,sort = g in
332 let irl = mk_irl canonical_ctx in
333 let goal = Cic.Meta(goalno, irl) in
334 let proof = CicMetaSubst.apply_subst s goal in
335 let green_proof, closed_proof =
336 let b = is_a_green_cut proof in
338 b, (* close_proof proof gty m ctx *) proof
342 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
343 if is_a_green_cut key then
344 (* if the initia goal was closed, we cut alternatives *)
345 let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
346 let orlist, fl = eat_head todo goalno fl orlist in
348 if size < minsize then
349 (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
351 (* if the proof is closed we cache it *)
352 if green_proof then cache_add_success cache key proof
353 else (* cache_add_success cache key closed_proof *)
354 (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
356 cache, orlist, fl, true
359 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
360 if size < minsize then
361 (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
362 (* if the substituted goal and the proof are closed we cache it *)
363 if is_a_green_cut gty then
364 if green_proof then cache_add_success cache gty proof
365 else (* cache_add_success cache gty closed_proof *)
366 (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
370 CicTypeChecker.type_of_aux' ~subst:s
371 m ctx closed_proof CicUniv.oblivion_ugraph
373 if is_a_green_cut ty then
374 cache_add_success cache ty closed_proof
377 | CicTypeChecker.TypeCheckerFailure _ ->*)
378 (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
380 cache, orlist, fl, false
382 let close_failures (fl : fail list) (cache : cache) =
384 (fun cache ((gno,depth,_),gty) ->
385 if CicUtil.is_meta_closed gty then
386 ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
387 cache_add_failure cache gty depth)
392 let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
393 let entry = goalno, (canonical_ctx, t,ty) in
394 assert_subst_are_disjoint subst [entry];
395 let subst = entry :: subst in
397 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
402 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
403 None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
407 tables cache depth fake_proof goalno goalty subst context
410 let active,passive,bag = tables in
411 let ppterm = ppterm context in
412 let status = (fake_proof,goalno) in
413 if flags.use_only_paramod then
415 debug_print (lazy ("PARAMODULATION SU: " ^
416 string_of_int goalno ^ " " ^ ppterm goalty ));
417 let goal_steps, saturation_steps, timeout =
418 max_int,max_int,flags.timeout
421 Saturation.given_clause bag status active passive
422 goal_steps saturation_steps timeout
424 | None, active, passive, bag ->
425 [], (active,passive,bag), cache, flags
426 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
428 assert_subst_are_disjoint subst subst';
429 let subst = subst@subst' in
431 order_new_goals metasenv subst open_goals ppterm
434 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
437 [(!candidate_no,proof),metasenv,subst,open_goals],
438 (active,passive,bag), cache, flags
442 debug_print (lazy ("NARROWING DEL GOAL: " ^
443 string_of_int goalno ^ " " ^ ppterm goalty ));
444 let goal_steps, saturation_steps, timeout =
448 Saturation.solve_narrowing bag status active passive goal_steps
450 | None, active, passive, bag ->
451 [], (active,passive,bag), cache, flags
452 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
454 assert_subst_are_disjoint subst subst';
455 let subst = subst@subst' in
457 order_new_goals metasenv subst open_goals ppterm
460 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
463 [(!candidate_no,proof),metasenv,subst,open_goals],
464 (active,passive,bag), cache, flags
468 let params = ([],["use_context","false"]) in
469 let automation_cache = {
470 AutomationCache.tables = tables ;
471 AutomationCache.univ = Universe.empty; }
474 let ((_,metasenv,subst,_,_,_),open_goals) =
476 solve_rewrite ~params ~automation_cache
479 let proof = lazy (Cic.Meta (-1,[])) in
480 [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
481 with ProofEngineTypes.Fail _ -> [], tables, cache, flags
483 let res = Saturation.all_subsumed bag status active passive in
486 (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
487 assert_subst_are_disjoint subst subst';
488 let subst = subst@subst' in
490 order_new_goals metasenv subst open_goals ppterm
493 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
496 (!candidate_no,proof),metasenv,subst,open_goals)
499 res', (active,passive,bag), cache, flags
506 List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
507 let p1 = List.length (prop_only l1) in
508 let p2 = List.length (prop_only l2) in
509 if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
513 let try_candidate dbd
514 goalty tables subst fake_proof goalno depth context cand
516 let ppterm = ppterm context in
518 let actives, passives, bag = tables in
519 let (_,metasenv,subst,_,_,_), open_goals =
520 ProofEngineTypes.apply_tactic
521 (PrimitiveTactics.apply_tac ~term:cand)
524 let tables = actives, passives,
525 Equality.push_maxmeta bag
526 (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
528 debug_print (lazy (" OK: " ^ ppterm cand));
529 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
530 let open_goals = order_new_goals metasenv subst open_goals ppterm in
531 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
533 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
535 | ProofEngineTypes.Fail s -> None,tables
536 | CicUnification.Uncertain s -> None,tables
539 let applicative_case dbd
540 tables depth subst fake_proof goalno goalty metasenv context
541 signature universe cache flags
545 | Cic.Appl (hd::tl) ->
546 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
549 let goalty_aux = goalty in
551 get_candidates flags.skip_trie_filtering universe cache goalty_aux
553 (* if the goal is an equality we skip the congruence theorems
555 if is_equational_case goalty flags
556 then List.filter not_default_eq_term candidates
559 let candidates = List.filter (only signature context metasenv) candidates
563 (fun (tables,elems) cand ->
565 try_candidate dbd goalty
566 tables subst fake_proof goalno depth context cand
568 | None, tables -> tables, elems
569 | Some x, tables -> tables, x::elems)
570 (tables,[]) candidates
572 let elems = sort_new_elems elems in
576 let try_smart_candidate dbd
577 goalty tables subst fake_proof goalno depth context cand
579 let ppterm = ppterm context in
581 let params = ([],[]) in
582 let automation_cache = {
583 AutomationCache.tables = tables ;
584 AutomationCache.univ = Universe.empty; }
586 debug_print (lazy ("candidato per " ^ string_of_int goalno
587 ^ ": " ^ CicPp.ppterm cand));
589 let (_,metasenv,subst,_,_,_) = fake_proof in
590 prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
591 prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
593 let ((_,metasenv,subst,_,_,_),open_goals) =
594 apply_smart ~dbd ~term:cand ~params ~automation_cache
597 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
598 let open_goals = order_new_goals metasenv subst open_goals ppterm in
599 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
601 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
603 | ProofEngineTypes.Fail s -> None,tables
604 | CicUnification.Uncertain s -> None,tables
607 let smart_applicative_case dbd
608 tables depth subst fake_proof goalno goalty metasenv context signature
613 | Cic.Appl (hd::tl) ->
614 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
617 let smart_candidates =
618 get_candidates flags.skip_trie_filtering universe cache goalty_aux
621 get_candidates flags.skip_trie_filtering universe cache goalty
623 let smart_candidates =
625 (fun x -> not(List.mem x candidates)) smart_candidates
628 (lazy ("smart_candidates" ^ " = " ^
629 (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
630 debug_print debug_msg;
631 let candidates = List.filter (only signature context metasenv) candidates in
632 let smart_candidates =
633 List.filter (only signature context metasenv) smart_candidates
636 let penalty cand depth =
637 if only signature context metasenv cand then depth else ((prerr_endline (
638 "penalizzo " ^ CicPp.ppterm cand));depth -1)
643 (fun (tables,elems) cand ->
645 try_candidate dbd goalty
646 tables subst fake_proof goalno depth context cand
649 (* if normal application fails we try to be smart *)
650 (match try_smart_candidate dbd goalty
651 tables subst fake_proof goalno depth context cand
653 | None, tables -> tables, elems
654 | Some x, tables -> tables, x::elems)
655 | Some x, tables -> tables, x::elems)
656 (tables,[]) candidates
658 let tables, smart_elems =
660 (fun (tables,elems) cand ->
662 try_smart_candidate dbd goalty
663 tables subst fake_proof goalno depth context cand
665 | None, tables -> tables, elems
666 | Some x, tables -> tables, x::elems)
667 (tables,[]) smart_candidates
669 let elems = sort_new_elems (elems @ smart_elems) in
673 let equational_and_applicative_case dbd
674 signature universe flags m s g gty tables cache context
676 let goalno, depth, sort = g in
677 let fake_proof = mk_fake_proof m s g gty context in
678 if is_equational_case gty flags then
679 let elems,tables,cache, flags =
680 equational_case tables cache
681 depth fake_proof goalno gty s context flags
683 let more_elems, tables, cache =
684 if flags.use_only_paramod then
688 tables depth s fake_proof goalno
689 gty m context signature universe cache flags
691 elems@more_elems, tables, cache, flags
693 let elems, tables, cache =
694 match LibraryObjects.eq_URI () with
696 smart_applicative_case dbd tables depth s fake_proof goalno
697 gty m context signature universe cache flags
699 applicative_case dbd tables depth s fake_proof goalno
700 gty m context signature universe cache flags
702 elems, tables, cache, flags
704 let rec condition_for_hint i = function
706 | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
707 | _::tl -> condition_for_hint i tl
709 let prunable_for_size flags s m todo =
710 let rec aux b = function
711 | (S _)::tl -> aux b tl
712 | (D (_,_,T))::tl -> aux b tl
714 (match calculate_goal_ty g s m with
716 | Some (canonical_ctx, gty) ->
719 ~consider_metas:false ~count_metas_occurrences:true gty in
720 let newb = b || gsize > flags.maxgoalsizefactor in
727 let prunable ty todo =
728 let rec aux b = function
729 | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
730 | (D (_,_,T))::tl -> aux b tl
738 let prunable menv subst ty todo =
739 let rec aux = function
740 | (S(_,k,_,_))::tl ->
741 (match Equality.meta_convertibility_subst k ty menv with
744 no_progress variant tl (* || aux tl*))
745 | (D (_,_,T))::tl -> aux tl
747 and no_progress variant = function
748 | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
749 | D ((n,_,P) as g)::tl ->
750 (match calculate_goal_ty g subst menv with
751 | None -> no_progress variant tl
753 (match calculate_goal_ty g variant menv with
754 | None -> assert false
756 if gty = gty' then no_progress variant tl
758 (prerr_endline (string_of_int n);
759 prerr_endline (CicPp.ppterm gty);
760 prerr_endline (CicPp.ppterm gty');
761 prerr_endline "---------- subst";
762 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
763 prerr_endline "---------- variant";
764 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
765 prerr_endline "---------- menv";
766 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
767 no_progress variant tl) *)
769 | _::tl -> no_progress variant tl
774 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
776 HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
778 List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
780 let filter_prune_hint c l =
781 let prune = !prune_hint in
782 prune_hint := []; (* possible race... *)
783 if prune = [] then c,l
785 cache_reset_underinspection c,
786 List.filter (condition_for_prune_hint prune) l
792 auto_all_solutions dbd tables universe cache context metasenv gl flags
797 MetadataConstraints.UriManagerSet.union set
798 (MetadataQuery.signature_of metasenv g)
800 MetadataConstraints.UriManagerSet.empty gl
802 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
805 (fun (x,s) -> D (x,flags.maxdepth,s)) goals
807 let elems = [metasenv,[],1,[],goals,[]] in
808 let rec aux tables solutions cache elems flags =
809 match auto_main dbd tables context flags signature universe cache elems with
810 | Gaveup (tables,cache) ->
811 solutions,cache, tables
812 | Proved (metasenv,subst,others,tables,cache) ->
813 if Unix.gettimeofday () > flags.timeout then
814 ((subst,metasenv)::solutions), cache, tables
816 aux tables ((subst,metasenv)::solutions) cache others flags
818 let rc = aux tables [] cache elems flags in
820 | [],cache,tables -> [],cache,tables
821 | solutions, cache,tables ->
824 (fun (subst,newmetasenv) ->
826 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
828 if opened = [] then Some subst else None)
831 solutions,cache,tables
834 (******************* AUTO ***************)
837 let auto dbd flags metasenv tables universe cache context metasenv gl =
838 let initial_time = Unix.gettimeofday() in
842 MetadataConstraints.UriManagerSet.union set
843 (MetadataQuery.signature_of metasenv g)
845 MetadataConstraints.UriManagerSet.empty gl
847 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
848 let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
849 let elems = [metasenv,[],1,[],goals,[]] in
850 match auto_main dbd tables context flags signature universe cache elems with
851 | Proved (metasenv,subst,_, tables,cache) ->
853 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
854 Some (subst,metasenv), cache
855 | Gaveup (tables,cache) ->
857 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
861 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
862 let flags = flags_of_params params () in
863 let use_library = flags.use_library in
864 let universe, tables, cache =
865 init_cache_and_tables
866 ~dbd ~use_library ~use_context:(not flags.skip_context)
867 automation_cache univ (proof, goal)
869 let _,metasenv,subst,_,_, _ = proof in
870 let _,context,goalty = CicUtil.lookup_meta goal metasenv in
871 let signature = MetadataQuery.signature_of metasenv goal in
876 CicTypeChecker.type_of_aux' metasenv context t
877 CicUniv.oblivion_ugraph
879 MetadataConstraints.UriManagerSet.union set
880 (MetadataConstraints.constants_of ty)
885 if flags.close_more then
887 tables context (proof, goal)
888 (auto_all_solutions dbd) signature universe cache
890 let initial_time = Unix.gettimeofday() in
891 let (_,oldmetasenv,_,_,_, _) = proof in
894 metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
896 match auto_main dbd tables context flags signature universe cache [elem] with
897 | Proved (metasenv,subst,_, tables,cache) ->
899 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
901 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
902 proof goal subst metasenv
905 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
906 ~newmetasenv:metasenv
909 | Gaveup (tables,cache) ->
912 string_of_float(Unix.gettimeofday()-.initial_time)));
913 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
918 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
920 let keys_of_term status t =
921 let status, orig_ty = typeof status (ctx_of t) t in
922 let _, ty, _ = saturate ~delta:max_int status orig_ty in
925 let _, ty = term_of_cic_term status ty (ctx_of ty) in
927 | NCic.Const (NReference.Ref (_,NReference.Def h))
928 | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_)
930 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
937 let mk_th_cache status gl =
939 (fun (status, acc) g ->
940 let gty = get_goalty status g in
941 let ctx = ctx_of gty in
942 debug_print(lazy("th cache for: "^ppterm status gty));
943 debug_print(lazy("th cache in: "^ppcontext status ctx));
944 if List.mem_assq ctx acc then status, acc else
945 let idx = InvRelDiscriminationTree.empty in
948 (fun (status, i, idx) _ ->
949 let t = mk_cic_term ctx (NCic.Rel i) in
950 debug_print(lazy("indexing: "^ppterm status t));
951 let status, keys = keys_of_term status t in
953 List.fold_left (fun idx k ->
954 InvRelDiscriminationTree.index idx k t) idx keys
959 status, (ctx, idx) :: acc)
963 let add_to_th t c ty =
964 let key_c = ctx_of t in
965 if not (List.mem_assq key_c c) then
966 (key_c ,InvRelDiscriminationTree.index
967 InvRelDiscriminationTree.empty ty t ) :: c
969 let rec replace = function
971 | (x, idx) :: tl when x == key_c ->
972 (x, InvRelDiscriminationTree.index idx ty t) :: tl
973 | x :: tl -> x :: replace tl
978 let pp_idx status idx =
979 InvRelDiscriminationTree.iter idx
981 debug_print(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
983 (fun t -> debug_print(lazy("\t"^ppterm status t)))
990 debug_print(lazy( "-----------------------------------------------"));
991 debug_print(lazy( (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx)));
992 debug_print(lazy( "||====> "));
997 let search_in_th gty th =
998 let c = ctx_of gty in
999 let rec aux acc = function
1000 | [] -> Ncic_termSet.elements acc
1003 let idx = List.assq k th in
1004 let acc = Ncic_termSet.union acc
1005 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
1008 with Not_found -> aux acc tl
1010 aux Ncic_termSet.empty c
1012 type cache_examination_result =
1015 | `Succeded of NCic.term
1020 type goal = int * sort (* goal, depth, sort *)
1021 type fail = goal * cic_term
1022 type candidate = int * Ast.term (* unique candidate number, candidate *)
1025 (* goal has to be proved *)
1027 (* goal has to be cached as a success obtained using candidate as the first
1029 | S of goal * (#tac_status as 'a)
1030 (* * cic_term * candidate (* int was minsize *) *)
1031 | L of goal * (#tac_status as 'a)
1033 let pp_goal (g,_) = string_of_int g
1034 let pp_item = function
1035 | D g -> "D" ^ pp_goal g
1036 | S (g,_) -> "S" ^ pp_goal g
1037 | L (g,_) -> "L" ^ pp_goal g
1040 do_types : bool; (* solve goals in Type *)
1047 type 'a tree_status = #tac_status as 'a * int * int
1048 type 'a tree_item = 'a op
1051 (AndOrTree.andT, 'a tree_status, 'a tree_item) AndOrTree.position
1053 (AndOrTree.orT, 'a tree_status, 'a tree_item) AndOrTree.position
1055 type 'a auto_status = 'a and_pos * th_cache
1057 type 'a auto_result =
1059 | Proved of (#tac_status as 'a) * 'a auto_status option (* alt. proofs *)
1061 let close_failures _ c = c;;
1062 let prunable _ _ _ = false;;
1063 let cache_examine cache gty = `Notfound;;
1064 let put_in_subst s _ _ _ = s;;
1065 let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;;
1066 let cache_add_underinspection c _ _ = c;;
1067 let equational_case _ _ _ _ _ _ = [];;
1068 let only _ _ _ = true;;
1070 let candidate_no = ref 0;;
1072 let sort_new_elems l =
1073 List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l
1076 let try_candidate flags depth status t g =
1078 debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
1079 let status = NTactics.focus_tac [g] status in
1080 let status = NTactics.apply_tac ("",0,t) status in
1081 let open_goals = head_goals status#stack in
1083 (lazy ("success: "^String.concat " "(List.map string_of_int open_goals)));
1084 if List.length open_goals > flags.maxwidth ||
1085 (depth = flags.maxdepth && open_goals <> []) then
1086 (debug_print ~depth (lazy "pruned immediately"); None)
1089 Some ((!candidate_no,t),status,open_goals))
1090 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1093 let rec mk_irl n = function
1095 | _ :: tl -> NCic.Rel n :: mk_irl (n+1) tl
1098 let get_candidates status cache_th signature gty =
1099 let universe = status#auto_cache in
1100 let context = ctx_of gty in
1101 let _, raw_gty = term_of_cic_term status gty context in
1103 NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe raw_gty
1106 List.filter (only signature context)
1107 (NDiscriminationTree.TermSet.elements cands)
1110 let _status, t = term_of_cic_term status t context in Ast.NCic t)
1111 (search_in_th gty cache_th)
1113 List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
1116 let applicative_case depth signature status flags g gty cache =
1117 let candidates = get_candidates status cache signature gty in
1119 (lazy ("candidates: " ^ string_of_int (List.length candidates)));
1123 match try_candidate flags depth status cand g with
1125 | Some x -> x::elems)
1130 let calculate_goal_ty (goalno,_) status =
1131 try Some (get_goalty status goalno)
1132 with Error _ -> None
1135 let equational_and_applicative_case
1136 signature flags status g depth gty cache
1139 if false (*is_equational_case gty flags*) then
1142 signature status flags g gty cache
1145 applicative_case depth
1146 signature status flags g gty cache
1151 (*match LibraryObjects.eq_URI () with
1153 smart_applicative_case dbd tables depth s fake_proof goalno
1154 gty m context signature universe cache flags
1156 applicative_case depth
1157 signature status flags g gty cache
1162 List.map (fun c,s,gl ->
1163 c,1,1,s,List.map (fun i ->
1165 match calculate_goal_ty (i,()) s with
1166 | None -> assert false
1168 let _, sort = typeof s (ctx_of gty) gty in
1169 match term_of_cic_term s sort (ctx_of sort) with
1170 | _, NCic.Sort NCic.Prop -> P
1175 let elems = sort_new_elems elems in
1181 let rec aux acc = function
1182 | (D g)::tl -> aux (acc@[g]) tl
1183 | (S _|L _)::tl -> aux acc tl
1189 List.filter (function (_,P) -> true | _ -> false) l
1192 let rec guess_name name ctx =
1193 if name = "_" then guess_name "auto" ctx else
1194 if not (List.mem_assoc name ctx) then name else
1195 guess_name (name^"'") ctx
1198 let intro_case status gno gty depth cache name =
1199 let status = NTactics.focus_tac [gno] status in
1200 let status = NTactics.intro_tac (guess_name name (ctx_of gty)) status in
1201 let open_goals = head_goals status#stack in
1202 assert (List.length open_goals = 1);
1203 let open_goal = List.hd open_goals in
1204 let ngty = get_goalty status open_goal in
1205 let ctx = ctx_of ngty in
1206 let t = mk_cic_term ctx (NCic.Rel 1) in
1207 let status, keys = keys_of_term status t in
1208 let cache = List.fold_left (add_to_th t) cache keys in
1209 debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
1211 (* XXX calculate the sort *)
1212 [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[open_goal,P]],
1216 let do_something signature flags s gno depth gty cache =
1217 let _s, raw_gty = term_of_cic_term s gty (ctx_of gty) in
1219 | NCic.Prod (name,_,_) -> intro_case s gno gty depth cache name
1221 equational_and_applicative_case signature flags s gno depth gty cache
1225 module Z = AndOrTree
1227 let img_counter = ref 0 ;;
1230 let file = ("/tmp/a"^string_of_int !img_counter^".dot") in
1231 debug_print (lazy("generating " ^ file));
1233 let oc = open_out file in
1234 let fmt = Format.formatter_of_out_channel oc in
1235 GraphvizPp.Dot.header fmt;
1236 Z.dump pp_item pos fmt;
1237 GraphvizPp.Dot.trailer fmt;
1238 Format.fprintf fmt "@?";
1240 ignore(Sys.command ("dot -Tpng "^file^" > "^file^".png"));
1241 (*ignore(Sys.command ("eog "^file^".png"))*))
1244 let rightmost_bro pred pos =
1245 let rec last acc pos =
1246 let acc = if pred pos then Some pos else acc in
1247 match Z.right pos with
1249 | Some pos -> last acc pos
1254 let leftmost_bro pred pos =
1256 if pred pos then Some pos else
1257 match Z.right pos with
1259 | Some pos -> fst pos
1264 let rec first_left_mark_L_as_D pred pos =
1269 match Z.getA pos with
1271 Z.inject T.Nil (Z.setA s (D g) pos)
1274 match Z.left pos with
1277 first_left_mark_L_as_D pred pos
1281 match Z.getO pos with
1283 | D _ | L _ -> false
1288 match Z.getA pos with
1290 | _,D _ | _,L _ -> false
1293 let is_not_oS x = not (is_oS x);;
1294 let is_not_aS x = not (is_aS x);;
1296 let is_oL pos = match Z.getO pos with L _ -> true | _ -> false ;;
1297 let is_aL pos = match Z.getA pos with _,L _ -> true | _ -> false ;;
1299 let is_not_oL x = not (is_oL x) ;;
1300 let is_not_aL x = not (is_aL x) ;;
1302 let rec forall_left pred pos =
1303 match Z.left pos with
1305 | Some pos -> if pred pos then forall_left pred pos else false
1309 let rec product = function
1311 | ((g,s) :: tl) as l -> (s,List.map fst l) :: product tl
1314 let has_no_alternatives (pos : 'a and_pos) =
1315 match Z.getA pos with
1320 let rec collect_left_up (pos : 'a and_pos) =
1321 match Z.left pos with
1323 (match Z.getA pos with
1324 | _, L (g,s) -> (g,s) :: collect_left_up pos
1327 match Z.upA pos with
1328 | None -> [] (* root *)
1329 | Some pos -> collect_left_up (Z.upO pos)
1332 let compute_failed_goals (pos : 'a and_pos) =
1333 let curr = match Z.getA pos with (s,_,_),D g -> (g,s) | _ -> assert false in
1334 product (List.rev (curr :: collect_left_up pos) )
1338 debug_print (lazy("CACHE FAILURES/UNDERINSPECTION"));
1339 List.iter (fun (s,gl) ->
1340 debug_print (lazy("FAIL: " ^
1341 String.concat " , " (List.map (fun g ->
1342 match calculate_goal_ty g s with
1346 let _,_,_,subst,_ = s#obj in
1347 let _,cc,_,ty = NCicUtils.lookup_subst i subst in
1348 let ty = mk_cic_term cc ty in
1349 string_of_int i^":"^ppterm s ty
1350 with NCicUtils.Subst_not_found _ -> "XXXX")
1352 let s, gty = apply_subst s (ctx_of gty) gty in
1353 string_of_int (fst g)^":"^ppterm s gty) gl))))
1358 match Z.getA pos with
1361 (match calculate_goal_ty g s with
1363 | Some gty -> metas_of_term s gty = [])
1364 | _, L _ -> assert false
1367 let auto_main flags signature (pos : 'a and_pos) cache =
1368 let solved g depth size s (pos : 'a and_pos) =
1369 Z.inject (T.Node(`Or,[D g,T.Node(`And(s,depth,size),[])])) pos
1371 let failed (pos : 'a and_pos) =
1372 pp_failures (compute_failed_goals pos);
1373 Z.inject (T.Node(`Or,[])) pos
1376 let rec next ~unfocus (pos : 'a and_pos) cache =
1377 (* TODO: process USER HINT is any *)
1378 match Z.downA pos with
1379 | Z.Unexplored -> attack pos cache (Z.getA pos)
1380 | Z.Alternatives pos -> nextO ~unfocus pos cache
1382 and nextO ~unfocus (pos : 'a or_pos) cache =
1383 match Z.getO pos with
1384 | S _ | L _ -> assert false (* XXX set to Nil when backtrack *)
1386 match Z.downO pos with
1387 | Z.Solution (s,_,_) -> move_solution_up ~unfocus true s pos cache
1388 | Z.Todo pos -> next ~unfocus:true pos cache
1390 and next_choice_point (pos : 'a and_pos) cache =
1392 let rec global_choice_point (pos : 'a and_pos) : 'a auto_result =
1393 (* prerr_endline "global"; show pos; *)
1394 match Z.upA pos with
1397 let alts = Z.inject T.Nil alts in
1399 match Z.getO alts with
1400 | S (s,g) -> Z.setO (L (s,g)) alts
1401 | D (g) -> Z.setO (L (g,Obj.magic g)) alts
1402 (* L (and other marks) for OR should have no arguments *)
1403 | L _ -> assert false
1405 match Z.right alts with
1407 let upalts = Z.upO alts in
1408 let upalts = Z.inject T.Nil upalts in
1410 match Z.getA upalts with
1411 | s,S (a,b) -> Z.setA s (L (a,b)) upalts
1412 | _,L _ -> assert false
1413 | s,D (a) -> Z.setA s (L (a,Obj.magic a)) upalts
1417 match Z.downO pos with
1418 | Z.Solution (s,_,_) ->
1419 move_solution_up ~unfocus:false true s pos cache
1420 | Z.Todo pos -> next ~unfocus:true pos cache
1422 and backtrack (pos : 'a and_pos) : 'a auto_result =
1423 (* prerr_endline "backtrack"; show pos; *)
1424 let pos = Z.inject T.Nil pos in
1426 match Z.getA pos with
1427 | s,D g | s, S (g,_) | s,L(g,_) -> Z.setA s (D g) pos
1429 match first_left_mark_L_as_D is_aS pos with
1430 | None -> global_choice_point pos
1432 let rec local_choice_point pos =
1433 (* prerr_endline "local"; show pos; *)
1434 match Z.downA pos with
1435 | Z.Unexplored -> attack pos cache (Z.getA pos)
1436 | Z.Alternatives alts ->
1437 match leftmost_bro is_not_oL alts with
1438 | None -> assert false (* is not L, thus has alternatives *)
1440 let is_D = is_not_oS pos in
1441 match if is_D then Z.downO pos else Z.downOr pos with
1442 | Z.Solution (s,_,_) -> assert(is_D);
1443 move_solution_up ~unfocus:false true s pos cache
1444 | Z.Todo pos when is_D -> attack pos cache (Z.getA pos)
1446 match first_left_mark_L_as_D is_aS pos with
1447 | Some pos -> local_choice_point pos
1448 | None -> assert false
1450 local_choice_point pos
1454 and next_choice (pos : 'a and_pos) cache =
1455 next_choice_point pos cache
1457 and move_solution_up
1459 (status : #tac_status as 'a) (pos : 'a or_pos) cache
1461 let pos = (* mark as solved *)
1462 match Z.getO pos with
1463 | L _ -> assert false (* XXX *)
1467 Z.inject T.Nil (Z.setO (L (g,status)) pos)
1469 Z.setO (S (g,status)) pos
1471 let has_alternative_or = match Z.right pos with None -> false | _ -> true in
1472 let pos = Z.upO pos in
1473 let are_all_lbro_L = forall_left is_aL pos in
1474 let has_no_alternative =
1475 ((not has_alternative_or) && are_sons_L) ||
1478 match Z.getA pos with
1479 | _, L _ -> assert false
1480 | (_, size, depth), S (g,_)
1481 (* S if already solved and then solved again because of a backtrack *)
1482 | (_, size, depth), D g ->
1484 if has_no_alternative then (L (g,status)) else (S (g,status))in
1485 (* TODO: cache success g *)
1486 let pos = if has_no_alternative then Z.inject T.Nil pos else pos in
1487 let status = if unfocus then NTactics.unfocus_tac status else status
1489 let news = status,size,depth in
1490 let pos = Z.setA news newg pos in
1491 match Z.right pos with
1492 | Some pos -> next ~unfocus:true pos cache
1494 match Z.upA pos with
1495 | None -> Proved (status, Some (pos,cache))
1498 ~unfocus:true (has_no_alternative && are_all_lbro_L)
1501 and attack pos cache and_item =
1502 (* show pos; uncomment to show the tree *)
1504 | _, S _ -> assert false (* next would close the proof or give a D *)
1505 | _, L _ -> assert false (* L is a final solution *)
1506 | (_, depth, _),_ when Unix.gettimeofday () > flags.timeout ->
1507 debug_print ~depth (lazy ("fail timeout"));
1509 | (s, depth, width), D (_, T as g) when not flags.do_types ->
1510 debug_print ~depth (lazy "skip goal in Type");
1511 next ~unfocus:false (solved g depth width s pos) cache
1512 | (_,depth,_), D _ when depth > flags.maxdepth ->
1513 debug_print ~depth (lazy "fail depth");
1514 next_choice (failed pos) cache
1515 | (_,depth,size), D _ when size > flags.maxsize ->
1516 debug_print ~depth (lazy "fail size");
1517 next_choice (failed pos) cache
1518 | (s,depth,size), D (gno,_ as g) ->
1519 assert (Z.eject pos = T.Nil); (*subtree must be unexplored *)
1520 match calculate_goal_ty g s with
1522 debug_print ~depth (lazy("success side effect: "^string_of_int gno));
1523 next ~unfocus:false (solved g depth size s pos) cache
1525 let s, gty = apply_subst s (ctx_of gty) gty in
1526 debug_print ~depth (lazy ("EXAMINE: "^ ppterm s gty));
1527 match cache_examine cache gty with
1528 | `Failed_in d when d <= depth ->
1529 debug_print ~depth(lazy("fail depth (c): "^string_of_int gno));
1530 next_choice (failed pos) cache
1531 | `UnderInspection ->
1532 debug_print ~depth (lazy("fail loop: "^string_of_int gno));
1533 next_choice (failed pos) cache
1535 debug_print ~depth (lazy("success (c): "^string_of_int gno));
1536 let s = put_in_subst s g t gty in
1537 next ~unfocus:true (solved g depth size s pos) cache
1540 (* more depth than before or first time we see the goal *)
1541 if prunable s gty () then
1542 (debug_print ~depth (lazy( "fail one father is equal"));
1543 next_choice (failed pos) cache)
1545 let cache = cache_add_underinspection cache gty depth in
1546 debug_print ~depth (lazy ("INSPECTING: " ^
1547 string_of_int gno ^ "("^ string_of_int size ^ ") "));
1548 let subgoals, cache =
1549 do_something signature flags s gno depth gty cache
1551 if subgoals = [] then (* this goal has failed *)
1552 next_choice (failed pos) cache
1554 let size_gl l = List.length (prop_only l) in
1557 (fun (_cand,depth_incr,size_mult,s,gl) ->
1560 (s,depth+depth_incr,size+size_mult*(size_gl gl)),
1561 List.map (fun g -> D g,T.Nil) gl))
1565 (Z.inject (T.Node (`Or,subtrees)) pos) cache
1567 (next ~unfocus:true pos cache : 'a auto_result)
1570 let int name l def =
1571 try int_of_string (List.assoc name l)
1572 with Failure _ | Not_found -> def
1575 let auto_tac ~params:(_univ,flags) status =
1576 let goals = head_goals status#stack in
1577 let status, cache = mk_th_cache status goals in
1578 (* pp_th status cache; *)
1580 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1582 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1583 String.concat "\n " (List.map (
1584 NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[])
1585 (NDiscriminationTree.TermSet.elements t))
1588 let depth = int "depth" flags 3 in
1589 let size = int "size" flags 10 in
1590 let width = int "width" flags (3+List.length goals) in
1592 let goals = List.map (fun i -> D(i,P), T.Nil) goals in
1593 let elems = Z.start (T.Node (`And(status,0,0),goals)) in
1594 let signature = () in
1599 timeout = Unix.gettimeofday() +. 3000.;
1603 if x > y then raise (Error (lazy "auto gave up", None))
1605 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1606 let flags = { flags with maxdepth = x } in
1607 match auto_main flags signature elems cache with
1608 | Gaveup -> up_to (x+1) y
1610 HLog.debug ("proved at depth " ^ string_of_int x);
1613 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1621 let rec rm_assoc n = function
1622 | [] -> assert false
1623 | (x,i)::tl when n=x -> i,tl
1624 | p::tl -> let i,tl = rm_assoc n tl in i,p::tl
1627 let merge canonicals elements n m =
1628 let cn,canonicals = rm_assoc n canonicals in
1629 let cm,canonicals = rm_assoc m canonicals in
1630 let ln,elements = rm_assoc cn elements in
1631 let lm,elements = rm_assoc cm elements in
1633 (n,cm)::(m,cm)::List.map
1635 if xc = cn then (x,cm) else p) canonicals
1637 let elements = (cn,ln@lm)::elements
1643 let canonicals = List.map (fun x -> (x,x)) l in
1644 let elements = List.map (fun x -> (x,[x])) l in
1646 (fun (canonicals,elements) x ->
1649 (fun (canonicals,elements) d ->
1650 merge canonicals elements d x)
1651 (canonicals,elements) dep)
1652 (canonicals,elements) l
1655 let group_by_tac ~eq_predicate ~action:tactic status =
1656 let goals = head_goals status#stack in
1657 if List.length goals < 2 then tactic status
1659 let eq_predicate = eq_predicate status in
1660 let rec aux classes = function
1664 let c = List.find (fun c -> eq_predicate c g) classes in
1665 let classes = List.filter ((<>) c) classes in
1666 aux ((g::c) :: classes) tl
1667 with Not_found -> aux ([g] :: classes) tl
1669 let classes = aux [] goals in
1672 HLog.debug ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1675 let l2 = HExtlib.list_mapi (fun x i -> x,i+1) l2 in
1676 List.map (fun x -> List.assoc x l2) l1
1678 NTactics.block_tac ([ NTactics.branch_tac ]
1680 HExtlib.list_concat ~sep:[NTactics.shift_tac]
1681 (List.map (fun gl-> [NTactics.pos_tac (pos_of gl goals); tactic]) classes)
1683 [ NTactics.merge_tac ]) status
1686 module IntSet = Set.Make(struct type t = int let compare = compare end)
1688 let type_dependency status gl g =
1689 let rec closure acc = function
1691 | x::l when IntSet.mem x acc -> closure acc l
1693 let acc = IntSet.add x acc in
1694 let gty = get_goalty status x in
1695 let deps = metas_of_term status gty in
1696 closure acc (deps @ l)
1698 not (IntSet.is_empty
1700 (closure IntSet.empty gl)
1701 (closure IntSet.empty [g])))
1704 let auto_tac ~params =
1705 group_by_tac ~eq_predicate:type_dependency ~action:(auto_tac ~params)
1708 (* ========================= dispatching of auto/auto_paramod ============ *)
1709 let auto_tac ~params:(_,flags as params) =
1710 if List.mem_assoc "paramodulation" flags then
1711 auto_paramod_tac ~params
1712 else if List.mem_assoc "paramod" flags then
1713 NnAuto.paramod_tac ~params
1714 else if List.mem_assoc "fast_paramod" flags then
1715 NnAuto.fast_eq_check_tac ~params
1716 else if List.mem_assoc "slir" flags then
1717 NnAuto.auto_tac ~params