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

(* $Id$ *)

open Util
open Pp
open Names
open Nameops
open Univ
open Term
open Termops
open Sign
open Environ
open Evd
open Instantiate
open Reductionops
open Indrec
open Pretype_errors


let rec filter_unique = function
  | [] -> []
  | x::l ->
      if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l)
      else x::filter_unique l

(*
let distinct_id_list = 
  let rec drec fresh = function
      [] -> List.rev fresh 
    | id::rest ->
 	let id' = next_ident_away_from id fresh in drec (id'::fresh) rest
  in drec []
*)

(*
let filter_sign p sign x =
  sign_it
    (fun id ty (v,ids,sgn) ->
      let (disc,v') = p v (id,ty) in
      if disc then (v', id::ids, sgn) else (v', ids, add_sign (id,ty) sgn))
    sign
    (x,[],nil_sign)
*)

(* Expanding existential variables (pretyping.ml) *)
(* 1- whd_ise fails if an existential is undefined *)

exception Uninstantiated_evar of int

let rec whd_ise sigma c =
  match kind_of_term c with
    | Evar (ev,args) when Evd.in_dom sigma ev ->
	if Evd.is_defined sigma ev then
          whd_ise sigma (existential_value sigma (ev,args))
	else raise (Uninstantiated_evar ev)
  | _ -> c


(* Expand evars, possibly in the head of an application *)
let whd_castappevar_stack sigma c = 
  let rec whrec (c, l as s) =
    match kind_of_term c with
      | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> 
	  whrec (existential_value sigma (ev,args), l)
      | Cast (c,_) -> whrec (c, l)
      | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
      | _ -> s
  in 
  whrec (c, [])

let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c)

let nf_evar = Pretype_errors.nf_evar
let j_nf_evar = Pretype_errors.j_nf_evar
let jl_nf_evar = Pretype_errors.jl_nf_evar
let jv_nf_evar = Pretype_errors.jv_nf_evar
let tj_nf_evar = Pretype_errors.tj_nf_evar

(**********************)
(* Creating new evars *)
(**********************)

let evar_env evd = Global.env_of_context evd.evar_hyps

(* Generator of existential names *)
let new_evar =
  let evar_ctr = ref 0 in
  fun () -> incr evar_ctr; !evar_ctr

let make_evar_instance env =
  fold_named_context
    (fun env (id, b, _) l -> (*if b=None then*) mkVar id :: l (*else l*))
    env ~init:[]

(* create an untyped existential variable *)
let new_evar_in_sign env =
  let ev = new_evar () in
  mkEvar (ev, Array.of_list (make_evar_instance env))

(*------------------------------------*
 * functional operations on evar sets *
 *------------------------------------*)

(* All ids of sign must be distincts! *)
let new_isevar_sign env sigma typ instance =
  let sign = named_context env in
  if not (list_distinct (ids_of_named_context sign)) then 
    error "new_isevar_sign: two vars have the same name";
  let newev = new_evar() in
  let info = { evar_concl = typ; evar_hyps = sign; 
	       evar_body = Evar_empty } in
  (Evd.add sigma newev info, mkEvar (newev,Array.of_list instance))

(* We don't try to guess in which sort the type should be defined, since
   any type has type Type. May cause some trouble, but not so far... *)
let new_Type () = mkType (new_univ ())

let new_Type_sort () = Type (new_univ ())

let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
(*
let new_Type () = mkType dummy_univ

let new_Type_sort () = Type dummy_univ

let judge_of_new_Type () = 
  { uj_val = mkSort (Type dummy_univ);
    uj_type = mkSort (Type dummy_univ) }
*)

(* This refreshes universes in types; works only for inferred types (i.e. for
   types of the form (x1:A1)...(xn:An)B with B a sort or an atom in
   head normal form) *)
let refresh_universes t =
  let modified = ref false in
  let rec refresh t = match kind_of_term t with
    | Sort (Type _) -> modified := true; new_Type ()
    | Prod (na,u,v) -> mkProd (na,u,refresh v)
    | _ -> t in
  let t' = refresh t in
  if !modified then t' else t

(* Declaring any type to be in the sort Type shouldn't be harmful since
   cumulativity now includes Prop and Set in Type. *)
let new_type_var env sigma =
  let instance = make_evar_instance env in
  let (sigma',c) = new_isevar_sign env sigma (new_Type ()) instance in
  (sigma', c)

let split_evar_to_arrow sigma (ev,args) =
  let evd = Evd.map sigma ev in
  let evenv = evar_env evd in
  let (sigma1,dom) = new_type_var evenv sigma in
  let hyps = evd.evar_hyps in
  let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in
  let newenv = push_named_decl (nvar, None, dom) evenv in
  let (sigma2,rng) = new_type_var newenv sigma1 in
  let prod = mkProd (named_hd newenv dom Anonymous, dom, subst_var nvar rng) in
  let sigma3 = Evd.define sigma2 ev prod in
  let dsp = fst (destEvar dom) in
  let rsp = fst (destEvar rng) in
  (sigma3, prod,
   (dsp,args), (rsp, array_cons (mkRel 1) (Array.map (lift 1) args)))

let define_evar_as_arrow sigma ev =
  let (sigma, prod, _, _) = split_evar_to_arrow sigma ev in
  (sigma, prod)

let define_evar_as_sort sigma (ev,args) =
  let s = new_Type () in
  let sigma = Evd.define sigma ev s in
  (sigma, destSort s)
<commit_msg>Bug mauvaise instance<commit_after>(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

open Util
open Pp
open Names
open Nameops
open Univ
open Term
open Termops
open Sign
open Environ
open Evd
open Instantiate
open Reductionops
open Indrec
open Pretype_errors


let rec filter_unique = function
  | [] -> []
  | x::l ->
      if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l)
      else x::filter_unique l

(*
let distinct_id_list = 
  let rec drec fresh = function
      [] -> List.rev fresh 
    | id::rest ->
 	let id' = next_ident_away_from id fresh in drec (id'::fresh) rest
  in drec []
*)

(*
let filter_sign p sign x =
  sign_it
    (fun id ty (v,ids,sgn) ->
      let (disc,v') = p v (id,ty) in
      if disc then (v', id::ids, sgn) else (v', ids, add_sign (id,ty) sgn))
    sign
    (x,[],nil_sign)
*)

(* Expanding existential variables (pretyping.ml) *)
(* 1- whd_ise fails if an existential is undefined *)

exception Uninstantiated_evar of int

let rec whd_ise sigma c =
  match kind_of_term c with
    | Evar (ev,args) when Evd.in_dom sigma ev ->
	if Evd.is_defined sigma ev then
          whd_ise sigma (existential_value sigma (ev,args))
	else raise (Uninstantiated_evar ev)
  | _ -> c


(* Expand evars, possibly in the head of an application *)
let whd_castappevar_stack sigma c = 
  let rec whrec (c, l as s) =
    match kind_of_term c with
      | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> 
	  whrec (existential_value sigma (ev,args), l)
      | Cast (c,_) -> whrec (c, l)
      | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
      | _ -> s
  in 
  whrec (c, [])

let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c)

let nf_evar = Pretype_errors.nf_evar
let j_nf_evar = Pretype_errors.j_nf_evar
let jl_nf_evar = Pretype_errors.jl_nf_evar
let jv_nf_evar = Pretype_errors.jv_nf_evar
let tj_nf_evar = Pretype_errors.tj_nf_evar

(**********************)
(* Creating new evars *)
(**********************)

let evar_env evd = Global.env_of_context evd.evar_hyps

(* Generator of existential names *)
let new_evar =
  let evar_ctr = ref 0 in
  fun () -> incr evar_ctr; !evar_ctr

let make_evar_instance env =
  fold_named_context
    (fun env (id, b, _) l -> (*if b=None then*) mkVar id :: l (*else l*))
    env ~init:[]

(* create an untyped existential variable *)
let new_evar_in_sign env =
  let ev = new_evar () in
  mkEvar (ev, Array.of_list (make_evar_instance env))

(*------------------------------------*
 * functional operations on evar sets *
 *------------------------------------*)

(* All ids of sign must be distincts! *)
let new_isevar_sign env sigma typ instance =
  let sign = named_context env in
  if not (list_distinct (ids_of_named_context sign)) then 
    error "new_isevar_sign: two vars have the same name";
  let newev = new_evar() in
  let info = { evar_concl = typ; evar_hyps = sign; 
	       evar_body = Evar_empty } in
  (Evd.add sigma newev info, mkEvar (newev,Array.of_list instance))

(* We don't try to guess in which sort the type should be defined, since
   any type has type Type. May cause some trouble, but not so far... *)
let new_Type () = mkType (new_univ ())

let new_Type_sort () = Type (new_univ ())

let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
(*
let new_Type () = mkType dummy_univ

let new_Type_sort () = Type dummy_univ

let judge_of_new_Type () = 
  { uj_val = mkSort (Type dummy_univ);
    uj_type = mkSort (Type dummy_univ) }
*)

(* This refreshes universes in types; works only for inferred types (i.e. for
   types of the form (x1:A1)...(xn:An)B with B a sort or an atom in
   head normal form) *)
let refresh_universes t =
  let modified = ref false in
  let rec refresh t = match kind_of_term t with
    | Sort (Type _) -> modified := true; new_Type ()
    | Prod (na,u,v) -> mkProd (na,u,refresh v)
    | _ -> t in
  let t' = refresh t in
  if !modified then t' else t

(* Declaring any type to be in the sort Type shouldn't be harmful since
   cumulativity now includes Prop and Set in Type. *)
let new_type_var env sigma =
  let instance = make_evar_instance env in
  let (sigma',c) = new_isevar_sign env sigma (new_Type ()) instance in
  (sigma', c)

let split_evar_to_arrow sigma (ev,args) =
  let evd = Evd.map sigma ev in
  let evenv = evar_env evd in
  let (sigma1,dom) = new_type_var evenv sigma in
  let hyps = evd.evar_hyps in
  let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in
  let newenv = push_named_decl (nvar, None, dom) evenv in
  let (sigma2,rng) = new_type_var newenv sigma1 in
  let x = named_hd newenv dom Anonymous in
  let prod = mkProd (x, dom, subst_var nvar rng) in
  let sigma3 = Evd.define sigma2 ev prod in
  let evdom = fst (destEvar dom), args in
  let evrng =
    fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
  let prod' = mkProd (x, mkEvar evdom, mkEvar evrng) in
  (sigma3, prod', evdom, evrng)

let define_evar_as_arrow sigma ev =
  let (sigma, prod, _, _) = split_evar_to_arrow sigma ev in
  (sigma, prod)

let define_evar_as_sort sigma (ev,args) =
  let s = new_Type () in
  let sigma = Evd.define sigma ev s in
  (sigma, destSort s)

{'fraction_non_alphanumeric': 0.1549920198616776, 'fraction_numerical': 0.002482709700301472, 'mean_word_length': 3.2498116051243406, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 41, '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': '3179902', 'n_tokens_mistral': 4122, 'n_tokens_neox': 3979, 'n_words': 1328}