registered parsers: error reporting

src/core/env.ml

@@ -68,14 +68,17 @@ let env_tag env = env.env_tag
 
 type parse_only   = env -> string -> in_channel -> unit
 type read_channel = env -> string -> in_channel -> theory Mnm.t
+type error_report = Format.formatter -> exn -> unit
 
 let parse_only_table   = Hashtbl.create 17 (* parser name -> parse_only *)
 let read_channel_table = Hashtbl.create 17 (* parser name -> read_channel *)
+let error_report_table = Hashtbl.create 17 (* parser name -> error_report *)
 let suffixes_table     = Hashtbl.create 17 (* suffix -> parser name *)
 
-let register_parser name suffixes po rc =
+let register_parser name suffixes po rc er =
   Hashtbl.add parse_only_table   name po;
   Hashtbl.add read_channel_table name rc;
+  Hashtbl.add error_report_table name er;
   List.iter (fun s -> Hashtbl.add suffixes_table ("." ^ s) name) suffixes
 
 exception UnknownParser of string (* parser name *)
@@ -109,3 +112,17 @@ let read_channel ?name env file ic =
   let rc = find_parser read_channel_table n in
   rc env file ic
 
+let report ?name file fmt e =
+  let n = parser_for_file ?name file in 
+  let er = find_parser error_report_table n in
+  er fmt e
+
+let list_formats () =
+  let h = Hashtbl.create 17 in
+  let add s p = 
+    let l = try Hashtbl.find h p with Not_found -> [] in
+    Hashtbl.replace h p (s :: l)
+  in
+  Hashtbl.iter add suffixes_table;
+  Hashtbl.fold (fun p l acc -> (p, l) :: acc) h []
+

src/core/env.mli

@@ -39,9 +39,10 @@ exception TheoryNotFound of string list * string
 
 type parse_only   = env -> string -> in_channel -> unit
 type read_channel = env -> string -> in_channel -> theory Mnm.t
+type error_report = Format.formatter -> exn -> unit
 
 val register_parser :
-  string -> string list -> parse_only -> read_channel -> unit
+  string -> string list -> parse_only -> read_channel -> error_report -> unit
   (** [register_parser name extensions f1 f2] registers a new parser
       under name [name], for files with extensions in list [extensions];
       [f1] is the function to perform parsing only;
@@ -51,5 +52,9 @@ val parse_only   : ?name:string -> parse_only
 
 val read_channel : ?name:string -> read_channel
 
+val report : ?name:string -> string -> error_report
+
 exception UnknownParser of string (* parser name *)
 
+val list_formats : unit -> (string * string list) list
+

src/main.ml

@@ -76,6 +76,7 @@ let add_opt_goal x = match !opt_theory with
 let add_opt_trans x = opt_trans := x::!opt_trans
 
 let opt_config = ref None
+let opt_parser = ref None
 let opt_prover = ref None
 let opt_loadpath = ref []
 let opt_driver = ref None
@@ -89,6 +90,7 @@ let opt_print_namespace = ref false
 let opt_list_transforms = ref false
 let opt_list_printers = ref false
 let opt_list_provers = ref false
+let opt_list_formats = ref false
 
 let opt_parse_only = ref false
 let opt_type_only = ref false
@@ -119,6 +121,10 @@ let option_list = Arg.align [
       "<prover> Prove or print (with -o) the selected goals";
   "--prover", Arg.String (fun s -> opt_prover := Some s),
       " same as -P";
+  "-F", Arg.String (fun s -> opt_parser := Some s),
+      "<format> Input format (default: \"why\")";
+  "--format", Arg.String (fun s -> opt_parser := Some s),
+      " same as -F";
   "-T", Arg.Int (fun i -> opt_timelimit := Some i),
       "<sec> Set the prover's time limit (default=10, no limit=0)";
   "--timelimit", Arg.Int (fun i -> opt_timelimit := Some i),
@@ -145,6 +151,8 @@ let option_list = Arg.align [
       " List the registered printers";
   "--list-provers", Arg.Set opt_list_provers,
       " List the known provers";
+  "--list-formats", Arg.Set opt_list_formats,
+      " List the known input formats";
   "--parse-only", Arg.Set opt_parse_only,
       " Stop after parsing";
   "--type-only", Arg.Set opt_type_only,
@@ -167,10 +175,20 @@ let () =
       (Pp.print_list Pp.newline Pp.string)
       (List.sort String.compare (Register.list_transforms_l ()));
   end;
-  if !opt_list_printers then
+  if !opt_list_printers then begin
     printf "@[<hov 2>Registered printers:@\n%a@]@\n@."
       (Pp.print_list Pp.newline Pp.string)
-      (List.sort String.compare (Register.list_printers ()));
+      (List.sort String.compare (Register.list_printers ()))
+  end;
+  if !opt_list_formats then begin
+    let print1 fmt s = fprintf fmt "%S" s in
+    let print fmt (p, l) = 
+      fprintf fmt "%s [%a]" p (Pp.print_list Pp.comma print1) l
+    in
+    printf "@[<hov 2>Known input formats:@\n%a@]@." 
+      (Pp.print_list Pp.newline print)
+      (List.sort Pervasives.compare (Env.list_formats ()))
+  end;
   if !opt_list_provers then begin
     let config = read_config !opt_config in
     let print fmt s prover = fprintf fmt "%s (%s)@\n" s prover.name in
@@ -178,7 +196,8 @@ let () =
     printf "@[<hov 2>Known provers:@\n%a@]@." print config.provers
   end;
 
-  if !opt_list_transforms || !opt_list_printers || !opt_list_provers
+  if !opt_list_transforms || !opt_list_printers || !opt_list_provers ||
+     !opt_list_formats
   then exit 0;
 
   if Queue.is_empty opt_queue then begin
@@ -247,10 +266,10 @@ let memlimit = match !opt_memlimit with
 let debug = !opt_debug
 
 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
+  | Lexer.Error e ->
+      fprintf fmt "lexical error: %a" Lexer.report e;
   | Parsing.Parse_error ->
       fprintf fmt "syntax error"
   | Denv.Error e ->
@@ -272,7 +291,10 @@ let rec report fmt = function
       Prover.report fmt e
   | Register.Error e ->
       Register.report fmt e
-  | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
+  | Env.UnknownParser 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
@@ -384,21 +406,28 @@ let do_input env drv = function
         | "-" -> "stdin", stdin
         | f   -> f, open_in f
       in
-      if !opt_parse_only then begin
-	Env.parse_only env fname cin;
-        close_in cin
-      end else begin
-        let m = Env.read_channel env fname cin in
-        close_in cin;
-        if !opt_type_only then ()
-        else if Queue.is_empty tlist then
-          let glist = Queue.create () in
-          let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
-          let do_th _ (t,th) = do_theory drv fname t th trans glist in
-          Ident.Mid.iter do_th (Mnm.fold add_th m Ident.Mid.empty)
-        else
-          Queue.iter (do_local_theory drv fname m) tlist
-      end
+      let report = Env.report ?name:!opt_parser fname in
+      try
+	if !opt_parse_only then begin
+	  Env.parse_only ?name:!opt_parser env fname cin;
+          close_in cin
+	end else begin
+          let m = Env.read_channel ?name:!opt_parser env fname cin in
+          close_in cin;
+          if !opt_type_only then ()
+          else if Queue.is_empty tlist then
+            let glist = Queue.create () in
+            let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
+            let do_th _ (t,th) = do_theory drv fname t th trans glist in
+            Ident.Mid.iter do_th (Mnm.fold add_th m Ident.Mid.empty)
+          else
+            Queue.iter (do_local_theory drv fname m) tlist
+	end
+      with 
+	| Loc.Located (loc, e) ->
+	    eprintf "%a%a" Loc.report_position loc report e; exit 1
+	| e ->
+	    report err_formatter e; exit 1
 
 let () =
   try

src/parser/typing.ml

@@ -1064,7 +1064,19 @@ let parse_only _env fname cin =
   ignore (Lexer.parse_logic_file lb);
   close_in cin
 
-let () = Env.register_parser "why" ["why"] parse_only read_channel
+let error_report fmt = function
+  | 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
+  | Error e ->
+      report fmt e
+  | e -> 
+      raise e
+
+let () = Env.register_parser "why" ["why"] parse_only read_channel error_report
 
 (*
 Local Variables: