(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.              
     \ /   This software is distributed as is, NO WARRANTY.              
      V_______________________________________________________________ *)

module KF = Filename

module C = Cps

type uri_generator = string -> string

type kernel = V4 | V3 | V0

IFDEF MANAGER THEN

type manager = Quiet
             | Coq
             | Matita
             | LP1    (* elpi helena *)
             | LP2    (* elpi helena *)
             | TJ2    (* teyjus helena *)
             | TJ3    (* teyjus helena *)
             | CC0    (* elpi cic *)
             | LYP    (* elpi lyp *)

END

(* interface functions ******************************************************)

let version_string b =
   if b then "Helena 0.8.3 M (December 2017)"
   else "Helena 0.8.3 M - December 2017"

let kernel = ref V3          (* kernel type *)

let si = ref false           (* use sort inclusion *)

let cover = ref ""           (* initial uri segment *)

let cc = ref false           (* activate conversion constraints *)

let indexes = ref false      (* show de Bruijn indexes *)

let alpha = ref ""           (* prefix of numeric identifiers *)

let first = ref 0            (* begin trace here *)

let last = ref max_int       (* end trace here *) 

let restricted = ref true    (* restricted applications *) 

let infinity = ref false     (* use ∞-abstractions in contexts *) 

let short = ref false        (* short global constants *) 

let cast = ref false         (* anticipate cast *)

let root = ref ""            (* initial segment of URI hierarchy *)

let trace = ref 0            (* trace level *)

IFDEF LEXER THEN
let debug_lexer = ref false  (* output lexer debug information *)
END

IFDEF PARSER THEN
let debug_parser = ref false (* output parser debug information *)
END

IFDEF TRACE THEN
let ct = ref 0               (* current trace level *)
END

IFDEF SUMMARY THEN
let summary = ref false      (* log summary information *)
END

IFDEF EXPAND THEN
let expand = ref false       (* always expand global definitions *)
END

IFDEF MANAGER THEN
let manager_dir = ref ""     (* output directory for manager *)
let manager = ref Quiet      (* manager *)
let preamble = ref ""        (* preamble file for manager *)
END

IFDEF STAGE THEN
let stage = ref 3            (* stage *)
END

IFDEF OBJECTS THEN
let export = ref false       (* export entities to XML *)
let xdir = ref ""            (* directory for XML output *)
END

IFDEF PREPROCESS THEN
let preprocess = ref false   (* preprocess source *)
END

IFDEF QUOTE THEN
let quote = ref false        (* quote identifiers when lexing *)
END

IFDEF TYPE THEN
let validate = ref true      (* validate vs. typecheck *)
let icm = ref 0              (* complexity measure of relocated terms *)
END

let kernel_id () = 
   let id = match !kernel with
      | V4 -> "Environment"
      | V3 -> "Environment_V3"
      | V0 -> "Environment_V0"
   in
   let si = if !si then "_si" else "" in
   let rest = if !restricted then "" else "_x" in
   id ^ si ^ rest

let get_baseuri () =
   String.concat "/" ["ld:"; kernel_id (); !cover; "" ]

let get_mk_uri () =
   let bu = get_baseuri () in
   fun s -> KF.concat bu (s ^ ".ld")

IFDEF TRACE THEN
let set_current_trace n =
   ct := if !first <= n && n <= !last then !trace else 0
END

let clear () =
   root := ""; first := 0; last := max_int;
   kernel := V3; si := false; restricted := true; infinity := false; cast := false; cover := ""; 
   indexes := false; short := false; trace := 0;
   IFDEF LEXER THEN debug_lexer := false ELSE () END;
   IFDEF PARSER THEN debug_parser := false ELSE () END;
   IFDEF SUMMARY THEN summary := false ELSE () END;
   IFDEF EXPAND THEN expand := false ELSE () END;
   IFDEF MANAGER THEN manager_dir := ""; manager := Quiet; preamble := "" ELSE () END;
   IFDEF STAGE THEN stage := 3 ELSE () END;
   IFDEF OBJECTS THEN export := false; xdir := "" ELSE () END; 
   IFDEF PREPROCESS THEN preprocess := false ELSE () END;
   IFDEF QUOTE THEN quote := false ELSE () END;
   IFDEF TYPE THEN validate := true; icm := 0 ELSE () END