Skip to content

Commit d7e9ad3

Browse files
wimmerswimmers
committed
Streamline command line arguments
1 parent 6b7a22f commit d7e9ad3

File tree

3 files changed

+116
-59
lines changed

3 files changed

+116
-59
lines changed

‎ML/Muntac.sml

Lines changed: 35 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ fun print_timings () =
88
in map print_time tab; () end
99

1010
(*** Wrapping up the checker ***)
11-
fun
11+
fun run_and_print
1212
implementation num_threads check_deadlock s =
1313
let
1414
val debug_level: Int32.int Unsynchronized.ref = ref 0
@@ -46,7 +46,7 @@ fun check_and_verify_from_stream implementation num_threads model check_deadlock
4646
if input = ""
4747
then println "Failed to read line from input!"
4848
(* We append a space to terminate the input for the parser *)
49-
else input ^ " " |>
49+
else input ^ " " |> run_and_print
5050
implementation num_threads check_deadlock
5151
end;
5252

@@ -105,17 +105,25 @@ fun read_and_check check_deadlock (model, certificate, renaming, implementation,
105105
)
106106
end
107107

108+
val arguments = common_arguments @ [
109+
(["show-cert", "sc"], "Print the certificate.", Flag),
110+
(["renaming", "r"], "Path to renaming JSON.", Arg),
111+
(["certificate", "c"], "Path to binary certificate.", Arg),
112+
(["implementation", "i"], "The certifier variant to choose.", Arg)
113+
]
114+
108115
fun main () =
109116
let
110-
val args = CommandLine.arguments()
111-
val check_deadlock = List.find (fn x => x = "-deadlock" orelse x = "-dc") args <> NONE
112-
val cpu_time = List.find (fn x => x = "-cpu-time" orelse x = "-cpu") args <> NONE
113-
val model = find_with_arg (fn x => x = "-model" orelse x = "-m") args
114-
val certificate = find_with_arg (fn x => x = "-certificate" orelse x = "-c") args
115-
val renaming = find_with_arg (fn x => x = "-renaming" orelse x = "-r") args
116-
val num_threads = find_with_arg (fn x => x = "-num-threads" orelse x = "-n") args
117-
val implementation = find_with_arg (fn x => x = "-implementation" orelse x = "-i") args
118-
val show_cert = List.find (fn x => x = "-explored" orelse x = "-e") args <> NONE
117+
val _ = read_arguments arguments
118+
val check_deadlock = is_present "deadlock"
119+
val cpu_time = is_present "cpu-time"
120+
val model = find_arg "model"
121+
val num_threads = find_arg "num-threads"
122+
val show_help = is_present "help"
123+
val certificate = find_arg "certificate"
124+
val renaming = find_arg "renaming"
125+
val implementation = find_arg "implementation"
126+
val show_cert = is_present "show-cert"
119127
fun convert f NONE = NONE
120128
| convert f (SOME x) = SOME (f x)
121129
handle Fail msg => (println ("Argument error: " ^ msg); OS.Process.exit OS.Process.failure)
@@ -151,17 +159,21 @@ fun main () =
151159
val args = [model, certificate, renaming]
152160
val _ = if cpu_time then Timing.set_cpu true else ()
153161
in
154-
if certificate = NONE andalso renaming = NONE andalso model <> NONE then
155-
(
156-
println "Falling back to munta!";
157-
check_and_verify_from_stream implementation num_threads (the model) check_deadlock
162+
if show_help then
163+
print_usage arguments
164+
else (
165+
if certificate = NONE andalso renaming = NONE andalso model <> NONE then
166+
(
167+
println "Falling back to munta!";
168+
check_and_verify_from_stream implementation num_threads (the model) check_deadlock
169+
)
170+
else if exists (fn x => x = NONE) args then
171+
println "Missing command line arguments!"
172+
else
173+
let
174+
val [model, certificate, renaming] = map the args
175+
in
176+
read_and_check check_deadlock (model, certificate, renaming, implementation, num_threads, show_cert)
177+
end
158178
)
159-
else if exists (fn x => x = NONE) args then
160-
println "Missing command line arguments!"
161-
else
162-
let
163-
val [model, certificate, renaming] = map the args
164-
in
165-
read_and_check check_deadlock (model, certificate, renaming, implementation, num_threads, show_cert)
166-
end
167179
end

‎ML/Muntax.sml

Lines changed: 23 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ fun run_and_print check_deadlock s =
2424
val _ = println("")
2525
in () end else ()
2626
in println r end
27-
end;
27+
end
2828

2929
fun check_and_verify_from_stream stream _ =
3030
let
@@ -36,27 +36,18 @@ fun check_and_verify_from_stream stream _ =
3636
then println "Failed to read line from input!"
3737
(* We append a space to terminate the input for the parser *)
3838
else input ^ " " |> run_and_print check_deadlock
39-
end;
39+
end
4040

4141
val to_large_int = fn x => x;
4242

43-
fun print_usage () =
43+
fun print_json () =
4444
let
45-
val prelude = "Usage:\n"
46-
val usage = [
47-
("m ", "Input file for the model & formula. "
48-
^ "If this is not specified, the input is read from stdin."),
49-
("dc", "Ignore formula and run deadlock check."),
50-
("e ", "Report set of explored states (only works for reachability formulas)."),
51-
("s ", "Print back the JSON that was parsed from the input.")
52-
]
53-
in
54-
usage
55-
|> map (fn (opt, s) => "-" ^ opt ^ ": " ^ s ^ "\n")
56-
|> String.concat
57-
|> (fn s => prelude ^ s)
58-
|> println
59-
end
45+
val messages = Logging.get_trace ()
46+
val jsons = filter (fn (i, s) => i = 2) messages |> map snd
47+
val _ = println ""
48+
val _ = println "The following JSON was read by the parser:"
49+
val _ = if length jsons > 0 then println (hd jsons) else ()
50+
in () end
6051

6152
fun print_explored () =
6253
let
@@ -72,16 +63,21 @@ fun print_explored () =
7263
val _ = if length final > 0 then map println final else [()]
7364
in () end
7465

66+
val arguments = common_arguments @ [
67+
(["explored", "e"], "Report set of explored states (only works for reachability formulas).", Flag),
68+
(["show", "s"], "Print back the JSON that was parsed from the input.", Flag)
69+
]
70+
7571
fun main () =
7672
let
77-
val args = CommandLine.arguments()
78-
val check_deadlock = List.find (fn x => x = "-deadlock" orelse x = "-dc") args <> NONE
79-
val cpu_time = List.find (fn x => x = "-cpu-time" orelse x = "-cpu") args <> NONE
80-
val trace_explored = List.find (fn x => x = "-explored" orelse x = "-e") args <> NONE
81-
val model = find_with_arg (fn x => x = "-model" orelse x = "-m") args
82-
val num_threads = find_with_arg (fn x => x = "-num-threads" orelse x = "-n") args
83-
val show_json = List.find (fn x => x = "-show" orelse x = "-s") args <> NONE
84-
val show_help = List.find (fn x => x = "-help" orelse x = "-h" orelse x = "-?") args <> NONE
73+
val _ = read_arguments arguments
74+
val check_deadlock = is_present "deadlock"
75+
val cpu_time = is_present "cpu-time"
76+
val trace_explored = is_present "explored"
77+
val model = find_arg "model"
78+
val num_threads = find_arg "num-threads"
79+
val show_json = is_present "show"
80+
val show_help = is_present "help"
8581
fun convert f NONE = NONE
8682
| convert f (SOME x) = SOME (f x)
8783
handle Fail msg => (println ("Argument error: " ^ msg); OS.Process.exit OS.Process.failure)
@@ -107,7 +103,7 @@ fun main () =
107103
val input = ref ""
108104
in
109105
if show_help then
110-
print_usage ()
106+
print_usage arguments
111107
else (case model of
112108
NONE => input := read_lines TextIO.stdIn |
113109
SOME f =>

‎ML/Util.sml

Lines changed: 58 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -24,20 +24,69 @@ fun find_with_arg P [] = NONE
2424
| find_with_arg P [_] = NONE
2525
| find_with_arg P (x :: y :: xs) = if P x then SOME y else find_with_arg P (y :: xs)
2626

27+
datatype 'a argument = Is_Present | Is_Not_Present | Has_Val of 'a
28+
29+
type arguments = string argument list
30+
31+
exception Unknown_Argument of string
32+
33+
val the_args = ref []
34+
35+
fun is_present arg = case List.find (fn (k, v) => k = arg) (!the_args) of
36+
NONE => raise Unknown_Argument arg
37+
| SOME (_, Is_Not_Present) => false
38+
| _ => true
39+
40+
fun find_arg arg = case List.find (fn (k, v) => k = arg) (!the_args) of
41+
NONE => raise Unknown_Argument arg
42+
| SOME (_, Has_Val v) => SOME v
43+
| _ => NONE
44+
45+
val get_arg = the o find_arg
46+
47+
datatype argument_type = Arg | Flag
48+
49+
val common_arguments = [
50+
(["deadlock", "dc"], "Ignore formula and run deadlock check.", Flag),
51+
(["model", "m"],
52+
"Input file for the model & formula. "
53+
^ "If this is not specified, the input is read from stdin.",
54+
Arg),
55+
(["help", "h", "?"], "Show this help string.", Flag),
56+
(["cpu-time", "cpu"], "Report CPU time.", Flag),
57+
(["num-threads", "n"], "Number of threads.", Arg)
58+
]
59+
60+
fun read_arguments arguments =
61+
let
62+
val args = CommandLine.arguments()
63+
fun find_name names name = List.find (fn x => "-" ^ x = name) names <> NONE
64+
fun find_it (names, Flag) =
65+
(case List.find (find_name names) args of
66+
NONE => Is_Not_Present
67+
| SOME _ => Is_Present)
68+
| find_it (names, Arg) =
69+
(case find_with_arg (find_name names) args of
70+
NONE => Is_Not_Present
71+
| SOME x => Has_Val x)
72+
val args = map (fn (names, _, typ) => (hd names, find_it (names, typ))) arguments
73+
in
74+
the_args := args
75+
end
76+
77+
fun print_usage arguments =
78+
arguments
79+
|> map (fn (names, descr, _) =>
80+
(map (fn s => "-" ^ s ^ " ") names|> String.concat) ^ ": " ^ descr ^ "\n")
81+
|> String.concat
82+
|> (fn s => "Usage:\n" ^ s)
83+
|> println
84+
2785
fun read_file f =
2886
let
2987
val file = TextIO.openIn f
3088
val s = read_lines file
3189
val _ = TextIO.closeIn file
3290
in s end
3391

34-
fun print_json () =
35-
let
36-
val messages = Logging.get_trace ()
37-
val jsons = filter (fn (i, s) => i = 2) messages |> map snd
38-
val _ = println ""
39-
val _ = println "The following JSON was read by the parser:"
40-
val _ = if length jsons > 0 then println (hd jsons) else ()
41-
in () end
42-
4392
end

0 commit comments

Comments
 (0)