diff --git a/src/main.ml b/src/main.ml index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..736f48a8f3fbdd7786525c18bd9e9700a91cbfdd 100644 --- a/src/main.ml +++ b/src/main.ml @@ -0,0 +1,109 @@ +(**************************************************************************) +(* *) +(* This file is part of Caisar. *) +(* *) +(**************************************************************************) + +open Base +open Cmdliner +module Format = Caml.Format + +let caisar = "caisar" + +(* Logs. *) + +let pp_header = + let x = + match Array.length Caml.Sys.argv with + | 0 -> Caml.(Filename.basename Sys.executable_name) + | _ -> Caml.(Filename.basename Sys.argv.(0)) + in + let pp_h ppf style h = Fmt.pf ppf "[%s][%a] " x Fmt.(styled style string) h in + fun ppf (l, h) -> + let open Logs_fmt in + match l with + | Logs.App -> Fmt.pf ppf "[%a] " Fmt.(styled app_style string) x + | Logs.Error -> + pp_h ppf err_style (match h with None -> "ERROR" | Some h -> h) + | Logs.Warning -> + pp_h ppf warn_style (match h with None -> "WARNING" | Some h -> h) + | Logs.Info -> + pp_h ppf info_style (match h with None -> "INFO" | Some h -> h) + | Logs.Debug -> + pp_h ppf debug_style (match h with None -> "DEBUG" | Some h -> h) + +let setup_logs = + let setup_log level = + Fmt_tty.setup_std_outputs ~style_renderer:`Ansi_tty (); + Logs.set_level level; + Logs.set_reporter (Logs_fmt.reporter ~pp_header ()) + in + Term.(const setup_log $ Logs_cli.level ()) + +(* Commands. *) + +let config cmd detect () = + Logs.debug (fun m -> m "Command `%s'." cmd); + if detect then Logs.app (fun m -> m "Automatic detection.") + +(* Command line. *) + +let config_cmd = + let cmdname = "config" in + let dirvar = "DIR" in + let envs = + [ + Term.env_info + ~doc: + "Absolute path to the directory containing the executable of a \ + solver." + dirvar; + ] + in + let detect = + let doc = + Format.sprintf "Detect solvers in \\$PATH (or \\$%s, if specified)." + dirvar + in + Arg.(value & flag & info [ "d"; "detect" ] ~doc) + in + let doc = Format.sprintf "%s configuration." caisar in + let exits = Term.default_exits in + let man = + [ + `S Manpage.s_description; + `P (Format.sprintf "Handle the configuration of %s." caisar); + ] + in + ( Term.( + ret + (const (fun cmdname detect _ -> + if not detect then `Help (`Pager, Some "config") + else + (* TODO: Do not only check for [detect], and enable it by + default, as soon as other options are available. *) + `Ok (config cmdname true ())) + $ const cmdname $ detect $ setup_logs)), + Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man ) + +let default_cmd = + let doc = "Framework for neural networks property verification and more." in + let sdocs = Manpage.s_common_options in + let man = + [ + `S Manpage.s_common_options; + `P "These options are common to all commands."; + `S "MORE HELP"; + `P "Use `$(mname) $(i,COMMAND) --help' for help on a single command."; + `S Manpage.s_bugs; + `P "Email bug reports to <...>"; + ] + in + let version = "0.0" in + ( Term.(ret (const (fun _ -> `Help (`Pager, None)) $ const ())), + Term.info caisar ~version ~doc ~sdocs ~exits:Term.default_exits ~man ) + +let () = + match Term.(eval_choice default_cmd [ config_cmd ]) with + | `Error _ -> Caml.exit 1 + | _ -> Caml.exit (if Logs.err_count () > 0 then 1 else 0)