Options.curry 5.99 KB
Newer Older
Michael Hanus 's avatar
Michael Hanus committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
------------------------------------------------------------------------------
--- Definition and processing of options for CurryCheck
------------------------------------------------------------------------------

module CC.Options where

import Char        ( toUpper )
import GetOpt
import IO
import List        ( isPrefixOf )
import ReadNumeric ( readNat )

------------------------------------------------------------------------------
-- Representation of command line options.
data Options = Options
  { optHelp     :: Bool
  , optVerb     :: Int
  , optKeep     :: Bool
  , optMaxTest  :: Int
  , optMaxFail  :: Int
  , optDefType  :: String
  , optSource   :: Bool
Michael Hanus 's avatar
Michael Hanus committed
23
  , optIOTest   :: Bool
Michael Hanus 's avatar
Michael Hanus committed
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
  , optProp     :: Bool
  , optSpec     :: Bool
  , optDet      :: Bool
  , optProof    :: Bool
  , optEquiv    :: EquivOption
  , optTime     :: Bool
  , optColor    :: Bool
  , optMainProg :: String
  }

-- Default command line options.
defaultOptions :: Options
defaultOptions  = Options
  { optHelp     = False
  , optVerb     = 1
  , optKeep     = False
  , optMaxTest  = 0
  , optMaxFail  = 0
  , optDefType  = "Ordering"
  , optSource   = True
Michael Hanus 's avatar
Michael Hanus committed
44
  , optIOTest   = True
Michael Hanus 's avatar
Michael Hanus committed
45 46 47 48 49 50 51 52 53 54 55
  , optProp     = True
  , optSpec     = True
  , optDet      = True
  , optProof    = True
  , optEquiv    = Manual
  , optTime     = False
  , optColor    = True
  , optMainProg = ""
  }

--- Options for equivalence tests.
56
data EquivOption = Safe | Autoselect | Manual | Ground
Michael Hanus 's avatar
Michael Hanus committed
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
 deriving Eq

-- 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 3) (safeReadNat checkVerb)) "<n>")
            "verbosity level:\n0: quiet (same as `-q')\n1: show test names (default)\n2: show more information about test generation\n3: show test data (same as `-v')\n4: show also some debug information"
  , Option "k" ["keep"] (NoArg (\opts -> opts { optKeep = True }))
           "keep temporarily generated program files"
  , Option "m" ["maxtests"]
           (ReqArg (safeReadNat (\n opts -> opts { optMaxTest = n })) "<n>")
           "maximal number of tests (default: 100)"
  , Option "f" ["maxfails"]
           (ReqArg (safeReadNat (\n opts -> opts { optMaxFail = n })) "<n>")
           "maximal number of condition failures\n(default: 10000)"
  , Option "d" ["deftype"]
           (ReqArg checkDefType "<t>")
           "type for defaulting polymorphic tests:\nBool | Int | Char | Ordering (default)"
  , Option "e" ["equivalence"]
           (ReqArg checkEquivOption "<e>")
82
           "option for equivalence tests:\nsafe | autoselect | manual (default) | ground"
Michael Hanus 's avatar
Michael Hanus committed
83 84 85 86 87
  , Option "t" ["time"] (NoArg (\opts -> opts { optTime = True }))
           "show run time for executing each property test"
  , Option "" ["nosource"]
           (NoArg (\opts -> opts { optSource = False }))
           "do not perform source code checks"
Michael Hanus 's avatar
Michael Hanus committed
88 89 90
  , Option "" ["noiotest"]
           (NoArg (\opts -> opts { optIOTest = False }))
           "do not test I/O properties"
Michael Hanus 's avatar
Michael Hanus committed
91 92
  , Option "" ["noprop"]
           (NoArg (\opts -> opts { optProp = False }))
Michael Hanus 's avatar
Michael Hanus committed
93
           "do not perform property tests"
Michael Hanus 's avatar
Michael Hanus committed
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
  , Option "" ["nospec"]
           (NoArg (\opts -> opts { optSpec = False }))
           "do not perform specification/postcondition tests"
  , Option "" ["nodet"]
           (NoArg (\opts -> opts { optDet = False }))
           "do not perform determinism tests"
  , Option "" ["noproof"]
           (NoArg (\opts -> opts { optProof = False }))
           "do not consider proofs to simplify properties"
  , Option "" ["nocolor"]
           (NoArg (\opts -> opts { optColor = False }))
           "do not use colors when showing tests"
  , Option "" ["mainprog"]
           (ReqArg (\s opts -> opts { optMainProg = s }) "<prog>")
           "name of generated main program\n(default: TEST<pid>.curry)"
  ]
 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<5
                     then opts { optVerb = n }
                     else error "Illegal verbosity level (try `-h' for help)"

  checkDefType s opts = if s `elem` ["Bool","Int","Char","Ordering"]
                        then opts { optDefType = s }
                        else error "Illegal default type (try `-h' for help)"

  checkEquivOption s opts
126 127 128
    | ls `isPrefixOf` "SAFE"       = opts { optEquiv = Safe }
    | ls `isPrefixOf` "AUTOSELECT" = opts { optEquiv = Autoselect }
    | ls `isPrefixOf` "MANUAL"     = opts { optEquiv = Manual }
129
    | ls `isPrefixOf` "GROUND"     = opts { optEquiv = Ground }
Michael Hanus 's avatar
Michael Hanus committed
130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146
    | otherwise = error "Illegal equivalence option (try `-h' for help)"
   where ls = map toUpper s

--- Further option processing, e.g., setting coloring mode.
processOpts :: Options -> IO Options
processOpts opts = do
  isterm <- hIsTerminalDevice stdout
  return $ if isterm then opts else opts { optColor = False}

isQuiet :: Options -> Bool
isQuiet opts = optVerb opts == 0

--- Print second argument if verbosity level is not quiet:
putStrIfNormal :: Options -> String -> IO ()
putStrIfNormal opts s = unless (isQuiet opts) (putStr s >> hFlush stdout)

--- Print second argument if verbosity level > 1:
147 148
putStrIfDetails :: Options -> String -> IO ()
putStrIfDetails opts s = when (optVerb opts > 1) (putStr s >> hFlush stdout)
Michael Hanus 's avatar
Michael Hanus committed
149 150 151 152 153 154 155 156 157 158

--- Print second argument if verbosity level > 3:
putStrLnIfDebug :: Options -> String -> IO ()
putStrLnIfDebug opts s = when (optVerb opts > 3) (putStrLn s >> hFlush stdout)

--- use some coloring (from library AnsiCodes) if color option is on:
withColor :: Options -> (String -> String) -> String -> String
withColor opts coloring = if optColor opts then coloring else id

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