1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
module ToolOptions
( Options(..), defaultOptions, processOptions
, whenStatus, printWhenStatus, printWhenIntermediate, printWhenAll
)
where
import GetOpt
import ReadNumeric ( readNat )
import System ( exitWith )
import System.CurryPath ( stripCurrySuffix )
data Options = Options
{ optVerb :: Int
, optHelp :: Bool
, optName :: String
, optError :: Bool
, optRec :: Bool
, optContract:: Bool
, optStrict :: Bool
, optTime :: Bool
}
defaultOptions :: Options
defaultOptions = Options 1 False "" False False False False False
processOptions :: String -> [String] -> IO (Options,[String])
processOptions banner argv = do
let (funopts, args, opterrors) = getOpt Permute options argv
opts = foldl (flip id) defaultOptions funopts
unless (null opterrors)
(putStr (unlines opterrors) >> printUsage >> exitWith 1)
when (optHelp opts) (printUsage >> exitWith 0)
return (opts, map stripCurrySuffix args)
where
printUsage = putStrLn (banner ++ "\n" ++ usageText)
usageText :: String
usageText =
usageInfo ("Usage: curry-failfree [options] <module names>\n") options
options :: [OptDescr (Options -> Options)]
options =
[ Option "h?" ["help"]
(NoArg (\opts -> opts { optHelp = True }))
"print help and exit"
, Option "n" ["name"]
(ReqArg (\s opts -> opts { optName = s }) "<f>")
"show only the name of a non-fail condition"
, Option "q" ["quiet"]
(NoArg (\opts -> opts { optVerb = 0 }))
"run quietly (no output, only exit code)"
, Option "v" ["verbosity"]
(OptArg (maybe (checkVerb 2) (safeReadNat checkVerb)) "<n>")
"verbosity level:\n0: quiet (same as `-q')\n1: show status messages (default)\n2: show intermediate results (same as `-v')\n3: show all details (e.g., SMT scripts)"
, Option "e" ["error"]
(NoArg (\opts -> opts { optError = True }))
"consider 'Prelude.error' as a failing operation"
, Option "r" ["recursive"]
(NoArg (\opts -> opts { optRec = True }))
"recursive, i.e., verify imported modules first"
, Option "c" ["contract"]
(NoArg (\opts -> opts { optContract = True }))
"consider contracts (pre/postcondition) for verification"
, Option "s" ["strict"]
(NoArg (\opts -> opts { optStrict = True }))
"check contracts w.r.t. strict evaluation strategy"
, Option "t" ["time"]
(NoArg (\opts -> opts { optTime = True }))
"show total verification time for each module"
]
where
safeReadNat opttrans s opts =
let numError = error "Illegal number argument (try `-h' for help)"
in maybe numError
(\ (n,rs) -> if null rs then opttrans n opts else numError)
(readNat s)
checkVerb n opts = if n>=0 && n<4
then opts { optVerb = n }
else error "Illegal verbosity level (try `-h' for help)"
whenStatus :: Options -> IO () -> IO ()
whenStatus opts = when (optVerb opts > 0)
printWhenStatus :: Options -> String -> IO ()
printWhenStatus opts s = whenStatus opts (printWT s)
printWhenIntermediate :: Options -> String -> IO ()
printWhenIntermediate opts s =
when (optVerb opts > 1) (printWT s)
printWhenAll :: Options -> String -> IO ()
printWhenAll opts s =
when (optVerb opts > 2) (printWT s)
printWT :: String -> IO ()
printWT s = putStrLn $ s
|