<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 Term
open Termops
open Sign
open Environ
open Global
open Declare
open Coqast
open Ast
open Termast
open Libnames
open Extend
open Nametab
open Ppconstr

let emacs_str s = if !Options.print_emacs then s else "" 

(**********************************************************************)
(* Old Ast printing *)

let constr_syntax_universe = "constr"
(* This is starting precedence for printing constructions or tactics *)
(* Level 9 means no parentheses except for applicative terms (at level 10) *)
let constr_initial_prec_v7 = Some (9,Ppextend.L)
let constr_initial_prec = Some (200,Ppextend.E)

let dfltpr ast = (str"#GENTERM " ++ print_ast ast);;

let global_const_name kn =
  try pr_global Idset.empty (ConstRef kn)
  with Not_found -> (* May happen in debug *)
    (str ("CONST("^(string_of_kn kn)^")"))

let global_var_name id =
  try pr_global Idset.empty (VarRef id)
  with Not_found -> (* May happen in debug *)
    (str ("SECVAR("^(string_of_id id)^")"))

let global_ind_name (kn,tyi) =
  try pr_global Idset.empty (IndRef (kn,tyi))
  with Not_found -> (* May happen in debug *)
    (str ("IND("^(string_of_kn kn)^","^(string_of_int tyi)^")"))

let global_constr_name ((kn,tyi),i) =
  try pr_global Idset.empty (ConstructRef ((kn,tyi),i))
  with Not_found -> (* May happen in debug *)
    (str ("CONSTRUCT("^(string_of_kn kn)^","^(string_of_int tyi)
		  ^","^(string_of_int i)^")"))

let globpr gt = match gt with
  | Nvar(_,s) -> (pr_id s)
  | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
  | Node(_,"CONST",[Path(_,sl)]) ->
      global_const_name (section_path sl)
  | Node(_,"SECVAR",[Nvar(_,s)]) ->
      global_var_name s
  | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
      global_ind_name (section_path sl, tyi)
  | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
      global_constr_name ((section_path sl, tyi), i)
  | Dynamic(_,d) ->
    if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>")
    else dfltpr gt
  | gt -> dfltpr gt


let wrap_exception = function
    Anomaly (s1,s2) ->
      warning ("Anomaly ("^s1^")"); pp s2;
      str"<PP error: non-printable term>"
  | Failure _ | UserError _ | Not_found ->
      str"<PP error: non-printable term>"
  | s -> raise s

let gentermpr_fail gt =
  let prec =
    if !Options.v7 then constr_initial_prec_v7 else constr_initial_prec in
  Esyntax.genprint globpr constr_syntax_universe prec gt

let gentermpr gt =
  try gentermpr_fail gt
  with s -> wrap_exception s

(**********************************************************************)
(* Generic printing: choose old or new printers *)

(* [at_top] means ids of env must be avoided in bound variables *)
let gentermpr_core at_top env t =
  if !Options.v7 then gentermpr (Termast.ast_of_constr at_top env t)
  else Ppconstrnew.pr_constr (Constrextern.extern_constr at_top env t)
let pr_cases_pattern t =
  if !Options.v7 then gentermpr (Termast.ast_of_cases_pattern t)
  else Ppconstrnew.pr_cases_pattern
    (Constrextern.extern_cases_pattern Idset.empty t)
let pr_pattern_env tenv env t =
  if !Options.v7 then gentermpr (Termast.ast_of_pattern tenv env t)
  else Ppconstrnew.pr_constr
    (Constrextern.extern_pattern tenv env t)<commit_msg>lconstr pour genterm en v8<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 Term
open Termops
open Sign
open Environ
open Global
open Declare
open Coqast
open Ast
open Termast
open Libnames
open Extend
open Nametab
open Ppconstr

let emacs_str s = if !Options.print_emacs then s else "" 

(**********************************************************************)
(* Old Ast printing *)

let constr_syntax_universe = "constr"
(* This is starting precedence for printing constructions or tactics *)
(* Level 9 means no parentheses except for applicative terms (at level 10) *)
let constr_initial_prec_v7 = Some (9,Ppextend.L)
let constr_initial_prec = Some (200,Ppextend.E)

let dfltpr ast = (str"#GENTERM " ++ print_ast ast);;

let global_const_name kn =
  try pr_global Idset.empty (ConstRef kn)
  with Not_found -> (* May happen in debug *)
    (str ("CONST("^(string_of_kn kn)^")"))

let global_var_name id =
  try pr_global Idset.empty (VarRef id)
  with Not_found -> (* May happen in debug *)
    (str ("SECVAR("^(string_of_id id)^")"))

let global_ind_name (kn,tyi) =
  try pr_global Idset.empty (IndRef (kn,tyi))
  with Not_found -> (* May happen in debug *)
    (str ("IND("^(string_of_kn kn)^","^(string_of_int tyi)^")"))

let global_constr_name ((kn,tyi),i) =
  try pr_global Idset.empty (ConstructRef ((kn,tyi),i))
  with Not_found -> (* May happen in debug *)
    (str ("CONSTRUCT("^(string_of_kn kn)^","^(string_of_int tyi)
		  ^","^(string_of_int i)^")"))

let globpr gt = match gt with
  | Nvar(_,s) -> (pr_id s)
  | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
  | Node(_,"CONST",[Path(_,sl)]) ->
      global_const_name (section_path sl)
  | Node(_,"SECVAR",[Nvar(_,s)]) ->
      global_var_name s
  | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
      global_ind_name (section_path sl, tyi)
  | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
      global_constr_name ((section_path sl, tyi), i)
  | Dynamic(_,d) ->
    if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>")
    else dfltpr gt
  | gt -> dfltpr gt


let wrap_exception = function
    Anomaly (s1,s2) ->
      warning ("Anomaly ("^s1^")"); pp s2;
      str"<PP error: non-printable term>"
  | Failure _ | UserError _ | Not_found ->
      str"<PP error: non-printable term>"
  | s -> raise s

let gentermpr_fail gt =
  let prec =
    if !Options.v7 then constr_initial_prec_v7 else constr_initial_prec in
  Esyntax.genprint globpr constr_syntax_universe prec gt

let gentermpr gt =
  try gentermpr_fail gt
  with s -> wrap_exception s

(**********************************************************************)
(* Generic printing: choose old or new printers *)

(* [at_top] means ids of env must be avoided in bound variables *)
let gentermpr_core at_top env t =
  if !Options.v7 then gentermpr (Termast.ast_of_constr at_top env t)
  else Ppconstrnew.pr_lconstr (Constrextern.extern_constr at_top env t)
let pr_cases_pattern t =
  if !Options.v7 then gentermpr (Termast.ast_of_cases_pattern t)
  else Ppconstrnew.pr_cases_pattern
    (Constrextern.extern_cases_pattern Idset.empty t)
let pr_pattern_env tenv env t =
  if !Options.v7 then gentermpr (Termast.ast_of_pattern tenv env t)
  else Ppconstrnew.pr_constr
    (Constrextern.extern_pattern tenv env t)
{'fraction_non_alphanumeric': 0.209143457698371, 'fraction_numerical': 0.005123489227535471, 'mean_word_length': 4.182437031994554, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 41, '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': '465114', 'n_tokens_mistral': 2658, 'n_tokens_neox': 2578, 'n_words': 717}