<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 Rawterm
open Declarations
open Libobject
open Declare
open Coqast
open Environ
open Pattern
open Matching
open Printer
open Libnames
open Nametab

(* The functions print_constructors and crible implement the behavior needed
   for the Coq searching commands.
   These functions take as first argument the procedure
   that will be called to treat each entry.  This procedure receives the name
   of the object, the assumptions that will make it possible to print its type,
   and the constr term that represent its type. *)

let print_constructors indsp fn env nconstr =
  for i = 1 to nconstr do
    fn (ConstructRef (indsp,i)) env (Inductive.type_of_constructor env (indsp,i))
  done

let rec head_const c = match kind_of_term c with
  | Prod (_,_,d) -> head_const d
  | LetIn (_,_,_,d) -> head_const d
  | App (f,_)   -> head_const f
  | Cast (d,_)   -> head_const d
  | _            -> c

(* General search, restricted to head constant if [only_head] *)

let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
  let env = Global.env () in
  let imported = Library.opened_libraries() in
  let crible_rec (sp,_) lobj = match object_tag lobj with
    | "VARIABLE" ->
	(try 
	   let (idc,_,typ) = get_variable (basename sp) in 
           if refopt = None
	     || head_const typ = constr_of_reference (out_some refopt)
	   then
	     fn (VarRef idc) env typ
	 with Not_found -> (* we are in a section *) ())
    | "CONSTANT" ->
	let kn = locate_constant (qualid_of_sp sp) in
	let {const_type=typ} = Global.lookup_constant kn in
        if refopt = None
	  || head_const typ = constr_of_reference (out_some refopt)
	then
	  fn (ConstRef kn) env typ
    | "INDUCTIVE" -> 
	let kn = locate_mind (qualid_of_sp sp) in
        let mib = Global.lookup_mind kn in 
        (match refopt with 
	  | Some (IndRef ((kn',tyi) as ind)) when kn=kn' ->
	      print_constructors ind fn env
	        (Array.length (mib.mind_packets.(tyi).mind_user_lc))
	  | _ ->
              Array.iteri 
	        (fun i mip -> print_constructors (kn,i) fn env
	          (Array.length mip.mind_user_lc)) mib.mind_packets)
    | _ -> ()
  in 
  try 
    Declaremods.iter_all_segments false crible_rec
  with Not_found -> 
    ()
<commit_msg>Bug Search<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 Rawterm
open Declarations
open Libobject
open Declare
open Coqast
open Environ
open Pattern
open Matching
open Printer
open Libnames
open Nametab

(* The functions print_constructors and crible implement the behavior needed
   for the Coq searching commands.
   These functions take as first argument the procedure
   that will be called to treat each entry.  This procedure receives the name
   of the object, the assumptions that will make it possible to print its type,
   and the constr term that represent its type. *)

let print_constructors indsp fn env nconstr =
  for i = 1 to nconstr do
    fn (ConstructRef (indsp,i)) env (Inductive.type_of_constructor env (indsp,i))
  done

let rec head_const c = match kind_of_term c with
  | Prod (_,_,d) -> head_const d
  | LetIn (_,_,_,d) -> head_const d
  | App (f,_)   -> head_const f
  | Cast (d,_)   -> head_const d
  | _            -> c

(* General search, restricted to head constant if [only_head] *)

let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
  let env = Global.env () in
  let imported = Library.opened_libraries() in
  let crible_rec (sp,_) lobj = match object_tag lobj with
    | "VARIABLE" ->
	(try 
	   let (idc,_,typ) = get_variable (basename sp) in 
           if refopt = None
	     || head_const typ = constr_of_reference (out_some refopt)
	   then
	     fn (VarRef idc) env typ
	 with Not_found -> (* we are in a section *) ())
    | "CONSTANT" ->
	let kn = locate_constant (qualid_of_sp sp) in
	let {const_type=typ} = Global.lookup_constant kn in
        if refopt = None
	  || head_const typ = constr_of_reference (out_some refopt)
	then
	  fn (ConstRef kn) env typ
    | "INDUCTIVE" -> 
	let kn = locate_mind (qualid_of_sp sp) in
        let mib = Global.lookup_mind kn in 
        (match refopt with 
	  | Some (IndRef ((kn',tyi) as ind)) when kn=kn' ->
	      print_constructors ind fn env
	        (Array.length (mib.mind_packets.(tyi).mind_user_lc))
          | Some _ -> ()
	  | _ ->
              Array.iteri 
	        (fun i mip -> print_constructors (kn,i) fn env
	          (Array.length mip.mind_user_lc)) mib.mind_packets)
    | _ -> ()
  in 
  try 
    Declaremods.iter_all_segments false crible_rec
  with Not_found -> 
    ()

{'fraction_non_alphanumeric': 0.1577558916637355, 'fraction_numerical': 0.001055223355610271, 'mean_word_length': 2.9059065934065935, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 38, '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': '185163', 'n_tokens_mistral': 1804, 'n_tokens_neox': 1742, 'n_words': 598}