From f8e2e9eebbb16c061f7b6dde75cf822e0873be9b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 21 Oct 2009 14:27:38 +0000 Subject: [PATCH] more printings --- helm/software/components/ng_tactics/nAuto.ml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index 8506c3adb..c72550744 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -1335,6 +1335,15 @@ let auto_tac ~params:(_univ,flags) status = let goals = head_goals status#stack in let status, cache = mk_th_cache status goals in (* pp_th status cache; *) +(* + NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t -> + debug_print (lazy( + NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^ + String.concat "\n " (List.map ( + NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[]) + (NDiscriminationTree.TermSet.elements t)) + ))); +*) let depth = int "depth" flags 3 in let size = int "size" flags 10 in let width = int "width" flags (3+List.length goals) in @@ -1351,6 +1360,7 @@ let auto_tac ~params:(_univ,flags) status = let rec up_to x = if x > depth then raise (Error (lazy "auto gave up", None)) else + let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in match auto_main flags signature (elems x) cache with | Gaveup -> up_to (x+1) | Proved (s, (_orlist, _cache)) -> @@ -1380,6 +1390,11 @@ let group_by_tac eq_predicate tactic status = with Not_found -> aux ([g] :: classes) tl in let classes = aux [] goals in + List.iter + (fun l -> + HLog.debug ("cluster:" ^ + String.concat "," (List.map string_of_int l))) + classes; let pos_of l1 l2 = let l2 = HExtlib.list_mapi (fun x i -> x,i+1) l2 in List.map (fun x -> List.assoc x l2) l1 -- 2.39.2