(**************************************************************************)
(*                                                                        *)
(*                               DeepSec                                  *)
(*                                                                        *)
(*               Vincent Cheval, project PESTO, INRIA Nancy               *)
(*                Steve Kremer, project PESTO, INRIA Nancy                *)
(*            Itsaka Rakotonirina, project PESTO, INRIA Nancy             *)
(*                                                                        *)
(*   Copyright (C) INRIA 2017-2020                                        *)
(*                                                                        *)
(*   All rights reserved.  This file is distributed under the terms of    *)
(*   the GNU General Public License version 3.0 as described in the       *)
(*   file LICENSE                                                         *)
(*                                                                        *)
(**************************************************************************)

exception Internal_error of string

let running_api = ref false

let debug_activated = false
let record_time = false

let log_file =
  if debug_activated || record_time
  then
    begin
      let exe_path = Filename.dirname (String.escaped Sys.executable_name) in
      let log_dir = Filename.concat exe_path "log" in
      if not (Sys.file_exists log_dir)
      then Unix.mkdir log_dir 0o770;
      let pid = Unix.getpid () in
      let local_time = Unix.localtime (Unix.time()) in
      let path =
        Unix.(Printf.sprintf "log/log_%d_%d_%d_%dh%dm%ds_%d.txt"
        local_time.tm_year local_time.tm_mon local_time.tm_mday
        local_time.tm_hour local_time.tm_min local_time.tm_sec
        pid)
      in
      let file = Filename.concat exe_path path in
      open_out file
    end
  else stdout

let internal_error msg =
  if debug_activated
  then
    begin
      Printf.fprintf log_file "Internal error : %s\nPlease report the bug to vincent.cheval@inria.fr with the input file and output, or post an issue at https://github.com/DeepSec-prover/deepsec/issues\n" msg;
      flush log_file
    end;
  raise (Internal_error msg)

let debug =
  if debug_activated
  then fun f -> f ()
  else fun _ -> ()

type log_level =
  | Always
  | Record_time
  | Core
  | Constraint_solving
  | Constraint_systems
  | Process
  | Distribution
  | Debug

let log_level_to_print = ref [Always;Distribution;Debug]

let log_in_debug log_level s =
  if List.mem log_level !log_level_to_print
  then
    begin
      let local_time = Unix.localtime(Unix.time ()) in
      let time =
        Unix.(Printf.sprintf "%dh%dm%ds"
          local_time.tm_hour local_time.tm_min local_time.tm_sec
          )
      in
      Printf.fprintf log_file "%s %s\n" time s;
      flush log_file
    end

let log =
  if debug_activated || record_time
  then (fun log_level f -> log_in_debug log_level (f ()))
  else fun _ _ -> ()

(**** Version ****)

let version = "VERSION"
let git_commit = "GITCOMMIT"
let git_branch = "GITBRANCH"
let os_type = "OSTYPE"

(**** Paths ****)

let path_deepsec = ref ""
let path_database = ref ""

let setup_path_result_files () = match Sys.os_type with
  | "Unix" ->
      if os_type = "Darwin"
      then
        begin
          let home = Unix.getenv "HOME" in
          let app_support = Filename.concat home "Library/Application Support/DeepSec" in
          if not (Sys.file_exists app_support)
          then Unix.mkdir app_support 0o770;

          path_database := Filename.concat app_support "result_files";

          if not (Sys.file_exists !path_database)
          then Unix.mkdir !path_database 0o770
        end
      else
        begin
          let home = Unix.getenv "HOME" in
          let app_support = Filename.concat home ".deepsec" in
          if not (Sys.file_exists app_support)
          then Unix.mkdir app_support 0o770;

          path_database := Filename.concat app_support "result_files";

          if not (Sys.file_exists !path_database)
          then Unix.mkdir !path_database 0o770
        end
  | "Cygwin" ->
      let main_path = Filename.concat (Filename.concat "%USERPROFILE%" "AppData") "deepsec" in
      if not (Sys.file_exists main_path)
      then Unix.mkdir main_path 0o770;
      path_database := Filename.concat main_path "result_files";
      if not (Sys.file_exists !path_database)
      then Unix.mkdir !path_database 0o770
  | _ -> internal_error "Operating system not supported."

(**** Trace display ****)

let display_trace = ref false
let quiet = ref false

(**** Distribution ****)

let physical_core = PHYSICALCORE

let distributed = ref None
let local_workers = ref None
let distant_workers = ref ([]:(string*string*int option) list)
let number_of_jobs = ref None
let round_timer = ref 120
let core_factor = ref 100

(**** Semantics ****)

let default_semantics = ref Types.Private
let local_semantics = ref None
let por = ref true
