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

open Compat
open Pp
open Util
open Indtypes
open Type_errors
open Pretype_errors
open Indrec

let print_loc loc =
  if loc = dummy_loc then
    (str"<unknown>")
  else
    let loc = unloc loc in
    (int (fst loc) ++ str"-" ++ int (snd loc))

let guill s = "\""^s^"\""

let where s =
  if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())

exception EvaluatedError of std_ppcmds * exn option

(* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)

let rec explain_exn_default_aux anomaly_string report_fn = function
  | Stream.Failure ->
      hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
  | Stream.Error txt ->
      hov 0 (str "Syntax error: " ++ str txt ++ str ".")
  | Token.Error txt ->
      hov 0 (str "Syntax error: " ++ str txt ++ str ".")
  | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err))
  | Sys_error msg ->
      hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ())
  | UserError(s,pps) ->
      hov 0 (str "Error: " ++ where s ++ pps)
  | Out_of_memory ->
      hov 0 (str "Out of memory.")
  | Stack_overflow ->
      hov 0 (str "Stack overflow.")
  | Timeout ->
      hov 0 (str "Timeout!")
  | Anomaly (s,pps) ->
      hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
  | AnomalyOnError (s,exc) ->
      hov 0 (anomaly_string () ++ str s ++ str ". Received exception is:" ++
	fnl() ++ explain_exn_default_aux anomaly_string report_fn exc)
  | Match_failure(filename,pos1,pos2) ->
      hov 0 (anomaly_string () ++ str "Match failure in file " ++
	     str (guill filename) ++ str " at line " ++ int pos1 ++
	     str " character " ++ int pos2 ++ report_fn ())
  | Not_found ->
      hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report_fn ())
  | Failure s ->
      hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report_fn ())
  | Invalid_argument s ->
      hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ())
  | Sys.Break ->
      hov 0 (fnl () ++ str "User interrupt.")
  | Loc.Exc_located (loc,exc) ->
      hov 0 ((if loc = dummy_loc then (mt ())
               else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
               ++ explain_exn_default_aux anomaly_string report_fn exc)
  | Assert_failure (s,b,e) ->
      hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
	       (if s = "" then mt ()
		else
		  (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
		   str ", characters " ++ int e ++ str "-" ++
		   int (e+6) ++ str ")")) ++
	       report_fn ())
  | EvaluatedError (msg,None) ->
      msg
  | EvaluatedError (msg,Some reraise) ->
      msg ++ explain_exn_default_aux anomaly_string report_fn reraise
  | reraise ->
      hov 0 (anomaly_string () ++ str "Uncaught exception " ++
	       str (Printexc.to_string reraise) ++ report_fn ())

let wrap_vernac_error strm =
  EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None)

let rec process_vernac_interp_error = function
  | Univ.UniverseInconsistency (o,u,v) ->
      let msg =
	if !Constrextern.print_universes then
	  spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
          str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=")
	  ++ spc() ++ Univ.pr_uni v ++ str")"
	else
	  mt() in
      wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".")
  | TypeError(ctx,te) ->
      wrap_vernac_error (Himsg.explain_type_error ctx te)<commit_msg>correcting a non catch error reported as an anomaly (Ploc.Exc)<commit_after>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Compat
open Pp
open Util
open Indtypes
open Type_errors
open Pretype_errors
open Indrec

let print_loc loc =
  if loc = dummy_loc then
    (str"<unknown>")
  else
    let loc = unloc loc in
    (int (fst loc) ++ str"-" ++ int (snd loc))

let guill s = "\""^s^"\""

let where s =
  if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())

exception EvaluatedError of std_ppcmds * exn option

(* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)

let rec explain_exn_default_aux anomaly_string report_fn = function
  | Stream.Failure ->
      hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
  | Stream.Error txt ->
      hov 0 (str "Syntax error: " ++ str txt ++ str ".")
  | Token.Error txt ->
      hov 0 (str "Syntax error: " ++ str txt ++ str ".")
  | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err))
  | Sys_error msg ->
      hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ())
  | UserError(s,pps) ->
      hov 0 (str "Error: " ++ where s ++ pps)
  | Out_of_memory ->
      hov 0 (str "Out of memory.")
  | Stack_overflow ->
      hov 0 (str "Stack overflow.")
  | Timeout ->
      hov 0 (str "Timeout!")
  | Anomaly (s,pps) ->
      hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
  | AnomalyOnError (s,exc) ->
      hov 0 (anomaly_string () ++ str s ++ str ". Received exception is:" ++
	fnl() ++ explain_exn_default_aux anomaly_string report_fn exc)
  | Match_failure(filename,pos1,pos2) ->
      hov 0 (anomaly_string () ++ str "Match failure in file " ++
	     str (guill filename) ++ str " at line " ++ int pos1 ++
	     str " character " ++ int pos2 ++ report_fn ())
  | Not_found ->
      hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report_fn ())
  | Failure s ->
      hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report_fn ())
  | Invalid_argument s ->
      hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ())
  | Sys.Break ->
      hov 0 (fnl () ++ str "User interrupt.")
  | Loc.Exc_located (loc,exc) ->
      hov 0 ((if loc = dummy_loc then (mt ())
               else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
               ++ explain_exn_default_aux anomaly_string report_fn exc)
  | Assert_failure (s,b,e) ->
      hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
	       (if s = "" then mt ()
		else
		  (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
		   str ", characters " ++ int e ++ str "-" ++
		   int (e+6) ++ str ")")) ++
	       report_fn ())
  | EvaluatedError (msg,None) ->
      msg
  | EvaluatedError (msg,Some reraise) ->
      msg ++ explain_exn_default_aux anomaly_string report_fn reraise
  | Ploc.Exc(loc,exc) -> 
      hov 0 ((if loc = dummy_loc then (mt ())
               else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
               ++ explain_exn_default_aux anomaly_string report_fn exc)
  | reraise ->
      hov 0 (anomaly_string () ++ str "Uncaught exception " ++
	       str (Printexc.to_string reraise) ++ report_fn ())

let wrap_vernac_error strm =
  EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None)

let rec process_vernac_interp_error = function
  | Univ.UniverseInconsistency (o,u,v) ->
      let msg =
	if !Constrextern.print_universes then
	  spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
          str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=")
	  ++ spc() ++ Univ.pr_uni v ++ str")"
	else
	  mt() in
      wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".")
  | TypeError(ctx,te) ->
      wrap_vernac_error (Himsg.explain_type_error ctx te)
{'fraction_non_alphanumeric': 0.19756010896600734, 'fraction_numerical': 0.008409333175411584, 'mean_word_length': 2.843422849340009, 'pattern_counts': {'":': 5, '<': 11, '<?xml version=': 0, '>': 58, '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': '5283332', 'n_tokens_mistral': 2955, 'n_tokens_neox': 2723, 'n_words': 821}