- put back "assert false" in Eliminate_inductive

- rewrite Trans.report to stop my eyes bleeding

src/core/trans.ml

@@ -118,15 +118,13 @@ let notImplemented s = error (NotImplemented s)
 
 let report fmt = function
   | UnsupportedExpression (e,s) ->
+      let msg = "The transformation doesn't support this expression" in
       Format.fprintf fmt
-        "@[<hov 3> The transformation doesn't support this expression :@\n\
-%a@\n\
-%s@]@\n" Pretty.print_expr e s
+        "@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_expr e s
   | UnsupportedDeclaration (d,s) ->
+      let msg = "The transformation doesn't support this declaration" in
       Format.fprintf fmt
-        "@[<hov 3> The transformation doesn't support this declaration :@\n\
-%a@\n\
-%s@]@\n" Pretty.print_decl d s
+        "@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_decl d s
   | NotImplemented (s) ->
-      Format.fprintf fmt
-        "@[<hov 3> Unimplemented features :@\n%s@]@\n" s
+      Format.fprintf fmt "@[<hov 3> Unimplemented feature:@\n%s@]@\n" s
+

src/core/trans.mli

@@ -57,10 +57,8 @@ val decl_l : (decl -> decl list list) -> task -> task tlist
 
 val rewrite : (term -> term) -> (fmla -> fmla) -> task -> task trans
 
-
 (** exception to use in a transformation *)
 
-
 type error =
   | UnsupportedExpression of expr * string
   | UnsupportedDeclaration of decl * string
@@ -70,7 +68,7 @@ exception Error of error
 
 val unsupportedExpression : expr -> string -> 'a
 val unsupportedDeclaration : decl -> string -> 'a
-(** - [expr] is the problematic formula 
+(** - [expr] is the problematic formula
     - [string] explain the problem and
       possibly a way to solve it (such as applying another
       transforamtion) *)
@@ -78,5 +76,5 @@ val unsupportedDeclaration : decl -> string -> 'a
 val notImplemented : string -> 'a
 (** [string] explain what is not implemented *)
 
-
 val report : Format.formatter -> error -> unit
+

src/transform/eliminate_inductive.ml

@@ -36,7 +36,7 @@ let exi vl (_,f) =
     | Fapp (_,tl) ->
         let marry acc v t = f_and_simp acc (f_equ v t) in
         List.fold_left2 marry f_true vl tl
-    | _ -> Trans.unsupportedExpression (Fmla f) "eliminate_inductive"
+    | _ -> assert false
   in
   descend f