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 (* =================================== paramod =========================== *)
29 let auto_paramod ~params:(l,_) status goal =
30 let gty = get_goalty status goal in
31 let n,h,metasenv,subst,o = status#obj in
32 let status,t = term_of_cic_term status gty (ctx_of gty) in
36 let status, t = disambiguate status (ctx_of gty) t None in
37 let status, ty = typeof status (ctx_of t) t in
38 let status, t = term_of_cic_term status t (ctx_of gty) in
39 let status, ty = term_of_cic_term status ty (ctx_of ty) in
40 (status, (t,ty) :: l))
44 NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
46 | [] -> raise (Error (lazy "no proof found",None))
47 | (pt, metasenv, subst)::_ ->
48 let status = status#set_obj (n,h,metasenv,subst,o) in
49 instantiate status goal (mk_cic_term (ctx_of gty) pt)
52 let auto_paramod_tac ~params status =
53 NTactics.distribute_tac (auto_paramod ~params) status
56 (*************** subsumption ****************)
57 module IntSet = Set.Make(struct type t = int let compare = compare end)
60 let get_sgoalty status g =
61 let _,_,metasenv,subst,_ = status#obj in
63 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
64 let ty = NCicUntrusted.apply_subst subst ctx ty in
65 let ctx = NCicUntrusted.apply_subst_context
66 ~fix_projections:true subst ctx
68 NTacStatus.mk_cic_term ctx ty
69 with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
73 let gty = get_sgoalty status g in
74 metas_of_term status gty
77 let menv_closure status gl =
78 let rec closure acc = function
80 | x::l when IntSet.mem x acc -> closure acc l
81 | x::l -> closure (IntSet.add x acc) (deps status x @ l)
82 in closure IntSet.empty gl
85 let close_wrt_context =
89 | name, NCic.Decl t -> NCic.Prod(name,t,ty)
90 | name, NCic.Def(bo, _) -> NCicSubstitution.subst bo ty)
93 let args_for_context ?(k=1) ctx =
96 (fun (n,l) ctx_entry ->
98 | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
99 | name, NCic.Def(bo, _) -> n+1,l)
103 let constant_for_meta ctx ty i =
104 let name = "cic:/foo"^(string_of_int i)^".con" in
105 let uri = NUri.uri_of_string name in
106 let ty = close_wrt_context ty ctx in
107 (* prerr_endline (NCicPp.ppterm [] [] [] ty); *)
108 let attr = (`Generated,`Definition,`Local) in
109 let obj = NCic.Constant([],name,None,ty,attr) in
110 (* Constant of relevance * string * term option * term * c_attr *)
114 let refresh metasenv =
116 (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
117 let ikind = NCicUntrusted.kind_of_meta iattr in
118 let metasenv,j,instance,ty =
119 NCicMetaSubst.mk_meta ~attrs:iattr
120 metasenv ctx ~with_type:ty ikind in
121 let s_entry = i,(iattr, ctx, instance, ty) in
122 let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
123 metasenv,s_entry::subst)
124 (metasenv,[]) metasenv
126 (* close metasenv returns a ground instance of all the metas in the
127 metasenv, insantiatied with axioms, and the list of these axioms *)
128 let close_metasenv metasenv subst =
130 let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
132 let metasenv = NCicUntrusted.sort_metasenv subst metasenv in
134 (fun (subst,objs) (i,(iattr,ctx,ty)) ->
135 let ty = NCicUntrusted.apply_subst subst ctx ty in
137 NCicUntrusted.apply_subst_context ~fix_projections:true
139 let (uri,_,_,_,obj) as okind =
140 constant_for_meta ctx ty i in
142 NCicEnvironment.check_and_add_obj okind;
143 let iref = NReference.reference_of_spec uri NReference.Decl in
145 let args = args_for_context ctx in
146 if args = [] then NCic.Const iref
147 else NCic.Appl(NCic.Const iref::args)
149 (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
150 let s_entry = i, ([], ctx, iterm, ty)
151 in s_entry::subst,okind::objs
152 with _ -> assert false)
156 let ground_instances status gl =
157 let _,_,metasenv,subst,_ = status#obj in
158 let subset = menv_closure status gl in
159 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
161 let submenv = metasenv in
163 let subst, objs = close_metasenv submenv subst in
167 let (_, ctx, t, _) = List.assoc i subst in
168 debug_print (lazy (NCicPp.ppterm ctx [] [] t));
170 (fun (uri,_,_,_,_) as obj ->
171 NCicEnvironment.invalidate_item (`Obj (uri, obj)))
176 Not_found -> assert false
180 let replace_meta i args target =
181 let rec aux k = function
182 (* TODO: local context *)
183 | NCic.Meta (j,lc) when i = j ->
187 List.map (NCicSubstitution.subst_meta lc) args in
188 NCic.Appl(NCic.Rel k::args))
189 | NCic.Meta (j,lc) as m ->
196 aux k (NCicSubstitution.lift n t)) l))))
197 | t -> NCicUtils.map (fun _ k -> k+1) k aux t
202 let close_wrt_metasenv subst =
204 (fun ty (i,(iattr,ctx,mty)) ->
205 let mty = NCicUntrusted.apply_subst subst ctx mty in
207 NCicUntrusted.apply_subst_context ~fix_projections:true
209 let cty = close_wrt_context mty ctx in
210 let name = "foo"^(string_of_int i) in
211 let ty = NCicSubstitution.lift 1 ty in
212 let args = args_for_context ~k:1 ctx in
213 (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
214 let ty = replace_meta i args ty
216 NCic.Prod(name,cty,ty))
220 let _,_,metasenv,subst,_ = status#obj in
221 let subset = menv_closure status [g] in
222 let subset = IntSet.remove g subset in
223 let elems = IntSet.elements subset in
224 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
225 let ty = NCicUntrusted.apply_subst subst ctx ty in
226 debug_print (lazy ("metas in " ^ (NCicPp.ppterm ctx [] metasenv ty)));
227 debug_print (lazy (String.concat ", " (List.map string_of_int elems)));
228 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
229 let submenv = List.rev (NCicUntrusted.sort_metasenv subst submenv) in
231 let submenv = metasenv in
233 let ty = close_wrt_metasenv subst ty submenv in
234 debug_print (lazy (NCicPp.ppterm ctx [] [] ty));
240 (* =================================== auto =========================== *)
241 (****************** AUTO ********************
243 let calculate_timeout flags =
244 if flags.timeout = 0. then
245 (debug_print (lazy "AUTO WITH NO TIMEOUT");
246 {flags with timeout = infinity})
250 let is_equational_case goalty flags =
251 let ensure_equational t =
252 if is_an_equational_goal t then true
255 (flags.use_paramod && is_an_equational_goal goalty) ||
256 (flags.use_only_paramod && ensure_equational goalty)
259 type menv = Cic.metasenv
260 type subst = Cic.substitution
261 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
262 let candidate_no = ref 0;;
263 type candidate = int * Cic.term Lazy.t
264 type cache = AutoCache.cache
267 (* the goal (mainly for depth) and key of the goal *)
268 goal * AutoCache.cache_key
270 (* goal has to be proved *)
272 (* goal has to be cached as a success obtained using candidate as the first
274 | S of goal * AutoCache.cache_key * candidate * int
276 (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
277 menv * subst * int * op list * op list * fail list
279 (* list of computations that may lead to the solution: all op list will
280 * end with the same (S(g,_)) *)
283 (* menv, subst, alternatives, tables, cache *)
284 | Proved of menv * subst * elem list * AutomationCache.tables * cache
285 | Gaveup of AutomationCache.tables * cache
288 (* the status exported to the external observer *)
290 (* context, (goal,candidate) list, and_list, history *)
291 Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
292 (int * Cic.term * int) list * Cic.term Lazy.t list
295 let rec aux acc = function
296 | (D g)::tl -> aux (acc@[g]) tl
302 let calculate_goal_ty (goalno,_,_) s m =
304 let _,cc,goalty = CicUtil.lookup_meta goalno m in
305 (* XXX applicare la subst al contesto? *)
306 Some (cc, CicMetaSubst.apply_subst s goalty)
307 with CicUtil.Meta_not_found i when i = goalno -> None
310 let calculate_closed_goal_ty (goalno,_,_) s =
312 let cc,_,goalty = List.assoc goalno s in
313 (* XXX applicare la subst al contesto? *)
314 Some (cc, CicMetaSubst.apply_subst s goalty)
319 let pp_status ctx status =
321 let names = Utils.names_of_context ctx in
324 ProofEngineReduction.replace
325 ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
326 ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
330 let string_of_do m s (gi,_,_ as g) d =
331 match calculate_goal_ty g s m with
332 | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
333 | None -> Printf.sprintf "D(%d, _, %d)" gi d
335 let string_of_s m su k (ci,ct) gi =
336 Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
338 let string_of_ol m su l =
342 | D (g,d,s) -> string_of_do m su (g,d,s) d
343 | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
346 let string_of_fl m s fl =
348 (List.map (fun ((i,_,_),ty) ->
349 Printf.sprintf "(%d, %s)" i (pp ty)) fl)
351 let rec aux = function
353 | (m,s,_,_,ol,fl)::tl ->
354 Printf.eprintf "< [%s] ;;; [%s]>\n"
355 (string_of_ol m s ol) (string_of_fl m s fl);
358 Printf.eprintf "-------------------------- status -------------------\n";
360 Printf.eprintf "-----------------------------------------------------\n";
363 let auto_status = ref [] ;;
364 let auto_context = ref [];;
365 let in_pause = ref false;;
366 let pause b = in_pause := b;;
367 let cond = Condition.create ();;
368 let mutex = Mutex.create ();;
369 let hint = ref None;;
370 let prune_hint = ref [];;
372 let step _ = Condition.signal cond;;
373 let give_hint n = hint := Some n;;
374 let give_prune_hint hint =
375 prune_hint := hint :: !prune_hint
382 Condition.wait cond mutex;
387 let get_auto_status _ =
388 let status = !auto_status in
389 let and_list,elems,last =
392 | (m,s,_,don,gl,fail)::tl ->
395 (fun (id,d,_ as g) ->
396 match calculate_goal_ty g s m with
397 | Some (_,x) -> Some (id,x,d) | None -> None)
401 (* these are the S goalsin the or list *)
404 (fun (m,s,_,don,gl,fail) ->
406 (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
410 (* this function eats id from a list l::[id,x] returning x, l *)
411 let eat_tail_if_eq id l =
412 let rec aux (s, l) = function
414 | ((id1,_,_),k1,c)::tl when id = id1 ->
416 | None -> aux (Some c,l) tl
417 | Some _ -> assert false)
418 | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
420 let c, l = aux (None, []) l in
423 let eat_in_parallel id l =
424 let rec aux (b,eaten, new_l as acc) l =
428 match eat_tail_if_eq id l with
429 | None, l -> aux (b@[false], eaten, new_l@[l]) tl
430 | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
434 let rec eat_all rows l =
438 match List.rev elem with
439 | ((to_eat,depth,_),k,_)::next_lunch ->
440 let b, eaten, l = eat_in_parallel to_eat l in
441 let eaten = HExtlib.list_uniq eaten in
442 let eaten = List.rev eaten in
443 let b = true (* List.hd (List.rev b) *) in
444 let rows = rows @ [to_eat,k,b,depth,eaten] in
446 | [] -> eat_all rows or_list
448 eat_all [] (List.rev orlist)
452 (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
455 (* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
456 and_list, rows, history
458 !auto_context, elems, and_list, last
461 (* Works if there is no dependency over proofs *)
462 let is_a_green_cut goalty =
463 CicUtil.is_meta_closed goalty
465 let rec first_s = function
466 | (D _)::tl -> first_s tl
467 | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
470 let list_union l1 l2 =
471 (* TODO ottimizzare compare *)
472 HExtlib.list_uniq (List.sort compare (l1 @ l1))
474 let rec eq_todo l1 l2 =
476 | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
477 | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
478 when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
479 if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
483 let eat_head todo id fl orlist =
484 let rec aux acc = function
486 | (m, s, _, _, todo1, fl1)::tl as orlist ->
488 match first_s todo1 with
489 | None -> orlist, acc
490 | Some (((gno,_,_),_,_,_), todo11) ->
491 (* TODO confronto tra todo da ottimizzare *)
492 if gno = id && eq_todo todo11 todo then
493 aux (list_union fl1 acc) tl
501 let close_proof p ty menv context =
503 List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
505 let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
506 naif_closure p menv context
508 (* XXX capire bene quando aggiungere alla cache *)
509 let add_to_cache_and_del_from_orlist_if_green_cut
510 g s m cache key todo orlist fl ctx size minsize
512 let cache = cache_remove_underinspection cache key in
513 (* prima per fare la irl usavamo il contesto vero e proprio e non quello
515 match calculate_closed_goal_ty g s with
516 | None -> assert false
517 | Some (canonical_ctx , gty) ->
518 let goalno,depth,sort = g in
519 let irl = mk_irl canonical_ctx in
520 let goal = Cic.Meta(goalno, irl) in
521 let proof = CicMetaSubst.apply_subst s goal in
522 let green_proof, closed_proof =
523 let b = is_a_green_cut proof in
525 b, (* close_proof proof gty m ctx *) proof
529 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
530 if is_a_green_cut key then
531 (* if the initia goal was closed, we cut alternatives *)
532 let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
533 let orlist, fl = eat_head todo goalno fl orlist in
535 if size < minsize then
536 (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
538 (* if the proof is closed we cache it *)
539 if green_proof then cache_add_success cache key proof
540 else (* cache_add_success cache key closed_proof *)
541 (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
543 cache, orlist, fl, true
546 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
547 if size < minsize then
548 (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
549 (* if the substituted goal and the proof are closed we cache it *)
550 if is_a_green_cut gty then
551 if green_proof then cache_add_success cache gty proof
552 else (* cache_add_success cache gty closed_proof *)
553 (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
557 CicTypeChecker.type_of_aux' ~subst:s
558 m ctx closed_proof CicUniv.oblivion_ugraph
560 if is_a_green_cut ty then
561 cache_add_success cache ty closed_proof
564 | CicTypeChecker.TypeCheckerFailure _ ->*)
565 (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
567 cache, orlist, fl, false
569 let close_failures (fl : fail list) (cache : cache) =
571 (fun cache ((gno,depth,_),gty) ->
572 if CicUtil.is_meta_closed gty then
573 ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
574 cache_add_failure cache gty depth)
579 let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
580 let entry = goalno, (canonical_ctx, t,ty) in
581 assert_subst_are_disjoint subst [entry];
582 let subst = entry :: subst in
584 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
589 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
590 None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
594 tables cache depth fake_proof goalno goalty subst context
597 let active,passive,bag = tables in
598 let ppterm = ppterm context in
599 let status = (fake_proof,goalno) in
600 if flags.use_only_paramod then
602 debug_print (lazy ("PARAMODULATION SU: " ^
603 string_of_int goalno ^ " " ^ ppterm goalty ));
604 let goal_steps, saturation_steps, timeout =
605 max_int,max_int,flags.timeout
608 Saturation.given_clause bag status active passive
609 goal_steps saturation_steps timeout
611 | None, active, passive, bag ->
612 [], (active,passive,bag), cache, flags
613 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
615 assert_subst_are_disjoint subst subst';
616 let subst = subst@subst' in
618 order_new_goals metasenv subst open_goals ppterm
621 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
624 [(!candidate_no,proof),metasenv,subst,open_goals],
625 (active,passive,bag), cache, flags
629 debug_print (lazy ("NARROWING DEL GOAL: " ^
630 string_of_int goalno ^ " " ^ ppterm goalty ));
631 let goal_steps, saturation_steps, timeout =
635 Saturation.solve_narrowing bag status active passive goal_steps
637 | None, active, passive, bag ->
638 [], (active,passive,bag), cache, flags
639 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
641 assert_subst_are_disjoint subst subst';
642 let subst = subst@subst' in
644 order_new_goals metasenv subst open_goals ppterm
647 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
650 [(!candidate_no,proof),metasenv,subst,open_goals],
651 (active,passive,bag), cache, flags
655 let params = ([],["use_context","false"]) in
656 let automation_cache = {
657 AutomationCache.tables = tables ;
658 AutomationCache.univ = Universe.empty; }
661 let ((_,metasenv,subst,_,_,_),open_goals) =
663 solve_rewrite ~params ~automation_cache
666 let proof = lazy (Cic.Meta (-1,[])) in
667 [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
668 with ProofEngineTypes.Fail _ -> [], tables, cache, flags
670 let res = Saturation.all_subsumed bag status active passive in
673 (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
674 assert_subst_are_disjoint subst subst';
675 let subst = subst@subst' in
677 order_new_goals metasenv subst open_goals ppterm
680 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
683 (!candidate_no,proof),metasenv,subst,open_goals)
686 res', (active,passive,bag), cache, flags
693 List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
694 let p1 = List.length (prop_only l1) in
695 let p2 = List.length (prop_only l2) in
696 if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
700 let try_candidate dbd
701 goalty tables subst fake_proof goalno depth context cand
703 let ppterm = ppterm context in
705 let actives, passives, bag = tables in
706 let (_,metasenv,subst,_,_,_), open_goals =
707 ProofEngineTypes.apply_tactic
708 (PrimitiveTactics.apply_tac ~term:cand)
711 let tables = actives, passives,
712 Equality.push_maxmeta bag
713 (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
715 debug_print (lazy (" OK: " ^ ppterm cand));
716 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
717 let open_goals = order_new_goals metasenv subst open_goals ppterm in
718 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
720 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
722 | ProofEngineTypes.Fail s -> None,tables
723 | CicUnification.Uncertain s -> None,tables
726 let applicative_case dbd
727 tables depth subst fake_proof goalno goalty metasenv context
728 signature universe cache flags
732 | Cic.Appl (hd::tl) ->
733 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
736 let goalty_aux = goalty in
738 get_candidates flags.skip_trie_filtering universe cache goalty_aux
740 (* if the goal is an equality we skip the congruence theorems
742 if is_equational_case goalty flags
743 then List.filter not_default_eq_term candidates
746 let candidates = List.filter (only signature context metasenv) candidates
750 (fun (tables,elems) cand ->
752 try_candidate dbd goalty
753 tables subst fake_proof goalno depth context cand
755 | None, tables -> tables, elems
756 | Some x, tables -> tables, x::elems)
757 (tables,[]) candidates
759 let elems = sort_new_elems elems in
763 let try_smart_candidate dbd
764 goalty tables subst fake_proof goalno depth context cand
766 let ppterm = ppterm context in
768 let params = ([],[]) in
769 let automation_cache = {
770 AutomationCache.tables = tables ;
771 AutomationCache.univ = Universe.empty; }
773 debug_print (lazy ("candidato per " ^ string_of_int goalno
774 ^ ": " ^ CicPp.ppterm cand));
776 let (_,metasenv,subst,_,_,_) = fake_proof in
777 prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
778 prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
780 let ((_,metasenv,subst,_,_,_),open_goals) =
781 apply_smart ~dbd ~term:cand ~params ~automation_cache
784 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
785 let open_goals = order_new_goals metasenv subst open_goals ppterm in
786 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
788 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
790 | ProofEngineTypes.Fail s -> None,tables
791 | CicUnification.Uncertain s -> None,tables
794 let smart_applicative_case dbd
795 tables depth subst fake_proof goalno goalty metasenv context signature
800 | Cic.Appl (hd::tl) ->
801 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
804 let smart_candidates =
805 get_candidates flags.skip_trie_filtering universe cache goalty_aux
808 get_candidates flags.skip_trie_filtering universe cache goalty
810 let smart_candidates =
812 (fun x -> not(List.mem x candidates)) smart_candidates
815 (lazy ("smart_candidates" ^ " = " ^
816 (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
817 debug_print debug_msg;
818 let candidates = List.filter (only signature context metasenv) candidates in
819 let smart_candidates =
820 List.filter (only signature context metasenv) smart_candidates
823 let penalty cand depth =
824 if only signature context metasenv cand then depth else ((prerr_endline (
825 "penalizzo " ^ CicPp.ppterm cand));depth -1)
830 (fun (tables,elems) cand ->
832 try_candidate dbd goalty
833 tables subst fake_proof goalno depth context cand
836 (* if normal application fails we try to be smart *)
837 (match try_smart_candidate dbd goalty
838 tables subst fake_proof goalno depth context cand
840 | None, tables -> tables, elems
841 | Some x, tables -> tables, x::elems)
842 | Some x, tables -> tables, x::elems)
843 (tables,[]) candidates
845 let tables, smart_elems =
847 (fun (tables,elems) cand ->
849 try_smart_candidate dbd goalty
850 tables subst fake_proof goalno depth context cand
852 | None, tables -> tables, elems
853 | Some x, tables -> tables, x::elems)
854 (tables,[]) smart_candidates
856 let elems = sort_new_elems (elems @ smart_elems) in
860 let equational_and_applicative_case dbd
861 signature universe flags m s g gty tables cache context
863 let goalno, depth, sort = g in
864 let fake_proof = mk_fake_proof m s g gty context in
865 if is_equational_case gty flags then
866 let elems,tables,cache, flags =
867 equational_case tables cache
868 depth fake_proof goalno gty s context flags
870 let more_elems, tables, cache =
871 if flags.use_only_paramod then
875 tables depth s fake_proof goalno
876 gty m context signature universe cache flags
878 elems@more_elems, tables, cache, flags
880 let elems, tables, cache =
881 match LibraryObjects.eq_URI () with
883 smart_applicative_case dbd tables depth s fake_proof goalno
884 gty m context signature universe cache flags
886 applicative_case dbd tables depth s fake_proof goalno
887 gty m context signature universe cache flags
889 elems, tables, cache, flags
891 let rec condition_for_hint i = function
893 | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
894 | _::tl -> condition_for_hint i tl
896 let prunable_for_size flags s m todo =
897 let rec aux b = function
898 | (S _)::tl -> aux b tl
899 | (D (_,_,T))::tl -> aux b tl
901 (match calculate_goal_ty g s m with
903 | Some (canonical_ctx, gty) ->
906 ~consider_metas:false ~count_metas_occurrences:true gty in
907 let newb = b || gsize > flags.maxgoalsizefactor in
914 let prunable ty todo =
915 let rec aux b = function
916 | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
917 | (D (_,_,T))::tl -> aux b tl
925 let prunable menv subst ty todo =
926 let rec aux = function
927 | (S(_,k,_,_))::tl ->
928 (match Equality.meta_convertibility_subst k ty menv with
931 no_progress variant tl (* || aux tl*))
932 | (D (_,_,T))::tl -> aux tl
934 and no_progress variant = function
935 | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
936 | D ((n,_,P) as g)::tl ->
937 (match calculate_goal_ty g subst menv with
938 | None -> no_progress variant tl
940 (match calculate_goal_ty g variant menv with
941 | None -> assert false
943 if gty = gty' then no_progress variant tl
945 (prerr_endline (string_of_int n);
946 prerr_endline (CicPp.ppterm gty);
947 prerr_endline (CicPp.ppterm gty');
948 prerr_endline "---------- subst";
949 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
950 prerr_endline "---------- variant";
951 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
952 prerr_endline "---------- menv";
953 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
954 no_progress variant tl) *)
956 | _::tl -> no_progress variant tl
961 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
963 HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
965 List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
967 let filter_prune_hint c l =
968 let prune = !prune_hint in
969 prune_hint := []; (* possible race... *)
970 if prune = [] then c,l
972 cache_reset_underinspection c,
973 List.filter (condition_for_prune_hint prune) l
979 auto_all_solutions dbd tables universe cache context metasenv gl flags
984 MetadataConstraints.UriManagerSet.union set
985 (MetadataQuery.signature_of metasenv g)
987 MetadataConstraints.UriManagerSet.empty gl
989 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
992 (fun (x,s) -> D (x,flags.maxdepth,s)) goals
994 let elems = [metasenv,[],1,[],goals,[]] in
995 let rec aux tables solutions cache elems flags =
996 match auto_main dbd tables context flags signature universe cache elems with
997 | Gaveup (tables,cache) ->
998 solutions,cache, tables
999 | Proved (metasenv,subst,others,tables,cache) ->
1000 if Unix.gettimeofday () > flags.timeout then
1001 ((subst,metasenv)::solutions), cache, tables
1003 aux tables ((subst,metasenv)::solutions) cache others flags
1005 let rc = aux tables [] cache elems flags in
1007 | [],cache,tables -> [],cache,tables
1008 | solutions, cache,tables ->
1011 (fun (subst,newmetasenv) ->
1013 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1015 if opened = [] then Some subst else None)
1018 solutions,cache,tables
1021 (******************* AUTO ***************)
1024 let auto dbd flags metasenv tables universe cache context metasenv gl =
1025 let initial_time = Unix.gettimeofday() in
1029 MetadataConstraints.UriManagerSet.union set
1030 (MetadataQuery.signature_of metasenv g)
1032 MetadataConstraints.UriManagerSet.empty gl
1034 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1035 let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1036 let elems = [metasenv,[],1,[],goals,[]] in
1037 match auto_main dbd tables context flags signature universe cache elems with
1038 | Proved (metasenv,subst,_, tables,cache) ->
1040 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1041 Some (subst,metasenv), cache
1042 | Gaveup (tables,cache) ->
1044 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1048 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
1049 let flags = flags_of_params params () in
1050 let use_library = flags.use_library in
1051 let universe, tables, cache =
1052 init_cache_and_tables
1053 ~dbd ~use_library ~use_context:(not flags.skip_context)
1054 automation_cache univ (proof, goal)
1056 let _,metasenv,subst,_,_, _ = proof in
1057 let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1058 let signature = MetadataQuery.signature_of metasenv goal in
1063 CicTypeChecker.type_of_aux' metasenv context t
1064 CicUniv.oblivion_ugraph
1066 MetadataConstraints.UriManagerSet.union set
1067 (MetadataConstraints.constants_of ty)
1072 if flags.close_more then
1074 tables context (proof, goal)
1075 (auto_all_solutions dbd) signature universe cache
1076 else tables,cache in
1077 let initial_time = Unix.gettimeofday() in
1078 let (_,oldmetasenv,_,_,_, _) = proof in
1081 metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
1083 match auto_main dbd tables context flags signature universe cache [elem] with
1084 | Proved (metasenv,subst,_, tables,cache) ->
1086 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1087 let proof,metasenv =
1088 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1089 proof goal subst metasenv
1092 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1093 ~newmetasenv:metasenv
1096 | Gaveup (tables,cache) ->
1099 string_of_float(Unix.gettimeofday()-.initial_time)));
1100 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1104 (****************** types **************)
1105 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
1107 let keys_of_term status t =
1108 let status, orig_ty = typeof status (ctx_of t) t in
1109 let _, ty, _ = saturate ~delta:max_int status orig_ty in
1112 let _, ty = term_of_cic_term status ty (ctx_of ty) in
1114 | NCic.Const (NReference.Ref (_,NReference.Def h))
1115 | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_)
1117 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
1124 let mk_th_cache status gl =
1126 (fun (status, acc) g ->
1127 let gty = get_goalty status g in
1128 let ctx = ctx_of gty in
1129 debug_print(lazy("th cache for: "^ppterm status gty));
1130 debug_print(lazy("th cache in: "^ppcontext status ctx));
1131 if List.mem_assq ctx acc then status, acc else
1132 let idx = InvRelDiscriminationTree.empty in
1135 (fun (status, i, idx) _ ->
1136 let t = mk_cic_term ctx (NCic.Rel i) in
1137 debug_print(lazy("indexing: "^ppterm status t));
1138 let status, keys = keys_of_term status t in
1140 List.fold_left (fun idx k ->
1141 InvRelDiscriminationTree.index idx k t) idx keys
1144 (status, 1, idx) ctx
1146 status, (ctx, idx) :: acc)
1150 let add_to_th t c ty =
1151 let key_c = ctx_of t in
1152 if not (List.mem_assq key_c c) then
1153 (key_c ,InvRelDiscriminationTree.index
1154 InvRelDiscriminationTree.empty ty t ) :: c
1156 let rec replace = function
1158 | (x, idx) :: tl when x == key_c ->
1159 (x, InvRelDiscriminationTree.index idx ty t) :: tl
1160 | x :: tl -> x :: replace tl
1165 let pp_idx status idx =
1166 InvRelDiscriminationTree.iter idx
1168 debug_print(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
1170 (fun t -> debug_print(lazy("\t"^ppterm status t)))
1177 debug_print(lazy( "-----------------------------------------------"));
1178 debug_print(lazy( (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx)));
1179 debug_print(lazy( "||====> "));
1183 let search_in_th gty th =
1184 let c = ctx_of gty in
1185 let rec aux acc = function
1186 | [] -> Ncic_termSet.elements acc
1189 let idx = List.assq k th in
1190 let acc = Ncic_termSet.union acc
1191 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
1194 with Not_found -> aux acc tl
1196 aux Ncic_termSet.empty c
1200 do_types : bool; (* solve goals in Type *)
1208 type goal = int * sort (* goal, depth, sort *)
1209 type fail = goal * cic_term
1210 type candidate = int * Ast.term (* unique candidate number, candidate *)
1212 exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
1213 atoms of the input goals *)
1214 exception Proved of #NTacStatus.tac_status
1216 (* let close_failures _ c = c;; *)
1217 (* let prunable _ _ _ = false;; *)
1218 (* let cache_examine cache gty = `Notfound;; *)
1219 (* let put_in_subst s _ _ _ = s;; *)
1220 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
1221 (* let cache_add_underinspection c _ _ = c;; *)
1222 let equational_case _ _ _ _ _ _ = [];;
1223 let only _ _ _ = true;;
1225 let candidate_no = ref 0;;
1227 let sort_new_elems l =
1228 List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l
1231 let try_candidate flags depth status t =
1233 debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
1234 let status = NTactics.apply_tac ("",0,t) status in
1235 let open_goals = head_goals status#stack in
1237 (lazy ("success: "^String.concat " "(List.map string_of_int open_goals)));
1238 if List.length open_goals > flags.maxwidth ||
1239 (depth = flags.maxdepth && open_goals <> []) then
1240 (debug_print ~depth (lazy "pruned immediately"); None)
1243 Some ((!candidate_no,t),status,open_goals))
1244 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1247 let get_candidates status cache signature gty =
1248 let universe = status#auto_cache in
1249 let context = ctx_of gty in
1250 let _, raw_gty = term_of_cic_term status gty context in
1251 let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1255 List.filter (only signature context)
1256 (NDiscriminationTree.TermSet.elements cands)
1259 let _status, t = term_of_cic_term status t context in Ast.NCic t)
1260 (search_in_th gty cache)
1262 List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
1265 let applicative_case depth signature status flags gty cache =
1266 let tcache,_ = cache in
1267 app_counter:= !app_counter+1;
1268 let candidates = get_candidates status tcache signature gty in
1270 (lazy ("candidates: " ^ string_of_int (List.length candidates)));
1274 match try_candidate flags depth status cand with
1276 | Some x -> x::elems)
1285 (* gty is supposed to be meta-closed *)
1286 let is_subsumed depth status gty (_,cache) =
1287 if cache=[] then false else (
1288 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1289 let n,h,metasenv,subst,obj = status#obj in
1290 let ctx = ctx_of gty in
1291 let _ , target = term_of_cic_term status gty ctx in
1292 let target = NCicSubstitution.lift 1 target in
1293 (* candidates must only be searched w.r.t the given context *)
1296 let idx = List.assq ctx cache in
1297 Ncic_termSet.elements
1298 (InvRelDiscriminationTree.retrieve_generalizations idx gty)
1299 with Not_found -> []
1302 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1306 let _ , source = term_of_cic_term status t ctx in
1308 NCic.Prod("foo",source,target) in
1309 let metasenv,j,_,_ =
1310 NCicMetaSubst.mk_meta
1311 metasenv ctx ~with_type:implication `IsType in
1312 let status = status#set_obj (n,h,metasenv,subst,obj) in
1313 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1315 let status = NTactics.intro_tac "foo" status in
1317 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1319 if (head_goals status#stack = []) then raise Found
1324 with Found -> debug_print ~depth (lazy "success");true)
1328 let equational_and_applicative_case
1329 signature flags status g depth gty cache
1332 if false (*is_equational_case gty flags*) then
1335 signature status flags g gty cache
1338 applicative_case depth
1339 signature status flags gty cache
1344 (*match LibraryObjects.eq_URI () with
1346 smart_applicative_case dbd tables depth s fake_proof goalno
1347 gty m context signature universe cache flags
1349 applicative_case depth
1350 signature status flags gty cache
1355 List.map (fun c,s,gl ->
1356 c,1,1,s,List.map (fun i ->
1358 let gty = get_goalty s i in
1359 let _, sort = typeof s (ctx_of gty) gty in
1360 match term_of_cic_term s sort (ctx_of sort) with
1361 | _, NCic.Sort NCic.Prop -> P
1366 (* let elems = sort_new_elems elems in *)
1370 let rec guess_name name ctx =
1371 if name = "_" then guess_name "auto" ctx else
1372 if not (List.mem_assoc name ctx) then name else
1373 guess_name (name^"'") ctx
1376 let intro ~depth status (tcache,fcache) name =
1377 let status = NTactics.intro_tac name status in
1378 let open_goals = head_goals status#stack in
1379 assert (List.length open_goals = 1);
1380 let open_goal = List.hd open_goals in
1381 let ngty = get_goalty status open_goal in
1382 let ctx = ctx_of ngty in
1383 let t = mk_cic_term ctx (NCic.Rel 1) in
1384 let status, keys = keys_of_term status t in
1385 let tcache = List.fold_left (add_to_th t) tcache keys in
1386 debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
1387 (* unprovability is not stable w.r.t introduction *)
1391 let rec intros ~depth status cache =
1392 let open_goals = head_goals status#stack in
1393 assert (List.length open_goals = 1);
1394 let open_goal = List.hd open_goals in
1395 let gty = get_goalty status open_goal in
1396 let _, raw_gty = term_of_cic_term status gty (ctx_of gty) in
1398 | NCic.Prod (name,_,_) ->
1400 intro ~depth status cache (guess_name name (ctx_of gty))
1401 in intros ~depth status cache
1402 | _ -> status, cache, open_goal
1405 let reduce ~depth status g =
1406 let n,h,metasenv,subst,o = status#obj in
1407 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1408 let ty = NCicUntrusted.apply_subst subst ctx ty in
1409 let ty' = NCicReduction.whd ~subst ctx ty in
1413 (lazy ("reduced to: "^ NCicPp.ppterm ctx subst metasenv ty'));
1415 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1417 let status = status#set_obj (n,h,metasenv,subst,o) in
1419 [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[g,P]])
1422 let do_something signature flags status g depth gty cache =
1423 let l = reduce ~depth status g in
1425 (equational_and_applicative_case
1426 signature flags status g depth gty cache)
1428 sort_new_elems (l@l1), cache
1431 let pp_goal = function
1432 | (_,Continuationals.Stack.Open i)
1433 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1436 let pp_goals status l =
1440 let gty = get_goalty status i in
1441 NTacStatus.ppterm status gty)
1448 let compare = Pervasives.compare
1452 module MS = HTopoSort.Make(M)
1455 let sort_tac status =
1457 match status#stack with
1458 | [] -> assert false
1459 | (goals, t, k, tag) :: s ->
1460 let g = head_goals status#stack in
1462 (List.rev (MS.topological_sort g (deps status))) in
1463 debug_print (lazy ("old g = " ^
1464 String.concat "," (List.map string_of_int g)));
1465 debug_print (lazy ("sorted goals = " ^
1466 String.concat "," (List.map string_of_int sortedg)));
1467 let is_it i = function
1468 | (_,Continuationals.Stack.Open j )
1469 | (_,Continuationals.Stack.Closed j ) -> i = j
1472 List.map (fun i -> List.find (is_it i) goals) sortedg
1474 (sorted_goals, t, k, tag) :: s
1476 status#set_stack gstatus
1479 let clean_up_tac status =
1481 match status#stack with
1482 | [] -> assert false
1483 | (g, t, k, tag) :: s ->
1484 let is_open = function
1485 | (_,Continuationals.Stack.Open _) -> true
1486 | (_,Continuationals.Stack.Closed _) -> false
1488 let g' = List.filter is_open g in
1489 (g', t, k, tag) :: s
1491 status#set_stack gstatus
1494 let focus_tac focus status =
1496 match status#stack with
1497 | [] -> assert false
1498 | (g, t, k, tag) :: s ->
1499 let in_focus = function
1500 | (_,Continuationals.Stack.Open i)
1501 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1503 let focus,others = List.partition in_focus g
1505 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1506 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1508 status#set_stack gstatus
1511 let rec auto_clusters
1512 flags signature cache depth status : unit =
1513 debug_print ~depth (lazy "entering auto clusters");
1514 (* ignore(Unix.select [] [] [] 0.01); *)
1515 let status = clean_up_tac status in
1516 let goals = head_goals status#stack in
1517 if goals = [] then raise (Proved status)
1518 else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
1519 else if List.length goals < 2 then
1520 auto_main flags signature cache depth status
1522 debug_print ~depth (lazy ("goals = " ^
1523 String.concat "," (List.map string_of_int goals)));
1524 let classes = HExtlib.clusters (deps status) goals in
1530 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1535 let status = focus_tac gl status in
1537 debug_print ~depth (lazy ("focusing on" ^
1538 String.concat "," (List.map string_of_int gl)));
1539 auto_main flags signature cache depth status; status
1540 with Proved(status) -> NTactics.merge_tac status)
1542 in raise (Proved status)
1546 (* let rec auto_main flags signature cache status k depth = *)
1548 auto_main flags signature cache depth status: unit =
1549 debug_print ~depth (lazy "entering auto main");
1550 (* ignore(Unix.select [] [] [] 0.01); *)
1551 let status = sort_tac (clean_up_tac status) in
1552 let goals = head_goals status#stack in
1554 | [] -> raise (Proved status)
1556 if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
1559 if tlg=[] then status
1560 else NTactics.branch_tac status in
1561 let status, cache, g = intros ~depth status cache in
1562 let gty = get_goalty status g in
1563 let ctx,ty = close status g in
1564 let closegty = mk_cic_term ctx ty in
1565 let status, gty = apply_subst status (ctx_of gty) gty in
1566 debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
1567 if is_subsumed depth status closegty cache then
1568 (debug_print (lazy "SUBSUMED");
1569 raise (Gaveup IntSet.add g IntSet.empty))
1571 let alternatives, cache =
1572 do_something signature flags status g depth gty cache in
1574 let tcache,fcache = cache in
1575 tcache,add_to_th closegty fcache closegty in
1578 (* the underscore information does not need to be returned
1580 (fun unsat ((_,t),_,_,status,_) ->
1581 let depth',looping_cache =
1582 if t=(Ast.Implicit `JustOne) then depth,cache
1583 else depth+1, loop_cache in
1584 debug_print (~depth:depth')
1585 (lazy ("Case: " ^ CicNotationPp.pp_term t));
1586 try auto_clusters flags signature loop_cache
1587 depth' status; unsat
1590 debug_print (~depth:depth') (lazy "proved");
1591 if tlg=[] then raise (Proved status)
1593 let status = NTactics.merge_tac status
1595 ( (* old cache, here *)
1596 try auto_clusters flags signature cache
1597 depth status; assert false
1600 (lazy ("Unsat1 at depth " ^ (string_of_int depth)
1602 (pp_goals status (IntSet.elements f))));
1603 (* TODO: cache failures *)
1604 IntSet.union f unsat)
1606 debug_print (~depth:depth')
1607 (lazy ("Unsat2 at depth " ^ (string_of_int depth')
1609 (pp_goals status (IntSet.elements f))));
1610 (* TODO: cache local failures *)
1612 IntSet.empty alternatives
1614 raise (Gaveup IntSet.add g unsat)
1617 let int name l def =
1618 try int_of_string (List.assoc name l)
1619 with Failure _ | Not_found -> def
1622 let auto_tac ~params:(_univ,flags) status =
1623 let goals = head_goals status#stack in
1624 let status, cache = mk_th_cache status goals in
1625 (* pp_th status cache; *)
1627 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1629 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1630 String.concat "\n " (List.map (
1631 NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[])
1632 (NDiscriminationTree.TermSet.elements t))
1635 let depth = int "depth" flags 3 in
1636 let size = int "size" flags 10 in
1637 let width = int "width" flags (3+List.length goals) in
1639 let goals = List.map (fun i -> (i,P)) goals in
1640 let signature = () in
1645 timeout = Unix.gettimeofday() +. 3000.;
1648 let initial_time = Unix.gettimeofday() in
1653 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1655 ("Applicative nodes:"^string_of_int !app_counter));
1656 raise (Error (lazy "auto gave up", None)))
1658 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1659 let flags = { flags with maxdepth = x }
1661 try auto_clusters flags signature (cache,[]) 0 status;status
1663 | Gaveup _ -> up_to (x+1) y
1665 print (lazy ("proved at depth " ^ string_of_int x));
1668 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1673 let s = up_to depth depth in
1675 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1677 ("Applicative nodes:"^string_of_int !app_counter));