From 204600c93b7e4d0bbd8c414835c6d57917b1f1a0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 23 Oct 2009 14:04:42 +0000 Subject: [PATCH] added code to print the tree --- .../software/components/ng_tactics/zipTree.ml | 26 +++++++++++++++++++ .../components/ng_tactics/zipTree.mli | 2 ++ 2 files changed, 28 insertions(+) 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 -> "" ^ 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 -- 2.39.2