Further progress. WIP.

Data/SBV/Client/BaseIO.hs

@@ -812,19 +812,19 @@ 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 :: (SymVal a, SymVal 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_ :: (SymVal a, SymVal 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 :: (SymVal a, SymVal b) => [String] -> Symbolic [SArray a b]
 sArrays = Trans.sArrays
 
 -- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing

Data/SBV/Compilers/C.hs

@@ -760,8 +760,8 @@ ppExpr cfg consts (SBVApp op opArgs) lhs (typ, var)
         hd w []    = error $ "Data.SBV.C.ppExpr: Impossible happened: " ++ w ++ ", received empty list!"
 
         p :: Op -> [Doc] -> Doc
-        p (ArrRead _)       _  = tbd "User specified arrays (ArrRead)"
-        p (ArrEq _ _)       _  = tbd "User specified arrays (ArrEq)"
+        p ReadArray{}       _  = tbd "User specified arrays (ReadArray)"
+        p WriteArray{}      _  = tbd "User specified arrays (WriteArray)"
         p (Label s)        [a] = a <+> text "/*" <+> text s <+> text "*/"
         p (IEEEFP w)         as = handleIEEE w  consts (zip opArgs as) var
         p (PseudoBoolean pb) as = handlePB pb as

Data/SBV/Core/Data.hs

@@ -49,7 +49,7 @@ module Data.SBV.Core.Data
  , SBV(..), NodeId(..), mkSymSBV
  , sbvToSV, sbvToSymSV, forceSVArg
  , SBVExpr(..), newExpr
- , cache, Cached, uncache, uncacheAI, HasKind(..)
+ , cache, Cached, uncache, HasKind(..)
  , Op(..), PBOp(..), FPOp(..), StrOp(..), RegExOp(..), SeqOp(..), RegExp(..), NamedSymVar(..), OvOp(..), getTableIndex
  , SBVPgm(..), Symbolic, runSymbolic, State, getPathCondition, extendPathCondition
  , inSMTMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..)

Data/SBV/Core/Model.hs

@@ -322,13 +322,13 @@ instance SymVal a => SymVal (Maybe a) where
   fromCV (CV (KMaybe k) (CMaybe (Just x))) = Just $ fromCV $ CV k x
   fromCV bad                               = error $ "SymVal.fromCV (Maybe): Malformed sum received: " ++ show bad
 
-instance (HasKind a, HasKind b, SymVal a, SymVal b, Lambda Symbolic (a -> b)) => SymVal (a -> b) where
+instance (HasKind a, HasKind b, SymVal a, SymVal b) => SymVal (a -> b) where
    mkSymVal = genMkSymVar (kindOf (Proxy @(a -> b)))
 
    literal f = SBV . SVal k . Right $ cache g
        where k = KArray (kindOf (Proxy @a)) (kindOf (Proxy @b))
 
-             g st = do def <- lambdaStr st (kindOf (Proxy @b)) f
+             g st = do def <- lambdaStr st (kindOf (Proxy @(SBV b))) f
                        newExpr st k (SBVApp (ArrayLambda def) [])
 
    fromCV (CV _ (CArray f)) i = fromCV $ CV (kindOf (Proxy @b)) (f (toCV i))
@@ -700,15 +700,15 @@ 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 :: (SymVal a, SymVal 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_ :: (SymVal a, SymVal 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 :: (SymVal a, SymVal 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
@@ -924,7 +924,7 @@ instance EqSymbolic (SBV a) where
 -- | 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 :: forall a. (Eq a, SymVal a) => [SBV a] -> [SBV a] -> SBool
 distinctExcept []  _       = sTrue
 distinctExcept [_] _       = sTrue
 distinctExcept es  ignored
@@ -3221,7 +3221,7 @@ instance {-# OVERLAPPABLE #-} (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e,
   k === l = prove $ \a b c d e f g -> k (a, b, c, d, e, f, g) .== l (a, b, c, d, e, f, g)
 
 -- | Reading a value from an array
-readArray :: forall key val. (SymVal key, SymVal val, HasKind val, Lambda Symbolic (key -> val)) => SArray key val -> SBV key -> SBV val
+readArray :: forall key val. (SymVal key, SymVal val, HasKind val) => SArray key val -> SBV key -> SBV val
 readArray array key
    | Just f <- unliteral array, Just k <- unliteral key
    = literal (f k)
@@ -3233,7 +3233,7 @@ readArray array key
                    newExpr st kb (SBVApp ReadArray [f, k])
 
 -- | Writing a value to an array
-writeArray :: forall key val. (Eq key, HasKind key, SymVal key, SymVal val, HasKind val, Lambda Symbolic (key -> val)) => SArray key val -> SBV key -> SBV val -> SArray key val
+writeArray :: forall key val. (Eq key, HasKind key, SymVal key, SymVal val, HasKind val) => SArray key val -> SBV key -> SBV val -> SArray key val
 writeArray array key value
    | Just f <- unliteral array, Just keyVal <- unliteral key, Just val <- unliteral value
    = literal (\k' -> if k' == keyVal then val else f k')

Data/SBV/Core/Symbolic.hs

@@ -47,7 +47,6 @@ module Data.SBV.Core.Symbolic
   , svToSV, svToSymSV, forceSVArg
   , SBVExpr(..), newExpr, isCodeGenMode, isSafetyCheckingIStage, isRunIStage, isSetupIStage
   , Cached, cache, uncache, modifyState, modifyIncState
-  , ArrayIndex(..), uncacheAI
   , NamedSymVar(..), Name, UserInputs, Inputs(..), getSV, swNodeId, namedNodeId
   , addInternInput, addUserInput
   , getUserName', getUserName
@@ -232,8 +231,6 @@ data Op = Plus
         | ZeroExtend Int
         | SignExtend Int
         | LkUp (Int, Kind, Kind, Int) !SV !SV   -- (table-index, arg-type, res-type, length of the table) index out-of-bounds-value
-        | ArrEq   ArrayIndex ArrayIndex         -- Array equality
-        | ArrRead ArrayIndex
         | KindCast Kind Kind
         | Uninterpreted String
         | QuantifiedBool [Op] String            -- When we generate a forall/exists (nested etc.) boolean value
@@ -604,9 +601,6 @@ instance Show Op where
         = "lookup(" ++ tinfo ++ ", " ++ show i ++ ", " ++ show e ++ ")"
         where tinfo = "table" ++ show ti ++ "(" ++ show at ++ " -> " ++ show rt ++ ", " ++ show l ++ ")"
 
-  show (ArrEq i j)          = "array_" ++ show i ++ " == array_" ++ show j
-  show (ArrRead i)          = "select array_" ++ show i
-
   show (KindCast fr to)     = "cast_" ++ show fr ++ "_" ++ show to
   show (Uninterpreted i)    = "[uninterpreted] " ++ i
   show (QuantifiedBool _ i) = "[quantified boolean] " ++ i
@@ -1235,7 +1229,6 @@ data State  = State { sbvContext          :: SBVContext
                     , rAsserts            :: IORef [(String, Maybe CallStack, SV)]
                     , rOutstandingAsserts :: IORef Bool            -- Did we send an assert after the last check-sat call?
                     , rSVCache            :: IORef (Cache SV)
-                    , rAICache            :: IORef (Cache ArrayIndex)
                     , rQueryState         :: IORef (Maybe QueryState)
                     , parentState         :: Maybe State  -- Pointer to our parent if we're in a sublevel
                     }
@@ -1856,7 +1849,6 @@ mkNewState cfg currentRunMode = liftIO $ do
      cgs                <- newIORef Map.empty
      defns              <- newIORef []
      swCache            <- newIORef IMap.empty
-     aiCache            <- newIORef IMap.empty
      usedKinds          <- newIORef Set.empty
      usedLbls           <- newIORef Set.empty
      cstrs              <- newIORef S.empty
@@ -1893,7 +1885,6 @@ mkNewState cfg currentRunMode = liftIO $ do
                   , rCgMap              = cgs
                   , rDefns              = defns
                   , rSVCache            = swCache
-                  , rAICache            = aiCache
                   , rConstraints        = cstrs
                   , rPartitionVars      = pvs
                   , rSMTOptions         = smtOpts
@@ -2122,20 +2113,6 @@ cache = Cached
 uncache :: Cached SV -> State -> IO SV
 uncache = uncacheGen rSVCache
 
--- | An SMT array index is simply an int value, and the context this array was created in
-data ArrayIndex = ArrayIndex { unArrayIndex   :: Int
-                             , unArrayContext :: SBVContext
-                             }
-               deriving (Eq, Ord, G.Data, NFData, Generic)
-
--- | We simply show indexes as the underlying integer
-instance Show ArrayIndex where
-  show = show . unArrayIndex
-
--- | Uncache, retrieving SMT array indexes
-uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex
-uncacheAI = uncacheGen rAICache
-
 -- | Generic uncaching. Note that this is entirely safe, since we do it in the IO monad.
 uncacheGen :: (State -> IORef (Cache a)) -> Cached a -> State -> IO a
 uncacheGen getCache (Cached f) st = do

Data/SBV/Lambda.hs

@@ -98,7 +98,6 @@ inSubState inState comp = do
                    , rctr                = fresh rctr
                    , rLambdaLevel        = fresh rLambdaLevel
                    , rtblMap             = fresh rtblMap
-                   , rAICache            = fresh rAICache
                    , rinps               = fresh rinps
                    , rlambdaInps         = fresh rlambdaInps
                    , rConstraints        = fresh rConstraints

Data/SBV/SMT/SMTLib2.hs

@@ -884,8 +884,8 @@ cvtExp curProgInfo caps rm tableMap expr@(SBVApp _ arguments) = sh expr
 
         sh (SBVApp (KindCast f t) [a]) = handleKindCast hasInt2bv f t (cvtSV a)
 
-        sh (SBVApp (ArrEq i j) [])  = "(= array_" ++ show i ++ " array_" ++ show j ++")"
-        sh (SBVApp (ArrRead i) [a]) = "(select array_" ++ show i ++ " " ++ cvtSV a ++ ")"
+        sh (SBVApp ReadArray  [a, i])    = "(select " ++ cvtSV a ++ " " ++ cvtSV i ++ ")"
+        sh (SBVApp WriteArray [a, i, v]) = "(store "  ++ cvtSV a ++ " " ++ cvtSV i ++ " " ++ cvtSV v ++ ")"
 
         sh (SBVApp (Uninterpreted nm) [])   = nm
         sh (SBVApp (Uninterpreted nm) args) = "(" ++ nm ++ " " ++ unwords (map cvtSV args) ++ ")"

Documentation/SBV/Examples/Misc/LambdaArray.hs

@@ -52,8 +52,7 @@ memsetExample = prove $ do
 --   idx  = 1 :: Integer
 outOfInit :: IO SatResult
 outOfInit = sat $ do
-   mem  <- newArray "mem" Nothing
-
+   mem  <- sArray "mem"
    lo   <- sInteger "lo"
    hi   <- sInteger "hi"
    zero <- sInteger "zero"