-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Misc.Tuple
-- Copyright : (c) Joel Burget
--                 Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A basic tuple use case, also demonstrating regular expressions,
-- strings, etc. This is a basic template for getting SBV to produce
-- valid data for applications that require inputs that satisfy
-- arbitrary criteria.
-----------------------------------------------------------------------------

{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Misc.Tuple where

import Data.SBV
import Data.SBV.Tuple
import Data.SBV.Control

import Prelude hiding ((!!))
import Data.SBV.List   ((!!))
import Data.SBV.RegExp

import qualified Data.SBV.String as S
import qualified Data.SBV.List   as L

-- | A dictionary is a list of lookup values. Note that we
-- store the type @[(a, b)]@ as a symbolic value here, mixing
-- sequences and tuples.
type Dict a b = SBV [(a, b)]

-- | Create a dictionary of length 5, such that each element
-- has an string key and each value is the length of the key.
-- We impose a few more constraints to make the output interesting. 
-- For instance, you might get:
--
-- @ ghci> example
-- [("nt_",3),("dHAk",4),("kzkk0",5),("mZxs9s",6),("c32'dPM",7)]
-- @
--
-- Depending on your version of z3, a different answer might be provided.
-- Here, we check that it satisfies our length conditions:
--
-- >>> import Data.List (genericLength)
-- >>> example >>= \ex -> return (length ex == 5 && all (\(l, i) -> genericLength l == i) ex)
-- True
example :: IO [(String, Integer)]
example :: IO [(String, Integer)]
example = Symbolic [(String, Integer)] -> IO [(String, Integer)]
forall a. Symbolic a -> IO a
runSMT (Symbolic [(String, Integer)] -> IO [(String, Integer)])
-> Symbolic [(String, Integer)] -> IO [(String, Integer)]
forall a b. (a -> b) -> a -> b
$ do Dict String Integer
dict :: Dict String Integer <- String -> Symbolic (Dict String Integer)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"dict"

                      -- require precisely 5 elements
                      let len :: Int
len   = Int
5 :: Int
                          range :: [Int]
range = [Int
0 .. Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

                      SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Dict String Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
L.length Dict String Integer
dict SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Int -> SInteger
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
len

                      -- require each key to be at of length 3 more than the index it occupies
                      -- and look like an identifier
                      let goodKey :: a -> SBV String -> SBool
goodKey a
i SBV String
s = let l :: SInteger
l = SBV String -> SInteger
S.length SBV String
s
                                            r :: RegExp
r = RegExp
asciiLower RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
KStar (RegExp
asciiLetter RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
digit RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"_" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"'")
                                      in SInteger
l SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a -> SInteger
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
iSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
3 SBool -> SBool -> SBool
.&& SBV String
s SBV String -> RegExp -> SBool
forall a. RegExpMatchable a => a -> RegExp -> SBool
`match` RegExp
r

                          restrict :: a -> m ()
restrict a
i = case SBV (String, Integer) -> (SBV String, SInteger)
forall tup a. Tuple tup a => SBV tup -> a
untuple (Dict String Integer
dict Dict String Integer -> SInteger -> SBV (String, Integer)
forall a. SymVal a => SList a -> SInteger -> SBV a
!! a -> SInteger
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
i) of
                                         (SBV String
k, SInteger
v) -> SBool -> m ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ a -> SBV String -> SBool
forall a. Integral a => a -> SBV String -> SBool
goodKey a
i SBV String
k SBool -> SBool -> SBool
.&& SInteger
v SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV String -> SInteger
S.length SBV String
k

                      (Int -> SymbolicT IO ()) -> [Int] -> SymbolicT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Int -> SymbolicT IO ()
forall a (m :: * -> *). (Integral a, SolverContext m) => a -> m ()
restrict [Int]
range

                      -- require distinct keys:
                      let keys :: [SBV String]
keys = [(Dict String Integer
dict Dict String Integer -> SInteger -> SBV (String, Integer)
forall a. SymVal a => SList a -> SInteger -> SBV a
!! Int -> SInteger
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)SBV (String, Integer)
-> (SBV (String, Integer) -> SBV String) -> SBV String
forall a b. a -> (a -> b) -> b
^.SBV (String, Integer) -> SBV String
forall b a. HasField "_1" b a => SBV a -> SBV b
_1 | Int
i <- [Int]
range]
                      SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ [SBV String] -> SBool
forall a. EqSymbolic a => [a] -> SBool
distinct [SBV String]
keys

                      Query [(String, Integer)] -> Symbolic [(String, Integer)]
forall a. Query a -> Symbolic a
query (Query [(String, Integer)] -> Symbolic [(String, Integer)])
-> Query [(String, Integer)] -> Symbolic [(String, Integer)]
forall a b. (a -> b) -> a -> b
$ do Query ()
ensureSat
                                 Dict String Integer -> Query [(String, Integer)]
forall a. SymVal a => SBV a -> Query a
getValue Dict String Integer
dict