From 45e1b8a5ba04aa3064f8179d1aa387c2b892e007 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 10 Oct 2011 12:18:57 +0000 Subject: [PATCH] Ported changes amde on the main branch: 1. Reintroduced a failure cache 2. Corrected a bug in subsumption 3. Crippled the search space of not-last (side) equational goals. --- matitaB/components/ng_tactics/nnAuto.ml | 289 ++++++++++++++++-------- 1 file changed, 198 insertions(+), 91 deletions(-) diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index 387e644b0..d77fd2f74 100644 --- a/matitaB/components/ng_tactics/nnAuto.ml +++ b/matitaB/components/ng_tactics/nnAuto.ml @@ -12,7 +12,7 @@ open Printf let print ?(depth=0) s = - prerr_endline (String.make depth '\t'^Lazy.force s) + prerr_endline (String.make (2*depth) ' '^Lazy.force s) let noprint ?(depth=0) _ = () let debug_print = noprint @@ -215,7 +215,7 @@ let height_of_goals status = (fun open_goal -> h := max !h (height_of_goal open_goal status)) open_goals; - debug_print (lazy ("altezza sequente: " ^ string_of_int !h)); + noprint (lazy ("altezza sequente: " ^ string_of_int !h)); !h ;; @@ -231,21 +231,21 @@ let solve f status eq_cache goal = let gty = NCicUntrusted.apply_subst status subst ctx gty in let build_status (pt, _, metasenv, subst) = try - debug_print (lazy ("refining: "^(status#ppterm ctx subst metasenv pt))); + noprint (lazy ("refining: "^(status#ppterm ctx subst metasenv pt))); let stamp = Unix.gettimeofday () in let metasenv, subst, pt, pty = (* NCicRefiner.typeof status (* (status#set_coerc_db NCicCoercion.empty_db) *) metasenv subst ctx pt None in - print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt))); - debug_print (lazy ("synt: "^(status#ppterm ctx subst metasenv pty))); + debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt))); + noprint (lazy ("synt: "^(status#ppterm ctx subst metasenv pty))); let metasenv, subst = NCicUnification.unify status metasenv subst ctx gty pty *) NCicRefiner.typeof (status#set_coerc_db NCicCoercion.empty_db) metasenv subst ctx pt (Some gty) in - debug_print (lazy (Printf.sprintf "Refined in %fs" + noprint (lazy (Printf.sprintf "Refined in %fs" (Unix.gettimeofday() -. stamp))); let status = status#set_obj (n,h,metasenv,subst,o) in let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in @@ -288,7 +288,7 @@ let auto_eq_check eq_cache status = ;; let index_local_equations eq_cache status = - debug_print (lazy "indexing equations"); + noprint (lazy "indexing equations"); let open_goals = head_goals status#stack in let open_goal = List.hd open_goals in let ngty = get_goalty status open_goal in @@ -301,10 +301,10 @@ let index_local_equations eq_cache status = try let ty = NCicTypeChecker.typeof status [] [] ctx t in if is_a_fact status (mk_cic_term ctx ty) then - (debug_print(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty))); + (noprint(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty))); NCicParamod.forward_infer_step status [] [] ctx eq_cache t ty) else - (debug_print (lazy ("not a fact: " ^ (status#ppterm ctx [] [] ty))); + (noprint (lazy ("not a fact: " ^ (status#ppterm ctx [] [] ty))); eq_cache) with | NCicTypeChecker.TypeCheckerFailure _ @@ -447,7 +447,7 @@ let ground_instances status gl = List.iter (fun i -> let (_, ctx, t, _) = List.assoc i subst in - debug_print (lazy (status#ppterm ctx [] [] t)); + noprint (lazy (status#ppterm ctx [] [] t)); List.iter (fun (uri,_,_,_,_) as obj -> NCicEnvironment.invalidate_item status (`Obj (uri, obj))) @@ -505,15 +505,15 @@ let close status g = let elems = IntSet.elements subset in let _, ctx, ty = NCicUtils.lookup_meta g metasenv in let ty = NCicUntrusted.apply_subst status subst ctx ty in - debug_print (lazy ("metas in " ^ (status#ppterm ctx [] metasenv ty))); - debug_print (lazy (String.concat ", " (List.map string_of_int elems))); + noprint (lazy ("metas in " ^ (status#ppterm ctx [] metasenv ty))); + noprint (lazy (String.concat ", " (List.map string_of_int elems))); let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in let submenv = List.rev (NCicUntrusted.sort_metasenv status subst submenv) in (* let submenv = metasenv in *) let ty = close_wrt_metasenv status subst ty submenv in - debug_print (lazy (status#ppterm ctx [] [] ty)); + noprint (lazy (status#ppterm ctx [] [] ty)); ctx,ty ;; @@ -575,7 +575,7 @@ let smart_apply t unit_eq status g = let _,_,metasenv,subst,_ = status#obj in let _,ctx,jty = List.assoc j metasenv in let jty = NCicUntrusted.apply_subst status subst ctx jty in - debug_print(lazy("goal " ^ (status#ppterm ctx [] [] jty))); + noprint(lazy("goal " ^ (status#ppterm ctx [] [] jty))); fast_eq_check unit_eq status j with | NCicEnvironment.ObjectNotFound s as e -> @@ -712,8 +712,8 @@ let mk_th_cache status gl = (fun (status, acc) g -> let gty = get_goalty status g in let ctx = ctx_of gty in - debug_print(lazy("th cache for: "^ppterm status gty)); - debug_print(lazy("th cache in: "^ppcontext status ctx)); + noprint(lazy("th cache for: "^ppterm status gty)); + noprint(lazy("th cache in: "^ppcontext status ctx)); if List.mem_assq ctx acc then status, acc else let idx = InvRelDiscriminationTree.empty in let status,_,idx = @@ -721,7 +721,7 @@ let mk_th_cache status gl = (fun (status, i, idx) _ -> let t = mk_cic_term ctx (NCic.Rel i) in let status, keys = keys_of_term status t in - debug_print(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys))); + noprint(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys))); let idx = List.fold_left (fun idx k -> InvRelDiscriminationTree.index idx k t) idx keys @@ -733,6 +733,14 @@ let mk_th_cache status gl = (status,[]) gl ;; +let all_elements ctx cache = + let dummy = mk_cic_term ctx (NCic.Meta (0,(0, (NCic.Irl 0)))) in + try + let idx = List.assq ctx cache in + Ncic_termSet.elements + (InvRelDiscriminationTree.retrieve_unifiables idx dummy) + with Not_found -> [] + let add_to_th t c ty = let key_c = ctx_of t in if not (List.mem_assq key_c c) then @@ -764,7 +772,7 @@ let rm_from_th t c ty = let pp_idx status idx = InvRelDiscriminationTree.iter idx (fun k set -> - debug_print(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k)); + noprint(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k)); Ncic_termSet.iter (fun t -> debug_print(lazy("\t"^ppterm status t))) set) @@ -773,9 +781,9 @@ let pp_idx status idx = let pp_th (status: #NTacStatus.pstatus) = List.iter (fun ctx, idx -> - debug_print(lazy( "-----------------------------------------------")); - debug_print(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx))); - debug_print(lazy( "||====> ")); + noprint(lazy( "-----------------------------------------------")); + noprint(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx))); + noprint(lazy( "||====> ")); pp_idx status idx) ;; @@ -808,6 +816,7 @@ type flags = { type cache = {facts : th_cache; (* positive results *) under_inspection : cic_term list * th_cache; (* to prune looping *) + failures : th_cache; (* to avoid repetitions *) unit_eq : NCicParamod.state; trace: Ast.term list } @@ -838,8 +847,7 @@ type goal = int * sort (* goal, depth, sort *) type fail = goal * cic_term type candidate = int * Ast.term (* unique candidate number, candidate *) -exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive - atoms of the input goals *) +exception Gaveup of th_cache (* failure cache *) exception Proved of NTacStatus.tac_status * Ast.term list (* let close_failures _ c = c;; *) @@ -849,11 +857,13 @@ exception Proved of NTacStatus.tac_status * Ast.term list (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *) (* let cache_add_underinspection c _ _ = c;; *) -let init_cache ?(facts=[]) ?(under_inspection=[],[]) +let init_cache ?(facts=[]) ?(under_inspection=[],[]) + ?(failures=[]) ?(unit_eq=NCicParamod.empty_state) ?(trace=[]) _ = {facts = facts; + failures = failures; under_inspection = under_inspection; unit_eq = unit_eq; trace = trace} @@ -867,10 +877,10 @@ let only signature _context candidate = true let height = fast_height_of_term status candidate_ty in let rc = signature >= height in if rc = false then - debug_print (lazy ("Filtro: " ^ status#ppterm ~context:[] ~subst:[] + noprint (lazy ("Filtro: " ^ status#ppterm ~context:[] ~subst:[] ~metasenv:[] candidate ^ ": " ^ string_of_int height)) else - debug_print (lazy ("Tengo: " ^ status#ppterm ~context:[] ~subst:[] + noprint (lazy ("Tengo: " ^ status#ppterm ~context:[] ~subst:[] ~metasenv:[] candidate ^ ": " ^ string_of_int height)); rc *) @@ -887,7 +897,7 @@ let sort_candidates status ctx candidates = let status,t = term_of_cic_term status ct ctx in let ty = NCicTypeChecker.typeof status subst metasenv ctx t in let res = branch status (mk_cic_term ctx ty) in - debug_print (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = " + noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = " ^ (string_of_int res))); res in @@ -895,7 +905,7 @@ let sort_candidates status ctx candidates = let candidates = List.sort (fun (a,_) (b,_) -> a - b) candidates in let candidates = List.map snd candidates in - debug_print (lazy ("candidates =\n" ^ (String.concat "\n" + noprint (lazy ("candidates =\n" ^ (String.concat "\n" (List.map (NotationPp.pp_term status) candidates)))); candidates @@ -926,9 +936,9 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = let ty = NCicTypeChecker.typeof subst metasenv ctx ct in let res = branch status (mk_cic_term ctx ty) in if smart=1 && og_no > res then - (print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " + (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no))); - print ~depth (lazy "strange application"); None) + debug_print ~depth (lazy "strange application"); None) else *) (incr candidate_no; Some ((!candidate_no,t),status)) @@ -976,14 +986,18 @@ let get_candidates ?(smart=true) depth flags status cache signature gty = let _,_,metasenv,subst,_ = status#obj in let context = ctx_of gty in let _, raw_gty = term_of_cic_term status gty context in + debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty)); let raw_weak_gty, weak_gty = if smart then match raw_gty with | NCic.Appl _ | NCic.Const _ | NCic.Rel _ -> - let weak = perforate_small status subst metasenv context raw_gty in - Some weak, Some (mk_cic_term context weak) + let raw_weak = + perforate_small status subst metasenv context raw_gty in + let weak = mk_cic_term context raw_weak in + debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak)); + Some raw_weak, Some (weak) | _ -> None,None else None,None in @@ -995,7 +1009,7 @@ let get_candidates ?(smart=true) depth flags status cache signature gty = let mapf s = let to_ast = function | NCic.Const r when true (*is_relevant statistics r*) -> Some (Ast.NRef r) - | NCic.Const _ -> None + (* | NCic.Const _ -> None *) | _ -> assert false in HExtlib.filter_map to_ast (NDiscriminationTree.TermSet.elements s) in @@ -1113,7 +1127,7 @@ let applicative_case depth signature status flags gty cache = | NCic.Prod _ -> true, false | _ -> false, NCicParamod.is_equation status metasenv subst context t in - debug_print~depth (lazy (string_of_bool is_eq)); + debug_print ~depth (lazy (string_of_bool is_eq)); (* old let candidates, smart_candidates = get_candidates ~smart:(not is_eq) depth @@ -1148,10 +1162,12 @@ let applicative_case depth signature status flags gty cache = let sm = 0 in let smart_candidates = [] in *) let sm = if is_eq then 0 else 2 in - let maxd = ((depth + 1) = flags.maxdepth) in + (* wrong: we constraint maxdepth for equality goals to three *) + (* let maxdepth = if is_eq then min flags.maxdepth 6 else flags.maxdepth in *) + let maxd = (depth + 1 = flags.maxdepth) in let only_one = flags.last && maxd in - debug_print (lazy ("only_one: " ^ (string_of_bool only_one))); - debug_print (lazy ("maxd: " ^ (string_of_bool maxd))); + debug_print ~depth (lazy ("only_one: " ^ (string_of_bool only_one))); + debug_print ~depth (lazy ("maxd: " ^ (string_of_bool maxd))); let elems = List.fold_left (fun elems cand -> @@ -1159,7 +1175,7 @@ let applicative_case depth signature status flags gty cache = else if (maxd && not(is_prod) & not(is_a_fact_ast status subst metasenv context cand)) - then (debug_print (lazy "pruned: not a fact"); elems) + then (debug_print ~depth (lazy "pruned: not a fact"); elems) else match try_candidate (~smart:sm) flags depth status cache.unit_eq context cand with @@ -1176,9 +1192,9 @@ let applicative_case depth signature status flags gty cache = else if (maxd && not(is_prod) && not(is_a_fact_ast status subst metasenv context cand)) - then (debug_print (lazy "pruned: not a fact"); elems) + then (debug_print ~depth (lazy "pruned: not a fact"); elems) else - match try_candidate (~smart:1) + match try_candidate (~smart:2) (* was smart:1 *) flags depth status cache.unit_eq context cand with | None -> elems | Some x -> x::elems) @@ -1190,22 +1206,50 @@ let applicative_case depth signature status flags gty cache = exception Found ;; + (* gty is supposed to be meta-closed *) -let is_subsumed depth status gty cache = +let is_subsumed depth filter_depth status gty cache = if cache=[] then false else ( debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty))); let n,h,metasenv,subst,obj = status#obj in let ctx = ctx_of gty in - let _ , target = term_of_cic_term status gty ctx in - let target = NCicSubstitution.lift status 1 target in + let _ , raw_gty = term_of_cic_term status gty ctx in + let target = NCicSubstitution.lift status 1 raw_gty in + (* we compute candidates using the perforated type *) + let weak_gty = + match target with + | NCic.Appl _ + | NCic.Const _ + | NCic.Rel _ -> + let raw_weak = + perforate_small status subst metasenv ctx raw_gty in + let weak = mk_cic_term ctx raw_weak in + debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak)); + Some (weak) + | _ -> None + in (* candidates must only be searched w.r.t the given context *) let candidates = try let idx = List.assq ctx cache in - Ncic_termSet.elements - (InvRelDiscriminationTree.retrieve_generalizations idx gty) + match weak_gty with + | Some weak -> + Ncic_termSet.elements + (InvRelDiscriminationTree.retrieve_unifiables idx weak) + |None -> [] with Not_found -> [] in + (* this is a dirty trick: the first argument of an application is used + to remember at which depth a goal failed *) + let filter t = + let ctx = ctx_of t in + let _, src = term_of_cic_term status t ctx in + match src with + | NCic.Appl [NCic.Implicit (`Typeof d); t] + when d <= depth -> Some (mk_cic_term ctx t) + | _ -> None in + let candidates = + if filter_depth then HExtlib.filter_map filter candidates else candidates in debug_print ~depth (lazy ("failure candidates: " ^ string_of_int (List.length candidates))); try @@ -1329,7 +1373,7 @@ let do_something signature flags status g depth gty cache = if l0 <> [] then l0, cache else (* whd *) - let l = (*reduce ~whd:true ~depth status g @*) reduce ~whd:true ~depth status g in + let l = reduce ~whd:true ~depth status g in (* if l <> [] then l,cache else *) (* backward aplications *) let l1 = @@ -1385,9 +1429,9 @@ let sort_tac status = let g = head_goals status#stack in let sortedg = (List.rev (MS.topological_sort g (deps status))) in - debug_print (lazy ("old g = " ^ + noprint (lazy ("old g = " ^ String.concat "," (List.map string_of_int g))); - debug_print (lazy ("sorted goals = " ^ + noprint (lazy ("sorted goals = " ^ String.concat "," (List.map string_of_int sortedg))); let is_it i = function | (_,Continuationals.Stack.Open j ) @@ -1493,14 +1537,14 @@ let rec auto_clusters ?(top=false) if depth = 0 then raise (Proved (status, cache.trace)) else let status = NTactics.merge_tac status in - let cache = - let l,tree = cache.under_inspection in - match l with + let cache = + let l,tree = cache.under_inspection in + match l with | [] -> cache (* possible because of intros that cleans the cache *) | a::tl -> let tree = rm_from_th a tree a in - {cache with under_inspection = tl,tree} - in - auto_clusters flags signature cache (depth-1) status + {cache with under_inspection = tl,tree} + in + auto_clusters flags signature cache (depth-1) status else if List.length goals < 2 then auto_main flags signature cache depth status else @@ -1508,30 +1552,34 @@ let rec auto_clusters ?(top=false) debug_print ~depth (lazy ("goals = " ^ String.concat "," (List.map string_of_int all_goals))); let classes = HExtlib.clusters (deps status) all_goals in - List.iter - (fun gl -> - if List.length gl > flags.maxwidth then - (debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); - raise (Gaveup IntSet.empty)) - else ()) classes; + (* if any of the classes exceed maxwidth we fail *) + List.iter + (fun gl -> + if List.length gl > flags.maxwidth then + begin + debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); + HLog.warn (sprintf "global width (%u) exceeded: %u" + flags.maxwidth (List.length gl)); + raise (Gaveup cache.failures) + end else ()) classes; if List.length classes = 1 then let flags = {flags with last = (List.length all_goals = 1)} in (* no need to cluster *) - auto_main flags signature cache depth status + auto_main flags signature cache depth status else - let classes = if top then List.rev classes else classes in + let classes = if top then List.rev classes else classes in debug_print ~depth (lazy (String.concat "\n" (List.map - (fun l -> - ("cluster:" ^ String.concat "," (List.map string_of_int l))) + (fun l -> + ("cluster:" ^ String.concat "," (List.map string_of_int l))) classes))); - let status,trace,b = + (* we now process each cluster *) + let status,cache,b = List.fold_left - (fun (status,trace,b) gl -> - let cache = {cache with trace = trace} in + (fun (status,cache,b) gl -> let flags = {flags with last = (List.length gl = 1)} in let lold = List.length status#stack in @@ -1545,17 +1593,20 @@ let rec auto_clusters ?(top=false) with | Proved(status,trace) -> let status = NTactics.merge_tac status in + let cache = {cache with trace = trace} in let lnew = List.length status#stack in assert (lold = lnew); - (status,trace,true) - | Gaveup _ when top -> (status,trace,b) + (status,cache,true) + | Gaveup failures when top -> + let cache = {cache with failures = failures} in + (status,cache,b) ) - (status,cache.trace,false) classes + (status,cache,false) classes in let rec final_merge n s = if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s) in let status = final_merge depth status - in if b then raise (Proved(status,trace)) else raise (Gaveup IntSet.empty) + in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures) and @@ -1595,33 +1646,57 @@ auto_main flags signature cache depth status: unit = else let ng = List.length goals in (* moved inside auto_clusters *) - if ng > flags.maxwidth then - (print ~depth (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty)) - else if depth = flags.maxdepth then - raise (Gaveup IntSet.empty) + if ng > flags.maxwidth then begin + debug_print ~depth (lazy "FAIL LOCAL WIDTH"); + HLog.warn (sprintf "local width (%u) exceeded: %u" + flags.maxwidth ng); + raise (Gaveup cache.failures) + end else if depth = flags.maxdepth then + raise (Gaveup cache.failures) else let status = NTactics.branch_tac ~force:true status in let g,gctx, gty = current_goal status in let ctx,ty = close status g in let closegty = mk_cic_term ctx ty in let status, gty = apply_subst status gctx gty in - debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty)); - if is_subsumed depth status closegty (snd cache.under_inspection) then + debug_print ~depth (lazy("Attacking goal " ^ + string_of_int g ^ " : "^ppterm status gty)); + debug_print ~depth (lazy ("current failures: " ^ + string_of_int (List.length (all_elements ctx cache.failures)))); + let is_eq = + let _,_,metasenv,subst,_ = status#obj in + NCicParamod.is_equation status metasenv subst ctx ty in + (* if the goal is an equality we artificially raise its depth up to + flags.maxdepth - 1 *) + if (not flags.last && is_eq && (depth < (flags.maxdepth -1))) then + (* for efficiency reasons, in this case we severely cripple the + search depth *) + (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1))); + auto_main flags signature cache (depth+1) status) + (* check for loops *) + else if is_subsumed depth false status closegty (snd cache.under_inspection) then (debug_print ~depth (lazy "SUBSUMED"); - raise (Gaveup IntSet.add g IntSet.empty)) + raise (Gaveup cache.failures)) + (* check for failures *) + else if is_subsumed depth true status closegty cache.failures then + (debug_print ~depth (lazy "ALREADY MET"); + raise (Gaveup cache.failures)) else let new_sig = height_of_goal g status in if new_sig < signature then - (debug_print (lazy ("news = " ^ (string_of_int new_sig))); - debug_print (lazy ("olds = " ^ (string_of_int signature)))); + (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig))); + debug_print ~depth (lazy ("olds = " ^ (string_of_int signature)))); let alternatives, cache = do_something signature flags status g depth gty cache in let loop_cache = - let l,tree = cache.under_inspection in - let l,tree = closegty::l, add_to_th closegty tree closegty in - {cache with under_inspection = l,tree} in - List.iter - (fun ((_,t),status) -> + if flags.last then + let l,tree = cache.under_inspection in + let l,tree = closegty::l, add_to_th closegty tree closegty in + {cache with under_inspection = l,tree} + else cache in + let failures = + List.fold_left + (fun allfailures ((_,t),status) -> debug_print ~depth (lazy ("(re)considering goal " ^ (string_of_int g) ^" : "^ppterm status gty)); @@ -1633,13 +1708,25 @@ auto_main flags signature cache depth status: unit = then depth, cache else depth+1,loop_cache in let cache = add_to_trace status ~depth cache t in + let cache = {cache with failures = allfailures} in try - auto_clusters flags signature cache depth status - with Gaveup _ -> + auto_clusters flags signature cache depth status; + assert false; + with Gaveup fail -> debug_print ~depth (lazy "Failed"); - ()) - alternatives; - raise (debug_print(lazy "no more candidates"); Gaveup IntSet.empty) + fail) + cache.failures alternatives in + let failures = + if flags.last then + let newfail = + let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in + mk_cic_term ctx dty + in + prerr_endline ("FAILURE : " ^ ppterm status gty); + add_to_th newfail failures closegty + else failures in + debug_print ~depth (lazy "no more candidates"); + raise (Gaveup failures) ;; let int name l def = @@ -1710,7 +1797,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = app_counter:= 0; let rec up_to x y = if x > y then - (print(lazy + (debug_print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); debug_print(lazy ("Applicative nodes:"^string_of_int !app_counter)); @@ -1757,3 +1844,23 @@ let auto_tac ~params:(_,flags as params) ?trace_ref = fast_eq_check_tac ~params else auto_tac ~params ?trace_ref ;; + + + + + + + + + + + + + + + + + + + + -- 2.39.2