<commit_before>
(* $Id$ *)

open Pp
open Util
open Names
open Term
open Sign
open Environ
open Global
open Declare
open Coqast
open Termast

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

let dfltpr ast = [< 'sTR"#GENTERM " ; Ast.print_ast ast >];;

let section_path sl s =
  let sl = List.rev sl in
  make_path (List.tl sl) (id_of_string (List.hd sl)) (kind_of_string s)

(*
let pr_global k oper =
  let id = id_of_global oper in
  [< 'sTR (string_of_id id) >]
*)

let pr_qualified_path sp id =
  if Nametab.sp_of_id (kind_of_path sp) id = sp then [<'sTR(string_of_id id)>]
  else [<'sTR(string_of_path (make_path (dirpath sp) id (kind_of_path sp)))>]

let globpr gt = match gt with
  | Nvar(_,s) -> [< 'sTR s >]
  | Node(_,"EVAR", [Num (_,ev)]) -> [< 'sTR ("?" ^ (string_of_int ev)) >]
  | Node(_,"CONST",[Path(_,sl,s)]) ->
      let sp = section_path sl s in
      pr_qualified_path sp (basename (section_path sl s))
  | Node(_,"MUTIND",[Path(_,sl,s); Num(_,tyi)]) ->
      let sp = section_path sl s in
      pr_qualified_path sp (Global.id_of_global (IndRef (sp,tyi)))
  | Node(_,"MUTCONSTRUCT",[Path(_,sl,s); Num(_,tyi); Num(_,i)]) ->
      let sp = section_path sl s in
      pr_qualified_path sp (Global.id_of_global (ConstructRef ((sp,tyi),i)))
(*
  | Node(_,"EVAR", (Num (_,ev))::_) ->
      if !print_arguments then dfltpr gt
      else pr_existential (ev,[])
  | Node(_,"CONST"),(Path(_,sl,s))::_) ->
      if !print_arguments then dfltpr gt
      else pr_constant (section_path sl s,[])
  | Node(_,"MUTIND",(Path(_,sl,s))::(Num(_,tyi))::_) ->
      if !print_arguments then (dfltpr gt)
      else pr_inductive ((section_path sl s,tyi),[])
  | Node(_,"MUTCONSTRUCT",(Path(_,sl,s))::(Num(_,tyi))::(Num(_,i))::_) ->
      if !print_arguments then (dfltpr gt)
      else pr_constructor (((section_path sl s,tyi),i),[])
*)
  | 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

(* These are the names of the universes where the pp rules for constr and
   tactic are put (must be consistent with files PPConstr.v and PPTactic.v *)

let constr_syntax_universe = "constr"
let tactic_syntax_universe = "tactic"

(* 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 = Some ((constr_syntax_universe,(9,0,0)),Extend.L)
let tactic_initial_prec = Some ((tactic_syntax_universe,(9,0,0)),Extend.L)

let gentermpr_fail gt =
  Esyntax.genprint globpr constr_syntax_universe constr_initial_prec gt

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

(* [at_top] means ids of env must be avoided in bound variables *)
let gentermpr_core at_top env t =
  gentermpr (Termast.ast_of_constr at_top env t)

let prterm_env_at_top env = gentermpr_core true env
let prterm_env env = gentermpr_core false env
let prterm = prterm_env empty_env

let prtype_env env typ = prterm_env env (incast_type typ)
let prtype = prtype_env empty_env

let prjudge_env env j =
  (prterm_env env j.uj_val, prterm_env env (incast_type j.uj_type))
let prjudge = prjudge_env empty_env

(* Plus de "k"...
let gentermpr k = gentermpr_core false
let gentermpr_at_top k = gentermpr_core true

let fprterm_env a = gentermpr FW a
let fprterm = fprterm_env empty_env

let fprtype_env env typ = fprterm_env env (incast_type typ)
let fprtype = fprtype_env empty_env
*)

let fprterm_env a =
  warning "Fw printing not implemented, use CCI printing 1"; prterm_env a
let fprterm a =
  warning "Fw printing not implemented, use CCI printing 2"; prterm a

let fprtype_env env typ =
  warning "Fw printing not implemented, use CCI printing 3"; prtype_env env typ
let fprtype a =
  warning "Fw printing not implemented, use CCI printing 4"; prtype a

(* For compatibility *)
let fterm0 = fprterm_env

let pr_constant env cst = gentermpr (ast_of_constant env cst)
let pr_existential env ev = gentermpr (ast_of_existential env ev)
let pr_inductive env ind = gentermpr (ast_of_inductive env ind)
let pr_constructor env cstr =
  gentermpr (ast_of_constructor env cstr)

open Pattern
let pr_ref_label = function (* On triche sur le contexte *)
  | ConstNode sp -> pr_constant (Global.env()) (sp,[||])
  | IndNode sp -> pr_inductive (Global.env()) (sp,[||])
  | CstrNode sp -> pr_constructor (Global.env()) (sp,[||])
  | VarNode id -> print_id id

let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t)
let pr_pattern_env env t = gentermpr (Termast.ast_of_pattern env t)
let pr_pattern t = pr_pattern_env empty_names_context t

let rec gentacpr gt =
  Esyntax.genprint default_tacpr tactic_syntax_universe tactic_initial_prec gt

and default_tacpr = function
    | Nvar(_,s) -> [< 'sTR s >]
    | Node(_,s,[]) -> [< 'sTR s >]
    | Node(_,s,ta) ->
	[< 'sTR s; 'bRK(1,2); hOV 0 (prlist_with_sep pr_spc gentacpr ta) >]
    | gt -> dfltpr gt

let pr_var_decl env (id,c,typ) =<commit_msg>Ajout de globpr dans tacpr<commit_after>
(* $Id$ *)

open Pp
open Util
open Names
open Term
open Sign
open Environ
open Global
open Declare
open Coqast
open Termast

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

let dfltpr ast = [< 'sTR"#GENTERM " ; Ast.print_ast ast >];;

let section_path sl s =
  let sl = List.rev sl in
  make_path (List.tl sl) (id_of_string (List.hd sl)) (kind_of_string s)

(*
let pr_global k oper =
  let id = id_of_global oper in
  [< 'sTR (string_of_id id) >]
*)

let pr_qualified_path sp id =
  if Nametab.sp_of_id (kind_of_path sp) id = sp then [<'sTR(string_of_id id)>]
  else [<'sTR(string_of_path (make_path (dirpath sp) id (kind_of_path sp)))>]

let globpr gt = match gt with
  | Nvar(_,s) -> [< 'sTR s >]
  | Node(_,"EVAR", [Num (_,ev)]) -> [< 'sTR ("?" ^ (string_of_int ev)) >]
  | Node(_,"CONST",[Path(_,sl,s)]) ->
      let sp = section_path sl s in
      pr_qualified_path sp (basename (section_path sl s))
  | Node(_,"MUTIND",[Path(_,sl,s); Num(_,tyi)]) ->
      let sp = section_path sl s in
      pr_qualified_path sp (Global.id_of_global (IndRef (sp,tyi)))
  | Node(_,"MUTCONSTRUCT",[Path(_,sl,s); Num(_,tyi); Num(_,i)]) ->
      let sp = section_path sl s in
      pr_qualified_path sp (Global.id_of_global (ConstructRef ((sp,tyi),i)))
  | 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

(* These are the names of the universes where the pp rules for constr and
   tactic are put (must be consistent with files PPConstr.v and PPTactic.v *)

let constr_syntax_universe = "constr"
let tactic_syntax_universe = "tactic"

(* 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 = Some ((constr_syntax_universe,(9,0,0)),Extend.L)
let tactic_initial_prec = Some ((tactic_syntax_universe,(9,0,0)),Extend.L)

let gentermpr_fail gt =
  Esyntax.genprint globpr constr_syntax_universe constr_initial_prec gt

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

(* [at_top] means ids of env must be avoided in bound variables *)
let gentermpr_core at_top env t =
  gentermpr (Termast.ast_of_constr at_top env t)

let prterm_env_at_top env = gentermpr_core true env
let prterm_env env = gentermpr_core false env
let prterm = prterm_env empty_env

let prtype_env env typ = prterm_env env (incast_type typ)
let prtype = prtype_env empty_env

let prjudge_env env j =
  (prterm_env env j.uj_val, prterm_env env (incast_type j.uj_type))
let prjudge = prjudge_env empty_env

(* Plus de "k"...
let gentermpr k = gentermpr_core false
let gentermpr_at_top k = gentermpr_core true

let fprterm_env a = gentermpr FW a
let fprterm = fprterm_env empty_env

let fprtype_env env typ = fprterm_env env (incast_type typ)
let fprtype = fprtype_env empty_env
*)

let fprterm_env a =
  warning "Fw printing not implemented, use CCI printing 1"; prterm_env a
let fprterm a =
  warning "Fw printing not implemented, use CCI printing 2"; prterm a

let fprtype_env env typ =
  warning "Fw printing not implemented, use CCI printing 3"; prtype_env env typ
let fprtype a =
  warning "Fw printing not implemented, use CCI printing 4"; prtype a

(* For compatibility *)
let fterm0 = fprterm_env

let pr_constant env cst = gentermpr (ast_of_constant env cst)
let pr_existential env ev = gentermpr (ast_of_existential env ev)
let pr_inductive env ind = gentermpr (ast_of_inductive env ind)
let pr_constructor env cstr =
  gentermpr (ast_of_constructor env cstr)

open Pattern
let pr_ref_label = function (* On triche sur le contexte *)
  | ConstNode sp -> pr_constant (Global.env()) (sp,[||])
  | IndNode sp -> pr_inductive (Global.env()) (sp,[||])
  | CstrNode sp -> pr_constructor (Global.env()) (sp,[||])
  | VarNode id -> print_id id

let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t)
let pr_pattern_env env t = gentermpr (Termast.ast_of_pattern env t)
let pr_pattern t = pr_pattern_env empty_names_context t

let rec gentacpr gt =
  Esyntax.genprint default_tacpr tactic_syntax_universe tactic_initial_prec gt

and default_tacpr = function
    | Nvar(_,s) -> [< 'sTR s >]

    (* constr's may occur inside tac expressions ! *)
    | Node(_,"EVAR", [Num (_,ev)]) -> [< 'sTR ("?" ^ (string_of_int ev)) >]
    | Node(_,"CONST",[Path(_,sl,s)]) ->
	let sp = section_path sl s in
	pr_qualified_path sp (basename (section_path sl s))
    | Node(_,"MUTIND",[Path(_,sl,s); Num(_,tyi)]) ->
	let sp = section_path sl s in
	pr_qualified_path sp (Global.id_of_global (IndRef (sp,tyi)))
    | Node(_,"MUTCONSTRUCT",[Path(_,sl,s); Num(_,tyi); Num(_,i)]) ->
	let sp = section_path sl s in
	pr_qualified_path sp (Global.id_of_global (ConstructRef ((sp,tyi),i)))

    (* This should be tactics *)
    | Node(_,s,[]) -> [< 'sTR s >]
    | Node(_,s,ta) ->
	[< 'sTR s; 'bRK(1,2); hOV 0 (prlist_with_sep pr_spc gentacpr ta) >]
    | gt -> dfltpr gt 

let pr_var_decl env (id,c,typ) =
{'fraction_non_alphanumeric': 0.12129380053908356, 'fraction_numerical': 0.004043126684636119, 'mean_word_length': 4.2682555780933065, 'pattern_counts': {'":': 0, '<': 30, '<?xml version=': 0, '>': 74, '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': '2084848', 'n_tokens_mistral': 3998, 'n_tokens_neox': 3908, 'n_words': 1162}