<commit_before>(**********************************************************************)
(* Equations                                                          *)
(* Copyright (c) 2009-2019 <NAME> <<EMAIL>> *)
(**********************************************************************)
(* This file is distributed under the terms of the                    *)
(* GNU Lesser General Public License Version 2.1                      *)
(**********************************************************************)

open Util
open Names
open Nameops
open Constr
open Declarations
open Globnames
open Vars
open Equations_common
open EConstr
open Vars

let name_context env sigma ctx =
  let avoid, ctx =
    List.fold_right (fun decl (avoid, acc) ->
      let (n, b, t) = to_tuple decl in
      match n with
      | Name id -> let id' = Namegen.next_ident_away id avoid in
        let avoid = Id.Set.add id' avoid in
        (avoid, make_def (Name id') b t :: acc)
      | Anonymous ->
        let id' = Namegen.id_of_name_using_hdchar
            (push_rel_context acc env) sigma t Anonymous in
        let avoid = Id.Set.add id' avoid in
        (avoid, make_def (Name id') b t :: acc))
      ctx (Id.Set.empty, [])
  in ctx

let occur_rigidly sigma i concl =
  let rec aux concl =
    match kind sigma concl with
    | App (f, cl) ->
      if isConstruct sigma f then
        Array.exists aux cl
      else false
    | Rel k -> Int.equal k i
    | _ -> false
  in
  let hd, args = decompose_appvect sigma concl in
  Array.exists aux args

(* On [xn :: ... x1] returns [forcedn :: .. :: forced1] *)
let get_forced_positions sigma args concl =
  let is_forced i acc _ =
    if occur_rigidly sigma i concl then true :: acc
    else false :: acc
  in
  List.rev (List.fold_left_i is_forced 1 [] args)

let derive_noConfusion_package env sigma polymorphic (ind,u as indu) indid ~prefix ~tactic cstNoConf =
  let mindb, oneind = Global.lookup_inductive ind in
  let pi = (fst indu, EConstr.EInstance.kind sigma (snd indu)) in
  let ctx = subst_instance_context (snd pi) oneind.mind_arity_ctxt in
  let ctx = List.map of_rel_decl ctx in
  let ctx = smash_rel_context sigma ctx in
  let len =
    if prefix = "" then mindb.mind_nparams
    else List.length ctx in
  let argsvect = rel_vect 0 len in
  let noid = add_prefix "noConfusion" (add_prefix prefix (add_prefix "_" indid))
  and packid = add_prefix "NoConfusion" (add_prefix prefix (add_prefix "Package_" indid)) in
  let tc = Typeclasses.class_info (Lazy.force coq_noconfusion_class) in
  let sigma, noconf = Evd.fresh_global ~rigid:Evd.univ_rigid env sigma (ConstRef cstNoConf) in<commit_msg>Fix spurious universe in noconf_hom<commit_after>(**********************************************************************)
(* Equations                                                          *)
(* Copyright (c) 2009-2019 <NAME> <<EMAIL>> *)
(**********************************************************************)
(* This file is distributed under the terms of the                    *)
(* GNU Lesser General Public License Version 2.1                      *)
(**********************************************************************)

open Util
open Names
open Nameops
open Constr
open Declarations
open Globnames
open Vars
open Equations_common
open EConstr
open Vars

let name_context env sigma ctx =
  let avoid, ctx =
    List.fold_right (fun decl (avoid, acc) ->
      let (n, b, t) = to_tuple decl in
      match n with
      | Name id -> let id' = Namegen.next_ident_away id avoid in
        let avoid = Id.Set.add id' avoid in
        (avoid, make_def (Name id') b t :: acc)
      | Anonymous ->
        let id' = Namegen.id_of_name_using_hdchar
            (push_rel_context acc env) sigma t Anonymous in
        let avoid = Id.Set.add id' avoid in
        (avoid, make_def (Name id') b t :: acc))
      ctx (Id.Set.empty, [])
  in ctx

let occur_rigidly sigma i concl =
  let rec aux concl =
    match kind sigma concl with
    | App (f, cl) ->
      if isConstruct sigma f then
        Array.exists aux cl
      else false
    | Rel k -> Int.equal k i
    | _ -> false
  in
  let hd, args = decompose_appvect sigma concl in
  Array.exists aux args

(* On [xn :: ... x1] returns [forcedn :: .. :: forced1] *)
let get_forced_positions sigma args concl =
  let is_forced i acc _ =
    if occur_rigidly sigma i concl then true :: acc
    else false :: acc
  in
  List.rev (List.fold_left_i is_forced 1 [] args)

let derive_noConfusion_package env sigma0 polymorphic (ind,u as indu) indid ~prefix ~tactic cstNoConf =
  let mindb, oneind = Global.lookup_inductive ind in
  let pi = (fst indu, EConstr.EInstance.kind sigma0 (snd indu)) in
  let ctx = subst_instance_context (snd pi) oneind.mind_arity_ctxt in
  let ctx = List.map of_rel_decl ctx in
  let ctx = smash_rel_context sigma0 ctx in
  let len =
    if prefix = "" then mindb.mind_nparams
    else List.length ctx in
  let argsvect = rel_vect 0 len in
  let noid = add_prefix "noConfusion" (add_prefix prefix (add_prefix "_" indid))
  and packid = add_prefix "NoConfusion" (add_prefix prefix (add_prefix "Package_" indid)) in
  let tc = Typeclasses.class_info (Lazy.force coq_noconfusion_class) in
  let sigma = Evd.from_env env in
  let sigma, noconf = Evd.fresh_global ~rigid:Evd.univ_rigid env sigma (ConstRef cstNoConf) in
{'fraction_non_alphanumeric': 0.15754841135551795, 'fraction_numerical': 0.00582816318856928, 'mean_word_length': 2.9465875370919883, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 21, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '462875', 'n_tokens_mistral': 1683, 'n_tokens_neox': 1598, 'n_words': 582}