0 | module Hedgehog.Internal.Options
 1 |
 2 | import Data.String
 3 | import Decidable.Equality
 4 | import Hedgehog.Internal.Property
 5 | import System.GetOpts
 6 |
 7 | %default total
 8 |
 9 | public export
10 | data NumTest = Relaxed TestLimit | Forced TestLimit
11 |
12 | public export
13 | record Config where
14 |   constructor MkConfig
15 |   printHelp  : Bool
16 |   numTests   : Maybe NumTest
17 |   numShrinks : Maybe ShrinkLimit
18 |   confidence : Maybe Confidence
19 |
20 | export
21 | init : Config
22 | init = MkConfig False Nothing Nothing Nothing
23 |
24 | parseNat : String -> Either (List String) Nat
25 | parseNat s =
26 |   maybe (Left [#"Not a natural number: \#{s}"#]) Right $ parsePositive s
27 |
28 | toConfidence : Nat -> Either (List String) Confidence
29 | toConfidence n =
30 |   let c := cast {to = Bits64} n
31 |    in case decEq (c >= 2) True of
32 |         (Yes prf)   => Right $ MkConfidence c prf
33 |         (No contra) => Left [ #"Not a valid confidence value: \#{show n}"# ]
34 |
35 | setTests : String -> Config -> Either (List String) Config
36 | setTests s c =
37 |   map
38 |     (\n => { numTests := Just $ Relaxed $ MkTagged n} c)
39 |     (parseNat s)
40 |
41 | setShrinks : String -> Config -> Either (List String) Config
42 | setShrinks s c =
43 |   map
44 |     (\n => { numShrinks := Just $ MkTagged n} c)
45 |     (parseNat s)
46 |
47 | setConfidence : String -> Config -> Either (List String) Config
48 | setConfidence s c =
49 |   map
50 |     (\n => { confidence := Just n} c)
51 |     (parseNat s >>= toConfidence)
52 |
53 | setTestsForced : String -> Config -> Either (List String) Config
54 | setTestsForced s c =
55 |   map
56 |     (\n => { numTests := Just $ Forced $ MkTagged n} c)
57 |     (parseNat s)
58 |
59 | setHelp : Config -> Either (List String) Config
60 | setHelp = Right . { printHelp := True }
61 |
62 | descs : List $ OptDescr (Config -> Either (List String) Config)
63 | descs =
64 |   [ MkOpt ['n'] ["testlimit"] (ReqArg setTests "<tests>")
65 |       "number of tests to be passed by each property"
66 |   , MkOpt ['N'] ["testlimit!"] (ReqArg setTestsForced "<tests>")
67 |       "like -n but includes tests that are only run once"
68 |   , MkOpt ['s'] ["shrinklimit"] (ReqArg setShrinks "<shrinks>")
69 |       "maximal number of shrinks in case of a failed test"
70 |   , MkOpt ['c'] ["confidence"] (ReqArg setConfidence "<confidence>")
71 |       "acceptable occurence of false positives"
72 |   , MkOpt [] ["--help"] (NoArg setHelp)
73 |       "print this help text"
74 |   ]
75 |
76 | export
77 | info : String
78 | info = usageInfo "Hedgehog command line args:\n" descs
79 |
80 | export
81 | applyArgs : List String -> Either (List String) Config
82 | applyArgs args =
83 |   case getOpt Permute descs args of
84 |     MkResult opts _ _ [] => foldl (>>=) (Right init) opts
85 |     MkResult _    _ _ e  => Left e
86 |
87 | export
88 | applyConfig : Config -> Group -> Group
89 | applyConfig (MkConfig _ nt ns c) =
90 |   maybe id adjTests nt . maybe id withShrinks ns . maybe id withConfidence c
91 |
92 |   where
93 |     adjPropTests : NumTest -> Property -> Property
94 |     adjPropTests (Forced x)  = withTests x
95 |     adjPropTests (Relaxed x) = mapTests $ \n => if n > 1 then x else n
96 |
97 |     adjTests : NumTest -> Group -> Group
98 |     adjTests = mapProperty . adjPropTests
99 |