(* This file is part of the Kind 2 model checker.

   Copyright (c) 2015 by the Board of Trustees of the University of Iowa

   Licensed under the Apache License, Version 2.0 (the "License"); you
   may not use this file except in compliance with the License.  You
   may obtain a copy of the License at

   http://www.apache.org/licenses/LICENSE-2.0 

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
   implied. See the License for the specific language governing
   permissions and limitations under the License. 

*)

open KindPretty
open KindLib


(* Signature of module for reuse in Event *)
module type Sig = sig
  type 'a log_printer =
    KindLib.log_level ->
    ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a
  type 'a m_log_printer =
    KindLib.kind_module -> 'a log_printer
  val set_module : KindLib.kind_module -> unit 
  val get_module : unit -> KindLib.kind_module
  type log_format = | F_pt | F_xml | F_json | F_relay
  val get_log_format : unit -> log_format
  val set_log_format : log_format -> unit
  val set_log_format_pt : unit -> unit
  val set_log_format_xml : unit -> unit
  val set_log_format_json : unit -> unit
  val set_relay_log : unit -> unit
  val unset_relay_log : unit -> unit
  val pp_print_kind_module_xml_src : Format.formatter -> KindLib.kind_module -> unit
  val print_xml_trailer : unit -> unit
  val printf_xml : 'a m_log_printer
  val printf_json : 'a m_log_printer
  val parse_log_xml : KindLib.log_level -> KindLib.position -> string -> unit
  val parse_log_json : KindLib.log_level -> KindLib.position -> string -> unit
end



(* ********************************************************************** *)
(* Initialization for the messaging system                                *)
(* ********************************************************************** *)

type 'a log_printer =
  KindLib.log_level ->
  ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a

type 'a m_log_printer =
  KindLib.kind_module -> 'a log_printer

(* Module currently running *)
let this_module = ref `Parser

(* Set module currently running *)
let set_module mdl = this_module := mdl 

(* Get module currently running *)
let get_module () = !this_module


(* ********************************************************************** *)
(* State of the logger                                                    *)
(* ********************************************************************** *)


(* Log formats *)
type log_format = 
  | F_pt
  | F_xml
  | F_json
  | F_relay


(* Current log format *)
let log_format = ref F_pt
let prev_log_format = ref !log_format

let get_log_format () = !log_format
let set_log_format l = log_format := l




(* ********************************************************************** *)
(* Plain text output                                                      *)
(* ********************************************************************** *)


(* Pretty-print kind module for plain text output *)
let pp_print_kind_module_pt =
  pp_print_kind_module


(* Output message as plain text *)
let printf_pt mdl level fmt =
  (ignore_or_fprintf level)
    !log_ppf ("%a @[<hov>" ^^ fmt ^^ "@]@.@.") tag_of_level level


(* Unconditional printing as plain text. *)
let printf_pt_uncond mdl fmt =
  Format.fprintf !log_ppf ("@[<hov>" ^^ fmt ^^ "@]@.@.")



(* ********************************************************************** *)
(* XML output                                                             *)
(* ********************************************************************** *)

(* Level to class attribute of log tag *)
let xml_cls_of_level = string_of_log_level

(* XML at the beginning the output *)
let print_xml_header () =
  Format.fprintf !log_ppf "<?xml version=\"1.0\"?>@."


(* Pretty-print level as class attribute of log tag *)
let pp_print_level_xml_cls ppf l = 
  Format.fprintf ppf "%s" (xml_cls_of_level l)

(* Kind module as source attribute of log tag *)
let xml_src_of_kind_module = short_name_of_kind_module

(* Pretty-print kind module as source attribute of log tag *)
let pp_print_kind_module_xml_src ppf m = 
  Format.fprintf ppf "%s" (xml_src_of_kind_module m)


(* XML at the end of the output *)
let print_xml_trailer () = 
  Format.fprintf !log_ppf "@.@.</Results>@."


(* Output message as XML *)
let printf_xml mdl level fmt = 

  (ignore_or_fprintf level)
    !log_ppf 
    ("@[<hv 2><Log class=\"%a\" source=\"%a\">@,@[<hov>" ^^ 
     fmt ^^ 
     "@]@;<0 -2></Log>@]@.") 
    pp_print_level_xml_cls level
    pp_print_kind_module_xml_src mdl


let parse_log_xml level pos msg =
  let pp_print_fname ppf fname =
    if fname = "" then () else
    Format.fprintf ppf " file=\"%s\"" fname
  in
  let file, lnum, cnum = file_row_col_of_pos pos in
  (ignore_or_fprintf level)
    !log_ppf
    "@[<hv 2><Log class=\"%a\" source=\"parse\" line=\"%d\" column=\"%d\"%a>\
    @,@[<hov>%s@]@;<0 -2></Log>@]@."
    pp_print_level_xml_cls level lnum cnum pp_print_fname file msg


(* ********************************************************************** *)
(* JSON output                                                            *)
(* ********************************************************************** *)

let escape_json_string s =
  let backslash = Str.regexp "\\" in
  let double_quotes = Str.regexp "\"" in
  let newline = Str.regexp "\n" in
  s |> Str.global_replace backslash "\\\\"
    |> Str.global_replace double_quotes "\\\""
    |> Str.global_replace newline "\\n"

(* Output message as JSON *)
let printf_json mdl level fmt =

  (ignore_or_fprintf level)
    !log_ppf
    (",@.{@[<v 1>@," ^^
      "\"objectType\" : \"log\",@," ^^
      "\"level\" : \"%s\",@," ^^
      "\"source\" : \"%s\",@," ^^
      "\"value\" : \"" ^^ fmt ^^ "\"" ^^
      "@]@.}@.")
    (string_of_log_level level)
    (short_name_of_kind_module mdl)

let parse_log_json level pos msg =
  let pp_print_fname ppf fname =
    if fname = "" then () else
    Format.fprintf ppf "\"file\" : \"%s\",@," fname
  in
  let file, lnum, cnum = file_row_col_of_pos pos in
  (ignore_or_fprintf level)
    !log_ppf
    ",@.{@[<v 1>@,\
     \"objectType\" : \"log\",@,\
     \"level\" : \"%s\",@,\
     \"source\" : \"parse\",@,\
     %a\
     \"line\" : %d,@,\
     \"column\" : %d,@,\
     \"value\" : \"%s\"\
     @]@.}@.\
    "
    (string_of_log_level level)
    pp_print_fname file
    lnum cnum msg


(*****************************************************************)
(* Setup                                                         *)
(*****************************************************************)
  
(* Set log format to plain text *)
let set_log_format_pt () = log_format := F_pt

(* Set log format to XML *)
let set_log_format_xml () = 
  log_format := F_xml;
  (* Print XML header *)
  print_xml_header ()

(* Set log format to JSON *)
let set_log_format_json () = log_format := F_json

(* Relay log messages to invariant manager *)
let set_relay_log () =
  prev_log_format := !log_format;
  log_format := F_relay


let unset_relay_log () = log_format := !prev_log_format


module type SLog = sig
  val log : 'a log_printer
  val log_uncond : ('a, Format.formatter, unit) format -> 'a
end

module Make (R : sig val printf_relay : 'a m_log_printer end) : SLog = struct

  (* ********************************************************************** *)
  (* Generic logging functions                                              *)
  (* ********************************************************************** *)

  (* Log a message with source and log level *)
  let log level fmt =

    let mdl = get_module () in

    match !log_format with 
    | F_pt -> printf_pt mdl level fmt
    | F_xml -> printf_xml mdl level fmt
    | F_json -> printf_json mdl level fmt
    | F_relay -> R.printf_relay mdl level fmt


  (* Unconditionally logs a message. *)
  let log_uncond fmt =

    let mdl = get_module () in

    match !log_format with 
    | F_pt -> printf_pt_uncond mdl fmt
    | F_xml -> printf_xml mdl L_info fmt
    | F_json -> printf_json mdl L_info fmt
    | F_relay -> R.printf_relay mdl L_info fmt
                   
end


include Make (struct let printf_relay _ _ _ = failwith "Uninitialized" end)


(* 
   Local Variables:
   compile-command: "make -C .. -k"
   tuareg-interactive-program: "./kind2.top -I ./_build -I ./_build/SExpr"
   indent-tabs-mode: nil
   End: 
*)
