Adding a debug flag to print the list of labels used in the code (for main)

src/core/ident.ml

@@ -38,6 +38,11 @@ let create_label s = Hslab.hashcons {
   lab_tag    = -1
 }
 
+let list_label () =
+  let acc = ref [] in
+  Hslab.iter (fun label -> acc := label.lab_string :: !acc);
+  !acc
+
 let lab_equal : label -> label -> bool = (==)
 let lab_hash lab = lab.lab_tag
 let lab_compare l1 l2 = Pervasives.compare l1.lab_tag l2.lab_tag

src/core/ident.mli

@@ -27,6 +27,8 @@ val lab_hash : label -> int
 
 val create_label : string -> label
 
+val list_label: unit -> string list
+
 (** {2 Naming convention } *)
 
 val infix: string -> string

src/tools/main.ml

@@ -23,6 +23,7 @@ let opt_list_printers = ref false
 let opt_list_provers = ref false
 let opt_list_formats = ref false
 let opt_list_metas = ref false
+let opt_list_labels = ref false
 
 let option_list = [
   "--list-transforms", Arg.Set opt_list_transforms,
@@ -35,6 +36,7 @@ let option_list = [
       " list known input formats";
   "--list-metas", Arg.Set opt_list_metas,
       " list known metas";
+  "--list-labels", Arg.Set opt_list_labels, "list used labels";
   "--print-libdir",
       Arg.Unit (fun _ -> printf "%s@." Config.libdir; exit 0),
       " print location of binary components (plugins, etc)";
@@ -151,6 +153,11 @@ let () = try
     printf "@[<hov 2>Known metas:@\n%a@]@\n@."
       (Pp.print_list Pp.newline2 print) (List.sort cmp (Theory.list_metas ()))
   end;
+  if !opt_list_labels then begin
+    opt_list := true;
+    let l = List.sort String.compare (Ident.list_label ()) in
+    List.iter (fun x -> Format.eprintf "%s@." x) l
+  end;
   if !opt_list then exit 0;
 
   printf "@[%s%a@]" usage_msg extra_help ()