(************************************************************************)
(*         *      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 Util
open Names
open Constr
open Environ
open Evd
open Termops
open Namegen

module ERelevance = EConstr.ERelevance

module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration

let create_clos_infos env sigma flags =
  let open CClosure in
  let evars = Evd.evar_handler sigma in
  create_clos_infos ~univs:(Evd.universes sigma) ~evars flags env


(****************************************************)
(* Expanding/testing/exposing existential variables *)
(****************************************************)

let finalize ?abort_on_undefined_evars ?poly sigma f =
  let sigma = minimize_universes ?poly sigma in
  let uvars = ref Univ.Level.Set.empty in
  let nf_constr c =
    let _, varsc = EConstr.universes_of_constr sigma c in
    let c = EConstr.to_constr ?abort_on_undefined_evars sigma c in
    uvars := Univ.Level.Set.union !uvars varsc;
    c
  in
  let v = f nf_constr in
  let sigma = restrict_ustate sigma !uvars in
  sigma, v

(** Term exploration up to instantiation. *)
let kind_of_term_upto = EConstr.kind_upto

let nf_evars_universes sigma t = EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t)
let whd_evar = EConstr.whd_evar

let nf_evar = Evd.MiniEConstr.nf_evar

let j_nf_evar sigma j =
  { uj_val = nf_evar sigma j.uj_val;
    uj_type = nf_evar sigma j.uj_type }
let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
let tj_nf_evar sigma {utj_val=v;utj_type=t} =
  {utj_val=nf_evar sigma v;utj_type=t}

let nf_relevance sigma r =
  UState.nf_relevance (Evd.ustate sigma) r

let nf_named_decl_evar sigma status ctx =
  status, Context.Named.Declaration.map_constr_with_relevance (nf_relevance sigma) (nf_evars_universes sigma) ctx

let nf_rel_context_evar sigma ctx =
  let nf_relevance r = ERelevance.make (ERelevance.kind sigma r) in
  Context.Rel.map_with_relevance nf_relevance (nf_evar sigma) ctx

let nf_env_evar sigma env =
  let nc' = Environ.map_named_val (nf_named_decl_evar sigma) (Environ.named_context_val env) in
  let rel' = nf_rel_context_evar sigma (EConstr.rel_context env) in
    EConstr.push_rel_context rel' (reset_with_named_context nc' env)

let nf_evar_info evc info = map_evar_info (nf_evar evc) info

let nf_evar_map evm =
  Evd.raw_map { map = fun _ evi -> nf_evar_info evm evi } evm

let nf_evar_map_undefined evm =
  Evd.raw_map_undefined (fun _ evi -> nf_evar_info evm evi) evm

(*-------------------*)
(* Auxiliary functions for the conversion algorithms modulo evars
 *)

let has_undefined_evars evd t =
  let rec f h t =
    let (h, knd) = EConstr.Expand.kind evd h t in
    match knd with
    | Evar _ -> raise NotInstantiatedEvar
    | _ -> EConstr.Expand.iter evd f h knd
  in
  let h, t = EConstr.Expand.make t in
  try let _ = f h t in false
  with (Not_found | NotInstantiatedEvar) -> true

let has_undefined_evars_or_metas evd t =
  let rec has_ev t =
    match EConstr.kind evd t with
    | Evar _ | Meta _ -> raise NotInstantiatedEvar
    | _ -> EConstr.iter evd has_ev t in
  try let _ = has_ev t in false
  with (Not_found | NotInstantiatedEvar) -> true

let is_ground_term evd t =
  not (has_undefined_evars evd t)

let is_ground_env evd env =
  let is_ground_rel_decl = function
    | RelDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b)
    | _ -> true in
  let is_ground_named_decl = function
    (* skip if SecVar? *)
    | NamedDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b)
    | _ -> true in
  List.for_all is_ground_rel_decl (rel_context env) &&
  List.for_all is_ground_named_decl (named_context env)

(* Expand head evar if any (currently consider only applications but I
   guess it should consider Case too) *)

let whd_head_evar_stack sigma c =
  let rec whrec (c, l) =
    match EConstr.kind sigma c with
      | Cast (c,_,_) -> whrec (c, l)
      | App (f,args) -> whrec (f, args :: l)
      | c -> (EConstr.of_kind c, l)
  in
  whrec (c, [])

let whd_head_evar sigma c =
  let open EConstr in
  let (f, args) = whd_head_evar_stack sigma c in
  match args with
  | [arg] -> mkApp (f, arg)
  | _ -> mkApp (f, Array.concat args)

(**********************)
(* Creating new metas *)
(**********************)

let meta_counter_summary_name = "meta counter"

(* Generator of metavariables *)
let meta_ctr, meta_counter_summary_tag =
  Summary.ref_tag 0 ~name:meta_counter_summary_name

let new_meta () =
  let open Summary.Ref in
  meta_ctr := !meta_ctr + 1;
  !meta_ctr

(* The list of non-instantiated existential declarations (order is important) *)

(*------------------------------------*
 * functional operations on evar sets *
 *------------------------------------*)

(* [push_rel_context_to_named_context] builds the defining context and the
 * initial instance of an evar. If the evar is to be used in context
 *
 * Gamma =  a1     ...    an xp      ...       x1
 *          \- named part -/ \- de Bruijn part -/
 *
 * then the x1...xp are turned into variables so that the evar is declared in
 * context
 *
 *          a1     ...    an xp      ...       x1
 *          \----------- named part ------------/
 *
 * but used applied to the initial instance "a1 ... an Rel(p) ... Rel(1)"
 * so that ev[a1:=a1 ... an:=an xp:=Rel(p) ... x1:=Rel(1)] is correctly typed
 * in context Gamma.
 *
 * Remark 1: The instance is reverted in practice (i.e. Rel(1) comes first)
 * Remark 2: If some of the ai or xj are definitions, we keep them in the
 *   instance. This is necessary so that no unfolding of local definitions
 *   happens when inferring implicit arguments (consider e.g. the problem
 *   "x:nat; x':=x; f:forall y, y=y -> Prop |- f _ (refl_equal x')" which
 *   produces the equation "?y[x,x']=?y[x,x']" =? "x'=x'": we want
 *   the hole to be instantiated by x', not by x (which would have been
 *   the case in [invert_definition] if x' had disappeared from the instance).
 *   Note that at any time, if, in some context env, the instance of
 *   declaration x:A is t and the instance of definition x':=phi(x) is u, then
 *   we have the property that u and phi(t) are convertible in env.
 *)

let next_ident_away id avoid =
  let avoid id = Id.Set.mem id avoid in
  next_ident_away_from id avoid

type subst_val =
| SRel of int
| SVar of Id.t

type csubst = {
  csubst_len : int;
  (** Cardinal of [csubst_rel] *)
  csubst_var : Constr.t Id.Map.t;
  (** A mapping of variables to variables. We use the more general
      [Constr.t] to share allocations, but all values are of shape [Var _]. *)
  csubst_rel : Constr.t Int.Map.t;
  (** A contiguous mapping of integers to variables. Same remark for values. *)
  csubst_rev : subst_val Id.Map.t;
  (** Reverse mapping of the substitution *)
}
(** This type represents a name substitution for the named and De Bruijn parts of
    an environment. For efficiency we also store the reverse substitution.
    Invariant: all identifiers in the codomain of [csubst_var] and [csubst_rel]
    must be pairwise distinct. *)

let empty_csubst = {
  csubst_len = 0;
  csubst_rel = Int.Map.empty;
  csubst_var = Id.Map.empty;
  csubst_rev = Id.Map.empty;
}

let csubst_subst sigma { csubst_len = k; csubst_var = v; csubst_rel = s } c =
  (* Safe because this is a substitution *)
  let c = EConstr.Unsafe.to_constr c in
  let rec subst n c = match Constr.kind c with
  | Rel m ->
    if m <= n then c
    else if m - n <= k then Int.Map.find (k - m + n) s
    else mkRel (m - k)
  | Var id ->
    begin try Id.Map.find id v with Not_found -> c end
  | Evar (evk, args) ->
    let EvarInfo evi = Evd.find sigma evk in
    let args' = subst_instance n (evar_filtered_context evi) args in
    if args' == args then c else Constr.mkEvar (evk, args') (* FIXME: preserve sharing *)
  | _ -> Constr.map_with_binders succ subst n c

  and subst_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 try Some (Id.Map.find (NamedDecl.get_id decl) v) with Not_found -> c end
    | Some c ->
      let c' = subst n c in
      if isVarId (NamedDecl.get_id decl) c' then None else Some c'
    in
    SList.cons_opt c' (subst_instance n ctx args)
  | _ :: _, None | [], Some _ -> assert false
  in
  let c = if k = 0 && Id.Map.is_empty v then c else subst 0 c in
  EConstr.of_constr c

type ext_named_context = {
  ext_subst : csubst;
  ext_avoid : Id.Set.t;
  ext_ctx : named_context_val;
}

let ext_named_context_val ext = ext.ext_ctx
let ext_csubst ext = ext.ext_subst

let push_var id { csubst_len = n; csubst_var = v; csubst_rel = s; csubst_rev = r } =
  let s = Int.Map.add n (Constr.mkVar id) s in
  let r = Id.Map.add id (SRel n) r in
  { csubst_len = succ n; csubst_var = v; csubst_rel = s; csubst_rev = r }

(** Post-compose the substitution with the generator [src ↦ tgt] *)
let update_var src tgt subst =
  let cur =
    try Some (Id.Map.find src subst.csubst_rev)
    with Not_found -> None
  in
  match cur with
  | None ->
    (* Missing keys stand for identity substitution [src ↦ src] *)
    let csubst_var = Id.Map.add src (Constr.mkVar tgt) subst.csubst_var in
    let csubst_rev = Id.Map.add tgt (SVar src) subst.csubst_rev in
    { subst with csubst_var; csubst_rev }
  | Some bnd ->
    let csubst_rev = Id.Map.add tgt bnd (Id.Map.remove src subst.csubst_rev) in
    match bnd with
    | SRel m ->
      let csubst_rel = Int.Map.add m (Constr.mkVar tgt) subst.csubst_rel in
      { subst with csubst_rel; csubst_rev }
    | SVar id ->
      let csubst_var = Id.Map.add id (Constr.mkVar tgt) subst.csubst_var in
      { subst with csubst_var; csubst_rev }

let push_rel_decl_to_named_context
  env sigma decl (ext : ext_named_context) =
  let open EConstr in
  let open Vars in
  let map_decl f d =
    NamedDecl.map_constr f d
  in
  let rec replace_var_named_declaration id0 id nc = match match_named_context_val nc with
  | None -> empty_named_context_val
  | Some (status, decl, nc) ->
    if Id.equal id0 (NamedDecl.get_id decl) then
      (* Stop here, the variable cannot occur before its definition
         NB: we lose section variable status *)
      push_named_context_val ProofVar (NamedDecl.set_id id decl) nc
    else
      let nc = replace_var_named_declaration id0 id nc in
      let vsubst = [id0 , mkVar id] in
      push_named_context_val status (map_decl (fun c -> replace_vars sigma vsubst c) decl) nc
  in
  let extract_if_neq id = function
    | Anonymous -> None
    | Name id' when Id.equal id id' -> None
    | Name id' -> Some id'
  in
  let na = RelDecl.get_name decl in
  let id =
    (* id_of_name_using_hdchar only depends on the rel context which is empty
        here *)
    next_ident_away (id_of_name_using_hdchar (reset_context env) sigma (RelDecl.get_type decl) na) ext.ext_avoid
  in
  match extract_if_neq id na with
  | Some id0 ->
    if Environ.mem_named_ctxt id0 ext.ext_ctx && is_section_variable_sign ext.ext_ctx id0 then
      (* spiwack: if [id0] is a section variable renaming it is
          incorrect. We revert to a less robust behaviour where
          the new binder has name [id]. Which amounts to the same
          behaviour than when [id=id0]. *)
      let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst sigma ext.ext_subst) in
      { ext_subst = push_var id ext.ext_subst;
        ext_avoid = Id.Set.add id ext.ext_avoid;
        ext_ctx = push_named_context_val ProofVar d ext.ext_ctx }
    else
      (* spiwack: if [id<>id0], rather than introducing a new
          binding named [id], we will keep [id0] (the name given
          by the user) and rename [id0] into [id] in the named
          context. Unless [id] is a section variable. *)
      let subst = update_var id0 id ext.ext_subst in
      let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst sigma subst) in
      let nc = replace_var_named_declaration id0 id ext.ext_ctx in
      let avoid = Id.Set.add id (Id.Set.add id0 ext.ext_avoid) in
      { ext_subst = push_var id0 subst;
        ext_avoid = avoid;
        ext_ctx = push_named_context_val ProofVar d nc }
  | None ->
    let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst sigma ext.ext_subst) in
    { ext_subst = push_var id ext.ext_subst;
      ext_avoid = Id.Set.add id ext.ext_avoid;
      ext_ctx = push_named_context_val ProofVar d ext.ext_ctx }

let csubst_instance subst ctx =
  let fold decl accu = match Id.Map.find (NamedDecl.get_id decl) subst.csubst_rev with
  | SRel n -> SList.cons (EConstr.mkRel (subst.csubst_len - n)) accu
  | SVar id -> SList.cons (EConstr.mkVar id) accu
  | exception Not_found -> SList.default accu
  in
  List.fold_right fold ctx SList.empty

let ext_rev_subst { ext_subst = subst } id0 =
  match Id.Map.find id0 subst.csubst_rev with
  | SRel n -> EConstr.mkRel (subst.csubst_len - n)
  | SVar id -> EConstr.mkVar id

let default_ext_instance { ext_subst = subst; ext_ctx = ctx } =
  csubst_instance subst (named_context_of_val ctx)

let push_rel_context_to_named_context env sigma typ =
  (* compute the instances relative to the named context and rel_context *)
  let open EConstr in
  let ctx = named_context_val env in
  if List.is_empty (Environ.rel_context env) then
    let inst = SList.defaultn (List.length @@ named_context_of_val ctx) SList.empty in
    (ctx, typ, inst, empty_csubst)
  else
    let avoid = Environ.ids_of_named_context_val (named_context_val env) in
    (* move the rel context to a named context and extend the named instance *)
    (* with vars of the rel context *)
    (* We do keep the instances corresponding to local definition (see above) *)
    let init = { ext_subst = empty_csubst; ext_avoid = avoid; ext_ctx = ctx } in
    let ext =
      Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context env sigma d acc)
        (rel_context env) ~init in
    let inst = default_ext_instance ext in
    (ext.ext_ctx, csubst_subst sigma ext.ext_subst typ, inst, ext.ext_subst)

let ext_named_context_of_env env sigma =
  let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
  let init = { ext_subst = empty_csubst; ext_avoid = avoid; ext_ctx = named_context_val env } in
  Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context env sigma d acc)
    (EConstr.rel_context env) ~init

(*------------------------------------*
 * Entry points to define new evars   *
 *------------------------------------*)

let new_pure_evar = Evd.new_pure_evar

let next_evar_name naming = match naming with
| IntroAnonymous -> None
| IntroFresh id -> Some (id, true)
| IntroIdentifier id -> Some (id, false)

(* [new_evar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
let new_evar ?src ?filter ?relevance ?abstract_arguments ?candidates ?(naming = IntroAnonymous) ?parent ?typeclass_candidate
    ?rrpat env evd typ =
  let name = next_evar_name naming in
  let sign,typ',instance,subst = push_rel_context_to_named_context env evd typ in
  let map c = csubst_subst evd subst c in
  let candidates = Option.map (fun l -> List.map map l) candidates in
  let instance =
    match filter with
    | None -> instance
    | Some filter -> Filter.filter_slist filter instance in
  let relevance = match relevance with
  | Some r -> r
  | None -> ERelevance.relevant (* FIXME: relevant_of_type not defined yet *)
  in
  let (evd, evk) = new_pure_evar sign evd typ' ?src ?rrpat ?filter ~relevance ?abstract_arguments ?candidates ?name ?parent
    ?typeclass_candidate in
  (evd, EConstr.mkEvar (evk, instance))

let new_type_evar ?src ?filter ?naming env evd rigid =
  let (evd', s) = new_sort_variable rigid evd in
  let relevance = EConstr.ESorts.relevance_of_sort s in
  let (evd', e) = new_evar env evd' ?src ?filter ~relevance ?naming ~typeclass_candidate:false (EConstr.mkSort s) in
  evd', (e, s)

let new_Type ?(rigid=Evd.univ_flexible) evd =
  let open EConstr in
  let (evd, s) = new_sort_variable rigid evd in
  (evd, mkSort s)

(* Safe interface to unification problems *)
type unification_pb = conv_pb * env * EConstr.constr * EConstr.constr

let eq_unification_pb evd (pbty,env,t1,t2) (pbty',env',t1',t2') =
  pbty == pbty' && env == env' &&
    EConstr.eq_constr evd t1 t1' &&
    EConstr.eq_constr evd t2 t2'

let add_unification_pb ?(tail=false) pb evd =
  let conv_pbs = Evd.conv_pbs evd in
  if not (List.exists (eq_unification_pb evd pb) conv_pbs) then
    let (pbty,env,t1,t2) = pb in
    Evd.add_conv_pb ~tail (pbty,env,t1,t2) evd
  else evd

(* This assumes an evar with identity instance and generalizes it over only
   the de Bruijn part of the context *)
let generalize_evar_over_rels sigma (ev,args) =
  let open EConstr in
  let evi = Evd.find_undefined sigma ev in
  let args = Evd.expand_existential sigma (ev, args) in
  let sign = named_context_of_val (Evd.evar_hyps evi) in
  List.fold_left2
    (fun (c,inst as x) a d ->
      if isRel sigma a then (mkNamedProd_or_LetIn sigma d c,a::inst) else x)
     (Evd.evar_concl evi,[]) args sign

(************************************)
(* Removing a dependency in an evar *)
(************************************)

type clear_dependency_error =
| OccurHypInSimpleClause of Id.t option
| EvarTypingBreak of EConstr.existential
| NoCandidatesLeft of Evar.t

exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option

exception Depends of Id.t

let set_of_evctx l =
  List.fold_left (fun s decl -> Id.Set.add (NamedDecl.get_id decl) s) Id.Set.empty l

let filter_effective_candidates evd evi filter candidates =
  let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in
  List.filter (fun a -> Id.Set.subset (collect_vars evd a) ids) candidates

let restrict_evar evd evk filter candidates =
  let evar_info = Evd.find_undefined evd evk in
  let candidates = Option.map (filter_effective_candidates evd evar_info filter) candidates in
  match candidates with
  | Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None))
  | _ -> Evd.restrict evk filter ?candidates evd

(* FIXME: put this somewhere more sensible *)
let vars_of_global env sigma gr =
  let open GlobRef in
  match gr with
  | ConstRef cst ->
    let eff = Evd.eval_side_effects sigma in
    if Safe_typing.is_empty_private_constants @@ Evd.seff_private @@ eff then
      Environ.vars_of_global env gr
    else
      let senv = Evd.get_senv_side_effects eff in
      Environ.vars_of_global (Safe_typing.env_of_safe_env senv) gr
  | VarRef _ | IndRef _ | ConstructRef _ -> Environ.vars_of_global env gr

let check_vars env sigma ids c =
  let rec check_rec c =
    match EConstr.destRef sigma c with
    | gr, _ ->
      let vars = vars_of_global env sigma gr in
      Id.Map.iter (fun id _ -> if Id.Set.mem id vars then raise (Depends id)) ids
    | exception DestKO -> EConstr.iter sigma check_rec c
  in
  check_rec c

let rec check_and_clear_in_constr env evdref err ids ~global c =
  (* returns a new constr where all the evars have been 'cleaned'
     (ie the hypotheses ids have been removed from the contexts of
     evars). [global] should be true iff there is some variable of [ids] which
     is a section variable *)
    match EConstr.kind !evdref c with
      | Var id' ->
      if Id.Set.mem id' ids then raise (ClearDependencyError (id', err, None)) else c

      | ( Const _ | Ind _ | Construct _ ) as ref ->
        let () = if global then
          let r = match ref with
          | Const (c, _) -> GlobRef.ConstRef c
          | Ind (ind, _) -> IndRef ind
          | Construct (c, _) -> ConstructRef c
          | _ -> assert false
          in
          let check id' =
            if Id.Set.mem id' ids then
              raise (ClearDependencyError (id',err,Some r))
          in
          Id.Set.iter check (vars_of_global env !evdref r)
        in
        c

      | Evar (evk,l as ev) ->
            (* We check for dependencies to elements of ids in the
               evar_info corresponding to e and in the instance of
               arguments. Concurrently, we build a new evar
               corresponding to e where hypotheses of ids have been
               removed *)
            let evi = Evd.find_undefined !evdref evk in
            let ctxt = Evd.evar_filtered_context evi in
            let rec fold accu ctxt args = match ctxt, SList.view args with
            | [], Some _ | _ :: _, None -> assert false
            | [], None -> accu
            | h :: ctxt, Some (a, args) ->
              let (ri, filter) = fold accu ctxt args in
              try
              (* Check if some id to clear occurs in the instance
                  a of rid in ev and remember the dependency *)
                let check id = if Id.Set.mem id ids then raise (Depends id) in
                let a = match a with
                | None -> Id.Set.singleton (NamedDecl.get_id h)
                | Some a -> collect_vars !evdref a
                in
                let () = Id.Set.iter check a in
              (* Check if some rid to clear in the context of ev
                  has dependencies in another hyp of the context of ev
                  and transitively remember the dependency *)
                let () =
                  if not @@ Id.Map.is_empty ri then
                    NamedDecl.iter_constr (fun c -> check_vars env !evdref ri c) h
                in
              (* No dependency at all, we can keep this ev's context hyp *)
                (ri, true::filter)
              with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter)
            in
            let (rids, filter) = fold (Id.Map.empty, []) ctxt l in

            if Id.Map.is_empty rids then c
            else
              (* Check if some rid to clear in the context of ev has dependencies
               in the type of ev and adjust the source of the dependency *)
              let _nconcl : EConstr.t =
                try
                  let nids = Id.Map.domain rids in
                  let env = evar_filtered_env env evi in
                  let global = Id.Set.exists (is_section_variable_env env) nids in
                  let concl = evar_concl evi in
                  check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids ~global concl
                with ClearDependencyError (rid,err,where) ->
                  raise (ClearDependencyError (Id.Map.find rid rids,err,where))
              in
              let origfilter = Evd.evar_filter evi in
              let filter = Evd.Filter.apply_subfilter origfilter filter in
              let evd = !evdref in
              let candidates = Evd.evar_candidates evi in
              let (evd,_) = restrict_evar evd evk filter candidates in
              evdref := evd;
              Evd.existential_value !evdref ev

      | _ -> EConstr.map !evdref (check_and_clear_in_constr env evdref err ids ~global) c

let clear_hyps_in_evi_main env sigma hyps terms ids =
  (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
     hypothesis does not depend on a element of ids, and erases ids in
     the contexts of the evars occurring in evi *)
  let evdref = ref sigma in
  let global = Id.Set.exists (is_section_variable_env env) ids in
  let terms =
    List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids ~global) terms in
  let nhyps =
    let check_context status decl =
      let decl = EConstr.of_named_decl decl in
      let err = OccurHypInSimpleClause (Some (NamedDecl.get_id decl)) in
      status, EConstr.Unsafe.to_named_decl @@ NamedDecl.map_constr (check_and_clear_in_constr env evdref err ids ~global) decl
    in
    remove_hyps ids check_context hyps
  in
  (!evdref, nhyps, terms)

let check_and_clear_in_constr env evd err ids c =
  let evdref = ref evd in
  let global = Id.Set.exists (is_section_variable_env env) ids in
  let _ : EConstr.constr = check_and_clear_in_constr
      ~global
      env evdref err ids c
  in
  !evdref

let clear_hyps_in_evi env sigma hyps concl ids =
  match clear_hyps_in_evi_main env sigma hyps [concl] ids with
  | (sigma,nhyps,[nconcl]) -> (sigma,nhyps,nconcl)
  | _ -> assert false

let clear_hyps2_in_evi env sigma hyps t concl ids =
  match clear_hyps_in_evi_main env sigma hyps [t;concl] ids with
  | (sigma,nhyps,[t;nconcl]) -> (sigma,nhyps,t,nconcl)
  | _ -> assert false

(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
    the current avatar of [g] (for instance [g] was changed by [clear]
    into [g']). It returns [None] if [g] has been (partially)
    solved. *)
(* spiwack: [advance] is probably performance critical, and the good
   behaviour of its definition may depend sensitively to the actual
   definition of [Evd.find]. Currently, [Evd.find] starts looking for
   a value in the heap of undefined variable, which is small. Hence in
   the most common case, where [advance] is applied to an unsolved
   goal ([advance] is used to figure if a side effect has modified the
   goal) it terminates quickly. *)
let rec advance sigma evk =
  if Evd.is_undefined sigma evk then Some evk
  else
    match is_aliased_evar sigma evk with
    | Some evk -> advance sigma evk
    | None -> None

let reachable_from_evars sigma evars =
  let aliased = Evd.get_aliased_evars sigma in
  let rec search evk visited =
    if Evar.Set.mem evk visited then visited
    else
      let visited = Evar.Set.add evk visited in
      match Evar.Map.find evk aliased with
      | evk' -> search evk' visited
      | exception Not_found -> visited
  in
  Evar.Set.fold (fun evk visited -> search evk visited) evars Evar.Set.empty

(** The following functions return the set of undefined evars
    contained in the object, the defined evars being traversed.
    This is roughly a combination of the previous functions and
    [nf_evar]. *)

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

let undefined_evars_of_named_context evd nc =
  Context.Named.fold_outside
    (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd (EConstr.of_constr c))))
    nc
    ~init:Evar.Set.empty

(* not sure how useful it is to have 2 layers of mutability (mutable field + refs in the map) *)
type undefined_evars_cache = {
  mutable cache : (EConstr.named_declaration * Evar.Set.t) ref Id.Map.t;
}

let create_undefined_evars_cache () = { cache = Id.Map.empty; }

let cached_evar_of_hyp cache sigma decl accu = match cache with
| None ->
  let fold c acc =
    let evs = undefined_evars_of_term sigma c in
    Evar.Set.union evs acc
  in
  NamedDecl.fold_constr fold decl accu
| Some cache ->
  let id = NamedDecl.get_id decl in
  let evs = match Id.Map.find_opt id cache.cache with
    | Some {contents = decl',evs } when NamedDecl.equal (==) (==) decl decl' -> evs
    | None | Some _ as r ->
      let fold c acc =
        let evs = undefined_evars_of_term sigma c in
        Evar.Set.union evs acc
      in
      let evs = NamedDecl.fold_constr fold decl Evar.Set.empty in
      let () = match r with
        | None -> cache.cache <- Id.Map.add id (ref (decl,evs)) cache.cache
        | Some r -> r := (decl,evs)
      in
      evs
  in
  Evar.Set.fold Evar.Set.add evs accu

let filtered_undefined_evars_of_evar_info (type a) ?cache sigma (evi : a evar_info) =
  let evars_of_named_context cache accu nc =
    let fold decl accu = cached_evar_of_hyp cache sigma (EConstr.of_named_decl decl) accu in
    Context.Named.fold_outside fold nc ~init:accu
  in
  let accu = match Evd.evar_body evi with
  | Evar_empty -> undefined_evars_of_term sigma (Evd.evar_concl evi)
  | Evar_defined b -> evars_of_term sigma b
  in
  let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in
  evars_of_named_context cache accu ctxt

(* spiwack: this is a more complete version of
   {!Termops.occur_evar}. The latter does not look recursively into an
   [evar_map]. If unification only need to check superficially, tactics
   do not have this luxury, and need the more complete version. *)
let occur_evar_upto sigma n c =
  let rec occur_rec c = match EConstr.kind sigma c with
    | Evar (evk, _) -> if Evar.equal evk n then raise Occur
    | _ -> EConstr.iter sigma occur_rec c
  in
  try occur_rec c; false with Occur -> true

(* We don't try to guess in which sort the type should be defined, since
   any type has type Type. May cause some trouble, but not so far... *)

let judge_of_new_Type evd =
  let open EConstr in
  let (evd', s) = new_sort_variable univ_rigid evd in
  (evd', { uj_val = mkSort s; uj_type = mkSort (ESorts.super evd s) })

let subterm_source evk ?where (loc,k) =
  let evk = match k with
    | Evar_kinds.SubEvar (None,evk) when where = None -> evk
    | _ -> evk in
  (loc,Evar_kinds.SubEvar (where,evk))

(* Add equality constraints for covariant/invariant positions. For
   irrelevant positions, unify universes when flexible. *)
let compare_cumulative_instances cv_pb variances u u' sigma =
  let open UnivProblem in
  let cstrs = Univ.UnivConstraints.empty in
  let soft = Set.empty in
  let qs, us = UVars.Instance.to_array u
  and qs', us' = UVars.Instance.to_array u' in
  let qcstrs = enforce_eq_qualities qs qs' Set.empty in
  match Evd.add_constraints sigma qcstrs with
  | exception UGraph.UniverseInconsistency p -> Inr p
  | sigma ->
  let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' ->
      let open UVars.Variance in
      match v with
      | Irrelevant -> cstrs, Set.add (UWeak (u,u')) soft
      | Covariant when cv_pb == Conversion.CUMUL ->
        Univ.UnivConstraints.add (u,Univ.UnivConstraint.Le,u') cstrs, soft
      | Covariant | Invariant -> Univ.UnivConstraints.add (u,Univ.UnivConstraint.Eq,u') cstrs, soft)
      (cstrs,soft) variances us us'
  in
  match Evd.add_univ_constraints sigma cstrs with
  | sigma ->
    Inl (Evd.add_constraints sigma soft)
  | exception UGraph.UniverseInconsistency p -> Inr p

let compare_constructor_instances evd u u' =
  let open UnivProblem in
  let qs, us = UVars.Instance.to_array u
  and qs', us' = UVars.Instance.to_array u' in
  let qcstrs = enforce_eq_qualities qs qs' Set.empty in
  match Evd.add_constraints evd qcstrs with
  | exception UGraph.UniverseInconsistency p -> Inr p
  | evd ->
    let soft =
      Array.fold_left2 (fun cs u u' -> Set.add (UWeak (u,u')) cs)
        Set.empty us us'
    in
    Inl (Evd.add_constraints evd soft)

(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of
    [t] and [u] up to existential variable instantiation and
    equal universes. The term [t] is interpreted in [evd] while
    [u] is interpreted in [extended_evd]. The universe constraints in
    [extended_evd] are assumed to be an extension of those in [evd]. *)
let eq_constr_univs_test ~evd ~extended_evd t u =
  (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
  let t = EConstr.Unsafe.to_constr t
  and u = EConstr.Unsafe.to_constr u in
  let eq_universes _ u1 u2 =
    EConstr.EInstance.(equal extended_evd (make u1) (make u2))
  in
  let eq_sorts s1 s2 = EConstr.ESorts.(equal extended_evd (make s1) (make s2)) in
  let eq_existential eq e1 e2 =
    let eq c1 c2 = eq 0 (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
    EConstr.eq_existential evd eq (EConstr.of_existential e1) (EConstr.of_existential e2)
  in
  let kind1 = kind_of_term_upto evd in
  let kind2 = kind_of_term_upto extended_evd in
  let rec eq_constr' nargs m n =
    Constr.compare_head_gen_leq_with kind1 kind2 eq_universes eq_sorts (eq_existential eq_constr') eq_constr' eq_constr' nargs m n
  in
  compare_head_gen_leq_with kind1 kind2 eq_universes eq_sorts (eq_existential eq_constr') eq_constr' eq_constr' 0 t u