<commit_before>(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq 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)         *)
(************************************************************************)

module CVars = Vars
open Pp
open CErrors
open Util
open Names
open Nameops
open Term
open Constr
open Context
open Termops
open EConstr
open Vars
open Namegen
open Inductive
open Inductiveops
open Libnames
open Globnames
open Reductionops
open Typing
open Retyping
open Tacmach.New
open Logic
open Hipattern
open Tacticals.New
open Tactics
open Tacred
open Coqlib
open Declarations
open Indrec
open Clenv
open Ind_tables
open Eqschemes
open Locus
open Locusops
open Tactypes
open Proofview.Notations
open Unification
open Context.Named.Declaration

module NamedDecl = Context.Named.Declaration

(* Options *)

type inj_flags = {
    keep_proof_equalities : bool;
    injection_in_context : bool;
    injection_pattern_l2r_order : bool;
  }

open Goptions

let use_injection_pattern_l2r_order = function
  | None -> true
  | Some flags -> flags.injection_pattern_l2r_order

let injection_in_context = ref false

let use_injection_in_context = function
  | None -> !injection_in_context
  | Some flags -> flags.injection_in_context

let () =
  declare_bool_option
    { optdepr  = false;
      optkey   = ["Structural";"Injection"];
      optread  = (fun () -> !injection_in_context) ;
      optwrite = (fun b -> injection_in_context := b) }

(* Rewriting tactics *)

type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
type freeze_evars_flag = bool (* true = don't instantiate existing evars *)

type orientation = bool

type conditions =
  | Naive (* Only try the first occurrence of the lemma (default) *)
  | FirstSolved (* Use the first match whose side-conditions are solved *)
  | AllMatches (* Rewrite all matches whose side-conditions are solved *)

(* Warning : rewriting from left to right only works
   if there exists in the context a theorem named <eqname>_<suffsort>_r
   with type (A:<sort>)(x:A)(P:A->Prop)(P x)->(y:A)(eqname A y x)->(P y).
   If another equality myeq is introduced, then corresponding theorems
   myeq_ind_r, myeq_rec_r and myeq_rect_r have to be proven. See below.
   -- Eduardo (19/8/97)
*)

let rewrite_core_unif_flags = {
  modulo_conv_on_closed_terms = None;
  use_metas_eagerly_in_conv_on_closed_terms = true;
  use_evars_eagerly_in_conv_on_closed_terms = false;
  modulo_delta = TransparentState.empty;
  modulo_delta_types = TransparentState.empty;
  check_applied_meta_types = true;
  use_pattern_unification = true;
  use_meta_bound_pattern_unification = true;
  allowed_evars = Evarsolve.AllowedEvars.all;
  restrict_conv_on_strict_subterms = false;
  modulo_betaiota = false;
  modulo_eta = true;
}

let rewrite_unif_flags = {
  core_unify_flags = rewrite_core_unif_flags;
  merge_unify_flags = rewrite_core_unif_flags;
  subterm_unify_flags = rewrite_core_unif_flags;
  allow_K_in_toplevel_higher_order_unification = false;
    (* allow_K does not matter in practice because calls w_typed_unify *)
  resolve_evars = true
}

let freeze_initial_evars sigma flags clause =
  (* We take evars of the type: this may include old evars! For excluding *)
  (* all old evars, including the ones occurring in the rewriting lemma, *)
  (* we would have to take the clenv_value *)
  let newevars = lazy (Evarutil.undefined_evars_of_term sigma (clenv_type clause)) in
  let initial = Evd.undefined_map sigma in
  let allowed evk =
    if Evar.Map.mem evk initial then false
    else Evar.Set.mem evk (Lazy.force newevars)
  in
  let allowed_evars = Evarsolve.AllowedEvars.from_pred allowed in
  {flags with
    core_unify_flags = {flags.core_unify_flags with allowed_evars};
    merge_unify_flags = {flags.merge_unify_flags with allowed_evars};
    subterm_unify_flags = {flags.subterm_unify_flags with allowed_evars}}

let make_flags frzevars sigma flags clause =
  if frzevars then freeze_initial_evars sigma flags clause else flags

let side_tac tac sidetac =
  match sidetac with
  | None -> tac
  | Some sidetac -> tclTHENSFIRSTn tac [|Proofview.tclUNIT ()|] sidetac

let instantiate_lemma_all frzevars gl c ty l l2r concl =
  let env = Proofview.Goal.env gl in
  let sigma = project gl in
  let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
  let (equiv, args) = decompose_app_vect sigma (Clenv.clenv_type eqclause) in
  let arglen = Array.length args in
  let () = if arglen < 2 then user_err Pp.(str "The term provided is not an applied relation.") in
  let c1 = args.(arglen - 2) in
  let c2 = args.(arglen - 1) in
  let try_occ (evd', c') =
    let clenv = Clenv.update_clenv_evd eqclause evd' in
    Clenv.clenv_pose_dependent_evars ~with_evars:true clenv
  in
  let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
  let occs =
    w_unify_to_subterm_all ~flags env eqclause.evd
      ((if l2r then c1 else c2),concl)
  in List.map try_occ occs

let instantiate_lemma gl c ty l l2r concl =
  let sigma, ct = pf_type_of gl c in<commit_msg>Do not retype the argument of Equality.instantiate_lemma.<commit_after>(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq 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)         *)
(************************************************************************)

module CVars = Vars
open Pp
open CErrors
open Util
open Names
open Nameops
open Term
open Constr
open Context
open Termops
open EConstr
open Vars
open Namegen
open Inductive
open Inductiveops
open Libnames
open Globnames
open Reductionops
open Typing
open Retyping
open Tacmach.New
open Logic
open Hipattern
open Tacticals.New
open Tactics
open Tacred
open Coqlib
open Declarations
open Indrec
open Clenv
open Ind_tables
open Eqschemes
open Locus
open Locusops
open Tactypes
open Proofview.Notations
open Unification
open Context.Named.Declaration

module NamedDecl = Context.Named.Declaration

(* Options *)

type inj_flags = {
    keep_proof_equalities : bool;
    injection_in_context : bool;
    injection_pattern_l2r_order : bool;
  }

open Goptions

let use_injection_pattern_l2r_order = function
  | None -> true
  | Some flags -> flags.injection_pattern_l2r_order

let injection_in_context = ref false

let use_injection_in_context = function
  | None -> !injection_in_context
  | Some flags -> flags.injection_in_context

let () =
  declare_bool_option
    { optdepr  = false;
      optkey   = ["Structural";"Injection"];
      optread  = (fun () -> !injection_in_context) ;
      optwrite = (fun b -> injection_in_context := b) }

(* Rewriting tactics *)

type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
type freeze_evars_flag = bool (* true = don't instantiate existing evars *)

type orientation = bool

type conditions =
  | Naive (* Only try the first occurrence of the lemma (default) *)
  | FirstSolved (* Use the first match whose side-conditions are solved *)
  | AllMatches (* Rewrite all matches whose side-conditions are solved *)

(* Warning : rewriting from left to right only works
   if there exists in the context a theorem named <eqname>_<suffsort>_r
   with type (A:<sort>)(x:A)(P:A->Prop)(P x)->(y:A)(eqname A y x)->(P y).
   If another equality myeq is introduced, then corresponding theorems
   myeq_ind_r, myeq_rec_r and myeq_rect_r have to be proven. See below.
   -- Eduardo (19/8/97)
*)

let rewrite_core_unif_flags = {
  modulo_conv_on_closed_terms = None;
  use_metas_eagerly_in_conv_on_closed_terms = true;
  use_evars_eagerly_in_conv_on_closed_terms = false;
  modulo_delta = TransparentState.empty;
  modulo_delta_types = TransparentState.empty;
  check_applied_meta_types = true;
  use_pattern_unification = true;
  use_meta_bound_pattern_unification = true;
  allowed_evars = Evarsolve.AllowedEvars.all;
  restrict_conv_on_strict_subterms = false;
  modulo_betaiota = false;
  modulo_eta = true;
}

let rewrite_unif_flags = {
  core_unify_flags = rewrite_core_unif_flags;
  merge_unify_flags = rewrite_core_unif_flags;
  subterm_unify_flags = rewrite_core_unif_flags;
  allow_K_in_toplevel_higher_order_unification = false;
    (* allow_K does not matter in practice because calls w_typed_unify *)
  resolve_evars = true
}

let freeze_initial_evars sigma flags clause =
  (* We take evars of the type: this may include old evars! For excluding *)
  (* all old evars, including the ones occurring in the rewriting lemma, *)
  (* we would have to take the clenv_value *)
  let newevars = lazy (Evarutil.undefined_evars_of_term sigma (clenv_type clause)) in
  let initial = Evd.undefined_map sigma in
  let allowed evk =
    if Evar.Map.mem evk initial then false
    else Evar.Set.mem evk (Lazy.force newevars)
  in
  let allowed_evars = Evarsolve.AllowedEvars.from_pred allowed in
  {flags with
    core_unify_flags = {flags.core_unify_flags with allowed_evars};
    merge_unify_flags = {flags.merge_unify_flags with allowed_evars};
    subterm_unify_flags = {flags.subterm_unify_flags with allowed_evars}}

let make_flags frzevars sigma flags clause =
  if frzevars then freeze_initial_evars sigma flags clause else flags

let side_tac tac sidetac =
  match sidetac with
  | None -> tac
  | Some sidetac -> tclTHENSFIRSTn tac [|Proofview.tclUNIT ()|] sidetac

let instantiate_lemma_all frzevars gl c ty l l2r concl =
  let env = Proofview.Goal.env gl in
  let sigma = project gl in
  let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
  let (equiv, args) = decompose_app_vect sigma (Clenv.clenv_type eqclause) in
  let arglen = Array.length args in
  let () = if arglen < 2 then user_err Pp.(str "The term provided is not an applied relation.") in
  let c1 = args.(arglen - 2) in
  let c2 = args.(arglen - 1) in
  let try_occ (evd', c') =
    let clenv = Clenv.update_clenv_evd eqclause evd' in
    Clenv.clenv_pose_dependent_evars ~with_evars:true clenv
  in
  let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
  let occs =
    w_unify_to_subterm_all ~flags env eqclause.evd
      ((if l2r then c1 else c2),concl)
  in List.map try_occ occs

let instantiate_lemma gl c ct l l2r concl =
  let sigma = Proofview.Goal.sigma gl in
{'fraction_non_alphanumeric': 0.1078096947935368, 'fraction_numerical': 0.003590664272890485, 'mean_word_length': 4.075626423690205, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 31, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '191918', 'n_tokens_mistral': 3738, 'n_tokens_neox': 3597, 'n_words': 1109}