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 77a724f405bc7ee447d5ca8ad42e55452e897a68..2259ae5283abab16d51803e6a7ffc2208d1bff1a 100644 (file)
--- 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 a74206cc3b4256833e3fec2a9b6f97f1f6da82b3..6a6c4d67f4a51d3dbb1ef937eb664680c319ba10 100644 (file)
--- 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