From d94fe51e1c4c5ae9a71032f1072f2dfb2d29faf6 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 27 Apr 2007 14:00:24 +0000 Subject: [PATCH] Subst is passed in input to apapluy, so no need to concatenate the results --- components/tactics/auto.ml | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index aca89bd4a..6a31bd347 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -26,7 +26,7 @@ open AutoTypes;; open AutoCache;; -let debug = false;; +let debug = true;; let debug_print s = if debug then prerr_endline (Lazy.force s);; @@ -708,8 +708,8 @@ let try_candidate in debug_print (lazy (" OK: " ^ ppterm cand)); let metasenv = CicRefine.pack_coercion_metasenv metasenv in - assert_subst_are_disjoint subst subst'; - let subst = subst@subst' in + (* assert_subst_are_disjoint subst subst'; *) + let subst = subst' in let open_goals = order_new_goals metasenv subst open_goals ppterm in let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in Some (metasenv,subst,open_goals), tables , maxmeta @@ -792,10 +792,12 @@ let rec auto_main tables maxm context flags elems universe cache = debug_print (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty)); debug_print (lazy (AutoCache.cache_print context cache)); - if sort = T && tl <> [] then (* FIXME!!!! *) + if sort = T (* && tl <> []*) then + Success (metasenv,subst,tl), tables, cache,maxm + (* (debug_print (lazy (" FAILURE(not in prop)")); - aux flags tables maxm cache tl (* FAILURE (not in prop) *)) + aux flags tables maxm cache tl (* FAILURE (not in prop) *)) *) else match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with | Fail s, tables, cache, maxm' -> @@ -818,12 +820,12 @@ let rec auto_main tables maxm context flags elems universe cache = debug_print (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof)); if is_a_green_cut goalty then - (assert_proof_is_valid proof metasenv context goalty; + (* assert_proof_is_valid proof metasenv context goalty; *) let cache = cache_add_success sort cache goalty proof in - aux flags tables maxm cache ((metasenv,subst,gl)::tl)) + aux flags tables maxm cache ((metasenv,subst,gl)::tl) else (let goalty = CicMetaSubst.apply_subst subst goalty in - assert_proof_is_valid proof metasenv context goalty; + (* assert_proof_is_valid proof metasenv context goalty; *) let cache = if is_a_green_cut goalty then cache_add_success sort cache goalty proof @@ -848,6 +850,10 @@ let rec auto_main tables maxm context flags elems universe cache = let goalty = CicMetaSubst.apply_subst subst goalty in (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *) (* FAILURE (euristic cut) *) + if depth <= 0 then + Fail (string_of_int goalno ^ "as depth <=0"), + tables,cache,maxm (*FAILURE(depth)*) + else match cache_examine cache goalty with | Failed_in d when d >= depth -> Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth), -- 2.39.2