new module Warning for warnings

warning for possibly useless quantifiers (unless a leading underscore is used)

Makefile.in

@@ -116,7 +116,7 @@ LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
 	       src/driver/driver_lexer.ml src/session/xml.ml
 
 LIB_UTIL = stdlib exn_printer pp debug loc print_tree \
-	   cmdline hashweak hashcons util sysutil rc plugin
+	   cmdline hashweak hashcons util warning sysutil rc plugin
 
 LIB_CORE = ident ty term pattern decl theory task pretty env trans printer
 

src/parser/denv.ml

@@ -196,20 +196,13 @@ and dtrigger =
   | TRterm of dterm
   | TRfmla of dfmla
 
-
-exception UnusedVar of string
-
-let () = Exn_printer.register (fun fmt e -> match e with
-  | UnusedVar s ->
-      fprintf fmt "Unused variable %s" s
-  | _ -> raise e)
-
 let allowed_unused s = String.length s > 0 && s.[0] = '_'
 
 let check_used_var vars v =
   if not (Mvs.mem v vars) then
     let s = v.vs_name.id_string in
-    if allowed_unused s then () else raise (UnusedVar s)
+    if not (allowed_unused s) then
+      Warning.emit ?loc:v.vs_name.Ident.id_loc "unused variable %s" s
 
 let check_used_vars vars =
   List.iter (check_used_var vars)

src/util/warning.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2012                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Guillaume Melquiond                                                 *)
+(*    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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Format
+open Util
+
+let default_hook ?loc s =
+  option_iter (Loc.report_position err_formatter) loc;
+  eprintf "warning: %s@." s
+
+let hook = ref default_hook
+let set_hook = (:=) hook
+
+let emit ?loc p =
+  let b = Buffer.create 100 in
+  let fmt = formatter_of_buffer b in
+  let handle fmt =
+    Format.pp_print_flush fmt (); !hook ?loc (Buffer.contents b) in
+  kfprintf handle fmt p

src/util/warning.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2012                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Guillaume Melquiond                                                 *)
+(*    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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+val emit:
+  ?loc:Loc.position -> ('b, Format.formatter, unit, unit) format4 -> 'b
+
+(* The default behavior is to emit warning on standard error,
+   with position on a first line (if any) and message on a second line.
+   This can be changed using the following function. *)
+
+val set_hook: (?loc:Loc.position -> string -> unit) -> unit
+
+

tests/test-jcf.why

@@ -3,7 +3,7 @@ theory T
 
   use import int.Int
 
-  goal G: 1+3 > 2
+  goal G: exists x: int. 1+3 > 2
 
 end