<commit_before>(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(*i*)
open Names
open Context
open CErrors
open Util
open Glob_term
open Constrexpr
open Libnames
open Typeclasses
open Pp
open Libobject
open Nameops
open Context.Rel.Declaration

module RelDecl = Context.Rel.Declaration
(*i*)

let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"

let declare_generalizable_ident table {CAst.loc;v=id} =
  if not (Id.equal id (root_of_id id)) then
    user_err ?loc ~hdr:"declare_generalizable_ident"
    ((Id.print id ++ str
      " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _"));
  if Id.Pred.mem id table then
    user_err ?loc ~hdr:"declare_generalizable_ident"
                ((Id.print id++str" is already declared as a generalizable identifier"))
  else Id.Pred.add id table

let add_generalizable gen table =
  match gen with
  | None -> Id.Pred.empty
  | Some [] -> Id.Pred.full
  | Some l -> List.fold_left (fun table lid -> declare_generalizable_ident table lid)
      table l

let cache_generalizable_type (_,(local,cmd)) =
  generalizable_table := add_generalizable cmd !generalizable_table

let load_generalizable_type _ (_,(local,cmd)) =
  generalizable_table := add_generalizable cmd !generalizable_table

let in_generalizable : bool * lident list option -> obj =
  declare_object {(default_object "GENERALIZED-IDENT") with
    load_function = load_generalizable_type;
    cache_function = cache_generalizable_type;
    classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
  }

let declare_generalizable ~local gen =
 Lib.add_anonymous_leaf (in_generalizable (local, gen))

let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table

let is_global id =
  try ignore (Nametab.locate_extended (qualid_of_ident id)); true
  with Not_found -> false

let is_named id env =
  try ignore (Environ.lookup_named id env); true
  with Not_found -> false

let is_freevar ids env x =
  not (Id.Set.mem x ids || is_named x env || is_global x)


(* Auxiliary functions for the inference of implicitly quantified variables. *)

let ungeneralizable loc id =
  user_err ?loc ~hdr:"Generalization"
               (str "Unbound and ungeneralizable variable " ++ Id.print id)

let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
  let found loc id bdvars l =
    if Id.List.mem id l then l
    else if is_freevar bdvars (Global.env ()) id
    then
      if find_generalizable_ident id then id :: l
      else ungeneralizable loc id
    else l
  in
  let rec aux bdvars l c = match CAst.(c.v) with
    | CRef (qid,_) when qualid_is_ident qid ->
      found c.CAst.loc (qualid_basename qid) bdvars l
    | CNotation (_,(InConstrEntry,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
        qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
        Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
    | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
  in aux bound l c

let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
  let rec vars bound vs c = match DAst.get c with
    | GVar id ->
        let loc = c.CAst.loc in
        if is_freevar bound (Global.env ()) id then
          if List.exists (fun {CAst.v} -> Id.equal v id) vs then vs
          else CAst.(make ?loc id) :: vs
        else vs
    | _ -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
  in fun rt ->
    let vars = List.rev (vars bound [] rt) in
      List.iter (fun {CAst.loc;v=id} -><commit_msg>Missing period in an error message.<commit_after>(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(*i*)
open Names
open Context
open CErrors
open Util
open Glob_term
open Constrexpr
open Libnames
open Typeclasses
open Pp
open Libobject
open Nameops
open Context.Rel.Declaration

module RelDecl = Context.Rel.Declaration
(*i*)

let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"

let declare_generalizable_ident table {CAst.loc;v=id} =
  if not (Id.equal id (root_of_id id)) then
    user_err ?loc ~hdr:"declare_generalizable_ident"
    ((Id.print id ++ str
      " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _"));
  if Id.Pred.mem id table then
    user_err ?loc ~hdr:"declare_generalizable_ident"
                ((Id.print id++str" is already declared as a generalizable identifier"))
  else Id.Pred.add id table

let add_generalizable gen table =
  match gen with
  | None -> Id.Pred.empty
  | Some [] -> Id.Pred.full
  | Some l -> List.fold_left (fun table lid -> declare_generalizable_ident table lid)
      table l

let cache_generalizable_type (_,(local,cmd)) =
  generalizable_table := add_generalizable cmd !generalizable_table

let load_generalizable_type _ (_,(local,cmd)) =
  generalizable_table := add_generalizable cmd !generalizable_table

let in_generalizable : bool * lident list option -> obj =
  declare_object {(default_object "GENERALIZED-IDENT") with
    load_function = load_generalizable_type;
    cache_function = cache_generalizable_type;
    classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
  }

let declare_generalizable ~local gen =
 Lib.add_anonymous_leaf (in_generalizable (local, gen))

let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table

let is_global id =
  try ignore (Nametab.locate_extended (qualid_of_ident id)); true
  with Not_found -> false

let is_named id env =
  try ignore (Environ.lookup_named id env); true
  with Not_found -> false

let is_freevar ids env x =
  not (Id.Set.mem x ids || is_named x env || is_global x)


(* Auxiliary functions for the inference of implicitly quantified variables. *)

let ungeneralizable loc id =
  user_err ?loc ~hdr:"Generalization"
               (str "Unbound and ungeneralizable variable " ++ Id.print id ++ str ".")

let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
  let found loc id bdvars l =
    if Id.List.mem id l then l
    else if is_freevar bdvars (Global.env ()) id
    then
      if find_generalizable_ident id then id :: l
      else ungeneralizable loc id
    else l
  in
  let rec aux bdvars l c = match CAst.(c.v) with
    | CRef (qid,_) when qualid_is_ident qid ->
      found c.CAst.loc (qualid_basename qid) bdvars l
    | CNotation (_,(InConstrEntry,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
        qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
        Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
    | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
  in aux bound l c

let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
  let rec vars bound vs c = match DAst.get c with
    | GVar id ->
        let loc = c.CAst.loc in
        if is_freevar bound (Global.env ()) id then
          if List.exists (fun {CAst.v} -> Id.equal v id) vs then vs
          else CAst.(make ?loc id) :: vs
        else vs
    | _ -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
  in fun rt ->
    let vars = List.rev (vars bound [] rt) in
      List.iter (fun {CAst.loc;v=id} ->
{'fraction_non_alphanumeric': 0.1419221495005167, 'fraction_numerical': 0.00045929498220231943, 'mean_word_length': 3.326875310481868, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 39, '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': '4714360', 'n_tokens_mistral': 2775, 'n_tokens_neox': 2722, 'n_words': 884}