<commit_before>
(* $Id$ *)

open Pp
open Util
open Univ
open Names
open Term
open Inductive
open Sign
open Environ
open Declare
open Impargs
open Coqast
open Ast
open Rawterm
open Pattern

(* In this file, we translate rawconstr to ast, in order to print constr *)

(**********************************************************************)
(* Parametrization                                                    *)

(* This governs printing of local context of references *)
let print_arguments = ref false

(* If true, prints local context of evars, whatever print_arguments *)
let print_evar_arguments = ref false

(* This forces printing of cast nodes *)
let print_casts = ref true

(* This governs printing of implicit arguments.  When
   [print_implicits] is on then [print_implicits_explicit_args] tells
   how implicit args are printed. If on, implicit args are printed
   prefixed by "!" otherwise the function and not the arguments is
   prefixed by "!" *)
let print_implicits = ref false
let print_implicits_explicit_args = ref false

(* This forces printing of coercions *)
let print_coercions = ref false

let with_option o f x =
  let old = !o in o:=true;
  try let r = f x in o := old; r
  with e -> o := old; raise e

let with_arguments f = with_option print_arguments f
let with_casts f = with_option print_casts f
let with_implicits f = with_option print_implicits f
let with_coercions f = with_option print_coercions f

(**********************************************************************)
(* conversion of references                                           *)

let ids_of_ctxt ctxt =
  Array.to_list
    (Array.map
       (function c -> match kind_of_term c with
	  | IsVar id -> id
	  | _ ->
       error
       "Termast: arbitrary substitution of references not yet implemented")
     ctxt)

let ast_of_ident id = nvar (string_of_id id)

let ast_of_name = function 
  | Name id -> nvar (string_of_id id)
  | Anonymous -> nvar "_"

let stringopt_of_name = function 
  | Name id -> Some (string_of_id id)
  | Anonymous -> None

let ast_of_constant_ref pr (sp,ids) =
  let a = ope("CONST", [path_section dummy_loc sp]) in
  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
  else a

let ast_of_existential_ref pr  (ev,ids) =
  let a = ope("EVAR", [num ev]) in
  if !print_arguments or !print_evar_arguments then
    ope("INSTANCE",a::(array_map_to_list pr ids))
  else a

let ast_of_constructor_ref pr  (((sp,tyi),n) as cstr_sp,ids) =
  let a = ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n]) in
  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
  else a

let ast_of_inductive_ref pr  ((sp,tyi) as ind_sp,ids) =
  let a = ope("MUTIND",	[path_section dummy_loc sp; num tyi]) in
  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
  else a

let ast_of_ref pr r =
  (* TODO grer le ctxt *)
  let ctxt = [||] in match r with
  | ConstRef sp -> ast_of_constant_ref pr (sp,ctxt)
  | IndRef sp -> ast_of_inductive_ref pr (sp,ctxt)
  | ConstructRef sp -> ast_of_constructor_ref pr (sp,ctxt)
  | VarRef sp -> ast_of_ident (basename sp)
  | EvarRef ev -> ast_of_existential_ref pr (ev,ctxt)

let ast_of_qualid p =
  let dir, s = repr_qualid p in
  let args = List.map nvar (dir@[s]) in
  ope ("QUALID", args)

(**********************************************************************)
(* conversion of patterns                                             *)

let adapt (cstr_sp,ctxt) = (cstr_sp,Array.of_list ctxt)

let rec ast_of_cases_pattern = function   (* loc is thrown away for printing *)
  | PatVar (loc,Name id) -> nvar (string_of_id id)
  | PatVar (loc,Anonymous) -> nvar "_"
  | PatCstr(loc,cstr,args,Name id) ->
      let args = List.map ast_of_cases_pattern args in
      ope("PATTAS",
	  [nvar (string_of_id id);
	   ope("PATTCONSTRUCT",
	       (ast_of_constructor_ref ast_of_ident (adapt cstr))::args)])
  | PatCstr(loc,cstr,args,Anonymous) ->
      ope("PATTCONSTRUCT",
	  (ast_of_constructor_ref ast_of_ident (adapt cstr))::
	  List.map ast_of_cases_pattern args)
	
let ast_dependent na aty =
  match na with
    | Name id -> occur_var_ast (string_of_id id) aty
    | Anonymous -> false

(* Implicit args indexes are in ascending order *)
let explicitize =
  let rec exprec n lastimplargs impl = function
    | a::args ->
	(match impl with
	   | i::l when i=n ->
	       exprec (n+1) (ope("EXPL", [num i; a])::lastimplargs) l args
	   | _ ->
	       let tail = a::(exprec (n+1) [] impl args) in
	       if (!print_implicits & !print_implicits_explicit_args) then
		 List.rev_append lastimplargs tail
	       else tail)
    (* Tail impl args are always printed even if implicit printing is off *)
    | [] -> List.rev lastimplargs
  in exprec 1 []

let rec skip_coercion dest_ref (f,args as app) =
  if !print_coercions then app
  else
    try
      match dest_ref f with
	| Some r ->
	    let n = Classops.coercion_params r in
	    if n >= List.length args then app
	    else (* We skip a coercion *)
	      let _,fargs = list_chop n args in
	      skip_coercion dest_ref (List.hd fargs,List.tl fargs)
	| None -> app
    with Not_found -> app

let ast_of_app impl f args =
  if !print_implicits & not !print_implicits_explicit_args then 
    ope("APPLISTEXPL", f::args)
  else
    ope("APPLIST", f::(explicitize impl args))
(*
    let largs = List.length args in
    let impl = List.rev (List.filter (fun i -> i <= largs) impl) in
    let impl1,impl2 = div_implicits largs impl in
    let al1 = Array.of_list args in
    List.iter
      (fun i -> al1.(i) <-
         ope("EXPL", [str "EX"; num i; al1.(i)]))
      impl2;
    List.iter
      (fun i -> al1.(i) <-
         ope("EXPL",[num i; al1.(i)]))
      impl1;
    (* On laisse les implicites,  charge du PP de ne pas les imprimer *)
    ope("APPLISTEXPL",f::(Array.to_list al1))
*)

let rec ast_of_raw = function
  | RRef (_,ref) -> ast_of_ref ast_of_raw ref
  | RVar (_,id) -> ast_of_ident id
  | RMeta (_,n) -> ope("META",[num n])
  | RApp (_,f,args) ->
      let (f,args) =
	skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in
      let astf = ast_of_raw f in
      let astargs = List.map ast_of_raw args in
      (match f with 
	 | RRef (_,ref) -> ast_of_app (implicits_of_global ref) astf astargs
	 | RVar (_,id) ->
	     let imp =
	       try 
		 let ref = Nametab.locate (make_qualid [] (string_of_id id)) in
		 implicits_of_global ref
	       with Not_found -> [] in
	     ast_of_app imp astf astargs
	 | _       -> ast_of_app [] astf astargs)
  | RBinder (_,BProd,Anonymous,t,c) ->
      (* Anonymous product are never factorized *)
      ope("PROD",[ast_of_raw t; slam(None,ast_of_raw c)])
  | RBinder (_,BLetIn,na,t,c) ->
      ope("LETIN",[ast_of_raw t; slam(stringopt_of_name na,ast_of_raw c)])
  | RBinder (_,bk,na,t,c) ->
      let (n,a) = factorize_binder 1 bk na (ast_of_raw t) c in
      let tag = match bk with
	  (* LAMBDA et LAMBDALIST se comportent pareil ... Non ! *)
	  (* Pour compatibilit des theories, il faut LAMBDALIST partout *)
	| BLambda -> (* if n=1 then "LAMBDA" else *) "LAMBDALIST"
	  (* PROD et PRODLIST doivent tre distingus  cause du cas *)
	  (* non dpendant, pour isoler l'implication; peut-tre un *)
	  (* constructeur ARROW serait-il plus justifi ? *) 
	| BProd -> if n=1 then "PROD" else "PRODLIST" 
	| BLetIn -> if n=1 then "LETIN" else "LETINLIST" <commit_msg>Suppression de l'affichage des instances des ?n<commit_after>
(* $Id$ *)

open Pp
open Util
open Univ
open Names
open Term
open Inductive
open Sign
open Environ
open Declare
open Impargs
open Coqast
open Ast
open Rawterm
open Pattern

(* In this file, we translate rawconstr to ast, in order to print constr *)

(**********************************************************************)
(* Parametrization                                                    *)

(* This governs printing of local context of references *)
let print_arguments = ref false

(* If true, prints local context of evars, whatever print_arguments *)
let print_evar_arguments = ref false

(* This forces printing of cast nodes *)
let print_casts = ref true

(* This governs printing of implicit arguments.  When
   [print_implicits] is on then [print_implicits_explicit_args] tells
   how implicit args are printed. If on, implicit args are printed
   prefixed by "!" otherwise the function and not the arguments is
   prefixed by "!" *)
let print_implicits = ref false
let print_implicits_explicit_args = ref false

(* This forces printing of coercions *)
let print_coercions = ref false

let with_option o f x =
  let old = !o in o:=true;
  try let r = f x in o := old; r
  with e -> o := old; raise e

let with_arguments f = with_option print_arguments f
let with_casts f = with_option print_casts f
let with_implicits f = with_option print_implicits f
let with_coercions f = with_option print_coercions f

(**********************************************************************)
(* conversion of references                                           *)

let ids_of_ctxt ctxt =
  Array.to_list
    (Array.map
       (function c -> match kind_of_term c with
	  | IsVar id -> id
	  | _ ->
       error
       "Termast: arbitrary substitution of references not yet implemented")
     ctxt)

let ast_of_ident id = nvar (string_of_id id)

let ast_of_name = function 
  | Name id -> nvar (string_of_id id)
  | Anonymous -> nvar "_"

let stringopt_of_name = function 
  | Name id -> Some (string_of_id id)
  | Anonymous -> None

let ast_of_constant_ref pr (sp,ids) =
  let a = ope("CONST", [path_section dummy_loc sp]) in
  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
  else a

let ast_of_existential_ref pr  (ev,ids) =
  let a = ope("EVAR", [num ev]) in
  if !print_arguments or !print_evar_arguments then
    ope("INSTANCE",a::(array_map_to_list pr ids))
  else a

let ast_of_constructor_ref pr  (((sp,tyi),n) as cstr_sp,ids) =
  let a = ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n]) in
  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
  else a

let ast_of_inductive_ref pr  ((sp,tyi) as ind_sp,ids) =
  let a = ope("MUTIND",	[path_section dummy_loc sp; num tyi]) in
  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
  else a

let ast_of_ref pr r =
  (* TODO grer le ctxt *)
  let ctxt = [||] in match r with
  | ConstRef sp -> ast_of_constant_ref pr (sp,ctxt)
  | IndRef sp -> ast_of_inductive_ref pr (sp,ctxt)
  | ConstructRef sp -> ast_of_constructor_ref pr (sp,ctxt)
  | VarRef sp -> ast_of_ident (basename sp)
  | EvarRef ev -> ast_of_existential_ref pr (ev,ctxt)

let ast_of_qualid p =
  let dir, s = repr_qualid p in
  let args = List.map nvar (dir@[s]) in
  ope ("QUALID", args)

(**********************************************************************)
(* conversion of patterns                                             *)

let adapt (cstr_sp,ctxt) = (cstr_sp,Array.of_list ctxt)

let rec ast_of_cases_pattern = function   (* loc is thrown away for printing *)
  | PatVar (loc,Name id) -> nvar (string_of_id id)
  | PatVar (loc,Anonymous) -> nvar "_"
  | PatCstr(loc,cstr,args,Name id) ->
      let args = List.map ast_of_cases_pattern args in
      ope("PATTAS",
	  [nvar (string_of_id id);
	   ope("PATTCONSTRUCT",
	       (ast_of_constructor_ref ast_of_ident (adapt cstr))::args)])
  | PatCstr(loc,cstr,args,Anonymous) ->
      ope("PATTCONSTRUCT",
	  (ast_of_constructor_ref ast_of_ident (adapt cstr))::
	  List.map ast_of_cases_pattern args)
	
let ast_dependent na aty =
  match na with
    | Name id -> occur_var_ast (string_of_id id) aty
    | Anonymous -> false

(* Implicit args indexes are in ascending order *)
let explicitize =
  let rec exprec n lastimplargs impl = function
    | a::args ->
	(match impl with
	   | i::l when i=n ->
	       exprec (n+1) (ope("EXPL", [num i; a])::lastimplargs) l args
	   | _ ->
	       let tail = a::(exprec (n+1) [] impl args) in
	       if (!print_implicits & !print_implicits_explicit_args) then
		 List.rev_append lastimplargs tail
	       else tail)
    (* Tail impl args are always printed even if implicit printing is off *)
    | [] -> List.rev lastimplargs
  in exprec 1 []

let rec skip_coercion dest_ref (f,args as app) =
  if !print_coercions then app
  else
    try
      match dest_ref f with
	| Some r ->
	    let n = Classops.coercion_params r in
	    if n >= List.length args then app
	    else (* We skip a coercion *)
	      let _,fargs = list_chop n args in
	      skip_coercion dest_ref (List.hd fargs,List.tl fargs)
	| None -> app
    with Not_found -> app

let ast_of_app impl f args =
  if !print_implicits & not !print_implicits_explicit_args then 
    ope("APPLISTEXPL", f::args)
  else
    ope("APPLIST", f::(explicitize impl args))
(*
    let largs = List.length args in
    let impl = List.rev (List.filter (fun i -> i <= largs) impl) in
    let impl1,impl2 = div_implicits largs impl in
    let al1 = Array.of_list args in
    List.iter
      (fun i -> al1.(i) <-
         ope("EXPL", [str "EX"; num i; al1.(i)]))
      impl2;
    List.iter
      (fun i -> al1.(i) <-
         ope("EXPL",[num i; al1.(i)]))
      impl1;
    (* On laisse les implicites,  charge du PP de ne pas les imprimer *)
    ope("APPLISTEXPL",f::(Array.to_list al1))
*)

let rec ast_of_raw = function
  | RRef (_,ref) -> ast_of_ref ast_of_raw ref
  | RVar (_,id) -> ast_of_ident id
  | RMeta (_,n) -> ope("META",[num n])
  | RApp (_,f,args) ->
      let (f,args) =
	skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in
      let astf = ast_of_raw f in
      let astargs = List.map ast_of_raw args in
      (match f with 
	 | RRef (_,(EvarRef _ as ref)) ->
	     ast_of_ref ast_of_raw ref (* we drop args *)
	 | RRef (_,ref) -> ast_of_app (implicits_of_global ref) astf astargs

	 | RVar (_,id) ->
	     let imp =
	       try 
		 let ref = Nametab.locate (make_qualid [] (string_of_id id)) in
		 implicits_of_global ref
	       with Not_found -> [] in
	     ast_of_app imp astf astargs
	 | _       -> ast_of_app [] astf astargs)
  | RBinder (_,BProd,Anonymous,t,c) ->
      (* Anonymous product are never factorized *)
      ope("PROD",[ast_of_raw t; slam(None,ast_of_raw c)])
  | RBinder (_,BLetIn,na,t,c) ->
      ope("LETIN",[ast_of_raw t; slam(stringopt_of_name na,ast_of_raw c)])
  | RBinder (_,bk,na,t,c) ->
      let (n,a) = factorize_binder 1 bk na (ast_of_raw t) c in
      let tag = match bk with
	  (* LAMBDA et LAMBDALIST se comportent pareil ... Non ! *)
	  (* Pour compatibilit des theories, il faut LAMBDALIST partout *)
	| BLambda -> (* if n=1 then "LAMBDA" else *) "LAMBDALIST"
	  (* PROD et PRODLIST doivent tre distingus  cause du cas *)
	  (* non dpendant, pour isoler l'implication; peut-tre un *)
	  (* constructeur ARROW serait-il plus justifi ? *) 
	| BProd -> if n=1 then "PROD" else "PRODLIST" 
	| BLetIn -> if n=1 then "LETIN" else "LETINLIST" 
{'fraction_non_alphanumeric': 0.13404069572224833, 'fraction_numerical': 0.002283258343966154, 'mean_word_length': 3.164429530201342, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 96, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '67260', 'n_tokens_mistral': 5334, 'n_tokens_neox': 5146, 'n_words': 1620}