add Debug.stack_trace flag and Trans.apply_named call

src/core/trans.ml

@@ -40,8 +40,14 @@ let singleton f x = [f x]
 let compose   f g x =            g (f x)
 let compose_l f g x = list_apply g (f x)
 
+exception TransFailure of (string * exn)
+
 let apply f x = f x
 
+let apply_named s f x = try apply f x with
+  | e when not (Debug.test_flag Debug.stack_trace) ->
+      raise (TransFailure (s,e))
+
 module Wtask = Hashweak.Make (struct
   type t = task_hd
   let tag t = t.task_tag
@@ -213,5 +219,8 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
       Format.fprintf fmt "Transformation '%s' is already registered" s
   | UnknownTrans s ->
       Format.fprintf fmt "Unknown transformation '%s'" s
+  | TransFailure (s,e) ->
+      Format.fprintf fmt "Failure in transformation %s@\n%a" s
+        Exn_printer.exn_printer e
   | e -> raise e)
 

src/core/trans.mli

@@ -95,3 +95,5 @@ val lookup_transform_l : string -> Env.env -> task tlist
 val list_transforms   : unit -> string list
 val list_transforms_l : unit -> string list
 
+val apply_named : string -> 'a trans -> (task -> 'a)
+

src/driver/driver.ml

@@ -209,7 +209,6 @@ let call_on_buffer ~command ?timelimit ?memlimit drv buffer =
 (** print'n'prove *)
 
 exception NoPrinter
-exception TransFailure of (string * exn)
 
 let update_task drv task =
   let task, goal = match task with
@@ -240,8 +239,6 @@ let update_task drv task =
   add_tdecl task goal
 
 let print_task drv fmt task =
-  (* TODO: wrong debug flag, should use one in Trans *)
-  let debug = Debug.test_flag Call_provers.debug in
   let p = match drv.drv_printer with
     | None -> raise NoPrinter
     | Some p -> p
@@ -253,8 +250,7 @@ let print_task drv fmt task =
   let transl = List.map lookup_transform drv.drv_transform in
   let apply task (t, tr) =
 (*  Format.printf "@\n@\n[%f] %s@." (Sys.time ()) t; *)
-    try Trans.apply tr task
-    with e when not debug -> raise (TransFailure (t,e))
+    Trans.apply_named t tr task
   in
 (*Format.printf "@\n@\nTASK";*)
   let task = update_task drv task in
@@ -279,8 +275,6 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
       "Plugins are not supported, recomplie Why"
   | Duplicate s -> Format.fprintf fmt
       "Duplicate %s specification" s
-  | TransFailure (s,e) -> Format.fprintf fmt
-      "Failure in transformation %s@\n%a" s Exn_printer.exn_printer e
   | UnknownType (thl,idl) -> Format.fprintf fmt
       "Unknown type symbol %s" (string_of_qualid thl idl)
   | UnknownLogic (thl,idl) -> Format.fprintf fmt

src/main.ml

@@ -325,9 +325,6 @@ let memlimit = match !opt_memlimit with
   | Some i when i <= 0 -> 0
   | Some i -> i
 
-(* TODO: move every debugging output to the proper module *)
-let debug = !opt_debug_all
-
 let print_th_namespace fmt th =
   Pretty.print_namespace fmt th.th_name.Ident.id_string th
 
@@ -366,15 +363,8 @@ let do_tasks env drv fname tname th trans task =
   in
   let transl = List.fold_left lookup [] trans in
   let apply tasks (s, tr) =
-    try
-      if debug then Format.eprintf "apply transformation %s@." s;
-      let l = List.fold_left
-        (fun acc task ->
-           List.rev_append (Trans.apply tr task) acc) [] tasks in
-      List.rev l (* In order to keep the order for 1-1 transformation *)
-    with e when not debug ->
-      Format.eprintf "failure in transformation %s@." s;
-      raise e
+    List.rev (List.fold_left (fun acc task ->
+      List.rev_append (Trans.apply_named s tr task) acc) [] tasks)
   in
   let tasks = List.fold_left apply [task] transl in
   List.iter (do_task drv fname tname th) tasks
@@ -453,7 +443,7 @@ let () =
     let env = Env.create_env (Lexer.retrieve !opt_loadpath) in
     let drv = Util.option_map (load_driver env) !opt_driver in
     Queue.iter (do_input env drv) opt_queue
-  with e when not debug ->
+  with e when not (Debug.test_flag Debug.stack_trace) ->
     eprintf "%a@." Exn_printer.exn_printer e;
     exit 1
 

src/parser/lexer.mll

@@ -224,7 +224,7 @@ and comment = parse
   | newline 
       { newline lexbuf; comment lexbuf }
   | eof
-      { raise (Loc.Located (!comment_start_loc,UnterminatedComment)) }
+      { raise (Loc.Located (!comment_start_loc, UnterminatedComment)) }
   | _ 
       { comment lexbuf }
 
@@ -244,9 +244,8 @@ and string = parse
 
 {
   let with_location f lb =
-    try 
-      f lb 
-    with 
+    if Debug.test_flag Debug.stack_trace then f lb else
+    try f lb with
       | Loc.Located _ as e -> raise e
       | e -> raise (Loc.Located (loc lb, e))
 

src/util/debug.ml

@@ -46,3 +46,5 @@ let () = Exn_printer.register (fun fmt e -> match e with
   | UnknownFlag s -> Format.fprintf fmt "unknown debug flag `%s'@." s
   | _ -> raise e)
 
+let stack_trace = register_flag "stack_trace"
+

src/util/debug.mli

@@ -29,3 +29,4 @@ val toggle_flag : flag -> unit
 
 val test_flag : flag -> bool
 
+val stack_trace : flag