print_tree.ml 2.51 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(*s Tree structures. *)

module type Tree = sig
  type t
  val decomp : t -> string * t list
end

(*s Pretty-print functor. *)

module Make(T : Tree) = struct

  open Format

  (* [print_node] prints one node and [print_sons] its children.
     [pref] is the prefix to output at the beginning of line
     and [start] is the branching drawing (["+-"] the first time, 
     and then ["|-"]). *)

  let print fmt t =
    let rec print_node pref t = 
      let (s, sons) = T.decomp t in
      pp_print_string fmt s;
      if sons <> [] then 
        let w = String.length s in
        let pref' = pref ^ String.make (w + 1) ' ' in
        match sons with
          | [t'] -> pp_print_string fmt "---"; print_node (pref' ^ "  ") t'
          | _ -> pp_print_string fmt "-"; print_sons pref' "+-" sons

    and print_sons pref start = function
      | [] -> 
          assert false
      | [s] -> 
          pp_print_string fmt "`-"; print_node (pref ^ "  ") s
      | s :: sons -> 
          pp_print_string fmt start; print_node (pref ^ "| ") s;
          pp_force_newline fmt (); pp_print_string fmt pref;
          print_sons pref "|-" sons

    in
    print_node "" t
        
end