<commit_before>
(* $Id$ *)

open Pp
open Util
open Names
(* open Generic *)
open Term
open Global
open Sign
open Environ
open Inductive
open Printer
open Reduction
open Retyping
open Tacmach
open Proof_type
open Clenv
open Tactics
open Wcclausenv
open Tacticals
open Tactics
open Elim
open Equality
open Typing
open Pattern

(* [make_inv_predicate (ity,args) C]
  
   is given the inductive type, its arguments, both the global
   parameters and its local arguments, and is expected to produce a
   predicate P such that if largs is the "local" part of the
   arguments, then (P largs) will be convertible with a conclusion of
   the form:

   <A1>a1=a1-><A2>a2=a2 ... -> C

   Algorithm: suppose length(largs)=n

   (1) Push the entire arity, [xbar:Abar], carrying along largs and
   the conclusion

   (2) Pair up each ai with its respective Rel version: a1==(Rel n),
   a2==(Rel n-1), etc.

   (3) For each pair, ai,Rel j, if the Ai is dependent - that is, the
   type of [Rel j] is an open term, then we construct the iterated
   tuple, [make_iterated_tuple] does it, and use that for our equation

   Otherwise, we just use <Ai>ai=Rel j

 *)

let dest_match_eq gls eqn =
  try 
    pf_matches gls (eq_pattern ()) eqn
  with PatternMatchingFailure -> 
    (try 
       pf_matches gls (eqT_pattern ()) eqn
     with PatternMatchingFailure -> 
       (try 
	  pf_matches gls (idT_pattern ()) eqn
        with PatternMatchingFailure ->
	  errorlabstrm "dest_match_eq" 
	    [< 'sTR "no primitive equality here" >]))
    
(* Environment management *)
let push_rel_type sigma (na,t) env =
  push_rel_decl (na,make_typed t (get_sort_of env sigma t)) env

let push_rels vars env =
  List.fold_left (fun env nvar -> push_rel_type Evd.empty nvar env) env vars

type inversion_status = Dep of constr option | NoDep

let compute_eqn env sigma n i ai =
  (ai,get_type_of env sigma ai),
  (mkRel (n-i),get_type_of env sigma (mkRel (n-i)))

let make_inv_predicate env sigma ind id status concl =
  let indf,realargs = dest_ind_type ind in
  let nrealargs = List.length realargs in<commit_msg>Bug ordre dans push_rels<commit_after>
(* $Id$ *)

open Pp
open Util
open Names
(* open Generic *)
open Term
open Global
open Sign
open Environ
open Inductive
open Printer
open Reduction
open Retyping
open Tacmach
open Proof_type
open Clenv
open Tactics
open Wcclausenv
open Tacticals
open Tactics
open Elim
open Equality
open Typing
open Pattern

(* [make_inv_predicate (ity,args) C]
  
   is given the inductive type, its arguments, both the global
   parameters and its local arguments, and is expected to produce a
   predicate P such that if largs is the "local" part of the
   arguments, then (P largs) will be convertible with a conclusion of
   the form:

   <A1>a1=a1-><A2>a2=a2 ... -> C

   Algorithm: suppose length(largs)=n

   (1) Push the entire arity, [xbar:Abar], carrying along largs and
   the conclusion

   (2) Pair up each ai with its respective Rel version: a1==(Rel n),
   a2==(Rel n-1), etc.

   (3) For each pair, ai,Rel j, if the Ai is dependent - that is, the
   type of [Rel j] is an open term, then we construct the iterated
   tuple, [make_iterated_tuple] does it, and use that for our equation

   Otherwise, we just use <Ai>ai=Rel j

 *)

let dest_match_eq gls eqn =
  try 
    pf_matches gls (eq_pattern ()) eqn
  with PatternMatchingFailure -> 
    (try 
       pf_matches gls (eqT_pattern ()) eqn
     with PatternMatchingFailure -> 
       (try 
	  pf_matches gls (idT_pattern ()) eqn
        with PatternMatchingFailure ->
	  errorlabstrm "dest_match_eq" 
	    [< 'sTR "no primitive equality here" >]))
    
(* Environment management *)
let push_rel_type sigma (na,t) env =
  push_rel_decl (na,make_typed t (get_sort_of env sigma t)) env

let push_rels vars env =
  List.fold_right (push_rel_type Evd.empty) vars env

type inversion_status = Dep of constr option | NoDep

let compute_eqn env sigma n i ai =
  (ai,get_type_of env sigma ai),
  (mkRel (n-i),get_type_of env sigma (mkRel (n-i)))

let make_inv_predicate env sigma ind id status concl =
  let indf,realargs = dest_ind_type ind in
  let nrealargs = List.length realargs in
{'fraction_non_alphanumeric': 0.07805348108889425, 'fraction_numerical': 0.005781739339918092, 'mean_word_length': 3.567656765676568, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 22, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6909455', 'n_tokens_mistral': 1463, 'n_tokens_neox': 1390, 'n_words': 547}