main.ml 6.67 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10 11 12 13 14 15 16 17
(********************************************************************)

open Format
open Why3
open Whyconf
open Theory

let usage_msg = sprintf
18
  "Usage: %s [options] <command> [options]"
19 20 21 22 23 24 25
  (Filename.basename Sys.argv.(0))

let opt_list_transforms = ref false
let opt_list_printers = ref false
let opt_list_provers = ref false
let opt_list_formats = ref false
let opt_list_metas = ref false
Andrei Paskevich's avatar
Andrei Paskevich committed
26
let opt_list_attrs = ref false
27

28
let option_list = [
29
  "--list-transforms", Arg.Set opt_list_transforms,
30
      " list known transformations";
31
  "--list-printers", Arg.Set opt_list_printers,
32
      " list known printers";
33
  "--list-provers", Arg.Set opt_list_provers,
34
      " list known provers";
35
  "--list-formats", Arg.Set opt_list_formats,
36
      " list known input formats";
37
  "--list-metas", Arg.Set opt_list_metas,
38
      " list known metas";
Andrei Paskevich's avatar
Andrei Paskevich committed
39
  "--list-attributes", Arg.Set opt_list_attrs, "list used attributes";
40 41 42 43 44 45 46
  "--print-libdir",
      Arg.Unit (fun _ -> printf "%s@." Config.libdir; exit 0),
      " print location of binary components (plugins, etc)";
  "--print-datadir",
      Arg.Unit (fun _ -> printf "%s@." Config.datadir; exit 0),
      " print location of non-binary data (theories, modules, etc)";
  "--version",
47 48
      Arg.Unit (fun _ -> printf "Why3 platform, version %s@."
        Config.version; exit 0),
49 50 51 52
      " print version information";
]

let command_path = match Config.localdir with
53 54 55
  | Some p -> Filename.concat p "bin"
  | None -> Filename.concat Config.libdir "commands"

56 57 58 59
let extra_help fmt commands =
  fprintf fmt "@\nAvailable commands:@.";
  List.iter (fun (v,_) -> fprintf fmt "  %s@." v) commands

60 61 62
let available_commands () =
  let commands = Sys.readdir command_path in
  Array.sort String.compare commands;
63
  let re = Str.regexp "^why3\\([^.]+\\)\\([.].*\\)?" in
64 65 66 67 68 69 70 71 72 73
  let commands = Array.fold_left (fun acc v ->
    if Str.string_match re v 0 then
      let w = Str.matched_group 1 v in
      match acc with
      | (h,_)::_ when h = w -> acc
      | _ -> (w, v) :: acc
    else acc) [] commands in
  List.rev commands

let command sscmd =
74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
  let sscmd,args =
    let cur = !Arg.current in
    if sscmd = "help" then begin
      if cur + 1 >= Array.length Sys.argv then begin
        let extra_help fmt () = extra_help fmt (available_commands ()) in
        Args.exit_with_usage ~exit_code:0 ~extra_help option_list usage_msg
      end;
      let sscmd = Sys.argv.(cur + 1) in
      sscmd, ["--help"]
    end else begin
      let args = ref [] in
      for i = 1 to Array.length Sys.argv - 1 do
        if i <> cur then args := Sys.argv.(i) :: !args;
      done;
      sscmd, List.rev !args
    end in
90
  let cmd =
91 92
    let scmd = "why3" ^ sscmd in
    let cmd = Filename.concat command_path scmd in
93
    if cmd <> "" && Sys.file_exists cmd
94
    then cmd
95 96 97
    else begin
      let commands = available_commands () in
      let scmd =
98 99 100 101 102 103
        try List.assoc sscmd commands
        with Not_found ->
          eprintf "'%s' is not a Why3 command.@\n%a"
            sscmd extra_help commands;
          exit 1 in
      Filename.concat command_path scmd
104
    end in
105
  let scmd = "why3 " ^ sscmd in
106
  Unix.execv cmd (Array.of_list (scmd :: args))
107 108

let () = try
109
  let extra_help fmt () = extra_help fmt (available_commands ()) in
110
  let config,_,_ = Args.initialize ~extra_help option_list command usage_msg in
111

112
  (* listings *)
113 114 115 116 117 118 119 120 121 122 123 124

  let sort_pair (x,_) (y,_) = String.compare x y in
  let opt_list = ref false in
  if !opt_list_transforms then begin
    opt_list := true;
    let print_trans_desc fmt (x,r) =
      fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" x Pp.formatted r in
    printf "@[<hov 2>Known non-splitting transformations:@\n%a@]@\n@."
      (Pp.print_list Pp.newline2 print_trans_desc)
      (List.sort sort_pair (Trans.list_transforms ()));
    printf "@[<hov 2>Known splitting transformations:@\n%a@]@\n@."
      (Pp.print_list Pp.newline2 print_trans_desc)
125 126
      (List.sort sort_pair (Trans.list_transforms_l ()));
    let list_transform_with_arg =
127 128
      Trans.list_transforms_with_args () @
      Trans.list_transforms_with_args_l () in
129 130 131
    printf "@[<hov 2>Known transformations with arguments:@\n%a@]@\n@."
      (Pp.print_list Pp.newline2 print_trans_desc)
      (List.sort sort_pair list_transform_with_arg)
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
  end;
  if !opt_list_printers then begin
    opt_list := true;
    let print_printer_desc fmt (s,f) =
      fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" s Pp.formatted f in
    printf "@[<hov 2>Known printers:@\n%a@]@\n@."
      (Pp.print_list Pp.newline2 print_printer_desc)
      (List.sort sort_pair (Printer.list_printers ()))
  end;
  if !opt_list_formats then begin
    opt_list := true;
    let print1 fmt s = fprintf fmt "%S" s in
    let print fmt (p, l, f) =
      fprintf fmt "@[%s [%a]@\n  @[%a@]@]"
        p (Pp.print_list Pp.comma print1) l
        Pp.formatted f
    in
    printf "@[Known input formats:@\n  @[%a@]@]@."
      (Pp.print_list Pp.newline2 print)
151
      (List.sort Pervasives.compare (Env.list_formats Env.base_language))
152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172
  end;
  if !opt_list_provers then begin
    opt_list := true;
    let print = Pp.print_iter2 Mprover.iter Pp.newline Pp.nothing
      print_prover Pp.nothing in
    let provers = get_provers config in
    printf "@[<hov 2>Known provers:@\n%a@]@." print provers
  end;
  if !opt_list_metas then begin
    opt_list := true;
    let print fmt m = fprintf fmt "@[<h 2>%s %s%a@\n@[<hov>%a@]@]"
      (let s = m.meta_name in
        if String.contains s ' ' then "\"" ^ s ^ "\"" else s)
      (if m.meta_excl then "(flag) " else "")
      (Pp.print_list Pp.space Pretty.print_meta_arg_type) m.meta_type
      Pp.formatted m.meta_desc
    in
    let cmp m1 m2 = Pervasives.compare m1.meta_name m2.meta_name in
    printf "@[<hov 2>Known metas:@\n%a@]@\n@."
      (Pp.print_list Pp.newline2 print) (List.sort cmp (Theory.list_metas ()))
  end;
Andrei Paskevich's avatar
Andrei Paskevich committed
173
  if !opt_list_attrs then begin
174
    opt_list := true;
Andrei Paskevich's avatar
Andrei Paskevich committed
175
    let l = List.sort String.compare (Ident.list_attributes ()) in
176 177
    List.iter (fun x -> Format.eprintf "%s@." x) l
  end;
178 179
  if !opt_list then exit 0;

180
  printf "@[%s%a@]" usage_msg extra_help ()
181

182 183 184
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1