Improve options display

src/bin/sail.ml

@@ -67,6 +67,7 @@
 
 open Libsail
 
+let opt_new_cli = ref false
 let opt_file_arguments : string list ref = ref []
 let opt_file_out : string option ref = ref None
 let opt_just_check : bool ref = ref false
@@ -83,16 +84,68 @@ let opt_format_backup : string option ref = ref None
 let opt_format_only : string list ref = ref []
 let opt_format_skip : string list ref = ref []
 
-(* Allow calling all options as either -foo_bar or -foo-bar *)
+(* Allow calling all options as either -foo_bar or -foo-bar. If
+   !opt_new_cli is set we force --foo for long options and -f for
+   short options. *)
 let rec fix_options = function
   | (flag, spec, doc) :: opts ->
-      (flag, spec, doc) :: (String.map (function '_' -> '-' | c -> c) flag, spec, "") :: fix_options opts
+      if !opt_new_cli then
+        if flag = "-help" || flag = "--help" then (flag, spec, doc) :: fix_options opts
+        else (
+          let flag = String.map (function '_' -> '-' | c -> c) flag in
+          let flag = if String.length flag > 2 then "-" ^ flag else flag in
+          (flag, spec, doc) :: fix_options opts
+        )
+      else if Option.is_some (String.index_from_opt flag 0 '_') then
+        (String.map (function '_' -> '-' | c -> c) flag, spec, "") :: (flag, spec, doc) :: fix_options opts
+      else (flag, spec, doc) :: fix_options opts
   | [] -> []
 
+(* This function does roughly the same thing as Arg.align, except we
+   can call it per target and it won't add additional -help
+   options. *)
+let target_align opts =
+  let split_doc doc =
+    if String.length doc > 0 then
+      if doc.[0] = ' ' then ("", doc)
+      else if doc.[0] = '\n' then ("", doc)
+      else (
+        match String.index_from_opt doc 0 ' ' with
+        | Some n -> (String.sub doc 0 n, String.sub doc n (String.length doc - n))
+        | None -> ("", doc)
+      )
+    else ("", "")
+  in
+  let opts = List.map (fun (flag, spec, doc) -> (flag, spec, split_doc doc)) opts in
+  let alignment = List.fold_left (fun a (flag, _, (arg, _)) -> max a (String.length flag + String.length arg)) 0 opts in
+  let opts =
+    List.map
+      (fun (flag, spec, (arg, doc)) ->
+        if doc = "" then (flag, spec, arg)
+        else (flag, spec, arg ^ String.make (max 0 (alignment - (String.length flag + String.length arg))) ' ' ^ doc)
+      )
+      opts
+  in
+  opts
+
+(* Add a header to separate arguments from each plugin *)
+let add_target_header plugin opts =
+  let add_header (flag, spec, doc) =
+    let desc =
+      match Target.extract_registered () with
+      | [] -> "plugin " ^ plugin
+      | [name] -> "target " ^ name
+      | names -> "targets " ^ Util.string_of_list ", " (fun x -> x) names
+    in
+    (flag, spec, doc ^ " \n\nOptions for " ^ desc)
+  in
+  Util.update_last add_header opts
+
 let load_plugin opts plugin =
   try
     Dynlink.loadfile_private plugin;
-    opts := Arg.align (!opts @ fix_options (Target.extract_options ()))
+    let plugin_opts = Target.extract_options () |> fix_options |> target_align in
+    opts := add_target_header plugin !opts @ plugin_opts
   with Dynlink.Error msg -> prerr_endline ("Failed to load plugin " ^ plugin ^ ": " ^ Dynlink.error_message msg)
 
 let version =
@@ -148,10 +201,10 @@ let rec options =
         Arg.String (fun suffix -> opt_format_backup := Some suffix),
         "<suffix> Create backups of formated files as 'file.suffix'"
       );
-      ("-fmt_only", Arg.String (fun file -> opt_format_only := file :: !opt_format_only), "<file> Format only this file");
+      ("-fmt_only", Arg.String (fun file -> opt_format_only := file :: !opt_format_only), "<file> format only this file");
       ( "-fmt_skip",
         Arg.String (fun file -> opt_format_skip := file :: !opt_format_skip),
-        "<file> Skip formatting this file"
+        "<file> skip formatting this file"
       );
       ( "-D",
         Arg.String (fun symbol -> Preprocess.add_symbol symbol),
@@ -210,7 +263,7 @@ let rec options =
       );
       ( "-smt_linearize",
         Arg.Set Type_env.opt_smt_linearize,
-        "(experimental) force linearization for constraints involving exponentials"
+        " (experimental) force linearization for constraints involving exponentials"
       );
       ("-Oconstant_fold", Arg.Set Constant_fold.optimize_constant_fold, " apply constant folding optimizations");
       ( "-Oaarch64_fast",
@@ -255,32 +308,29 @@ let rec options =
       );
       ("-dmono_continue", Arg.Set Rewrites.opt_dmono_continue, " (debug) continue despite monomorphisation errors");
       ("-dpattern_warning_no_literals", Arg.Set Pattern_completeness.opt_debug_no_literals, "");
-      ( "-infer_effects",
-        Arg.Unit (fun () -> Reporting.simple_warn "-infer_effects option is deprecated"),
-        " Ignored for compatibility with older versions; effects are always inferred now (deprecated)"
-      );
       ( "-dbacktrace",
         Arg.Int (fun l -> Reporting.opt_backtrace_length := l),
-        "<length> Length of backtrace to show when reporting unreachable code"
+        "<length> (debug) length of backtrace to show when reporting unreachable code"
+      );
+      ( "-infer_effects",
+        Arg.Unit (fun () -> Reporting.simple_warn "-infer_effects option is deprecated"),
+        " (deprecated) ignored for compatibility with older versions; effects are always inferred now"
       );
       ("-v", Arg.Set opt_print_version, " print version");
       ("-version", Arg.Set opt_print_version, " print version");
       ("-verbose", Arg.Int (fun verbosity -> Util.opt_verbosity := verbosity), "<verbosity> produce verbose output");
       ( "-explain_all_variables",
         Arg.Set Type_error.opt_explain_all_variables,
-        " Explain all type variables in type error messages"
-      );
-      ( "-explain_constraints",
-        Arg.Set Type_error.opt_explain_constraints,
-        " Explain all type variables in type error messages"
+        " explain all type variables in type error messages"
       );
+      ("-explain_constraints", Arg.Set Type_error.opt_explain_constraints, " explain constraints in type error messages");
       ( "-explain_verbose",
         Arg.Tuple [Arg.Set Type_error.opt_explain_all_variables; Arg.Set Type_error.opt_explain_constraints],
-        " Add the maximum amount of explanation to type errors"
+        " add the maximum amount of explanation to type errors"
       );
-      ("-help", Arg.Unit (fun () -> help !options), " Display this list of options. Also available as -h or --help");
-      ("-h", Arg.Unit (fun () -> help !options), "");
-      ("--help", Arg.Unit (fun () -> help !options), "");
+      ("-h", Arg.Unit (fun () -> help !options), " display this list of options. Also available as -help or --help");
+      ("-help", Arg.Unit (fun () -> help !options), " display this list of options");
+      ("--help", Arg.Unit (fun () -> help !options), " display this list of options");
     ]
 
 let register_default_target () = Target.register ~name:"default" (fun _ _ _ _ _ _ -> ())
@@ -394,6 +444,10 @@ let parse_config_file file =
     None
 
 let main () =
+  if Option.is_some (Sys.getenv_opt "SAIL_NEW_CLI") then opt_new_cli := true;
+
+  options := Arg.align (fix_options !options);
+
   begin
     match Sys.getenv_opt "SAIL_NO_PLUGINS" with
     | Some _ -> ()
@@ -410,8 +464,6 @@ let main () =
       )
   end;
 
-  options := Arg.align !options;
-
   Arg.parse_dynamic options (fun s -> opt_file_arguments := !opt_file_arguments @ [s]) usage_msg;
 
   let config = Option.bind (get_config_file ()) parse_config_file in

src/lib/target.ml

@@ -92,6 +92,7 @@ let rewrites tgt = Rewrites.instantiate_rewrites tgt.rewrites
 
 let asserts_termination tgt = tgt.asserts_termination
 
+let registered = ref []
 let targets = ref StringMap.empty
 
 let the_target = ref None
@@ -118,13 +119,19 @@ let register ~name ?flag ?description:desc ?(options = []) ?(pre_parse_hook = fu
       asserts_termination;
     }
   in
+  registered := name :: !registered;
   targets := StringMap.add name tgt !targets;
   tgt
 
 let get_the_target () = match !the_target with Some name -> StringMap.find_opt name !targets | None -> None
 
 let get ~name = StringMap.find_opt name !targets
 
+let extract_registered () =
+  let names = !registered in
+  registered := [];
+  List.rev names
+
 let extract_options () =
   let opts = StringMap.bindings !targets |> List.map (fun (_, tgt) -> tgt.options) |> List.concat in
   targets := StringMap.map (fun tgt -> { tgt with options = [] }) !targets;

src/lib/target.mli

@@ -135,5 +135,8 @@ val get_the_target : unit -> target option
 
 val get : name:string -> target option
 
+(** Used internally when updating the option list during plugin loading *)
+val extract_registered : unit -> string list
+
 (** Used internally to dynamically update the option list when loading plugins *)
 val extract_options : unit -> (Arg.key * Arg.spec * Arg.doc) list

src/lib/util.ml

@@ -179,6 +179,8 @@ let rec compare_list f l1 l2 =
       let c = f x y in
       if c = 0 then compare_list f l1 l2 else c
 
+let rec update_last f = function [] -> [] | [x] -> [f x] | x :: xs -> x :: update_last f xs
+
 let rec map_last f = function [] -> [] | [x] -> [f true x] | x :: xs -> f false x :: map_last f xs
 
 let rec iter_last f = function

src/lib/util.mli

@@ -102,6 +102,9 @@ val assoc_compare_opt : ('a -> 'a -> int) -> 'a -> ('a * 'b) list -> 'b option
 
 val power : int -> int -> int
 
+(** Apply a function to the last element of a list *)
+val update_last : ('a -> 'a) -> 'a list -> 'a list
+
 (** Map but pass true to the function for the last element *)
 val map_last : (bool -> 'a -> 'b) -> 'a list -> 'b list
 

src/sail_ocaml_backend/sail_plugin_ocaml.ml

@@ -169,7 +169,7 @@ let tofrominterp_target _ _ out_file ast _ _ =
 
 let _ =
   Target.register ~name:"tofrominterp"
-    ~description:"output OCaml functions to translate between shallow embedding and interpreter"
+    ~description:" output OCaml functions to translate between shallow embedding and interpreter"
     ~options:tofrominterp_options ~rewrites:tofrominterp_rewrites tofrominterp_target
 
 let marshal_target _ _ out_file ast _ env =
@@ -184,5 +184,5 @@ let marshal_target _ _ out_file ast _ env =
   close_out f
 
 let _ =
-  Target.register ~name:"marshal" ~description:"OCaml-marshal out the rewritten AST to a file"
+  Target.register ~name:"marshal" ~description:" OCaml-marshal out the rewritten AST to a file"
     ~rewrites:tofrominterp_rewrites marshal_target