Structure and share command line arguments among components and tools

text/000-argument-parsing-oo.md

@@ -0,0 +1,279 @@
+- Title: Structure and share command line arguments among components and tools
+
+- Drivers: Enrico
+
+----
+
+# Summary
+
+Coq ships many binaries: coqc, coqtop, coqdep, coqdoc, coqide.
+As well a few technical binaries: stmproofworkertop, ...
+Coq is made of components that are parametrized by sets of options.
+
+We propose an approach (and a POC library) to:
+- declare options together with their documentation
+- groups options into sets, corresponding to component or tools
+- these sets can be freely combined, eg reused
+- components API can declare the set of options they understand
+- subtyping automatically shrinks a set of options to fit an API, if wanted 
+
+# Motivation
+
+Today we lack a proper infrastructure for:
+- sharing parsing options and documentation across components/tools
+- organize/structure options in coherent sets
+
+As a result documentation is not at the same place where the option syntax is
+declared and hence the usage messages get out of sync. Parsin is done by
+hand in different ways depending on the tool, even if the option to be parsed
+is literally the same.
+
+# Detailed design
+
+Get the [code](https://github.com/gares/ooarg)
+
+```ocaml
+(* engine ------------------------------------------------------------ *)
+
+
+(* type of flags, to share parsing/printing among flags *)
+type t =
+ | Flag of (unit -> unit)
+ | Bool of (bool -> unit)
+ | String of (string -> unit)
+ | Enum : (string * 'a) list * ('a -> unit) -> t
+
+let coq_bool_of_string = function
+  | "yes" | "on" | "true" -> true
+  | "no" | "off" | "false" -> false
+  | _ -> failwith "not a boolean"
+
+let mk_parser k t l =
+  match t, l with     
+  | Bool f, x :: y :: rest when x = k -> f (coq_bool_of_string y); Some rest
+  | Flag f, x :: rest when x = k -> f (); Some rest
+  | String f, x :: y :: rest when x = k -> f y; Some rest
+  | Enum (vals,f), x :: y :: rest when x = k ->
+      f (List.assoc y vals); Some rest
+  | _ -> None
+
+let mk_printer s d t fmt () =
+  Format.pp_print_string fmt s;
+  Format.pp_print_tab fmt ();
+  Format.pp_open_box fmt 0;
+  begin match t with
+  | Flag _ -> ()
+  | Enum (vals,_) ->
+      Format.pp_print_string fmt "(";
+      let vals = List.map fst vals in
+      let x, xs = List.(hd vals, tl vals) in
+      Format.pp_print_string fmt x;
+      List.iter (Format.fprintf fmt "|%s") xs;
+      Format.pp_print_string fmt ") "
+  | String _ -> Format.pp_print_string fmt "<string> "
+  | Bool _ -> Format.pp_print_string fmt "<yes/no> " end;
+  Format.pp_print_text fmt d;
+  Format.pp_close_box fmt ();
+  Format.pp_print_tab fmt ()
+;;
+
+(* collection of options to be parsed or printed *)
+class registry = object(self)
+  val mutable parsers = []
+  val mutable printers = []
+  val mutable max_len = 10
+  val mutable keys = []
+  method register s d t =
+   if not (List.mem s keys) then begin
+     keys <- s :: keys;
+     parsers <- mk_parser s t :: parsers;
+     printers <- mk_printer s d t :: printers;
+     max_len <- max max_len (String.length s)
+   end
+
+  method parse l =
+    let rec aux = function
+    | [] -> l (* this is what is left, we could error *)
+    | p::ps ->
+       match p l with
+       | None -> aux ps
+       | Some l -> self#parse l
+    in
+      aux parsers
+
+  method usage (fmt : Format.formatter) () =
+    Format.pp_open_tbox fmt ();
+    Format.pp_set_tab fmt ();
+    Format.fprintf fmt "option";
+    for i = 1 to max_len - 3 do Format.fprintf fmt " "; done;
+    Format.pp_set_tab fmt ();
+    Format.fprintf fmt "description";
+    Format.pp_print_tab fmt ();
+    List.iter (fun p -> p fmt ()) printers;
+    Format.pp_close_tbox fmt ();
+    Format.pp_print_newline fmt ()
+
+end
+
+(* convenient way of inheriting the API of a set of option *) 
+class option_set (r : registry) = object
+  method parse = r#parse
+  method usage = r#usage
+end
+
+(* declaration of some options ------------------------------------------ *)
+
+class         print_version = fun r -> object
+  val mutable print_version = false 
+       method print_version = print_version
+  initializer r#register
+    "-print-version" "prints the version of Coq"
+    (Flag (fun () -> print_version <- true))
+end
+
+class         file_name = fun r -> object
+  val mutable file_name = None
+       method file_name = file_name
+  initializer r#register
+    "-file-name" "sets the file name of whatever"
+    (String (fun x -> (* one could File.exists x here *) file_name <- Some x))
+end
+
+class         async_proofs = fun r -> object
+  val mutable async_proofs = None
+       method async_proofs = async_proofs
+  initializer r#register
+    "-async-proofs" "enables/disables super powers and this is a terribly long line that wraps around to test the documentation layout"
+    (Bool (fun x -> async_proofs <- Some x))
+end
+
+type diffs_t = On | Off | Removed
+class         diffs = fun r -> object
+  val mutable diffs = Off
+       method diffs = diffs
+  initializer r#register
+    "-diffs" "highlight differences between proof steps"
+    (Enum(["on",On;"off",Off;"removed",Removed], (fun x -> diffs <- x)))
+end
+
+(* usage example --------------------------------------------------------- *)
+
+class coqdep_options r =
+  object(self)
+    inherit option_set r
+
+    inherit file_name r
+    inherit print_version r
+end
+
+let coqdep_options = new coqdep_options (new registry);;
+
+Format.printf "coqdep usage:@\n%a@\n" coqdep_options#usage ();;
+
+let rest = coqdep_options#parse ["-print-version";"-file-name";"foo"];;
+assert(rest=[]);;
+
+module Coqdep : sig
+
+  (* various ways to express the list of supported options *)
+  (* I use .. or # to let one pass a larger set of options, but
+   * we can also be strict. See the last example for a concrete use case *)
+
+  val main : < print_version : bool;
+               file_name : string option;
+               .. >
+          -> unit
+
+  (* or we can use the exact set of options if it has a name *)
+  val main2 : #coqdep_options -> unit
+
+end = struct
+
+  let main options = 
+    Format.printf "Coqdep receives options: %b %s@\n@\n"
+      options#print_version
+      (match options#file_name with Some x -> x | _ -> "unset");;
+
+  let main2 = main
+
+end
+  ;;
+
+Coqdep.main coqdep_options;;
+Coqdep.main2 coqdep_options;;
+
+(* usage example -------------------------------------------------------- *)
+
+(* Stm as a component, I add print_version just to complicate the next
+ * example *)
+class stm_options r = object
+    inherit option_set r
+
+    inherit print_version r
+    inherit async_proofs r
+end
+
+module Stm : sig
+
+  val init : #async_proofs -> unit
+
+end = struct let init _ = () end
+
+let stm_options = new stm_options (new registry);;
+ignore(stm_options#parse ["-async-proofs";"yes"]);;
+Stm.init stm_options;;
+
+(* usage example -------------------------------------------------------- *)
+  (* here I mix and mach:
+      - single options
+      - options for a component
+      - options for a tool *)
+class coqtop_options r = object
+    inherit option_set r
+
+    inherit stm_options r (* we take all options of the stm component *)
+    inherit diffs r (* plus this one *)
+    inherit! coqdep_options r (* plus the ones supported by coqdep *)
+    (* Last line gets a warning that print_version occurs twice, to silence
+     * it one can use inherit! (in both cases it works, since multiple
+     * inheritance works in OCaml) *)
+end
+
+let coqtop_options = new coqtop_options (new registry);;
+Format.printf "coqtop usage:@\n%a@\n" coqtop_options#usage ();;
+
+coqtop_options#parse ["-diffs";"removed"];;
+
+module Coqtop : sig
+
+  val main : coqtop_options -> unit
+
+end = struct
+
+  let main o =
+     (* the Stm.init type accepts any large enough set of options,
+      * so we can directy pass o *)
+     Stm.init o;
+     Format.printf "diffs are: %s@\n"
+        (match o#diffs with Removed -> "rm" | On -> "ok" | Off -> "off");;
+
+end;;
+
+Coqtop.main coqtop_options;;
+
+```
+
+# Drawbacks
+
+Objects are not the most well known feature of OCaml, in spite of their beauty.
+
+# Alternatives
+
+One could use nested records. This approach has less flexibility, since
+records cannot overlap and subtyping is not available. 
+
+I have a similar file that uses functional objects, but it is more involved
+since the copying construct `{< .. >}` needs to be in a method, for good reasons,
+and this in turn makes the boilreplate to declare an option significantly longer
+and the type annotations a bit havier.
+