-----------------------------------------------------------------------------
-- |
-- 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 = forall a. Symbolic a -> IO a
runSMT forall a b. (a -> b) -> a -> b
$ do Dict String Integer
dict :: 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 forall a. Num a => a -> a -> a
- Int
1]

                      forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SList a -> SInteger
L.length Dict String Integer
dict forall a. EqSymbolic a => a -> a -> SBool
.== 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 forall a. Num a => a -> a -> a
* RegExp -> RegExp
KStar (RegExp
asciiLetter forall a. Num a => a -> a -> a
+ RegExp
digit forall a. Num a => a -> a -> a
+ RegExp
"_" forall a. Num a => a -> a -> a
+ RegExp
"'")
                                      in SInteger
l forall a. EqSymbolic a => a -> a -> SBool
.== forall a b. (Integral a, Num b) => a -> b
fromIntegral a
iforall a. Num a => a -> a -> a
+SInteger
3 SBool -> SBool -> SBool
.&& SBV String
s forall a. RegExpMatchable a => a -> RegExp -> SBool
`match` RegExp
r

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

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

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

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