-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.List
-- Copyright : (c) Joel Burget
--                 Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A collection of list utilities, useful when working with symbolic lists.
-- To the extent possible, the functions in this module follow those of "Data.List"
-- so importing qualified is the recommended workflow. Also, it is recommended
-- you use the @OverloadedLists@ and @OverloadedStrings@ extensions to allow literal
-- lists and strings to be used as symbolic literals.
--
-- You can find proofs of many list related properties in "Data.SBV.TP.List".
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                    #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE NamedFieldPuns         #-}
{-# LANGUAGE OverloadedLists        #-}
{-# LANGUAGE Rank2Types             #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE UndecidableInstances   #-}

{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

module Data.SBV.List (
        -- * Length, emptiness
          length, null

        -- * Deconstructing/Reconstructing
        , nil, (.:), snoc, head, tail, uncons, init, last, singleton, listToListAt, elemAt, (!!), implode, concat, (++)

        -- * Containment
        , elem, notElem, isInfixOf, isSuffixOf, isPrefixOf

        -- * List equality
        , listEq

        -- * Sublists
        , take, drop, splitAt, subList, replace, indexOf, offsetIndexOf

        -- * Reverse
        , reverse

        -- * Mapping
        , map, concatMap

        -- * Difference
        , (\\)

        -- * Folding
        , foldl, foldr

        -- * Zipping
        , zip, zipWith

        -- * Lookup
        , lookup

        -- * Filtering
        , filter, partition, takeWhile, dropWhile

        -- * Predicate transformers
        , all, any, and, or

        -- * Generators
        , replicate, inits, tails

        -- * Sum and product
        , sum, product

        -- * Conversion between strings and naturals
        , strToNat, natToStr

        -- * Symbolic enumerations
        , EnumSymbolic(..)
        ) where

import Prelude hiding (head, tail, init, last, length, take, drop, splitAt, concat, null, elem,
                       notElem, reverse, (++), (!!), map, concatMap, foldl, foldr, zip, zipWith, filter,
                       all, any, and, or, replicate, fst, snd, sum, product, Enum(..), lookup,
                       takeWhile, dropWhile)
import qualified Prelude as P

import Data.SBV.Core.Kind
import Data.SBV.Core.Data
import Data.SBV.Core.Model
import Data.SBV.Core.SizedFloats
import Data.SBV.Core.Floating

import Data.SBV.Tuple

import Data.Maybe (isNothing, catMaybes)
import qualified Data.Char as C

import Data.List (genericLength, genericIndex, genericDrop, genericTake, genericReplicate)
import qualified Data.List as L (inits, tails, isSuffixOf, isPrefixOf, isInfixOf, partition, (\\))

import Data.Proxy

import GHC.Exts (IsList(..))

#ifdef DOCTEST
-- $setup
-- >>> import Prelude hiding (head, tail, init, last, length, take, drop, concat, null, elem, notElem, reverse, (++), (!!), map, foldl, foldr, zip, zipWith, filter, all, any, replicate, lookup, splitAt, concatMap, and, or, sum, product, takeWhile, dropWhile)
-- >>> import qualified Prelude as P(map)
-- >>> import Data.SBV
-- >>> :set -XDataKinds
-- >>> :set -XOverloadedLists
-- >>> :set -XOverloadedStrings
-- >>> :set -XScopedTypeVariables
-- >>> :set -XTypeApplications
-- >>> :set -XQuasiQuotes
#endif

-- | IsList instance allows list literals to be written compactly.
instance SymVal a => IsList (SList a) where
  type Item (SList a) = SBV a

  fromList :: [Item (SList a)] -> SList a
fromList = (SBV a -> SList a -> SList a) -> SList a -> [SBV a] -> SList a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
P.foldr SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
(.:) SList a
forall a. SymVal a => SList a
nil -- Don't use [] here for nil, as this is the very definition of doing overloaded lists
  toList :: SList a -> [Item (SList a)]
toList SList a
x = case SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
x of
               Maybe [a]
Nothing -> String -> [SBV a]
forall a. HasCallStack => String -> a
error String
"IsList.toList used in a symbolic context"
               Just [a]
xs -> (a -> SBV a) -> [a] -> [SBV a]
forall a b. (a -> b) -> [a] -> [b]
P.map a -> SBV a
forall a. SymVal a => a -> SBV a
literal [a]
xs

-- | Length of a list.
--
-- >>> sat $ \(l :: SList Word16) -> length l .== 2
-- Satisfiable. Model:
--   s0 = [0,0] :: [Word16]
-- >>> sat $ \(l :: SList Word16) -> length l .< 0
-- Unsatisfiable
-- >>> prove $ \(l1 :: SList Word16) (l2 :: SList Word16) -> length l1 + length l2 .== length (l1 ++ l2)
-- Q.E.D.
-- >>> sat $ \(s :: SString) -> length s .== 2
-- Satisfiable. Model:
--   s0 = "BA" :: String
-- >>> sat $ \(s :: SString) -> length s .< 0
-- Unsatisfiable
-- >>> prove $ \(s1 :: SString) s2 -> length s1 + length s2 .== length (s1 ++ s2)
-- Q.E.D.
length :: forall a. SymVal a => SList a -> SInteger
length :: forall a. SymVal a => SList a -> SInteger
length = Bool -> SeqOp -> Maybe ([a] -> Integer) -> SBV [a] -> SInteger
forall a b.
(SymVal a, SymVal b) =>
Bool -> SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 Bool
False (Kind -> SeqOp
SeqLen (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))) (([a] -> Integer) -> Maybe ([a] -> Integer)
forall a. a -> Maybe a
Just (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> ([a] -> Int) -> [a] -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
P.length))

-- | @`null` s@ is True iff the list is empty
--
-- >>> prove $ \(l :: SList Word16) -> null l .<=> length l .== 0
-- Q.E.D.
-- >>> prove $ \(l :: SList Word16) -> null l .<=> l .== []
-- Q.E.D.
-- >>> prove $ \(s :: SString) -> null s .<=> length s .== 0
-- Q.E.D.
-- >>> prove $ \(s :: SString) -> null s .<=> s .== ""
-- Q.E.D.
null :: SymVal a => SList a -> SBool
null :: forall a. SymVal a => SList a -> SBool
null SList a
l
  | Just [a]
cs <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
  = Bool -> SBool
forall a. SymVal a => a -> SBV a
literal ([a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [a]
cs)
  | Bool
True
  = SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0

-- | @`head`@ returns the first element of a list. Unspecified if the list is empty.
--
-- >>> prove $ \c -> head [c] .== (c :: SInteger)
-- Q.E.D.
-- >>> prove $ \c -> c .== literal 'A' .=> ([c] :: SString) .== "A"
-- Q.E.D.
-- >>> prove $ \(c :: SChar) -> length ([c] :: SString) .== 1
-- Q.E.D.
-- >>> prove $ \(c :: SChar) -> head ([c] :: SString) .== c
-- Q.E.D.
head :: SymVal a => SList a -> SBV a
head :: forall a. SymVal a => SList a -> SBV a
head = (SList a -> SInteger -> SBV a
forall a. SymVal a => SList a -> SInteger -> SBV a
`elemAt` SInteger
0)

-- | @`tail`@ returns the tail of a list. Unspecified if the list is empty.
--
-- >>> prove $ \(h :: SInteger) t -> tail ([h] ++ t) .== t
-- Q.E.D.
-- >>> prove $ \(l :: SList Integer) -> length l .> 0 .=> length (tail l) .== length l - 1
-- Q.E.D.
-- >>> prove $ \(l :: SList Integer) -> sNot (null l) .=> [head l] ++ tail l .== l
-- Q.E.D.
-- >>> prove $ \(h :: SChar) s -> tail ([h] ++ s) .== s
-- Q.E.D.
-- >>> prove $ \(s :: SString) -> length s .> 0 .=> length (tail s) .== length s - 1
-- Q.E.D.
-- >>> prove $ \(s :: SString) -> sNot (null s) .=> [head s] ++ tail s .== s
-- Q.E.D.
tail :: SymVal a => SList a -> SList a
tail :: forall a. SymVal a => SList a -> SList a
tail SList a
l
 | Just (a
_:[a]
cs) <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
 = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal [a]
cs
 | Bool
True
 = SList a -> SInteger -> SInteger -> SList a
forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList SList a
l SInteger
1 (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)

-- | @`uncons`@ returns the pair of the head and tail. Unspecified if the list is empty.
--
-- >>> prove $ \(x :: SInteger) xs -> uncons (x .: xs) .== (x, xs)
-- Q.E.D.
uncons :: SymVal a => SList a -> (SBV a, SList a)
uncons :: forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
l = (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
head SList a
l, SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
l)

-- | @`init`@ returns all but the last element of the list. Unspecified if the list is empty.
--
-- >>> prove $ \(h :: SInteger) t -> init (t ++ [h]) .== t
-- Q.E.D.
-- >>> prove $ \(c :: SChar) t -> init (t ++ [c]) .== t
-- Q.E.D.
init :: SymVal a => SList a -> SList a
init :: forall a. SymVal a => SList a -> SList a
init SList a
l
 | Just cs :: [a]
cs@(a
_:[a]
_) <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
 = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal ([a] -> SList a) -> [a] -> SList a
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. HasCallStack => [a] -> [a]
P.init [a]
cs
 | Bool
True
 = SList a -> SInteger -> SInteger -> SList a
forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList SList a
l SInteger
0 (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)

-- | @`last`@ returns the last element of the list. Unspecified if the list is empty.
--
-- >>> prove $ \(l :: SInteger) i -> last (i ++ [l]) .== l
-- Q.E.D.
last :: SymVal a => SList a -> SBV a
last :: forall a. SymVal a => SList a -> SBV a
last SList a
l = SList a
l SList a -> SInteger -> SBV a
forall a. SymVal a => SList a -> SInteger -> SBV a
`elemAt` (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)

-- | @`singleton` x@ is the list of length 1 that contains the only value @x@.
--
-- >>> prove $ \(x :: SInteger) -> head [x] .== x
-- Q.E.D.
-- >>> prove $ \(x :: SInteger) -> length [x] .== 1
-- Q.E.D.
singleton :: forall a. SymVal a => SBV a -> SList a
singleton :: forall a. SymVal a => SBV a -> SList a
singleton = Bool -> SeqOp -> Maybe (a -> [a]) -> SBV a -> SBV [a]
forall a b.
(SymVal a, SymVal b) =>
Bool -> SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 Bool
False (Kind -> SeqOp
SeqUnit (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))) ((a -> [a]) -> Maybe (a -> [a])
forall a. a -> Maybe a
Just (a -> [a] -> [a]
forall a. a -> [a] -> [a]
: []))

-- | @`listToListAt` l offset@. List of length 1 at @offset@ in @l@. Unspecified if
-- index is out of bounds.
--
-- >>> prove $ \(l1 :: SList Integer) l2 -> listToListAt (l1 ++ l2) (length l1) .== listToListAt l2 0
-- Q.E.D.
-- >>> sat $ \(l :: SList Word16) -> length l .>= 2 .&& listToListAt l 0 ./= listToListAt l (length l - 1)
-- Satisfiable. Model:
--   s0 = [0,64] :: [Word16]
listToListAt :: SymVal a => SList a -> SInteger -> SList a
listToListAt :: forall a. SymVal a => SList a -> SInteger -> SList a
listToListAt SList a
s SInteger
offset = SList a -> SInteger -> SInteger -> SList a
forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList SList a
s SInteger
offset SInteger
1

-- | @`elemAt` l i@ is the value stored at location @i@, starting at 0. Unspecified if
-- index is out of bounds.
--
-- >>> prove $ \i -> i `inRange` (0, 4) .=> [1,1,1,1,1] `elemAt` i .== (1::SInteger)
-- Q.E.D.
-- >>> prove $ \i -> i .>= 0 .&& i .<= 4 .=> "AAAAA" `elemAt` i .== literal 'A'
-- Q.E.D.
elemAt :: forall a. SymVal a => SList a -> SInteger -> SBV a
elemAt :: forall a. SymVal a => SList a -> SInteger -> SBV a
elemAt SList a
l SInteger
i
  | Just [a]
xs <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l, Just Integer
ci <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
i, Integer
ci Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0, Integer
ci Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< [a] -> Integer
forall i a. Num i => [a] -> i
genericLength [a]
xs, let x :: a
x = [a]
xs [a] -> Integer -> a
forall i a. Integral i => [a] -> i -> a
`genericIndex` Integer
ci
  = a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
x
  | Bool
True
  = Bool
-> SeqOp
-> Maybe ([a] -> Integer -> a)
-> SList a
-> SInteger
-> SBV a
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 Bool
False (Kind -> SeqOp
SeqNth (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))) Maybe ([a] -> Integer -> a)
forall a. Maybe a
Nothing SList a
l SInteger
i

-- | Short cut for 'elemAt'
--
-- >>> prove $ \(xs :: SList Integer) i -> xs !! i .== xs `elemAt` i
-- Q.E.D.
(!!) :: SymVal a => SList a -> SInteger -> SBV a
!! :: forall a. SymVal a => SList a -> SInteger -> SBV a
(!!) = SList a -> SInteger -> SBV a
forall a. SymVal a => SList a -> SInteger -> SBV a
elemAt

-- | @`implode` es@ is the list of length @|es|@ containing precisely those
-- elements. Note that there is no corresponding function @explode@, since
-- we wouldn't know the length of a symbolic list.
--
-- >>> prove $ \(e1 :: SInteger) e2 e3 -> length (implode [e1, e2, e3]) .== 3
-- Q.E.D.
-- >>> prove $ \(e1 :: SInteger) e2 e3 -> P.map (elemAt (implode [e1, e2, e3])) (P.map literal [0 .. 2]) .== [e1, e2, e3]
-- Q.E.D.
-- >>> prove $ \(c1 :: SChar) c2 c3 -> length (implode [c1, c2, c3]) .== 3
-- Q.E.D.
-- >>> prove $ \(c1 :: SChar) c2 c3 -> P.map (elemAt (implode [c1, c2, c3])) (P.map literal [0 .. 2]) .== [c1, c2, c3]
-- Q.E.D.
implode :: SymVal a => [SBV a] -> SList a
implode :: forall a. SymVal a => [SBV a] -> SList a
implode = (SBV a -> SList a -> SList a) -> SList a -> [SBV a] -> SList a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
P.foldr (SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
(++) (SList a -> SList a -> SList a)
-> (SBV a -> SList a) -> SBV a -> SList a -> SList a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \SBV a
x -> [Item (SList a)
SBV a
x]) ([a] -> SList a
forall a. SymVal a => a -> SBV a
literal [])

-- | Prepend an element, the traditional @cons@.
--
-- >>> 1 .: 2 .: 3 .: [4, 5, 6 :: SInteger]
-- [1,2,3,4,5,6] :: [SInteger]
infixr 5 .:
(.:) :: SymVal a => SBV a -> SList a -> SList a
SBV a
a .: :: forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as = SBV a -> SList a
forall a. SymVal a => SBV a -> SList a
singleton SBV a
a SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
as  -- NB. Don't do "[a] ++ as" here. That type-checks but is recursive due to how overloaded-lists work.

-- | Append an element
--
-- >>> [1, 2, 3 :: SInteger] `snoc` 4 `snoc` 5 `snoc` 6
-- [1,2,3,4,5,6] :: [SInteger]
snoc :: SymVal a => SList a -> SBV a -> SList a
SList a
as snoc :: forall a. SymVal a => SList a -> SBV a -> SList a
`snoc` SBV a
a = SList a
as SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ [Item (SList a)
SBV a
a]

-- | Empty list. This value has the property that it's the only list with length 0. If you use @OverloadedLists@ extension,
-- you can write it as the familiar `[]`.
--
-- >>> prove $ \(l :: SList Integer) -> length l .== 0 .<=> l .== []
-- Q.E.D.
-- >>> prove $ \(l :: SString) -> length l .== 0 .<=> l .== []
-- Q.E.D.
nil :: SymVal a => SList a
nil :: forall a. SymVal a => SList a
nil = [a] -> SBV [a]
forall a. SymVal a => a -> SBV a
literal []

-- | Append two lists.
--
-- >>> sat $ \x y (z :: SList Integer) -> length x .== 5 .&& length y .== 1 .&& x ++ y ++ z .== [sEnum|1 .. 12|]
-- Satisfiable. Model:
--   s0 =      [1,2,3,4,5] :: [Integer]
--   s1 =              [6] :: [Integer]
--   s2 = [7,8,9,10,11,12] :: [Integer]
-- >>> sat $ \(x :: SString) y z -> length x .== 5 .&& length y .== 1 .&& x ++ y ++ z .== "Hello world!"
-- Satisfiable. Model:
--   s0 =  "Hello" :: String
--   s1 =      " " :: String
--   s2 = "world!" :: String
infixr 5 ++
(++) :: forall a. SymVal a => SList a -> SList a -> SList a
SList a
x ++ :: forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
y | SList a -> Bool
forall a. SymVal a => SList a -> Bool
isConcretelyEmpty SList a
x = SList a
y
       | SList a -> Bool
forall a. SymVal a => SList a -> Bool
isConcretelyEmpty SList a
y = SList a
x
       | Bool
True                = Bool
-> SeqOp
-> Maybe ([a] -> [a] -> [a])
-> SList a
-> SList a
-> SList a
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 Bool
False (Kind -> SeqOp
SeqConcat (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))) (([a] -> [a] -> [a]) -> Maybe ([a] -> [a] -> [a])
forall a. a -> Maybe a
Just [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(P.++)) SList a
x SList a
y

-- | @`elem` e l@. Does @l@ contain the element @e@?
--
-- >>> prove $ \(xs :: SList Integer) x -> x `elem` xs .=> length xs .>= 1
-- Q.E.D.
elem :: (Eq a, SymVal a) => SBV a -> SList a -> SBool
SBV a
e elem :: forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList a
l = [Item (SList a)
SBV a
e] SList a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
`isInfixOf` SList a
l

-- | @`notElem` e l@. Does @l@ not contain the element @e@?
--
-- >>> prove $ \(x :: SList Integer) -> x `notElem` []
-- Q.E.D.
notElem :: (Eq a, SymVal a) => SBV a -> SList a -> SBool
SBV a
e notElem :: forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`notElem` SList a
l = SBool -> SBool
sNot (SBV a
e SBV a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList a
l)

-- | @`isInfixOf` sub l@. Does @l@ contain the subsequence @sub@?
--
-- >>> prove $ \(l1 :: SList Integer) l2 l3 -> l2 `isInfixOf` (l1 ++ l2 ++ l3)
-- Q.E.D.
-- >>> prove $ \(l1 :: SList Integer) l2 -> l1 `isInfixOf` l2 .&& l2 `isInfixOf` l1 .<=> l1 .== l2
-- Q.E.D.
-- >>> prove $ \(s1 :: SString) s2 s3 -> s2 `isInfixOf` (s1 ++ s2 ++ s3)
-- Q.E.D.
-- >>> prove $ \(s1 :: SString) s2 -> s1 `isInfixOf` s2 .&& s2 `isInfixOf` s1 .<=> s1 .== s2
-- Q.E.D.
isInfixOf :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
SList a
sub isInfixOf :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
`isInfixOf` SList a
l
  | SList a -> Bool
forall a. SymVal a => SList a -> Bool
isConcretelyEmpty SList a
sub
  = Bool -> SBool
forall a. SymVal a => a -> SBV a
literal Bool
True
  | Bool
True
  = Bool
-> SeqOp
-> Maybe ([a] -> [a] -> Bool)
-> SList a
-> SList a
-> SBool
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 Bool
True (Kind -> SeqOp
SeqContains (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))) (([a] -> [a] -> Bool) -> Maybe ([a] -> [a] -> Bool)
forall a. a -> Maybe a
Just (([a] -> [a] -> Bool) -> [a] -> [a] -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
L.isInfixOf)) SList a
l SList a
sub -- NB. flip, since `SeqContains` takes args in rev order!

-- | @`isPrefixOf` pre l@. Is @pre@ a prefix of @l@?
--
-- >>> prove $ \(l1 :: SList Integer) l2 -> l1 `isPrefixOf` (l1 ++ l2)
-- Q.E.D.
-- >>> prove $ \(l1 :: SList Integer) l2 -> l1 `isPrefixOf` l2 .=> subList l2 0 (length l1) .== l1
-- Q.E.D.
-- >>> prove $ \(s1 :: SString) s2 -> s1 `isPrefixOf` (s1 ++ s2)
-- Q.E.D.
-- >>> prove $ \(s1 :: SString) s2 -> s1 `isPrefixOf` s2 .=> subList s2 0 (length s1) .== s1
-- Q.E.D.
isPrefixOf :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
SList a
pre isPrefixOf :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
`isPrefixOf` SList a
l
  | SList a -> Bool
forall a. SymVal a => SList a -> Bool
isConcretelyEmpty SList a
pre
  = Bool -> SBool
forall a. SymVal a => a -> SBV a
literal Bool
True
  | Bool
True
  = Bool
-> SeqOp
-> Maybe ([a] -> [a] -> Bool)
-> SList a
-> SList a
-> SBool
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 Bool
True (Kind -> SeqOp
SeqPrefixOf (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))) (([a] -> [a] -> Bool) -> Maybe ([a] -> [a] -> Bool)
forall a. a -> Maybe a
Just [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
L.isPrefixOf) SList a
pre SList a
l

-- | @listEq@ is a variant of equality that you can use for lists of floats. It respects @NaN /= NaN@. The reason
-- we do not do this automatically is that it complicates proof objectives usually, as it does not simply resolve to
-- the native equality check.
listEq :: forall a. SymVal a => SList a -> SList a -> SBool
listEq :: forall a. SymVal a => SList a -> SList a -> SBool
listEq
  | Kind -> Bool
containsFloats (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))
  = String
-> (SList a -> SList a -> SBool) -> SList a -> SList a -> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"listEq" ((SList a -> SList a -> SBool) -> SList a -> SList a -> SBool)
-> (SList a -> SList a -> SBool) -> SList a -> SList a -> SBool
forall a b. (a -> b) -> a -> b
$ \SList a
xs SList a
ys -> SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs) (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
ys) (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
head SList a
xs SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
head SList a
ys SBool -> SBool -> SBool
.&& SList a -> SList a -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
listEq (SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
xs) (SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
ys))
  | Bool
True
  = SList a -> SList a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
(.==)

-- | @`isSuffixOf` suf l@. Is @suf@ a suffix of @l@?
--
-- >>> prove $ \(l1 :: SList Word16) l2 -> l2 `isSuffixOf` (l1 ++ l2)
-- Q.E.D.
-- >>> prove $ \(l1 :: SList Word16) l2 -> l1 `isSuffixOf` l2 .=> subList l2 (length l2 - length l1) (length l1) .== l1
-- Q.E.D.
-- >>> prove $ \(s1 :: SString) s2 -> s2 `isSuffixOf` (s1 ++ s2)
-- Q.E.D.
-- >>> prove $ \(s1 :: SString) s2 -> s1 `isSuffixOf` s2 .=> subList s2 (length s2 - length s1) (length s1) .== s1
-- Q.E.D.
isSuffixOf :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
SList a
suf isSuffixOf :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
`isSuffixOf` SList a
l
  | SList a -> Bool
forall a. SymVal a => SList a -> Bool
isConcretelyEmpty SList a
suf
  = Bool -> SBool
forall a. SymVal a => a -> SBV a
literal Bool
True
  | Bool
True
  = Bool
-> SeqOp
-> Maybe ([a] -> [a] -> Bool)
-> SList a
-> SList a
-> SBool
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 Bool
True (Kind -> SeqOp
SeqSuffixOf (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))) (([a] -> [a] -> Bool) -> Maybe ([a] -> [a] -> Bool)
forall a. a -> Maybe a
Just [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
L.isSuffixOf) SList a
suf SList a
l

-- | @`take` len l@. Corresponds to Haskell's `take` on symbolic lists.
--
-- >>> prove $ \(l :: SList Integer) i -> i .>= 0 .=> length (take i l) .<= i
-- Q.E.D.
-- >>> prove $ \(s :: SString) i -> i .>= 0 .=> length (take i s) .<= i
-- Q.E.D.
take :: SymVal a => SInteger -> SList a -> SList a
take :: forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
i SList a
l = SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0)        ([a] -> SList a
forall a. SymVal a => a -> SBV a
literal [])
         (SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l) SList a
l
         (SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ SList a -> SInteger -> SInteger -> SList a
forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList SList a
l SInteger
0 SInteger
i

-- | @`drop` len s@. Corresponds to Haskell's `drop` on symbolic-lists.
--
-- >>> prove $ \(l :: SList Word16) i -> length (drop i l) .<= length l
-- Q.E.D.
-- >>> prove $ \(l :: SList Word16) i -> take i l ++ drop i l .== l
-- Q.E.D.
-- >>> prove $ \(s :: SString) i -> length (drop i s) .<= length s
-- Q.E.D.
-- >>> prove $ \(s :: SString) i -> take i s ++ drop i s .== s
-- Q.E.D.
drop :: SymVal a => SInteger -> SList a -> SList a
drop :: forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
i SList a
s = SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
ls) ([a] -> SList a
forall a. SymVal a => a -> SBV a
literal [])
         (SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0)  SList a
s
         (SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ SList a -> SInteger -> SInteger -> SList a
forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList SList a
s SInteger
i (SInteger
ls SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
i)
  where ls :: SInteger
ls = SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
s

-- | @splitAt n xs = (take n xs, drop n xs)@
--
-- >>> prove $ \n (xs :: SList Integer) -> let (l, r) = splitAt n xs in l ++ r .== xs
-- Q.E.D.
splitAt :: SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt :: forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt SInteger
n SList a
xs = (SInteger -> SList a -> SList a
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList a
xs, SInteger -> SList a -> SList a
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList a
xs)

-- | @`subList` s offset len@ is the sublist of @s@ at offset @offset@ with length @len@.
-- This function is under-specified when the offset is outside the range of positions in @s@ or @len@
-- is negative or @offset+len@ exceeds the length of @s@.
--
-- >>> prove $ \(l :: SList Integer) i -> i .>= 0 .&& i .< length l .=> subList l 0 i ++ subList l i (length l - i) .== l
-- Q.E.D.
-- >>> sat  $ \i j -> subList [sEnum|1..5|] i j .== [sEnum|2..4::SInteger|]
-- Satisfiable. Model:
--   s0 = 1 :: Integer
--   s1 = 3 :: Integer
-- >>> sat  $ \i j -> subList [sEnum|1..5|] i j .== [sEnum|6..7::SInteger|]
-- Unsatisfiable
-- >>> prove $ \(s1 :: SString) (s2 :: SString) -> subList (s1 ++ s2) (length s1) 1 .== subList s2 0 1
-- Q.E.D.
-- >>> sat $ \(s :: SString) -> length s .>= 2 .&& subList s 0 1 ./= subList s (length s - 1) 1
-- Satisfiable. Model:
--   s0 = "AB" :: String
-- >>> prove $ \(s :: SString) i -> i .>= 0 .&& i .< length s .=> subList s 0 i ++ subList s i (length s - i) .== s
-- Q.E.D.
-- >>> sat  $ \i j -> subList "hello" i j .== ("ell" :: SString)
-- Satisfiable. Model:
--   s0 = 1 :: Integer
--   s1 = 3 :: Integer
-- >>> sat  $ \i j -> subList "hell" i j .== ("no" :: SString)
-- Unsatisfiable
subList :: forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList :: forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList SList a
l SInteger
offset SInteger
len
  | Just [a]
c  <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l                   -- a constant list
  , Just Integer
o  <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
offset              -- a constant offset
  , Just Integer
sz <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
len                 -- a constant length
  , let lc :: Integer
lc = [a] -> Integer
forall i a. Num i => [a] -> i
genericLength [a]
c                 -- length of the list
  , let valid :: Integer -> Bool
valid Integer
x = Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
lc          -- predicate that checks valid point
  , Integer -> Bool
valid Integer
o                                  -- offset is valid
  , Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0                                  -- length is not-negative
  , Integer -> Bool
valid (Integer -> Bool) -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ Integer
o Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
sz                           -- we don't overrun
  = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal ([a] -> SList a) -> [a] -> SList a
forall a b. (a -> b) -> a -> b
$ Integer -> [a] -> [a]
forall i a. Integral i => i -> [a] -> [a]
genericTake Integer
sz ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ Integer -> [a] -> [a]
forall i a. Integral i => i -> [a] -> [a]
genericDrop Integer
o [a]
c
  | Bool
True                                     -- either symbolic, or something is out-of-bounds
  = Bool
-> SeqOp
-> Maybe ([a] -> Integer -> Integer -> [a])
-> SList a
-> SInteger
-> SInteger
-> SList a
forall a b c d.
(SymVal a, SymVal b, SymVal c, SymVal d) =>
Bool
-> SeqOp
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> SBV d
lift3 Bool
False (Kind -> SeqOp
SeqSubseq (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))) Maybe ([a] -> Integer -> Integer -> [a])
forall a. Maybe a
Nothing SList a
l SInteger
offset SInteger
len

-- | @`replace` l src dst@. Replace the first occurrence of @src@ by @dst@ in @s@
--
-- >>> prove $ \l -> replace [sEnum|1..5|] l [sEnum|6..10|] .== [sEnum|6..10|] .=> l .== [sEnum|1..5::SWord8|]
-- Q.E.D.
-- >>> prove $ \(l1 :: SList Integer) l2 l3 -> length l2 .> length l1 .=> replace l1 l2 l3 .== l1
-- Q.E.D.
-- >>> prove $ \(s :: SString) -> replace "hello" s "world" .== "world" .=> s .== "hello"
-- Q.E.D.
-- >>> prove $ \(s1 :: SString) s2 s3 -> length s2 .> length s1 .=> replace s1 s2 s3 .== s1
-- Q.E.D.
replace :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SList a -> SList a
replace :: forall a.
(Eq a, SymVal a) =>
SList a -> SList a -> SList a -> SList a
replace SList a
l SList a
src SList a
dst
  | Just [a]
b <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
src, [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [a]
b   -- If src is null, simply prepend
  = SList a
dst SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
l
  | Kind -> Bool
eqCheckIsObjectEq Kind
ka
  , Just [a]
a <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
  , Just [a]
b <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
src
  , Just [a]
c <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
dst
  = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal ([a] -> SList a) -> [a] -> SList a
forall a b. (a -> b) -> a -> b
$ [a] -> [a] -> [a] -> [a]
forall {a}. Eq a => [a] -> [a] -> [a] -> [a]
walk [a]
a [a]
b [a]
c
  | Bool
True
  = Bool
-> SeqOp
-> Maybe ([a] -> [a] -> [a] -> [a])
-> SList a
-> SList a
-> SList a
-> SList a
forall a b c d.
(SymVal a, SymVal b, SymVal c, SymVal d) =>
Bool
-> SeqOp
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> SBV d
lift3 Bool
True (Kind -> SeqOp
SeqReplace Kind
ka) Maybe ([a] -> [a] -> [a] -> [a])
forall a. Maybe a
Nothing SList a
l SList a
src SList a
dst
  where walk :: [a] -> [a] -> [a] -> [a]
walk [a]
haystack [a]
needle [a]
newNeedle = [a] -> [a]
go [a]
haystack   -- note that needle is guaranteed non-empty here.
           where go :: [a] -> [a]
go []       = []
                 go i :: [a]
i@(a
c:[a]
cs)
                  | [a]
needle [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` [a]
i = [a]
newNeedle [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
P.++ Integer -> [a] -> [a]
forall i a. Integral i => i -> [a] -> [a]
genericDrop ([a] -> Integer
forall i a. Num i => [a] -> i
genericLength [a]
needle :: Integer) [a]
i
                  | Bool
True                    = a
c a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a]
go [a]
cs

        ka :: Kind
ka = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)

-- | @`indexOf` l sub@. Retrieves first position of @sub@ in @l@, @-1@ if there are no occurrences.
-- Equivalent to @`offsetIndexOf` l sub 0@.
--
-- >>> prove $ \(l1 :: SList Word16) l2 -> length l2 .> length l1 .=> indexOf l1 l2 .== -1
-- Q.E.D.
-- >>> prove $ \s1 s2 -> length s2 .> length s1 .=> indexOf s1 s2 .== -1
-- Q.E.D.
indexOf :: (Eq a, SymVal a) => SList a -> SList a -> SInteger
indexOf :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SInteger
indexOf SList a
s SList a
sub = SList a -> SList a -> SInteger -> SInteger
forall a.
(Eq a, SymVal a) =>
SList a -> SList a -> SInteger -> SInteger
offsetIndexOf SList a
s SList a
sub SInteger
0

-- | @`offsetIndexOf` l sub offset@. Retrieves first position of @sub@ at or
-- after @offset@ in @l@, @-1@ if there are no occurrences.
--
-- >>> prove $ \(l :: SList Int8) sub -> offsetIndexOf l sub 0 .== indexOf l sub
-- Q.E.D.
-- >>> prove $ \(l :: SList Int8) sub i -> i .>= length l .&& length sub .> 0 .=> offsetIndexOf l sub i .== -1
-- Q.E.D.
-- >>> prove $ \(l :: SList Int8) sub i -> i .> length l .=> offsetIndexOf l sub i .== -1
-- Q.E.D.
-- >>> prove $ \(s :: SString) sub -> offsetIndexOf s sub 0 .== indexOf s sub
-- Q.E.D.
-- >>> prove $ \(s :: SString) sub i -> i .>= length s .&& length sub .> 0 .=> offsetIndexOf s sub i .== -1
-- Q.E.D.
-- >>> prove $ \(s :: SString) sub i -> i .> length s .=> offsetIndexOf s sub i .== -1
-- Q.E.D.
offsetIndexOf :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SInteger -> SInteger
offsetIndexOf :: forall a.
(Eq a, SymVal a) =>
SList a -> SList a -> SInteger -> SInteger
offsetIndexOf SList a
s SList a
sub SInteger
offset
  | Kind -> Bool
eqCheckIsObjectEq Kind
ka
  , Just [a]
c <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
s        -- a constant list
  , Just [a]
n <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
sub      -- a constant search pattern
  , Just Integer
o <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
offset   -- at a constant offset
  , Integer
o Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0, Integer
o Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= [a] -> Integer
forall i a. Num i => [a] -> i
genericLength [a]
c        -- offset is good
  = case [Integer
i | (Integer
i, [a]
t) <- [Integer] -> [[a]] -> [(Integer, [a])]
forall a b. [a] -> [b] -> [(a, b)]
P.zip [Integer
Item [Integer]
o ..] ([a] -> [[a]]
forall a. [a] -> [[a]]
L.tails (Integer -> [a] -> [a]
forall i a. Integral i => i -> [a] -> [a]
genericDrop Integer
o [a]
c)), [a]
n [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` [a]
t] of
      (Integer
i:[Integer]
_) -> Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
i
      [Integer]
_     -> -SInteger
1
  | Bool
True
  = Bool
-> SeqOp
-> Maybe ([a] -> [a] -> Integer -> Integer)
-> SList a
-> SList a
-> SInteger
-> SInteger
forall a b c d.
(SymVal a, SymVal b, SymVal c, SymVal d) =>
Bool
-> SeqOp
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> SBV d
lift3 Bool
True (Kind -> SeqOp
SeqIndexOf Kind
ka) Maybe ([a] -> [a] -> Integer -> Integer)
forall a. Maybe a
Nothing SList a
s SList a
sub SInteger
offset
  where ka :: Kind
ka = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)

-- | @`reverse` s@ reverses the sequence.
--
-- NB. We can define @reverse@ in terms of @foldl@ as: @foldl (\soFar elt -> [elt] ++ soFar) []@
-- But in my experiments, I found that this definition performs worse instead of the recursive definition
-- SBV generates for reverse calls. So we're keeping it intact.
--
-- >>> sat $ \(l :: SList Integer) -> reverse l .== literal [3, 2, 1]
-- Satisfiable. Model:
--   s0 = [1,2,3] :: [Integer]
-- >>> prove $ \(l :: SList Word32) -> reverse l .== [] .<=> null l
-- Q.E.D.
-- >>> sat $ \(l :: SString ) -> reverse l .== "321"
-- Satisfiable. Model:
--   s0 = "123" :: String
-- >>> prove $ \(l :: SString) -> reverse l .== "" .<=> null l
-- Q.E.D.
reverse :: forall a. SymVal a => SList a -> SList a
reverse :: forall a. SymVal a => SList a -> SList a
reverse SList a
l
  | Just [a]
l' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
  = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal ([a] -> [a]
forall a. [a] -> [a]
P.reverse [a]
l')
  | Bool
True
  = SList a -> SList a
def SList a
l
  where def :: SList a -> SList a
def = String -> (SList a -> SList a) -> SList a -> SList a
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"sbv.reverse" ((SList a -> SList a) -> SList a -> SList a)
-> (SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ \SList a
xs -> SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs) [] (let (SBV a
h, SList a
t) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs in SList a -> SList a
def SList a
t SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ [Item (SList a)
SBV a
h])

-- | A class of mappable functions. In SBV, we make a distinction between closures and regular functions, and
-- we instantiate this class appropriately so it can handle both cases.
class (SymVal a, SymVal b) => SMap func a b | func -> a b where
  -- | Map a function (or a closure) over a symbolic list.
  --
  -- >>> map (+ (1 :: SInteger)) [sEnum|1 .. 5 :: SInteger|]
  -- [2,3,4,5,6] :: [SInteger]
  -- >>> map (+ (1 :: SWord 8)) [sEnum|1 .. 5 :: SWord 8|]
  -- [2,3,4,5,6] :: [SWord8]
  -- >>> map (\x -> [x] :: SList Integer) [sEnum|1 .. 3 :: SInteger|]
  -- [[1],[2],[3]] :: [[SInteger]]
  -- >>> import Data.SBV.Tuple
  -- >>> map (\t -> t^._1 + t^._2) (literal [(x, y) | x <- [1..3], y <- [4..6]] :: SList (Integer, Integer))
  -- [5,6,7,6,7,8,7,8,9] :: [SInteger]
  --
  -- Of course, SBV's 'map' can also be reused in reverse:
  --
  -- >>> sat $ \l -> map (+(1 :: SInteger)) l .== [1,2,3 :: SInteger]
  -- Satisfiable. Model:
  --   s0 = [0,1,2] :: [Integer]
  map :: func -> SList a -> SList b

  -- | Handle the concrete case of mapping. Used internally only.
  concreteMap :: func -> (SBV a -> SBV b) -> SList a -> Maybe [b]
  concreteMap func
_ SBV a -> SBV b
f SList a
sas
    | Just [a]
as <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
sas
    = case (a -> Maybe b) -> [a] -> [Maybe b]
forall a b. (a -> b) -> [a] -> [b]
P.map (SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBV b -> Maybe b) -> (a -> SBV b) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SBV b
f (SBV a -> SBV b) -> (a -> SBV a) -> a -> SBV b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SBV a
forall a. SymVal a => a -> SBV a
literal) [a]
as of
         [Maybe b]
bs | (Maybe b -> Bool) -> [Maybe b] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
P.any Maybe b -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe b]
bs -> Maybe [b]
forall a. Maybe a
Nothing
            | Bool
True               -> [b] -> Maybe [b]
forall a. a -> Maybe a
Just ([Maybe b] -> [b]
forall a. [Maybe a] -> [a]
catMaybes [Maybe b]
bs)
    | Bool
True
    = Maybe [b]
forall a. Maybe a
Nothing

-- | Mapping symbolic functions.
instance (SymVal a, SymVal b) => SMap (SBV a -> SBV b) a b where
  -- | @`map` f s@ maps the operation on to sequence.
  map :: (SBV a -> SBV b) -> SList a -> SList b
map SBV a -> SBV b
f SList a
l
    | Just [b]
concResult <- (SBV a -> SBV b) -> (SBV a -> SBV b) -> SList a -> Maybe [b]
forall func a b.
SMap func a b =>
func -> (SBV a -> SBV b) -> SList a -> Maybe [b]
concreteMap SBV a -> SBV b
f SBV a -> SBV b
f SList a
l
    = [b] -> SList b
forall a. SymVal a => a -> SBV a
literal [b]
concResult
    | Bool
True
    = SList a -> SList b
sbvMap SList a
l
    where sbvMap :: SList a -> SList b
sbvMap = String
-> (SBV a -> SBV b) -> (SList a -> SList b) -> SList a -> SList b
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.map" SBV a -> SBV b
f ((SList a -> SList b) -> SList a -> SList b)
-> (SList a -> SList b) -> SList a -> SList b
forall a b. (a -> b) -> a -> b
$ \SList a
xs -> SBool -> SList b -> SList b -> SList b
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs) [] (let (SBV a
h, SList a
t) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs in SBV a -> SBV b
f SBV a
h SBV b -> SList b -> SList b
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList b
sbvMap SList a
t)

-- | Mapping symbolic closures.
instance (SymVal env, SymVal a, SymVal b) => SMap (Closure (SBV env) (SBV a -> SBV b)) a b where
  map :: Closure (SBV env) (SBV a -> SBV b) -> SList a -> SList b
map cls :: Closure (SBV env) (SBV a -> SBV b)
cls@Closure{SBV env
closureEnv :: SBV env
closureEnv :: forall env a. Closure env a -> env
closureEnv, SBV env -> SBV a -> SBV b
closureFun :: SBV env -> SBV a -> SBV b
closureFun :: forall env a. Closure env a -> env -> a
closureFun} SList a
l
    | Just [b]
concResult <- Closure (SBV env) (SBV a -> SBV b)
-> (SBV a -> SBV b) -> SList a -> Maybe [b]
forall func a b.
SMap func a b =>
func -> (SBV a -> SBV b) -> SList a -> Maybe [b]
concreteMap Closure (SBV env) (SBV a -> SBV b)
cls (SBV env -> SBV a -> SBV b
closureFun SBV env
closureEnv) SList a
l
    = [b] -> SList b
forall a. SymVal a => a -> SBV a
literal [b]
concResult
    | Bool
True
    = SBV (env, [a]) -> SList b
sbvMap ((SBV env, SList a) -> SBV (env, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
closureEnv, SList a
l))
    where sbvMap :: SBV (env, [a]) -> SList b
sbvMap = String
-> (SBV env -> SBV a -> SBV b)
-> (SBV (env, [a]) -> SList b)
-> SBV (env, [a])
-> SList b
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.closureMap" SBV env -> SBV a -> SBV b
closureFun
                 ((SBV (env, [a]) -> SList b) -> SBV (env, [a]) -> SList b)
-> (SBV (env, [a]) -> SList b) -> SBV (env, [a]) -> SList b
forall a b. (a -> b) -> a -> b
$ \SBV (env, [a])
envxs -> let (SBV env
cEnv, SList a
xs) = SBV (env, [a]) -> (SBV env, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple SBV (env, [a])
envxs
                                 (SBV a
h, SList a
t)     = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                             in SBool -> SList b -> SList b -> SList b
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs) [] (SBV env -> SBV a -> SBV b
closureFun SBV env
cEnv SBV a
h SBV b -> SList b -> SList b
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV (env, [a]) -> SList b
sbvMap ((SBV env, SList a) -> SBV (env, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
cEnv, SList a
t)))

-- | @concatMap f xs@ maps f over elements and concats the result.
--
-- >>> concatMap (\x -> [x, x] :: SList Integer) [sEnum|1 .. 3|]
-- [1,1,2,2,3,3] :: [SInteger]
concatMap :: (SMap func a [b], SymVal b) => func -> SList a -> SList b
concatMap :: forall func a b.
(SMap func a [b], SymVal b) =>
func -> SList a -> SList b
concatMap func
f = SList [b] -> SList b
forall a. SymVal a => SList [a] -> SList a
concat (SList [b] -> SList b)
-> (SList a -> SList [b]) -> SList a -> SList b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. func -> SList a -> SList [b]
forall func a b. SMap func a b => func -> SList a -> SList b
map func
f

-- | A class of left foldable functions. In SBV, we make a distinction between closures and regular functions, and
-- we instantiate this class appropriately so it can handle both cases.
class (SymVal a, SymVal b) => SFoldL func a b | func -> a b where
  -- | @`foldl` f base s@ folds the from the left.
  --
  -- >>> foldl ((+) @SInteger) 0 [sEnum|1 .. 5|]
  -- 15 :: SInteger
  -- >>> foldl ((*) @SInteger) 1 [sEnum|1 .. 5|]
  -- 120 :: SInteger
  -- >>> foldl (\soFar elt -> [elt] ++ soFar) ([] :: SList Integer) [sEnum|1 .. 5|]
  -- [5,4,3,2,1] :: [SInteger]
  --
  -- Again, we can use 'Data.SBV.List.foldl' in the reverse too:
  --
  -- >>> sat $ \l -> foldl (\soFar elt -> [elt] ++ soFar) ([] :: SList Integer) l .== [5, 4, 3, 2, 1 :: SInteger]
  -- Satisfiable. Model:
  --   s0 = [1,2,3,4,5] :: [Integer]
  foldl :: (SymVal a, SymVal b) => func -> SBV b -> SList a -> SBV b

  -- | Handle the concrete case for folding left. Used internally only.
  concreteFoldl :: func -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> Maybe b
  concreteFoldl func
_ SBV b -> SBV a -> SBV b
f SBV b
sb SList a
sas
     | Just b
b <- SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just [a]
as <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
sas
     = b -> [a] -> Maybe b
go b
b [a]
as
     | Bool
True
     = Maybe b
forall a. Maybe a
Nothing
     where go :: b -> [a] -> Maybe b
go b
b []     = b -> Maybe b
forall a. a -> Maybe a
Just b
b
           go b
b (a
e:[a]
es) = case SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral (b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
b SBV b -> SBV a -> SBV b
`f` a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
e) of
                           Maybe b
Nothing -> Maybe b
forall a. Maybe a
Nothing
                           Just b
b' -> b -> [a] -> Maybe b
go b
b' [a]
es

-- | Folding left with symbolic functions.
instance (SymVal a, SymVal b) => SFoldL (SBV b -> SBV a -> SBV b) a b where
  -- | @`foldl` f b s@ folds the sequence from the left.
  foldl :: (SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SBV b -> SBV a -> SBV b
f SBV b
base SList a
l
    | Just b
concResult <- (SBV b -> SBV a -> SBV b)
-> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> Maybe b
forall func a b.
SFoldL func a b =>
func -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> Maybe b
concreteFoldl SBV b -> SBV a -> SBV b
f SBV b -> SBV a -> SBV b
f SBV b
base SList a
l
    = b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
concResult
    | Bool
True
    = SBV (b, [a]) -> SBV b
sbvFoldl (SBV (b, [a]) -> SBV b) -> SBV (b, [a]) -> SBV b
forall a b. (a -> b) -> a -> b
$ (SBV b, SList a) -> SBV (b, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV b
base, SList a
l)
    where sbvFoldl :: SBV (b, [a]) -> SBV b
sbvFoldl = String
-> (SBV (b, a) -> SBV b)
-> (SBV (b, [a]) -> SBV b)
-> SBV (b, [a])
-> SBV b
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.foldl" ((SBV b -> SBV a -> SBV b) -> (SBV b, SBV a) -> SBV b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SBV b -> SBV a -> SBV b
f ((SBV b, SBV a) -> SBV b)
-> (SBV (b, a) -> (SBV b, SBV a)) -> SBV (b, a) -> SBV b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV (b, a) -> (SBV b, SBV a)
forall tup a. Tuple tup a => SBV tup -> a
untuple)
                   ((SBV (b, [a]) -> SBV b) -> SBV (b, [a]) -> SBV b)
-> (SBV (b, [a]) -> SBV b) -> SBV (b, [a]) -> SBV b
forall a b. (a -> b) -> a -> b
$ \SBV (b, [a])
exs -> let (SBV b
e, SList a
xs) = SBV (b, [a]) -> (SBV b, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple SBV (b, [a])
exs
                                 (SBV a
h, SList a
t)  = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                             in SBool -> SBV b -> SBV b -> SBV b
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                    SBV b
e
                                    (SBV (b, [a]) -> SBV b
sbvFoldl ((SBV b, SList a) -> SBV (b, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV b
e SBV b -> SBV a -> SBV b
`f` SBV a
h, SList a
t)))

-- | Folding left with symbolic closures.
instance (SymVal env, SymVal a, SymVal b) => SFoldL (Closure (SBV env) (SBV b -> SBV a -> SBV b)) a b where
  foldl :: (SymVal a, SymVal b) =>
Closure (SBV env) (SBV b -> SBV a -> SBV b)
-> SBV b -> SList a -> SBV b
foldl cls :: Closure (SBV env) (SBV b -> SBV a -> SBV b)
cls@Closure{SBV env
closureEnv :: forall env a. Closure env a -> env
closureEnv :: SBV env
closureEnv, SBV env -> SBV b -> SBV a -> SBV b
closureFun :: forall env a. Closure env a -> env -> a
closureFun :: SBV env -> SBV b -> SBV a -> SBV b
closureFun} SBV b
base SList a
l
    | Just b
concResult <- Closure (SBV env) (SBV b -> SBV a -> SBV b)
-> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> Maybe b
forall func a b.
SFoldL func a b =>
func -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> Maybe b
concreteFoldl Closure (SBV env) (SBV b -> SBV a -> SBV b)
cls (SBV env -> SBV b -> SBV a -> SBV b
closureFun SBV env
closureEnv) SBV b
base SList a
l
    = b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
concResult
    | Bool
True
    = SBV (env, b, [a]) -> SBV b
sbvFoldl (SBV (env, b, [a]) -> SBV b) -> SBV (env, b, [a]) -> SBV b
forall a b. (a -> b) -> a -> b
$ (SBV env, SBV b, SList a) -> SBV (env, b, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
closureEnv, SBV b
base, SList a
l)
    where sbvFoldl :: SBV (env, b, [a]) -> SBV b
sbvFoldl = String
-> (SBV env -> SBV b -> SBV a -> SBV b)
-> (SBV (env, b, [a]) -> SBV b)
-> SBV (env, b, [a])
-> SBV b
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.closureFoldl" SBV env -> SBV b -> SBV a -> SBV b
closureFun
                   ((SBV (env, b, [a]) -> SBV b) -> SBV (env, b, [a]) -> SBV b)
-> (SBV (env, b, [a]) -> SBV b) -> SBV (env, b, [a]) -> SBV b
forall a b. (a -> b) -> a -> b
$ \SBV (env, b, [a])
envxs -> let (SBV env
cEnv, SBV b
e, SList a
xs) = SBV (env, b, [a]) -> (SBV env, SBV b, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple SBV (env, b, [a])
envxs
                                   (SBV a
h, SList a
t)        = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                               in SBool -> SBV b -> SBV b -> SBV b
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                      SBV b
e
                                      (SBV (env, b, [a]) -> SBV b
sbvFoldl ((SBV env, SBV b, SList a) -> SBV (env, b, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
cEnv, SBV env -> SBV b -> SBV a -> SBV b
closureFun SBV env
closureEnv SBV b
e SBV a
h, SList a
t)))

-- | A class of right foldable functions. In SBV, we make a distinction between closures and regular functions, and
-- we instantiate this class appropriately so it can handle both cases.
class (SymVal a, SymVal b) => SFoldR func a b | func -> a b where
  -- | @`foldr` f base s@ folds the from the right.
  --
  -- >>> foldr ((+) @SInteger) 0 [sEnum|1 .. 5|]
  -- 15 :: SInteger
  -- >>> foldr ((*) @SInteger) 1 [sEnum|1 .. 5|]
  -- 120 :: SInteger
  -- >>> foldr (\elt soFar -> soFar ++ [elt]) ([] :: SList Integer) [sEnum|1 .. 5|]
  -- [5,4,3,2,1] :: [SInteger]
  foldr :: func -> SBV b -> SList a -> SBV b

  -- | Handle the concrete case for folding left. Used internally only.
  concreteFoldr :: func -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> Maybe b
  concreteFoldr func
_ SBV a -> SBV b -> SBV b
f SBV b
sb SList a
sas
     | Just b
b <- SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just [a]
as <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
sas
     = b -> [a] -> Maybe b
go b
b [a]
as
     | Bool
True
     = Maybe b
forall a. Maybe a
Nothing
     where go :: b -> [a] -> Maybe b
go b
b []     = b -> Maybe b
forall a. a -> Maybe a
Just b
b
           go b
b (a
e:[a]
es) = case b -> [a] -> Maybe b
go b
b [a]
es of
                           Maybe b
Nothing  -> Maybe b
forall a. Maybe a
Nothing
                           Just b
res -> SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral (a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
e SBV a -> SBV b -> SBV b
`f` b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
res)

-- | Folding right with symbolic functions.
instance (SymVal a, SymVal b) => SFoldR (SBV a -> SBV b -> SBV b) a b where
  -- | @`foldr` f base s@ folds the sequence from the right.
  foldr :: (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SBV a -> SBV b -> SBV b
f SBV b
base SList a
l
    | Just b
concResult <- (SBV a -> SBV b -> SBV b)
-> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> Maybe b
forall func a b.
SFoldR func a b =>
func -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> Maybe b
concreteFoldr SBV a -> SBV b -> SBV b
f SBV a -> SBV b -> SBV b
f SBV b
base SList a
l
    = b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
concResult
    | Bool
True
    = SBV (b, [a]) -> SBV b
sbvFoldr (SBV (b, [a]) -> SBV b) -> SBV (b, [a]) -> SBV b
forall a b. (a -> b) -> a -> b
$ (SBV b, SList a) -> SBV (b, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV b
base, SList a
l)
    where sbvFoldr :: SBV (b, [a]) -> SBV b
sbvFoldr = String
-> (SBV (a, b) -> SBV b)
-> (SBV (b, [a]) -> SBV b)
-> SBV (b, [a])
-> SBV b
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.foldr" ((SBV a -> SBV b -> SBV b) -> (SBV a, SBV b) -> SBV b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SBV a -> SBV b -> SBV b
f ((SBV a, SBV b) -> SBV b)
-> (SBV (a, b) -> (SBV a, SBV b)) -> SBV (a, b) -> SBV b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV (a, b) -> (SBV a, SBV b)
forall tup a. Tuple tup a => SBV tup -> a
untuple)
                   ((SBV (b, [a]) -> SBV b) -> SBV (b, [a]) -> SBV b)
-> (SBV (b, [a]) -> SBV b) -> SBV (b, [a]) -> SBV b
forall a b. (a -> b) -> a -> b
$ \SBV (b, [a])
exs -> let (SBV b
e, SList a
xs) = SBV (b, [a]) -> (SBV b, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple SBV (b, [a])
exs
                                 (SBV a
h, SList a
t)  = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                             in SBool -> SBV b -> SBV b -> SBV b
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                    SBV b
e
                                    (SBV a
h SBV a -> SBV b -> SBV b
`f` SBV (b, [a]) -> SBV b
sbvFoldr ((SBV b, SList a) -> SBV (b, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV b
e, SList a
t)))

-- | Folding right with symbolic closures.
instance (SymVal env, SymVal a, SymVal b) => SFoldR (Closure (SBV env) (SBV a -> SBV b -> SBV b)) a b where
  foldr :: Closure (SBV env) (SBV a -> SBV b -> SBV b)
-> SBV b -> SList a -> SBV b
foldr cls :: Closure (SBV env) (SBV a -> SBV b -> SBV b)
cls@Closure{SBV env
closureEnv :: forall env a. Closure env a -> env
closureEnv :: SBV env
closureEnv, SBV env -> SBV a -> SBV b -> SBV b
closureFun :: forall env a. Closure env a -> env -> a
closureFun :: SBV env -> SBV a -> SBV b -> SBV b
closureFun} SBV b
base SList a
l
    | Just b
concResult <- Closure (SBV env) (SBV a -> SBV b -> SBV b)
-> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> Maybe b
forall func a b.
SFoldR func a b =>
func -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> Maybe b
concreteFoldr Closure (SBV env) (SBV a -> SBV b -> SBV b)
cls (SBV env -> SBV a -> SBV b -> SBV b
closureFun SBV env
closureEnv) SBV b
base SList a
l
    = b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
concResult
    | Bool
True
    = SBV (env, b, [a]) -> SBV b
sbvFoldr (SBV (env, b, [a]) -> SBV b) -> SBV (env, b, [a]) -> SBV b
forall a b. (a -> b) -> a -> b
$ (SBV env, SBV b, SList a) -> SBV (env, b, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
closureEnv, SBV b
base, SList a
l)
    where sbvFoldr :: SBV (env, b, [a]) -> SBV b
sbvFoldr = String
-> (SBV env -> SBV a -> SBV b -> SBV b)
-> (SBV (env, b, [a]) -> SBV b)
-> SBV (env, b, [a])
-> SBV b
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.closureFoldr" SBV env -> SBV a -> SBV b -> SBV b
closureFun
                   ((SBV (env, b, [a]) -> SBV b) -> SBV (env, b, [a]) -> SBV b)
-> (SBV (env, b, [a]) -> SBV b) -> SBV (env, b, [a]) -> SBV b
forall a b. (a -> b) -> a -> b
$ \SBV (env, b, [a])
envxs -> let (SBV env
cEnv, SBV b
e, SList a
xs) = SBV (env, b, [a]) -> (SBV env, SBV b, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple SBV (env, b, [a])
envxs
                                   (SBV a
h, SList a
t)        = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                               in SBool -> SBV b -> SBV b -> SBV b
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                      SBV b
e
                                      (SBV env -> SBV a -> SBV b -> SBV b
closureFun SBV env
closureEnv SBV a
h (SBV (env, b, [a]) -> SBV b
sbvFoldr ((SBV env, SBV b, SList a) -> SBV (env, b, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
cEnv, SBV b
e, SList a
t))))

-- | @`zip` xs ys@ zips the lists to give a list of pairs. The length of the final list is
-- the minumum of the lengths of the given lists.
--
-- >>> zip [sEnum|1..10 :: SInteger|] [sEnum|11..20 :: SInteger|]
-- [(1,11),(2,12),(3,13),(4,14),(5,15),(6,16),(7,17),(8,18),(9,19),(10,20)] :: [(SInteger, SInteger)]
-- >>> import Data.SBV.Tuple
-- >>> foldr ((+) @SInteger) 0 (map (\t -> t^._1+t^._2::SInteger) (zip [sEnum|1..10|] [sEnum|10, 9..1|]))
-- 110 :: SInteger
zip :: forall a b. (SymVal a, SymVal b) => SList a -> SList b -> SList (a, b)
zip :: forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList a
xs SList b
ys
 | Just [a]
xs' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
xs, Just [b]
ys' <- SList b -> Maybe [b]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList b
ys
 = [(a, b)] -> SBV [(a, b)]
forall a. SymVal a => a -> SBV a
literal ([(a, b)] -> SBV [(a, b)]) -> [(a, b)] -> SBV [(a, b)]
forall a b. (a -> b) -> a -> b
$ [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip [a]
xs' [b]
ys'
 | Bool
True
 = SList a -> SList b -> SBV [(a, b)]
def SList a
xs SList b
ys
 where def :: SList a -> SList b -> SBV [(a, b)]
def = String
-> (SList a -> SList b -> SBV [(a, b)])
-> SList a
-> SList b
-> SBV [(a, b)]
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"sbv.zip" ((SList a -> SList b -> SBV [(a, b)])
 -> SList a -> SList b -> SBV [(a, b)])
-> (SList a -> SList b -> SBV [(a, b)])
-> SList a
-> SList b
-> SBV [(a, b)]
forall a b. (a -> b) -> a -> b
$ \SList a
as SList b
bs -> SBool -> SBV [(a, b)] -> SBV [(a, b)] -> SBV [(a, b)]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
as SBool -> SBool -> SBool
.|| SList b -> SBool
forall a. SymVal a => SList a -> SBool
null SList b
bs) [] ((SBV a, SBV b) -> SBV (a, b)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
head SList a
as, SList b -> SBV b
forall a. SymVal a => SList a -> SBV a
head SList b
bs) SBV (a, b) -> SBV [(a, b)] -> SBV [(a, b)]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList b -> SBV [(a, b)]
def (SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
as) (SList b -> SList b
forall a. SymVal a => SList a -> SList a
tail SList b
bs))

-- | A class of function that we can zip-with. In SBV, we make a distinction between closures and regular
-- functions, and we instantiate this class appropriately so it can handle both cases.
class (SymVal a, SymVal b, SymVal c) => SZipWith func a b c | func -> a b c where
  -- | @`zipWith` f xs ys@ zips the lists to give a list of pairs, applying the function to each pair of elements.
  -- The length of the final list is the minumum of the lengths of the given lists.
   --
   -- >>> zipWith ((+) @SInteger) ([sEnum|1..10::SInteger|]) ([sEnum|11..20::SInteger|])
   -- [12,14,16,18,20,22,24,26,28,30] :: [SInteger]
   -- >>> foldr ((+) @SInteger) 0 (zipWith ((+) @SInteger) [sEnum|1..10 :: SInteger|] [sEnum|10, 9..1 :: SInteger|])
   -- 110 :: SInteger
  zipWith :: func -> SList a -> SList b -> SList c

  -- | Handle the concrete case of zipping. Used internally only.
  concreteZipWith :: func -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> Maybe [c]
  concreteZipWith func
_ SBV a -> SBV b -> SBV c
f SList a
sas SList b
sbs
   | Just [a]
as <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
sas, Just [b]
bs <- SList b -> Maybe [b]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList b
sbs
   = [a] -> [b] -> Maybe [c]
go [a]
as [b]
bs
   | Bool
True
   = Maybe [c]
forall a. Maybe a
Nothing
   where go :: [a] -> [b] -> Maybe [c]
go []     [b]
_      = [c] -> Maybe [c]
forall a. a -> Maybe a
Just []
         go [a]
_      []     = [c] -> Maybe [c]
forall a. a -> Maybe a
Just []
         go (a
a:[a]
as) (b
b:[b]
bs) = (:) (c -> [c] -> [c]) -> Maybe c -> Maybe ([c] -> [c])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV c -> Maybe c
forall a. SymVal a => SBV a -> Maybe a
unliteral (a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
a SBV a -> SBV b -> SBV c
`f` b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
b) Maybe ([c] -> [c]) -> Maybe [c] -> Maybe [c]
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [a] -> [b] -> Maybe [c]
go [a]
as [b]
bs

-- | Zipping with symbolic functions.
instance (SymVal a, SymVal b, SymVal c) => SZipWith (SBV a -> SBV b -> SBV c) a b c where
   -- | @`zipWith`@ zips two sequences with a symbolic function.
   zipWith :: (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c
zipWith SBV a -> SBV b -> SBV c
f SList a
xs SList b
ys
    | Just [c]
concResult <- (SBV a -> SBV b -> SBV c)
-> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> Maybe [c]
forall func a b c.
SZipWith func a b c =>
func
-> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> Maybe [c]
concreteZipWith SBV a -> SBV b -> SBV c
f SBV a -> SBV b -> SBV c
f SList a
xs SList b
ys
    = [c] -> SList c
forall a. SymVal a => a -> SBV a
literal [c]
concResult
    | Bool
True
    = SBV ([a], [b]) -> SList c
sbvZipWith (SBV ([a], [b]) -> SList c) -> SBV ([a], [b]) -> SList c
forall a b. (a -> b) -> a -> b
$ (SList a, SList b) -> SBV ([a], [b])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList a
xs, SList b
ys)
    where sbvZipWith :: SBV ([a], [b]) -> SList c
sbvZipWith = String
-> (SBV (a, b) -> SBV c)
-> (SBV ([a], [b]) -> SList c)
-> SBV ([a], [b])
-> SList c
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.zipWith" ((SBV a -> SBV b -> SBV c) -> (SBV a, SBV b) -> SBV c
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SBV a -> SBV b -> SBV c
f ((SBV a, SBV b) -> SBV c)
-> (SBV (a, b) -> (SBV a, SBV b)) -> SBV (a, b) -> SBV c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV (a, b) -> (SBV a, SBV b)
forall tup a. Tuple tup a => SBV tup -> a
untuple)
                     ((SBV ([a], [b]) -> SList c) -> SBV ([a], [b]) -> SList c)
-> (SBV ([a], [b]) -> SList c) -> SBV ([a], [b]) -> SList c
forall a b. (a -> b) -> a -> b
$ \SBV ([a], [b])
asbs -> let (SList a
as, SList b
bs) = SBV ([a], [b]) -> (SList a, SList b)
forall tup a. Tuple tup a => SBV tup -> a
untuple SBV ([a], [b])
asbs
                                in SBool -> SList c -> SList c -> SList c
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
as SBool -> SBool -> SBool
.|| SList b -> SBool
forall a. SymVal a => SList a -> SBool
null SList b
bs)
                                       []
                                       (SBV a -> SBV b -> SBV c
f (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
head SList a
as) (SList b -> SBV b
forall a. SymVal a => SList a -> SBV a
head SList b
bs) SBV c -> SList c -> SList c
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV ([a], [b]) -> SList c
sbvZipWith ((SList a, SList b) -> SBV ([a], [b])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
as, SList b -> SList b
forall a. SymVal a => SList a -> SList a
tail SList b
bs)))

-- | Zipping with closures.
instance (SymVal env, SymVal a, SymVal b, SymVal c) => SZipWith (Closure (SBV env) (SBV a -> SBV b -> SBV c)) a b c where
   zipWith :: Closure (SBV env) (SBV a -> SBV b -> SBV c)
-> SList a -> SList b -> SList c
zipWith cls :: Closure (SBV env) (SBV a -> SBV b -> SBV c)
cls@Closure{SBV env
closureEnv :: forall env a. Closure env a -> env
closureEnv :: SBV env
closureEnv, SBV env -> SBV a -> SBV b -> SBV c
closureFun :: forall env a. Closure env a -> env -> a
closureFun :: SBV env -> SBV a -> SBV b -> SBV c
closureFun} SList a
xs SList b
ys
    | Just [c]
concResult <- Closure (SBV env) (SBV a -> SBV b -> SBV c)
-> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> Maybe [c]
forall func a b c.
SZipWith func a b c =>
func
-> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> Maybe [c]
concreteZipWith Closure (SBV env) (SBV a -> SBV b -> SBV c)
cls (SBV env -> SBV a -> SBV b -> SBV c
closureFun SBV env
closureEnv) SList a
xs SList b
ys
    = [c] -> SList c
forall a. SymVal a => a -> SBV a
literal [c]
concResult
    | Bool
True
    = SBV (env, [a], [b]) -> SList c
sbvZipWith (SBV (env, [a], [b]) -> SList c) -> SBV (env, [a], [b]) -> SList c
forall a b. (a -> b) -> a -> b
$ (SBV env, SList a, SList b) -> SBV (env, [a], [b])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
closureEnv, SList a
xs, SList b
ys)
    where sbvZipWith :: SBV (env, [a], [b]) -> SList c
sbvZipWith = String
-> (SBV env -> SBV a -> SBV b -> SBV c)
-> (SBV (env, [a], [b]) -> SList c)
-> SBV (env, [a], [b])
-> SList c
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.closureZipWith" SBV env -> SBV a -> SBV b -> SBV c
closureFun
                     ((SBV (env, [a], [b]) -> SList c)
 -> SBV (env, [a], [b]) -> SList c)
-> (SBV (env, [a], [b]) -> SList c)
-> SBV (env, [a], [b])
-> SList c
forall a b. (a -> b) -> a -> b
$ \SBV (env, [a], [b])
envasbs -> let (SBV env
cEnv, SList a
as, SList b
bs) = SBV (env, [a], [b]) -> (SBV env, SList a, SList b)
forall tup a. Tuple tup a => SBV tup -> a
untuple SBV (env, [a], [b])
envasbs
                                   in SBool -> SList c -> SList c -> SList c
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
as SBool -> SBool -> SBool
.|| SList b -> SBool
forall a. SymVal a => SList a -> SBool
null SList b
bs)
                                          []
                                          (SBV env -> SBV a -> SBV b -> SBV c
closureFun SBV env
cEnv (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
head SList a
as) (SList b -> SBV b
forall a. SymVal a => SList a -> SBV a
head SList b
bs) SBV c -> SList c -> SList c
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV (env, [a], [b]) -> SList c
sbvZipWith ((SBV env, SList a, SList b) -> SBV (env, [a], [b])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
cEnv, SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
as, SList b -> SList b
forall a. SymVal a => SList a -> SList a
tail SList b
bs)))

-- | Concatenate list of lists.
--
-- >>> concat [[sEnum|1..3::SInteger|], [sEnum|4..7|], [sEnum|8..10|]]
-- [1,2,3,4,5,6,7,8,9,10] :: [SInteger]
concat :: forall a. SymVal a => SList [a] -> SList a
concat :: forall a. SymVal a => SList [a] -> SList a
concat = (SList a -> SList a -> SList a) -> SList a -> SList [a] -> SList a
forall func a b.
SFoldR func a b =>
func -> SBV b -> SList a -> SBV b
foldr SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
(++) []

-- | Check all elements satisfy the predicate.
--
-- >>> let isEven x = x `sMod` 2 .== 0
-- >>> all isEven [2, 4, 6, 8, 10 :: SInteger]
-- True
-- >>> all isEven [2, 4, 6, 1, 8, 10 :: SInteger]
-- False
all :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
all :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
all SBV a -> SBool
f = (SBV a -> SBool -> SBool) -> SBool -> SList a -> SBool
forall func a b.
SFoldR func a b =>
func -> SBV b -> SList a -> SBV b
foldr (SBool -> SBool -> SBool
(.&&) (SBool -> SBool -> SBool)
-> (SBV a -> SBool) -> SBV a -> SBool -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SBool
f) SBool
sTrue

-- | Check some element satisfies the predicate.
--
-- >>> let isEven x = x `sMod` 2 .== 0
-- >>> any (sNot . isEven) [2, 4, 6, 8, 10 :: SInteger]
-- False
-- >>> any isEven [2, 4, 6, 1, 8, 10 :: SInteger]
-- True
any :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
any :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
any SBV a -> SBool
f = (SBV a -> SBool -> SBool) -> SBool -> SList a -> SBool
forall func a b.
SFoldR func a b =>
func -> SBV b -> SList a -> SBV b
foldr (SBool -> SBool -> SBool
(.||) (SBool -> SBool -> SBool)
-> (SBV a -> SBool) -> SBV a -> SBool -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SBool
f) SBool
sFalse

-- | Conjunction of all the elements.
--
-- >>> and []
-- True
-- >>> prove $ \s -> and [s, sNot s] .== sFalse
-- Q.E.D.
and :: SList Bool -> SBool
and :: SList Bool -> SBool
and = (SBool -> SBool) -> SList Bool -> SBool
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
all SBool -> SBool
forall a. a -> a
id

-- | Disjunction of all the elements.
--
-- >>> or []
-- False
-- >>> prove $ \s -> or [s, sNot s]
-- Q.E.D.
or :: SList Bool -> SBool
or :: SList Bool -> SBool
or = (SBool -> SBool) -> SList Bool -> SBool
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
any SBool -> SBool
forall a. a -> a
id

-- | Replicate an element a given number of times.
--
-- >>> replicate 3 (2 :: SInteger) .== [2, 2, 2 :: SInteger]
-- True
-- >>> replicate (-2) (2 :: SInteger) .== ([] :: SList Integer)
-- True
replicate :: forall a. SymVal a => SInteger -> SBV a -> SList a
replicate :: forall a. SymVal a => SInteger -> SBV a -> SList a
replicate SInteger
c SBV a
e
 | Just Integer
c' <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
c, Just a
e' <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
e
 = [a] -> SBV [a]
forall a. SymVal a => a -> SBV a
literal (Integer -> a -> [a]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
c' a
e')
 | Bool
True
 = SInteger -> SBV a -> SBV [a]
def SInteger
c SBV a
e
 where def :: SInteger -> SBV a -> SBV [a]
def = String
-> (SInteger -> SBV a -> SBV [a]) -> SInteger -> SBV a -> SBV [a]
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"sbv.replicate" ((SInteger -> SBV a -> SBV [a]) -> SInteger -> SBV a -> SBV [a])
-> (SInteger -> SBV a -> SBV [a]) -> SInteger -> SBV a -> SBV [a]
forall a b. (a -> b) -> a -> b
$ \SInteger
count SBV a
elt -> SBool -> SBV [a] -> SBV [a] -> SBV [a]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
count SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) [] (SBV a
elt SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SBV a -> SBV [a]
def (SInteger
count SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SBV a
elt)

-- | inits of a list.
--
-- >>> inits ([] :: SList Integer)
-- [[]] :: [[SInteger]]
-- >>> inits [1,2,3,4::SInteger]
-- [[],[1],[1,2],[1,2,3],[1,2,3,4]] :: [[SInteger]]
inits :: forall a. SymVal a => SList a -> SList [a]
inits :: forall a. SymVal a => SList a -> SList [a]
inits SList a
xs
 | Just [a]
xs' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
xs
 = [[a]] -> SBV [[a]]
forall a. SymVal a => a -> SBV a
literal ([a] -> [[a]]
forall a. [a] -> [[a]]
L.inits [a]
xs')
 | Bool
True
 = SList a -> SBV [[a]]
def SList a
xs
 where def :: SList a -> SBV [[a]]
def = String -> (SList a -> SBV [[a]]) -> SList a -> SBV [[a]]
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"sbv.inits" ((SList a -> SBV [[a]]) -> SList a -> SBV [[a]])
-> (SList a -> SBV [[a]]) -> SList a -> SBV [[a]]
forall a b. (a -> b) -> a -> b
$ \SList a
l -> SBool -> SBV [[a]] -> SBV [[a]] -> SBV [[a]]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
l) [[]] (SList a -> SBV [[a]]
def (SList a -> SList a
forall a. SymVal a => SList a -> SList a
init SList a
l) SBV [[a]] -> SBV [[a]] -> SBV [[a]]
forall a. SymVal a => SList a -> SList a -> SList a
++ [Item (SBV [[a]])
SList a
l])

-- | tails of a list.
--
-- >>> tails ([] :: SList Integer)
-- [[]] :: [[SInteger]]
-- >>> tails [1,2,3,4::SInteger]
-- [[1,2,3,4],[2,3,4],[3,4],[4],[]] :: [[SInteger]]
tails :: forall a. SymVal a => SList a -> SList [a]
tails :: forall a. SymVal a => SList a -> SList [a]
tails SList a
xs
 | Just [a]
xs' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
xs
 = [[a]] -> SBV [[a]]
forall a. SymVal a => a -> SBV a
literal ([a] -> [[a]]
forall a. [a] -> [[a]]
L.tails [a]
xs')
 | Bool
True
 = SList a -> SBV [[a]]
def SList a
xs
 where def :: SList a -> SBV [[a]]
def = String -> (SList a -> SBV [[a]]) -> SList a -> SBV [[a]]
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"sbv.tails" ((SList a -> SBV [[a]]) -> SList a -> SBV [[a]])
-> (SList a -> SBV [[a]]) -> SList a -> SBV [[a]]
forall a b. (a -> b) -> a -> b
$ \SList a
l -> SBool -> SBV [[a]] -> SBV [[a]] -> SBV [[a]]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
l) [[]] (SList a
l SList a -> SBV [[a]] -> SBV [[a]]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SBV [[a]]
def (SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
l))

-- | Difference.
--
-- >>> [1, 2] \\ [3, 4 :: SInteger]
-- [1,2] :: [SInteger]
-- >>> [1, 2] \\ [2, 4 :: SInteger]
-- [1] :: [SInteger]
(\\) :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SList a
SList a
xs \\ :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SList a
\\ SList a
ys
 | Just [a]
xs' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
xs, Just [a]
ys' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
ys
 = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal ([a]
xs' [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
L.\\ [a]
ys')
 | Bool
True
 = SList a -> SList a -> SList a
def SList a
xs SList a
ys
 where def :: SList a -> SList a -> SList a
def = String
-> (SList a -> SList a -> SList a) -> SList a -> SList a -> SList a
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"sbv.diff" ((SList a -> SList a -> SList a) -> SList a -> SList a -> SList a)
-> (SList a -> SList a -> SList a) -> SList a -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ \SList a
x SList a
y -> SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
x)
                                                  []
                                                  (let (SBV a
h, SList a
t) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
x
                                                       r :: SList a
r      = SList a -> SList a -> SList a
def SList a
t SList a
y
                                                   in SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
h SBV a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList a
y) SList a
r (SBV a
h SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
r))
infix 5 \\  -- CPP: do not eat the final newline

-- | A class of filtering-like functions. In SBV, we make a distinction between closures and regular functions,
-- and we instantiate this class appropriately so it can handle both cases.
class SymVal a => SFilter func a | func -> a where
  -- | Filter a list via a predicate.
  --
  -- >>> filter (\(x :: SInteger) -> x `sMod` 2 .== 0) (literal [1 .. 10])
  -- [2,4,6,8,10] :: [SInteger]
  -- >>> filter (\(x :: SInteger) -> x `sMod` 2 ./= 0) (literal [1 .. 10])
  -- [1,3,5,7,9] :: [SInteger]
  filter :: func -> SList a -> SList a

  -- | Handle the concrete case of filtering. Used internally only.
  concreteFilter :: func -> (SBV a -> SBool) -> SList a -> Maybe [a]
  concreteFilter func
_ SBV a -> SBool
f SList a
sas
   | Just [a]
as <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
sas
   = case (a -> Maybe Bool) -> [a] -> [Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
P.map (SBool -> Maybe Bool
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBool -> Maybe Bool) -> (a -> SBool) -> a -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SBool
f (SBV a -> SBool) -> (a -> SBV a) -> a -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SBV a
forall a. SymVal a => a -> SBV a
literal) [a]
as of
        [Maybe Bool]
xs | (Maybe Bool -> Bool) -> [Maybe Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
P.any Maybe Bool -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe Bool]
xs -> Maybe [a]
forall a. Maybe a
Nothing
           | Bool
True               -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a
e | (Bool
True, a
e) <- [Bool] -> [a] -> [(Bool, a)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip ([Maybe Bool] -> [Bool]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Bool]
xs) [a]
as]
   | Bool
True
   = Maybe [a]
forall a. Maybe a
Nothing

  -- | Partition a symbolic list according to a predicate.
  --
  -- >>> partition (\(x :: SInteger) -> x `sMod` 2 .== 0) (literal [1 .. 10])
  -- ([2,4,6,8,10],[1,3,5,7,9]) :: ([SInteger], [SInteger])
  partition :: func -> SList a -> STuple [a] [a]

  -- | Handle the concrete case of partitioning. Used internally only.
  concretePartition :: func -> (SBV a -> SBool) -> SList a -> Maybe ([a], [a])
  concretePartition func
_ SBV a -> SBool
f SList a
l
    | Just [a]
l' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
    = case (a -> Maybe Bool) -> [a] -> [Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
P.map (SBool -> Maybe Bool
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBool -> Maybe Bool) -> (a -> SBool) -> a -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SBool
f (SBV a -> SBool) -> (a -> SBV a) -> a -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SBV a
forall a. SymVal a => a -> SBV a
literal) [a]
l' of
        [Maybe Bool]
xs | (Maybe Bool -> Bool) -> [Maybe Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
P.any Maybe Bool -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe Bool]
xs -> Maybe ([a], [a])
forall a. Maybe a
Nothing
           | Bool
True               -> let ([(Bool, a)]
ts, [(Bool, a)]
fs) = ((Bool, a) -> Bool) -> [(Bool, a)] -> ([(Bool, a)], [(Bool, a)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Bool, a) -> Bool
forall a b. (a, b) -> a
P.fst ([Bool] -> [a] -> [(Bool, a)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip ([Maybe Bool] -> [Bool]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Bool]
xs) [a]
l')
                                   in ([a], [a]) -> Maybe ([a], [a])
forall a. a -> Maybe a
Just (((Bool, a) -> a) -> [(Bool, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
P.map (Bool, a) -> a
forall a b. (a, b) -> b
P.snd [(Bool, a)]
ts, ((Bool, a) -> a) -> [(Bool, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
P.map (Bool, a) -> a
forall a b. (a, b) -> b
P.snd [(Bool, a)]
fs)
    | Bool
True
    = Maybe ([a], [a])
forall a. Maybe a
Nothing

  -- | Symbolic equivalent of @takeWhile@
  --
  -- >>> takeWhile (\(x :: SInteger) -> x `sMod` 2 .== 0) (literal [1..10])
  -- [] :: [SInteger]
  -- >>> takeWhile (\(x :: SInteger) -> x `sMod` 2 ./= 0) (literal [1..10])
  -- [1] :: [SInteger]
  takeWhile :: func -> SList a -> SList a

  -- | Handle the concrete case of take-while. Used internally only.
  concreteTakeWhile :: func -> (SBV a -> SBool) -> SList a -> Maybe [a]
  concreteTakeWhile func
_ SBV a -> SBool
f SList a
sas
   | Just [a]
as <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
sas
   = case (a -> Maybe Bool) -> [a] -> [Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
P.map (SBool -> Maybe Bool
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBool -> Maybe Bool) -> (a -> SBool) -> a -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SBool
f (SBV a -> SBool) -> (a -> SBV a) -> a -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SBV a
forall a. SymVal a => a -> SBV a
literal) [a]
as of
        [Maybe Bool]
xs | (Maybe Bool -> Bool) -> [Maybe Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
P.any Maybe Bool -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe Bool]
xs -> Maybe [a]
forall a. Maybe a
Nothing
           | Bool
True               -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just (((Bool, a) -> a) -> [(Bool, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
P.map (Bool, a) -> a
forall a b. (a, b) -> b
P.snd (((Bool, a) -> Bool) -> [(Bool, a)] -> [(Bool, a)]
forall a. (a -> Bool) -> [a] -> [a]
P.takeWhile (Bool, a) -> Bool
forall a b. (a, b) -> a
P.fst ([Bool] -> [a] -> [(Bool, a)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip ([Maybe Bool] -> [Bool]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Bool]
xs) [a]
as)))
   | Bool
True
   = Maybe [a]
forall a. Maybe a
Nothing

  -- | Symbolic equivalent of @dropWhile@
  -- >>> dropWhile (\(x :: SInteger) -> x `sMod` 2 .== 0) (literal [1..10])
  -- [1,2,3,4,5,6,7,8,9,10] :: [SInteger]
  -- >>> dropWhile (\(x :: SInteger) -> x `sMod` 2 ./= 0) (literal [1..10])
  -- [2,3,4,5,6,7,8,9,10] :: [SInteger]
  dropWhile :: func -> SList a -> SList a

  -- | Handle the concrete case of take-while. Used internally only.
  concreteDropWhile :: func -> (SBV a -> SBool) -> SList a -> Maybe [a]
  concreteDropWhile func
_ SBV a -> SBool
f SList a
sas
   | Just [a]
as <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
sas
   = case (a -> Maybe Bool) -> [a] -> [Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
P.map (SBool -> Maybe Bool
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBool -> Maybe Bool) -> (a -> SBool) -> a -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SBool
f (SBV a -> SBool) -> (a -> SBV a) -> a -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SBV a
forall a. SymVal a => a -> SBV a
literal) [a]
as of
        [Maybe Bool]
xs | (Maybe Bool -> Bool) -> [Maybe Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
P.any Maybe Bool -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe Bool]
xs -> Maybe [a]
forall a. Maybe a
Nothing
           | Bool
True               -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just (((Bool, a) -> a) -> [(Bool, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
P.map (Bool, a) -> a
forall a b. (a, b) -> b
P.snd (((Bool, a) -> Bool) -> [(Bool, a)] -> [(Bool, a)]
forall a. (a -> Bool) -> [a] -> [a]
P.dropWhile (Bool, a) -> Bool
forall a b. (a, b) -> a
P.fst ([Bool] -> [a] -> [(Bool, a)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip ([Maybe Bool] -> [Bool]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Bool]
xs) [a]
as)))
   | Bool
True
   = Maybe [a]
forall a. Maybe a
Nothing

-- | Filtering with symbolic functions.
instance SymVal a => SFilter (SBV a -> SBool) a where
  -- | @filter f xs@ filters the list with the given predicate.
  filter :: (SBV a -> SBool) -> SList a -> SList a
filter SBV a -> SBool
f SList a
l
    | Just [a]
concResult <- (SBV a -> SBool) -> (SBV a -> SBool) -> SList a -> Maybe [a]
forall func a.
SFilter func a =>
func -> (SBV a -> SBool) -> SList a -> Maybe [a]
concreteFilter SBV a -> SBool
f SBV a -> SBool
f SList a
l
    = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal [a]
concResult
    | Bool
True
    = SList a -> SList a
sbvFilter SList a
l
    where sbvFilter :: SList a -> SList a
sbvFilter = String
-> (SBV a -> SBool) -> (SList a -> SList a) -> SList a -> SList a
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.filter" SBV a -> SBool
f ((SList a -> SList a) -> SList a -> SList a)
-> (SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ \SList a
xs -> SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                                                []
                                                                (let (SBV a
h, SList a
t) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                                                                     r :: SList a
r      = SList a -> SList a
sbvFilter SList a
t
                                                                 in SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a -> SBool
f SBV a
h) (SBV a
h SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
r) SList a
r)

  -- | @partition f xs@ splits the list into two and returns those that satisfy the predicate in the
  -- first element, and those that don't in the second.
  partition :: (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition SBV a -> SBool
f SList a
l
    | Just ([a], [a])
concResult <- (SBV a -> SBool) -> (SBV a -> SBool) -> SList a -> Maybe ([a], [a])
forall func a.
SFilter func a =>
func -> (SBV a -> SBool) -> SList a -> Maybe ([a], [a])
concretePartition SBV a -> SBool
f SBV a -> SBool
f SList a
l
    = ([a], [a]) -> STuple [a] [a]
forall a. SymVal a => a -> SBV a
literal ([a], [a])
concResult
    | Bool
True
    = SList a -> STuple [a] [a]
sbvPartition SList a
l
    where sbvPartition :: SList a -> STuple [a] [a]
sbvPartition = String
-> (SBV a -> SBool)
-> (SList a -> STuple [a] [a])
-> SList a
-> STuple [a] [a]
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.partition" SBV a -> SBool
f ((SList a -> STuple [a] [a]) -> SList a -> STuple [a] [a])
-> (SList a -> STuple [a] [a]) -> SList a -> STuple [a] [a]
forall a b. (a -> b) -> a -> b
$ \SList a
xs -> SBool -> STuple [a] [a] -> STuple [a] [a] -> STuple [a] [a]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                                                      ((SList a, SList a) -> STuple [a] [a]
forall tup a. Tuple tup a => a -> SBV tup
tuple ([], []))
                                                                      (let (SBV a
h, SList a
t)   = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                                                                           (SList a
as, SList a
bs) = STuple [a] [a] -> (SList a, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple (STuple [a] [a] -> (SList a, SList a))
-> STuple [a] [a] -> (SList a, SList a)
forall a b. (a -> b) -> a -> b
$ SList a -> STuple [a] [a]
sbvPartition SList a
t
                                                                       in SBool -> STuple [a] [a] -> STuple [a] [a] -> STuple [a] [a]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a -> SBool
f SBV a
h)
                                                                              ((SList a, SList a) -> STuple [a] [a]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV a
h SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as, SList a
bs))
                                                                              ((SList a, SList a) -> STuple [a] [a]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList a
as, SBV a
h SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
bs)))

  -- | @takeWhile f xs@ takes the prefix of @xs@ that satisfy the predicate.
  takeWhile :: (SBV a -> SBool) -> SList a -> SList a
takeWhile SBV a -> SBool
f SList a
l
    | Just [a]
concResult <- (SBV a -> SBool) -> (SBV a -> SBool) -> SList a -> Maybe [a]
forall func a.
SFilter func a =>
func -> (SBV a -> SBool) -> SList a -> Maybe [a]
concreteTakeWhile SBV a -> SBool
f SBV a -> SBool
f SList a
l
    = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal [a]
concResult
    | Bool
True
    = SList a -> SList a
sbvTakeWhile SList a
l
    where sbvTakeWhile :: SList a -> SList a
sbvTakeWhile = String
-> (SBV a -> SBool) -> (SList a -> SList a) -> SList a -> SList a
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.takeWhile" SBV a -> SBool
f ((SList a -> SList a) -> SList a -> SList a)
-> (SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ \SList a
xs -> SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                                                      []
                                                                      (let (SBV a
h, SList a
t) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                                                                       in SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a -> SBool
f SBV a
h) (SBV a
h SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a
sbvTakeWhile SList a
t) [])

  -- | @dropWhile f xs@ drops the prefix of @xs@ that satisfy the predicate.
  dropWhile :: (SBV a -> SBool) -> SList a -> SList a
dropWhile SBV a -> SBool
f SList a
l
    | Just [a]
concResult <- (SBV a -> SBool) -> (SBV a -> SBool) -> SList a -> Maybe [a]
forall func a.
SFilter func a =>
func -> (SBV a -> SBool) -> SList a -> Maybe [a]
concreteDropWhile SBV a -> SBool
f SBV a -> SBool
f SList a
l
    = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal [a]
concResult
    | Bool
True
    = SList a -> SList a
sbvDropWhile SList a
l
    where sbvDropWhile :: SList a -> SList a
sbvDropWhile = String
-> (SBV a -> SBool) -> (SList a -> SList a) -> SList a -> SList a
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.dropWhile" SBV a -> SBool
f ((SList a -> SList a) -> SList a -> SList a)
-> (SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ \SList a
xs -> SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                                                      []
                                                                      (let (SBV a
h, SList a
t) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                                                                       in SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a -> SBool
f SBV a
h) (SList a -> SList a
sbvDropWhile SList a
t) SList a
xs)

-- | Filtering with closures.
instance (SymVal env, SymVal a) => SFilter (Closure (SBV env) (SBV a -> SBool)) a where
  filter :: Closure (SBV env) (SBV a -> SBool) -> SList a -> SList a
filter cls :: Closure (SBV env) (SBV a -> SBool)
cls@Closure{SBV env
closureEnv :: forall env a. Closure env a -> env
closureEnv :: SBV env
closureEnv, SBV env -> SBV a -> SBool
closureFun :: forall env a. Closure env a -> env -> a
closureFun :: SBV env -> SBV a -> SBool
closureFun} SList a
l
    | Just [a]
concResult <- Closure (SBV env) (SBV a -> SBool)
-> (SBV a -> SBool) -> SList a -> Maybe [a]
forall func a.
SFilter func a =>
func -> (SBV a -> SBool) -> SList a -> Maybe [a]
concreteFilter Closure (SBV env) (SBV a -> SBool)
cls (SBV env -> SBV a -> SBool
closureFun SBV env
closureEnv) SList a
l
    = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal [a]
concResult
    | Bool
True
    = SBV (env, [a]) -> SList a
sbvFilter ((SBV env, SList a) -> SBV (env, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
closureEnv, SList a
l))
    where sbvFilter :: SBV (env, [a]) -> SList a
sbvFilter = String
-> (SBV env -> SBV a -> SBool)
-> (SBV (env, [a]) -> SList a)
-> SBV (env, [a])
-> SList a
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.closureFilter" SBV env -> SBV a -> SBool
closureFun
                    ((SBV (env, [a]) -> SList a) -> SBV (env, [a]) -> SList a)
-> (SBV (env, [a]) -> SList a) -> SBV (env, [a]) -> SList a
forall a b. (a -> b) -> a -> b
$ \SBV (env, [a])
envxs -> let (SBV env
cEnv, SList a
xs) = SBV (env, [a]) -> (SBV env, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple SBV (env, [a])
envxs
                                    (SBV a
h, SList a
t)     = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                                    r :: SList a
r          = SBV (env, [a]) -> SList a
sbvFilter ((SBV env, SList a) -> SBV (env, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
cEnv, SList a
t))
                                in SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV env -> SBV a -> SBool
closureFun SBV env
cEnv SBV a
h) (SBV a
h SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
r) SList a
r

  partition :: Closure (SBV env) (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition cls :: Closure (SBV env) (SBV a -> SBool)
cls@Closure{SBV env
closureEnv :: forall env a. Closure env a -> env
closureEnv :: SBV env
closureEnv, SBV env -> SBV a -> SBool
closureFun :: forall env a. Closure env a -> env -> a
closureFun :: SBV env -> SBV a -> SBool
closureFun} SList a
l
    | Just ([a], [a])
concResult <- Closure (SBV env) (SBV a -> SBool)
-> (SBV a -> SBool) -> SList a -> Maybe ([a], [a])
forall func a.
SFilter func a =>
func -> (SBV a -> SBool) -> SList a -> Maybe ([a], [a])
concretePartition Closure (SBV env) (SBV a -> SBool)
cls (SBV env -> SBV a -> SBool
closureFun SBV env
closureEnv) SList a
l
    = ([a], [a]) -> STuple [a] [a]
forall a. SymVal a => a -> SBV a
literal ([a], [a])
concResult
    | Bool
True
    = SBV (env, [a]) -> STuple [a] [a]
sbvPartition ((SBV env, SList a) -> SBV (env, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
closureEnv, SList a
l))
    where sbvPartition :: SBV (env, [a]) -> STuple [a] [a]
sbvPartition = String
-> (SBV env -> SBV a -> SBool)
-> (SBV (env, [a]) -> STuple [a] [a])
-> SBV (env, [a])
-> STuple [a] [a]
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.closurePartition" SBV env -> SBV a -> SBool
closureFun
                       ((SBV (env, [a]) -> STuple [a] [a])
 -> SBV (env, [a]) -> STuple [a] [a])
-> (SBV (env, [a]) -> STuple [a] [a])
-> SBV (env, [a])
-> STuple [a] [a]
forall a b. (a -> b) -> a -> b
$ \SBV (env, [a])
envxs -> let (SBV env
cEnv, SList a
xs) = SBV (env, [a]) -> (SBV env, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple SBV (env, [a])
envxs
                                       (SBV a
h,    SList a
t)  = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                                       (SList a
as,   SList a
bs) = STuple [a] [a] -> (SList a, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple (STuple [a] [a] -> (SList a, SList a))
-> STuple [a] [a] -> (SList a, SList a)
forall a b. (a -> b) -> a -> b
$ SBV (env, [a]) -> STuple [a] [a]
sbvPartition ((SBV env, SList a) -> SBV (env, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
cEnv, SList a
t))
                                   in SBool -> STuple [a] [a] -> STuple [a] [a] -> STuple [a] [a]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV env -> SBV a -> SBool
closureFun SBV env
cEnv SBV a
h)
                                          ((SList a, SList a) -> STuple [a] [a]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV a
h SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as, SList a
bs))
                                          ((SList a, SList a) -> STuple [a] [a]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList a
as, SBV a
h SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
bs))

  takeWhile :: Closure (SBV env) (SBV a -> SBool) -> SList a -> SList a
takeWhile cls :: Closure (SBV env) (SBV a -> SBool)
cls@Closure{SBV env
closureEnv :: forall env a. Closure env a -> env
closureEnv :: SBV env
closureEnv, SBV env -> SBV a -> SBool
closureFun :: forall env a. Closure env a -> env -> a
closureFun :: SBV env -> SBV a -> SBool
closureFun} SList a
l
    | Just [a]
concResult <- Closure (SBV env) (SBV a -> SBool)
-> (SBV a -> SBool) -> SList a -> Maybe [a]
forall func a.
SFilter func a =>
func -> (SBV a -> SBool) -> SList a -> Maybe [a]
concreteTakeWhile Closure (SBV env) (SBV a -> SBool)
cls (SBV env -> SBV a -> SBool
closureFun SBV env
closureEnv) SList a
l
    = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal [a]
concResult
    | Bool
True
    = SBV (env, [a]) -> SList a
sbvTakeWhile ((SBV env, SList a) -> SBV (env, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
closureEnv, SList a
l))
    where sbvTakeWhile :: SBV (env, [a]) -> SList a
sbvTakeWhile = String
-> (SBV env -> SBV a -> SBool)
-> (SBV (env, [a]) -> SList a)
-> SBV (env, [a])
-> SList a
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.closureTakeWhile" SBV env -> SBV a -> SBool
closureFun
                       ((SBV (env, [a]) -> SList a) -> SBV (env, [a]) -> SList a)
-> (SBV (env, [a]) -> SList a) -> SBV (env, [a]) -> SList a
forall a b. (a -> b) -> a -> b
$ \SBV (env, [a])
envxs -> let (SBV env
cEnv, SList a
xs) = SBV (env, [a]) -> (SBV env, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple SBV (env, [a])
envxs
                                       (SBV a
h, SList a
t)     = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                                in SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV env -> SBV a -> SBool
closureFun SBV env
cEnv SBV a
h) (SBV a
h SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV (env, [a]) -> SList a
sbvTakeWhile ((SBV env, SList a) -> SBV (env, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
cEnv, SList a
t))) []

  dropWhile :: Closure (SBV env) (SBV a -> SBool) -> SList a -> SList a
dropWhile cls :: Closure (SBV env) (SBV a -> SBool)
cls@Closure{SBV env
closureEnv :: forall env a. Closure env a -> env
closureEnv :: SBV env
closureEnv, SBV env -> SBV a -> SBool
closureFun :: forall env a. Closure env a -> env -> a
closureFun :: SBV env -> SBV a -> SBool
closureFun} SList a
l
    | Just [a]
concResult <- Closure (SBV env) (SBV a -> SBool)
-> (SBV a -> SBool) -> SList a -> Maybe [a]
forall func a.
SFilter func a =>
func -> (SBV a -> SBool) -> SList a -> Maybe [a]
concreteDropWhile Closure (SBV env) (SBV a -> SBool)
cls (SBV env -> SBV a -> SBool
closureFun SBV env
closureEnv) SList a
l
    = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal [a]
concResult
    | Bool
True
    = SBV (env, [a]) -> SList a
sbvDropWhile ((SBV env, SList a) -> SBV (env, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
closureEnv, SList a
l))
    where sbvDropWhile :: SBV (env, [a]) -> SList a
sbvDropWhile = String
-> (SBV env -> SBV a -> SBool)
-> (SBV (env, [a]) -> SList a)
-> SBV (env, [a])
-> SList a
forall a b f.
(SMTDefinable (a -> SBV b), Lambda Symbolic f,
 Lambda Symbolic (a -> SBV b), HasKind b, HasKind f, Typeable a,
 Typeable b, Typeable f) =>
String -> f -> (a -> SBV b) -> a -> SBV b
smtHOFunction String
"sbv.closureDropWhile" SBV env -> SBV a -> SBool
closureFun
                       ((SBV (env, [a]) -> SList a) -> SBV (env, [a]) -> SList a)
-> (SBV (env, [a]) -> SList a) -> SBV (env, [a]) -> SList a
forall a b. (a -> b) -> a -> b
$ \SBV (env, [a])
envxs -> let (SBV env
cEnv, SList a
xs) = SBV (env, [a]) -> (SBV env, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple SBV (env, [a])
envxs
                                       (SBV a
h, SList a
t)     = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
xs
                                in SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV env -> SBV a -> SBool
closureFun SBV env
cEnv SBV a
h) (SBV (env, [a]) -> SList a
sbvDropWhile ((SBV env, SList a) -> SBV (env, [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV env
cEnv, SList a
t))) SList a
xs

-- | @`sum` s@. Sum the given sequence.
--
-- >>> sum [sEnum|1 .. 10::SInteger|]
-- 55 :: SInteger
sum :: forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum :: forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum = (SBV a -> SBV a -> SBV a) -> SBV a -> SList a -> SBV a
forall func a b.
SFoldR func a b =>
func -> SBV b -> SList a -> SBV b
foldr (forall a. Num a => a -> a -> a
(+) @(SBV a)) SBV a
0

-- | @`product` s@. Multiply out the given sequence.
--
-- >>> product [sEnum|1 .. 10::SInteger|]
-- 3628800 :: SInteger
product :: forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
product :: forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
product = (SBV a -> SBV a -> SBV a) -> SBV a -> SList a -> SBV a
forall func a b.
SFoldR func a b =>
func -> SBV b -> SList a -> SBV b
foldr (forall a. Num a => a -> a -> a
(*) @(SBV a)) SBV a
1

-- | A class of symbolic aware enumerations. This is similar to Haskell's @Enum@ class,
-- except some of the methods are generalized to work with symbolic values. Together
-- with the 'Data.SBV.sEnum' quasiquoter, you can write symbolic arithmetic progressions,
-- such as:
--
-- >>> [sEnum| 5, 7 .. 16::SInteger|]
-- [5,7,9,11,13,15] :: [SInteger]
-- >>> [sEnum| 4 ..|] :: SList (WordN 4)
-- [4,5,6,7,8,9,10,11,12,13,14,15] :: [SWord 4]
-- >>> [sEnum| 9, 12 ..|] :: SList (IntN 4)
-- [-7,-4,-1,2,5] :: [SInt 4]
class EnumSymbolic a where
   -- | @`succ`@, same as in the @Enum@ class
   succ :: SBV a -> SBV a

   -- | @`pred`@, same as in the @Enum@ class
   pred :: SBV a -> SBV a

   -- | @`toEnum`@, same as in the @Enum@ class, except it takes an 'SInteger'
   toEnum :: SInteger -> SBV a

   -- | @`fromEnum`@, same as in the @Enum@ class, except it returns an 'SInteger'
   fromEnum :: SBV a -> SInteger

   -- | @`enumFrom` m@. Symbolic version of @[m ..]@
   enumFrom :: SBV a -> SList a

   -- | @`enumFromThen` m@. Symbolic version of @[m, m' ..]@
   enumFromThen :: SBV a -> SBV a -> SList a

   -- | @`enumFromTo` m n@. Symbolic version of @[m .. n]@
   enumFromTo :: SymVal a => SBV a -> SBV a -> SList a

   -- | @`enumFromThenTo` m n@. Symbolic version of @[m, m' .. n]@
   enumFromThenTo :: SymVal a => SBV a -> SBV a -> SBV a -> SList a

-- | 'EnumSymbolic' instance for words
instance {-# OVERLAPPABLE #-} (SymVal a, Bounded a, Integral a, Num a, Num (SBV a)) => EnumSymbolic a where
  succ :: SBV a -> SBV a
succ = String -> (SBV a -> SBV a) -> SBV a -> SBV a
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.succ" (\SBV a
x -> SBool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
x SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
forall a. Bounded a => a
maxBound) (String -> (SBV a -> SBool) -> SBV a
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"EnumSymbolic.succ.maxBound" (SBool -> SBV a -> SBool
forall a b. a -> b -> a
const SBool
sTrue)) (SBV a
xSBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+SBV a
1))
  pred :: SBV a -> SBV a
pred = String -> (SBV a -> SBV a) -> SBV a -> SBV a
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.pred" (\SBV a
x -> SBool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
x SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
forall a. Bounded a => a
minBound) (String -> (SBV a -> SBool) -> SBV a
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"EnumSymbolic.pred.minBound" (SBool -> SBV a -> SBool
forall a b. a -> b -> a
const SBool
sTrue)) (SBV a
xSBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
-SBV a
1))

  toEnum :: SInteger -> SBV a
toEnum = String -> (SInteger -> SBV a) -> SInteger -> SBV a
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.toEnum" ((SInteger -> SBV a) -> SInteger -> SBV a)
-> (SInteger -> SBV a) -> SInteger -> SBV a
forall a b. (a -> b) -> a -> b
$ \SInteger
x ->
                         SBool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (forall a. Bounded a => a
minBound @(SBV a))) (String -> (SBV a -> SBool) -> SBV a
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"EnumSymbolic.toEnum.<minBound" (SBool -> SBV a -> SBool
forall a b. a -> b -> a
const SBool
sTrue))
                       (SBV a -> SBV a) -> SBV a -> SBV a
forall a b. (a -> b) -> a -> b
$ SBool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (forall a. Bounded a => a
maxBound @(SBV a))) (String -> (SBV a -> SBool) -> SBV a
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"EnumSymbolic.toEnum.>maxBound" (SBool -> SBV a -> SBool
forall a b. a -> b -> a
const SBool
sTrue))
                       (SBV a -> SBV a) -> SBV a -> SBV a
forall a b. (a -> b) -> a -> b
$ SInteger -> SBV a
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SInteger
x

  fromEnum :: SBV a -> SInteger
fromEnum = SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral

  enumFrom :: SBV a -> SList a
enumFrom SBV a
n   = (SInteger -> SBV a) -> SList Integer -> SList a
forall func a b. SMap func a b => func -> SList a -> SList b
map SInteger -> SBV a
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (forall a. (EnumSymbolic a, SymVal a) => SBV a -> SBV a -> SList a
enumFromTo @Integer (SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV a
n) (SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (forall a. Bounded a => a
maxBound @(SBV a))))
  enumFromThen :: SBV a -> SBV a -> SList a
enumFromThen = String -> (SBV a -> SBV a -> SList a) -> SBV a -> SBV a -> SList a
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.enumFromThen" ((SBV a -> SBV a -> SList a) -> SBV a -> SBV a -> SList a)
-> (SBV a -> SBV a -> SList a) -> SBV a -> SBV a -> SList a
forall a b. (a -> b) -> a -> b
$ \SBV a
n1 SBV a
n2 ->
                             let i_n1, i_n2 :: SInteger
                                 i_n1 :: SInteger
i_n1 = SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV a
n1
                                 i_n2 :: SInteger
i_n2 = SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV a
n2
                             in (SInteger -> SBV a) -> SList Integer -> SList a
forall func a b. SMap func a b => func -> SList a -> SList b
map SInteger -> SBV a
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i_n2 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
i_n1)
                                                       (SInteger -> SInteger -> SInteger -> SList Integer
forall a.
(EnumSymbolic a, SymVal a) =>
SBV a -> SBV a -> SBV a -> SList a
enumFromThenTo SInteger
i_n1 SInteger
i_n2 (SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (forall a. Bounded a => a
maxBound @(SBV a))))
                                                       (SInteger -> SInteger -> SInteger -> SList Integer
forall a.
(EnumSymbolic a, SymVal a) =>
SBV a -> SBV a -> SBV a -> SList a
enumFromThenTo SInteger
i_n1 SInteger
i_n2 (SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (forall a. Bounded a => a
minBound @(SBV a)))))

  enumFromTo :: SymVal a => SBV a -> SBV a -> SList a
enumFromTo     SBV a
n SBV a
m   = (SInteger -> SBV a) -> SList Integer -> SList a
forall func a b. SMap func a b => func -> SList a -> SList b
map SInteger -> SBV a
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (forall a. (EnumSymbolic a, SymVal a) => SBV a -> SBV a -> SList a
enumFromTo     @Integer (SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV a
n) (SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV a
m))
  enumFromThenTo :: SymVal a => SBV a -> SBV a -> SBV a -> SList a
enumFromThenTo SBV a
n SBV a
m SBV a
t = (SInteger -> SBV a) -> SList Integer -> SList a
forall func a b. SMap func a b => func -> SList a -> SList b
map SInteger -> SBV a
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (forall a.
(EnumSymbolic a, SymVal a) =>
SBV a -> SBV a -> SBV a -> SList a
enumFromThenTo @Integer (SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV a
n) (SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV a
m) (SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV a
t))

-- | 'EnumSymbolic' instance for integer. NB. The above definition goes thru integers, hence we need to define this explicitly.
instance {-# OVERLAPPING #-} EnumSymbolic Integer where
   succ :: SInteger -> SInteger
succ SInteger
x = SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1
   pred :: SInteger -> SInteger
pred SInteger
x = SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1

   toEnum :: SInteger -> SInteger
toEnum   = SInteger -> SInteger
forall a. a -> a
id
   fromEnum :: SInteger -> SInteger
fromEnum = SInteger -> SInteger
forall a. a -> a
id

   enumFrom :: SInteger -> SList Integer
enumFrom   SInteger
n = SInteger -> SInteger -> SList Integer
forall a. EnumSymbolic a => SBV a -> SBV a -> SList a
enumFromThen   SInteger
n (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
   enumFromTo :: SymVal Integer => SInteger -> SInteger -> SList Integer
enumFromTo SInteger
n = SInteger -> SInteger -> SInteger -> SList Integer
forall a.
(EnumSymbolic a, SymVal a) =>
SBV a -> SBV a -> SBV a -> SList a
enumFromThenTo SInteger
n (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)

   enumFromThen :: SInteger -> SInteger -> SList Integer
enumFromThen SInteger
x SInteger
y = SInteger -> SInteger -> SList Integer
go SInteger
x (SInteger
ySInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
x)
     where go :: SInteger -> SInteger -> SList Integer
go = String
-> (SInteger -> SInteger -> SList Integer)
-> SInteger
-> SInteger
-> SList Integer
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.Integer.enumFromThen" ((SInteger -> SInteger -> SList Integer)
 -> SInteger -> SInteger -> SList Integer)
-> (SInteger -> SInteger -> SList Integer)
-> SInteger
-> SInteger
-> SList Integer
forall a b. (a -> b) -> a -> b
$ \SInteger
start SInteger
delta -> SInteger
start SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SInteger -> SList Integer
go (SInteger
startSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
delta) SInteger
delta

   enumFromThenTo :: SymVal Integer => SInteger -> SInteger -> SInteger -> SList Integer
enumFromThenTo SInteger
x SInteger
y SInteger
z = SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
delta SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0) (SInteger -> SInteger -> SInteger -> SList Integer
up SInteger
x SInteger
delta SInteger
z) (SInteger -> SInteger -> SInteger -> SList Integer
down SInteger
x SInteger
delta SInteger
z)
     where delta :: SInteger
delta = SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
x

           up, down :: SInteger -> SInteger -> SInteger -> SList Integer
           up :: SInteger -> SInteger -> SInteger -> SList Integer
up    = String
-> (SInteger -> SInteger -> SInteger -> SList Integer)
-> SInteger
-> SInteger
-> SInteger
-> SList Integer
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.Integer.enumFromThenTo.up"   ((SInteger -> SInteger -> SInteger -> SList Integer)
 -> SInteger -> SInteger -> SInteger -> SList Integer)
-> (SInteger -> SInteger -> SInteger -> SList Integer)
-> SInteger
-> SInteger
-> SInteger
-> SList Integer
forall a b. (a -> b) -> a -> b
$ \SInteger
start SInteger
d SInteger
end -> SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
start SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
end) [] (SInteger
start SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SInteger -> SInteger -> SList Integer
up   (SInteger
start SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
d) SInteger
d SInteger
end)
           down :: SInteger -> SInteger -> SInteger -> SList Integer
down  = String
-> (SInteger -> SInteger -> SInteger -> SList Integer)
-> SInteger
-> SInteger
-> SInteger
-> SList Integer
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.Integer.enumFromThenTo.down" ((SInteger -> SInteger -> SInteger -> SList Integer)
 -> SInteger -> SInteger -> SInteger -> SList Integer)
-> (SInteger -> SInteger -> SInteger -> SList Integer)
-> SInteger
-> SInteger
-> SInteger
-> SList Integer
forall a b. (a -> b) -> a -> b
$ \SInteger
start SInteger
d SInteger
end -> SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
start SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
end) [] (SInteger
start SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SInteger -> SInteger -> SList Integer
down (SInteger
start SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
d) SInteger
d SInteger
end)

-- | 'EnumSymbolic instance for 'Float'. Note that the termination requirement as defined by the Haskell standard for floats state:
--      > For Float and Double, the semantics of the enumFrom family is given by the rules for Int above,
--      > except that the list terminates when the elements become greater than @e3 + i/2@ for positive increment @i@,
--      > or when they become less than @e3 + i/2@ for negative @i@.
instance {-# OVERLAPPING #-} EnumSymbolic Float where
   succ :: SBV Float -> SBV Float
succ SBV Float
x = SBV Float
x SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+ SBV Float
1
   pred :: SBV Float -> SBV Float
pred SBV Float
x = SBV Float
x SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
- SBV Float
1

   toEnum :: SInteger -> SBV Float
toEnum   = SInteger -> SBV Float
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral
   fromEnum :: SBV Float -> SInteger
fromEnum = SRoundingMode -> SBV Float -> SInteger
forall a.
IEEEFloatConvertible a =>
SRoundingMode -> SBV Float -> SBV a
fromSFloat SRoundingMode
sRTZ

   enumFrom :: SBV Float -> SList Float
enumFrom   SBV Float
n = SBV Float -> SBV Float -> SList Float
forall a. EnumSymbolic a => SBV a -> SBV a -> SList a
enumFromThen   SBV Float
n (SBV Float
nSBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+SBV Float
1)
   enumFromTo :: SymVal Float => SBV Float -> SBV Float -> SList Float
enumFromTo SBV Float
n = SBV Float -> SBV Float -> SBV Float -> SList Float
forall a.
(EnumSymbolic a, SymVal a) =>
SBV a -> SBV a -> SBV a -> SList a
enumFromThenTo SBV Float
n (SBV Float
nSBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+SBV Float
1)

   enumFromThen :: SBV Float -> SBV Float -> SList Float
enumFromThen SBV Float
x SBV Float
y = SBV Float -> SBV Float -> SBV Float -> SList Float
go SBV Float
0 SBV Float
x (SBV Float
ySBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
-SBV Float
x)
     where go :: SBV Float -> SBV Float -> SBV Float -> SList Float
go = String
-> (SBV Float -> SBV Float -> SBV Float -> SList Float)
-> SBV Float
-> SBV Float
-> SBV Float
-> SList Float
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.Float.enumFromThen" ((SBV Float -> SBV Float -> SBV Float -> SList Float)
 -> SBV Float -> SBV Float -> SBV Float -> SList Float)
-> (SBV Float -> SBV Float -> SBV Float -> SList Float)
-> SBV Float
-> SBV Float
-> SBV Float
-> SList Float
forall a b. (a -> b) -> a -> b
$ \SBV Float
k SBV Float
n SBV Float
d -> (SBV Float
n SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+ SBV Float
k SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
* SBV Float
d) SBV Float -> SList Float -> SList Float
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV Float -> SBV Float -> SBV Float -> SList Float
go (SBV Float
kSBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+SBV Float
1) SBV Float
n SBV Float
d

   enumFromThenTo :: SymVal Float => SBV Float -> SBV Float -> SBV Float -> SList Float
enumFromThenTo SBV Float
x SBV Float
y SBV Float
zIn = SBool -> SList Float -> SList Float -> SList Float
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Float
delta SBV Float -> SBV Float -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Float
0) (SBV Float -> SBV Float -> SBV Float -> SBV Float -> SList Float
up SBV Float
0 SBV Float
x SBV Float
delta SBV Float
z) (SBV Float -> SBV Float -> SBV Float -> SBV Float -> SList Float
down SBV Float
0 SBV Float
x SBV Float
delta SBV Float
z)
     where delta, z :: SFloat
           delta :: SBV Float
delta = SBV Float
y SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
- SBV Float
x
           z :: SBV Float
z     = SBV Float
zIn SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+ SBV Float
delta SBV Float -> SBV Float -> SBV Float
forall a. Fractional a => a -> a -> a
/ SBV Float
2

           up, down :: SFloat -> SFloat -> SFloat -> SFloat -> SList Float
           up :: SBV Float -> SBV Float -> SBV Float -> SBV Float -> SList Float
up    = String
-> (SBV Float
    -> SBV Float -> SBV Float -> SBV Float -> SList Float)
-> SBV Float
-> SBV Float
-> SBV Float
-> SBV Float
-> SList Float
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.Float.enumFromThenTo.up"   ((SBV Float -> SBV Float -> SBV Float -> SBV Float -> SList Float)
 -> SBV Float -> SBV Float -> SBV Float -> SBV Float -> SList Float)
-> (SBV Float
    -> SBV Float -> SBV Float -> SBV Float -> SList Float)
-> SBV Float
-> SBV Float
-> SBV Float
-> SBV Float
-> SList Float
forall a b. (a -> b) -> a -> b
$ \SBV Float
k SBV Float
n SBV Float
d SBV Float
end -> let c :: SBV Float
c = SBV Float
n SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+ SBV Float
k SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
* SBV Float
d in SBool -> SList Float -> SList Float -> SList Float
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Float
c SBV Float -> SBV Float -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Float
end) [] (SBV Float
c SBV Float -> SList Float -> SList Float
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV Float -> SBV Float -> SBV Float -> SBV Float -> SList Float
up   (SBV Float
kSBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+SBV Float
1) SBV Float
n SBV Float
d SBV Float
end)
           down :: SBV Float -> SBV Float -> SBV Float -> SBV Float -> SList Float
down  = String
-> (SBV Float
    -> SBV Float -> SBV Float -> SBV Float -> SList Float)
-> SBV Float
-> SBV Float
-> SBV Float
-> SBV Float
-> SList Float
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.Float.enumFromThenTo.down" ((SBV Float -> SBV Float -> SBV Float -> SBV Float -> SList Float)
 -> SBV Float -> SBV Float -> SBV Float -> SBV Float -> SList Float)
-> (SBV Float
    -> SBV Float -> SBV Float -> SBV Float -> SList Float)
-> SBV Float
-> SBV Float
-> SBV Float
-> SBV Float
-> SList Float
forall a b. (a -> b) -> a -> b
$ \SBV Float
k SBV Float
n SBV Float
d SBV Float
end -> let c :: SBV Float
c = SBV Float
n SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+ SBV Float
k SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
* SBV Float
d in SBool -> SList Float -> SList Float -> SList Float
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Float
c SBV Float -> SBV Float -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Float
end) [] (SBV Float
c SBV Float -> SList Float -> SList Float
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV Float -> SBV Float -> SBV Float -> SBV Float -> SList Float
down (SBV Float
kSBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+SBV Float
1) SBV Float
n SBV Float
d SBV Float
end)

-- | 'EnumSymbolic instance for 'Double'
instance {-# OVERLAPPING #-} EnumSymbolic Double where
   succ :: SBV Double -> SBV Double
succ SBV Double
x = SBV Double
x SBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
+ SBV Double
1
   pred :: SBV Double -> SBV Double
pred SBV Double
x = SBV Double
x SBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
- SBV Double
1

   toEnum :: SInteger -> SBV Double
toEnum   = SInteger -> SBV Double
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral
   fromEnum :: SBV Double -> SInteger
fromEnum = SRoundingMode -> SBV Double -> SInteger
forall a.
IEEEFloatConvertible a =>
SRoundingMode -> SBV Double -> SBV a
fromSDouble SRoundingMode
sRTZ

   enumFrom :: SBV Double -> SList Double
enumFrom   SBV Double
n = SBV Double -> SBV Double -> SList Double
forall a. EnumSymbolic a => SBV a -> SBV a -> SList a
enumFromThen   SBV Double
n (SBV Double
nSBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
+SBV Double
1)
   enumFromTo :: SymVal Double => SBV Double -> SBV Double -> SList Double
enumFromTo SBV Double
n = SBV Double -> SBV Double -> SBV Double -> SList Double
forall a.
(EnumSymbolic a, SymVal a) =>
SBV a -> SBV a -> SBV a -> SList a
enumFromThenTo SBV Double
n (SBV Double
nSBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
+SBV Double
1)

   enumFromThen :: SBV Double -> SBV Double -> SList Double
enumFromThen SBV Double
x SBV Double
y = SBV Double -> SBV Double -> SBV Double -> SList Double
go SBV Double
0 SBV Double
x (SBV Double
ySBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
-SBV Double
x)
     where go :: SBV Double -> SBV Double -> SBV Double -> SList Double
go = String
-> (SBV Double -> SBV Double -> SBV Double -> SList Double)
-> SBV Double
-> SBV Double
-> SBV Double
-> SList Double
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.Double.enumFromThen" ((SBV Double -> SBV Double -> SBV Double -> SList Double)
 -> SBV Double -> SBV Double -> SBV Double -> SList Double)
-> (SBV Double -> SBV Double -> SBV Double -> SList Double)
-> SBV Double
-> SBV Double
-> SBV Double
-> SList Double
forall a b. (a -> b) -> a -> b
$ \SBV Double
k SBV Double
n SBV Double
d -> (SBV Double
n SBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
+ SBV Double
k SBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
* SBV Double
d) SBV Double -> SList Double -> SList Double
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV Double -> SBV Double -> SBV Double -> SList Double
go (SBV Double
kSBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
+SBV Double
1) SBV Double
n SBV Double
d

   enumFromThenTo :: SymVal Double =>
SBV Double -> SBV Double -> SBV Double -> SList Double
enumFromThenTo SBV Double
x SBV Double
y SBV Double
zIn = SBool -> SList Double -> SList Double -> SList Double
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Double
delta SBV Double -> SBV Double -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Double
0) (SBV Double
-> SBV Double -> SBV Double -> SBV Double -> SList Double
up SBV Double
0 SBV Double
x SBV Double
delta SBV Double
z) (SBV Double
-> SBV Double -> SBV Double -> SBV Double -> SList Double
down SBV Double
0 SBV Double
x SBV Double
delta SBV Double
z)
     where delta, z :: SDouble
           delta :: SBV Double
delta = SBV Double
y SBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
- SBV Double
x
           z :: SBV Double
z     = SBV Double
zIn SBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
+ SBV Double
delta SBV Double -> SBV Double -> SBV Double
forall a. Fractional a => a -> a -> a
/ SBV Double
2

           up, down :: SDouble -> SDouble -> SDouble -> SDouble -> SList Double
           up :: SBV Double
-> SBV Double -> SBV Double -> SBV Double -> SList Double
up    = String
-> (SBV Double
    -> SBV Double -> SBV Double -> SBV Double -> SList Double)
-> SBV Double
-> SBV Double
-> SBV Double
-> SBV Double
-> SList Double
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.Double.enumFromThenTo.up"   ((SBV Double
  -> SBV Double -> SBV Double -> SBV Double -> SList Double)
 -> SBV Double
 -> SBV Double
 -> SBV Double
 -> SBV Double
 -> SList Double)
-> (SBV Double
    -> SBV Double -> SBV Double -> SBV Double -> SList Double)
-> SBV Double
-> SBV Double
-> SBV Double
-> SBV Double
-> SList Double
forall a b. (a -> b) -> a -> b
$ \SBV Double
k SBV Double
n SBV Double
d SBV Double
end -> let c :: SBV Double
c = SBV Double
n SBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
+ SBV Double
k SBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
* SBV Double
d in SBool -> SList Double -> SList Double -> SList Double
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Double
c SBV Double -> SBV Double -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Double
end) [] (SBV Double
c SBV Double -> SList Double -> SList Double
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV Double
-> SBV Double -> SBV Double -> SBV Double -> SList Double
up   (SBV Double
kSBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
+SBV Double
1) SBV Double
n SBV Double
d SBV Double
end)
           down :: SBV Double
-> SBV Double -> SBV Double -> SBV Double -> SList Double
down  = String
-> (SBV Double
    -> SBV Double -> SBV Double -> SBV Double -> SList Double)
-> SBV Double
-> SBV Double
-> SBV Double
-> SBV Double
-> SList Double
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.Double.enumFromThenTo.down" ((SBV Double
  -> SBV Double -> SBV Double -> SBV Double -> SList Double)
 -> SBV Double
 -> SBV Double
 -> SBV Double
 -> SBV Double
 -> SList Double)
-> (SBV Double
    -> SBV Double -> SBV Double -> SBV Double -> SList Double)
-> SBV Double
-> SBV Double
-> SBV Double
-> SBV Double
-> SList Double
forall a b. (a -> b) -> a -> b
$ \SBV Double
k SBV Double
n SBV Double
d SBV Double
end -> let c :: SBV Double
c = SBV Double
n SBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
+ SBV Double
k SBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
* SBV Double
d in SBool -> SList Double -> SList Double -> SList Double
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Double
c SBV Double -> SBV Double -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Double
end) [] (SBV Double
c SBV Double -> SList Double -> SList Double
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV Double
-> SBV Double -> SBV Double -> SBV Double -> SList Double
down (SBV Double
kSBV Double -> SBV Double -> SBV Double
forall a. Num a => a -> a -> a
+SBV Double
1) SBV Double
n SBV Double
d SBV Double
end)

-- | 'EnumSymbolic instance for arbitrary floats
instance {-# OVERLAPPING #-} ValidFloat eb sb => EnumSymbolic (FloatingPoint eb sb) where
   succ :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
succ SBV (FloatingPoint eb sb)
x = SBV (FloatingPoint eb sb)
x SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
+ SBV (FloatingPoint eb sb)
1
   pred :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
pred SBV (FloatingPoint eb sb)
x = SBV (FloatingPoint eb sb)
x SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
- SBV (FloatingPoint eb sb)
1

   toEnum :: SInteger -> SBV (FloatingPoint eb sb)
toEnum   = SInteger -> SBV (FloatingPoint eb sb)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral
   fromEnum :: SBV (FloatingPoint eb sb) -> SInteger
fromEnum = SRoundingMode -> SBV (FloatingPoint eb sb) -> SInteger
forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SFloatingPoint eb sb -> SInteger
forall a (eb :: Nat) (sb :: Nat).
(IEEEFloatConvertible a, ValidFloat eb sb) =>
SRoundingMode -> SFloatingPoint eb sb -> SBV a
fromSFloatingPoint SRoundingMode
sRTZ

   enumFrom :: SBV (FloatingPoint eb sb) -> SList (FloatingPoint eb sb)
enumFrom   SBV (FloatingPoint eb sb)
n = SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SList (FloatingPoint eb sb)
forall a. EnumSymbolic a => SBV a -> SBV a -> SList a
enumFromThen   SBV (FloatingPoint eb sb)
n (SBV (FloatingPoint eb sb)
nSBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
+SBV (FloatingPoint eb sb)
1)
   enumFromTo :: SymVal (FloatingPoint eb sb) =>
SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SList (FloatingPoint eb sb)
enumFromTo SBV (FloatingPoint eb sb)
n = SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
forall a.
(EnumSymbolic a, SymVal a) =>
SBV a -> SBV a -> SBV a -> SList a
enumFromThenTo SBV (FloatingPoint eb sb)
n (SBV (FloatingPoint eb sb)
nSBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
+SBV (FloatingPoint eb sb)
1)

   enumFromThen :: SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SList (FloatingPoint eb sb)
enumFromThen SBV (FloatingPoint eb sb)
x SBV (FloatingPoint eb sb)
y = SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
go SBV (FloatingPoint eb sb)
0 SBV (FloatingPoint eb sb)
x (SBV (FloatingPoint eb sb)
ySBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
-SBV (FloatingPoint eb sb)
x)
     where go :: SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
go = String
-> (SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SList (FloatingPoint eb sb))
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.FloatingPoint.enumFromThen" ((SBV (FloatingPoint eb sb)
  -> SBV (FloatingPoint eb sb)
  -> SBV (FloatingPoint eb sb)
  -> SList (FloatingPoint eb sb))
 -> SBV (FloatingPoint eb sb)
 -> SBV (FloatingPoint eb sb)
 -> SBV (FloatingPoint eb sb)
 -> SList (FloatingPoint eb sb))
-> (SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SList (FloatingPoint eb sb))
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
forall a b. (a -> b) -> a -> b
$ \SBV (FloatingPoint eb sb)
k SBV (FloatingPoint eb sb)
n SBV (FloatingPoint eb sb)
d -> (SBV (FloatingPoint eb sb)
n SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
+ SBV (FloatingPoint eb sb)
k SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
* SBV (FloatingPoint eb sb)
d) SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb) -> SList (FloatingPoint eb sb)
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
go (SBV (FloatingPoint eb sb)
kSBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
+SBV (FloatingPoint eb sb)
1) SBV (FloatingPoint eb sb)
n SBV (FloatingPoint eb sb)
d

   enumFromThenTo :: SymVal (FloatingPoint eb sb) =>
SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
enumFromThenTo SBV (FloatingPoint eb sb)
x SBV (FloatingPoint eb sb)
y SBV (FloatingPoint eb sb)
zIn = SBool
-> SList (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV (FloatingPoint eb sb)
delta SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV (FloatingPoint eb sb)
0) (SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
up SBV (FloatingPoint eb sb)
0 SBV (FloatingPoint eb sb)
x SBV (FloatingPoint eb sb)
delta SBV (FloatingPoint eb sb)
z) (SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
down SBV (FloatingPoint eb sb)
0 SBV (FloatingPoint eb sb)
x SBV (FloatingPoint eb sb)
delta SBV (FloatingPoint eb sb)
z)
     where delta, z :: SFloatingPoint eb sb
           delta :: SBV (FloatingPoint eb sb)
delta = SBV (FloatingPoint eb sb)
y SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
- SBV (FloatingPoint eb sb)
x
           z :: SBV (FloatingPoint eb sb)
z     = SBV (FloatingPoint eb sb)
zIn SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
+ SBV (FloatingPoint eb sb)
delta SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Fractional a => a -> a -> a
/ SBV (FloatingPoint eb sb)
2

           up, down :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SList (FloatingPoint eb sb)
           up :: SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
up    = String
-> (SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SList (FloatingPoint eb sb))
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.FloatingPoint.enumFromThenTo.up"   ((SBV (FloatingPoint eb sb)
  -> SBV (FloatingPoint eb sb)
  -> SBV (FloatingPoint eb sb)
  -> SBV (FloatingPoint eb sb)
  -> SList (FloatingPoint eb sb))
 -> SBV (FloatingPoint eb sb)
 -> SBV (FloatingPoint eb sb)
 -> SBV (FloatingPoint eb sb)
 -> SBV (FloatingPoint eb sb)
 -> SList (FloatingPoint eb sb))
-> (SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SList (FloatingPoint eb sb))
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
forall a b. (a -> b) -> a -> b
$ \SBV (FloatingPoint eb sb)
k SBV (FloatingPoint eb sb)
n SBV (FloatingPoint eb sb)
d SBV (FloatingPoint eb sb)
end -> let c :: SBV (FloatingPoint eb sb)
c = SBV (FloatingPoint eb sb)
n SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
+ SBV (FloatingPoint eb sb)
k SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
* SBV (FloatingPoint eb sb)
d in SBool
-> SList (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV (FloatingPoint eb sb)
c SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV (FloatingPoint eb sb)
end) [] (SBV (FloatingPoint eb sb)
c SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb) -> SList (FloatingPoint eb sb)
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
up   (SBV (FloatingPoint eb sb)
kSBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
+SBV (FloatingPoint eb sb)
1) SBV (FloatingPoint eb sb)
n SBV (FloatingPoint eb sb)
d SBV (FloatingPoint eb sb)
end)
           down :: SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
down  = String
-> (SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SList (FloatingPoint eb sb))
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.FloatingPoint.enumFromThenTo.down" ((SBV (FloatingPoint eb sb)
  -> SBV (FloatingPoint eb sb)
  -> SBV (FloatingPoint eb sb)
  -> SBV (FloatingPoint eb sb)
  -> SList (FloatingPoint eb sb))
 -> SBV (FloatingPoint eb sb)
 -> SBV (FloatingPoint eb sb)
 -> SBV (FloatingPoint eb sb)
 -> SBV (FloatingPoint eb sb)
 -> SList (FloatingPoint eb sb))
-> (SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SList (FloatingPoint eb sb))
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
forall a b. (a -> b) -> a -> b
$ \SBV (FloatingPoint eb sb)
k SBV (FloatingPoint eb sb)
n SBV (FloatingPoint eb sb)
d SBV (FloatingPoint eb sb)
end -> let c :: SBV (FloatingPoint eb sb)
c = SBV (FloatingPoint eb sb)
n SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
+ SBV (FloatingPoint eb sb)
k SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
* SBV (FloatingPoint eb sb)
d in SBool
-> SList (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV (FloatingPoint eb sb)
c SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV (FloatingPoint eb sb)
end) [] (SBV (FloatingPoint eb sb)
c SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb) -> SList (FloatingPoint eb sb)
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SList (FloatingPoint eb sb)
down (SBV (FloatingPoint eb sb)
kSBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Num a => a -> a -> a
+SBV (FloatingPoint eb sb)
1) SBV (FloatingPoint eb sb)
n SBV (FloatingPoint eb sb)
d SBV (FloatingPoint eb sb)
end)

-- | 'EnumSymbolic instance for arbitrary AlgReal. We don't have to use the multiplicative trick here
-- since alg-reals are precise. But, following rational in Haskell, we do use the stopping point of @z + delta / 2@.
instance {-# OVERLAPPING #-} EnumSymbolic AlgReal where
   succ :: SBV AlgReal -> SBV AlgReal
succ SBV AlgReal
x = SBV AlgReal
x SBV AlgReal -> SBV AlgReal -> SBV AlgReal
forall a. Num a => a -> a -> a
+ SBV AlgReal
1
   pred :: SBV AlgReal -> SBV AlgReal
pred SBV AlgReal
x = SBV AlgReal
x SBV AlgReal -> SBV AlgReal -> SBV AlgReal
forall a. Num a => a -> a -> a
- SBV AlgReal
1

   toEnum :: SInteger -> SBV AlgReal
toEnum   = SInteger -> SBV AlgReal
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral
   fromEnum :: SBV AlgReal -> SInteger
fromEnum = SBV AlgReal -> SInteger
sRealToSIntegerTruncate

   enumFrom :: SBV AlgReal -> SList AlgReal
enumFrom   SBV AlgReal
n = SBV AlgReal -> SBV AlgReal -> SList AlgReal
forall a. EnumSymbolic a => SBV a -> SBV a -> SList a
enumFromThen   SBV AlgReal
n (SBV AlgReal
nSBV AlgReal -> SBV AlgReal -> SBV AlgReal
forall a. Num a => a -> a -> a
+SBV AlgReal
1)
   enumFromTo :: SymVal AlgReal => SBV AlgReal -> SBV AlgReal -> SList AlgReal
enumFromTo SBV AlgReal
n = SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal
forall a.
(EnumSymbolic a, SymVal a) =>
SBV a -> SBV a -> SBV a -> SList a
enumFromThenTo SBV AlgReal
n (SBV AlgReal
nSBV AlgReal -> SBV AlgReal -> SBV AlgReal
forall a. Num a => a -> a -> a
+SBV AlgReal
1)

   enumFromThen :: SBV AlgReal -> SBV AlgReal -> SList AlgReal
enumFromThen SBV AlgReal
x SBV AlgReal
y = SBV AlgReal -> SBV AlgReal -> SList AlgReal
go SBV AlgReal
x (SBV AlgReal
ySBV AlgReal -> SBV AlgReal -> SBV AlgReal
forall a. Num a => a -> a -> a
-SBV AlgReal
x)
     where go :: SBV AlgReal -> SBV AlgReal -> SList AlgReal
go = String
-> (SBV AlgReal -> SBV AlgReal -> SList AlgReal)
-> SBV AlgReal
-> SBV AlgReal
-> SList AlgReal
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.AlgReal.enumFromThen" ((SBV AlgReal -> SBV AlgReal -> SList AlgReal)
 -> SBV AlgReal -> SBV AlgReal -> SList AlgReal)
-> (SBV AlgReal -> SBV AlgReal -> SList AlgReal)
-> SBV AlgReal
-> SBV AlgReal
-> SList AlgReal
forall a b. (a -> b) -> a -> b
$ \SBV AlgReal
start SBV AlgReal
delta -> SBV AlgReal
start SBV AlgReal -> SList AlgReal -> SList AlgReal
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV AlgReal -> SBV AlgReal -> SList AlgReal
go (SBV AlgReal
startSBV AlgReal -> SBV AlgReal -> SBV AlgReal
forall a. Num a => a -> a -> a
+SBV AlgReal
delta) SBV AlgReal
delta

   enumFromThenTo :: SymVal AlgReal =>
SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal
enumFromThenTo SBV AlgReal
x SBV AlgReal
y SBV AlgReal
zIn = SBool -> SList AlgReal -> SList AlgReal -> SList AlgReal
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV AlgReal
delta SBV AlgReal -> SBV AlgReal -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV AlgReal
0) (SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal
up SBV AlgReal
x SBV AlgReal
delta SBV AlgReal
z) (SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal
down SBV AlgReal
x SBV AlgReal
delta SBV AlgReal
z)
     where delta, z :: SReal
           delta :: SBV AlgReal
delta = SBV AlgReal
y SBV AlgReal -> SBV AlgReal -> SBV AlgReal
forall a. Num a => a -> a -> a
- SBV AlgReal
x
           z :: SBV AlgReal
z     = SBV AlgReal
zIn SBV AlgReal -> SBV AlgReal -> SBV AlgReal
forall a. Num a => a -> a -> a
+ SBV AlgReal
delta SBV AlgReal -> SBV AlgReal -> SBV AlgReal
forall a. Fractional a => a -> a -> a
/ SBV AlgReal
2

           up, down :: SReal -> SReal -> SReal -> SList AlgReal
           up :: SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal
up    = String
-> (SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal)
-> SBV AlgReal
-> SBV AlgReal
-> SBV AlgReal
-> SList AlgReal
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.AlgReal.enumFromThenTo.up"   ((SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal)
 -> SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal)
-> (SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal)
-> SBV AlgReal
-> SBV AlgReal
-> SBV AlgReal
-> SList AlgReal
forall a b. (a -> b) -> a -> b
$ \SBV AlgReal
start SBV AlgReal
d SBV AlgReal
end -> SBool -> SList AlgReal -> SList AlgReal -> SList AlgReal
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV AlgReal
start SBV AlgReal -> SBV AlgReal -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV AlgReal
end) [] (SBV AlgReal
start SBV AlgReal -> SList AlgReal -> SList AlgReal
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal
up   (SBV AlgReal
start SBV AlgReal -> SBV AlgReal -> SBV AlgReal
forall a. Num a => a -> a -> a
+ SBV AlgReal
d) SBV AlgReal
d SBV AlgReal
end)
           down :: SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal
down  = String
-> (SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal)
-> SBV AlgReal
-> SBV AlgReal
-> SBV AlgReal
-> SList AlgReal
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"EnumSymbolic.AlgReal.enumFromThenTo.down" ((SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal)
 -> SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal)
-> (SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal)
-> SBV AlgReal
-> SBV AlgReal
-> SBV AlgReal
-> SList AlgReal
forall a b. (a -> b) -> a -> b
$ \SBV AlgReal
start SBV AlgReal
d SBV AlgReal
end -> SBool -> SList AlgReal -> SList AlgReal -> SList AlgReal
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV AlgReal
start SBV AlgReal -> SBV AlgReal -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV AlgReal
end) [] (SBV AlgReal
start SBV AlgReal -> SList AlgReal -> SList AlgReal
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal
down (SBV AlgReal
start SBV AlgReal -> SBV AlgReal -> SBV AlgReal
forall a. Num a => a -> a -> a
+ SBV AlgReal
d) SBV AlgReal
d SBV AlgReal
end)

-- | Lookup. If we can't find, then the result is unspecified.
--
-- >>> lookup (4 :: SInteger) (literal [(5, 12), (4, 3), (2, 6 :: Integer)])
-- 3 :: SInteger
-- >>> prove  $ \(x :: SInteger) -> x .== lookup 9 (literal [(5, 12), (4, 3), (2, 6 :: Integer)])
-- Falsifiable. Counter-example:
--   Data.SBV.List.lookup_notFound @Integer = 0 :: Integer
--   s0                                     = 1 :: Integer
lookup :: (SymVal k, SymVal v) => SBV k -> SList (k, v) -> SBV v
lookup :: forall k v. (SymVal k, SymVal v) => SBV k -> SList (k, v) -> SBV v
lookup = String
-> (SBV k -> SList (k, v) -> SBV v)
-> SBV k
-> SList (k, v)
-> SBV v
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"Data.SBV.List.lookup" ((SBV k -> SList (k, v) -> SBV v)
 -> SBV k -> SList (k, v) -> SBV v)
-> (SBV k -> SList (k, v) -> SBV v)
-> SBV k
-> SList (k, v)
-> SBV v
forall a b. (a -> b) -> a -> b
$ \SBV k
k SList (k, v)
lst -> SBool -> SBV v -> SBV v -> SBV v
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList (k, v) -> SBool
forall a. SymVal a => SList a -> SBool
null SList (k, v)
lst)
                                                            (String -> (SBV v -> SBool) -> SBV v
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"Data.SBV.List.lookup_notFound" (SBool -> SBV v -> SBool
forall a b. a -> b -> a
const SBool
sTrue))
                                                            (let (SBV k
k', SBV v
v) = SBV (k, v) -> (SBV k, SBV v)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SList (k, v) -> SBV (k, v)
forall a. SymVal a => SList a -> SBV a
head SList (k, v)
lst)
                                                             in SBool -> SBV v -> SBV v -> SBV v
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV k
k SBV k -> SBV k -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV k
k') SBV v
v (SBV k -> SList (k, v) -> SBV v
forall k v. (SymVal k, SymVal v) => SBV k -> SList (k, v) -> SBV v
lookup SBV k
k (SList (k, v) -> SList (k, v)
forall a. SymVal a => SList a -> SList a
tail SList (k, v)
lst)))

-- | @`strToNat` s@. Retrieve integer encoded by string @s@ (ground rewriting only).
-- Note that by definition this function only works when @s@ only contains digits,
-- that is, if it encodes a natural number. Otherwise, it returns '-1'.
--
-- >>> prove $ \s -> let n = strToNat s in length s .== 1 .=> (-1) .<= n .&& n .<= 9
-- Q.E.D.
strToNat :: SString -> SInteger
strToNat :: SString -> SInteger
strToNat SString
s
 | Just String
a <- SString -> Maybe String
forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s
 = if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
P.all Char -> Bool
C.isDigit String
a Bool -> Bool -> Bool
&& Bool -> Bool
not (String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null String
a)
   then Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal (String -> Integer
forall a. Read a => String -> a
read String
a)
   else -SInteger
1
 | Bool
True
 = StrOp -> Maybe (String -> Integer) -> SString -> SInteger
forall a b.
(SymVal a, SymVal b) =>
StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1Str StrOp
StrStrToNat Maybe (String -> Integer)
forall a. Maybe a
Nothing SString
s

-- | @`natToStr` i@. Retrieve string encoded by integer @i@ (ground rewriting only).
-- Again, only naturals are supported, any input that is not a natural number
-- produces empty string, even though we take an integer as an argument.
--
-- >>> prove $ \i -> length (natToStr i) .== 3 .=> i .<= 999
-- Q.E.D.
natToStr :: SInteger -> SString
natToStr :: SInteger -> SString
natToStr SInteger
i
 | Just Integer
v <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
i
 = String -> SString
forall a. SymVal a => a -> SBV a
literal (String -> SString) -> String -> SString
forall a b. (a -> b) -> a -> b
$ if Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Integer -> String
forall a. Show a => a -> String
show Integer
v else String
""
 | Bool
True
 = StrOp -> Maybe (Integer -> String) -> SInteger -> SString
forall a b.
(SymVal a, SymVal b) =>
StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1Str StrOp
StrNatToStr Maybe (Integer -> String)
forall a. Maybe a
Nothing SInteger
i

-- | Lift a unary operator over lists.
lift1 :: forall a b. (SymVal a, SymVal b) => Bool -> SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 :: forall a b.
(SymVal a, SymVal b) =>
Bool -> SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 Bool
simpleEq SeqOp
w Maybe (a -> b)
mbOp SBV a
a
  | Just SBV b
cv <- Bool -> Maybe (a -> b) -> SBV a -> Maybe (SBV b)
forall a b.
(SymVal a, SymVal b) =>
Bool -> Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 Bool
simpleEq Maybe (a -> b)
mbOp SBV a
a
  = SBV b
cv
  | Bool
True
  = SVal -> SBV b
forall a. SVal -> SBV a
SBV (SVal -> SBV b) -> SVal -> SBV b
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k = Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)
        r :: State -> IO SV
r State
st = do SV
sva <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (SeqOp -> Op
SeqOp SeqOp
w) [Item [SV]
SV
sva])

-- | Lift a binary operator over lists.
lift2 :: forall a b c. (SymVal a, SymVal b, SymVal c) => Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 :: forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 Bool
simpleEq SeqOp
w Maybe (a -> b -> c)
mbOp SBV a
a SBV b
b
  | Just SBV c
cv <- Bool -> Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
concEval2 Bool
simpleEq Maybe (a -> b -> c)
mbOp SBV a
a SBV b
b
  = SBV c
cv
  | Bool
True
  = SVal -> SBV c
forall a. SVal -> SBV a
SBV (SVal -> SBV c) -> SVal -> SBV c
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k = Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @c)
        r :: State -> IO SV
r State
st = do SV
sva <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  SV
svb <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
b
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (SeqOp -> Op
SeqOp SeqOp
w) [Item [SV]
SV
sva, Item [SV]
SV
svb])

-- | Lift a ternary operator over lists.
lift3 :: forall a b c d. (SymVal a, SymVal b, SymVal c, SymVal d) => Bool -> SeqOp -> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> SBV d
lift3 :: forall a b c d.
(SymVal a, SymVal b, SymVal c, SymVal d) =>
Bool
-> SeqOp
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> SBV d
lift3 Bool
simpleEq SeqOp
w Maybe (a -> b -> c -> d)
mbOp SBV a
a SBV b
b SBV c
c
  | Just SBV d
cv <- Bool
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> Maybe (SBV d)
forall a b c d.
(SymVal a, SymVal b, SymVal c, SymVal d) =>
Bool
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> Maybe (SBV d)
concEval3 Bool
simpleEq Maybe (a -> b -> c -> d)
mbOp SBV a
a SBV b
b SBV c
c
  = SBV d
cv
  | Bool
True
  = SVal -> SBV d
forall a. SVal -> SBV a
SBV (SVal -> SBV d) -> SVal -> SBV d
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k = Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @d)
        r :: State -> IO SV
r State
st = do SV
sva <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  SV
svb <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
b
                  SV
svc <- State -> SBV c -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV c
c
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (SeqOp -> Op
SeqOp SeqOp
w) [Item [SV]
SV
sva, Item [SV]
SV
svb, Item [SV]
SV
svc])

-- | Concrete evaluation for unary ops
concEval1 :: forall a b. (SymVal a, SymVal b) => Bool -> Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 :: forall a b.
(SymVal a, SymVal b) =>
Bool -> Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 Bool
simpleEq Maybe (a -> b)
mbOp SBV a
a
  | Bool -> Bool
not Bool
simpleEq Bool -> Bool -> Bool
|| Kind -> Bool
eqCheckIsObjectEq (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) = b -> SBV b
forall a. SymVal a => a -> SBV a
literal (b -> SBV b) -> Maybe b -> Maybe (SBV b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe (a -> b)
mbOp Maybe (a -> b) -> Maybe a -> Maybe b
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a)
  | Bool
True                                                  = Maybe (SBV b)
forall a. Maybe a
Nothing

-- | Concrete evaluation for binary ops
concEval2 :: forall a b c. (SymVal a, SymVal b, SymVal c) => Bool -> Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
concEval2 :: forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
concEval2 Bool
simpleEq Maybe (a -> b -> c)
mbOp SBV a
a SBV b
b
  | Bool -> Bool
not Bool
simpleEq Bool -> Bool -> Bool
|| Kind -> Bool
eqCheckIsObjectEq (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) = c -> SBV c
forall a. SymVal a => a -> SBV a
literal (c -> SBV c) -> Maybe c -> Maybe (SBV c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe (a -> b -> c)
mbOp Maybe (a -> b -> c) -> Maybe a -> Maybe (b -> c)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a Maybe (b -> c) -> Maybe b -> Maybe c
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
b)
  | Bool
True                                                  = Maybe (SBV c)
forall a. Maybe a
Nothing

-- | Concrete evaluation for ternary ops
concEval3 :: forall a b c d. (SymVal a, SymVal b, SymVal c, SymVal d) => Bool -> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> Maybe (SBV d)
concEval3 :: forall a b c d.
(SymVal a, SymVal b, SymVal c, SymVal d) =>
Bool
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> Maybe (SBV d)
concEval3 Bool
simpleEq Maybe (a -> b -> c -> d)
mbOp SBV a
a SBV b
b SBV c
c
  | Bool -> Bool
not Bool
simpleEq Bool -> Bool -> Bool
|| Kind -> Bool
eqCheckIsObjectEq (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) = d -> SBV d
forall a. SymVal a => a -> SBV a
literal (d -> SBV d) -> Maybe d -> Maybe (SBV d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe (a -> b -> c -> d)
mbOp Maybe (a -> b -> c -> d) -> Maybe a -> Maybe (b -> c -> d)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a Maybe (b -> c -> d) -> Maybe b -> Maybe (c -> d)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
b Maybe (c -> d) -> Maybe c -> Maybe d
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SBV c -> Maybe c
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
c)
  | Bool
True                                                  = Maybe (SBV d)
forall a. Maybe a
Nothing

-- | Is the list concretely known empty?
isConcretelyEmpty :: SymVal a => SList a -> Bool
isConcretelyEmpty :: forall a. SymVal a => SList a -> Bool
isConcretelyEmpty SList a
sl | Just [a]
l <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
sl = [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [a]
l
                     | Bool
True                   = Bool
False

-- | Lift a unary operator over strings.
lift1Str :: forall a b. (SymVal a, SymVal b) => StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1Str :: forall a b.
(SymVal a, SymVal b) =>
StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1Str StrOp
w Maybe (a -> b)
mbOp SBV a
a
  | Just SBV b
cv <- b -> SBV b
forall a. SymVal a => a -> SBV a
literal (b -> SBV b) -> Maybe b -> Maybe (SBV b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe (a -> b)
mbOp Maybe (a -> b) -> Maybe a -> Maybe b
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a)
  = SBV b
cv
  | Bool
True
  = SVal -> SBV b
forall a. SVal -> SBV a
SBV (SVal -> SBV b) -> SVal -> SBV b
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k = Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)
        r :: State -> IO SV
r State
st = do SV
sva <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (StrOp -> Op
StrOp StrOp
w) [Item [SV]
SV
sva])

{- HLint ignore implode "Use :" -}