<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 Util
open Extend
open Tacexpr
open Rawterm
open Topconstr
open Genarg
open Libnames
open Pattern

let pr_red_expr = Ppconstr.pr_red_expr
let pr_may_eval = Ppconstr.pr_may_eval
let pr_sort = Ppconstr.pr_sort
let pr_global = Ppconstr.pr_global Idset.empty
let pr_name = Ppconstr.pr_name
let pr_opt = Ppconstr.pr_opt
let pr_occurrences = Ppconstr.pr_occurrences

type grammar_terminals = string option list

  (* Extensions *)
let prtac_tab_v7 = Hashtbl.create 17
let prtac_tab = Hashtbl.create 17

let declare_extra_tactic_pprule for_v8 s (tags,prods) =
  Hashtbl.add prtac_tab_v7 (s,tags) prods;
  if for_v8 then Hashtbl.add prtac_tab (s,tags) prods

type 'a raw_extra_genarg_printer =
    (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) ->
      'a -> std_ppcmds
type 'a glob_extra_genarg_printer =
    (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) ->
      'a -> std_ppcmds
type 'a extra_genarg_printer =
    (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) ->
      'a -> std_ppcmds

let genarg_pprule_v7 = ref Stringmap.empty
let genarg_pprule = ref Stringmap.empty

let declare_extra_genarg_pprule for_v8 (rawwit, f) (globwit, g) (wit, h) =
  let s = match unquote wit with
    | ExtraArgType s -> s 
    | _ -> error
	"Can declare a pretty-printing rule only for extra argument types"
  in
  let f prc prtac x = f prc prtac (out_gen rawwit x) in
  let g prc prtac x = g prc prtac (out_gen globwit x) in
  let h prc prtac x = h prc prtac (out_gen wit x) in
  genarg_pprule_v7 := Stringmap.add s (f,g,h) !genarg_pprule_v7;
  if for_v8 then
    genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule 

let pi1 (a,_,_) = a
let pi2 (_,a,_) = a
let pi3 (_,_,a) = a

let pr_arg pr x = spc () ++ pr x

let pr_or_var pr = function
  | ArgArg x -> pr x
  | ArgVar (_,s) -> pr_id s

let pr_or_metaid pr = function
  | AI x -> pr x
  | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable"

let pr_and_short_name pr (c,_) = pr c

let pr_located pr (loc,x) = pr x

let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp)

let pr_evaluable_reference = function 
  | EvalVarRef id -> pr_id id
  | EvalConstRef sp -> pr_global (Libnames.ConstRef sp)

let pr_inductive ind = pr_global (Libnames.IndRef ind)

let pr_quantified_hypothesis = function
  | AnonHyp n -> int n
  | NamedHyp id -> pr_id id 

let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h

let pr_binding prc = function
  | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
  | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)

let pr_bindings prc prlc = function
  | ImplicitBindings l ->
      brk (1,1) ++ str "with" ++ brk (1,1) ++
      prlist_with_sep spc prc l
  | ExplicitBindings l ->
      brk (1,1) ++ str "with" ++ brk (1,1) ++ 
        prlist_with_sep spc
          (fun b -> if Options.do_translate () or not !Options.v7 then
	    str"(" ++ pr_binding prlc b ++ str")" 
	   else
	    pr_binding prc b)
        l
  | NoBindings -> mt ()

let pr_with_bindings prc prlc (c,bl) = 
  prc c ++ hv 0 (pr_bindings prc prlc bl)

let pr_with_constr prc = function
  | None -> mt ()
  | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)

let rec pr_intro_pattern = function
  | IntroOrAndPattern pll -> pr_case_intro_pattern pll
  | IntroWildcard -> str "_"
  | IntroIdentifier id -> pr_id id

and pr_case_intro_pattern pll =
  str "[" ++
  hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
  ++ str "]"
<commit_msg>Traduction des noms pour les refs de pr_glob_generic (via pr_global)<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 Util
open Extend
open Tacexpr
open Rawterm
open Topconstr
open Genarg
open Libnames
open Pattern

let pr_red_expr = Ppconstr.pr_red_expr
let pr_may_eval = Ppconstr.pr_may_eval
let pr_sort = Ppconstr.pr_sort
let pr_global x =
  if Options.do_translate () then (* for pr_gen *)
    Ppconstrnew.pr_global Idset.empty x
  else
    Ppconstr.pr_global Idset.empty x
let pr_name = Ppconstr.pr_name
let pr_opt = Ppconstr.pr_opt
let pr_occurrences = Ppconstr.pr_occurrences

type grammar_terminals = string option list

  (* Extensions *)
let prtac_tab_v7 = Hashtbl.create 17
let prtac_tab = Hashtbl.create 17

let declare_extra_tactic_pprule for_v8 s (tags,prods) =
  Hashtbl.add prtac_tab_v7 (s,tags) prods;
  if for_v8 then Hashtbl.add prtac_tab (s,tags) prods

type 'a raw_extra_genarg_printer =
    (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) ->
      'a -> std_ppcmds
type 'a glob_extra_genarg_printer =
    (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) ->
      'a -> std_ppcmds
type 'a extra_genarg_printer =
    (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) ->
      'a -> std_ppcmds

let genarg_pprule_v7 = ref Stringmap.empty
let genarg_pprule = ref Stringmap.empty

let declare_extra_genarg_pprule for_v8 (rawwit, f) (globwit, g) (wit, h) =
  let s = match unquote wit with
    | ExtraArgType s -> s 
    | _ -> error
	"Can declare a pretty-printing rule only for extra argument types"
  in
  let f prc prtac x = f prc prtac (out_gen rawwit x) in
  let g prc prtac x = g prc prtac (out_gen globwit x) in
  let h prc prtac x = h prc prtac (out_gen wit x) in
  genarg_pprule_v7 := Stringmap.add s (f,g,h) !genarg_pprule_v7;
  if for_v8 then
    genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule 

let pr_arg pr x = spc () ++ pr x

let pr_or_var pr = function
  | ArgArg x -> pr x
  | ArgVar (_,s) -> pr_id s

let pr_or_metaid pr = function
  | AI x -> pr x
  | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable"

let pr_and_short_name pr (c,_) = pr c

let pr_located pr (loc,x) = pr x

let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp)

let pr_evaluable_reference = function 
  | EvalVarRef id -> pr_id id
  | EvalConstRef sp -> pr_global (Libnames.ConstRef sp)

let pr_inductive ind = pr_global (Libnames.IndRef ind)

let pr_quantified_hypothesis = function
  | AnonHyp n -> int n
  | NamedHyp id -> pr_id id 

let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h

let pr_binding prc = function
  | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
  | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)

let pr_bindings prc prlc = function
  | ImplicitBindings l ->
      brk (1,1) ++ str "with" ++ brk (1,1) ++
      prlist_with_sep spc prc l
  | ExplicitBindings l ->
      brk (1,1) ++ str "with" ++ brk (1,1) ++ 
        prlist_with_sep spc
          (fun b -> if Options.do_translate () or not !Options.v7 then
	    str"(" ++ pr_binding prlc b ++ str")" 
	   else
	    pr_binding prc b)
        l
  | NoBindings -> mt ()

let pr_with_bindings prc prlc (c,bl) =
  prc c ++ hv 0 (pr_bindings prc prlc bl)

let pr_with_constr prc = function
  | None -> mt ()
  | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)

let rec pr_intro_pattern = function
  | IntroOrAndPattern pll -> pr_case_intro_pattern pll
  | IntroWildcard -> str "_"
  | IntroIdentifier id -> pr_id id

and pr_case_intro_pattern pll =
  str "[" ++
  hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
  ++ str "]"

{'fraction_non_alphanumeric': 0.14901492537313432, 'fraction_numerical': 0.007283582089552239, 'mean_word_length': 3.3625, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 75, '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': '3056065', 'n_tokens_mistral': 3272, 'n_tokens_neox': 3165, 'n_words': 902}