Simplify and clean-up

Documentation/SBV/Examples/ProofTools/BMC.hs

@@ -18,7 +18,6 @@
 -- What if @y@ starts at @11@?
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -36,7 +35,6 @@ import Data.SBV.Control
 
 -- | System state, containing the two integers.
 data S a = S { x :: a, y :: a }
-         deriving (Functor, Foldable, Traversable)
 
 -- | Show the state as a pair
 instance Show a => Show (S a) where
@@ -50,9 +48,9 @@ instance EqSymbolic a => EqSymbolic (S a) where
 instance Queriable IO (S SInteger) where
   type QueryResult (S SInteger) = S Integer
 
-  create  = S <$> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create          = S <$> freshVar_ <*> freshVar_
+  project S{x, y} = getValue x >>= \vx -> getValue y >>= \vy -> pure S{x = vx, y = vy}
+  embed   S{x, y} = pure S{x = literal x, y = literal y}
 
 -- * Encoding the problem
 

Documentation/SBV/Examples/ProofTools/Fibonacci.hs

@@ -22,9 +22,6 @@
 -- uninterpreted function.
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE DeriveAnyClass        #-}
-{-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -38,22 +35,19 @@ import Data.SBV
 import Data.SBV.Tools.Induction
 import Data.SBV.Control
 
-import GHC.Generics hiding (S)
-
 -- * System state
 
 -- | System state. We simply have two components, parameterized
 -- over the type so we can put in both concrete and symbolic values.
-data S a = S { i :: a, k :: a, m :: a, n :: a }
-         deriving (Show, Mergeable, Generic, Functor, Foldable, Traversable)
+data S a = S { i :: a, k :: a, m :: a, n :: a } deriving Show
 
 -- | 'Queriable instance for our state
 instance Queriable IO (S SInteger) where
   type QueryResult (S SInteger) = S Integer
 
-  create  = S <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create                = S <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_
+  project S{i, k, m, n} = getValue i >>= \vi -> getValue k >>= \vk -> getValue m >>= \vm -> getValue n >>= \vn -> pure S{i = vi, k = vk, m = vm, n = vn}
+  embed   S{i, k, m, n} = pure S{i = literal i, k = literal k, m = literal m, n = literal n}
 
 -- | Encoding partial correctness of the sum algorithm. We have:
 --

Documentation/SBV/Examples/ProofTools/Strengthen.hs

@@ -29,7 +29,6 @@
 -- in Bradley's paper quite closely.
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -47,16 +46,15 @@ import Data.SBV.Control
 
 -- | System state. We simply have two components, parameterized
 -- over the type so we can put in both concrete and symbolic values.
-data S a = S { x :: a, y :: a }
-         deriving (Show, Functor, Foldable, Traversable)
+data S a = S { x :: a, y :: a } deriving Show
 
 -- | 'Queriable instance for our state
 instance Queriable IO (S SInteger) where
   type QueryResult (S SInteger) = S Integer
 
-  create  = S <$> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create          = S <$> freshVar_ <*> freshVar_
+  project S{x, y} = getValue x >>= \vx -> getValue y >>= \vy -> pure S{x = vx, y = vy}
+  embed   S{x, y} = pure S{x = literal x, y = literal y}
 
 -- * Encoding the problem
 

Documentation/SBV/Examples/ProofTools/Sum.hs

@@ -21,9 +21,6 @@
 -- @s@ is the sum of all numbers up to and including @n@ upon termination.
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE DeriveAnyClass        #-}
-{-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -37,21 +34,19 @@ import Data.SBV
 import Data.SBV.Tools.Induction
 import Data.SBV.Control
 
-import GHC.Generics hiding (S)
-
 -- * System state
 
 -- | System state. We simply have two components, parameterized
 -- over the type so we can put in both concrete and symbolic values.
-data S a = S { s :: a, i :: a, n :: a } deriving (Show, Mergeable, Generic, Functor, Foldable, Traversable)
+data S a = S { s :: a, i :: a, n :: a } deriving Show
 
 -- | 'Queriable instance for our state
 instance Queriable IO (S SInteger) where
   type QueryResult (S SInteger) = S Integer
 
-  create  = S <$> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create             = S <$> freshVar_ <*> freshVar_ <*> freshVar_
+  project S{s, i, n} = getValue s >>= \vs -> getValue i >>= \vi -> getValue n >>= \vn -> pure S{s = vs, i = vi, n = vn}
+  embed   S{s, i, n} = pure S{s = literal s, i = literal i, n = literal n}
 
 -- | Encoding partial correctness of the sum algorithm. We have:
 --

Documentation/SBV/Examples/Puzzles/DieHard.hs

@@ -13,7 +13,6 @@
 
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveDataTypeable    #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -61,15 +60,15 @@ instance Queriable IO SState where
   project State{big, small, action} = do b <- getValue big
                                          s <- getValue small
                                          a <- getValue action
-                                         pure $ State { big    = b
-                                                      , small  = s
-                                                      , action = a
-                                                      }
-
-  embed State{big, small, action} = pure $ State { big    = literal big
-                                                 , small  = literal small
-                                                 , action = literal action
-                                                 }
+                                         pure State{ big    = b
+                                                   , small  = s
+                                                   , action = a
+                                                   }
+
+  embed State{big, small, action} = pure State{ big    = literal big
+                                              , small  = literal small
+                                              , action = literal action
+                                              }
 
 -- | Solve the problem using a BMC search. We have:
 --

Documentation/SBV/Examples/WeakestPreconditions/Append.hs

@@ -39,36 +39,27 @@ import GHC.Generics (Generic)
 -- * Program state
 
 -- | The state of the length program, paramaterized over the element type @a@
-data AppS a = AppS { xs :: SList a  -- ^ The first input list
-                   , ys :: SList a  -- ^ The second input list
-                   , ts :: SList a  -- ^ Temporary variable
-                   , zs :: SList a  -- ^ Output
+data AppS a = AppS { xs :: a  -- ^ The first input list
+                   , ys :: a  -- ^ The second input list
+                   , ts :: a  -- ^ Temporary variable
+                   , zs :: a  -- ^ Output
                    }
                    deriving (Generic, Mergeable)
 
--- | The concrete counterpart of 'AppS'. Again, we can't simply use the duality between
--- @SBV a@ and @a@ due to the difference between @SList a@ and @[a]@.
-data AppC a = AppC [a] [a] [a] [a]
-
--- | Show instance for 'AppS'. The above deriving clause would work just as well,
--- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
-instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (AppS a) where
-  show (AppS xs ys ts zs) = "{xs = " P.++ sh xs P.++ ", ys = " P.++ sh ys P.++ ", ts = " P.++ sh ts P.++ ", zs = " P.++ sh zs P.++ "}"
-    where sh v = maybe "<symbolic>" show (unliteral v)
-
 -- | Show instance, a bit more prettier than what would be derived:
-instance Show a => Show (AppC a) where
-  show (AppC xs ys ts zs) = "{xs = " P.++ show xs P.++ ", ys = " P.++ show ys P.++ ", ts = " P.++ show ts P.++ ", zs = " P.++ show zs P.++ "}"
+instance Show (f a) => Show (AppS (f a)) where
+  show AppS{xs, ys, ts, zs} = "{xs = " P.++ show xs P.++ ", ys = " P.++ show ys P.++ ", ts = " P.++ show ts P.++ ", zs = " P.++ show zs P.++ "}"
 
 -- | 'Queriable' instance for the program state
-instance Queriable IO (AppS Integer) where
-  type QueryResult (AppS Integer) = AppC Integer
-  create                     = AppS <$> freshVar_   <*> freshVar_   <*> freshVar_   <*> freshVar_
-  project (AppS xs ys ts zs) = AppC <$> getValue xs <*> getValue ys <*> getValue ts <*> getValue zs
-  embed   (AppC xs ys ts zs) = return $ AppS (literal xs) (literal ys) (literal ts) (literal zs)
+instance Queriable IO (AppS (SList Integer)) where
+  type QueryResult (AppS (SList Integer)) = AppS [Integer]
+
+  create                       = AppS <$> freshVar_  <*> freshVar_  <*> freshVar_  <*> freshVar_
+  project AppS{xs, ys, ts, zs} = getValue xs >>= \vxs -> getValue ys >>= \vxy -> getValue ts >>= \vts -> getValue zs >>= \vzs -> pure AppS{xs = vxs, ys = vxy, ts = vts, zs = vzs}
+  embed   AppS{xs, ys, ts, zs} = pure AppS{xs = literal xs, ys = literal ys, ts = literal ts, zs = literal zs}
 
 -- | Helper type synonym
-type A = AppS Integer
+type A = AppS (SList Integer)
 
 -- * The algorithm
 
@@ -122,5 +113,5 @@ imperativeAppend = Program { setup         = return ()
 -- >>> correctness
 -- Total correctness is established.
 -- Q.E.D.
-correctness :: IO (ProofResult (AppC Integer))
+correctness :: IO (ProofResult (AppS [Integer]))
 correctness = wpProveWith defaultWPCfg{wpVerbose=True} imperativeAppend

Documentation/SBV/Examples/WeakestPreconditions/Basics.hs

@@ -14,7 +14,6 @@
 {-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -45,7 +44,7 @@ import GHC.Generics (Generic)
 data IncS a = IncS { x :: a    -- ^ Input value
                    , y :: a    -- ^ Output
                    }
-                   deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable)
+                   deriving (Show, Generic, Mergeable)
 
 -- | Show instance for 'IncS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
@@ -57,9 +56,9 @@ instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (IncS (SBV a)) where
 instance Queriable IO (IncS SInteger) where
   type QueryResult (IncS SInteger) = IncS Integer
 
-  create  = IncS <$> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create             = IncS <$> freshVar_ <*> freshVar_
+  project IncS{x, y} = getValue x >>= \vx -> getValue y >>= \vy -> pure IncS{x = vx, y = vy}
+  embed   IncS{x, y} = pure IncS{x = literal x, y = literal y}
 
 -- | Helper type synonym
 type I = IncS SInteger

Documentation/SBV/Examples/WeakestPreconditions/Fib.hs

@@ -15,7 +15,6 @@
 {-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -48,7 +47,7 @@ data FibS a = FibS { n :: a    -- ^ The input value
                    , k :: a    -- ^ tracks @fib (i+1)@
                    , m :: a    -- ^ tracks @fib i@
                    }
-                   deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable)
+                   deriving (Show, Generic, Mergeable)
 
 -- | Show instance for 'FibS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
@@ -60,9 +59,9 @@ instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (FibS (SBV a)) where
 instance Queriable IO (FibS SInteger) where
   type QueryResult (FibS SInteger) = FibS Integer
 
-  create  = FibS <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create                   = FibS <$> freshVar_  <*> freshVar_ <*> freshVar_ <*> freshVar_
+  project FibS{n, i, k, m} = getValue n >>= \vn -> getValue i >>= \vi -> getValue k >>= \vk -> getValue m >>= \vm -> pure FibS{n = vn, i = vi, k = vk, m = vm}
+  embed   FibS{n, i, k, m} = pure FibS{n = literal n, i = literal i, k = literal k, m = literal m}
 
 -- | Helper type synonym
 type F = FibS SInteger

Documentation/SBV/Examples/WeakestPreconditions/GCD.hs

@@ -17,7 +17,6 @@
 {-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -54,7 +53,7 @@ data GCDS a = GCDS { x :: a    -- ^ First value
                    , i :: a    -- ^ Copy of x to be modified
                    , j :: a    -- ^ Copy of y to be modified
                    }
-                   deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable)
+                   deriving (Show, Generic, Mergeable)
 
 -- | Show instance for 'GCDS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
@@ -66,9 +65,9 @@ instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (GCDS (SBV a)) where
 instance Queriable IO (GCDS SInteger) where
   type QueryResult (GCDS SInteger) = GCDS Integer
 
-  create  = GCDS <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create                   = GCDS <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_
+  project GCDS{x, y, i, j} = getValue x >>= \vx -> getValue y >>= \vy -> getValue i >>= \vi -> getValue j >>= \vj -> pure GCDS{x = vx, y = vy, i = vi, j = vj}
+  embed   GCDS{x, y, i, j} = pure GCDS{x = literal x, y = literal y, i = literal i, j = literal j}
 
 -- | Helper type synonym
 type G = GCDS SInteger

Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs

@@ -13,7 +13,6 @@
 
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -38,7 +37,7 @@ data DivS a = DivS { x :: a   -- ^ The dividend
                    , q :: a   -- ^ The quotient
                    , r :: a   -- ^ The remainder
                    }
-                   deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable)
+                   deriving (Show, Generic, Mergeable)
 
 -- | Show instance for 'DivS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
@@ -50,9 +49,9 @@ instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (DivS (SBV a)) where
 instance SymVal a => Queriable IO (DivS (SBV a)) where
   type QueryResult (DivS (SBV a)) = DivS a
 
-  create  = DivS <$> freshVar_  <*> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create                   = DivS <$> freshVar_  <*> freshVar_ <*> freshVar_ <*> freshVar_
+  project DivS{x, y, q, r} = getValue x >>= \vx -> getValue y >>= \vy -> getValue q >>= \vq -> getValue r >>= \vr -> pure DivS{x = vx, y = vy, q = vq, r = vr}
+  embed   DivS{x, y, q, r} = pure DivS{x = literal x, y = literal y, q = literal q, r = literal r}
 
 -- | Helper type synonym
 type D = DivS SInteger

Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs

@@ -15,7 +15,6 @@
 
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -42,7 +41,7 @@ data SqrtS a = SqrtS { x    :: a   -- ^ The input
                      , i    :: a   -- ^ Successive squares, as the sum of j's
                      , j    :: a   -- ^ Successive odds
                      }
-                     deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable)
+                     deriving (Show, Generic, Mergeable)
 
 -- | Show instance for 'SqrtS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
@@ -54,9 +53,9 @@ instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (SqrtS (SBV a)) where
 instance SymVal a => Queriable IO (SqrtS (SBV a)) where
   type QueryResult (SqrtS (SBV a)) = SqrtS a
 
-  create  = SqrtS <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create                       = SqrtS <$> freshVar_  <*> freshVar_ <*> freshVar_ <*> freshVar_
+  project SqrtS{x, sqrt, i, j} = getValue x >>= \vx -> getValue sqrt >>= \vsqrt -> getValue i >>= \vi -> getValue j >>= \vj -> pure SqrtS{x = vx, sqrt = vsqrt, i = vi, j = vj}
+  embed   SqrtS{x, sqrt, i, j} = pure SqrtS{x = literal x, sqrt = literal sqrt, i = literal i, j = literal j}
 
 -- | Helper type synonym
 type S = SqrtS SInteger