-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Misc.LambdaArray
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates how lambda-abstractions can be used to model arrays.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Misc.LambdaArray where

import Data.SBV

-- | Given an array, and bounds on it, initialize it within the bounds to the element given.
-- Otherwise, leave it untouched.
memset :: SArray Integer Integer -> SInteger -> SInteger -> SInteger -> SArray Integer Integer
memset :: SArray Integer Integer
-> SInteger -> SInteger -> SInteger -> SArray Integer Integer
memset SArray Integer Integer
mem SInteger
lo SInteger
hi SInteger
newVal = (SInteger -> SInteger) -> SArray Integer Integer
forall a b. (SymVal a, HasKind b) => (SBV a -> SBV b) -> SArray a b
lambdaAsArray SInteger -> SInteger
update
  where update :: SInteger -> SInteger
        update :: SInteger -> SInteger
update SInteger
idx = let oldVal :: SInteger
oldVal = SArray Integer Integer -> SInteger -> SInteger
forall a b. SArray a b -> SBV a -> SBV b
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray SArray Integer Integer
mem SInteger
idx
                     in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
idx SBool -> SBool -> SBool
.&& SInteger
idx SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi) SInteger
newVal SInteger
oldVal

-- | Prove a simple property: If we read from the initialized region, we get the initial value. We have:
--
-- >>> memsetExample
-- Q.E.D.
memsetExample :: IO ThmResult
memsetExample :: IO ThmResult
memsetExample = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do
   mem  <- String -> Maybe SInteger -> Symbolic (SArray Integer Integer)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> Symbolic (array a b)
newArray String
"mem" Maybe SInteger
forall a. Maybe a
Nothing

   lo   <- sInteger "lo"
   hi   <- sInteger "hi"
   zero <- sInteger "zero"

   -- Get an index within lo/hi
   idx  <- sInteger "idx"
   constrain $ idx .>= lo .&& idx .<= hi

   -- It must be the case that we get zero back after mem-setting
   pure $ readArray (memset mem lo hi zero) idx .== zero

-- | Get an example of reading a value out of range. The value returned should be out-of-range for lo/hi
--
-- >>> outOfInit
-- Satisfiable. Model:
--   Read = 1 :: Integer
--   lo   = 0 :: Integer
--   hi   = 0 :: Integer
--   zero = 0 :: Integer
--   idx  = 1 :: Integer
outOfInit :: IO SatResult
outOfInit :: IO SatResult
outOfInit = SymbolicT IO () -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat (SymbolicT IO () -> IO SatResult)
-> SymbolicT IO () -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do
   mem  <- String -> Maybe SInteger -> Symbolic (SArray Integer Integer)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> Symbolic (array a b)
newArray String
"mem" Maybe SInteger
forall a. Maybe a
Nothing

   lo   <- sInteger "lo"
   hi   <- sInteger "hi"
   zero <- sInteger "zero"

   -- Get a meaningful range:
   constrain $ lo .<= hi

   -- Get an index
   idx  <- sInteger "idx"

   -- Let read produce non-zero
   constrain $ observe "Read" (readArray (memset mem lo hi zero) idx) ./= zero