helm/software/lambda-delta/lib/log.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module P = Printf
  13 module F = Format
  14 module C = Cps
  15
  16 type ('a, 'b) item = Term of 'a * 'b
  17                    | Context of 'a
  18                    | Warn of string
  19                    | String of string
  20                    | Loc
  21
  22 type ('a, 'b) specs = {
  23    pp_term   : 'a -> F.formatter -> 'b -> unit;
  24    pp_context: F.formatter -> 'a -> unit
  25 }
  26
  27 let level = ref 0
  28
  29 let loc = ref 0
  30
  31 (* Internal functions *******************************************************)
  32
  33 let std = F.std_formatter
  34
  35 let err = F.err_formatter
  36
  37 let pp_items frm st l items =
  38    let pp_item frm = function
  39       | Term (c, t) -> F.fprintf frm "@,%a" (st.pp_term c) t
  40       | Context c   -> F.fprintf frm "%a" st.pp_context c
  41       | Warn s      -> F.fprintf frm "@,%s" s
  42       | String s    -> F.fprintf frm "%s " s
  43       | Loc         -> F.fprintf frm " (line %u)" !loc
  44    in
  45    let iter map frm l = List.iter (map frm) l in
  46    if !level >= l then F.fprintf frm "%a" (iter pp_item) items
  47
  48 (* Interface functions ******************************************************)
  49
  50 let box l =
  51    if !level >= l then
  52    begin F.fprintf std "@,@[<v 2>%s" "  "; F.pp_print_if_newline std () end
  53
  54 let unbox l = if !level >= l then F.fprintf std "@]"
  55
  56 let flush l = if !level >= l then F.fprintf std "@]@."
  57
  58 let box_err () = F.fprintf err "@[<v>"
  59
  60 let flush_err () = F.fprintf err "@]@."
  61
  62 let log st l items = pp_items std st l items
  63
  64 let error st items = pp_items err st 0 items
  65
  66 let items1 s = [Warn s]
  67
  68 let t_items1 st c t =
  69    [Warn st; Term (c, t)]
  70
  71 let ct_items1 sc c st t =
  72    [Warn sc; Context c; Warn st; Term (c, t)]
  73
  74 let ct_items2 sc c st1 t1 st2 t2 =
  75    ct_items1 sc c st1 t1 @ [Warn st2; Term (c, t2)]
  76
  77 let ct_items3 sc c st1 t1 st2 t2 st3 t3 =
  78    ct_items2 sc c st1 t1 st2 t2 @ [Warn st3; Term (c, t3)]
  79
  80 let warn msg = F.fprintf std "@,%s" msg