From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 23 Oct 2009 14:04:42 +0000 (+0000)
Subject: added code to print the tree
X-Git-Tag: make_still_working~3256
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=204600c93b7e4d0bbd8c414835c6d57917b1f1a0;p=helm.git

added code to print the tree
---

diff --git a/helm/software/components/ng_tactics/zipTree.ml b/helm/software/components/ng_tactics/zipTree.ml
index 77a724f40..2259ae528 100644
--- a/helm/software/components/ng_tactics/zipTree.ml
+++ b/helm/software/components/ng_tactics/zipTree.ml
@@ -33,6 +33,8 @@ module type ZipTree = sig
 
   val inject: tree -> position -> position
   val eject: position -> tree
+  
+  val dump: position -> Format.formatter -> unit
 
 end
 
@@ -103,5 +105,29 @@ let previsit f acc (p : position) =
    aux acc (eject p)
 ;;
 
+let dump pos fmt =
+  let module Pp = GraphvizPp.Dot in
+  let tree = root pos in
+  let where = eject pos in
+  let c = ref 0 in
+  let rec aux (Node l as orig) =
+    let j = !c in
+    Pp.node ("node"^string_of_int j) ~attrs:(["shape","record"; 
+      "label",String.concat "|"
+        (HExtlib.list_mapi 
+          (fun (x,_) i -> "<f"^string_of_int i^">" ^ T.pp x)
+        l)] @ if orig == where then ["style","rounded"] else []) fmt;
+    ignore(HExtlib.list_mapi 
+      (fun (_,t) i -> 
+         incr c;
+         let k = !c in
+         Pp.edge 
+           ("node"^string_of_int j^":f"^string_of_int i)
+           ("node"^string_of_int k) fmt;
+         aux t)
+      l)
+  in
+   aux tree
+;;
 
 end
diff --git a/helm/software/components/ng_tactics/zipTree.mli b/helm/software/components/ng_tactics/zipTree.mli
index a74206cc3..6a6c4d67f 100644
--- a/helm/software/components/ng_tactics/zipTree.mli
+++ b/helm/software/components/ng_tactics/zipTree.mli
@@ -36,6 +36,8 @@ module type ZipTree = sig
   val inject: tree -> position -> position
   val eject: position -> tree
 
+  val dump: position -> Format.formatter -> unit
+
 end
 
 module Make(T : Elem) : ZipTree with type t = T.t