From 3a198e82376610d2bbca3a7aba9ea435271e4ee7 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 8 Feb 2010 07:25:32 +0000 Subject: [PATCH] Removed debug printings. --- helm/software/components/ng_tactics/nnAuto.ml | 69 ++++++++++++------- 1 file changed, 46 insertions(+), 23 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index c9f641cb3..ce0a1b00e 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -55,17 +55,21 @@ let menv_closure status gl = (* we call a "fact" an object whose hypothesis occur in the goal or in types of goal-variables *) -let is_a_fact status ty = - let status, ty, _ = saturate ~delta:0 status ty in - debug_print (lazy (ppterm status ty)); +let is_a_fact status ty = + let status, ty, metas = saturate ~delta:0 status ty in + debug_print (lazy ("saturated ty :" ^ (ppterm status ty))); let g_metas = metas_of_term status ty in let clos = menv_closure status g_metas in - let _,_,metasenv,_,_ = status#obj in + (* let _,_,metasenv,_,_ = status#obj in *) let menv = List.fold_left - (fun acc (i,_) -> IntSet.add i acc) - IntSet.empty metasenv - in IntSet.equal clos menv;; + (fun acc m -> + let _, m = term_of_cic_term status m (ctx_of m) in + match m with + | NCic.Meta(i,_) -> IntSet.add i acc + | _ -> assert false) + IntSet.empty metas + in IntSet.subset menv clos;; let is_a_fact_obj s uri = let obj = NCicEnvironment.get_checked_obj uri in @@ -75,6 +79,14 @@ let is_a_fact_obj s uri = (* aggiungere i costruttori *) | _ -> false +let is_a_fact_ast status subst metasenv ctx cand = + debug_print ~depth:0 + (lazy ("------- checking " ^ CicNotationPp.pp_term cand)); + let status, t = disambiguate status ctx ("",0,cand) None in + let status,t = term_of_cic_term status t ctx in + let ty = NCicTypeChecker.typeof subst metasenv ctx t in + is_a_fact status (mk_cic_term ctx ty) + let current_goal status = let open_goals = head_goals status#stack in assert (List.length open_goals = 1); @@ -112,7 +124,7 @@ let solve fast status eq_cache goal = (status#set_coerc_db NCicCoercion.empty_db) metasenv subst ctx pt (Some gty) *) in - print (lazy (Printf.sprintf "Refined in %fs" + debug_print (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 @@ -163,8 +175,12 @@ let index_local_equations eq_cache status = let t = NCic.Rel !c in try let ty = NCicTypeChecker.typeof [] [] ctx t in - debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty))); - NCicParamod.forward_infer_step eq_cache t ty + if is_a_fact status (mk_cic_term ctx ty) then + (debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty))); + NCicParamod.forward_infer_step eq_cache t ty) + else + (debug_print (lazy ("not a fact: " ^ (NCicPp.ppterm ctx [] [] ty))); + eq_cache) with | NCicTypeChecker.TypeCheckerFailure _ | NCicTypeChecker.AssertFailure _ -> eq_cache) @@ -1418,7 +1434,7 @@ let sort_new_elems l = let try_candidate ?(smart=0) flags depth status eq_cache t = try - print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t)); + debug_print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t)); let status = if smart= 0 then NTactics.apply_tac ("",0,t) status else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status @@ -1429,7 +1445,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache t = let og_no = openg_no status in if (* og_no > flags.maxwidth || *) ((depth + 1) = flags.maxdepth && og_no <> 0) then - (print ~depth (lazy "pruned immediately"); None) + (debug_print ~depth (lazy "pruned immediately"); None) else (incr candidate_no; Some ((!candidate_no,t),status)) @@ -1498,12 +1514,17 @@ let applicative_case depth signature status flags gty (cache:cache) = let sm = 0 in let smart_candidates = [] in *) let sm = if is_eq then 0 else 2 in - let only_one = flags.last && (depth + 1 = flags.maxdepth) in - print (lazy ("only_one: " ^ (string_of_bool only_one))); + 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))); let elems = List.fold_left (fun elems cand -> if (only_one && (elems <> [])) then elems + else + if (maxd && not(is_a_fact_ast status subst metasenv context cand)) + then (debug_print (lazy "pruned: not a fact"); elems) else match try_candidate (~smart:sm) flags depth status cache.unit_eq cand with @@ -1517,6 +1538,9 @@ let applicative_case depth signature status flags gty (cache:cache) = List.fold_left (fun elems cand -> if (only_one && (elems <> [])) then elems + else + if (maxd && not(is_a_fact_ast status subst metasenv context cand)) + then (debug_print (lazy "pruned: not a fact"); elems) else match try_candidate (~smart:1) flags depth status cache.unit_eq cand with @@ -1738,7 +1762,6 @@ let focus_tac focus status = let rec auto_clusters ?(top=false) flags signature cache depth status : unit = debug_print ~depth (lazy "entering auto clusters"); - print (lazy ("auto cluster: " ^ (string_of_bool flags.last))); (* ignore(Unix.select [] [] [] 0.01); *) let status = clean_up_tac status in let goals = head_goals status#stack in @@ -1747,7 +1770,7 @@ let rec auto_clusters ?(top=false) else if List.length goals < 2 then auto_main flags signature cache depth status else - print ~depth (lazy ("goals = " ^ + debug_print ~depth (lazy ("goals = " ^ String.concat "," (List.map string_of_int goals))); let classes = HExtlib.clusters (deps status) goals in let classes = if top then List.rev classes else classes in @@ -1779,7 +1802,6 @@ and of the initial head goals in the stack *) auto_main flags signature (cache:cache) depth status: unit = - print (lazy ("auto enter: " ^ (string_of_bool flags.last))); debug_print ~depth (lazy "entering auto main"); (* ignore(Unix.select [] [] [] 0.01); *) let status = sort_tac (clean_up_tac status) in @@ -1789,7 +1811,7 @@ auto_main flags signature (cache:cache) depth status: unit = | orig::_ -> let ng = List.length goals in if ng > flags.maxwidth then - (print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty)) + (debug_print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty)) else let branch = ng>1 in if depth = flags.maxdepth then raise (Gaveup IntSet.empty) else @@ -1829,7 +1851,8 @@ auto_main flags signature (cache:cache) depth status: unit = (* sistemare *) let flags' = {flags' with last = flags'.last && (not branch)} in - print (lazy ("auto last: " ^ (string_of_bool flags'.last))); + debug_print + (lazy ("auto last: " ^ (string_of_bool flags'.last))); try auto_clusters flags' signature loop_cache depth' status; unsat with @@ -1905,7 +1928,7 @@ let auto_tac ~params:(_univ,flags) status = if x > y then (print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); - print(lazy + debug_print(lazy ("Applicative nodes:"^string_of_int !app_counter)); raise (Error (lazy "auto gave up", None))) else @@ -1916,7 +1939,7 @@ let auto_tac ~params:(_univ,flags) status = with | Gaveup _ -> up_to (x+1) y | Proved s -> - print (lazy ("proved at depth " ^ string_of_int x)); + debug_print (lazy ("proved at depth " ^ string_of_int x)); let stack = match s#stack with | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest @@ -1926,9 +1949,9 @@ let auto_tac ~params:(_univ,flags) status = oldstatus#set_status s in let s = up_to depth depth in - print(lazy + debug_print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); - print(lazy + debug_print(lazy ("Applicative nodes:"^string_of_int !app_counter)); s ;; -- 2.39.2