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_______________________________________________________________ *)
15 let debug_print ?(depth=0) s =
16 if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
17 (* let print= debug_print *)
18 let print ?(depth=0) s =
19 prerr_endline (String.make depth '\t'^Lazy.force s)
21 let debug_do f = if !debug then f () else ()
23 open Continuationals.Stack
25 module Ast = CicNotationPt
26 let app_counter = ref 0
28 (* ======================= utility functions ========================= *)
29 module IntSet = Set.Make(struct type t = int let compare = compare end)
31 let get_sgoalty status g =
32 let _,_,metasenv,subst,_ = status#obj in
34 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
35 let ty = NCicUntrusted.apply_subst subst ctx ty in
36 let ctx = NCicUntrusted.apply_subst_context
37 ~fix_projections:true subst ctx
39 NTacStatus.mk_cic_term ctx ty
40 with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
44 let gty = get_sgoalty status g in
45 metas_of_term status gty
48 let menv_closure status gl =
49 let rec closure acc = function
51 | x::l when IntSet.mem x acc -> closure acc l
52 | x::l -> closure (IntSet.add x acc) (deps status x @ l)
53 in closure IntSet.empty gl
56 (* we call a "fact" an object whose hypothesis occurs in the goal
57 or in types of goal-variables *)
58 let is_a_fact status ty =
59 let status, ty, _ = saturate ~delta:max_int status ty in
60 let g_metas = metas_of_term status ty in
61 let clos = menv_closure status g_metas in
62 let _,_,metasenv,_,_ = status#obj in
65 (fun acc (i,_) -> IntSet.add i acc)
67 in IntSet.equal clos menv;;
69 let is_a_fact_obj s uri =
70 let obj = NCicEnvironment.get_checked_obj uri in
72 | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
73 is_a_fact s (mk_cic_term [] ty)
74 (* aggiungere i costruttori *)
77 let current_goal status =
78 let open_goals = head_goals status#stack in
79 assert (List.length open_goals = 1);
80 let open_goal = List.hd open_goals in
81 let gty = get_goalty status open_goal in
82 let ctx = ctx_of gty in
87 (* =============================== paramod =========================== *)
88 let auto_paramod ~params:(l,_) status goal =
89 let gty = get_goalty status goal in
90 let n,h,metasenv,subst,o = status#obj in
91 let status,t = term_of_cic_term status gty (ctx_of gty) in
95 let status, t = disambiguate status (ctx_of gty) t None in
96 let status, ty = typeof status (ctx_of t) t in
97 let status, t = term_of_cic_term status t (ctx_of gty) in
98 let status, ty = term_of_cic_term status ty (ctx_of ty) in
99 (status, (t,ty) :: l))
103 NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
105 | [] -> raise (Error (lazy "no proof found",None))
106 | (pt, metasenv, subst)::_ ->
107 let status = status#set_obj (n,h,metasenv,subst,o) in
108 instantiate status goal (mk_cic_term (ctx_of gty) pt)
111 let auto_paramod_tac ~params status =
112 NTactics.distribute_tac (auto_paramod ~params) status
115 let fast_eq_check_all status eq_cache goal =
116 let gty = get_goalty status goal in
117 let ctx = ctx_of gty in
118 let n,h,metasenv,subst,o = status#obj in
119 let status,t = term_of_cic_term status gty ctx in
120 let build_status (pt, metasenv, subst) =
121 let status = status#set_obj (n,h,metasenv,subst,o) in
122 let gty = get_goalty status goal in
123 instantiate status goal (mk_cic_term ctx pt)
125 List.map build_status
126 (NCicParamod.fast_eq_check status metasenv subst ctx
127 eq_cache (NCic.Rel ~-1,t))
130 let fast_eq_check eq_cache status goal =
131 match fast_eq_check_all status eq_cache goal with
132 | [] -> raise (Error (lazy "no proof found",None))
136 let fast_eq_check_tac ~params s =
137 NTactics.distribute_tac (fast_eq_check s#eq_cache) s
140 let auto_eq_check eq_cache status =
143 NTactics.distribute_tac (fast_eq_check eq_cache) status in
150 let fast_eq_check_tac_all ~params eq_cache status =
151 let g,_,_ = current_goal status in
152 let allstates = fast_eq_check_all status eq_cache g in
153 let pseudo_low_tac s _ _ = s in
154 let pseudo_low_tactics =
155 List.map pseudo_low_tac allstates
157 List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
161 (*************** subsumption ****************)
163 let close_wrt_context =
167 | name, NCic.Decl t -> NCic.Prod(name,t,ty)
168 | name, NCic.Def(bo, _) -> NCicSubstitution.subst bo ty)
171 let args_for_context ?(k=1) ctx =
174 (fun (n,l) ctx_entry ->
176 | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
177 | name, NCic.Def(bo, _) -> n+1,l)
181 let constant_for_meta ctx ty i =
182 let name = "cic:/foo"^(string_of_int i)^".con" in
183 let uri = NUri.uri_of_string name in
184 let ty = close_wrt_context ty ctx in
185 (* prerr_endline (NCicPp.ppterm [] [] [] ty); *)
186 let attr = (`Generated,`Definition,`Local) in
187 let obj = NCic.Constant([],name,None,ty,attr) in
188 (* Constant of relevance * string * term option * term * c_attr *)
192 let refresh metasenv =
194 (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
195 let ikind = NCicUntrusted.kind_of_meta iattr in
196 let metasenv,j,instance,ty =
197 NCicMetaSubst.mk_meta ~attrs:iattr
198 metasenv ctx ~with_type:ty ikind in
199 let s_entry = i,(iattr, ctx, instance, ty) in
200 let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
201 metasenv,s_entry::subst)
202 (metasenv,[]) metasenv
204 (* close metasenv returns a ground instance of all the metas in the
205 metasenv, insantiatied with axioms, and the list of these axioms *)
206 let close_metasenv metasenv subst =
208 let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
210 let metasenv = NCicUntrusted.sort_metasenv subst metasenv in
212 (fun (subst,objs) (i,(iattr,ctx,ty)) ->
213 let ty = NCicUntrusted.apply_subst subst ctx ty in
215 NCicUntrusted.apply_subst_context ~fix_projections:true
217 let (uri,_,_,_,obj) as okind =
218 constant_for_meta ctx ty i in
220 NCicEnvironment.check_and_add_obj okind;
221 let iref = NReference.reference_of_spec uri NReference.Decl in
223 let args = args_for_context ctx in
224 if args = [] then NCic.Const iref
225 else NCic.Appl(NCic.Const iref::args)
227 (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
228 let s_entry = i, ([], ctx, iterm, ty)
229 in s_entry::subst,okind::objs
230 with _ -> assert false)
234 let ground_instances status gl =
235 let _,_,metasenv,subst,_ = status#obj in
236 let subset = menv_closure status gl in
237 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
239 let submenv = metasenv in
241 let subst, objs = close_metasenv submenv subst in
245 let (_, ctx, t, _) = List.assoc i subst in
246 debug_print (lazy (NCicPp.ppterm ctx [] [] t));
248 (fun (uri,_,_,_,_) as obj ->
249 NCicEnvironment.invalidate_item (`Obj (uri, obj)))
254 Not_found -> assert false
258 let replace_meta i args target =
259 let rec aux k = function
260 (* TODO: local context *)
261 | NCic.Meta (j,lc) when i = j ->
265 List.map (NCicSubstitution.subst_meta lc) args in
266 NCic.Appl(NCic.Rel k::args))
267 | NCic.Meta (j,lc) as m ->
274 aux k (NCicSubstitution.lift n t)) l))))
275 | t -> NCicUtils.map (fun _ k -> k+1) k aux t
280 let close_wrt_metasenv subst =
282 (fun ty (i,(iattr,ctx,mty)) ->
283 let mty = NCicUntrusted.apply_subst subst ctx mty in
285 NCicUntrusted.apply_subst_context ~fix_projections:true
287 let cty = close_wrt_context mty ctx in
288 let name = "foo"^(string_of_int i) in
289 let ty = NCicSubstitution.lift 1 ty in
290 let args = args_for_context ~k:1 ctx in
291 (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
292 let ty = replace_meta i args ty
294 NCic.Prod(name,cty,ty))
298 let _,_,metasenv,subst,_ = status#obj in
299 let subset = menv_closure status [g] in
300 let subset = IntSet.remove g subset in
301 let elems = IntSet.elements subset in
302 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
303 let ty = NCicUntrusted.apply_subst subst ctx ty in
304 debug_print (lazy ("metas in " ^ (NCicPp.ppterm ctx [] metasenv ty)));
305 debug_print (lazy (String.concat ", " (List.map string_of_int elems)));
306 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
307 let submenv = List.rev (NCicUntrusted.sort_metasenv subst submenv) in
309 let submenv = metasenv in
311 let ty = close_wrt_metasenv subst ty submenv in
312 debug_print (lazy (NCicPp.ppterm ctx [] [] ty));
318 (* =================================== auto =========================== *)
319 (****************** AUTO ********************
321 let calculate_timeout flags =
322 if flags.timeout = 0. then
323 (debug_print (lazy "AUTO WITH NO TIMEOUT");
324 {flags with timeout = infinity})
328 let is_equational_case goalty flags =
329 let ensure_equational t =
330 if is_an_equational_goal t then true
333 (flags.use_paramod && is_an_equational_goal goalty) ||
334 (flags.use_only_paramod && ensure_equational goalty)
337 type menv = Cic.metasenv
338 type subst = Cic.substitution
339 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
340 let candidate_no = ref 0;;
341 type candidate = int * Cic.term Lazy.t
342 type cache = AutoCache.cache
345 (* the goal (mainly for depth) and key of the goal *)
346 goal * AutoCache.cache_key
348 (* goal has to be proved *)
350 (* goal has to be cached as a success obtained using candidate as the first
352 | S of goal * AutoCache.cache_key * candidate * int
354 (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
355 menv * subst * int * op list * op list * fail list
357 (* list of computations that may lead to the solution: all op list will
358 * end with the same (S(g,_)) *)
361 (* menv, subst, alternatives, tables, cache *)
362 | Proved of menv * subst * elem list * AutomationCache.tables * cache
363 | Gaveup of AutomationCache.tables * cache
366 (* the status exported to the external observer *)
368 (* context, (goal,candidate) list, and_list, history *)
369 Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
370 (int * Cic.term * int) list * Cic.term Lazy.t list
373 let rec aux acc = function
374 | (D g)::tl -> aux (acc@[g]) tl
380 let calculate_goal_ty (goalno,_,_) s m =
382 let _,cc,goalty = CicUtil.lookup_meta goalno m in
383 (* XXX applicare la subst al contesto? *)
384 Some (cc, CicMetaSubst.apply_subst s goalty)
385 with CicUtil.Meta_not_found i when i = goalno -> None
388 let calculate_closed_goal_ty (goalno,_,_) s =
390 let cc,_,goalty = List.assoc goalno s in
391 (* XXX applicare la subst al contesto? *)
392 Some (cc, CicMetaSubst.apply_subst s goalty)
397 let pp_status ctx status =
399 let names = Utils.names_of_context ctx in
402 ProofEngineReduction.replace
403 ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
404 ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
408 let string_of_do m s (gi,_,_ as g) d =
409 match calculate_goal_ty g s m with
410 | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
411 | None -> Printf.sprintf "D(%d, _, %d)" gi d
413 let string_of_s m su k (ci,ct) gi =
414 Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
416 let string_of_ol m su l =
420 | D (g,d,s) -> string_of_do m su (g,d,s) d
421 | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
424 let string_of_fl m s fl =
426 (List.map (fun ((i,_,_),ty) ->
427 Printf.sprintf "(%d, %s)" i (pp ty)) fl)
429 let rec aux = function
431 | (m,s,_,_,ol,fl)::tl ->
432 Printf.eprintf "< [%s] ;;; [%s]>\n"
433 (string_of_ol m s ol) (string_of_fl m s fl);
436 Printf.eprintf "-------------------------- status -------------------\n";
438 Printf.eprintf "-----------------------------------------------------\n";
441 let auto_status = ref [] ;;
442 let auto_context = ref [];;
443 let in_pause = ref false;;
444 let pause b = in_pause := b;;
445 let cond = Condition.create ();;
446 let mutex = Mutex.create ();;
447 let hint = ref None;;
448 let prune_hint = ref [];;
450 let step _ = Condition.signal cond;;
451 let give_hint n = hint := Some n;;
452 let give_prune_hint hint =
453 prune_hint := hint :: !prune_hint
460 Condition.wait cond mutex;
465 let get_auto_status _ =
466 let status = !auto_status in
467 let and_list,elems,last =
470 | (m,s,_,don,gl,fail)::tl ->
473 (fun (id,d,_ as g) ->
474 match calculate_goal_ty g s m with
475 | Some (_,x) -> Some (id,x,d) | None -> None)
479 (* these are the S goalsin the or list *)
482 (fun (m,s,_,don,gl,fail) ->
484 (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
488 (* this function eats id from a list l::[id,x] returning x, l *)
489 let eat_tail_if_eq id l =
490 let rec aux (s, l) = function
492 | ((id1,_,_),k1,c)::tl when id = id1 ->
494 | None -> aux (Some c,l) tl
495 | Some _ -> assert false)
496 | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
498 let c, l = aux (None, []) l in
501 let eat_in_parallel id l =
502 let rec aux (b,eaten, new_l as acc) l =
506 match eat_tail_if_eq id l with
507 | None, l -> aux (b@[false], eaten, new_l@[l]) tl
508 | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
512 let rec eat_all rows l =
516 match List.rev elem with
517 | ((to_eat,depth,_),k,_)::next_lunch ->
518 let b, eaten, l = eat_in_parallel to_eat l in
519 let eaten = HExtlib.list_uniq eaten in
520 let eaten = List.rev eaten in
521 let b = true (* List.hd (List.rev b) *) in
522 let rows = rows @ [to_eat,k,b,depth,eaten] in
524 | [] -> eat_all rows or_list
526 eat_all [] (List.rev orlist)
530 (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
533 (* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
534 and_list, rows, history
536 !auto_context, elems, and_list, last
539 (* Works if there is no dependency over proofs *)
540 let is_a_green_cut goalty =
541 CicUtil.is_meta_closed goalty
543 let rec first_s = function
544 | (D _)::tl -> first_s tl
545 | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
548 let list_union l1 l2 =
549 (* TODO ottimizzare compare *)
550 HExtlib.list_uniq (List.sort compare (l1 @ l1))
552 let rec eq_todo l1 l2 =
554 | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
555 | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
556 when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
557 if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
561 let eat_head todo id fl orlist =
562 let rec aux acc = function
564 | (m, s, _, _, todo1, fl1)::tl as orlist ->
566 match first_s todo1 with
567 | None -> orlist, acc
568 | Some (((gno,_,_),_,_,_), todo11) ->
569 (* TODO confronto tra todo da ottimizzare *)
570 if gno = id && eq_todo todo11 todo then
571 aux (list_union fl1 acc) tl
579 let close_proof p ty menv context =
581 List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
583 let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
584 naif_closure p menv context
586 (* XXX capire bene quando aggiungere alla cache *)
587 let add_to_cache_and_del_from_orlist_if_green_cut
588 g s m cache key todo orlist fl ctx size minsize
590 let cache = cache_remove_underinspection cache key in
591 (* prima per fare la irl usavamo il contesto vero e proprio e non quello
593 match calculate_closed_goal_ty g s with
594 | None -> assert false
595 | Some (canonical_ctx , gty) ->
596 let goalno,depth,sort = g in
597 let irl = mk_irl canonical_ctx in
598 let goal = Cic.Meta(goalno, irl) in
599 let proof = CicMetaSubst.apply_subst s goal in
600 let green_proof, closed_proof =
601 let b = is_a_green_cut proof in
603 b, (* close_proof proof gty m ctx *) proof
607 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
608 if is_a_green_cut key then
609 (* if the initia goal was closed, we cut alternatives *)
610 let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
611 let orlist, fl = eat_head todo goalno fl orlist in
613 if size < minsize then
614 (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
616 (* if the proof is closed we cache it *)
617 if green_proof then cache_add_success cache key proof
618 else (* cache_add_success cache key closed_proof *)
619 (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
621 cache, orlist, fl, true
624 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
625 if size < minsize then
626 (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
627 (* if the substituted goal and the proof are closed we cache it *)
628 if is_a_green_cut gty then
629 if green_proof then cache_add_success cache gty proof
630 else (* cache_add_success cache gty closed_proof *)
631 (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
635 CicTypeChecker.type_of_aux' ~subst:s
636 m ctx closed_proof CicUniv.oblivion_ugraph
638 if is_a_green_cut ty then
639 cache_add_success cache ty closed_proof
642 | CicTypeChecker.TypeCheckerFailure _ ->*)
643 (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
645 cache, orlist, fl, false
647 let close_failures (fl : fail list) (cache : cache) =
649 (fun cache ((gno,depth,_),gty) ->
650 if CicUtil.is_meta_closed gty then
651 ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
652 cache_add_failure cache gty depth)
657 let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
658 let entry = goalno, (canonical_ctx, t,ty) in
659 assert_subst_are_disjoint subst [entry];
660 let subst = entry :: subst in
662 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
667 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
668 None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
672 tables cache depth fake_proof goalno goalty subst context
675 let active,passive,bag = tables in
676 let ppterm = ppterm context in
677 let status = (fake_proof,goalno) in
678 if flags.use_only_paramod then
680 debug_print (lazy ("PARAMODULATION SU: " ^
681 string_of_int goalno ^ " " ^ ppterm goalty ));
682 let goal_steps, saturation_steps, timeout =
683 max_int,max_int,flags.timeout
686 Saturation.given_clause bag status active passive
687 goal_steps saturation_steps timeout
689 | None, active, passive, bag ->
690 [], (active,passive,bag), cache, flags
691 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
693 assert_subst_are_disjoint subst subst';
694 let subst = subst@subst' in
696 order_new_goals metasenv subst open_goals ppterm
699 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
702 [(!candidate_no,proof),metasenv,subst,open_goals],
703 (active,passive,bag), cache, flags
707 debug_print (lazy ("NARROWING DEL GOAL: " ^
708 string_of_int goalno ^ " " ^ ppterm goalty ));
709 let goal_steps, saturation_steps, timeout =
713 Saturation.solve_narrowing bag status active passive goal_steps
715 | None, active, passive, bag ->
716 [], (active,passive,bag), cache, flags
717 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
719 assert_subst_are_disjoint subst subst';
720 let subst = subst@subst' in
722 order_new_goals metasenv subst open_goals ppterm
725 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
728 [(!candidate_no,proof),metasenv,subst,open_goals],
729 (active,passive,bag), cache, flags
733 let params = ([],["use_context","false"]) in
734 let automation_cache = {
735 AutomationCache.tables = tables ;
736 AutomationCache.univ = Universe.empty; }
739 let ((_,metasenv,subst,_,_,_),open_goals) =
741 solve_rewrite ~params ~automation_cache
744 let proof = lazy (Cic.Meta (-1,[])) in
745 [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
746 with ProofEngineTypes.Fail _ -> [], tables, cache, flags
748 let res = Saturation.all_subsumed bag status active passive in
751 (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
752 assert_subst_are_disjoint subst subst';
753 let subst = subst@subst' in
755 order_new_goals metasenv subst open_goals ppterm
758 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
761 (!candidate_no,proof),metasenv,subst,open_goals)
764 res', (active,passive,bag), cache, flags
771 List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
772 let p1 = List.length (prop_only l1) in
773 let p2 = List.length (prop_only l2) in
774 if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
778 let try_candidate dbd
779 goalty tables subst fake_proof goalno depth context cand
781 let ppterm = ppterm context in
783 let actives, passives, bag = tables in
784 let (_,metasenv,subst,_,_,_), open_goals =
785 ProofEngineTypes.apply_tactic
786 (PrimitiveTactics.apply_tac ~term:cand)
789 let tables = actives, passives,
790 Equality.push_maxmeta bag
791 (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
793 debug_print (lazy (" OK: " ^ ppterm cand));
794 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
795 let open_goals = order_new_goals metasenv subst open_goals ppterm in
796 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
798 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
800 | ProofEngineTypes.Fail s -> None,tables
801 | CicUnification.Uncertain s -> None,tables
804 let applicative_case dbd
805 tables depth subst fake_proof goalno goalty metasenv context
806 signature universe cache flags
810 | Cic.Appl (hd::tl) ->
811 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
814 let goalty_aux = goalty in
816 get_candidates flags.skip_trie_filtering universe cache goalty_aux
818 (* if the goal is an equality we skip the congruence theorems
820 if is_equational_case goalty flags
821 then List.filter not_default_eq_term candidates
824 let candidates = List.filter (only signature context metasenv) candidates
828 (fun (tables,elems) cand ->
830 try_candidate dbd goalty
831 tables subst fake_proof goalno depth context cand
833 | None, tables -> tables, elems
834 | Some x, tables -> tables, x::elems)
835 (tables,[]) candidates
837 let elems = sort_new_elems elems in
841 let try_smart_candidate dbd
842 goalty tables subst fake_proof goalno depth context cand
844 let ppterm = ppterm context in
846 let params = ([],[]) in
847 let automation_cache = {
848 AutomationCache.tables = tables ;
849 AutomationCache.univ = Universe.empty; }
851 debug_print (lazy ("candidato per " ^ string_of_int goalno
852 ^ ": " ^ CicPp.ppterm cand));
854 let (_,metasenv,subst,_,_,_) = fake_proof in
855 prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
856 prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
858 let ((_,metasenv,subst,_,_,_),open_goals) =
859 apply_smart ~dbd ~term:cand ~params ~automation_cache
862 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
863 let open_goals = order_new_goals metasenv subst open_goals ppterm in
864 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
866 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
868 | ProofEngineTypes.Fail s -> None,tables
869 | CicUnification.Uncertain s -> None,tables
872 let smart_applicative_case dbd
873 tables depth subst fake_proof goalno goalty metasenv context signature
878 | Cic.Appl (hd::tl) ->
879 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
882 let smart_candidates =
883 get_candidates flags.skip_trie_filtering universe cache goalty_aux
886 get_candidates flags.skip_trie_filtering universe cache goalty
888 let smart_candidates =
890 (fun x -> not(List.mem x candidates)) smart_candidates
893 (lazy ("smart_candidates" ^ " = " ^
894 (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
895 debug_print debug_msg;
896 let candidates = List.filter (only signature context metasenv) candidates in
897 let smart_candidates =
898 List.filter (only signature context metasenv) smart_candidates
901 let penalty cand depth =
902 if only signature context metasenv cand then depth else ((prerr_endline (
903 "penalizzo " ^ CicPp.ppterm cand));depth -1)
908 (fun (tables,elems) cand ->
910 try_candidate dbd goalty
911 tables subst fake_proof goalno depth context cand
914 (* if normal application fails we try to be smart *)
915 (match try_smart_candidate dbd goalty
916 tables subst fake_proof goalno depth context cand
918 | None, tables -> tables, elems
919 | Some x, tables -> tables, x::elems)
920 | Some x, tables -> tables, x::elems)
921 (tables,[]) candidates
923 let tables, smart_elems =
925 (fun (tables,elems) cand ->
927 try_smart_candidate dbd goalty
928 tables subst fake_proof goalno depth context cand
930 | None, tables -> tables, elems
931 | Some x, tables -> tables, x::elems)
932 (tables,[]) smart_candidates
934 let elems = sort_new_elems (elems @ smart_elems) in
938 let equational_and_applicative_case dbd
939 signature universe flags m s g gty tables cache context
941 let goalno, depth, sort = g in
942 let fake_proof = mk_fake_proof m s g gty context in
943 if is_equational_case gty flags then
944 let elems,tables,cache, flags =
945 equational_case tables cache
946 depth fake_proof goalno gty s context flags
948 let more_elems, tables, cache =
949 if flags.use_only_paramod then
953 tables depth s fake_proof goalno
954 gty m context signature universe cache flags
956 elems@more_elems, tables, cache, flags
958 let elems, tables, cache =
959 match LibraryObjects.eq_URI () with
961 smart_applicative_case dbd tables depth s fake_proof goalno
962 gty m context signature universe cache flags
964 applicative_case dbd tables depth s fake_proof goalno
965 gty m context signature universe cache flags
967 elems, tables, cache, flags
969 let rec condition_for_hint i = function
971 | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
972 | _::tl -> condition_for_hint i tl
974 let prunable_for_size flags s m todo =
975 let rec aux b = function
976 | (S _)::tl -> aux b tl
977 | (D (_,_,T))::tl -> aux b tl
979 (match calculate_goal_ty g s m with
981 | Some (canonical_ctx, gty) ->
984 ~consider_metas:false ~count_metas_occurrences:true gty in
985 let newb = b || gsize > flags.maxgoalsizefactor in
992 let prunable ty todo =
993 let rec aux b = function
994 | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
995 | (D (_,_,T))::tl -> aux b tl
1003 let prunable menv subst ty todo =
1004 let rec aux = function
1005 | (S(_,k,_,_))::tl ->
1006 (match Equality.meta_convertibility_subst k ty menv with
1009 no_progress variant tl (* || aux tl*))
1010 | (D (_,_,T))::tl -> aux tl
1012 and no_progress variant = function
1013 | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
1014 | D ((n,_,P) as g)::tl ->
1015 (match calculate_goal_ty g subst menv with
1016 | None -> no_progress variant tl
1018 (match calculate_goal_ty g variant menv with
1019 | None -> assert false
1021 if gty = gty' then no_progress variant tl
1023 (prerr_endline (string_of_int n);
1024 prerr_endline (CicPp.ppterm gty);
1025 prerr_endline (CicPp.ppterm gty');
1026 prerr_endline "---------- subst";
1027 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
1028 prerr_endline "---------- variant";
1029 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
1030 prerr_endline "---------- menv";
1031 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
1032 no_progress variant tl) *)
1034 | _::tl -> no_progress variant tl
1039 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
1041 HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
1043 List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
1045 let filter_prune_hint c l =
1046 let prune = !prune_hint in
1047 prune_hint := []; (* possible race... *)
1048 if prune = [] then c,l
1050 cache_reset_underinspection c,
1051 List.filter (condition_for_prune_hint prune) l
1057 auto_all_solutions dbd tables universe cache context metasenv gl flags
1062 MetadataConstraints.UriManagerSet.union set
1063 (MetadataQuery.signature_of metasenv g)
1065 MetadataConstraints.UriManagerSet.empty gl
1067 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1070 (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1072 let elems = [metasenv,[],1,[],goals,[]] in
1073 let rec aux tables solutions cache elems flags =
1074 match auto_main dbd tables context flags signature universe cache elems with
1075 | Gaveup (tables,cache) ->
1076 solutions,cache, tables
1077 | Proved (metasenv,subst,others,tables,cache) ->
1078 if Unix.gettimeofday () > flags.timeout then
1079 ((subst,metasenv)::solutions), cache, tables
1081 aux tables ((subst,metasenv)::solutions) cache others flags
1083 let rc = aux tables [] cache elems flags in
1085 | [],cache,tables -> [],cache,tables
1086 | solutions, cache,tables ->
1089 (fun (subst,newmetasenv) ->
1091 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1093 if opened = [] then Some subst else None)
1096 solutions,cache,tables
1099 (******************* AUTO ***************)
1102 let auto dbd flags metasenv tables universe cache context metasenv gl =
1103 let initial_time = Unix.gettimeofday() in
1107 MetadataConstraints.UriManagerSet.union set
1108 (MetadataQuery.signature_of metasenv g)
1110 MetadataConstraints.UriManagerSet.empty gl
1112 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1113 let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1114 let elems = [metasenv,[],1,[],goals,[]] in
1115 match auto_main dbd tables context flags signature universe cache elems with
1116 | Proved (metasenv,subst,_, tables,cache) ->
1118 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1119 Some (subst,metasenv), cache
1120 | Gaveup (tables,cache) ->
1122 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1126 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
1127 let flags = flags_of_params params () in
1128 let use_library = flags.use_library in
1129 let universe, tables, cache =
1130 init_cache_and_tables
1131 ~dbd ~use_library ~use_context:(not flags.skip_context)
1132 automation_cache univ (proof, goal)
1134 let _,metasenv,subst,_,_, _ = proof in
1135 let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1136 let signature = MetadataQuery.signature_of metasenv goal in
1141 CicTypeChecker.type_of_aux' metasenv context t
1142 CicUniv.oblivion_ugraph
1144 MetadataConstraints.UriManagerSet.union set
1145 (MetadataConstraints.constants_of ty)
1150 if flags.close_more then
1152 tables context (proof, goal)
1153 (auto_all_solutions dbd) signature universe cache
1154 else tables,cache in
1155 let initial_time = Unix.gettimeofday() in
1156 let (_,oldmetasenv,_,_,_, _) = proof in
1159 metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
1161 match auto_main dbd tables context flags signature universe cache [elem] with
1162 | Proved (metasenv,subst,_, tables,cache) ->
1164 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1165 let proof,metasenv =
1166 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1167 proof goal subst metasenv
1170 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1171 ~newmetasenv:metasenv
1174 | Gaveup (tables,cache) ->
1177 string_of_float(Unix.gettimeofday()-.initial_time)));
1178 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1182 (****************** types **************)
1185 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
1187 let keys_of_term status t =
1188 let status, orig_ty = typeof status (ctx_of t) t in
1189 let _, ty, _ = saturate ~delta:max_int status orig_ty in
1192 let _, ty = term_of_cic_term status ty (ctx_of ty) in
1194 | NCic.Const (NReference.Ref (_,NReference.Def h))
1195 | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_)
1197 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
1204 let mk_th_cache status gl =
1206 (fun (status, acc) g ->
1207 let gty = get_goalty status g in
1208 let ctx = ctx_of gty in
1209 debug_print(lazy("th cache for: "^ppterm status gty));
1210 debug_print(lazy("th cache in: "^ppcontext status ctx));
1211 if List.mem_assq ctx acc then status, acc else
1212 let idx = InvRelDiscriminationTree.empty in
1215 (fun (status, i, idx) _ ->
1216 let t = mk_cic_term ctx (NCic.Rel i) in
1217 debug_print(lazy("indexing: "^ppterm status t));
1218 let status, keys = keys_of_term status t in
1220 List.fold_left (fun idx k ->
1221 InvRelDiscriminationTree.index idx k t) idx keys
1224 (status, 1, idx) ctx
1226 status, (ctx, idx) :: acc)
1230 let add_to_th t c ty =
1231 let key_c = ctx_of t in
1232 if not (List.mem_assq key_c c) then
1233 (key_c ,InvRelDiscriminationTree.index
1234 InvRelDiscriminationTree.empty ty t ) :: c
1236 let rec replace = function
1238 | (x, idx) :: tl when x == key_c ->
1239 (x, InvRelDiscriminationTree.index idx ty t) :: tl
1240 | x :: tl -> x :: replace tl
1245 let pp_idx status idx =
1246 InvRelDiscriminationTree.iter idx
1248 debug_print(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
1250 (fun t -> debug_print(lazy("\t"^ppterm status t)))
1257 debug_print(lazy( "-----------------------------------------------"));
1258 debug_print(lazy( (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx)));
1259 debug_print(lazy( "||====> "));
1263 let search_in_th gty th =
1264 let c = ctx_of gty in
1265 let rec aux acc = function
1266 | [] -> Ncic_termSet.elements acc
1269 let idx = List.assq k th in
1270 let acc = Ncic_termSet.union acc
1271 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
1274 with Not_found -> aux acc tl
1276 aux Ncic_termSet.empty c
1280 do_types : bool; (* solve goals in Type *)
1288 {facts : th_cache; (* positive results *)
1289 under_inspection : th_cache; (* to prune looping *)
1290 unit_eq : NCicParamod.state
1294 type goal = int * sort (* goal, depth, sort *)
1295 type fail = goal * cic_term
1296 type candidate = int * Ast.term (* unique candidate number, candidate *)
1298 exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
1299 atoms of the input goals *)
1300 exception Proved of #NTacStatus.tac_status
1302 (* let close_failures _ c = c;; *)
1303 (* let prunable _ _ _ = false;; *)
1304 (* let cache_examine cache gty = `Notfound;; *)
1305 (* let put_in_subst s _ _ _ = s;; *)
1306 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
1307 (* let cache_add_underinspection c _ _ = c;; *)
1309 let init_cache ?(facts=[]) ?(under_inspection=[])
1310 ?(unit_eq=NCicParamod.empty_state) _ =
1312 under_inspection = under_inspection;
1316 let only _ _ _ = true;;
1318 let candidate_no = ref 0;;
1320 let openg_no status = List.length (head_goals status#stack)
1322 let sort_new_elems l =
1323 List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
1325 let try_candidate flags depth status t =
1327 debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
1328 let status = NTactics.apply_tac ("",0,t) status in
1329 let og_no = openg_no status in
1330 if og_no > flags.maxwidth ||
1331 (depth = flags.maxdepth && og_no <> 0) then
1332 (debug_print ~depth (lazy "pruned immediately"); None)
1335 Some ((!candidate_no,t),status))
1336 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1339 let get_candidates status cache signature gty =
1340 let universe = status#auto_cache in
1341 let context = ctx_of gty in
1342 let _, raw_gty = term_of_cic_term status gty context in
1343 let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1347 List.filter (only signature context)
1348 (NDiscriminationTree.TermSet.elements cands)
1351 let _status, t = term_of_cic_term status t context in Ast.NCic t)
1352 (search_in_th gty cache)
1354 List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
1357 let applicative_case depth signature status flags gty (cache:cache) =
1358 let tcache = cache.facts in
1359 app_counter:= !app_counter+1;
1360 let candidates = get_candidates status tcache signature gty in
1362 (lazy ("candidates: " ^ string_of_int (List.length candidates)));
1366 match try_candidate flags depth status cand with
1368 | Some x -> x::elems)
1377 (* gty is supposed to be meta-closed *)
1378 let is_subsumed depth status gty cache =
1379 if cache=[] then false else (
1380 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1381 let n,h,metasenv,subst,obj = status#obj in
1382 let ctx = ctx_of gty in
1383 let _ , target = term_of_cic_term status gty ctx in
1384 let target = NCicSubstitution.lift 1 target in
1385 (* candidates must only be searched w.r.t the given context *)
1388 let idx = List.assq ctx cache in
1389 Ncic_termSet.elements
1390 (InvRelDiscriminationTree.retrieve_generalizations idx gty)
1391 with Not_found -> []
1394 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1398 let _ , source = term_of_cic_term status t ctx in
1400 NCic.Prod("foo",source,target) in
1401 let metasenv,j,_,_ =
1402 NCicMetaSubst.mk_meta
1403 metasenv ctx ~with_type:implication `IsType in
1404 let status = status#set_obj (n,h,metasenv,subst,obj) in
1405 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1407 let status = NTactics.intro_tac "foo" status in
1409 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1411 if (head_goals status#stack = []) then raise Found
1416 with Found -> debug_print ~depth (lazy "success");true)
1419 (* warning: ctx is supposed to be already instantiated w.r.t subst *)
1420 let index_local_equations eq_cache status =
1421 let open_goals = head_goals status#stack in
1422 assert (List.length open_goals = 1);
1423 let open_goal = List.hd open_goals in
1424 let ngty = get_goalty status open_goal in
1425 let ctx = ctx_of ngty in
1430 let t = NCic.Rel !c in
1432 let ty = NCicTypeChecker.typeof [] [] ctx t in
1433 prerr_endline ("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty));
1434 NCicParamod.forward_infer_step eq_cache t ty
1436 | NCicTypeChecker.TypeCheckerFailure _
1437 | NCicTypeChecker.AssertFailure _ -> eq_cache)
1441 let rec guess_name name ctx =
1442 if name = "_" then guess_name "auto" ctx else
1443 if not (List.mem_assoc name ctx) then name else
1444 guess_name (name^"'") ctx
1447 let is_prod status =
1448 let _, ctx, gty = current_goal status in
1449 let _, raw_gty = term_of_cic_term status gty ctx in
1451 | NCic.Prod (name,_,_) -> Some (guess_name name ctx)
1454 let intro ~depth status facts name =
1455 let status = NTactics.intro_tac name status in
1456 let _, ctx, ngty = current_goal status in
1457 let t = mk_cic_term ctx (NCic.Rel 1) in
1458 let status, keys = keys_of_term status t in
1459 let facts = List.fold_left (add_to_th t) facts keys in
1460 debug_print ~depth (lazy ("intro: "^ name));
1461 (* unprovability is not stable w.r.t introduction *)
1465 let rec intros_facts ~depth status facts =
1466 match is_prod status with
1469 intro ~depth status facts name
1470 in intros_facts ~depth status facts
1471 | _ -> status, facts
1474 let rec intros ~depth status (cache:cache) =
1475 match is_prod status with
1477 prerr_endline "is prod";
1479 intros_facts ~depth status cache.facts
1481 (* we reindex the equation from scratch *)
1483 index_local_equations status#eq_cache status in
1484 (* under_inspection must be set to empty *)
1485 status, init_cache ~facts ~unit_eq ()
1486 | _ -> status, cache
1489 let reduce ~depth status g =
1490 let n,h,metasenv,subst,o = status#obj in
1491 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1492 let ty = NCicUntrusted.apply_subst subst ctx ty in
1493 let ty' = NCicReduction.whd ~subst ctx ty in
1497 (lazy ("reduced to: "^ NCicPp.ppterm ctx subst metasenv ty'));
1499 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1501 let status = status#set_obj (n,h,metasenv,subst,o) in
1503 [(!candidate_no,Ast.Ident("__whd",None)),status])
1506 let do_something signature flags status g depth gty cache =
1508 let l = reduce ~depth status g in
1509 (* backward aplications *)
1510 let l1 = applicative_case depth signature status flags gty cache in
1511 (* fast paramodulation *)
1516 ((!candidate_no,Ast.Ident("__paramod",None)),s))
1517 (auto_eq_check cache.unit_eq status)
1518 (* states in l2 have have an set of subgoals: no point to sort them *)
1520 l2 @ (sort_new_elems (l@l1)), cache
1523 let pp_goal = function
1524 | (_,Continuationals.Stack.Open i)
1525 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1528 let pp_goals status l =
1532 let gty = get_goalty status i in
1533 NTacStatus.ppterm status gty)
1540 let compare = Pervasives.compare
1544 module MS = HTopoSort.Make(M)
1547 let sort_tac status =
1549 match status#stack with
1550 | [] -> assert false
1551 | (goals, t, k, tag) :: s ->
1552 let g = head_goals status#stack in
1554 (List.rev (MS.topological_sort g (deps status))) in
1555 debug_print (lazy ("old g = " ^
1556 String.concat "," (List.map string_of_int g)));
1557 debug_print (lazy ("sorted goals = " ^
1558 String.concat "," (List.map string_of_int sortedg)));
1559 let is_it i = function
1560 | (_,Continuationals.Stack.Open j )
1561 | (_,Continuationals.Stack.Closed j ) -> i = j
1564 List.map (fun i -> List.find (is_it i) goals) sortedg
1566 (sorted_goals, t, k, tag) :: s
1568 status#set_stack gstatus
1571 let clean_up_tac status =
1573 match status#stack with
1574 | [] -> assert false
1575 | (g, t, k, tag) :: s ->
1576 let is_open = function
1577 | (_,Continuationals.Stack.Open _) -> true
1578 | (_,Continuationals.Stack.Closed _) -> false
1580 let g' = List.filter is_open g in
1581 (g', t, k, tag) :: s
1583 status#set_stack gstatus
1586 let focus_tac focus status =
1588 match status#stack with
1589 | [] -> assert false
1590 | (g, t, k, tag) :: s ->
1591 let in_focus = function
1592 | (_,Continuationals.Stack.Open i)
1593 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1595 let focus,others = List.partition in_focus g
1597 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1598 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1600 status#set_stack gstatus
1603 let rec auto_clusters
1604 flags signature cache depth status : unit =
1605 debug_print ~depth (lazy "entering auto clusters");
1606 (* ignore(Unix.select [] [] [] 0.01); *)
1607 let status = clean_up_tac status in
1608 let goals = head_goals status#stack in
1609 if goals = [] then raise (Proved status)
1610 else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
1611 else if List.length goals < 2 then
1612 auto_main flags signature cache depth status
1614 debug_print ~depth (lazy ("goals = " ^
1615 String.concat "," (List.map string_of_int goals)));
1616 let classes = HExtlib.clusters (deps status) goals in
1622 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1627 let status = focus_tac gl status in
1629 debug_print ~depth (lazy ("focusing on" ^
1630 String.concat "," (List.map string_of_int gl)));
1631 auto_main flags signature cache depth status; status
1632 with Proved(status) -> NTactics.merge_tac status)
1634 in raise (Proved status)
1638 (* let rec auto_main flags signature cache status k depth = *)
1640 auto_main flags signature (cache:cache) depth status: unit =
1641 debug_print ~depth (lazy "entering auto main");
1642 (* ignore(Unix.select [] [] [] 0.01); *)
1643 let status = sort_tac (clean_up_tac status) in
1644 let goals = head_goals status#stack in
1646 | [] -> raise (Proved status)
1648 let branch = List.length(goals)>1 in
1649 if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
1652 if branch then NTactics.branch_tac status
1654 let status, cache = intros ~depth status cache in
1655 let g,gctx, gty = current_goal status in
1656 let ctx,ty = close status g in
1657 let closegty = mk_cic_term ctx ty in
1658 let status, gty = apply_subst status gctx gty in
1659 debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
1660 if is_subsumed depth status closegty cache.under_inspection then
1661 (debug_print (lazy "SUBSUMED");
1662 raise (Gaveup IntSet.add g IntSet.empty))
1664 let alternatives, cache =
1665 do_something signature flags status g depth gty cache in
1667 let under_inspection =
1668 add_to_th closegty cache.under_inspection closegty in
1669 {cache with under_inspection = under_inspection} in
1672 (* the underscore information does not need to be returned
1674 (fun unsat ((_,t),status) ->
1675 let depth',looping_cache =
1676 if t=Ast.Ident("__whd",None) then depth,cache
1677 else depth+1, loop_cache in
1678 debug_print (~depth:depth')
1679 (lazy ("Case: " ^ CicNotationPp.pp_term t));
1680 try auto_clusters flags signature loop_cache
1681 depth' status; unsat
1684 debug_print (~depth:depth') (lazy "proved");
1686 let status = NTactics.merge_tac status
1688 (* old cache, here *)
1689 try auto_clusters flags signature cache
1690 depth status; assert false
1693 (lazy ("Unsat1 at depth " ^ (string_of_int depth)
1695 (pp_goals status (IntSet.elements f))));
1696 (* TODO: cache failures *)
1697 IntSet.union f unsat
1698 else raise (Proved status)
1700 debug_print (~depth:depth')
1701 (lazy ("Unsat2 at depth " ^ (string_of_int depth')
1703 (pp_goals status (IntSet.elements f))));
1704 (* TODO: cache local failures *)
1706 IntSet.empty alternatives
1708 raise (Gaveup IntSet.add g unsat)
1711 let int name l def =
1712 try int_of_string (List.assoc name l)
1713 with Failure _ | Not_found -> def
1716 let auto_tac ~params:(_univ,flags) status =
1717 let goals = head_goals status#stack in
1718 let status, facts = mk_th_cache status goals in
1719 let unit_eq = index_local_equations status#eq_cache status in
1720 let cache = init_cache ~facts ~unit_eq () in
1721 (* pp_th status facts; *)
1723 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1725 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1726 String.concat "\n " (List.map (
1727 NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[])
1728 (NDiscriminationTree.TermSet.elements t))
1731 let depth = int "depth" flags 3 in
1732 let size = int "size" flags 10 in
1733 let width = int "width" flags (3+List.length goals) in
1735 let goals = List.map (fun i -> (i,P)) goals in
1736 let signature = () in
1741 timeout = Unix.gettimeofday() +. 3000.;
1744 let initial_time = Unix.gettimeofday() in
1749 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1751 ("Applicative nodes:"^string_of_int !app_counter));
1752 raise (Error (lazy "auto gave up", None)))
1754 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1755 let flags = { flags with maxdepth = x }
1757 try auto_clusters flags signature cache 0 status;assert false
1759 | Gaveup _ -> up_to (x+1) y
1761 print (lazy ("proved at depth " ^ string_of_int x));
1764 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1769 let s = up_to depth depth in
1771 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1773 ("Applicative nodes:"^string_of_int !app_counter));