src/pretty.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                               TAToo                                 *)
   4 (*                                                                     *)
   5 (*                     Kim Nguyen, LRI UMR8623                         *)
   6 (*                   Université Paris-Sud & CNRS                       *)
   7 (*                                                                     *)
   8 (*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
   9 (*  Recherche Scientifique. All rights reserved.  This file is         *)
  10 (*  distributed under the terms of the GNU Lesser General Public       *)
  11 (*  License, with the special exception on linking described in file   *)
  12 (*  ../LICENSE.                                                        *)
  13 (*                                                                     *)
  14 (***********************************************************************)
  15
  16 open Format
  17
  18 exception InvalidUtf8Codepoint of int
  19
  20 let subscripts = "₀₁₂₃₄₅₆₇₈₉"
  21 let superscripts = "⁰¹²³⁴⁵⁶⁷⁸⁹"
  22
  23 let char_length c =
  24   let code = Char.code c in
  25     if code <= 0x7f then 1
  26     else if 0xc2 <= code && code <= 0xdf then 2
  27     else if 0xe0 <= code && code <= 0xef then 3
  28     else if 0xf0 <= code && code <= 0xf4 then 4
  29     else raise (InvalidUtf8Codepoint code)
  30
  31
  32 let next_char s i len =
  33   let n = i + char_length s.[i] in
  34     if n >= len then -1 else n
  35
  36 let str_len s =
  37   let len = String.length s in
  38   let rec loop i acc =
  39     if i == -1 then acc
  40     else loop (next_char s i len) (acc+1)
  41   in
  42     loop 0 0
  43
  44 let length = str_len
  45
  46 let get_char s i =
  47   let len = String.length s in
  48   let rec loop j count =
  49     if count == i then String.sub s j (char_length s.[j])
  50     else loop (next_char s j len) (count+1)
  51   in
  52     loop 0 0
  53
  54
  55 let format_number digits i =
  56   let s = string_of_int i in
  57   let len = String.length s in
  58   let buf = Buffer.create (len*4) in
  59     for i = 0 to len - 1 do
  60       let d = Char.code s.[i] - Char.code '0' in
  61         Buffer.add_string buf (get_char digits d)
  62     done;
  63     Buffer.contents buf
  64
  65 let rev_explode s =
  66   let len = str_len s in
  67   let rec loop i acc =
  68       if i >= len then acc
  69       else
  70         loop (i+1) ((get_char s i) :: acc)
  71   in
  72       loop 0 []
  73
  74
  75 let explode s = List.rev (rev_explode s)
  76
  77 let combine_all comp s =
  78   let l = rev_explode s in
  79   String.concat "" (List.fold_left (fun acc e -> comp::e::acc) [] l)
  80
  81
  82 let subscript = format_number subscripts
  83 let superscript = format_number superscripts
  84 let down_arrow = "↓"
  85 let up_arrow = "↑"
  86 let right_arrow = "→"
  87 let left_arrow =  "←"
  88 let epsilon = "ϵ"
  89 let big_sigma = "∑"
  90 let cap = "∩"
  91 let cup = "∪"
  92 let lnot = "¬"
  93 let wedge = "∧"
  94 let vee = "∨"
  95 let top = "⊤"
  96 let bottom = "⊥"
  97 let dummy = "☠"
  98 let double_right_arrow = "⇒"
  99 let combining_overbar = "\204\133"
 100 let combining_underbar = "\204\178"
 101 let combining_stroke = "\204\182"
 102 let combining_vertical_line = "\226\131\146"
 103
 104
 105 let overline s = combine_all combining_overbar s
 106 let underline s = combine_all combining_underbar s
 107 let strike s = combine_all combining_stroke s
 108
 109 let mk_repeater c =
 110   let mk_str i = String.make i c in
 111   let _table = Array.init 16 mk_str in
 112      fun i -> try
 113       if i < 16 then _table.(i) else mk_str i
 114     with e -> print_int i; print_newline(); raise e
 115 let padding = mk_repeater ' '
 116 let line = mk_repeater '_'
 117
 118
 119
 120
 121 let ppf f fmt s =
 122   pp_print_string fmt (f s)
 123
 124 let pp_overline = ppf overline
 125 let pp_underline = ppf underline
 126 let pp_strike = ppf strike
 127 let pp_subscript = ppf subscript
 128 let pp_superscript = ppf superscript
 129 let dummy_printer fmt () = ()
 130
 131 let pp_print_list ?(sep=dummy_printer) printer fmt l =
 132   match l with
 133     [] -> ()
 134   | [ e ] -> printer fmt e
 135   | e :: es -> printer fmt e; List.iter
 136     (fun x ->
 137       sep fmt ();
 138       fprintf fmt "%a" printer x) es
 139
 140 let pp_print_array ?(sep=dummy_printer) printer fmt a =
 141   pp_print_list ~sep:sep printer fmt (Array.to_list a)
 142
 143 let print_list ?(sep=" ") printer fmt l =
 144   let sep_printer fmt () =
 145     pp_print_string fmt sep
 146   in
 147   pp_print_list ~sep:sep_printer printer fmt l
 148
 149 let print_array ?(sep=" ") printer fmt a =
 150   print_list ~sep:sep printer fmt (Array.to_list a)
 151
 152