More sArray changes; still not compiling

Data/SBV.hs

@@ -204,7 +204,7 @@ module Data.SBV (
   -- ** Sets
   , RCSet(..), SSet
   -- * Arrays of symbolic values
-  , readArray, writeArray, SArray
+  , readArray, writeArray, SArray, sArray, sArray_, sArrays
 
   -- * Creating symbolic values
   -- ** Single value
@@ -257,7 +257,7 @@ module Data.SBV (
 
   -- * Symbolic Equality and Comparisons
   -- $distinctNote
-  , EqSymbolic(..), OrdSymbolic(..), Equality(..)
+  , EqSymbolic(..), OrdSymbolic(..), Equality(..), distinctExcept
   -- * Conditionals: Mergeable values
   , Mergeable(..), ite, iteLazy
 
@@ -450,6 +450,7 @@ import Data.SBV.Core.Model      hiding (assertWithPenalty, minimize, maximize,
                                         sWord8, sWord8_, sWord8s, sWord16, sWord16_, sWord16s,
                                         sWord32, sWord32_, sWord32s, sWord64, sWord64_, sWord64s,
                                         sMaybe, sMaybe_, sMaybes, sEither, sEither_, sEithers, sSet, sSet_, sSets,
+                                        sArray, sArray_, sArrays,
                                         sBarrelRotateLeft, sBarrelRotateRight, zeroExtend, signExtend, sObserve)
 
 import qualified Data.SBV.Core.Model as M  (sBarrelRotateLeft, sBarrelRotateRight, zeroExtend, signExtend)

Data/SBV/Client/BaseIO.hs

@@ -28,8 +28,8 @@ import Data.SBV.Core.Data      (Kind, Outputtable, Penalty,
                                 SymVal, SBool, SBV, SChar, SDouble, SFloat, SWord, SInt,
                                 SFPHalf, SFPBFloat, SFPSingle, SFPDouble, SFPQuad, SFloatingPoint,
                                 SInt8, SInt16, SInt32, SInt64, SInteger, SList,
-                                SReal, SString, SV, SWord8, SWord16, SWord32,
-                                SWord64, SEither, SRational, SMaybe, SSet, constrain, (.==))
+                                SReal, SString, SV, SWord8, SWord16, SWord32, Lambda,
+                                SWord64, SEither, SRational, SMaybe, SSet, SArray, constrain, (.==))
 import Data.SBV.Core.Sized     (IntN, WordN)
 import Data.SBV.Core.Kind      (BVIsNonZero, ValidFloat)
 import Data.SBV.Core.Model     (Metric(..), SymTuple)
@@ -809,6 +809,24 @@ sSet_ = Trans.sSet_
 sSets :: (Ord a, SymVal a) => [String] -> Symbolic [SSet a]
 sSets = Trans.sSets
 
+-- | Declare a named 'SArray'
+--
+-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sArray'
+sArray :: (SymVal a, SymVal b, Lambda Symbolic (a -> b)) => String -> Symbolic (SArray a b)
+sArray = Trans.sArray
+
+-- | Declare an unnamed 'SArray'
+--
+-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sArray_'
+sArray_ :: (SymVal a, SymVal b, Lambda Symbolic (a -> b)) => Symbolic (SArray a b)
+sArray_ = Trans.sArray_
+
+-- | Declare a list of 'SArray' values.
+--
+-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sArrays'
+sArrays :: (SymVal a, SymVal b, Lambda Symbolic (a -> b)) => [String] -> Symbolic [SArray a b]
+sArrays = Trans.sArrays
+
 -- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing
 -- problems with constraints, like the following:
 --

Data/SBV/Core/Data.hs

@@ -700,11 +700,6 @@ class EqSymbolic a where
   -- | Returns (symbolic) 'sTrue' if all the elements of the given list are different.
   distinct :: [a] -> SBool
 
-  -- | Returns (symbolic) `sTrue` if all the elements of the given list are different. The second
-  -- list contains exceptions, i.e., if an element belongs to that set, it will be considered
-  -- distinct regardless of repetition.
-  distinctExcept :: [a] -> [a] -> SBool
-
   -- | Returns (symbolic) 'sTrue' if all the elements of the given list are the same.
   allEqual :: [a] -> SBool
 
@@ -733,15 +728,6 @@ class EqSymbolic a where
   default (.==) :: (G.Generic a, GEqSymbolic (G.Rep a)) => a -> a -> SBool
   (.==) = symbolicEqDefault
 
-  -- Default implementation of 'distinctExcept'. Note that we override
-  -- this method for the base types to generate better code.
-  distinctExcept es ignored = go es
-    where isIgnored = (`sElem` ignored)
-
-          go []     = sTrue
-          go (x:xs) = let xOK  = isIgnored x .|| sAll (\y -> isIgnored y .|| x ./= y) xs
-                      in xOK .&& go xs
-
 -- | Default implementation of symbolic equality, when the underlying type is generic
 -- Not exported, used with automatic deriving.
 symbolicEqDefault :: (G.Generic a, GEqSymbolic (G.Rep a)) => a -> a -> SBool

Data/SBV/Core/Model.hs

@@ -35,7 +35,7 @@ module Data.SBV.Core.Model (
   , sWord64, sWord64_, sWord64s, sInt8, sInt8_, sInt8s, sInt16, sInt16_, sInt16s, sInt32, sInt32_, sInt32s, sInt64, sInt64_
   , sInt64s, sInteger, sInteger_, sIntegers, sReal, sReal_, sReals, sFloat, sFloat_, sFloats, sDouble, sDouble_, sDoubles
   , sWord, sWord_, sWords, sInt, sInt_, sInts
-  , sFPHalf, sFPHalf_, sFPHalfs, sFPBFloat, sFPBFloat_, sFPBFloats, sFPSingle, sFPSingle_, sFPSingles, sFPDouble, sFPDouble_, sFPDoubles, sFPQuad, sFPQuad_, sFPQuads
+  , sFPHalf, sFPHalf_, sFPHalfs, sFPBFloat, sFPBFloat_, sFPBFloats, sFPSingle, sFPSingle_, sFPSingles, sFPDouble, sFPDouble_, sFPDoubles, sFPQuad, sFPQuad_, sFPQuads, sArray, sArray_, sArrays
   , sFloatingPoint, sFloatingPoint_, sFloatingPoints
   , sChar, sChar_, sChars, sString, sString_, sStrings, sList, sList_, sLists
   , sRational, sRational_, sRationals
@@ -52,6 +52,7 @@ module Data.SBV.Core.Model (
   , genLiteral, genFromCV, genMkSymVar
   , zeroExtend, signExtend
   , sbvQuickCheck
+  , distinctExcept
   , readArray, writeArray
   )
   where
@@ -698,6 +699,18 @@ sList_ = free_
 sLists :: (SymVal a, MonadSymbolic m) => [String] -> m [SList a]
 sLists = symbolics
 
+-- | Generalization of 'Data.SBV.sAray'
+sArray :: (SymVal a, SymVal b, Lambda Symbolic (a -> b), MonadSymbolic m) => String -> m (SArray a b)
+sArray = symbolic
+
+-- | Generalization of 'Data.SBV.sList_'
+sArray_ :: (SymVal a, SymVal b, Lambda Symbolic (a -> b), MonadSymbolic m) => m (SArray a b)
+sArray_ = free_
+
+-- | Generalization of 'Data.SBV.sLists'
+sArrays :: (SymVal a, SymVal b, Lambda Symbolic (a -> b), MonadSymbolic m) => [String] -> m [SArray a b]
+sArrays = symbolics
+
 -- | Identify tuple like things. Note that there are no methods, just instances to control type inference
 class SymTuple a
 instance SymTuple ()
@@ -908,36 +921,34 @@ instance EqSymbolic (SBV a) where
           isBool (SBV (SVal KBool _)) = True
           isBool _                    = False
 
-  -- Custom version of distinctExcept that generates better code for base types with equality
-  -- We essentially keep track of an array and count cardinalities as we walk along.
-  distinctExcept :: (Eq a, HasKind a, SymVal a, Lambda Symbolic (a -> Integer)) => [SBV a] -> [SBV a] -> SBool
-  distinctExcept []            _       = sTrue
-  distinctExcept [_]           _       = sTrue
-  distinctExcept es@(firstE:_) ignored
-    | all isConc (es ++ ignored)
-    = distinct (filter ignoreConc es)
-    | True
-    = SBV (SVal KBool (Right (cache r)))
-    where ignoreConc x = case x `sElem` ignored of
-                           SBV (SVal KBool (Left cv)) -> cvToBool cv
-                           _                          -> error $ "distinctExcept: Impossible happened, concrete sElem failed: " ++ show (es, ignored, x)
-
-          ek = case firstE of
-                 SBV (SVal k _) -> k
+-- | Returns (symbolic) `sTrue` if all the elements of the given list are different. The second
+-- list contains exceptions, i.e., if an element belongs to that set, it will be considered
+-- distinct regardless of repetition.
+distinctExcept :: forall a. (Eq a, SymVal a, Lambda Symbolic (a -> Integer)) => [SBV a] -> [SBV a] -> SBool
+distinctExcept []  _       = sTrue
+distinctExcept [_] _       = sTrue
+distinctExcept es  ignored
+  | all isConc (es ++ ignored)
+  = distinct (filter ignoreConc es)
+  | True
+  = SBV (SVal KBool (Right (cache r)))
+  where ignoreConc x = case x `sElem` ignored of
+                         SBV (SVal KBool (Left cv)) -> cvToBool cv
+                         _                          -> error $ "distinctExcept: Impossible happened, concrete sElem failed: " ++ show (es, ignored, x)
 
-          r st = do let incr x table = ite (x `sElem` ignored) (0 :: SInteger) (1 + readArray table x)
+        r st = do let incr x table = ite (x `sElem` ignored) (0 :: SInteger) (1 + readArray table x)
 
-                        initArray :: SArray a Integer
-                        initArray = literal $ const 0
+                      initArray :: SArray a Integer
+                      initArray = literal $ const 0
 
-                        finalArray = foldl (\table x -> writeArray table x (incr x table)) initArray es
+                      finalArray = foldl (\table x -> writeArray table x (incr x table)) initArray es
 
-                    sbvToSV st $ sAll (\e -> readArray finalArray e .<= (1 :: SInteger)) es
+                  sbvToSV st $ sAll (\e -> readArray finalArray e .<= (1 :: SInteger)) es
 
-          -- Sigh, we can't use isConcrete since that requires SymVal
-          -- constraint that we don't have here. (To support SBools.)
-          isConc (SBV (SVal _ (Left _))) = True
-          isConc _                       = False
+        -- Sigh, we can't use isConcrete since that requires SymVal
+        -- constraint that we don't have here. (To support SBools.)
+        isConc (SBV (SVal _ (Left _))) = True
+        isConc _                       = False
 
 -- | If comparison is over something SMTLib can handle, just translate it. Otherwise desugar.
 instance (Ord a, SymVal a) => OrdSymbolic (SBV a) where

Data/SBV/Trans.hs

@@ -43,10 +43,10 @@ module Data.SBV.Trans (
 
   -- * Creating symbolic values
   -- ** Single value
-  , sBool, sWord8, sWord16, sWord32, sWord64, sWord, sInt8, sInt16, sInt32, sInt64, sInt, sInteger, sReal, sFloat, sDouble, sChar, sString, sList
+  , sBool, sWord8, sWord16, sWord32, sWord64, sWord, sInt8, sInt16, sInt32, sInt64, sInt, sInteger, sReal, sFloat, sDouble, sChar, sString, sList, sArray
 
   -- ** List of values
-  , sBools, sWord8s, sWord16s, sWord32s, sWord64s, sWords, sInt8s, sInt16s, sInt32s, sInt64s, sInts, sIntegers, sReals, sFloats, sDoubles, sChars, sStrings, sLists
+  , sBools, sWord8s, sWord16s, sWord32s, sWord64s, sWords, sInt8s, sInt16s, sInt32s, sInt64s, sInts, sIntegers, sReals, sFloats, sDoubles, sChars, sStrings, sLists, sArrays
 
   -- * Symbolic Equality and Comparisons
   , EqSymbolic(..), OrdSymbolic(..), Equality(..)

Documentation/SBV/Examples/Misc/LambdaArray.hs

@@ -29,8 +29,7 @@ memset mem lo hi newVal = literal update
 -- Q.E.D.
 memsetExample :: IO ThmResult
 memsetExample = prove $ do
-   mem  <- newArray "mem" Nothing
-
+   mem  <- sArray   "mem"
    lo   <- sInteger "lo"
    hi   <- sInteger "hi"
    zero <- sInteger "zero"