open Support

let dprintf, _, _ = Debug.(makeFunctions' (toFlags [ 11 ]))

open Debug.Fmt

type t =
  { modules : string list
  ; hint_name : string
  ; hint_cnt : int option
  ; location : Location.t
  }

(* For reporting whether a name is used in a context. *)
type max_usage =
  [ `used of int option
  | `unused
  ]

let[@inline] location { location; _ } = location

(** Computes a string representation of a name, without modules. *)
let string_of_name n =
  let suf =
    match n.hint_cnt with
    | Option.None -> ""
    | Option.Some cnt -> string_of_int cnt
  in
  n.hint_name ^ suf

let pp ppf n =
  Format.fprintf ppf "%a%s"
    (Format.pp_print_list
       ~pp_sep:(fun _ _ -> ())
       (fun ppf x -> Format.fprintf ppf "%s." x))
    n.modules (string_of_name n)

(** Computes a string representation of a name, with all modules. *)
let show n =
  match n.modules with
  | [] -> string_of_name n
  | l -> String.concat "." l ^ "." ^ string_of_name n

let pp_list = List.pp ~pp_sep:Format.pp_print_space pp

(** Extract the base name of a variable. *)
let base_name x = x.hint_name

let modify_number f name = { name with hint_cnt = f name.hint_cnt }

let get_modules n = n.modules

let split_name s =
  try
    let pos =
      Str.search_backward (Str.regexp "[^0-9]") s (String.length s) + 1
    in
    (Str.string_before s pos, Some (int_of_string (Str.string_after s pos)))
  with
  | Failure _ -> (s, None)
  | Not_found -> raise (Failure "Cannot split an empty name")

let sanitize_name n =
  let s, cnt = split_name n.hint_name in
  { n with
    hint_name = s
  ; hint_cnt =
      (match n.hint_cnt with
      | Option.None -> cnt
      | Option.Some old_cnt -> (
          match cnt with
          | Option.None -> n.hint_cnt
          | Option.Some name_cnt ->
              Option.some
                (Int.of_string
                   (Int.to_string name_cnt ^ Int.to_string old_cnt))))
  }

let inc_hint_cnt : int option -> int option = function
  | Option.None -> Option.some 1
  | Option.Some k -> Option.some (k + 1)

let gen_fresh_name ns n =
  (* FIXME: Workaround fresh names generated by the indexing phase ending up
     in pretty-printer results. *)
  let n =
    if String.starts_with ~prefix:"\"" n.hint_name then
      { n with hint_name = "x" }
    else n
  in
  let rec next_unused y xs =
    if List.mem y xs then next_unused (inc_hint_cnt y) xs else y
  in
  let cnts =
    List.filter_map
      (fun n' ->
        let open Option in
        String.equal n'.hint_name n.hint_name
        |> Option.of_bool $> Fun.const n'.hint_cnt)
      ns
  in
  { n with hint_cnt = next_unused n.hint_cnt cnts }

let max_usage ctx s =
  let same_head s name = String.equal name.hint_name s in
  let max' k name = max k name.hint_cnt in
  match List1.of_list (List.filter (same_head s) ctx) with
  | None ->
      dprintf (fun p ->
          p.fmt "[max_usage] @[<v 2>%s is unused in@,@[%a@]@]" s pp_list ctx);
      `unused
  | Some names ->
      let k = List1.fold_left (fun x -> x.hint_cnt) max' names in
      dprintf (fun p ->
          p.fmt "[max_usage] @[<v 2>%s is USED, k = %a in@,@[%a@]@]" s
            (Option.pp Format.pp_print_int)
            k pp_list ctx);
      `used k

let[@inline] mk_name_helper ?(location = Location.ghost) ?(modules = [])
    (nm : string) : t =
  let hint_name, hint_cnt = split_name nm in
  { modules; hint_name; hint_cnt; location }

(* In cases where no pre-defined name can be used for a declaration, the
   following functions are helpers to create new unique names. This prevents
   the problem that when an {!Store.Typ.entry} or {!Store.Term.entry} is
   looked up, we never have to compare values of type {!string option}. This
   prevents the case where two entries appear to refer to the same name
   because [Option.none = Option.none]. For instance, when fresh
   meta-variables are generated during abstraction, we could not use the name
   [Option.none] for the meta-variable because it would be confused with
   other fresh meta-variables given the name [Option.none]. *)

(* FIXME: These generated variable names are not guaranteed to be fresh since
   they are not generated with respect to the referencing environment (i.e.,
   the constants and variables in scope, as well as the free variables
   occurring in the same abstraction scope). *)

let mk_bvar_name vGen_opt =
  match vGen_opt with
  | Option.None -> mk_name_helper (Gensym.VarData.gensym ())
  | Option.Some vGen -> mk_name_helper (vGen ())

let mk_mvar_name vGen_opt =
  match vGen_opt with
  | Option.None -> mk_name_helper (Gensym.MVarData.gensym ())
  | Option.Some vGen -> mk_name_helper (vGen ())

let mk_svar_name vGen_opt =
  match vGen_opt with
  | Option.None -> mk_name_helper ("$" ^ Gensym.MVarData.gensym ())
  | Option.Some vGen -> mk_name_helper ("$" ^ vGen ())

let mk_pvar_name vGen_opt =
  match vGen_opt with
  | Option.None -> mk_name_helper ("#" ^ Gensym.VarData.gensym ())
  | Option.Some vGen -> mk_name_helper ("#" ^ vGen ())

let mk_no_name () = mk_name_helper (Gensym.VarData.gensym ())

let mk_some_name x = sanitize_name x

let mk_some_string x = mk_name_helper x

let make_from_identifier identifier =
  let identifier_as_string = Identifier.show identifier in
  let hint_name, hint_cnt = split_name identifier_as_string in
  let location = Identifier.location identifier in
  let modules = [] in
  { modules; hint_name; hint_cnt; location }

let make_from_qualified_identifier qualified_identifier =
  let name = Qualified_identifier.name qualified_identifier in
  let name_as_string = Identifier.show name in
  let hint_name, hint_cnt = split_name name_as_string in
  let modules =
    List.map Identifier.show
      (Qualified_identifier.namespaces qualified_identifier)
  in
  let location = Qualified_identifier.location qualified_identifier in
  { modules; hint_name; hint_cnt; location }

let to_identifier name =
  assert (List.null name.modules);
  Identifier.make ~location:(location name) (show name)

let mk_blank = function
  | Option.Some location ->
      { modules = []; hint_name = "_"; hint_cnt = Option.none; location }
  | Option.None ->
      { modules = []
      ; hint_name = "_"
      ; hint_cnt = Option.none
      ; location = Location.ghost
      }

include (
  (val Eq.contramap (module String) string_of_name) : Eq.EQ with type t := t)

let hash = Fun.(show >> Hashtbl.hash)
