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
  21 type ('a, 'b) specs = {
  22    pp_term   : F.formatter -> 'a -> 'b -> unit;
  23    pp_context: F.formatter -> 'a -> unit
  24 }
  25
  26 let level = ref 0
  27
  28 (* Internal functions *******************************************************)
  29
  30 let init =
  31    let started = ref false in
  32    fun () ->
  33       if !started then () else
  34       begin P.printf "\n"; started := true end
  35
  36 let pp_items frm st l items =
  37    let pp_item = function
  38       | Term (c, t) -> st.pp_context frm c; st.pp_term frm c t
  39       | Context c   -> st.pp_context frm c
  40       | Warn s      -> F.fprintf frm "@[%s\n@]" s
  41       | String s    -> F.fprintf frm "@[%s @]" s
  42    in
  43    if !level >= l then List.iter pp_item items
  44
  45 (* Interface functions ******************************************************)
  46
  47 let warn msg =
  48    init (); P.printf " %s\n" msg; flush stdout
  49
  50 let log st l items = pp_items F.std_formatter st l items
  51
  52 let error st items = pp_items F.err_formatter st 0 items
  53
  54 let items1 s = [Warn s]
  55
  56 let ct_items1 s c t =
  57    [Warn s; Term (c, t)]
  58
  59 let ct_items2 s1 c1 t1 s2 c2 t2 =
  60    [Warn s1; Term (c1, t1); Warn s2; Term (c2, t2)]