use Exn_printer-based exception handling everywhere

TODO

@@ -24,3 +24,9 @@ s
   - open (et échouer si "open A" et "open B" avec A et B déclarant un symbole 
     de même nom)
 
+error reporting
+---------------
+
+  - should we create a common [exception Why.Error of exn] to facilitate
+    integration of the library? This would require a special [raise] call:
+        why_raise e = raise (Why.Error e)

src/core/env.mli

@@ -45,8 +45,7 @@ val register_format :
   string -> string list -> read_channel -> unit
   (** [register_format name extensions f1 f2] registers a new format
       under name [name], for files with extensions in list [extensions];
-      [f1] is the function to perform parsing;
-      [f2] is the function to report errors *)
+      [f1] is the function to perform parsing *)
 
 val read_channel : ?name:string -> read_channel
 

src/driver/driver_lexer.mll

@@ -23,6 +23,12 @@
   open Driver_parser
   open Lexer
 
+  exception IllegalCharacter of char
+
+  let () = Exn_printer.register (fun fmt e -> match e with
+    | IllegalCharacter c -> fprintf fmt "illegal character %c" c
+    | _ -> raise e)
+
   let keywords = Hashtbl.create 97
   let () =
     List.iter
@@ -88,7 +94,7 @@ rule token = parse
   | eof
       { EOF }
   | _ as c
-      { raise (Error (IllegalCharacter c)) }
+      { raise (IllegalCharacter c) }
 
 {
   let loc lb = (lexeme_start_p lb, lexeme_end_p lb)

src/driver/whyconf.ml

@@ -22,26 +22,23 @@ open Util
 
 (* Error handling *)
 
-type error =
-  | SyntaxError
-  | ExtraParameters of string
-  | MissingParameters of string
-  | UnknownSection of string
-  | UnknownField of string
-  | MissingSection of string
-  | MissingField of string
-  | DuplicateSection of string
-  | DuplicateField of string * Rc.rc_value * Rc.rc_value
-  | StringExpected of string * Rc.rc_value
-  | IdentExpected of string * Rc.rc_value
-  | IntExpected of string * Rc.rc_value
-  | DuplicateProver of string
-
-exception Error of error
+exception SyntaxError
+exception ExtraParameters of string
+exception MissingParameters of string
+exception UnknownSection of string
+exception UnknownField of string
+exception MissingSection of string
+exception MissingField of string
+exception DuplicateSection of string
+exception DuplicateField of string * Rc.rc_value * Rc.rc_value
+exception StringExpected of string * Rc.rc_value
+exception IdentExpected of string * Rc.rc_value
+exception IntExpected of string * Rc.rc_value
+exception DuplicateProver of string
 
 let error ?loc e = match loc with
-  | None -> raise (Error e)
-  | Some loc -> raise (Loc.Located (loc, Error e))
+  | None -> raise e
+  | Some loc -> raise (Loc.Located (loc, e))
 
 let print_rc_value fmt = function
   | Rc.RCint i -> fprintf fmt "%d" i
@@ -50,7 +47,7 @@ let print_rc_value fmt = function
   | Rc.RCstring s -> fprintf fmt "\"%s\"" s
   | Rc.RCident s -> fprintf fmt "%s" s
 
-let report fmt = function
+let () = Exn_printer.register (fun fmt e -> match e with
   | SyntaxError ->
       fprintf fmt "syntax error"
   | ExtraParameters s ->
@@ -81,11 +78,7 @@ let report fmt = function
         s print_rc_value v
   | 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)
+  | e -> raise e)
 
 (* Configuration file *)
 

src/driver/whyconf.mli

@@ -43,11 +43,3 @@ val read_config : string option -> config
 
 val save_config : config -> unit
 
-(** error reporting *)
-
-type error
-
-exception Error of error
-
-val report : Format.formatter -> error -> unit
-

src/ide/gmain.ml

@@ -33,12 +33,11 @@ let config =
   try 
     Whyconf.read_config None
   with 
-      Not_found -> 
+    | Not_found ->
         eprintf "%s No config file found.@." pname;
         exit 1
-    | Whyconf.Error e ->
-        eprintf "%s Error while reading config file: %a@." pname 
-          Whyconf.report e;
+    | e ->
+        eprintf "%a@." Exn_printer.exn_printer e;
         exit 1
 
 let () = eprintf "%s Load path is: %a@." pname
@@ -113,28 +112,6 @@ let env = Why.Env.create_env (Why.Typing.retrieve config.loadpath)
 (***********************)
 (* Parsing input file  *)
 (***********************)
-   
-let rec report fmt = function
-  | Lexer.Error e ->
-      fprintf fmt "lexical error: %a" Lexer.report e;
-  | Loc.Located (loc, e) ->
-      fprintf fmt "%a%a" Loc.report_position loc 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
-(*
-  | Driver.Error e ->
-      Driver.report fmt e
-*)
-  | Config.Dynlink.Error e ->
-      fprintf fmt "Dynlink : %s" (Config.Dynlink.error_message e)
-  | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
-
 
 let theories : Theory.theory Theory.Mnm.t =
   try
@@ -144,7 +121,7 @@ let theories : Theory.theory Theory.Mnm.t =
     eprintf "Parsing/Typing Ok@.";
     m
   with e -> 
-    eprintf "%a@." report e;
+    eprintf "%a@." Exn_printer.exn_printer e;
     exit 1
 
 (********************)

src/manager/db.ml

@@ -1142,16 +1142,6 @@ let try_prover ~(async:(unit->unit)->unit)
           (Why.Driver.print_task driver) g.task;
       Why.Driver.prove_task ~debug ~command ~timelimit ~memlimit driver g.task
     with
-(*
-    | Why.Driver.Error e ->
-        Format.eprintf "Db.try_prover: prove_task reports %a@." 
-          Why.Driver.report e;
-        fun () -> raise Exit
-    | Driver.Error e ->
-        Format.eprintf "Db.try_prover: prove_task reports %a@." 
-          Driver.report e;
-        fun () -> raise Exit
-*)
     | e ->
         try
           Printexc.print (fun () -> raise e) ()

src/manager/gmanager.ml

@@ -33,12 +33,11 @@ let config =
   try 
     Whyconf.read_config None
   with 
-      Not_found -> 
+    | Not_found ->
         eprintf "%s No config file found.@." pname;
         exit 1
-    | Whyconf.Error e ->
-        eprintf "%s Error while reading config file: %a@." pname 
-          Whyconf.report e;
+    | e ->
+        eprintf "%a@." Exn_printer.exn_printer e;
         exit 1
 
 let () = eprintf "%s Load path is: %a@." pname
@@ -115,28 +114,6 @@ let env = Why.Env.create_env (Why.Typing.retrieve config.loadpath)
 (* Parsing input file  *)
 (***********************)
    
-let rec report fmt = function
-  | Lexer.Error e ->
-      fprintf fmt "lexical error: %a" Lexer.report e;
-  | Loc.Located (loc, e) ->
-      fprintf fmt "%a%a" Loc.report_position loc 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
-(*
-  | Driver.Error e ->
-      Driver.report fmt e
-*)
-  | Config.Dynlink.Error e ->
-      fprintf fmt "Dynlink : %s" (Config.Dynlink.error_message e)
-  | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
-
-
 let theories : Theory.theory Theory.Mnm.t =
   try
     let cin = open_in fname in
@@ -145,7 +122,7 @@ let theories : Theory.theory Theory.Mnm.t =
     eprintf "Parsing/Typing Ok@.";
     m
   with e -> 
-    eprintf "%a@." report e;
+    eprintf "%a@." Exn_printer.exn_printer e;
     exit 1
 
 (********************)

src/manager/test.ml

@@ -72,8 +72,8 @@ let config =
         autodetection ();
 *)
         exit 1
-    | Whyconf.Error e ->
-        eprintf "Error while reading config file: %a@." Whyconf.report e;
+    | e ->
+        eprintf "%a@." Exn_printer.exn_printer e;
         exit 1
 
 let () = printf "Load path is: %a@." (Pp.print_list Pp.comma Pp.string) config.loadpath
@@ -126,28 +126,6 @@ let () =
 (***********************)
 (* Parsing input file  *)
 (***********************)
-   
-let rec report fmt = function
-  | Lexer.Error e ->
-      fprintf fmt "lexical error: %a" Lexer.report e;
-  | Loc.Located (loc, e) ->
-      fprintf fmt "%a%a" Loc.report_position loc 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
-(*
-  | Driver.Error e ->
-      Driver.report fmt e
-*)
-  | Config.Dynlink.Error e ->
-      fprintf fmt "Dynlink : %s" (Config.Dynlink.error_message e)
-  | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
-
 
 let m : Theory.theory Theory.Mnm.t =
   try
@@ -157,7 +135,7 @@ let m : Theory.theory Theory.Mnm.t =
     eprintf "Parsing/Typing Ok@.";
     m
   with e -> 
-    eprintf "%a@." report e;
+    eprintf "%a@." Exn_printer.exn_printer e;
     exit 1
 
 (***************************)

src/parser/denv.ml

@@ -26,23 +26,15 @@ open Ty
 open Term
 open Theory
 
-type error = 
-  | AnyMessage of string
-
-exception Error of error
+exception AnyMessage of string
 
 let error ?loc e = match loc with
-  | None -> raise (Error e)
-  | Some loc -> raise (Loc.Located (loc, Error e))
-
-let report fmt = function
-  | AnyMessage s ->
-      fprintf fmt "%s" s
+  | None -> raise e
+  | Some loc -> raise (Loc.Located (loc,e))
 
-let () = Exn_printer.register
-  (fun fmt exn -> match exn with
-    | Error error -> report fmt error
-    | _ -> raise exn)
+let () = Exn_printer.register (fun fmt e -> match e with
+  | AnyMessage s -> fprintf fmt "%s" s
+  | _ -> raise e)
 
 (** types with destructive type variables *)
 

src/parser/denv.mli

@@ -95,12 +95,3 @@ val specialize_term : loc:Ptree.loc -> type_var Htv.t -> term -> dterm
 
 val specialize_fmla : loc:Ptree.loc -> type_var Htv.t -> fmla -> dfmla
 
-
-(** Error reporting *)
-
-type error
-
-exception Error of error
-
-val report : Format.formatter -> error -> unit
-

src/parser/lexer.mli

@@ -17,13 +17,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type error = 
-  | IllegalCharacter of char
-  | UnterminatedComment
-  | UnterminatedString
-
-exception Error of error
-
 (** parsing entry points *)
 
 val parse_list0_decl : Lexing.lexbuf -> Ptree.decl list
@@ -39,8 +32,6 @@ val comment : Lexing.lexbuf -> unit
 
 val string : Lexing.lexbuf -> string
 
-val report : Format.formatter -> error -> unit
-
 val remove_leading_plus : string -> string
 
 val with_location : (Lexing.lexbuf -> 'a) -> Lexing.lexbuf -> 'a

src/parser/lexer.mll

@@ -26,24 +26,15 @@
 
   (* lexical errors *)
 
-  type error = 
-    | IllegalCharacter of char
-    | UnterminatedComment
-    | UnterminatedString
+  exception IllegalCharacter of char
+  exception UnterminatedComment
+  exception UnterminatedString
 
-  exception Error of error
-
-  let report fmt = function
+  let () = Exn_printer.register (fun fmt e -> match e with
     | IllegalCharacter c -> fprintf fmt "illegal character %c" c
     | 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)
-
+    | _ -> raise e)
 
   let keywords = Hashtbl.create 97
   let () = 
@@ -220,7 +211,7 @@ rule token = parse
   | eof 
       { EOF }
   | _ as c
-      { raise (Error (IllegalCharacter c)) }
+      { raise (IllegalCharacter c) }
 
 and comment = parse
   | "*)" 
@@ -230,7 +221,7 @@ and comment = parse
   | newline 
       { newline lexbuf; comment lexbuf }
   | eof
-      { raise (Loc.Located (!comment_start_loc, Error UnterminatedComment)) }
+      { raise (Loc.Located (!comment_start_loc,UnterminatedComment)) }
   | _ 
       { comment lexbuf }
 
@@ -244,7 +235,7 @@ and string = parse
   | newline 
       { newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
   | eof
-      { raise (Loc.Located (!string_start_loc, Error UnterminatedString)) }
+      { raise (Loc.Located (!string_start_loc, UnterminatedString)) }
   | _ as c
       { Buffer.add_char string_buf c; string lexbuf }
 

src/parser/typing.ml

@@ -31,31 +31,28 @@ open Denv
 
 (** errors *)
 
-type error =
-  | Message of string
-  | DuplicateTypeVar of string
-  | TypeArity of qualid * int * int
-  | Clash of string
-  | PredicateExpected
-  | TermExpected
-  | BadNumberOfArguments of Ident.ident * int * int
-  | ClashTheory of string
-  | UnboundTheory of qualid
-  | AlreadyTheory of string
-  | UnboundFile of string
-  | UnboundDir of string
-  | AmbiguousPath of string * string
-  | NotInLoadpath of string
-  | CyclicTypeDef
-  | UnboundTypeVar of string
-  | UnboundType of string list
-  | UnboundSymbol of string list
-
-exception Error of error
+exception Message of string
+exception DuplicateTypeVar of string
+exception TypeArity of qualid * int * int
+exception Clash of string
+exception PredicateExpected
+exception TermExpected
+exception BadNumberOfArguments of Ident.ident * int * int
+exception ClashTheory of string
+exception UnboundTheory of qualid
+exception AlreadyTheory of string
+exception UnboundFile of string
+exception UnboundDir of string
+exception AmbiguousPath of string * string
+exception NotInLoadpath of string
+exception CyclicTypeDef
+exception UnboundTypeVar of string
+exception UnboundType of string list
+exception UnboundSymbol of string list
 
 let error ?loc e = match loc with
-  | None -> raise (Error e)
-  | Some loc -> raise (Loc.Located (loc, Error e))
+  | None -> raise e
+  | Some loc -> raise (Loc.Located (loc,e))
 
 let errorm ?loc f =
   let buf = Buffer.create 512 in
@@ -72,7 +69,7 @@ let rec print_qualid fmt = function
   | Qident s -> fprintf fmt "%s" s.id
   | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
 
-let report fmt = function
+let () = Exn_printer.register (fun fmt e -> match e with
   | Message s ->
       fprintf fmt "%s" s
   | DuplicateTypeVar s ->
@@ -111,13 +108,7 @@ let report fmt = function
        fprintf fmt "Unbound type '%a'" (print_list dot pp_print_string) sl
   | 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)
+  | _ -> raise e)
 
 (** Environments *)
 
@@ -359,7 +350,7 @@ and dpat_args s loc env el pl =
   check_arg env (el, pl)
 
 let rec trigger_not_a_term_exn = function
-  | Error TermExpected -> true
+  | TermExpected -> true
   | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
   | _ -> false
 
@@ -881,7 +872,7 @@ and add_decl env lenv th = function
 	  find_theory env lenv q id
 	with
 	  | TheoryNotFound _ -> error ~loc (UnboundTheory use.use_theory)
-	  | Error (AmbiguousPath _ as e) -> error ~loc e
+	  | AmbiguousPath _ as e -> error ~loc e
       in
       let use_or_clone th = match subst with
 	| None ->

src/parser/typing.mli

@@ -32,15 +32,6 @@ val retrieve : string list -> retrieve_theory
 
 val add_decl : env -> theory Mnm.t -> theory_uc -> Ptree.decl -> theory_uc
 
-(** error reporting *)
-
-type error
-
-exception Error of error
-
-val report : Format.formatter -> error -> unit
-
-
 (******************************************************************************)
 (** The following is exported for program typing (src/programs/pgm_typing.ml) *)
 (******************************************************************************)

src/programs/pgm_lexer.mll

@@ -25,13 +25,14 @@
   open Term
   open Pgm_parser
 
-  type error = 
-    | UnterminatedLogic
+  exception UnterminatedLogic
+  exception IllegalCharacter of char
 
-  exception Error of error
-
-  let report fmt = function
+  let () = Exn_printer.register (fun fmt exn -> match exn with
     | UnterminatedLogic -> fprintf fmt "unterminated logic block"
+    | IllegalCharacter c -> fprintf fmt "illegal character %c" c
+    | Parsing.Parse_error -> fprintf fmt "syntax error"
+    | _ -> raise exn)
 
   let keywords = Hashtbl.create 97
   let () = 
@@ -203,7 +204,7 @@ rule token = parse
   | eof 
       { EOF }
   | _ as c
-      { raise (Lexer.Error (IllegalCharacter c)) }
+      { raise (IllegalCharacter c) }
 
 and logic = parse
   | "}"
@@ -213,7 +214,7 @@ and logic = parse
   | newline
       { newline lexbuf; Buffer.add_char logic_buffer '\n'; logic lexbuf }
   | eof
-      { raise (Loc.Located (!logic_start_loc, Error UnterminatedLogic)) }
+      { raise (Loc.Located (!logic_start_loc, UnterminatedLogic)) }
   | _ as c
       { Buffer.add_char logic_buffer c; logic lexbuf }
 

src/programs/pgm_main.ml

@@ -23,16 +23,6 @@ open Format
 open Why
 open Pgm_env
 
-let () = Exn_printer.register
-  (fun fmt exn -> match exn with
-    | Pgm_lexer.Error e ->
-        fprintf fmt "lexical error: %a" Pgm_lexer.report e;
-    | Parsing.Parse_error ->
-        fprintf fmt "syntax error"
-    | Pgm_typing.Error e ->
-        Pgm_typing.report fmt e
-    | _ -> raise exn)
-
 let parse_only _env file c =
   let lb = Lexing.from_channel c in
   Loc.set_file file lb;

src/programs/pgm_typing.ml

@@ -33,14 +33,11 @@ module E = Pgm_effect
 
 let debug = ref false
 
-type error =
-  | Message of string
-
-exception Error of error
+exception Message of string
 
 let error ?loc e = match loc with
-  | None -> raise (Error e)
-  | Some loc -> raise (Loc.Located (loc, Error e))
+  | None -> raise e
+  | Some loc -> raise (Loc.Located (loc, e))
 
 let errorm ?loc f =
   let buf = Buffer.create 512 in
@@ -53,9 +50,9 @@ let errorm ?loc f =
        error ?loc (Message s))
     fmt f
 
-let report fmt = function
-  | Message s ->
-      fprintf fmt "%s" s
+let () = Exn_printer.register (fun fmt e -> match e with
+  | Message s -> fprintf fmt "%s" s
+  | _ -> raise e)
 
 let id_result = "result"
 

src/programs/pgm_typing.mli

@@ -22,12 +22,6 @@ open Theory
 
 val debug : bool ref
 
-type error
-
-exception Error of error
-
-val report : Format.formatter -> error -> unit
-
 val decl : 
   Env.env -> Pgm_env.env -> Pgm_ptree.decl -> Pgm_env.env * Pgm_ttree.decl list
 

src/tptp2why/tptp2why.ml

@@ -17,7 +17,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** this is a tool to convert tptp files (.p files) to .why files *)
+(** this is a parser for tptp problems (.p files) *)
 
 open TptpTree
 
@@ -31,23 +31,13 @@ open TptpTranslate
 (** module to process a single file *)
 module Process : sig
 
-  (** deprecated *)
-  val printFile : Format.formatter -> string -> string -> string -> unit
-
   val read_channel : Env.read_channel
+
 end = struct
 
   let fromInclude = function | Include x -> x | _ -> assert false
   let isInclude = function | Include _ -> true | _ -> false
 
-  (** report errors *)
-  let () = Exn_printer.register (fun fmt exn -> match exn with
-    | TptpLexer.LexicalError (s, pos) ->
-      Format.fprintf fmt "lexical error: %a@." TptpLexer.report (s, pos)
-    | TptpParser.Error ->
-      Format.fprintf fmt "syntax error.@." (*TODO : find how to report pos*)
-    | e -> raise e)
-
   (** for a given file, returns the list of declarations
   for this file and all the files it includes, recursively *)
   let rec getAllDecls ?first:(first=false) include_dir filename =
@@ -86,61 +76,8 @@ end = struct
       let my_theory = theory_of_decls file decls in
       Theory.Mnm.add "Tptp" my_theory Theory.Mnm.empty
 
-
-  (** process a single file and all includes inside *)
-  let printFile fmter include_dir theoryName filename =
-    let decls = getAllDecls ~first:true include_dir filename in
-    let theory = TptpTranslate.theory_of_decls theoryName decls in
-    (* Format.eprintf "translation done@."; *)
-    Pretty.print_theory fmter theory
-
 end
 
-
-
-(*s main function and arg parsing *)
-
-
-
-(** module for options processing *)
-(*module Init = struct
-
-  let input_files = ref []
-  let output_chan = ref (Format.formatter_of_out_channel stdout)
-  let include_dir = ref "."
-
-  let output_updater filename = if filename <> "-"
-    then output_chan := Format.formatter_of_out_channel (open_out filename)
-    else ()
-
-  let include_updater s = include_dir := s
-
-  let options = [
-    ("-o", String output_updater, "outputs to a file");
-    ("-I", String include_updater, "search for included files in this dir");
-    ("-", Unit (fun () -> input_files := "-" :: !input_files), "reads from stdin")
-  ]
-
-  let usage = "tptp2why [file1|-] [file2...] [-o file] [-I dir]
-  It parses tptp files (fof or cnf format) and prints a why file
-  with one theory per input file."
-
-end
-
-open Init *)
-
-(** read options, and process each input file accordingly *)
-(* let () =
-  parse options (fun file -> input_files := file :: (!input_files)) usage;
-  input_files := List.rev !input_files;
-  let theoryCounter = ref 0 in
-  List.iter
-    (fun x -> let theoryName = "Theory"^(string_of_int !theoryCounter) in
-              incr theoryCounter;
-              Process.printFile !output_chan !include_dir theoryName x)
-    !input_files *)
-
-
 (** register as a .p/.ax file parser *)
 let () = Env.register_format "tptp" ["p"] Process.read_channel
 

src/tptp2why/tptpLexer.mll

@@ -45,6 +45,14 @@
     fprintf fmter "file %s, line %d, char %d"
       s (pos.pos_lnum) (pos.pos_cnum-pos.pos_bol)
 
+  (** report errors *)
+  let () = Why.Exn_printer.register (fun fmt exn -> match exn with
+    | TptpParser.Error ->
+      Format.fprintf fmt "syntax error.@."
+    | LexicalError (s, pos) ->
+      Format.fprintf fmt "lexical error: %a@." report (s, pos)
+    | e -> raise e)
+
 }
 
 let newline = '\n'

src/tptp2why/tptpParser.mly

@@ -21,7 +21,6 @@