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

open Pp
open CErrors
open Util
open Names
open Nameops
open Term
open Vars
open Termops
open Namegen
open Declarations
open Inductiveops
open Environ
open Reductionops
open Type_errors
open Glob_term
open Glob_ops
open Retyping
open Pretype_errors
open Evarutil
open Evardefine
open Evarsolve
open Evarconv
open Evd
open Sigma.Notations
open Context.Rel.Declaration

module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration

(* Pattern-matching errors *)

type pattern_matching_error =
  | BadPattern of constructor * constr
  | BadConstructor of constructor * inductive
  | WrongNumargConstructor of constructor * int
  | WrongNumargInductive of inductive * int
  | UnusedClause of cases_pattern list
  | NonExhaustive of cases_pattern list
  | CannotInferPredicate of (constr * types) array

exception PatternMatchingError of env * evar_map * pattern_matching_error

let raise_pattern_matching_error ?loc (env,sigma,te) =
  Loc.raise ?loc (PatternMatchingError(env,sigma,te))

let error_bad_pattern ?loc env sigma cstr ind =
  raise_pattern_matching_error ?loc
    (env, sigma, BadPattern (cstr,ind))

let error_bad_constructor ?loc env cstr ind =
  raise_pattern_matching_error
    (env, Evd.empty, BadConstructor (cstr,ind))

let error_wrong_numarg_constructor ?loc env c n =
  raise_pattern_matching_error (env, Evd.empty, WrongNumargConstructor(c,n))

let error_wrong_numarg_inductive ?loc env c n =
  raise_pattern_matching_error (env, Evd.empty, WrongNumargInductive(c,n))

let rec list_try_compile f = function
  | [a] -> f a
  | [] -> anomaly (str "try_find_f")
  | h::t ->
      try f h
      with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ ->
	    list_try_compile f t

let force_name =
  let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na
<commit_msg>Propagate location info on pattern match compilation.<commit_after>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open CErrors
open Util
open Names
open Nameops
open Term
open Vars
open Termops
open Namegen
open Declarations
open Inductiveops
open Environ
open Reductionops
open Type_errors
open Glob_term
open Glob_ops
open Retyping
open Pretype_errors
open Evarutil
open Evardefine
open Evarsolve
open Evarconv
open Evd
open Sigma.Notations
open Context.Rel.Declaration

module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration

(* Pattern-matching errors *)

type pattern_matching_error =
  | BadPattern of constructor * constr
  | BadConstructor of constructor * inductive
  | WrongNumargConstructor of constructor * int
  | WrongNumargInductive of inductive * int
  | UnusedClause of cases_pattern list
  | NonExhaustive of cases_pattern list
  | CannotInferPredicate of (constr * types) array

exception PatternMatchingError of env * evar_map * pattern_matching_error

let raise_pattern_matching_error ?loc (env,sigma,te) =
  Loc.raise ?loc (PatternMatchingError(env,sigma,te))

let error_bad_pattern ?loc env sigma cstr ind =
  raise_pattern_matching_error ?loc
    (env, sigma, BadPattern (cstr,ind))

let error_bad_constructor ?loc env cstr ind =
  raise_pattern_matching_error ?loc
    (env, Evd.empty, BadConstructor (cstr,ind))

let error_wrong_numarg_constructor ?loc env c n =
  raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargConstructor(c,n))

let error_wrong_numarg_inductive ?loc env c n =
  raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargInductive(c,n))

let rec list_try_compile f = function
  | [a] -> f a
  | [] -> anomaly (str "try_find_f")
  | h::t ->
      try f h
      with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ ->
	    list_try_compile f t

let force_name =
  let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na

{'fraction_non_alphanumeric': 0.1533678756476684, 'fraction_numerical': 0.004145077720207254, 'mean_word_length': 4.39217877094972, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 15, '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': '4395957', 'n_tokens_mistral': 1491, 'n_tokens_neox': 1398, 'n_words': 441}