1
1
structure Util =
2
2
struct
3
3
4
- (* ** Printing utilites * **)
4
+ (* * Printing utilites **)
5
5
fun println s = print (s ^ " \n " )
6
6
7
7
fun list_to_string f = (fn x => " [" ^ x ^ " ]" ) o String.concatWith " , " o map f
@@ -10,6 +10,7 @@ fun print_result NONE = println("Invalid input\n")
10
10
| print_result (SOME true ) = println(" Property is satisfied\n " )
11
11
| print_result (SOME false ) = println(" Property is not satisfied\n " )
12
12
13
+ (* * File reading **)
13
14
fun read_lines stream =
14
15
let
15
16
val input = TextIO.inputLine stream
@@ -20,16 +21,33 @@ fun read_lines stream =
20
21
| SOME input => input ^ read_lines stream
21
22
end
22
23
23
- fun find_with_arg P [] = NONE
24
- | find_with_arg P [_] = NONE
25
- | find_with_arg P (x :: y :: xs) = if P x then SOME y else find_with_arg P (y :: xs)
24
+ fun read_file f =
25
+ let
26
+ val file = TextIO.openIn f
27
+ val s = read_lines file
28
+ val _ = TextIO.closeIn file
29
+ in s end
26
30
31
+ (* * Processing command line arguments **)
27
32
datatype 'a argument = Is_Present | Is_Not_Present | Has_Val of 'a
28
33
29
34
type arguments = string argument list
30
35
31
36
exception Unknown_Argument of string
32
37
38
+ datatype argument_type = Arg | Flag
39
+
40
+ val common_arguments = [
41
+ ([" deadlock" , " dc" ], " Ignore formula and run deadlock check." , Flag),
42
+ ([" model" , " m" ],
43
+ " Input file for the model & formula. "
44
+ ^ " If this is not specified, the input is read from stdin." ,
45
+ Arg),
46
+ ([" help" , " h" , " ?" ], " Show this help string." , Flag),
47
+ ([" cpu-time" , " cpu" ], " Report CPU time." , Flag),
48
+ ([" num-threads" , " n" ], " Number of threads." , Arg)
49
+ ]
50
+
33
51
val the_args = ref []
34
52
35
53
fun is_present arg = case List.find (fn (k, v) => k = arg) (!the_args) of
@@ -44,18 +62,9 @@ fun find_arg arg = case List.find (fn (k, v) => k = arg) (!the_args) of
44
62
45
63
val get_arg = the o find_arg
46
64
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
- ]
65
+ fun find_with_arg P [] = NONE
66
+ | find_with_arg P [_] = NONE
67
+ | find_with_arg P (x :: y :: xs) = if P x then SOME y else find_with_arg P (y :: xs)
59
68
60
69
fun read_arguments arguments =
61
70
let
@@ -82,11 +91,4 @@ fun print_usage arguments =
82
91
|> (fn s => " Usage:\n " ^ s)
83
92
|> println
84
93
85
- fun read_file f =
86
- let
87
- val file = TextIO.openIn f
88
- val s = read_lines file
89
- val _ = TextIO.closeIn file
90
- in s end
91
-
92
94
end
0 commit comments