<commit_before>(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

open Pp
open Util
open Names
open Nameops
open Univ
open Term
open Termops
open Inductive
open Inductiveops
open Environ
open Reductionops
open Instantiate
open Typeops
open Typing
open Retyping
open Tacmach
open Proof_type
open Logic
open Evar_refiner
open Wcclausenv
open Pattern
open Hipattern
open Tacticals
open Tactics
open Tacinterp
open Tacred
open Vernacinterp
open Coqlib
open Setoid_replace
open Declarations

(* Rewriting tactics *)

(* 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 general_rewrite_bindings lft2rgt (c,l) gl =
  let ctype = pf_type_of gl c in 
  let env = pf_env gl in
  let sigma = project gl in 
  let _,t = splay_prod env sigma ctype in
  match match_with_equation t with
    | None -> 
	if l = []
	then general_s_rewrite lft2rgt c gl
	else error "The term provided does not end with an equation" 
    | Some (hdcncl,_) -> 
        let hdcncls = string_of_inductive hdcncl in 
	let suffix = Indrec.elimination_suffix (elimination_sort_of_goal gl)in
        let elim =
	  if lft2rgt then
            pf_global gl (id_of_string (hdcncls^suffix^"_r"))
          else
	    pf_global gl (id_of_string (hdcncls^suffix))
        in 
	tclNOTSAMEGOAL (general_elim (c,l) (elim,[])) gl
   (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal 
      and did not fail for useless conditional rewritings generating an
      extra condition *)

(* Conditional rewriting, the success of a rewriting is related 
   to the resolution of the conditions by a given tactic *)
let conditional_rewrite lft2rgt tac (c,bl) = 
  tclTHEN_i (general_rewrite_bindings lft2rgt (c,bl))
    (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac)

let general_rewrite lft2rgt c = general_rewrite_bindings lft2rgt (c,[])

let rewriteLR_bindings = general_rewrite_bindings true
let rewriteRL_bindings = general_rewrite_bindings false

let rewriteLR = general_rewrite true
let rewriteRL = general_rewrite false

let dyn_rewriteLR = function
  | [Command com; Bindings binds] -> 
      tactic_com_bind_list rewriteLR_bindings (com,binds)
  | [Constr c; Cbindings binds] -> 
      rewriteLR_bindings (c,binds)
  | _ -> assert false

let dyn_rewriteRL = function
  | [Command com; Bindings binds] -> 
      tactic_com_bind_list rewriteRL_bindings (com,binds)
  | [Constr c; Cbindings binds] -> 
      rewriteRL_bindings (c,binds)
  | _ -> assert false

let dyn_conditional_rewrite lft2rgt = function
  | [(Tacexp tac); (Command com);(Bindings binds)] -> 
      tactic_com_bind_list 
	(conditional_rewrite lft2rgt (Tacinterp.interp tac)) 
	(com,binds)
  | [(Tacexp tac); (Constr c);(Cbindings binds)] -> 
      conditional_rewrite lft2rgt (Tacinterp.interp tac) (c,binds)
  | _ -> assert false
                 
let v_rewriteLR = hide_tactic "RewriteLR" dyn_rewriteLR
let h_rewriteLR_bindings (c,bl) = v_rewriteLR [(Constr c);(Cbindings bl)] 
let h_rewriteLR c = h_rewriteLR_bindings (c,[])

let v_rewriteRL = hide_tactic "RewriteRL" dyn_rewriteRL
let h_rewriteRL_bindings (c,bl) = v_rewriteRL [(Constr c);(Cbindings bl)] 
let h_rewriteRL c = h_rewriteRL_bindings (c,[])
	
let v_conditional_rewriteLR = 
  hide_tactic "CondRewriteLR" (dyn_conditional_rewrite true)
let v_conditional_rewriteRL = 
  hide_tactic "CondRewriteRL" (dyn_conditional_rewrite false)


(* The Rewrite in tactic *)
let general_rewrite_in lft2rgt id (c,l) gl =
  let ctype = pf_type_of gl c in 
  let env = pf_env gl in
  let sigma = project gl in 
  let _,t = splay_prod env sigma ctype in
  match match_with_equation t with
    | None -> (* Do not deal with setoids yet *) 
        error "The term provided does not end with an equation" 
    | Some (hdcncl,_) -> 
        let hdcncls = string_of_inductive hdcncl in 
	let suffix =
          Indrec.elimination_suffix (elimination_sort_of_hyp id gl)in
        let elim =
	  if lft2rgt then
            pf_global gl (id_of_string (hdcncls^suffix))
          else
	    pf_global gl (id_of_string (hdcncls^suffix^"_r"))
        in 
	general_elim_in id (c,l) (elim,[]) gl

let conditional_rewrite_in lft2rgt id tac (c,bl) = 
  tclTHEN_i (general_rewrite_in lft2rgt id (c,bl))
    (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac)


let dyn_rewrite_in lft2rgt = function
  | [Identifier id;(Command com);(Bindings binds)] -> 
      tactic_com_bind_list (general_rewrite_in lft2rgt id) (com,binds)
  | [Identifier id;(Constr c);(Cbindings binds)] -> 
      general_rewrite_in lft2rgt id (c,binds)
  | _ -> assert false
    
let dyn_conditional_rewrite_in lft2rgt = function
  | [(Tacexp tac); Identifier id; (Command com);(Bindings binds)] -> 
      tactic_com_bind_list 
	(conditional_rewrite_in lft2rgt id (Tacinterp.interp tac)) 
	(com,binds)
  | [(Tacexp tac); Identifier id; (Constr c);(Cbindings binds)] -> 
      conditional_rewrite_in lft2rgt id (Tacinterp.interp tac) (c,binds)
  | _ -> assert false

let rewriteLR_in_tac =  hide_tactic "RewriteLRin" (dyn_rewrite_in true)
let rewriteRL_in_tac = hide_tactic "RewriteRLin" (dyn_rewrite_in false)
let v_conditional_rewriteLR_in = 
  hide_tactic "CondRewriteLRin" (dyn_conditional_rewrite_in true) 
let v_conditional_rewriteRL_in = 
  hide_tactic "CondRewriteRLin" (dyn_conditional_rewrite_in false)


(* Replacing tactics *)

(* eq,symeq : equality on Set and its symmetry theorem
   eqt,sym_eqt : equality on Type and its symmetry theorem
   c2 c1 : c1 is to be replaced by c2
   unsafe : If true, do not check that c1 and c2 are convertible
   gl : goal *)

let abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl =<commit_msg>assert failure avec Conditional Rewrite<commit_after>(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

open Pp
open Util
open Names
open Nameops
open Univ
open Term
open Termops
open Inductive
open Inductiveops
open Environ
open Reductionops
open Instantiate
open Typeops
open Typing
open Retyping
open Tacmach
open Proof_type
open Logic
open Evar_refiner
open Wcclausenv
open Pattern
open Hipattern
open Tacticals
open Tactics
open Tacinterp
open Tacred
open Vernacinterp
open Coqlib
open Setoid_replace
open Declarations

(* Rewriting tactics *)

(* 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 general_rewrite_bindings lft2rgt (c,l) gl =
  let ctype = pf_type_of gl c in 
  let env = pf_env gl in
  let sigma = project gl in 
  let _,t = splay_prod env sigma ctype in
  match match_with_equation t with
    | None -> 
	if l = []
	then general_s_rewrite lft2rgt c gl
	else error "The term provided does not end with an equation" 
    | Some (hdcncl,_) -> 
        let hdcncls = string_of_inductive hdcncl in 
	let suffix = Indrec.elimination_suffix (elimination_sort_of_goal gl)in
        let elim =
	  if lft2rgt then
            pf_global gl (id_of_string (hdcncls^suffix^"_r"))
          else
	    pf_global gl (id_of_string (hdcncls^suffix))
        in 
	tclNOTSAMEGOAL (general_elim (c,l) (elim,[])) gl
   (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal 
      and did not fail for useless conditional rewritings generating an
      extra condition *)

(* Conditional rewriting, the success of a rewriting is related 
   to the resolution of the conditions by a given tactic *)
let conditional_rewrite lft2rgt tac (c,bl) = 
  tclTHEN_i (general_rewrite_bindings lft2rgt (c,bl))
    (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac)

let general_rewrite lft2rgt c = general_rewrite_bindings lft2rgt (c,[])

let rewriteLR_bindings = general_rewrite_bindings true
let rewriteRL_bindings = general_rewrite_bindings false

let rewriteLR = general_rewrite true
let rewriteRL = general_rewrite false

let dyn_rewriteLR = function
  | [Command com; Bindings binds] -> 
      tactic_com_bind_list rewriteLR_bindings (com,binds)
  | [Constr c; Cbindings binds] -> 
      rewriteLR_bindings (c,binds)
  | _ -> assert false

let dyn_rewriteRL = function
  | [Command com; Bindings binds] -> 
      tactic_com_bind_list rewriteRL_bindings (com,binds)
  | [Constr c; Cbindings binds] -> 
      rewriteRL_bindings (c,binds)
  | _ -> assert false

let dyn_conditional_rewrite lft2rgt = function
  | [(Tacexp tac); (Command com);(Bindings binds)] -> 
      tactic_com_bind_list 
	(conditional_rewrite lft2rgt (Tacinterp.interp tac)) 
	(com,binds)
  | [(Tac (tac,_)); (Constr c);(Cbindings binds)] -> 
      conditional_rewrite lft2rgt tac (c,binds)
  | _ -> assert false
                 
let v_rewriteLR = hide_tactic "RewriteLR" dyn_rewriteLR
let h_rewriteLR_bindings (c,bl) = v_rewriteLR [(Constr c);(Cbindings bl)] 
let h_rewriteLR c = h_rewriteLR_bindings (c,[])

let v_rewriteRL = hide_tactic "RewriteRL" dyn_rewriteRL
let h_rewriteRL_bindings (c,bl) = v_rewriteRL [(Constr c);(Cbindings bl)] 
let h_rewriteRL c = h_rewriteRL_bindings (c,[])
	
let v_conditional_rewriteLR = 
  hide_tactic "CondRewriteLR" (dyn_conditional_rewrite true)
let v_conditional_rewriteRL = 
  hide_tactic "CondRewriteRL" (dyn_conditional_rewrite false)


(* The Rewrite in tactic *)
let general_rewrite_in lft2rgt id (c,l) gl =
  let ctype = pf_type_of gl c in 
  let env = pf_env gl in
  let sigma = project gl in 
  let _,t = splay_prod env sigma ctype in
  match match_with_equation t with
    | None -> (* Do not deal with setoids yet *) 
        error "The term provided does not end with an equation" 
    | Some (hdcncl,_) -> 
        let hdcncls = string_of_inductive hdcncl in 
	let suffix =
          Indrec.elimination_suffix (elimination_sort_of_hyp id gl)in
        let elim =
	  if lft2rgt then
            pf_global gl (id_of_string (hdcncls^suffix))
          else
	    pf_global gl (id_of_string (hdcncls^suffix^"_r"))
        in 
	general_elim_in id (c,l) (elim,[]) gl

let conditional_rewrite_in lft2rgt id tac (c,bl) = 
  tclTHEN_i (general_rewrite_in lft2rgt id (c,bl))
    (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac)


let dyn_rewrite_in lft2rgt = function
  | [Identifier id;(Command com);(Bindings binds)] -> 
      tactic_com_bind_list (general_rewrite_in lft2rgt id) (com,binds)
  | [Identifier id;(Constr c);(Cbindings binds)] -> 
      general_rewrite_in lft2rgt id (c,binds)
  | _ -> assert false
    
let dyn_conditional_rewrite_in lft2rgt = function
  | [(Tacexp tac); Identifier id; (Command com);(Bindings binds)] -> 
      tactic_com_bind_list 
	(conditional_rewrite_in lft2rgt id (Tacinterp.interp tac)) 
	(com,binds)
  | [(Tac (tac,_)); Identifier id; (Constr c);(Cbindings binds)] -> 
      conditional_rewrite_in lft2rgt id tac (c,binds)
  | _ -> assert false

let rewriteLR_in_tac =  hide_tactic "RewriteLRin" (dyn_rewrite_in true)
let rewriteRL_in_tac = hide_tactic "RewriteRLin" (dyn_rewrite_in false)
let v_conditional_rewriteLR_in = 
  hide_tactic "CondRewriteLRin" (dyn_conditional_rewrite_in true) 
let v_conditional_rewriteRL_in = 
  hide_tactic "CondRewriteRLin" (dyn_conditional_rewrite_in false)


(* Replacing tactics *)

(* eq,symeq : equality on Set and its symmetry theorem
   eqt,sym_eqt : equality on Type and its symmetry theorem
   c2 c1 : c1 is to be replaced by c2
   unsafe : If true, do not check that c1 and c2 are convertible
   gl : goal *)

let abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl =
{'fraction_non_alphanumeric': 0.111997497262631, 'fraction_numerical': 0.005787580165806351, 'mean_word_length': 3.860129228430255, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 57, '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': '876616', 'n_tokens_mistral': 4770, 'n_tokens_neox': 4424, 'n_words': 1302}