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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168

-------------------------------------------------------------------------
--- The options of the verification tool together with some
--- related operations.
---
--- @author Michael Hanus
--- @version November 2023
-------------------------------------------------------------------------

module Verify.Options
  ( Options(..), defaultOptions, processOptions
  , whenStatus, printWhenStatus, printWhenIntermediate, printWhenDetails
  , printWhenAll
  )
 where

import Curry.Compiler.Distribution ( curryCompiler, curryCompilerMajorVersion
                                   , curryCompilerMinorVersion
                                   , curryCompilerRevisionVersion )

import Control.Monad         ( when, unless )
import Data.Char             ( toUpper )
import Data.List             ( intercalate )
import Numeric               ( readNat )
import System.Console.GetOpt

import System.CurryPath      ( stripCurrySuffix )
import System.IO             ( hFlush, stdout )
import System.Process        ( exitWith )

data Options = Options
  { optVerb        :: Int  -- verbosity (0: quiet, 1: status, 2: interm, 3: all)
  , optHelp        :: Bool -- if help info should be printed
  , optFunction    :: String -- show the result for this function
  , optImports     :: Bool -- read/analyze imports/prelude? (only for testing)
  , optDeleteCache :: Bool -- delete the analysis cache?
  , optRerun       :: Bool -- rerun verification of current module
  , optPublic      :: Bool -- show types (call, in/out) of public ops only? 
  , optCallTypes   :: Bool -- show call types
  , optIOTypes     :: Bool -- show input/output types
  , optVerify      :: Bool -- verify call types
  , optError       :: Bool -- consider Prelude.error as failing operation?
  , optModule      :: Bool -- generate a `..._CALLTYPES` module?
  , optStats       :: Bool -- show and store statitics?
  , optTime        :: Bool -- show elapsed verification time?
  , optDomainID    :: String -- the unique id for the abstract term domain
  }

--- The default options of the verification tool.
defaultOptions :: Options
defaultOptions =
  Options 1 False "" True False False True False False True False
          False False False ""

--- Process the actual command line argument and return the options
--- and the name of the main program.
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)

-- Help text
usageText :: String
usageText =
  usageInfo ("Usage: curry-calltypes [options] <module names>\n") options

-- Definition of actual command line options.
options :: [OptDescr (Options -> Options)]
options =
  [ Option "h?" ["help"]
           (NoArg (\opts -> opts { optHelp = True }))
           "print help and exit"
  , 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 also verification details\n4: show all details"
  , Option "a" ["all"]
            (NoArg (\opts -> opts { optPublic = False }))
           "show types for all (also private) operations"
  , Option "c" ["calltypes"]
            (NoArg (\opts -> opts { optCallTypes = True }))
           "show call types"
  , Option "d" ["domain"]
           (ReqArg checkDomain "<d>")
           "the analysis domain (Values|Values2|Values5)"
  , Option "" ["delete"]
           (NoArg (\opts -> opts { optDeleteCache = True }))
           ("delete all cache files (for " ++ sysname ++ ")")
  , Option "e" ["error"]
           (NoArg (\opts -> opts { optError = True }))
           "consider 'Prelude.error' as a failing operation"
  , Option "f" ["function"]
            (ReqArg (\s opts -> opts { optFunction = s }) "<f>")
            "show the call and in/out type for function <f>"
  , Option "i" ["iotypes"]
            (NoArg (\opts -> opts { optIOTypes = True }))
           "show input/output types"
  --, Option "m" ["module"]
  --         (NoArg (\opts -> opts { optModule = True }))
  --         "write  a '..._CALLTYPES' module with required\ncall types"
  , Option "" ["noimports"]
           (NoArg (\opts -> opts { optImports = False }))
           "do not read/analyze imported modules (for testing)"
  , Option "n" ["noverify"]
           (NoArg (\opts -> opts { optVerify = False }))
           "do not verify call types in function calls"
  , Option "r" ["rerun"]
           (NoArg (\opts -> opts { optRerun = True }))
           "rerun verification of current module\n(ignore results of previous verification)"
  , Option "s" ["statistics"]
           (NoArg (\opts -> opts { optStats = True }))
           "show/store statistics (functions, failures,...)"
  , Option "t" ["time"]
           (NoArg (\opts -> opts { optTime = True }))
           "show total verification time for each module"
  ]
 where
  safeReadNat opttrans s opts = case readNat s of
    [(n,"")] -> opttrans n opts
    _        -> error "Illegal number argument (try `-h' for help)"

  checkVerb n opts = if n >= 0 && n <= 4
                       then opts { optVerb = n }
                       else error "Illegal verbosity level (try `-h' for help)"

  checkDomain s opts =
    if s `elem` ["Values", "Values2", "Values5"]
      then opts { optDomainID = s }
      else error "Illegal domain ID, allowed values: Value|Values2|Values5"

  sysname = curryCompiler ++ "-" ++
            intercalate "."
              (map show [ curryCompilerMajorVersion
                        , curryCompilerMinorVersion
                        , curryCompilerRevisionVersion ])

-------------------------------------------------------------------------

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)

printWhenDetails :: Options -> String -> IO ()
printWhenDetails opts s =
 when (optVerb opts > 2) (printWT s)

printWhenAll :: Options -> String -> IO ()
printWhenAll opts s =
 when (optVerb opts > 3) (printWT s)

printWT :: String -> IO ()
printWT s = do putStrLn $ s --"NON-FAIL INFERENCE: " ++ s
               hFlush stdout

---------------------------------------------------------------------------