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                    | LEnv 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_lenv: F.formatter -> 'a -> unit
  27 }
  28
  29 let level = ref 0
  30
  31 let loc = ref "unknown location"
  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       | LEnv c      -> F.fprintf frm "%a" st.pp_lenv c
  43       | Warn s      -> F.fprintf frm "@,%s" s
  44       | String s    -> F.fprintf frm "%s " s
  45       | Loc         -> F.fprintf frm " <%s>" !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 et_items1 sc c st t =
  74    [Warn sc; LEnv c; Warn st; Term (c, t)]
  75
  76 let et_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 =
  77    let tl = match sc2, c2 with
  78       | Some sc2, Some c2 -> et_items1 sc2 c2 st2 t2
  79       | None, None        -> t_items1 st2 c1 t2
  80       | _                 -> assert false
  81    in
  82    et_items1 sc1 c1 st1 t1 @ tl
  83
  84 let et_items3 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 ?sc3 ?c3 st3 t3 =
  85    let tl = match sc3, c3 with
  86       | Some sc3, Some c3 -> et_items1 sc3 c3 st3 t3
  87       | None, None        -> t_items1 st3 c1 t3
  88       | _                 -> assert false
  89    in
  90    et_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 @ tl
  91
  92 let warn msg = F.fprintf std "@,%s" msg