(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp
open CErrors
open Util
open Names
open Constr
open Vars
open Environ

module NamedDecl = Context.Named.Declaration

type econstr = constr
type etypes = types
type esorts = Sorts.t
type erelevance = Sorts.relevance
type einstance = UVars.Instance.t
type 'a puniverses = 'a * einstance

(** Generic filters *)
module Filter :
sig
  type t
  val equal : t -> t -> bool
  val identity : t
  val filter_list : t -> 'a list -> 'a list
  val filter_array : t -> 'a array -> 'a array
  val filter_slist : t -> 'a SList.t -> 'a SList.t
  val extend : int -> t -> t
  val compose : t -> t -> t
  val apply_subfilter : t -> bool list -> t
  val restrict_upon : t -> int -> (int -> bool) -> t option
  val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t
  val make : bool list -> t
  val repr :  t -> bool list option

  type compact =
  | Empty
  | TCons of int * compact
  | FCons of int * compact

  val unfold : t -> compact option

end =
struct

  type compact =
  | Empty
  | TCons of int * compact
  | FCons of int * compact

  let rec compact l = match l with
  | [] -> Empty
  | true :: l ->
    begin match compact l with
    | TCons (n, c) -> TCons (n + 1, c)
    | (Empty | FCons _ as c) -> TCons (1, c)
    end
  | false :: l ->
    begin match compact l with
    | FCons (n, c) -> FCons (n + 1, c)
    | (Empty | TCons _ as c) -> FCons (1, c)
    end

  type t = {
    data : bool list option;
    compact : compact;
  }
  (** We guarantee through the interface that if a filter is [Some _] then it
      contains at least one [false] somewhere. *)

  let identity = { data = None; compact = Empty }

  let rec equal l1 l2 = match l1, l2 with
  | [], [] -> true
  | h1 :: l1, h2 :: l2 ->
    (if h1 then h2 else not h2) && equal l1 l2
  | _ -> false

  let equal l1 l2 = match l1.data, l2.data with
  | None, None -> true
  | Some _, None | None, Some _ -> false
  | Some l1, Some l2 -> equal l1 l2

  let rec is_identity = function
  | [] -> true
  | true :: l -> is_identity l
  | false :: _ -> false

  let normalize f =
    if is_identity f then identity
    else { data = Some f; compact = compact f }

  let filter_list f l = match f.data with
  | None -> l
  | Some f -> CList.filter_with f l

  let filter_array f v = match f.data with
  | None -> v
  | Some f -> CArray.filter_with f v

  let filter_slist f l = match f.data with
  | None -> l
  | Some f ->
    let rec filter f l = match f, SList.view l with
    | [], None -> SList.empty
    | true :: f, Some (o, l) -> SList.cons_opt o (filter f l)
    | false :: f, Some (_, l) -> filter f l
    | _ :: _, None | [], Some _ -> invalid_arg "List.filter_with"
    in
    filter f l

  let rec extend n l =
    if n = 0 then l
    else extend (pred n) (true :: l)

  let extend n f =  match f.data with
  | None -> identity
  | Some f0 ->
    let compact = match f.compact with
    | Empty -> assert false
    | TCons (m, c) -> TCons (n + m, c)
    | c -> TCons (n, c)
    in
    { data = Some (extend n f0); compact }

  let compose f1 f2 = match f1.data with
  | None -> f2
  | Some f1 ->
    match f2.data with
    | None -> identity
    | Some f2 -> normalize (CList.filter_with f1 f2)

  let apply_subfilter_array filter subfilter =
    (* In both cases we statically know that the argument will contain at
       least one [false] *)
    match filter.data with
    | None ->
      let l = Array.to_list subfilter in
      { data = Some l; compact = compact l }
    | Some f ->
    let len = Array.length subfilter in
    let fold b (i, ans) =
      if b then
        let () = assert (0 <= i) in
        (pred i, Array.unsafe_get subfilter i :: ans)
      else
        (i, false :: ans)
    in
    let data = snd (List.fold_right fold f (pred len, [])) in
    { data = Some data; compact = compact data }

  let apply_subfilter filter subfilter =
    apply_subfilter_array filter (Array.of_list subfilter)

  let restrict_upon f len p =
    let newfilter = Array.init len p in
    if Array.for_all (fun id -> id) newfilter then None
    else
      Some (apply_subfilter_array f newfilter)

  let map_along f flt l =
    let ans = match flt.data with
    | None -> List.map (fun x -> f true x) l
    | Some flt -> List.map2 f flt l
    in
    normalize ans

  let make l = normalize l

  let repr f = f.data

  let unfold f = match f.data with
  | None -> None
  | Some _ -> Some f.compact

end

module Abstraction = struct

  type abstraction =
    | Abstract
    | Imitate

  type t = abstraction list

  let identity = []

  let abstract_last l = Abstract :: l
end

(* The kinds of existential variables are now defined in [Evar_kinds] *)

(* The type of mappings for existential variables *)

module Store = Store.Make ()

let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)

type defined = [ `defined ]
type undefined = [ `undefined ]

type _ evar_body =
  | Evar_empty : undefined evar_body
  | Evar_defined : econstr -> defined evar_body

type (_, 'a) when_undefined =
| Defined : (defined, 'a) when_undefined
| Undefined : 'a -> (undefined, 'a) when_undefined

type 'a evar_info = {
  evar_concl : ('a, constr) when_undefined;
  evar_hyps : named_context_val;
  evar_body : 'a evar_body;
  evar_filter : Filter.t;
  evar_abstract_arguments : ('a, Abstraction.t) when_undefined;
  evar_source : Evar_kinds.t Loc.located;
  evar_candidates : ('a, constr list option) when_undefined; (* if not None, list of allowed instances *)
  evar_relevance: Sorts.relevance;
}

type any_evar_info = EvarInfo : 'a evar_info -> any_evar_info

let instance_mismatch () =
  anomaly (Pp.str "Signature and its instance do not match.")

let evar_concl evi = match evi.evar_concl with
| Undefined c -> c

let evar_filter evi = evi.evar_filter

let evar_body evi = evi.evar_body

let evar_context evi = named_context_of_val evi.evar_hyps

let evar_filtered_context evi =
  Filter.filter_list (evar_filter evi) (evar_context evi)

let evar_candidates evi = match evi.evar_candidates with
| Undefined c -> c

let evar_abstract_arguments evi = match evi.evar_abstract_arguments with
| Undefined c -> c

let evar_relevance evi = evi.evar_relevance

let evar_hyps evi = evi.evar_hyps

let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with
| None -> evar_hyps evi
| Some filter ->
  let rec make_hyps filter ctxt = match filter, match_named_context_val ctxt with
  | [], None -> empty_named_context_val
  | false :: filter, Some (_, _,  ctxt) -> make_hyps filter ctxt
  | true :: filter, Some (status, decl, ctxt) ->
    let hyps = make_hyps filter ctxt in
    push_named_context_val status decl hyps
  | _ -> instance_mismatch ()
  in
  make_hyps filter (evar_hyps evi)

let evar_env env evi =
  Environ.reset_with_named_context evi.evar_hyps env

let evar_filtered_env env evi = Environ.reset_with_named_context (evar_filtered_hyps evi) env

let evar_identity_subst evi =
  let len = match Filter.repr evi.evar_filter with
  | None -> List.length @@ Environ.named_context_of_val evi.evar_hyps
  | Some f -> List.count (fun b -> b) f
  in
  SList.defaultn len SList.empty

let map_evar_body (type a) f : a evar_body -> a evar_body = function
  | Evar_empty -> Evar_empty
  | Evar_defined d -> Evar_defined (f d)

let map_when_undefined (type a b) f : (a, b) when_undefined -> (a, b) when_undefined = function
| Defined -> Defined
| Undefined x -> Undefined (f x)

let map_evar_info f evi =
  {evi with
    evar_body = map_evar_body f evi.evar_body;
    evar_hyps = map_named_val (fun status d -> status, NamedDecl.map_constr f d) evi.evar_hyps;
    evar_concl = map_when_undefined f evi.evar_concl;
    evar_candidates = map_when_undefined (fun c -> Option.map (List.map f) c) evi.evar_candidates }

(* This exception is raised by *.existential_value *)
exception NotInstantiatedEvar

(* Note: let-in contributes to the instance *)
let evar_instance_array empty push info args =
  let rec instrec pos filter args = match filter with
  | Filter.Empty -> if SList.is_empty args then empty else instance_mismatch ()
  | Filter.TCons (n, filter) -> instpush pos n filter args
  | Filter.FCons (n, filter) -> instrec (pos + n) filter args
  and instpush pos n filter args =
    if n <= 0 then instrec pos filter args
    else match args with
    | SList.Nil -> assert false
    | SList.Cons (c, args) ->
      let d = Environ.lookup_named_ctxt_pos pos info.evar_hyps in
      let id = NamedDecl.get_id d in
      push id c (instpush (pos + 1) (n - 1) filter args)
    | SList.Default (m, args) ->
      if m <= n then instpush (pos + m) (n - m) filter args
      else instrec (pos + n) filter (SList.defaultn (m - n) args)
  in
  match Filter.unfold (evar_filter info) with
  | None ->
    let rec instance pos args = match args with
    | SList.Nil -> empty
    | SList.Cons (c, args) ->
      let d = Environ.lookup_named_ctxt_pos pos info.evar_hyps in
      let id = NamedDecl.get_id d in
      push id c (instance (pos + 1) args)
    | SList.Default (n, args) -> instance (pos + n) args
    in
    instance 0 args
  | Some filter ->
    instrec 0 filter args

let make_evar_instance_array info args =
  if SList.is_default args then []
  else
    let push id c l = if isVarId id c then l else (id, c) :: l in
    evar_instance_array [] push info args

type 'a in_ustate = 'a * UState.t

(*************************)
(* Unification state *)

type conv_pb = Conversion.conv_pb
type evar_constraint = conv_pb * Environ.env * constr * constr

(** Exporting from Evarnames. *)
let generate_goal_names = Evarnames.generate_goal_names

module EvMap = Evar.Map

type evar_flags =
  { obligation_evars : Evar.Set.t;
    aliased_evars : Evar.t Evar.Map.t;
    typeclass_evars : Evar.Set.t;
    impossible_case_evars : Evar.Set.t;
    rewrite_rule_evars : Evar.Set.t;
  }

type side_effect_role =
| Schema of inductive * string

type side_effects = {
  seff_safeenv : Safe_typing.safe_environment option;
  (* If seff_safeenv = Some senv, then senv = Global.safe_env + seff_private *)
  seff_labels : Id.Set.t;
  seff_private : Safe_typing.private_constants;
  seff_roles : side_effect_role Cmap.t;
  seff_univs : UState.named_universes_entry Cmap.t;
}

module FutureGoals : sig

  type t

  val comb : t -> Evar.t list

  val map_filter : (Evar.t -> Evar.t option) -> t -> t
  (** Applies a function on the future goals *)

  val filter : (Evar.t -> bool) -> t -> t
  (** Applies a filter on the future goals *)

  type stack

  val empty_stack : stack

  val push : stack -> stack
  val pop : stack -> t * stack

  val add : Evar.t -> stack -> stack
  val remove : Evar.t -> stack -> stack
  val mem : Evar.t -> stack -> bool

  val fold : ('a -> Evar.t -> 'a) -> 'a -> stack -> 'a

  val pr_stack : stack -> Pp.t

end = struct

  type t = {
    uid : int;
    comb : Evar.t Int.Map.t;
    revmap : int Evar.Map.t;
  }

  let comb g =
    (* Keys are reversed, highest number is last introduced *)
    Int.Map.fold (fun _ evk accu -> evk :: accu) g.comb []

  type stack = t list

  let set f = function
  | [] -> anomaly Pp.(str"future_goals stack should not be empty")
  | hd :: tl ->
    f hd :: tl

  let add evk stack =
    let add fgl =
      let comb = Int.Map.add fgl.uid evk fgl.comb in
      let revmap = Evar.Map.add evk fgl.uid fgl.revmap in
      let uid = fgl.uid + 1 in
      let () = assert (0 <= uid) in
      { comb; revmap; uid }
    in
    set add stack

  let remove e stack =
    let remove fgl =
      let comb, revmap = match Evar.Map.find e fgl.revmap with
      | index -> (Int.Map.remove index fgl.comb, Evar.Map.remove e fgl.revmap)
      | exception Not_found -> fgl.comb, fgl.revmap
      in
      { comb; revmap; uid = fgl.uid }
    in
    List.map remove stack

  let mem e stack = List.exists (fun fgl -> Evar.Map.mem e fgl.revmap) stack

  let empty = {
    uid = 0;
    comb = Int.Map.empty;
    revmap = Evar.Map.empty;
  }

  let empty_stack = [empty]

  let push stack = empty :: stack

  let pop stack =
    match stack with
    | [] -> anomaly Pp.(str"future_goals stack should not be empty")
    | hd :: tl ->
      hd, tl

  let fold f acc stack =
    let future_goals = List.hd stack in
    List.fold_left f acc (comb future_goals)

  let filter f fgl =
    let fold index evk (comb, revmap) =
      if f evk then (comb, revmap)
      else (Int.Map.remove index comb, Evar.Map.remove evk revmap)
    in
    let (comb, revmap) = Int.Map.fold fold fgl.comb (fgl.comb, fgl.revmap) in
    { comb; revmap; uid = fgl.uid }

  let map_filter f fgl =
    let fold index evk (comb, revmap) = match f evk with
    | None -> (comb, revmap)
    | Some evk' ->
      (Int.Map.add index evk' comb, Evar.Map.add evk' index revmap)
    in
    let (comb, revmap) = Int.Map.fold fold fgl.comb (Int.Map.empty, Evar.Map.empty) in
    { comb; revmap; uid = fgl.uid }

  let pr_stack stack =
    let open Pp in
    let pr_future_goals fgl =
      let comb = comb fgl in
      prlist_with_sep spc Evar.print comb
    in
    if List.is_empty stack then str"(empty stack)"
    else prlist_with_sep (fun () -> str"||") pr_future_goals stack

end

type evar_map = {
  (* Existential variables *)
  defn_evars : defined evar_info EvMap.t;
  undf_evars : undefined evar_info EvMap.t;
  evar_names : Evarnames.t;
  candidate_evars : Evar.Set.t; (* The subset of undefined evars with a non-empty candidate list. *)
  (** Universes *)
  universes  : UState.t;
  (** Conversion problems *)
  conv_pbs   : evar_constraint list;
  last_mods  : Evar.Set.t;
  evar_flags : evar_flags;
  (** Interactive proofs *)
  effects    : side_effects;
  future_goals : FutureGoals.stack; (** list of newly created evars, to be
                                        eventually turned into goals if not solved.*)
  given_up : Evar.Set.t;
  shelf : Evar.t list list;
  extras : Store.t;
}

let find d e =
  try EvarInfo (EvMap.find e d.undf_evars)
  with Not_found -> EvarInfo (EvMap.find e d.defn_evars)

let rec thin_val = function
  | [] -> []
  | (id, c) :: tl ->
    match Constr.kind c with
    | Constr.Var v ->
      if Id.equal id v then thin_val tl
      else (id, make_substituend c) :: (thin_val tl)
    | _ -> (id, make_substituend c) :: (thin_val tl)

let rec find_var id = function
| [] -> raise_notrace Not_found
| (idc, c) :: subst ->
  if Id.equal id idc then c
  else find_var id subst

let replace_vars sigma var_alist x =
  let var_alist = thin_val var_alist in
  match var_alist with
  | [] -> x
  | _ ->
    let rec substrec n c = match Constr.kind c with
    | Constr.Var id ->
      begin match find_var id var_alist with
      | var -> (lift_substituend n var)
      | exception Not_found -> c
      end
    | Constr.Evar (evk, args) ->
      let EvarInfo evi = find sigma evk in
      let args' = substrec_instance n (evar_filtered_context evi) args in
      if args' == args then c
      else Constr.mkEvar (evk, args')
    | _ -> Constr.map_with_binders succ substrec n c

    and substrec_instance n ctx args = match ctx, SList.view args with
    | [], None -> SList.empty
    | decl :: ctx, Some (c, args) ->
      let c' = match c with
      | None ->
        begin match find_var (NamedDecl.get_id decl) var_alist with
        | var -> Some (lift_substituend n var)
        | exception Not_found -> None
        end
      | Some c ->
        let c' = substrec n c in
        if isVarId (NamedDecl.get_id decl) c' then None
        else Some c'
      in
      SList.cons_opt c' (substrec_instance n ctx args)
    | _ :: _, None | [], Some _ -> instance_mismatch ()
    in
    substrec 0 x

let instantiate_evar_array sigma info c args =
  let inst = make_evar_instance_array info args in
  match inst with
  | [] -> c
  | _ -> replace_vars sigma inst c

let expand_existential sigma (evk, args) =
  let EvarInfo evi = find sigma evk in
  let rec expand ctx args = match ctx, SList.view args with
  | [], None -> []
  | _ :: ctx, Some (Some c, args) -> c :: expand ctx args
  | decl :: ctx, Some (None, args) -> mkVar (NamedDecl.get_id decl) :: expand ctx args
  | [], Some _ | _ :: _, None -> instance_mismatch ()
  in
  expand (evar_filtered_context evi) args

let expand_existential0 = expand_existential

(*** Lifting primitive from Evar.Map. ***)

let add_name evk basename ?parent evd =
  { evd with evar_names = Evarnames.add basename evk ?parent evd.evar_names }

let transfer_name evk evk' evd =
  { evd with evar_names = Evarnames.transfer_name evk evk' evd.evar_names }

let add_with_name (type a) ?name ?parent ~typeclass_candidate ~rrpat d e (i : a evar_info) = match i.evar_body with
| Evar_empty ->
  let evar_names =
    match name with
    | Some (basename, fresh) ->
       (* If fresh (i.e. coming from ?[?ident] syntax), we first check for conflicts. *)
       if fresh then
         Evarnames.add_fresh basename e ?parent d.evar_names
       else
         Evarnames.add basename e ?parent d.evar_names
    | None -> d.evar_names
  in
  let evar_flags =
    if typeclass_candidate then
      let flags = d.evar_flags in
      { flags with typeclass_evars = Evar.Set.add e flags.typeclass_evars }
    else d.evar_flags
  in
  let evar_flags =
    if rrpat then
      { evar_flags with rewrite_rule_evars = Evar.Set.add e evar_flags.rewrite_rule_evars }
    else evar_flags
  in
  let evar_flags = match i.evar_source with
    | _, ImpossibleCase ->
      { evar_flags with impossible_case_evars = Evar.Set.add e evar_flags.impossible_case_evars }
    | _ -> evar_flags
  in
  let candidate_evars = match i.evar_candidates with
  | Undefined None -> Evar.Set.remove e d.candidate_evars
  | Undefined (Some _) -> Evar.Set.add e d.candidate_evars
  in
  { d with undf_evars = EvMap.add e i d.undf_evars; evar_names; evar_flags; candidate_evars }
| Evar_defined _ ->
  let evar_names = Evarnames.remove e d.evar_names in
  { d with defn_evars = EvMap.add e i d.defn_evars; evar_names }

(** Evd.add is a low-level function mainly used to update the evar_info
    associated to an evar, so we prevent registering its typeclass status. *)
let add d e i = add_with_name ~typeclass_candidate:false ~rrpat:false d e i

(*** Evar flags: typeclasses, aliased or obligation flag *)

let get_typeclass_evars evd = evd.evar_flags.typeclass_evars

let set_typeclass_evars evd tcs =
  let flags = evd.evar_flags in
  let tcs = Evar.Set.filter (fun evk -> Evar.Map.mem evk evd.undf_evars) tcs in
  { evd with evar_flags = { flags with typeclass_evars = tcs } }

let is_typeclass_evar evd evk =
  let flags = evd.evar_flags in
  Evar.Set.mem evk flags.typeclass_evars

let get_obligation_evars evd = evd.evar_flags.obligation_evars

let set_obligation_evar evd evk =
  let flags = evd.evar_flags in
  let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in
  { evd with evar_flags }

let is_obligation_evar evd evk =
  let flags = evd.evar_flags in
  Evar.Set.mem evk flags.obligation_evars

let get_impossible_case_evars evd = evd.evar_flags.impossible_case_evars

let is_rewrite_rule_evar evd evk =
  let flags = evd.evar_flags in
  Evar.Set.mem evk flags.rewrite_rule_evars

(** Inheritance of flags: for evar-evar and restriction cases *)

let inherit_evar_flags evar_flags evk evk' =
  if Evar.Set.mem evk evar_flags.rewrite_rule_evars then
    CErrors.anomaly Pp.(str "Tried to define or restrict a rewrite rule evar.");
  let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in
  let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in
  let evk_impossible = Evar.Set.mem evk evar_flags.impossible_case_evars in
  let aliased_evars = Evar.Map.add evk evk' evar_flags.aliased_evars in
  let typeclass_evars =
    if evk_typeclass then
      let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
      Evar.Set.add evk' typeclass_evars
    else evar_flags.typeclass_evars
  in
  let obligation_evars =
    if evk_obligation then
      let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
      Evar.Set.add evk' obligation_evars
    else evar_flags.obligation_evars
  in
  let impossible_case_evars =
    if evk_impossible then
      let impossible_case_evars = Evar.Set.remove evk evar_flags.impossible_case_evars in
      Evar.Set.add evk' impossible_case_evars
    else evar_flags.impossible_case_evars
  in
  let rewrite_rule_evars = evar_flags.rewrite_rule_evars in
  { obligation_evars; aliased_evars; typeclass_evars; impossible_case_evars; rewrite_rule_evars }

(** Removal: in all other cases of definition *)

let remove_evar_flags evk evar_flags =
  if Evar.Set.mem evk evar_flags.rewrite_rule_evars then
    CErrors.anomaly Pp.(str "Tried to define or restrict a rewrite rule evar.");
  { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
    obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
    impossible_case_evars = Evar.Set.remove evk evar_flags.impossible_case_evars;
    (* Aliasing information is kept. *)
    aliased_evars = evar_flags.aliased_evars;
    (* Cannot be a rewrite rule evar *)
    rewrite_rule_evars = evar_flags.rewrite_rule_evars
  }

(** New evars *)

let evar_counter_summary_name = "evar counter"

(* Generator of existential names *)
let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name
let new_untyped_evar () =
  let open Summary.Ref in
  evar_ctr := !evar_ctr + 1; Evar.unsafe_of_int !evar_ctr

let default_source = Loc.tag @@ Evar_kinds.InternalHole

let remove d e =
  let undf_evars = EvMap.remove e d.undf_evars in
  let defn_evars = EvMap.remove e d.defn_evars in
  let future_goals = FutureGoals.remove e d.future_goals in
  let evar_flags = remove_evar_flags e d.evar_flags in
  let candidate_evars = Evar.Set.remove e d.candidate_evars in
  { d with undf_evars; defn_evars; future_goals;
           evar_flags; candidate_evars }

let find_defined d e = EvMap.find_opt e d.defn_evars

let find_undefined d e = EvMap.find e d.undf_evars

let mem d e = EvMap.mem e d.undf_evars || EvMap.mem e d.defn_evars

let undefined_map d = d.undf_evars

let defined_map d = d.defn_evars

let drop_all_defined d = { d with defn_evars = EvMap.empty }

(* spiwack: not clear what folding over an evar_map, for now we shall
    simply fold over the inner evar_map. *)
let fold f d a =
  let f evk evi accu = f evk (EvarInfo evi) accu in
  EvMap.fold f d.defn_evars (EvMap.fold f d.undf_evars a)

let fold_undefined f d a = EvMap.fold f d.undf_evars a

type map = { map : 'r. Evar.t -> 'r evar_info -> 'r evar_info }

let raw_map f d =
  let defn_evars = EvMap.Smart.mapi f.map d.defn_evars in
  let undf_evars = EvMap.Smart.mapi f.map d.undf_evars in
  { d with defn_evars; undf_evars; }

let raw_map_undefined f d =
  { d with undf_evars = EvMap.Smart.mapi f d.undf_evars; }

let is_evar = mem

let is_defined d e = EvMap.mem e d.defn_evars

let is_undefined d e = EvMap.mem e d.undf_evars

let existential_opt_value d (n, args) =
  match EvMap.find_opt n d.defn_evars with
  | None -> None
  | Some info ->
    let Evar_defined c = evar_body info in
    Some (instantiate_evar_array d info c args)

let existential_value d ev = match existential_opt_value d ev with
  | None -> raise NotInstantiatedEvar
  | Some v -> v

let existential_opt_value0 = existential_opt_value

let existential_expand_value0 sigma (evk, args) = match existential_opt_value sigma (evk, args) with
| None ->
  let args = expand_existential sigma (evk, args) in
  CClosure.EvarUndefined (evk, args)
| Some c -> CClosure.EvarDefined c

let mkLEvar sigma (evk, args) =
  let EvarInfo evi = find sigma evk in
  let fold decl arg accu =
    if isVarId (NamedDecl.get_id decl) arg then SList.default accu
    else SList.cons arg accu
  in
  let args = List.fold_right2 fold (evar_filtered_context evi) args SList.empty in
  mkEvar (evk, args)

let is_relevance_irrelevant sigma r =
  match UState.nf_relevance sigma.universes r with
  | Irrelevant -> true
  | Relevant | RelevanceVar _ -> false

let get_senv_side_effects eff = match eff.seff_safeenv with
| Some senv -> senv
| None ->
  let (_, senv) = Safe_typing.export_private_constants eff.seff_private (Global.safe_env ()) in
  senv

let evar_handler sigma =
  let evar_expand ev = existential_expand_value0 sigma ev in
  let qvar_irrelevant q = is_relevance_irrelevant sigma (Sorts.RelevanceVar q) in
  let evar_irrelevant (evk, _) = match find sigma evk with
  | EvarInfo evi -> is_relevance_irrelevant sigma evi.evar_relevance
  | exception Not_found -> false (* Should be an anomaly *)
  in
  let evar_repack ev = mkLEvar sigma ev in
  let abstr_const cst =
    (* XXX: be more efficient *)
    let open Declarations in
    let senv = get_senv_side_effects sigma.effects in
    let env = Safe_typing.env_of_safe_env senv in
    let cb = Environ.lookup_constant cst env in
    let drop_opaque = function
    | OpaqueDef _ -> OpaqueDef ()
    | Def _ | Undef _ | Primitive _ | Symbol _ as body -> body
    in
    let drop_code = function
    | Vmemitcodes.BCdefined (mask, idx, patch) ->
      let code () = Environ.lookup_vm_code idx env in
      Vmemitcodes.BCdefined (mask, code, patch)
    | BCalias _ | BCconstant | BCuncompiled as code -> code
    in
    { cb with const_body = drop_opaque cb.const_body; const_body_code = drop_code cb.const_body_code }
  in
  let qual_equal q1 q2 = UState.check_eq_quality sigma.universes q1 q2 in
  { CClosure.evar_expand; evar_irrelevant; evar_repack; qvar_irrelevant; qual_equal; abstr_const }

let existential_type_opt d (n, args) =
  match find_undefined d n with
  | exception Not_found -> None
  | info ->
    Some (instantiate_evar_array d info (evar_concl info) args)

let existential_type d n = match existential_type_opt d n with
  | Some t -> t
  | None -> anomaly (str "Evar " ++ str (string_of_existential (fst n)) ++ str " was not declared.")

let add_univ_constraints d c =
  { d with universes = UState.add_univ_constraints d.universes c }

let add_poly_constraints ?src d c =
  { d with universes = UState.add_poly_constraints ?src d.universes c }

let add_constraints d c =
  { d with universes = UState.add_constraints d.universes c }

(*** /Lifting... ***)

(* evar_map are considered empty disregarding histories *)
let is_empty d =
  EvMap.is_empty d.defn_evars &&
  EvMap.is_empty d.undf_evars &&
  List.is_empty d.conv_pbs

let cmap f evd =
  { evd with
      defn_evars = EvMap.map (map_evar_info f) evd.defn_evars;
      undf_evars = EvMap.map (map_evar_info f) evd.undf_evars
  }

(* spiwack: deprecated *)
let create_evar_defs sigma = { sigma with
  conv_pbs=[]; last_mods=Evar.Set.empty }

let empty_evar_flags =
  { obligation_evars = Evar.Set.empty;
    aliased_evars = Evar.Map.empty;
    typeclass_evars = Evar.Set.empty;
    impossible_case_evars = Evar.Set.empty;
    rewrite_rule_evars = Evar.Set.empty;
  }

let empty_side_effects = {
  seff_safeenv = None;
  seff_labels = Id.Set.empty;
  seff_private = Safe_typing.empty_private_constants;
  seff_roles = Cmap.empty;
  seff_univs = Cmap.empty;
}

let empty = {
  defn_evars = EvMap.empty;
  undf_evars = EvMap.empty;
  universes  = UState.empty;
  conv_pbs   = [];
  last_mods  = Evar.Set.empty;
  evar_flags = empty_evar_flags;
  candidate_evars = Evar.Set.empty;
  effects    = empty_side_effects;
  evar_names = Evarnames.empty; (* id<->key for undefined evars *)
  future_goals = FutureGoals.empty_stack;
  given_up = Evar.Set.empty;
  shelf = [[]];
  extras = Store.empty;
}

let from_env e = { empty with universes = UState.from_env e }

let from_ustate uctx = { empty with universes = uctx }

let from_ctx = from_ustate

let from_auctx ?of_template e names = { empty with universes = UState.from_auctx ?of_template e names }

let has_undefined evd = not (EvMap.is_empty evd.undf_evars)

let has_given_up evd = not (Evar.Set.is_empty evd.given_up)

let has_shelved evd = not (List.for_all List.is_empty evd.shelf)

let merge_ustate evd uctx' =
  { evd with universes = UState.union evd.universes uctx' }

let merge_universe_context = merge_ustate

let set_ustate evd uctx' =
  { evd with universes = uctx' }

let set_universe_context = set_ustate

(* TODO: make unique *)
let add_conv_pb ?(tail=false) pb d =
  if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
  else {d with conv_pbs = pb::d.conv_pbs}

let conv_pbs d = d.conv_pbs

let evar_source evi = evi.evar_source

let evar_ident evk evd = Evarnames.name_of evk evd.evar_names
let evar_has_name evk evd = Evarnames.has_name evk evd.evar_names
let evar_has_unambiguous_name evk evd = Evarnames.has_unambiguous_name evk evd.evar_names
let evar_key name evd = Evarnames.resolve name evd.evar_names

let get_aliased_evars evd = evd.evar_flags.aliased_evars

let max_undefined_with_candidates evd =
  try Some (Evar.Set.max_elt evd.candidate_evars) with Not_found -> None

let is_aliased_evar evd evk =
  try Some (Evar.Map.find evk evd.evar_flags.aliased_evars)
  with Not_found -> None

let downcast evk ccl evd =
  if is_rewrite_rule_evar evd evk then
    CErrors.anomaly Pp.(str "Tried to define or restrict a rewrite rule evar.");
  let evar_info = EvMap.find evk evd.undf_evars in
  let evar_info' = { evar_info with evar_concl = Undefined ccl } in
  { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars }

let mem_head_evar c evars =
  (* Note: evar-sensitive code *)
  let rec hrec c = match kind c with
    | Evar (evk,_)   -> Evar.Set.mem evk evars
    | Case (_, _, _, _, _, c, _) -> hrec c
    | App (c,_)      -> hrec c
    | Cast (c,_,_)   -> hrec c
    | Proj (_, _, c)    -> hrec c
    | _              -> false
  in
  hrec c

let has_evar evars (pbty,_,t1,t2) =
  match evars with
  | None -> true
  | Some evars -> mem_head_evar t1 evars || mem_head_evar t2 evars

(* extracts conversion problems that satisfy predicate p *)
(* Note: conv_pbs not satisying p are stored back in reverse order *)
let extract_conv_pbs evd p =
  let (pbs,pbs1) =
    List.fold_left
      (fun (pbs,pbs1) pb ->
         if p pb then
           (pb::pbs,pbs1)
         else
           (pbs,pb::pbs1))
      ([],[])
      evd.conv_pbs
  in
  {evd with conv_pbs = pbs1; last_mods = Evar.Set.empty},
  pbs

let extract_changed_conv_pbs evd =
  extract_conv_pbs evd (has_evar (Some evd.last_mods))

let extract_changed_conv_pbs_from evd evars=
  extract_conv_pbs evd (has_evar evars)

let extract_all_conv_pbs evd =
  extract_conv_pbs evd (fun _ -> true)

let loc_of_conv_pb evd (pbty,env,t1,t2) =
  match kind (fst (decompose_app t1)) with
  | Evar (evk1,_) ->
    let EvarInfo evi = find evd evk1 in
    fst (evar_source evi)
  | _ ->
  match kind (fst (decompose_app t2)) with
  | Evar (evk2,_) ->
    let EvarInfo evi = find evd evk2 in
    fst (evar_source evi)
  | _             -> None

(**********************************************************)
(* Sort variables *)

type rigid = UState.rigid =
  | UnivRigid
  | UnivFlexible of bool (** Is substitution by an algebraic ok? *)

let univ_rigid = UnivRigid
let univ_flexible = UnivFlexible false
let univ_flexible_alg = UnivFlexible true

let ustate d = d.universes

let elim_graph d = UState.elim_graph d.universes

let universe_context_set d = UState.universe_context_set d.universes

let sort_context_set d = UState.sort_context_set d.universes

let to_universe_context evd = UState.context evd.universes

let quality_printer evd = UState.quality_printer (ustate evd)
let sort_printer evd = UState.sort_printer (ustate evd)

let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes

let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl

let check_univ_decl_early ~poly ~with_obls sigma udecl terms =
  let () =
    if with_obls && not @@ PolyFlags.univ_poly poly &&
       (not udecl.UState.univdecl_extensible_instance
        || not udecl.UState.univdecl_extensible_constraints)
    then
      CErrors.user_err
        Pp.(str "Non extensible universe declaration not supported \
                 with monomorphic Program definitions.")
  in
  let vars = List.fold_left (fun acc b -> Univ.Level.Set.union acc (Vars.universes_of_constr b)) Univ.Level.Set.empty terms in
  let uctx = ustate sigma in
  let uctx = UState.collapse_sort_variables ~only_above_prop:(not @@ PolyFlags.collapse_sort_variables poly) uctx in
  let uctx = UState.restrict uctx vars in
  ignore (UState.check_univ_decl ~poly uctx udecl)

let restrict_ustate evd vars =
  { evd with universes = UState.restrict evd.universes vars }

let restrict_universe_context = restrict_ustate

let universe_subst evd =
  UState.subst evd.universes

let merge_universe_context_set ?loc ?(sideff=false) rigid evd uctx' =
  {evd with universes = UState.merge_universe_context_set ?loc ~sideff rigid evd.universes uctx'}

let merge_sort_context_set ?loc ?sort_rigid ?(sideff=false) ?src rigid evd ctx' =
  {evd with universes = UState.merge_sort_context_set ?loc ?sort_rigid ~sideff rigid ?src evd.universes ctx'}

let with_sort_context_set ?loc ?sort_rigid ?src rigid d (a, ctx) =
  (merge_sort_context_set ?loc ?sort_rigid ?src rigid d ctx, a)

let new_univ_level_variable ?loc ?name rigid evd =
  let uctx', u = UState.new_univ_level_variable ?loc rigid name evd.universes in
    ({evd with universes = uctx'}, u)

let new_univ_variable ?loc ?name rigid evd =
  let evd, u = new_univ_level_variable ?loc ?name rigid evd in
  evd, Univ.Universe.make u

let new_quality_variable ?loc ?name evd =
  let uctx, q = UState.new_quality_variable ?loc ?name evd.universes in
  {evd with universes = uctx}, q

let new_sort_info ?loc ?sort_rigid ?name rigid sigma =
  let (sigma, u) = new_univ_variable ?loc rigid sigma in
  let uctx, q = UState.new_quality_variable ?sort_rigid ?name sigma.universes in
  ({ sigma with universes = uctx }, q, u)

let new_sort_variable ?loc ?sort_rigid ?name rigid sigma =
  let sigma, q, u = new_sort_info ?loc ?sort_rigid ?name rigid sigma in
  sigma, Sorts.vsort q u

let add_forgotten_univ d u =
  { d with universes = UState.add_forgotten_univ d.universes u }

let make_nonalgebraic_variable evd u =
  { evd with universes = UState.make_nonalgebraic_variable evd.universes u }

(****************************************)
(* Operations on constants              *)
(****************************************)

(* FIXME: do this more cleanly *)
let lookup_constant env sigma c = match Environ.lookup_constant_opt c env with
| Some cb -> cb
| None ->
  if Safe_typing.is_empty_private_constants sigma.effects.seff_private then
    CErrors.anomaly Pp.(str "Constant " ++ Constant.print c ++ str" does not appear in the environment.")
  else
    let senv = get_senv_side_effects sigma.effects in
    Environ.lookup_constant c (Safe_typing.env_of_safe_env senv)

let fresh_sort_in_quality ?loc ?(rigid=univ_flexible) evd s =
  with_sort_context_set ?loc rigid ~src:UState.Internal evd
    (UnivGen.fresh_sort_in_quality s)

let fresh_instance ?loc ?names env sigma gr =
  let open GlobRef in
  let auctx = match gr with
  | VarRef _ -> UVars.AbstractContext.empty
  | ConstRef c ->
    let cb = lookup_constant env sigma c in
    Declareops.constant_polymorphic_context cb
  | IndRef (mind,_) | ConstructRef ((mind,_),_) ->
    let mib = lookup_mind mind env in
    Declareops.inductive_polymorphic_context mib
  in
  let names = Option.map (fun x -> gr, x) names in
  let u, ctx = UnivGen.fresh_instance_from ?loc auctx names in
  u, ctx

let fresh_constant_instance ?loc ?(rigid=univ_flexible) env evd c =
  let (u, ctx) = fresh_instance env evd (GlobRef.ConstRef c) in
  with_sort_context_set ?loc rigid ~src:UState.Internal evd ((c, u), ctx)

let fresh_inductive_instance ?loc ?sort_rigid ?(rigid=univ_flexible) env evd i =
  with_sort_context_set ?loc ?sort_rigid rigid ~src:UState.Internal evd (UnivGen.fresh_inductive_instance env i)

let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c =
  with_sort_context_set ?loc rigid ~src:UState.Internal evd (UnivGen.fresh_constructor_instance env c)

let fresh_array_instance ?loc ?(rigid=univ_flexible) env evd =
  with_sort_context_set ?loc rigid ~src:UState.Internal evd (UnivGen.fresh_array_instance env)

let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
  let (u, ctx) = fresh_instance ?loc ?names env evd gr in
  with_sort_context_set ?loc rigid ~src:UState.Internal evd (mkRef (gr, u), ctx)

let is_flexible_level evd l =
  let uctx = evd.universes in
  UnivFlex.mem l (UState.subst uctx)

let is_eq_sort s1 s2 =
  if Sorts.equal s1 s2 then None
  else Some (s1, s2)

let normalize_universe_instance evd l =
  UState.nf_instance evd.universes l

let normalize_sort evars s =
  UState.nf_sort evars.universes s

(* FIXME inefficient *)
let set_eq_sort evd s1 s2 =
  let s1 = normalize_sort evd s1 and s2 = normalize_sort evd s2 in
  match is_eq_sort s1 s2 with
  | None -> evd
  | Some (u1, u2) ->
    if QGraph.ignore_constraints (UState.elim_graph evd.universes) then evd else
    add_constraints evd
      (UnivProblem.Set.singleton (UnivProblem.UEq (u1,u2)))

let set_eq_level d u1 u2 =
  add_univ_constraints d (Univ.enforce_eq_level u1 u2 Univ.UnivConstraints.empty)

let set_leq_level d u1 u2 =
  add_univ_constraints d (Univ.enforce_leq_level u1 u2 Univ.UnivConstraints.empty)

let set_eq_instances ?(flex=false) d u1 u2 =
  add_constraints d
    (UnivProblem.enforce_eq_instances_univs flex u1 u2 UnivProblem.Set.empty)

let set_leq_sort evd s1 s2 =
  let s1 = normalize_sort evd s1
  and s2 = normalize_sort evd s2 in
  match is_eq_sort s1 s2 with
  | None -> evd
  | Some (u1, u2) ->
    add_constraints evd @@
      UnivProblem.Set.singleton (UnivProblem.ULe (u1,u2))

let set_eq_qualities evd q1 q2 =
  add_constraints evd @@ UnivProblem.Set.singleton (QEq (q1, q2))

let set_above_prop evd q above =
  { evd with universes = UState.set_above_prop q above evd.universes }

let set_elim_to evd q1 q2 =
  add_constraints evd @@ UnivProblem.Set.singleton (QElimTo (q1, q2))

let check_eq evd s s' =
  let ustate = evd.universes in
  let univs = UState.ugraph ustate in
  UGraph.check_eq_sort Sorts.Quality.equal univs (UState.nf_sort ustate s) (UState.nf_sort ustate s')

let check_leq evd s s' =
  let ustate = evd.universes in
  let univs = UState.ugraph ustate in
  UGraph.check_leq_sort Sorts.Quality.equal univs (UState.nf_sort ustate s) (UState.nf_sort ustate s')

let check_univ_constraints evd csts =
  UGraph.check_constraints csts (UState.ugraph evd.universes)

let check_elim_constraints evd csts =
  UState.check_elim_constraints evd.universes csts

let check_poly_constraints evd (qcsts,ucsts) =
  check_elim_constraints evd qcsts && check_univ_constraints evd ucsts

let check_quality_constraints evd qcst =
  let fold (q1, q2) accu = UnivProblem.Set.add (UnivProblem.QEq (q1, q2)) accu in
  let qcst = UVars.QPairSet.fold fold qcst UnivProblem.Set.empty in
  UState.check_constraints evd.universes qcst

let fix_undefined_variables evd =
  { evd with universes = UState.fix_undefined_variables evd.universes }

let nf_univ_variables evd =
  let uctx = UState.normalize_variables evd.universes in
  {evd with universes = uctx}

let collapse_sort_variables ?except ~only_above_prop evd =
  let universes = UState.collapse_sort_variables ?except ~only_above_prop evd.universes in
  { evd with universes }

let minimize_universes_no_collapse evd =
  let uctx' = UState.normalize_variables evd.universes in
  let uctx' = UState.minimize uctx' in
  {evd with universes = uctx'}

let minimize_universes ?(poly=PolyFlags.default) evd =
  let collapse_sort_variables = PolyFlags.collapse_sort_variables poly in
  let uctx' =
    UState.collapse_sort_variables ~only_above_prop:(not collapse_sort_variables) evd.universes
  in
  minimize_universes_no_collapse {evd with universes = uctx'}

let universe_of_name evd s = UState.universe_of_name evd.universes s

let quality_of_name evd s = UState.quality_of_name evd.universes s

let is_rigid_qvar evd q = UState.is_rigid_qvar evd.universes q

let universe_binders evd = UState.universe_binders evd.universes

let universes evd = UState.ugraph evd.universes

let update_sigma_univs ugraph evd =
  { evd with universes = UState.update_sigma_univs evd.universes ugraph }

exception UniversesDiffer = UState.UniversesDiffer

(**********************************************************)
(* Side effects *)

let concat_side_effects eff1 eff2 = {
  seff_safeenv = None;
  seff_labels = Id.Set.fold Id.Set.add eff1.seff_labels eff2.seff_labels;
  seff_private = Safe_typing.concat_private eff1.seff_private eff2.seff_private;
  seff_roles = Cmap.fold Cmap.add eff1.seff_roles eff2.seff_roles;
  seff_univs = Cmap.fold Cmap.add eff1.seff_univs eff2.seff_univs;
}

let emit_side_effects eff evd =
  let senv = get_senv_side_effects eff in
  let _, senv = Safe_typing.export_private_constants eff.seff_private senv in
  let effects = concat_side_effects eff evd.effects in
  let effects = { effects with seff_safeenv = Some senv } in
  { evd with effects; universes = UState.emit_side_effects eff.seff_private evd.universes }

let set_side_effects eff evd =
  { evd with effects = eff }

let eval_side_effects evd = evd.effects

let push_side_effects ?role ?ts name de ctx effs =
  let senv = get_senv_side_effects effs in
  let senv = match ts with
  | None -> senv
  | Some ts -> Safe_typing.set_oracle ts senv
  in
  let (kn, prv), senv = Safe_typing.add_private_constant name ctx de senv in
  let seff_univs =
    if Univ.Level.Set.is_empty (fst ctx) then effs.seff_univs
    else
      Cmap.add kn (UState.Monomorphic_entry ctx, UnivNames.empty_binders) effs.seff_univs
  in
  let seff_roles = match role with
  | None -> effs.seff_roles
  | Some r -> Cmap.add kn r effs.seff_roles
  in
  let effs = {
    seff_private = Safe_typing.concat_private prv effs.seff_private;
    seff_labels = Id.Set.add (Constant.label kn) effs.seff_labels;
    seff_roles = seff_roles;
    seff_univs = seff_univs;
    seff_safeenv = Some senv;
  } in
  kn, effs

let avoid_side_effect_label id sigma =
  let eff = sigma.effects in
  let eff = { eff with seff_labels = Id.Set.add id eff.seff_labels } in
  { sigma with effects = eff }

let seff_mem_label id effs =
  Id.Set.mem id effs.seff_labels

let seff_private eff = eff.seff_private
let seff_roles effs = effs.seff_roles
let seff_univs effs = effs.seff_univs

(* Future goals *)
let declare_future_goal evk evd =
  let future_goals = FutureGoals.add evk evd.future_goals in
  { evd with future_goals }

let push_future_goals evd =
  { evd with future_goals = FutureGoals.push evd.future_goals }

let pop_future_goals evd =
  let hd, future_goals = FutureGoals.pop evd.future_goals in
  hd, { evd with future_goals }

let fold_future_goals f sigma =
  FutureGoals.fold f sigma sigma.future_goals

let remove_future_goal evd evk =
  { evd with future_goals = FutureGoals.remove evk evd.future_goals }

let pr_future_goals_stack evd =
  FutureGoals.pr_stack evd.future_goals

let give_up ev evd =
  { evd with given_up = Evar.Set.add ev evd.given_up }

let push_shelf evd =
  { evd with shelf = [] :: evd.shelf }

let pop_shelf evd =
  match evd.shelf with
  | [] -> anomaly Pp.(str"shelf stack should not be empty")
  | hd :: tl ->
    hd, { evd with shelf = tl }

let filter_shelf f evd =
  { evd with shelf = List.map (List.filter f) evd.shelf }

let shelve evd l =
  match evd.shelf with
  | [] -> anomaly Pp.(str"shelf stack should not be empty")
  | hd :: tl ->
    { evd with shelf = (hd@l) :: tl }

let unshelve evd l =
  { evd with shelf = List.map (List.filter (fun ev -> not (CList.mem_f Evar.equal ev l))) evd.shelf }

let given_up evd = evd.given_up

let shelf evd = List.flatten evd.shelf

let mem_shelf e evd = List.exists (List.exists (fun e' -> Evar.equal e e')) evd.shelf

let pr_shelf evd =
  let open Pp in
  if List.is_empty evd.shelf then str"(empty stack)"
  else prlist_with_sep (fun () -> str"||") (prlist_with_sep spc Evar.print) evd.shelf

let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ~relevance
  ?(abstract_arguments = Abstraction.identity) ?candidates
  ?name ?parent ?(typeclass_candidate = false) ?(rrpat = false) sign evd typ =
  let evi = {
    evar_hyps = sign;
    evar_concl = Undefined typ;
    evar_body = Evar_empty;
    evar_filter = filter;
    evar_abstract_arguments = Undefined abstract_arguments;
    evar_source = src;
    evar_candidates = Undefined candidates;
    evar_relevance = relevance;
  }
  in
  let newevk = new_untyped_evar () in
  let evd = add_with_name evd ?name ?parent ~typeclass_candidate ~rrpat newevk evi in
  let evd = declare_future_goal newevk evd in
  (evd, newevk)

let define_aux def undef evk body =
  let oldinfo =
    try EvMap.find evk undef
    with Not_found ->
      if EvMap.mem evk def then
        anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.")
      else
        anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
  in
  let () = assert (oldinfo.evar_body == Evar_empty) in
  let newinfo = { oldinfo with
    evar_body = Evar_defined body;
    evar_concl = Defined;
    evar_candidates = Defined;
    evar_abstract_arguments = Defined;
  } in
  EvMap.add evk newinfo def, EvMap.remove evk undef

(* define the existential of section path sp as the constr body *)
let define_gen evk body evd evar_flags =
  let future_goals = FutureGoals.remove evk evd.future_goals in
  let evd = { evd with future_goals } in
  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
  let last_mods = match evd.conv_pbs with
  | [] ->  evd.last_mods
  | _ -> Evar.Set.add evk evd.last_mods
  in
  let evar_names = Evarnames.remove evk evd.evar_names in
  let candidate_evars = Evar.Set.remove evk evd.candidate_evars in
  { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags; candidate_evars }

(** By default, the obligation and evar tag of the evar is removed *)
let define evk body evd =
  let evar_flags = remove_evar_flags evk evd.evar_flags in
  define_gen evk body evd evar_flags

(** In case of an evar-evar solution, the flags are inherited *)
let define_with_evar evk body evd =
  let evk' = fst (destEvar body) in
  let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
  let evd = unshelve evd [evk] in
  define_gen evk body evd evar_flags

(* In case of restriction, we declare the aliasing and inherit the obligation
   and typeclass flags. *)

let restrict evk filter ?candidates ?src evd =
  let evk' = new_untyped_evar () in
  let evar_info = EvMap.find evk evd.undf_evars in
  let len = Environ.nb_named evar_info.evar_hyps in
  let id_inst = Filter.filter_slist filter (SList.defaultn len SList.empty) in
  let evar_info' =
    { evar_info with evar_filter = filter;
      evar_candidates = Undefined candidates;
      evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
    } in
  let last_mods = match evd.conv_pbs with
  | [] ->  evd.last_mods
  | _ -> Evar.Set.add evk evd.last_mods in
  let evar_names = Evarnames.transfer_name evk evk' evd.evar_names in
  let body = mkEvar(evk',id_inst) in
  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
  let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
  let evar_flags = match src with
    | Some (_,Evar_kinds.ImpossibleCase) ->
      { evar_flags with impossible_case_evars = Evar.Set.add evk' evar_flags.impossible_case_evars }
    | _ -> evar_flags
  in
  let candidate_evars = Evar.Set.remove evk evd.candidate_evars in
  let candidate_evars = match candidates with
  | None -> candidate_evars
  | Some _ -> Evar.Set.add evk' candidate_evars
  in
  let evd = { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
    defn_evars; last_mods; evar_names; evar_flags; candidate_evars }
  in
  (* If evk was in the shelf or future goals, replace it with evk' *)
  let changed = ref false in
  let shelf =
    List.Smart.map (List.Smart.map (fun ev ->
      if Evar.equal ev evk then
        let () = changed := true in
        evk'
      else ev))
      evd.shelf
  in
  let evd =
    if !changed then { evd with shelf }
    else if FutureGoals.mem evk evd.future_goals then
      (* NB this moves the evar to the end of the future goals instead
         of keeping its location as we do for shelf *)
      let future_goals = FutureGoals.(add evk' @@ remove evk evd.future_goals) in
      { evd with future_goals }
    else evd
  in
  (evd, evk')

let update_source evd evk src =
  let modify _ info = { info with evar_source = src } in
  { evd with undf_evars = EvMap.modify evk modify evd.undf_evars }

let dependent_evar_ident ev evd =
  let EvarInfo evi = find evd ev in
  match evi.evar_source with
  | (_,Evar_kinds.VarInstance id) -> id
  | _ -> anomaly (str "Not an evar resulting of a dependent binding.")

(**********************************************************)
(* Extra data *)

let get_extra_data evd = evd.extras
let set_extra_data extras evd = { evd with extras }

(*******************************************************************)
(* The state monad with state an evar map. *)

module Monad =
  Monad.Make (struct

    type +'a t = evar_map -> evar_map * 'a

    let return a = fun s -> (s,a)

    let (>>=) x f = fun s ->
      let (s',a) = x s in
      f a s'

    let (>>) x y = fun s ->
      let (s',()) = x s in
      y s'

    let map f x = fun s ->
      on_snd f (x s)

  end)

(**********************************************************)
(* Failure explanation *)

type unsolvability_explanation = SeveralInstancesFound of int

module Expand :
sig
  type handle
  val empty_handle : handle
  val liftn_handle : int -> handle -> handle
  val kind : evar_map -> handle -> constr ->
    handle * (constr, constr, Sorts.t, UVars.Instance.t, Sorts.relevance) kind_of_term
  val expand : evar_map -> handle -> constr -> constr
  val expand_instance : skip: bool -> undefined evar_info -> handle -> econstr SList.t -> econstr SList.t
end =
struct

type clos = {
  evc_map : (int * clos * Constr.t) Id.Map.t;
  (* Map each bound ident to its value and the depth it was introduced at *)
  evc_lift : int; (* number of binders crossed since last evar *)
  evc_stack : int list; (* stack of binders crossed at each evar *)
  evc_depth : int; (* length of evc_stack *)
  evc_cache : int Int.Map.t ref option; (* Cache get_lift on evc_stack *)
}

let empty_clos = {
  evc_lift = 0;
  evc_depth = 0;
  evc_stack = [];
  evc_map = Id.Map.empty;
  evc_cache = None;
}

let push_clos info clos args =
  let push id c map = Id.Map.add id (clos.evc_depth, clos, c) map in
  let nmap = evar_instance_array clos.evc_map push info args in
  {
    evc_lift = 0;
    evc_map = nmap;
    evc_depth = clos.evc_depth + 1;
    evc_stack = clos.evc_lift :: clos.evc_stack;
    evc_cache = Some (ref Int.Map.empty);
  }

let find_clos clos id = match Id.Map.find_opt id clos.evc_map with
| None -> None
| Some (depth, nclos, v) ->
  let pos = clos.evc_depth - depth - 1 in
  let rec get_lift accu n lft =
    if Int.equal n 0 then accu
    else match lft with
    | [] -> assert false
    | k :: lft -> get_lift (accu + k) (n - 1) lft
  in
  let ans = match clos.evc_cache with
  | None -> assert false
  | Some cache ->
    match Int.Map.find_opt pos !cache with
    | None ->
      let ans = get_lift 0 pos clos.evc_stack in
      let () = cache := Int.Map.add pos ans !cache in
      ans
    | Some ans -> ans
  in
  let k = clos.evc_lift + ans in
  Some (k, nclos, v)

type handle = {
  h_clos : clos;
  h_lift : Esubst.lift;
}

let empty_handle = {
  h_clos = empty_clos;
  h_lift = Esubst.el_id;
}

let liftn_clos n s = { s with evc_lift = s.evc_lift + n }

let liftn_handle n h = {
  h_clos = liftn_clos n h.h_clos;
  h_lift = Esubst.el_liftn n h.h_lift;
}

let rec kind sigma h c = match Constr.kind c with
| Rel n -> h, Rel (Esubst.reloc_rel n h.h_lift)
| Var id as c0 ->
  begin match find_clos h.h_clos id with
  | None -> (h, c0)
  | Some (k, clos, v) ->
    let h = { h_clos = clos; h_lift = Esubst.el_shft k h.h_lift } in
    kind sigma h v
  end
| Evar (evk, args) as c0 ->
  begin match EvMap.find_opt evk sigma.defn_evars with
  | None -> (h, c0)
  | Some info ->
    let Evar_defined c = evar_body info in
    let nclos = push_clos info h.h_clos args in
    kind sigma { h_lift = h.h_lift; h_clos = nclos } c
  end
| Meta _ | Sort _ | Cast _  | Prod _ | Lambda _ | LetIn _ | App _
| Const _ | Ind _ | Construct _ | Case _ | Fix _ | CoFix _ | Proj _
| Int _ | Float _ | String _ | Array _ as c0 ->
  (h, c0)

let expand0 sigma h c =
  let lift h = liftn_handle 1 h in
  let rec aux h c = match Constr.kind c with
  | Rel n ->
    let n' = Esubst.reloc_rel n h.h_lift in
    if Int.equal n n' then c else mkRel n'
  | Var id ->
    begin match find_clos h.h_clos id with
    | None -> c
    | Some (k, clos, v) ->
      let h = { h_clos = clos; h_lift = Esubst.el_shft k h.h_lift } in
      aux h v
    end
  | Evar (evk, args) ->
    (* for efficiency do not expand evars, just their instance *)
    let EvarInfo evi = find sigma evk in
    let push decl c args =
      if isVarId (NamedDecl.get_id decl) c then SList.default args
      else SList.cons c args
    in
    let rec expand ctx args = match ctx, SList.view args with
    | [], None -> SList.empty
    | decl :: ctx, Some (Some c, args) ->
      let c = aux h c in
      push decl c (expand ctx args)
    | decl :: ctx, Some (None, args) ->
      let c = aux h (mkVar (NamedDecl.get_id decl)) in
      push decl c (expand ctx args)
    | [], Some _ | _ :: _, None -> instance_mismatch ()
    in
    let args = expand (evar_filtered_context evi) args in
    mkEvar (evk, args)
  | _ -> Constr.map_with_binders lift aux h c
  in
  aux h c

let expand sigma h c =
  if Esubst.is_lift_id h.h_lift && Id.Map.is_empty h.h_clos.evc_map then c
  else expand0 sigma h c

let expand_instance ~skip (evi : undefined evar_info) h (args : Constr.t SList.t) =
  if skip && Id.Map.is_empty h.h_clos.evc_map then args
  else
    let rec expand ctx args = match ctx, SList.view args with
    | [], None -> SList.empty
    | decl :: ctx, Some (None, args) ->
      let args = expand ctx args in
      let id = NamedDecl.get_id decl in
      if Id.Map.mem id h.h_clos.evc_map then
        (* Keep the non-default representation as kind will expand it *)
        SList.cons (mkVar id) args
      else if skip then SList.default args
      else SList.cons (mkVar id) args
    | decl :: ctx, Some (Some c, args) ->
      let args = expand ctx args in
      let id = NamedDecl.get_id decl in
      (* Same as above *)
      if skip && isVarId id c && not (Id.Map.mem id h.h_clos.evc_map) then SList.default args
      else SList.cons c args
    | [], Some _ | _ :: _, None -> instance_mismatch ()
    in
    expand (evar_filtered_context evi) args

end

module MiniEConstr = struct

  module ERelevance = struct
    type t = Sorts.relevance
    let make r = r
    let unsafe_to_relevance r = r
    let kind sigma r = UState.nf_relevance sigma.universes r
  end

  module ESorts =
  struct
    type t = Sorts.t
    let make s = s
    let kind = normalize_sort
    let unsafe_to_sorts s = s
  end

  module EInstance =
  struct
    type t = UVars.Instance.t
    let make i = i
    let kind sigma i =
      if UVars.Instance.is_empty i then i
      else normalize_universe_instance sigma i
    let empty = UVars.Instance.empty
    let is_empty = UVars.Instance.is_empty
    let unsafe_to_instance t = t
  end

  type t = econstr

  let rec whd_evar sigma c =
    match Constr.kind c with
    | Evar ev ->
      let (h, knd) = Expand.kind sigma Expand.empty_handle c in
      if Constr.kind c == knd then c
      else whd_kind sigma h knd
    | App (f, args) when isEvar f ->
      (* Enforce smart constructor invariant on applications *)
      let (h, knd) = Expand.kind sigma Expand.empty_handle f in
      if Constr.kind f == knd then c
      else mkApp (whd_kind sigma h knd, args)
    | Cast (c0, k, t) when isEvar c0 ->
      (* Enforce smart constructor invariant on casts. *)
      let (h, knd) = Expand.kind sigma Expand.empty_handle c0 in
      if Constr.kind c0 == knd then c
      else mkCast (whd_kind sigma h knd, k, t)
    | _ -> c
  and whd_kind sigma h knd =
    (* we need to force the head as Expand.expand does not expand evar subterms *)
    whd_evar sigma (Expand.expand sigma h (Constr.of_kind knd))

  let mkLEvar = mkLEvar
  let replace_vars = replace_vars
  let kind sigma c = Constr.kind (whd_evar sigma c)
  let kind_upto = kind
  let of_kind = Constr.of_kind
  let of_constr c = c
  let of_constr_array v = v
  let unsafe_to_constr c = c
  let unsafe_to_constr_array v = v
  let unsafe_eq = Refl
  let unsafe_relevance_eq = Refl

  type evclos = {
    evc_map : (int * Vars.substituend Lazy.t) Id.Map.t;
    (* Map each bound ident to its value and the depth it was introduced at *)
    evc_lift : int; (* number of binders crossed since last evar *)
    evc_stack : int list; (* stack of binders crossed at each evar *)
    evc_depth : int; (* length of evc_stack *)
    evc_cache : int Int.Map.t ref; (* Cache get_lift on evc_stack *)
  }

  let to_constr_gen ~expand ~ignore_missing sigma c =
    let saw_evar = ref false in
    let lsubst = universe_subst sigma in
    let univ_value l =
      UnivFlex.normalize_univ_variable lsubst l
    in
    let relevance_value r = UState.nf_relevance sigma.universes r in
    let qvar_value q = UState.nf_qvar sigma.universes q in
    let next s = { s with evc_lift = s.evc_lift + 1 } in
    let find clos id = match Id.Map.find_opt id clos.evc_map with
    | None -> None
    | Some (depth, lazy v) ->
      let pos = clos.evc_depth - depth - 1 in
      let rec get_lift accu n lft =
        if Int.equal n 0 then accu
        else match lft with
        | [] -> assert false
        | k :: lft -> get_lift (accu + k) (n - 1) lft
      in
      let ans = match Int.Map.find_opt pos clos.evc_cache.contents with
      | None ->
        let ans = get_lift 0 pos clos.evc_stack in
        let () = clos.evc_cache := Int.Map.add pos ans clos.evc_cache.contents in
        ans
      | Some ans -> ans
      in
      let k = clos.evc_lift + ans in
      Some (lift_substituend k v)
    in
    let rec self clos c = match Constr.kind c with
    | Var id ->
      begin match find clos id with
      | None -> c
      | Some v -> v
      end
    | Evar (evk, args) ->
      begin match EvMap.find_opt evk sigma.defn_evars with
      | None ->
        let () = saw_evar := true in
        begin match EvMap.find_opt evk sigma.undf_evars with
        | None ->
          if ignore_missing then
            let map c = self clos c in
            let args' = SList.Smart.map map args in
            if args' == args then c else mkEvar (evk, args')
          else raise Not_found
        | Some evi ->
          let rec inst ctx args = match ctx, SList.view args with
          | [], None -> SList.empty
          | decl :: ctx, Some (c, args) ->
            let c = match c with
            | None ->
              let c = find clos (NamedDecl.get_id decl) in
              if expand then match c with
              | None -> Some (mkVar (NamedDecl.get_id decl))
              | Some _  -> c
              else c
            | Some c -> Some (self clos c)
            in
            SList.cons_opt c (inst ctx args)
          | _ :: _, None | [], Some _ -> instance_mismatch ()
          in
          let args' = inst (evar_filtered_context evi) args in
          if args == args' then c else mkEvar (evk, args')
        end
      | Some info ->
        let Evar_defined c = evar_body info in
        let push id c map = Id.Map.add id (clos.evc_depth, lazy (make_substituend (self clos c))) map in
        let nmap = evar_instance_array clos.evc_map push info args in
        let nclos = {
          evc_lift = 0;
          evc_map = nmap;
          evc_depth = clos.evc_depth + 1;
          evc_stack = clos.evc_lift :: clos.evc_stack;
          evc_cache = ref Int.Map.empty;
        } in
        self nclos c
      end
    | _ ->
      UnivSubst.map_universes_opt_subst_with_binders next self relevance_value qvar_value univ_value clos c
    in
    let clos = {
      evc_lift = 0;
      evc_depth = 0;
      evc_stack = [];
      evc_map = Id.Map.empty;
      evc_cache = ref Int.Map.empty;
    } in
    let c = self clos c in
    !saw_evar, c

  let check_evar c =
    let exception SawEvar in
    let rec iter c = match Constr.kind c with
      | Evar _ -> raise SawEvar
      | _ -> Constr.iter iter c
    in
    try iter c; false with SawEvar -> true

  let to_constr ?(abort_on_undefined_evars=true) sigma c =
    let saw_evar, c = to_constr_gen ~expand:true ~ignore_missing:false sigma c in
    if abort_on_undefined_evars && saw_evar && check_evar c then
      anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term")
    else c

  let to_constr_opt sigma c =
    let saw_evar, c = to_constr_gen ~expand:false ~ignore_missing:false sigma c in
    if saw_evar && check_evar c then None else Some c

  let nf_evar sigma c =
    let _, c = to_constr_gen ~expand:false ~ignore_missing:true sigma c in
    c

  let of_named_decl d = d
  let unsafe_to_named_decl d = d
  let of_rel_decl d = d
  let unsafe_to_rel_decl d = d

  let of_named_context d = d
  let of_rel_context d = d

  let unsafe_to_case_invert x = x
  let of_case_invert x = x

  let lookup_constant = lookup_constant
end

(** The following functions return the set of evars immediately
    contained in the object *)

(* excluding defined evars *)

let evars_of_term evd c =
  let rec evrec acc c =
    let c = MiniEConstr.whd_evar evd c in
    match kind c with
    | Evar (n, l) -> Evar.Set.add n (SList.Skip.fold evrec acc l)
    | _ -> Constr.fold evrec acc c
  in
  evrec Evar.Set.empty c

let evars_of_named_context evd nc =
  Context.Named.fold_outside
    (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term evd constr)))
    nc
    ~init:Evar.Set.empty

let evars_of_filtered_evar_info (type a) evd (evi : a evar_info) =
  let concl = match evi.evar_concl with
  | Undefined c -> evars_of_term evd c
  | Defined -> Evar.Set.empty
  in
  Evar.Set.union concl
    (Evar.Set.union
       (match evi.evar_body with
       | Evar_empty -> Evar.Set.empty
       | Evar_defined b -> evars_of_term evd b)
       (evars_of_named_context evd (evar_filtered_context evi)))

let drop_new_defined ~original sigma =
  NewProfile.profile "drop_new_defined" (fun () ->
  let to_keep, to_drop = Evar.Map.partition (fun ev _ ->
      Evar.Map.mem ev original.defn_evars || Evar.Map.mem ev original.undf_evars)
      sigma.defn_evars
  in
  let dummy = { empty with defn_evars = to_drop } in
  let nfc c = snd @@ MiniEConstr.to_constr_gen ~expand:true ~ignore_missing:false dummy c in (* FIXME: do we really need to expand? *)
  assert (List.is_empty sigma.conv_pbs);
  let normalize_changed _ev orig evi =
    match orig, evi with
    | _, None -> None
    | None, Some evi -> Some (map_evar_info nfc evi)
    | Some orig, Some evi -> if orig == evi then None else Some (map_evar_info nfc evi)
  in
  let normalize_against original current =
    let normalized = EvMap.merge normalize_changed original current in
    EvMap.union (fun _ _ x -> Some x) current normalized
  in
  let to_keep = normalize_against original.defn_evars to_keep in
  let undf_evars = normalize_against original.undf_evars sigma.undf_evars in
  { sigma with defn_evars = to_keep; undf_evars })
    ()