<commit_before>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

open Util
open Names
open Univ
open Term
open Termops
open Sign
open Declarations
open Environ
open Reductionops

(* The following three functions are similar to the ones defined in
   Inductive, but they expect an env *)

let type_of_inductive env ind =
 let specif = Inductive.lookup_mind_specif env ind in
  Inductive.type_of_inductive specif

(* Return type as quoted by the user *)
let type_of_constructor env cstr =
 let specif =
  Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
 Inductive.type_of_constructor cstr specif

(* Return constructor types in normal form *)
let arities_of_constructors env ind =
 let specif = Inductive.lookup_mind_specif env ind in
  Inductive.arities_of_constructors ind specif

(* [inductive_family] = [inductive_instance] applied to global parameters *)
type inductive_family = inductive * constr list

let make_ind_family (mis, params) = (mis,params)
let dest_ind_family (mis,params) = (mis,params)

let map_ind_family f (mis,params) = (mis, List.map f params)

let liftn_inductive_family n d = map_ind_family (liftn n d)
let lift_inductive_family n = liftn_inductive_family n 1

let substnl_ind_family l n = map_ind_family (substnl l n)


type inductive_type = IndType of inductive_family * constr list

let make_ind_type (indf, realargs) = IndType (indf,realargs)
let dest_ind_type (IndType (indf,realargs)) = (indf,realargs)

let map_inductive_type f (IndType (indf, realargs)) =
  IndType (map_ind_family f indf, List.map f realargs)

let liftn_inductive_type n d = map_inductive_type (liftn n d)
let lift_inductive_type n = liftn_inductive_type n 1

let substnl_ind_type l n = map_inductive_type (substnl l n)

let mkAppliedInd (IndType ((ind,params), realargs)) =
  applist (mkInd ind,params@realargs)


(* Does not consider imbricated or mutually recursive types *) 
let mis_is_recursive_subset listind rarg = 
  let rec one_is_rec rvec = 
    List.exists
      (fun ra ->
        match dest_recarg ra with
	  | Mrec i -> List.mem i listind 
          | _ -> false) rvec
  in 
  array_exists one_is_rec (dest_subterms rarg)

let mis_is_recursive (ind,mib,mip) =
  mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1))
    mip.mind_recargs

let mis_nf_constructor_type (ind,mib,mip) j =
  let specif = mip.mind_nf_lc
  and ntypes = mib.mind_ntypes
  and nconstr = Array.length mip.mind_consnames in
  let make_Ik k = mkInd ((fst ind),ntypes-k-1) in 
  if j > nconstr then error "Not enough constructors in the type";
  substl (list_tabulate make_Ik ntypes) specif.(j-1)

(* Arity of constructors excluding parameters and local defs *)

let mis_constr_nargs indsp =
  let (mib,mip) = Global.lookup_inductive indsp in
  let recargs = dest_subterms mip.mind_recargs in
  Array.map List.length recargs

let mis_constr_nargs_env env (kn,i) = 
  let mib = Environ.lookup_mind kn env in
  let mip = mib.mind_packets.(i) in 
  let recargs = dest_subterms mip.mind_recargs in
  Array.map List.length recargs

let mis_constructor_nargs_env env ((kn,i),j) =
  let mib = Environ.lookup_mind kn env in
  let mip = mib.mind_packets.(i) in 
  recarg_length mip.mind_recargs j + mib.mind_nparams

let constructor_nrealargs env (ind,j) =
  let (_,mip) = Inductive.lookup_mind_specif env ind in
  recarg_length mip.mind_recargs j

let constructor_nrealhyps env (ind,j) =
  let (mib,mip) = Inductive.lookup_mind_specif env ind in
  mip.mind_consnrealargs.(j-1) - List.length (mib.mind_params_ctxt)

(* Length of arity (w/o local defs) *)

let inductive_nargs env ind =
  let (mib,mip) = Inductive.lookup_mind_specif env ind in
  mip.mind_nrealargs + rel_context_length mib.mind_params_ctxt

(* Annotation for cases *)
let make_case_info env ind style pats_source =
  let (mib,mip) = Inductive.lookup_mind_specif env ind in
  let print_info =
    { ind_nargs = mip.mind_nrealargs;
      style     = style;
      source    = pats_source } in
  { ci_ind     = ind;
    ci_npar    = mib.mind_nparams;
    ci_cstr_nargs = mip.mind_consnrealargs;
    ci_pp_info = print_info }

let make_default_case_info env style ind =
  let (mib,mip) = Inductive.lookup_mind_specif env ind in
  make_case_info env ind style
    (Array.map (fun _ -> RegularPat) mip.mind_consnames)

(*s Useful functions *)

type constructor_summary = {
  cs_cstr : constructor;
  cs_params : constr list;
  cs_nargs : int;
  cs_args : rel_context;
  cs_concl_realargs : constr array
}<commit_msg>Fonctions retournant les arits des constructeurs et inductifs (suite)<commit_after>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

open Util
open Names
open Univ
open Term
open Termops
open Sign
open Declarations
open Environ
open Reductionops

(* The following three functions are similar to the ones defined in
   Inductive, but they expect an env *)

let type_of_inductive env ind =
 let specif = Inductive.lookup_mind_specif env ind in
  Inductive.type_of_inductive specif

(* Return type as quoted by the user *)
let type_of_constructor env cstr =
 let specif =
  Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
 Inductive.type_of_constructor cstr specif

(* Return constructor types in normal form *)
let arities_of_constructors env ind =
 let specif = Inductive.lookup_mind_specif env ind in
  Inductive.arities_of_constructors ind specif

(* [inductive_family] = [inductive_instance] applied to global parameters *)
type inductive_family = inductive * constr list

let make_ind_family (mis, params) = (mis,params)
let dest_ind_family (mis,params) = (mis,params)

let map_ind_family f (mis,params) = (mis, List.map f params)

let liftn_inductive_family n d = map_ind_family (liftn n d)
let lift_inductive_family n = liftn_inductive_family n 1

let substnl_ind_family l n = map_ind_family (substnl l n)


type inductive_type = IndType of inductive_family * constr list

let make_ind_type (indf, realargs) = IndType (indf,realargs)
let dest_ind_type (IndType (indf,realargs)) = (indf,realargs)

let map_inductive_type f (IndType (indf, realargs)) =
  IndType (map_ind_family f indf, List.map f realargs)

let liftn_inductive_type n d = map_inductive_type (liftn n d)
let lift_inductive_type n = liftn_inductive_type n 1

let substnl_ind_type l n = map_inductive_type (substnl l n)

let mkAppliedInd (IndType ((ind,params), realargs)) =
  applist (mkInd ind,params@realargs)


(* Does not consider imbricated or mutually recursive types *) 
let mis_is_recursive_subset listind rarg = 
  let rec one_is_rec rvec = 
    List.exists
      (fun ra ->
        match dest_recarg ra with
	  | Mrec i -> List.mem i listind 
          | _ -> false) rvec
  in 
  array_exists one_is_rec (dest_subterms rarg)

let mis_is_recursive (ind,mib,mip) =
  mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1))
    mip.mind_recargs

let mis_nf_constructor_type (ind,mib,mip) j =
  let specif = mip.mind_nf_lc
  and ntypes = mib.mind_ntypes
  and nconstr = Array.length mip.mind_consnames in
  let make_Ik k = mkInd ((fst ind),ntypes-k-1) in 
  if j > nconstr then error "Not enough constructors in the type";
  substl (list_tabulate make_Ik ntypes) specif.(j-1)

(* Arity of constructors excluding parameters and local defs *)

let mis_constr_nargs indsp =
  let (mib,mip) = Global.lookup_inductive indsp in
  let recargs = dest_subterms mip.mind_recargs in
  Array.map List.length recargs

let mis_constr_nargs_env env (kn,i) = 
  let mib = Environ.lookup_mind kn env in
  let mip = mib.mind_packets.(i) in 
  let recargs = dest_subterms mip.mind_recargs in
  Array.map List.length recargs

let mis_constructor_nargs_env env ((kn,i),j) =
  let mib = Environ.lookup_mind kn env in
  let mip = mib.mind_packets.(i) in 
  recarg_length mip.mind_recargs j + mib.mind_nparams

let constructor_nrealargs env (ind,j) =
  let (_,mip) = Inductive.lookup_mind_specif env ind in
  recarg_length mip.mind_recargs j

let constructor_nrealhyps env (ind,j) =
  let (mib,mip) = Inductive.lookup_mind_specif env ind in
  mip.mind_consnrealargs.(j-1) - rel_context_length (mib.mind_params_ctxt)

(* Length of arity (w/o local defs) *)

let inductive_nargs env ind =
  let (mib,mip) = Inductive.lookup_mind_specif env ind in
  print_int mip.mind_nrealargs;
  print_int (rel_context_length mib.mind_params_ctxt);
  flush stdout;
  mip.mind_nrealargs + rel_context_nhyps mib.mind_params_ctxt

(* Annotation for cases *)
let make_case_info env ind style pats_source =
  let (mib,mip) = Inductive.lookup_mind_specif env ind in
  let print_info =
    { ind_nargs = mip.mind_nrealargs;
      style     = style;
      source    = pats_source } in
  { ci_ind     = ind;
    ci_npar    = mib.mind_nparams;
    ci_cstr_nargs = mip.mind_consnrealargs;
    ci_pp_info = print_info }

let make_default_case_info env style ind =
  let (mib,mip) = Inductive.lookup_mind_specif env ind in
  make_case_info env ind style
    (Array.map (fun _ -> RegularPat) mip.mind_consnames)

(*s Useful functions *)

type constructor_summary = {
  cs_cstr : constructor;
  cs_params : constr list;
  cs_nargs : int;
  cs_args : rel_context;
  cs_concl_realargs : constr array
}
{'fraction_non_alphanumeric': 0.11616612151848547, 'fraction_numerical': 0.001784121320249777, 'mean_word_length': 4.27443805541035, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 13, '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': '5970330', 'n_tokens_mistral': 3614, 'n_tokens_neox': 3490, 'n_words': 995}