Skip to content

Commit aaed3e5

Browse files
RyanGlScottRyanGlScott
committed
Factor out verifier-specific options into their own data type
Currently, there is only one verifier-specific option, the `Verbosity`. However, implementing a fix for #20 will require yet another option, so this patch will make it simpler to add another option when the time comes.
1 parent 6c6d652 commit aaed3e5

File tree

13 files changed

+71
-30
lines changed

13 files changed

+71
-30
lines changed

‎copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/UnderConstrained.hs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@ module Copilot.Verifier.Examples.ShouldFail.UnderConstrained where
66

77
import Language.Copilot
88
import Copilot.Compile.C99
9-
import Copilot.Verifier (Verbosity, verifyWithVerbosity)
9+
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
10+
, defaultVerifierOptions, verifyWithOptions )
1011

1112
spec :: Spec
1213
spec = do
@@ -19,7 +20,8 @@ spec = do
1920
verifySpec :: Verbosity -> IO ()
2021
verifySpec verb = do
2122
spec' <- reify spec
22-
verifyWithVerbosity verb mkDefaultCSettings
23+
verifyWithOptions defaultVerifierOptions{verbosity = verb}
24+
mkDefaultCSettings
2325
-- ["nonzero"]
2426
[]
2527
"underConstrained" spec'

‎copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,8 @@ import qualified Prelude as P
88

99
import Language.Copilot
1010
import Copilot.Compile.C99
11-
import Copilot.Verifier (Verbosity(..), verifyWithVerbosity)
11+
import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
12+
, defaultVerifierOptions, verifyWithOptions )
1213
import Copilot.Theorem.What4 (prove, Solver(..))
1314

1415
-- The largest unsigned 32-bit prime
@@ -45,6 +46,7 @@ verifySpec verb =
4546
r <- prove Z3 s
4647
when (verb P.== Noisy) $
4748
print r
48-
verifyWithVerbosity verb mkDefaultCSettings ["reduced"] "multRingSpec" s
49+
verifyWithOptions defaultVerifierOptions{verbosity = verb}
50+
mkDefaultCSettings ["reduced"] "multRingSpec" s
4951

5052
--verifySpec _ = interpret 10 engineMonitor

‎copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,8 @@ module Copilot.Verifier.Examples.ShouldPass.Array where
1515

1616
import Language.Copilot
1717
import Copilot.Compile.C99
18-
import Copilot.Verifier (Verbosity, verifyWithVerbosity)
18+
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
19+
, defaultVerifierOptions, verifyWithOptions )
1920

2021
-- Lets define an array of length 2.
2122
-- Make the buffer of the streams 3 elements long.
@@ -34,5 +35,6 @@ spec = do
3435

3536
-- Compile the spec
3637
verifySpec :: Verbosity -> IO ()
37-
verifySpec verb = reify spec >>= verifyWithVerbosity verb mkDefaultCSettings [] "array"
38+
verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
39+
mkDefaultCSettings [] "array"
3840
-- verifySpec _ = interpret 30 spec

‎copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,8 @@ import qualified Prelude as P
1212

1313
import Language.Copilot
1414
import Copilot.Compile.C99
15-
import Copilot.Verifier (Verbosity(..), verifyWithVerbosity)
15+
import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
16+
, defaultVerifierOptions, verifyWithOptions )
1617
import Copilot.Theorem.What4 (prove, Solver(..))
1718

1819
-- | We need to force a type for the argument of `period`.
@@ -41,4 +42,5 @@ verifySpec verb =
4142
r <- prove Z3 s
4243
when (verb P.== Noisy) $
4344
print r
44-
verifyWithVerbosity verb mkDefaultCSettings [] "clock" s
45+
verifyWithOptions defaultVerifierOptions{verbosity = verb}
46+
mkDefaultCSettings [] "clock" s

‎copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ import qualified Prelude as P
1313

1414
import Language.Copilot
1515
import Copilot.Compile.C99
16-
import Copilot.Verifier (Verbosity(..), verifyWithVerbosity)
16+
import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
17+
, defaultVerifierOptions, verifyWithOptions )
1718
import Copilot.Theorem.What4 (prove, Solver(..))
1819

1920
-- A resettable counter
@@ -51,4 +52,5 @@ verifySpec verb =
5152
r <- prove Z3 s
5253
when (verb P.== Noisy) $
5354
print r
54-
verifyWithVerbosity verb mkDefaultCSettings ["range", "range2"] "counter" s
55+
verifyWithOptions defaultVerifierOptions{verbosity = verb}
56+
mkDefaultCSettings ["range", "range2"] "counter" s

‎copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Engine.hs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@ module Copilot.Verifier.Examples.ShouldPass.Engine where
1010

1111
import Language.Copilot
1212
import Copilot.Compile.C99
13-
import Copilot.Verifier (Verbosity, verifyWithVerbosity)
13+
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
14+
, defaultVerifierOptions, verifyWithOptions )
1415

1516
import qualified Prelude as P
1617

@@ -38,5 +39,6 @@ engineMonitor = do
3839
cooler = Just $ [True, True] P.++ repeat False
3940

4041
verifySpec :: Verbosity -> IO ()
41-
verifySpec verb = reify engineMonitor >>= verifyWithVerbosity verb mkDefaultCSettings [] "engine"
42+
verifySpec verb = reify engineMonitor >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
43+
mkDefaultCSettings [] "engine"
4244
--verifySpec _ = interpret 10 engineMonitor

‎copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/FPOps.hs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,8 @@ module Copilot.Verifier.Examples.ShouldPass.FPOps where
55

66
import Copilot.Compile.C99 (mkDefaultCSettings)
77
import qualified Copilot.Language.Stream as Copilot
8-
import Copilot.Verifier (Verbosity, verifyWithVerbosity)
8+
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
9+
, defaultVerifierOptions, verifyWithOptions )
910
import Data.Proxy (Proxy(..))
1011
import Language.Copilot
1112
import qualified Prelude as P
@@ -83,4 +84,5 @@ testOp2 op stream =
8384
verifySpec :: Verbosity -> IO ()
8485
verifySpec verb = do
8586
spec' <- reify spec
86-
verifyWithVerbosity verb mkDefaultCSettings [] "fpOps" spec'
87+
verifyWithOptions defaultVerifierOptions{verbosity = verb}
88+
mkDefaultCSettings [] "fpOps" spec'

‎copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Heater.hs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,8 @@ import Copilot.Compile.C99
1414
--import Copilot.Core.PrettyDot (prettyPrintDot)
1515
--import Copilot.Language.Prelude
1616

17-
import Copilot.Verifier (Verbosity, verifyWithVerbosity)
17+
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
18+
, defaultVerifierOptions, verifyWithOptions )
1819

1920
import Prelude ()
2021

@@ -37,7 +38,8 @@ spec = do
3738

3839
-- Compile the spec
3940
verifySpec :: Verbosity -> IO ()
40-
verifySpec verb = reify spec >>= verifyWithVerbosity verb mkDefaultCSettings [] "heater"
41+
verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
42+
mkDefaultCSettings [] "heater"
4143
{-
4244
do spec' <- reify spec
4345
putStrLn $ prettyPrintDot spec'

‎copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,8 @@
22
module Copilot.Verifier.Examples.ShouldPass.IntOps where
33

44
import Copilot.Compile.C99 (mkDefaultCSettings)
5-
import Copilot.Verifier (Verbosity, verifyWithVerbosity)
5+
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
6+
, defaultVerifierOptions, verifyWithOptions )
67
import Language.Copilot
78
import qualified Prelude as P
89

@@ -59,4 +60,5 @@ testOp2 op stream1 stream2 =
5960
verifySpec :: Verbosity -> IO ()
6061
verifySpec verb = do
6162
spec' <- reify spec
62-
verifyWithVerbosity verb mkDefaultCSettings ["nonzero", "shiftByBits"] "intOps" spec'
63+
verifyWithOptions defaultVerifierOptions{verbosity = verb}
64+
mkDefaultCSettings ["nonzero", "shiftByBits"] "intOps" spec'

‎copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,8 @@ import qualified Prelude as P
1212
import Language.Copilot
1313
import Copilot.Compile.C99
1414
import Copilot.Theorem.What4
15-
import Copilot.Verifier (Verbosity(..), verifyWithVerbosity)
15+
import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
16+
, defaultVerifierOptions, verifyWithOptions )
1617

1718

1819
-- | Definition for `Volts`.
@@ -87,4 +88,5 @@ verifySpec verb = do
8788
Invalid -> putStrLn "invalid"
8889
Unknown -> putStrLn "unknown"
8990

90-
verifyWithVerbosity verb mkDefaultCSettings [] "structs" spec'
91+
verifyWithOptions defaultVerifierOptions{verbosity = verb}
92+
mkDefaultCSettings [] "structs" spec'

0 commit comments

Comments
 (0)