format "why" is not a default anymore, an exception is raised

if the extension or the format is not recognised

Makefile.in

@@ -679,8 +679,7 @@ testl-type: bin/whyml.byte
 	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
 
 test-api: src/why.cma
-	ocaml unix.cma str.cma nums.cma dynlink.cma \
-		src/why.cma -I src examples/use_api.ml \
+	ocaml $(EXTCMA)	src/why.cma -I src examples/use_api.ml \
 	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
 
 ## install: install-binary install-lib install-man

bench/bench

@@ -40,9 +40,9 @@ drivers () {
     for f in $1/*.drv; do
 	echo -n "  "$f"... "
 	# running Why
-	if ! echo "theory Test goal G : 1=2 end" | $pgm --driver $f - > /dev/null 2>&1; then
+	if ! echo "theory Test goal G : 1=2 end" | $pgm -F why --driver $f - > /dev/null 2>&1; then
 	    echo "why FAILED"
-            echo "theory Test goal G : 1=2 end" | $pgm --driver $f -
+            echo "theory Test goal G : 1=2 end" | $pgm -F why --driver $f -
 	    exit 1
 	fi
 	echo "why ok... "

src/core/env.ml

@@ -77,9 +77,11 @@ let register_format name suffixes rc =
   Hashtbl.add read_channel_table name rc;
   List.iter (fun s -> Hashtbl.add suffixes_table ("." ^ s) name) suffixes
 
+exception NoFormat
+exception UnknownExtension of string 
 exception UnknownFormat of string (* parser name *)
 
-let parser_for_file ?name file = match name with
+let parser_for_file ?format file = match format with
   | None ->
       begin try
 	let ext =
@@ -87,11 +89,11 @@ let parser_for_file ?name file = match name with
 	  let n = String.length s in
 	  String.sub file n (String.length file - n)
 	in
-	Hashtbl.find suffixes_table ext
-      with Invalid_argument _ | Not_found ->
-        Format.eprintf "Cannot determine format for file=%S@." file;
-        Format.eprintf "Using 'why' as default@.";
-        "why"
+        try
+	  Hashtbl.find suffixes_table ext
+        with Not_found -> raise (UnknownExtension ext)
+      with 
+        | Invalid_argument _ -> raise NoFormat
       end
   | Some n ->
       n
@@ -100,14 +102,14 @@ let find_parser table n =
   try Hashtbl.find table n
   with Not_found -> raise (UnknownFormat n)
 
-let read_channel ?name env file ic =
-  let n = parser_for_file ?name file in
+let read_channel ?format env file ic =
+  let n = parser_for_file ?format file in
   let rc = find_parser read_channel_table n in
   rc env file ic
 
-let read_file ?name env file =
+let read_file ?format env file =
   let cin = open_in file in
-  let m = read_channel ?name env file cin in
+  let m = read_channel ?format env file cin in
   close_in cin;
   m
 
@@ -129,6 +131,10 @@ let () = Exn_printer.register
         (Pp.print_list Pp.dot Format.pp_print_string) sl s
   | UnknownFormat s ->
       Format.fprintf fmt "Unknown input format: %s" s
+  | UnknownExtension s ->
+      Format.fprintf fmt "Unknown file extension: %s" s
+  | NoFormat ->
+      Format.fprintf fmt "No input format given"
   | _ -> raise exn
   end
 

src/core/env.mli

@@ -38,25 +38,35 @@ val find_theory : env -> string list -> string -> theory
 (** Parsers *)
 
 type read_channel = env -> string -> in_channel -> theory Mnm.t
+  (** a function of type [read_channel] parses the given channel using
+      its own syntax. The string argument indicates the origin of the stream
+      (e.g. file name) to be used in error messages *)
 
 val register_format : string -> string list -> read_channel -> unit
-  (** [register_format name extensions f1 f2] registers a new format
+  (** [register_format name extensions f] registers a new format
       under name [name], for files with extensions in list [extensions];
-      [f1] is the function to perform parsing *)
+      [f] is the function to perform parsing *)
 
-val read_channel : ?name:string -> read_channel
-(** [read_channel ?name env f c] returns the map of theories
-    in channel [c]. When given, [name] enforces the format, otherwise
+exception NoFormat
+exception UnknownExtension of string 
+exception UnknownFormat of string (* format name *)
+
+val read_channel : ?format:string -> read_channel
+(** [read_channel ?format env f c] returns the map of theories
+    in channel [c]. When given, [format] enforces the format, otherwise
     the format is chosen according to [f]'s extension. 
-    Beware that it cannot be checked that [c] corresponds 
-    to the contents of [f] *)
+    Beware that nothing ensures that [c] corresponds to the contents of [f] 
 
-val read_file : ?name:string -> env -> string -> theory Mnm.t 
-(** [read_file ?name env f] returns the map of theories
-    in file [f]. When given, [name] enforces the format, otherwise
-    the format is chosen according to [f]'s extension. *)
+    @raise [NoFormat] if [format] is not given and [f] has no extension
+    @raise [UnknownExtension s] if the extension [s] is not known in 
+      any registered parser
+    @raise [UnknownFormat f] if the [format] is not registered
+*)
 
-exception UnknownFormat of string (* format name *)
+val read_file : ?format:string -> env -> string -> theory Mnm.t 
+(** [read_file ?format env f] returns the map of theories
+    in file [f]. When given, [format] enforces the format, otherwise
+    the format is chosen according to [f]'s extension. *)
 
 val list_formats : unit -> (string * string list) list
 

src/main.ml

@@ -407,7 +407,7 @@ let do_input env drv = function
         | "-" -> "stdin", stdin
         | f   -> f, open_in f
       in
-      let m = Env.read_channel ?name:!opt_parser env fname cin in
+      let m = Env.read_channel ?format:!opt_parser env fname cin in
       close_in cin;
       if !opt_type_only then
         ()