print_tree.ml 2.99 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26

(*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
27
     and [start] is the branching drawing (["+-"] the first time,
28 29 30
     and then ["|-"]). *)

  let print fmt t =
31
    let rec print_node pref t =
32 33
      let (s, sons) = T.decomp t in
      pp_print_string fmt s;
34
      if sons <> [] then
35 36 37 38 39 40 41
        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
42
      | [] ->
43
          assert false
44
      | [s] ->
45
          pp_print_string fmt "`-"; print_node (pref ^ "  ") s
46
      | s :: sons ->
47 48 49 50 51 52
          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
53

54
end
François Bobot's avatar
François Bobot committed
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100


(*s Tree structures. *)

module type PTree = sig
  type 'a t
  val decomp : 'a t -> string * 'a t list
end

(*s Pretty-print functor. *)

module PMake(T : PTree) = 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