<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 Names
open Nameops
open Environ
open Util
open Extend
open Ppextend
open Ppconstrnew
open Tacexpr
open Rawterm
open Topconstr
open Genarg
open Libnames
open Pptactic

let sep_v = fun _ -> str"," ++ spc()

let strip_prod_binders_expr n ty =
  let rec strip_ty acc n ty =
    match ty with
        Topconstr.CProdN(_,bll,a) ->
          let nb =
            List.fold_left (fun i (nal,_) -> i + List.length nal) 0 bll in
          if nb >= n then (List.rev (bll@acc), a)
          else strip_ty (bll@acc) (n-nb) a
      | Topconstr.CArrow(_,a,b) ->
          if n=1 then
            (List.rev (([(dummy_loc,Anonymous)],a)::acc), b)
          else strip_ty (([(dummy_loc,Anonymous)],a)::acc) (n-1) b
      | _ -> error "Cannot translate fix tactic: not enough products" in
  strip_ty [] n ty

(* In v8 syntax only double quote char is escaped by repeating it *)
let rec escape_string_v8 s =
  let rec escape_at s i =
    if i<0 then s
    else if s.[i] == '"' then
      let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
      escape_at s' (i-1)
    else escape_at s (i-1) in
  escape_at s (String.length s - 1)

let qstringnew s = str ("\""^escape_string_v8 s^"\"")
let qsnew = qstringnew

let translate_v7_ltac = function
  | "DiscrR" -> "discrR"
  | "Sup0" -> "prove_sup0"
  | "SupOmega" -> "omega_sup"
  | "Sup" -> "prove_sup"
  | "RCompute" -> "Rcompute"
  | "IntroHypG" -> "intro_hyp_glob"
  | "IntroHypL" -> "intro_hyp_pt"
  | "IsDiff_pt" -> "is_diff_pt"
  | "IsDiff_glob" -> "is_diff_glob"
  | "IsCont_pt" -> "is_cont_pt"
  | "IsCont_glob" -> "is_cont_glob"
  | "RewTerm" -> "rew_term"
  | "ConsProof" -> "deriv_proof"
  | "SimplifyDerive" -> "simplify_derive"
  | "Reg" -> "reg" (* ??? *)
  | "SplitAbs" -> "split_case_Rabs"
  | "SplitAbsolu" -> "split_Rabs"
  | "SplitRmult" -> "split_Rmult"
  | "CaseEqk" -> "case_eq"
  | "SqRing" -> "ring_Rsqr"
  | "TailSimpl" -> "tail_simpl"
  | "CoInduction" -> "coinduction"
  | "ElimCompare" -> "elim_compare"
  | "CCsolve" -> "CCsolve"  (* ?? *)
  | "ArrayAccess" -> "array_access"
  | "MemAssoc" -> "mem_assoc"
  | "SeekVarAux" -> "seek_var_aux"
  | "SeekVar" -> "seek_var"
  | "NumberAux" -> "number_aux"
  | "Number" -> "number"
  | "BuildVarList" -> "build_varlist"
  | "Assoc" -> "assoc"
  | "Remove" -> "remove"
  | "Union" -> "union"
  | "RawGiveMult" -> "raw_give_mult"
  | "GiveMult" -> "give_mult"
  | "ApplyAssoc" -> "apply_assoc"
  | "ApplyDistrib" -> "apply_distrib"
  | "GrepMult" -> "grep_mult"
  | "WeakReduce" -> "weak_reduce"
  | "Multiply" -> "multiply"
  | "ApplyMultiply" -> "apply_multiply"
  | "ApplyInverse" -> "apply_inverse"
  | "StrongFail" -> "strong_fail"
  | "InverseTestAux" -> "inverse_test_aux"
  | "InverseTest" -> "inverse_test"
  | "ApplySimplif" -> "apply_simplif"
  | "Unfolds" -> "unfolds"
  | "Reduce" -> "reduce"
  | "Field_Gen_Aux" -> "field_gen_aux"
  | "Field_Gen" -> "field_gen"
  | "EvalWeakReduce" -> "eval_weak_reduce"
  | "Field_Term" -> "field_term"
  | "Fourier" -> "fourier" (* ou Fourier ?? *)
  | "FourierEq" -> "fourier_eq"
  | "S_to_plus" -> "rewrite_S_to_plus_term"
  | "S_to_plus_eq" -> "rewrite_S_to_plus"
  | "NatRing" -> "ring_nat"
  | "Solve1" -> "solve1"
  | "Solve2" -> "solve2"
  | "Elim_eq_term" -> "elim_eq_term"
  | "Elim_eq_Z" -> "elim_eq_Z"
  | "Elim_eq_pos" -> "elim_eq_pos"
  | "Elim_Zcompare" -> "elim_Zcompare"
  | "ProveStable" -> "prove_stable"
  | "interp_A" -> "interp_A"
  | "InitExp" -> "init_exp"
  | "SimplInv" -> "simpl_inv"
  | "Map" -> "map_tactic"
  | "BuildMonomAux" -> "build_monom_aux"
  | "BuildMonom" -> "build_monom"
  | "SimplMonomAux" -> "simpl_monom_aux"
  | "SimplMonom" -> "simpl_monom"
  | "SimplAllMonoms" -> "simpl_all_monomials"
  | "AssocDistrib" -> "assoc_distrib"
  | "NowShow" -> "now_show"
  | x -> x<commit_msg>Renommage de tactiques ltac coincidant avec certaines tactiques primitives<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 Names
open Nameops
open Environ
open Util
open Extend
open Ppextend
open Ppconstrnew
open Tacexpr
open Rawterm
open Topconstr
open Genarg
open Libnames
open Pptactic

let sep_v = fun _ -> str"," ++ spc()

let strip_prod_binders_expr n ty =
  let rec strip_ty acc n ty =
    match ty with
        Topconstr.CProdN(_,bll,a) ->
          let nb =
            List.fold_left (fun i (nal,_) -> i + List.length nal) 0 bll in
          if nb >= n then (List.rev (bll@acc), a)
          else strip_ty (bll@acc) (n-nb) a
      | Topconstr.CArrow(_,a,b) ->
          if n=1 then
            (List.rev (([(dummy_loc,Anonymous)],a)::acc), b)
          else strip_ty (([(dummy_loc,Anonymous)],a)::acc) (n-1) b
      | _ -> error "Cannot translate fix tactic: not enough products" in
  strip_ty [] n ty

(* In v8 syntax only double quote char is escaped by repeating it *)
let rec escape_string_v8 s =
  let rec escape_at s i =
    if i<0 then s
    else if s.[i] == '"' then
      let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
      escape_at s' (i-1)
    else escape_at s (i-1) in
  escape_at s (String.length s - 1)

let qstringnew s = str ("\""^escape_string_v8 s^"\"")
let qsnew = qstringnew

let translate_v7_ltac = function
  | "DiscrR" -> "discrR"
  | "Sup0" -> "prove_sup0"
  | "SupOmega" -> "omega_sup"
  | "Sup" -> "prove_sup"
  | "RCompute" -> "Rcompute"
  | "IntroHypG" -> "intro_hyp_glob"
  | "IntroHypL" -> "intro_hyp_pt"
  | "IsDiff_pt" -> "is_diff_pt"
  | "IsDiff_glob" -> "is_diff_glob"
  | "IsCont_pt" -> "is_cont_pt"
  | "IsCont_glob" -> "is_cont_glob"
  | "RewTerm" -> "rew_term"
  | "ConsProof" -> "deriv_proof"
  | "SimplifyDerive" -> "simplify_derive"
  | "Reg" -> "reg" (* ??? *)
  | "SplitAbs" -> "split_case_Rabs"
  | "SplitAbsolu" -> "split_Rabs"
  | "SplitRmult" -> "split_Rmult"
  | "CaseEqk" -> "case_eq"
  | "SqRing" -> "ring_Rsqr"
  | "TailSimpl" -> "tail_simpl"
  | "CoInduction" -> "coinduction"
  | "ElimCompare" -> "elim_compare"
  | "CCsolve" -> "CCsolve"  (* ?? *)
  | "ArrayAccess" -> "array_access"
  | "MemAssoc" -> "mem_assoc"
  | "SeekVarAux" -> "seek_var_aux"
  | "SeekVar" -> "seek_var"
  | "NumberAux" -> "number_aux"
  | "Number" -> "number"
  | "BuildVarList" -> "build_varlist"
  | "Assoc" -> "assoc"
  | "Remove" -> "remove"
  | "Union" -> "union"
  | "RawGiveMult" -> "raw_give_mult"
  | "GiveMult" -> "give_mult"
  | "ApplyAssoc" -> "apply_assoc"
  | "ApplyDistrib" -> "apply_distrib"
  | "GrepMult" -> "grep_mult"
  | "WeakReduce" -> "weak_reduce"
  | "Multiply" -> "multiply"
  | "ApplyMultiply" -> "apply_multiply"
  | "ApplyInverse" -> "apply_inverse"
  | "StrongFail" -> "strong_fail"
  | "InverseTestAux" -> "inverse_test_aux"
  | "InverseTest" -> "inverse_test"
  | "ApplySimplif" -> "apply_simplif"
  | "Unfolds" -> "unfolds"
  | "Reduce" -> "reduce"
  | "Field_Gen_Aux" -> "field_gen_aux"
  | "Field_Gen" -> "field_gen"
  | "EvalWeakReduce" -> "eval_weak_reduce"
  | "Field_Term" -> "field_term"
  | "Fourier" -> "fourier" (* ou Fourier ?? *)
  | "FourierEq" -> "fourier_eq"
  | "S_to_plus" -> "rewrite_S_to_plus_term"
  | "S_to_plus_eq" -> "rewrite_S_to_plus"
  | "NatRing" -> "ring_nat"
  | "Solve1" -> "solve1"
  | "Solve2" -> "solve2"
  | "Elim_eq_term" -> "elim_eq_term"
  | "Elim_eq_Z" -> "elim_eq_Z"
  | "Elim_eq_pos" -> "elim_eq_pos"
  | "Elim_Zcompare" -> "elim_Zcompare"
  | "ProveStable" -> "prove_stable"
  | "interp_A" -> "interp_A"
  | "InitExp" -> "init_exp"
  | "SimplInv" -> "simpl_inv"
  | "Map" -> "map_tactic"
  | "BuildMonomAux" -> "build_monom_aux"
  | "BuildMonom" -> "build_monom"
  | "SimplMonomAux" -> "simpl_monom_aux"
  | "SimplMonom" -> "simpl_monom"
  | "SimplAllMonoms" -> "simpl_all_monomials"
  | "AssocDistrib" -> "assoc_distrib"
  | "NowShow" -> "now_show"
  | ("subst"|"simpl"|"elim"|"destruct"|"apply"|"intro" (* ... *)) as x ->
      let x' = x^"_" in
      msgerrnl
      (str ("Warning: '"^
         x^"' is now a primitive tactic; it has been translated to '"^x'^"'"));
      x'
  | x -> x
{'fraction_non_alphanumeric': 0.2187952343836989, 'fraction_numerical': 0.0044538470103551945, 'mean_word_length': 3.1815642458100557, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 170, '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': '3710382', 'n_tokens_mistral': 3733, 'n_tokens_neox': 3598, 'n_words': 728}