Encoding : add some debugging informations

src/core/theory.ml

@@ -684,7 +684,7 @@ let create_meta m al =
     (* we allow "constant tysymbol <=> ty" conversion *)
     let a = match at,a with
       | MTtysymbol, MAty ({ ty_node = Tyapp (ts,[]) }) -> MAts ts
-      | MTty, MAts ts when ts.ts_args = [] -> MAty (ty_app ts [])
+      | MTty, MAts ({ts_args = []} as ts) -> MAty (ty_app ts [])
       | _, _ -> a
     in
     let mt = get_meta_arg_type a in

src/core/trans.ml

@@ -25,6 +25,8 @@ open Decl
 open Theory
 open Task
 
+let debug = Debug.register_flag "transform"
+
 (** Task transformation *)
 
 type 'a trans = task -> 'a
@@ -44,10 +46,14 @@ 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) ->
+let apply_named s f x =
+  Debug.dprintf debug "Apply transformation %s@." s;
+  try apply f x with
+    | e when not (Debug.test_flag Debug.stack_trace) ->
       raise (TransFailure (s,e))
 
+let catch_named = apply_named
+
 module Wtask = Hashweak.Make (struct
   type t = task_hd
   let tag t = t.task_tag
@@ -216,6 +222,17 @@ let on_tagged_pr t fn =
   in
   on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set Spr.empty))
 
+(** debug *)
+let print_meta f m task =
+  if Debug.test_flag f then
+    (let fmt = Debug.get_debug_formatter () in
+     Pp.print_iter1 Stdecl.iter Pp.newline
+       Pretty.print_tdecl
+       fmt
+       (find_meta_tds task m).tds_set;
+     (Pp.add_flush Pp.newline) fmt ());
+  task
+
 (** register transformations *)
 
 open Env

src/core/trans.mli

@@ -79,6 +79,12 @@ val on_tagged_ts : meta -> (Sts.t -> 'a trans) -> 'a trans
 val on_tagged_ls : meta -> (Sls.t -> 'a trans) -> 'a trans
 val on_tagged_pr : meta -> (Spr.t -> 'a trans) -> 'a trans
 
+(** debug transformation *)
+val print_meta : Debug.flag -> meta -> task trans
+(** [print_meta f m] if [d] is set pretty_print on the debug
+    formatter. In all the case the transformation is indeed the
+    identity *)
+
 (** {2 Registration} *)
 
 exception UnknownTrans of string
@@ -96,5 +102,9 @@ val lookup_transform_l : string -> Env.env -> task tlist
 val list_transforms   : unit -> string list
 val list_transforms_l : unit -> string list
 
+exception TransFailure of (string * exn)
+
 val apply_named : string -> 'a trans -> (task -> 'a)
 
+val catch_named : string -> 'a trans -> 'a trans
+(** catch the error, and reraise with TransFailure *)

src/transform/encoding.ml

@@ -22,9 +22,11 @@ open Theory
 open Task
 open Trans
 
-let meta_kept = register_meta "encoding : kept" [MTtysymbol]
+let meta_kept = register_meta "encoding : kept" [MTty]
 let meta_base = register_meta_excl "encoding : base" [MTtysymbol]
 
+let debug = Debug.register_flag "encoding"
+
 type enco_opt =
     { meta : meta;
       default : string;
@@ -51,11 +53,12 @@ let enco_gen opt env =
       | Some [MAstr s] -> s
       | _ -> assert false in
     try
-      (Hashtbl.find opt.table s) env
+      Trans.catch_named s ((Hashtbl.find opt.table s) env)
     with Not_found -> failwith
       (Format.sprintf "encoding : %s wrong argument %s" opt.meta.meta_name s))
 
-let enco_select = enco_gen select_opt
+let print_kept = print_meta debug meta_kept
+let enco_select env = compose (enco_gen select_opt env) print_kept
 let enco_kept = enco_gen kept_opt
 let enco_poly_smt = enco_gen poly_smt_opt
 let enco_poly_tptp = enco_gen poly_tptp_opt

src/util/debug.ml

@@ -52,6 +52,7 @@ let () = Exn_printer.register (fun fmt e -> match e with
 let stack_trace = register_flag "stack_trace"
 
 let set_debug_formatter = (:=) formatter
+let get_debug_formatter () = !formatter
 
 let dprintf flag =
   if !flag then Format.fprintf !formatter else Format.ifprintf !formatter

src/util/debug.mli

@@ -40,6 +40,10 @@ val nottest_flag : flag -> bool
 val set_debug_formatter : Format.formatter -> unit
 (** Set the formatter used when printing debug material *)
 
+val get_debug_formatter : unit -> Format.formatter
+(** Get the formatter used when printing debug material *)
+
+
 val dprintf : flag -> ('a, Format.formatter, unit) format -> 'a
 (** Print only if the flag is set *)