<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 Term
open Inductive
open Names
open Reductionops
open Environ
open Typeops
open Declarations
open Instantiate

type metamap = (int * constr) list

let outsort env sigma t =
  match kind_of_term (whd_betadeltaiota env sigma t) with
    | Sort s -> s
    | _ -> anomaly "Retyping: found a type of type which is not a sort"

let rec subst_type env sigma typ = function
  | [] -> typ
  | h::rest ->
      match kind_of_term (whd_betadeltaiota env sigma typ) with
        | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest
        | _ -> anomaly "Non-functional construction"

(* Si ft est le type d'un terme f, lequel est appliqu  args, *)
(* [sort_of_atomic_ty] calcule ft[args] qui doit tre une sorte *)
(* On suit une mthode paresseuse, en esprant que ft est une arit *)
(* et sinon on substitue *)

let sort_of_atomic_type env sigma ft args =
  let rec concl_of_arity env ar =
    match kind_of_term (whd_betadeltaiota env sigma ar) with
      | Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b
      | Sort s -> s
      | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args))
  in concl_of_arity env ft

let typeur sigma metamap =
  let rec type_of env cstr=
    match kind_of_term cstr with
    | Meta n ->
          (try strip_outer_cast (List.assoc n metamap)
           with Not_found -> anomaly "type_of: this is not a well-typed term")
    | Rel n ->
        let (_,_,ty) = lookup_rel n env in
        lift n (body_of_type ty)
    | Var id ->
        let (_,_,ty) = lookup_named id env in
        (try body_of_type ty
        with Not_found ->
          anomaly ("type_of: variable "^(string_of_id id)^" unbound"))
    | Const c ->
        let cb = lookup_constant c env in
        body_of_type cb.const_type
    | Evar ev -> existential_type sigma ev
    | Ind ind -> body_of_type (type_of_inductive env ind)
    | Construct cstr -> body_of_type (type_of_constructor env cstr)
    | Case (_,p,c,lf) ->
        (* TODO: could avoid computing the type of branches *)
        let i =
          try find_rectype env (type_of env c)
          with Induc -> anomaly "type_of: Bad recursive type" in
        let pj = { uj_val = p; uj_type = type_of env p } in
        let (_,ty,_) = type_case_branches env i pj c in
        ty
    | Lambda (name,c1,c2) ->
          mkProd (name, c1, type_of (push_rel (name,None,c1) env) c2)
    | LetIn (name,b,c1,c2) ->
         subst1 b (type_of (push_rel (name,Some b,c1) env) c2)
    | Fix ((_,i),(_,tys,_)) -> tys.(i)<commit_msg>exceptionmal ratrappee<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 Term
open Inductive
open Names
open Reductionops
open Environ
open Typeops
open Declarations
open Instantiate

type metamap = (int * constr) list

let outsort env sigma t =
  match kind_of_term (whd_betadeltaiota env sigma t) with
    | Sort s -> s
    | _ -> anomaly "Retyping: found a type of type which is not a sort"

let rec subst_type env sigma typ = function
  | [] -> typ
  | h::rest ->
      match kind_of_term (whd_betadeltaiota env sigma typ) with
        | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest
        | _ -> anomaly "Non-functional construction"

(* Si ft est le type d'un terme f, lequel est appliqu  args, *)
(* [sort_of_atomic_ty] calcule ft[args] qui doit tre une sorte *)
(* On suit une mthode paresseuse, en esprant que ft est une arit *)
(* et sinon on substitue *)

let sort_of_atomic_type env sigma ft args =
  let rec concl_of_arity env ar =
    match kind_of_term (whd_betadeltaiota env sigma ar) with
      | Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b
      | Sort s -> s
      | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args))
  in concl_of_arity env ft

let typeur sigma metamap =
  let rec type_of env cstr=
    match kind_of_term cstr with
    | Meta n ->
          (try strip_outer_cast (List.assoc n metamap)
           with Not_found -> anomaly "type_of: this is not a well-typed term")
    | Rel n ->
        let (_,_,ty) = lookup_rel n env in
        lift n (body_of_type ty)
    | Var id ->
        (try
          let (_,_,ty) = lookup_named id env in
          body_of_type ty
        with Not_found ->
          anomaly ("type_of: variable "^(string_of_id id)^" unbound"))
    | Const c ->
        let cb = lookup_constant c env in
        body_of_type cb.const_type
    | Evar ev -> existential_type sigma ev
    | Ind ind -> body_of_type (type_of_inductive env ind)
    | Construct cstr -> body_of_type (type_of_constructor env cstr)
    | Case (_,p,c,lf) ->
        (* TODO: could avoid computing the type of branches *)
        let i =
          try find_rectype env (type_of env c)
          with Induc -> anomaly "type_of: Bad recursive type" in
        let pj = { uj_val = p; uj_type = type_of env p } in
        let (_,ty,_) = type_case_branches env i pj c in
        ty
    | Lambda (name,c1,c2) ->
          mkProd (name, c1, type_of (push_rel (name,None,c1) env) c2)
    | LetIn (name,b,c1,c2) ->
         subst1 b (type_of (push_rel (name,Some b,c1) env) c2)
    | Fix ((_,i),(_,tys,_)) -> tys.(i)
{'fraction_non_alphanumeric': 0.16096057115041376, 'fraction_numerical': 0.005192276488723025, 'mean_word_length': 2.6646848989298455, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 49, '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': '2843383', 'n_tokens_mistral': 2082, 'n_tokens_neox': 2011, 'n_words': 686}