Commit b78caa70 authored by Francois Bobot's avatar Francois Bobot

centralisation des report d'erreur

parent 8d14aede
......@@ -93,7 +93,7 @@ LIBGENERATED = src/util/rc.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
src/driver/driver_parser.output src/driver/driver_lexer.ml
LIB_UTIL = pp loc print_tree hashweak hashcons util sysutil rc
LIB_UTIL = exn_printer pp loc print_tree hashweak hashcons util sysutil rc
LIB_CORE = ident ty term pattern decl theory task pretty trans env
......
......@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
# 21 "src/config.ml.in"
let why_version = "@VERSION@"
let why_builddate = "@BUILDDATE@"
let why_plugins = ("@enable_plugins@" = "yes")
......@@ -33,4 +35,3 @@ end
module Dynlink = struct
include @DYNLINK@
end
......@@ -534,3 +534,14 @@ let known_add_decl kn d =
ignore (check_match kn d);
kn
let () = Exn_printer.register
(fun fmt exn -> match exn with
| UnknownIdent i ->
fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_string
| UnboundVars vs ->
fprintf fmt "anomaly: unknown vars [%a]"
(Pp.print_iter1 Term.Svs.iter Pp.semi
(fun fmt vs -> pp_print_string fmt vs.vs_name.Ident.id_string)) vs
(* TODO other exceptions *)
| _ -> raise exn)
......@@ -121,3 +121,10 @@ let list_formats () =
Hashtbl.iter add suffixes_table;
Hashtbl.fold (fun p l acc -> (p, l) :: acc) h []
let () = Exn_printer.register
(fun fmt exn -> match exn with
| UnknownFormat p -> Format.fprintf fmt "unknown format '%s'" p
| _ -> raise exn)
......@@ -129,7 +129,7 @@ let ty_any pr ty =
(* smart constructors *)
exception BadTypeArity of int * int
exception BadTypeArity of tysymbol * int * int
exception DuplicateTypeVar of tvsymbol
exception UnboundTypeVars of Stv.t
......@@ -158,7 +158,7 @@ let rec tv_inst m ty = match ty.ty_node with
let ty_app s tl =
let tll = List.length tl in
let stl = List.length s.ts_args in
if tll <> stl then raise (BadTypeArity (stl,tll));
if tll <> stl then raise (BadTypeArity (s,stl,tll));
match s.ts_def with
| Some ty ->
let add m v t = Mtv.add v t m in
......@@ -225,3 +225,28 @@ let ty_tuple tyl =
ty_app (ts_tuple (List.length tyl)) tyl
let is_ts_tuple ts = ts == ts_tuple (List.length ts.ts_args)
open Format
let print_tv fmt tv = pp_print_string fmt tv.tv_name.id_string
let print_ts fmt ts = pp_print_string fmt ts.ts_name.id_string
let rec print_ty fmt ty = match ty.ty_node with
| Tyvar v -> print_tv fmt v
| Tyapp (ts, []) -> print_ts fmt ts
| Tyapp (ts, [t]) -> fprintf fmt "%a@ %a" print_ty t print_ts ts
| Tyapp (ts, l) -> fprintf fmt "(%a)@ %a"
(Pp.print_list Pp.comma print_ty) l print_ts ts
let () = Exn_printer.register
(fun fmt exn -> match exn with
| TypeMismatch (t1,t2) ->
Format.fprintf fmt "Type mismatch between %a and %a"
print_ty t1 print_ty t2
| BadTypeArity(ts, ts_arg, app_arg) ->
Format.fprintf fmt
"Bad type arity type symbol %a is applied \
with %i arguments instead of %i"
print_ts ts ts_arg app_arg
| _ -> raise exn)
......@@ -65,7 +65,7 @@ module Wty : Hashweak.S with type key = ty
val ts_equal : tysymbol -> tysymbol -> bool
val ty_equal : ty -> ty -> bool
exception BadTypeArity of int * int
exception BadTypeArity of tysymbol * int * int
exception DuplicateTypeVar of tvsymbol
exception UnboundTypeVars of Stv.t
......
......@@ -36,6 +36,11 @@ exception Error of error
let report = pp_print_string
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Error error -> report fmt error
| _ -> raise exn)
let error ?loc e = match loc with
| None -> raise (Error e)
| Some loc -> raise (Loc.Located (loc, Error e))
......
......@@ -29,6 +29,11 @@ exception Error of error
let report = pp_print_string
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Error error -> report fmt error
| _ -> raise exn)
let error e = raise (Error e)
let errorm f =
......
......@@ -203,6 +203,11 @@ let report fmt = function
| NotImplemented (s) ->
Format.fprintf fmt "@[<hov 3> Unimplemented feature:@\n%s@]@\n" s
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Error error -> report fmt error
| _ -> raise exn)
(** function which cath inner error *)
exception Unsupported of string
......
......@@ -82,6 +82,11 @@ let report fmt = function
| DuplicateProver s ->
fprintf fmt "prover %s is already listed" s
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Error error -> report fmt error
| _ -> raise exn)
(* Configuration file *)
type config_prover = {
......
......@@ -267,37 +267,6 @@ let memlimit = match !opt_memlimit with
let debug = !opt_debug
let rec report fmt = function
| Loc.Located (loc, e) ->
fprintf fmt "%a%a" Loc.report_position loc report e
| Lexer.Error e ->
fprintf fmt "lexical error: %a" Lexer.report e;
| Parsing.Parse_error ->
fprintf fmt "syntax error"
| Denv.Error e ->
Denv.report fmt e
| Typing.Error e ->
Typing.report fmt e
| Decl.UnknownIdent i ->
fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_string
| Decl.UnboundVars vs ->
fprintf fmt "anomaly: unknown vars [%a]"
(Pp.print_iter1 Term.Svs.iter Pp.semi Pretty.print_vs) vs
| Driver.Error e ->
Driver.report fmt e
| Config.Dynlink.Error e ->
fprintf fmt "Dynlink: %s" (Config.Dynlink.error_message e)
| Whyconf.Error e ->
fprintf fmt "Why config: %a" Whyconf.report e
| Prover.Error e ->
Prover.report fmt e
| Register.Error e ->
Register.report fmt e
| Env.UnknownFormat p ->
fprintf fmt "unknown format '%s'" p
| e ->
fprintf fmt "anomaly: %s" (Printexc.to_string e)
let print_th_namespace fmt th =
Pretty.print_namespace fmt th.th_name.Ident.id_string th.th_export
......@@ -437,7 +406,7 @@ let () =
let drv = Util.option_map (load_driver env) !opt_driver in
Queue.iter (do_input env drv) opt_queue
with e when not debug ->
eprintf "%a@." report e;
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
(*
......
......@@ -39,6 +39,10 @@ let report fmt = function
| AnyMessage s ->
fprintf fmt "%s" s
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Error error -> report fmt error
| _ -> raise exn)
(** types with destructive type variables *)
......
......@@ -38,6 +38,13 @@
| UnterminatedComment -> fprintf fmt "unterminated comment"
| UnterminatedString -> fprintf fmt "unterminated string"
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Error error -> report fmt error
| _ -> raise exn)
let keywords = Hashtbl.create 97
let () =
List.iter
......
......@@ -41,6 +41,12 @@
let infix s = "infix " ^ s
let prefix s = "prefix " ^ s
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Parsing.Parse_error -> Format.fprintf fmt "syntax error"
| _ -> raise exn
)
%}
/* Tokens */
......
......@@ -112,6 +112,11 @@ let report fmt = function
| UnboundSymbol sl ->
fprintf fmt "Unbound symbol '%a'" (print_list dot pp_print_string) sl
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Error error -> report fmt error
| _ -> raise exn)
(** Environments *)
(** typing using destructive type variables
......@@ -726,7 +731,7 @@ let add_types dl th =
in
begin try
ty_app ts (List.map apply tyl)
with Ty.BadTypeArity (tsal, tyll) ->
with Ty.BadTypeArity (_, tsal, tyll) ->
error ~loc:(qloc q) (TypeArity (q, tsal, tyll))
end
| PPTtuple tyl ->
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
type exn_printer = Format.formatter -> exn -> unit
let exn_printers =
(Stack.create () : (Format.formatter -> exn -> unit) Stack.t)
let register exn_printer = Stack.push exn_printer exn_printers
let () =
let all_exn_printer fmt exn =
Format.fprintf fmt "anomaly: %s" (Printexc.to_string exn) in
register all_exn_printer
exception Exit_loop
let exn_printer fmt exn =
let test f = try f fmt exn; raise Exit_loop
with Exit_loop -> raise Exit_loop
| _ -> () in
try
Stack.iter test exn_printers
with Exit_loop -> ()
(** For Config *)
let () = register
(fun fmt exn -> match exn with
| Config.Dynlink.Error error ->
Format.fprintf fmt "Dynlink: %s" (Config.Dynlink.error_message error)
| _ -> raise exn)
......@@ -107,6 +107,11 @@ let report_obligation_position ?(onlybasename=false) fmt loc =
let current_offset = ref 0
let reloc p = { p with pos_cnum = p.pos_cnum + !current_offset }
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Located (loc,e) ->
fprintf fmt "%a%a" report_position loc Exn_printer.exn_printer e
| _ -> raise exn)
(*
(* Identifiers localization *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment