(************************************************************************)
(*         *      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 Locus
open Evd
open Pretype_errors
open Environ
open EConstr

(** Finding subterms, possibly up to some unification function,
    possibly at some given occurrences *)

exception SubtermUnificationError of subterm_unification_error

(** A testing function is typically a unification function returning a
    substitution or failing with Error, together with a function to merge
    substitutions and an initial substitution;
    last_found is used for error messages and it has to be initialized
    with None. *)

type ('a, 'b) testing_function = {
  match_fun : int -> 'a -> constr -> ('b, unit) Result.t;
  merge_fun : 'b -> 'a -> ('a, unit) Result.t;
  mutable testing_state : 'a;
  mutable last_found : position_reporting option
}

(** This is the basic testing function, looking for exact matches of a
    closed term *)
val make_eq_univs_test : env -> evar_map -> constr -> (evar_map, evar_map) testing_function

(** [replace_term_occ_modulo occl test mk c] looks in [c] for subterm
    modulo a testing function [test] and replaces successfully
    matching subterms at the indicated occurrences [occl] with [mk
    ()]; it turns an Error value returned by the [merge_fun]
    function into a SubtermUnificationError. *)
val replace_term_occ_modulo : env -> evar_map -> occurrences or_like_first ->
  ('a, 'b) testing_function -> (unit -> constr) -> constr -> constr

(** [replace_term_occ_decl_modulo] is similar to
    [replace_term_occ_modulo] but for a named_declaration. *)
val replace_term_occ_decl_modulo :
  env -> evar_map ->
  (occurrences * hyp_location_flag) or_like_first ->
  ('a, 'b) testing_function -> (unit -> constr) ->
  named_declaration -> named_declaration

(** [subst_closed_term_occ occl c d] replaces occurrences of
    closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
    unifying universes which results in a set of constraints. *)
val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
  constr -> constr -> constr * evar_map

(** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of
    closed [c] at positions [occl] by [Rel 1] in [decl]. *)
val subst_closed_term_occ_decl : env -> evar_map ->
  (occurrences * hyp_location_flag) or_like_first ->
  constr -> named_declaration -> named_declaration * evar_map