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