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) message = ('a, 'b) item list
  23
  24 type ('a, 'b) specs = {
  25    pp_term   : 'a -> F.formatter -> 'b -> unit;
  26    pp_context: F.formatter -> 'a -> unit
  27 }
  28
  29 let level = ref 0
  30
  31 let loc = ref 0
  32
  33 (* Internal functions *******************************************************)
  34
  35 let std = F.std_formatter
  36
  37 let err = F.err_formatter
  38
  39 let pp_items frm st l items =
  40    let pp_item frm = function
  41       | Term (c, t) -> F.fprintf frm "@,%a" (st.pp_term c) t
  42       | Context c   -> F.fprintf frm "%a" st.pp_context c
  43       | Warn s      -> F.fprintf frm "@,%s" s
  44       | String s    -> F.fprintf frm "%s " s
  45       | Loc         -> F.fprintf frm " (line %u)" !loc
  46    in
  47    let iter map frm l = List.iter (map frm) l in
  48    if !level >= l then F.fprintf frm "%a" (iter pp_item) items
  49
  50 (* Interface functions ******************************************************)
  51
  52 let box l =
  53    if !level >= l then
  54    begin F.fprintf std "@,@[<v 2>%s" "  "; F.pp_print_if_newline std () end
  55
  56 let unbox l = if !level >= l then F.fprintf std "@]"
  57
  58 let flush l = if !level >= l then F.fprintf std "@]@."
  59
  60 let box_err () = F.fprintf err "@[<v>"
  61
  62 let flush_err () = F.fprintf err "@]@."
  63
  64 let log st l items = pp_items std st l items
  65
  66 let error st items = pp_items err st 0 items
  67
  68 let items1 s = [Warn s]
  69
  70 let t_items1 st c t =
  71    [Warn st; Term (c, t)]
  72
  73 let ct_items1 sc c st t =
  74    [Warn sc; Context c; Warn st; Term (c, t)]
  75
  76 let ct_items2 sc1 c1 st1 t1 sc2 c2 st2 t2 =
  77    ct_items1 sc1 c1 st1 t1 @ ct_items1 sc2 c2 st2 t2
  78
  79 let ct_items3 sc c st1 t1 st2 t2 st3 t3 =
  80    ct_items1 sc c st1 t1 @ [Warn st2; Term (c, t2); Warn st3; Term (c, t3)]
  81
  82 let warn msg = F.fprintf std "@,%s" msg