<commit_before>open Util
open Names
open Nameops
open Context
open Constr
open Globnames
open Pp
open List
open Libnames
open Tactics
open Tacticals
open Tacmach
open Proofview.Notations
open EConstr
open Equations_common
open Printer
open Ppconstr

open Syntax
open Context_map
open Splitting
open Covering
open Vars

open Cc_plugin.Cctac

type where_map = (constr * Names.Id.t * splitting) PathMap.t

type equations_info = {
 equations_id : Names.Id.t;
 equations_where_map : where_map;
 equations_f : EConstr.t;
 equations_prob : Context_map.context_map }

type ind_info = {
  term_info : term_info;
  pathmap : (Names.Id.t * Constr.t list) PathMap.t; (* path -> inductive name *)
  wheremap : where_map }

   
let find_helper_info env sigma info f =
  try List.find (fun (cst, arg') ->
         try Environ.QConstant.equal env cst (fst (destConst sigma f))
         with DestKO -> false)
	info.helpers_info
  with Not_found -> anomaly (str"Helper not found while proving induction lemma.")

let below_transparent_state () =
  Hints.Hint_db.transparent_state (Hints.searchtable_map "Below")

let simpl_star =
  tclTHEN simpl_in_concl (onAllHyps (fun id -> simpl_in_hyp (id, Locus.InHyp)))

let eauto_with_below ?depth ?(strategy=Class_tactics.Dfs) l =
  Class_tactics.typeclasses_eauto ~depth ~st:(below_transparent_state ()) 
    ~strategy (l@["subterm_relation"; "Below"; "rec_decision"])
    
let wf_obligations_base info =
  info.base_id ^ "_wf_obligations"

let simp_eqns l =
  tclREPEAT
    (tclTHENLIST [Autorewrite.autorewrite tclIDTAC l; tclTRY (eauto_with_below l)])

let simp_eqns_in clause l =
  tclREPEAT (tclTHENLIST 
		[Autorewrite.auto_multi_rewrite l clause;
		 tclTRY (eauto_with_below l)])

let autorewrites b = 
  tclREPEAT (Autorewrite.autorewrite tclIDTAC [b])

exception RewriteSucceeded of EConstr.t

let _rewrite_try_change tac = 
  Proofview.Goal.enter (fun gl ->
    let concl = Proofview.Goal.concl gl in
    Proofview.tclORELSE 
      (Proofview.tclTHEN tac 
      (Proofview.Goal.enter (fun gl ->
          let env = Proofview.Goal.env gl in
          let sigma = Proofview.Goal.sigma gl in
          let concl' = Proofview.Goal.concl gl in
          match Reductionops.infer_conv ~pb:Reduction.CONV env sigma concl concl' with
          | Some _ -> Proofview.tclZERO (RewriteSucceeded concl')
          | None -> Proofview.tclUNIT ())))
    (function
      | (RewriteSucceeded concl', _) -> convert_concl ~cast:true ~check:false concl' DEFAULTcast
      | (exn, info) -> Proofview.tclZERO ~info exn))

let autorewrite_one b =
  let rew_rules = Autorewrite.find_rewrites b in
  let rec aux rules =
    match rules with
    | [] -> tclFAIL (str"Couldn't rewrite")
    | r :: rules ->
       let global, _univs = Constr.destRef r.Autorewrite.rew_lemma in
       let tac =
         Proofview.tclBIND
         (pf_constr_of_global global)
         (if r.Autorewrite.rew_l2r then Equality.rewriteLR else Equality.rewriteRL)
       in
       Proofview.tclOR tac
         (fun e -> if !debug then Feedback.msg_debug (str"failed"); aux rules)
  in aux rew_rules

let revert_last =
  Proofview.Goal.enter (fun gl ->
      let hyp = pf_last_hyp gl in<commit_msg>Adapt w.r.t. coq/coq#16337.<commit_after>open Util
open Names
open Nameops
open Context
open Constr
open Globnames
open Pp
open List
open Libnames
open Tactics
open Tacticals
open Tacmach
open Proofview.Notations
open EConstr
open Equations_common
open Printer
open Ppconstr

open Syntax
open Context_map
open Splitting
open Covering
open Vars

open Cc_plugin.Cctac

type where_map = (constr * Names.Id.t * splitting) PathMap.t

type equations_info = {
 equations_id : Names.Id.t;
 equations_where_map : where_map;
 equations_f : EConstr.t;
 equations_prob : Context_map.context_map }

type ind_info = {
  term_info : term_info;
  pathmap : (Names.Id.t * Constr.t list) PathMap.t; (* path -> inductive name *)
  wheremap : where_map }

   
let find_helper_info env sigma info f =
  try List.find (fun (cst, arg') ->
         try Environ.QConstant.equal env cst (fst (destConst sigma f))
         with DestKO -> false)
	info.helpers_info
  with Not_found -> anomaly (str"Helper not found while proving induction lemma.")

let below_transparent_state () =
  Hints.Hint_db.transparent_state (Hints.searchtable_map "Below")

let simpl_star =
  tclTHEN simpl_in_concl (onAllHyps (fun id -> simpl_in_hyp (id, Locus.InHyp)))

let eauto_with_below ?depth ?(strategy=Class_tactics.Dfs) l =
  Class_tactics.typeclasses_eauto ~depth ~st:(below_transparent_state ()) 
    ~strategy (l@["subterm_relation"; "Below"; "rec_decision"])
    
let wf_obligations_base info =
  info.base_id ^ "_wf_obligations"

let simp_eqns l =
  tclREPEAT
    (tclTHENLIST [Autorewrite.autorewrite tclIDTAC l; tclTRY (eauto_with_below l)])

let simp_eqns_in clause l =
  tclREPEAT (tclTHENLIST 
		[Autorewrite.auto_multi_rewrite l clause;
		 tclTRY (eauto_with_below l)])

let autorewrites b = 
  tclREPEAT (Autorewrite.autorewrite tclIDTAC [b])

exception RewriteSucceeded of EConstr.t

let _rewrite_try_change tac = 
  Proofview.Goal.enter (fun gl ->
    let concl = Proofview.Goal.concl gl in
    Proofview.tclORELSE 
      (Proofview.tclTHEN tac 
      (Proofview.Goal.enter (fun gl ->
          let env = Proofview.Goal.env gl in
          let sigma = Proofview.Goal.sigma gl in
          let concl' = Proofview.Goal.concl gl in
          match Reductionops.infer_conv ~pb:Reduction.CONV env sigma concl concl' with
          | Some _ -> Proofview.tclZERO (RewriteSucceeded concl')
          | None -> Proofview.tclUNIT ())))
    (function
      | (RewriteSucceeded concl', _) -> convert_concl ~cast:true ~check:false concl' DEFAULTcast
      | (exn, info) -> Proofview.tclZERO ~info exn))

let autorewrite_one b =
  let rew_rules = Autorewrite.find_rewrites b in
  let rec aux rules =
    match rules with
    | [] -> tclFAIL (str"Couldn't rewrite")
    | r :: rules ->
       let global, _univs = Constr.destRef (snd @@ Autorewrite.RewRule.rew_lemma r) in
       let tac =
         Proofview.tclBIND
         (pf_constr_of_global global)
         (if (Autorewrite.RewRule.rew_l2r r) then Equality.rewriteLR else Equality.rewriteRL)
       in
       Proofview.tclOR tac
         (fun e -> if !debug then Feedback.msg_debug (str"failed"); aux rules)
  in aux rew_rules

let revert_last =
  Proofview.Goal.enter (fun gl ->
      let hyp = pf_last_hyp gl in
{'fraction_non_alphanumeric': 0.08890968647636874, 'fraction_numerical': 0.0010918733426922478, 'mean_word_length': 3.4281767955801103, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 33, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '85846', 'n_tokens_mistral': 2414, 'n_tokens_neox': 2279, 'n_words': 596}