X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Futils%2Fpretty.ml;fp=src%2Futils%2Fpretty.ml;h=c54d0edc526a9e0fdbed10dfe5bdbdbeffc2ab22;hp=0000000000000000000000000000000000000000;hb=30bc0bb1291426e5e26eb2dee1ffc41e4c246349;hpb=d9c0e4863807eaf472e875a4bad35cfefe985c95

diff --git a/src/utils/pretty.ml b/src/utils/pretty.ml
new file mode 100644
index 0000000..c54d0ed
--- /dev/null
+++ b/src/utils/pretty.ml
@@ -0,0 +1,156 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-01-30 19:08:11 CET by Kim Nguyen>
+*)
+
+open Format
+
+exception InvalidUtf8Codepoint of int
+
+let subscripts = "₀₁₂₃₄₅₆₇₈₉"
+let superscripts = "⁰¹²³⁴⁵⁶⁷⁸⁹"
+
+let char_length c =
+  let code = Char.code c in
+    if code <= 0x7f then 1
+    else if 0xc2 <= code && code <= 0xdf then 2
+    else if 0xe0 <= code && code <= 0xef then 3
+    else if 0xf0 <= code && code <= 0xf4 then 4
+    else raise (InvalidUtf8Codepoint code)
+
+
+let next_char s i len =
+  let n = i + char_length s.[i] in
+    if n >= len then -1 else n
+
+let str_len s =
+  let len = String.length s in
+  let rec loop i acc =
+    if i == -1 then acc
+    else loop (next_char s i len) (acc+1)
+  in
+    loop 0 0
+
+let length = str_len
+
+let get_char s i =
+  let len = String.length s in
+  let rec loop j count =
+    if count == i then String.sub s j (char_length s.[j])
+    else loop (next_char s j len) (count+1)
+  in
+    loop 0 0
+
+
+let format_number digits i =
+  let s = string_of_int i in
+  let len = String.length s in
+  let buf = Buffer.create (len*4) in
+    for i = 0 to len - 1 do
+      let d = Char.code s.[i] - Char.code '0' in
+	Buffer.add_string buf (get_char digits d)
+    done;
+    Buffer.contents buf
+
+let rev_explode s =
+  let len = str_len s in
+  let rec loop i acc =
+      if i >= len then acc
+      else
+	loop (i+1) ((get_char s i) :: acc)
+  in
+      loop 0 []
+
+
+let explode s = List.rev (rev_explode s)
+
+let combine_all comp s =
+  let l = rev_explode s in
+  String.concat "" (List.fold_left (fun acc e -> comp::e::acc) [] l)
+
+
+let subscript = format_number subscripts
+let superscript = format_number superscripts
+let down_arrow = "↓"
+let up_arrow = "↑"
+let right_arrow = "→"
+let left_arrow =  "←"
+let epsilon = "ϵ"
+let big_sigma = "∑"
+let cap = "∩"
+let cup = "∪"
+let lnot = "¬"
+let wedge = "∧"
+let vee = "∨"
+let top = "⊤"
+let bottom = "⊥"
+let dummy = "☠"
+let double_right_arrow = "⇒"
+let combining_overbar = "\204\133"
+let combining_underbar = "\204\178"
+let combining_stroke = "\204\182"
+let combining_vertical_line = "\226\131\146"
+
+
+let overline s = combine_all combining_overbar s
+let underline s = combine_all combining_underbar s
+let strike s = combine_all combining_stroke s
+
+let mk_repeater c =
+  let mk_str i = String.make i c in
+  let _table = Array.init 16 mk_str in
+     fun i -> try
+      if i < 16 then _table.(i) else mk_str i
+    with e -> print_int i; print_newline(); raise e
+let padding = mk_repeater ' '
+let line = mk_repeater '_'
+
+
+
+
+let ppf f fmt s =
+  pp_print_string fmt (f s)
+
+let pp_overline = ppf overline
+let pp_underline = ppf underline
+let pp_strike = ppf strike
+let pp_subscript = ppf subscript
+let pp_superscript = ppf superscript
+let dummy_printer fmt () = ()
+
+let pp_print_list ?(sep=dummy_printer) printer fmt l =
+  match l with
+    [] -> ()
+  | [ e ] -> printer fmt e
+  | e :: es -> printer fmt e; List.iter
+    (fun x ->
+      sep fmt ();
+      fprintf fmt "%a" printer x) es
+
+let pp_print_array ?(sep=dummy_printer) printer fmt a =
+  pp_print_list ~sep:sep printer fmt (Array.to_list a)
+
+let print_list ?(sep=" ") printer fmt l =
+  let sep_printer fmt () =
+    pp_print_string fmt sep
+  in
+  pp_print_list ~sep:sep_printer printer fmt l
+
+let print_array ?(sep=" ") printer fmt a =
+  print_list ~sep:sep printer fmt (Array.to_list a)
+
+