<commit_before>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Util
open Names
open Libnames
open Nameops
open Term
open Environ
open Declarations
open Entries
open Declare
open Nametab
open Constrintern
open Command
open Inductive
open Safe_typing
open Decl_kinds
open Indtypes
open Type_errors
open Topconstr

(********** definition d'un record (structure) **************)

let interp_evars evdref env impls k typ =
  let typ' = intern_gen true ~impls !evdref env typ in
  let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in
    imps, Pretyping.Default.understand_tcc_evars evdref env k typ'

let interp_fields_evars evars env impls_env nots l =
  List.fold_left2
    (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
      let impl, t' = interp_evars evars env impls Pretyping.IsType t in
      let b' = Option.map (fun x -> snd (interp_evars evars env impls (Pretyping.OfType (Some t')) x)) b in
      let impls =
	match i with
	| Anonymous -> impls
	| Name id -> Idmap.add id (compute_internalization_data env Constrintern.Method t' impl) impls
      in
      let d = (i,b',t') in
      List.iter (Metasyntax.set_notation_for_interpretation impls) no;
      (push_rel d env, impl :: uimpls, d::params, impls))
    (env, [], [], impls_env) nots l

let binder_of_decl = function
  | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
  | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None))

let binders_of_decls = List.map binder_of_decl

let typecheck_params_and_fields id t ps nots fs =
  let env0 = Global.env () in
  let evars = ref Evd.empty in
  let _ = 
    let error bk (loc, name) = 
      match bk with
      | Default _ ->
	  if name = Anonymous then 
	    user_err_loc (loc, "record", str "Record parameters must be named")
      | _ -> ()
    in
      List.iter 
	(function LocalRawDef (b, _) -> error default_binder_kind b
	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps
  in 
  let impls_env, ((env1,newps), imps) = interp_context_evars evars env0 ps in
  let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (Termops.new_Type ()) t) newps in
  let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
  let env2,impls,newfs,data =
    interp_fields_evars evars env_ar impls_env nots (binders_of_decls fs)
  in
  let evars = Evarconv.consider_remaining_unif_problems env_ar !evars in
  let evars = Typeclasses.resolve_typeclasses env_ar evars in
  let sigma =  evars in
  let newps = Evarutil.nf_rel_context_evar sigma newps in
  let newfs = Evarutil.nf_rel_context_evar sigma newfs in
  let ce t = Evarutil.check_evars env0 Evd.empty evars t in
    List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newps;
    List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newfs;
    imps, newps, impls, newfs

let degenerate_decl (na,b,t) =
  let id = match na with
    | Name id -> id
    | Anonymous -> anomaly "Unnamed record variable" in
  match b with<commit_msg>Check for unresolved evars in textual order of the params and fields declarations (fixes bug #2278).<commit_after>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Util
open Names
open Libnames
open Nameops
open Term
open Environ
open Declarations
open Entries
open Declare
open Nametab
open Constrintern
open Command
open Inductive
open Safe_typing
open Decl_kinds
open Indtypes
open Type_errors
open Topconstr

(********** definition d'un record (structure) **************)

let interp_evars evdref env impls k typ =
  let typ' = intern_gen true ~impls !evdref env typ in
  let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in
    imps, Pretyping.Default.understand_tcc_evars evdref env k typ'

let interp_fields_evars evars env impls_env nots l =
  List.fold_left2
    (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
      let impl, t' = interp_evars evars env impls Pretyping.IsType t in
      let b' = Option.map (fun x -> snd (interp_evars evars env impls (Pretyping.OfType (Some t')) x)) b in
      let impls =
	match i with
	| Anonymous -> impls
	| Name id -> Idmap.add id (compute_internalization_data env Constrintern.Method t' impl) impls
      in
      let d = (i,b',t') in
      List.iter (Metasyntax.set_notation_for_interpretation impls) no;
      (push_rel d env, impl :: uimpls, d::params, impls))
    (env, [], [], impls_env) nots l

let binder_of_decl = function
  | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
  | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None))

let binders_of_decls = List.map binder_of_decl

let typecheck_params_and_fields id t ps nots fs =
  let env0 = Global.env () in
  let evars = ref Evd.empty in
  let _ = 
    let error bk (loc, name) = 
      match bk with
      | Default _ ->
	  if name = Anonymous then 
	    user_err_loc (loc, "record", str "Record parameters must be named")
      | _ -> ()
    in
      List.iter 
	(function LocalRawDef (b, _) -> error default_binder_kind b
	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps
  in 
  let impls_env, ((env1,newps), imps) = interp_context_evars evars env0 ps in
  let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (Termops.new_Type ()) t) newps in
  let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
  let env2,impls,newfs,data =
    interp_fields_evars evars env_ar impls_env nots (binders_of_decls fs)
  in
  let evars = Evarconv.consider_remaining_unif_problems env_ar !evars in
  let evars = Typeclasses.resolve_typeclasses env_ar evars in
  let sigma =  evars in
  let newps = Evarutil.nf_rel_context_evar sigma newps in
  let newfs = Evarutil.nf_rel_context_evar sigma newfs in
  let ce t = Evarutil.check_evars env0 Evd.empty evars t in
    List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps);
    List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs);
    imps, newps, impls, newfs

let degenerate_decl (na,b,t) =
  let id = match na with
    | Name id -> id
    | Anonymous -> anomaly "Unnamed record variable" in
  match b with
{'fraction_non_alphanumeric': 0.1546318626755568, 'fraction_numerical': 0.005390835579514825, 'mean_word_length': 3.4705136334812936, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 37, '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': '2927043', 'n_tokens_mistral': 2501, 'n_tokens_neox': 2409, 'n_words': 790}