From: Andrea Asperti Date: Mon, 30 Apr 2007 10:31:15 +0000 (+0000) Subject: Removed an assert false; everything works again, but something X-Git-Tag: 0.4.95@7852~493 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8a7a410e8829c66c9cc70d11e2cd7d9abd55b6da;p=helm.git Removed an assert false; everything works again, but something is clearly wrong (to be fixed). --- diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index 6a31bd347..e85b89b95 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -745,7 +745,8 @@ let is_a_green_cut goalty = CicUtil.is_meta_closed goalty ;; -let prop = function (_,_,P) -> true | _ -> false;; +let prop = function (_,depth,P) -> depth < 9 | _ -> false;; + let calculate_timeout flags = if flags.timeout = 0. then (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity}) @@ -790,10 +791,12 @@ let rec auto_main tables maxm context flags elems universe cache = try let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in debug_print - (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty)); + (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty ^ + "with depth"^string_of_int depth)); debug_print (lazy (AutoCache.cache_print context cache)); if sort = T (* && tl <> []*) then - Success (metasenv,subst,tl), tables, cache,maxm + aux flags tables maxm cache ((metasenv,subst,gl)::tl) + (* Success (metasenv,subst,tl), tables, cache,maxm *) (* (debug_print (lazy (" FAILURE(not in prop)")); @@ -847,6 +850,7 @@ let rec auto_main tables maxm context flags elems universe cache = aux flags tables maxm cache ((metasenv,subst,gl)::tl) and aux_single flags tables maxm universe cache metasenv subst (goalno, depth, _) goalty cc = + (* let flags = if depth < 10 then {flags with maxwidth=3} else flags in *) let goalty = CicMetaSubst.apply_subst subst goalty in (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *) (* FAILURE (euristic cut) *) @@ -865,7 +869,9 @@ let rec auto_main tables maxm context flags elems universe cache = let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in debug_print (lazy (" CACHE HIT!")); Success (metasenv, subst, []), tables, cache, maxm - | UnderInspection -> Fail "looping",tables,cache, maxm + | UnderInspection -> + (* assert (not (is_a_green_cut goalty)); *) + Fail "looping",tables,cache, maxm | Notfound | Failed_in _ when depth > 0 -> (* we have more depth now *) let cache = cache_add_underinspection cache goalty depth in