sbv-14.3: Data/SBV/List.hs
-----------------------------------------------------------------------------
-- |
-- 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 QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -Werror -Wno-orphans #-}
module Data.SBV.List (
-- * Length, emptiness
length, null
-- * Deconstructing/Reconstructing
, nil, (.:), snoc, head, tail, uncons, init, last, singleton, listToListAt, elemAt, (!!), implode, concat, (++)
-- * Case analysis (for sCase quasi-quoter)
, list
-- * 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
-- * Minimum and maximum of a list
, minimum, maximum
-- * 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, minimum, maximum)
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.SCase (sCase)
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
#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, minimum, maximum)
-- >>> import qualified Prelude as P(map)
-- >>> import Data.SBV
-- >>> :set -XDataKinds
-- >>> :set -XOverloadedLists
-- >>> :set -XOverloadedStrings
-- >>> :set -XScopedTypeVariables
-- >>> :set -XTypeApplications
-- >>> :set -XQuasiQuotes
#endif
-- | 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 = lift1 False (SeqLen (kindOf (Proxy @a))) (Just (fromIntegral . 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 l
| Just cs <- unliteral l
= literal (P.null cs)
| True
= length l .== 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 = (`elemAt` 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 l
| Just (_:cs) <- unliteral l
= literal cs
| True
= subList l 1 (length l - 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 l = (head l, tail l)
-- | Case analysis on a symbolic list. If the list is empty, return the first argument.
-- Otherwise, apply the second argument to the head and tail of the list.
--
-- >>> list (0 :: SInteger) (\h _ -> h) ([] :: SList Integer)
-- 0 :: SInteger
-- >>> list (0 :: SInteger) (\h _ -> h) ([3, 4, 5] :: SList Integer)
-- 3 :: SInteger
-- >>> prove $ \(l :: SList Integer) -> null l .|| list sFalse (\_ _ -> sTrue) l
-- Q.E.D.
list :: (SymVal a, SymVal b) => SBV b -> (SBV a -> SList a -> SBV b) -> SList a -> SBV b
list nilCase consCase xs = [sCase| xs of
[] -> nilCase
h:ts -> consCase h ts
|]
-- | @`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 l
| Just cs@(_:_) <- unliteral l
= literal $ P.init cs
| True
= subList l 0 (length l - 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 l = l `elemAt` (length l - 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 = lift1 False (SeqUnit (kindOf (Proxy @a))) (Just (: []))
-- | @`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,32] :: [Word16]
listToListAt :: SymVal a => SList a -> SInteger -> SList a
listToListAt s offset = subList s offset 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 l i
| Just xs <- unliteral l, Just ci <- unliteral i, ci >= 0, ci < genericLength xs, let x = xs `genericIndex` ci
= literal x
| True
= lift2 False (SeqNth (kindOf (Proxy @a))) Nothing l 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
(!!) = 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 = P.foldr ((++) . \x -> [x]) (literal [])
-- | 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
as `snoc` a = as ++ [a]
-- nil is defined in Data.SBV.Core.Data and re-exported here.
-- | 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
x ++ y | isConcretelyEmpty x = y
| isConcretelyEmpty y = x
| True = lift2 False (SeqConcat (kindOf (Proxy @a))) (Just (P.++)) x 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
e `elem` l = [e] `isInfixOf` 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
e `notElem` l = sNot (e `elem` 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
sub `isInfixOf` l
| isConcretelyEmpty sub
= literal True
| True
= lift2 True (SeqContains (kindOf (Proxy @a))) (Just (flip L.isInfixOf)) l 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
pre `isPrefixOf` l
| isConcretelyEmpty pre
= literal True
| True
= lift2 True (SeqPrefixOf (kindOf (Proxy @a))) (Just L.isPrefixOf) pre 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.
--
-- NB. We case-split on @x@ only and use a guard for @y@ being empty, rather than case-splitting on the
-- tuple @(x, y)@. A 4-way tuple match produces a larger and\/or\/not SMTLib tree that z3 struggles with.
listEq :: forall a. SymVal a => SList a -> SList a -> SBool
listEq
| containsFloats (kindOf (Proxy @a))
= smtFunction "listEq"
$ \x y -> [sCase| x of
[] -> null y
a:xs -> case y of
[] -> sFalse
b : ys -> a .== b .&& xs `listEq` ys
|]
| True
= (.==)
-- | @`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
suf `isSuffixOf` l
| isConcretelyEmpty suf
= literal True
| True
= lift2 True (SeqSuffixOf (kindOf (Proxy @a))) (Just L.isSuffixOf) suf 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 i l = ite (i .<= 0) (literal [])
$ ite (i .>= length l) l
$ subList l 0 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 i s = ite (i .>= ls) (literal [])
$ ite (i .<= 0) s
$ subList s i (ls - i)
where ls = length 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 n xs = (take n xs, drop n 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 l offset len
| Just c <- unliteral l -- a constant list
, Just o <- unliteral offset -- a constant offset
, Just sz <- unliteral len -- a constant length
, let lc = genericLength c -- length of the list
, let valid x = x >= 0 && x <= lc -- predicate that checks valid point
, valid o -- offset is valid
, sz >= 0 -- length is not-negative
, valid $ o + sz -- we don't overrun
= literal $ genericTake sz $ genericDrop o c
| True -- either symbolic, or something is out-of-bounds
= lift3 False (SeqSubseq (kindOf (Proxy @a))) Nothing l offset 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 l src dst
| Just b <- unliteral src, P.null b -- If src is null, simply prepend
= dst ++ l
| eqCheckIsObjectEq ka
, Just a <- unliteral l
, Just b <- unliteral src
, Just c <- unliteral dst
= literal $ walk a b c
| True
= lift3 True (SeqReplace ka) Nothing l src dst
where walk haystack needle newNeedle = go haystack -- note that needle is guaranteed non-empty here.
where go [] = []
go i@(c:cs)
| needle `L.isPrefixOf` i = newNeedle P.++ genericDrop (genericLength needle :: Integer) i
| True = c : go cs
ka = kindOf (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 s sub = offsetIndexOf s sub 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 s sub offset
| eqCheckIsObjectEq ka
, Just c <- unliteral s -- a constant list
, Just n <- unliteral sub -- a constant search pattern
, Just o <- unliteral offset -- at a constant offset
, o >= 0, o <= genericLength c -- offset is good
= case [i | (i, t) <- P.zip [o ..] (L.tails (genericDrop o c)), n `L.isPrefixOf` t] of
(i:_) -> literal i
_ -> -1
| True
= lift3 True (SeqIndexOf ka) Nothing s sub offset
where ka = kindOf (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 l
| Just l' <- unliteral l
= literal (P.reverse l')
| True
= def l
where def = smtFunction "sbv.reverse"
$ \xs -> [sCase| xs of
[] -> []
h:ts -> def ts ++ [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 _ f sas
| Just as <- unliteral sas
= case P.map (unliteral . f . literal) as of
bs | P.any isNothing bs -> Nothing
| True -> Just (catMaybes bs)
| True
= 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 f l
| Just concResult <- concreteMap f f l
= literal concResult
| True
= sbvMap l
where sbvMap = smtHOFunction "sbv.map" f
$ \xs -> [sCase| xs of
[] -> []
h : t -> f h .: sbvMap t
|]
-- | Mapping symbolic closures.
instance (SymVal env, SymVal a, SymVal b) => SMap (Closure (SBV env) (SBV a -> SBV b)) a b where
map cls@Closure{closureEnv, closureFun} l
| Just concResult <- concreteMap cls (closureFun closureEnv) l
= literal concResult
| True
= sbvMap (tuple (closureEnv, l))
where sbvMap = smtHOFunction "sbv.closureMap" closureFun
$ \envxs -> [sCase| envxs of
(_, []) -> []
(cEnv, h : t) -> closureFun cEnv h .: sbvMap (tuple (cEnv, 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 f = concat . map 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 'sbv.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 _ f sb sas
| Just b <- unliteral sb, Just as <- unliteral sas
= go b as
| True
= Nothing
where go b [] = Just b
go b (e:es) = case unliteral (literal b `f` literal e) of
Nothing -> Nothing
Just b' -> go b' 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 f base l
| Just concResult <- concreteFoldl f f base l
= literal concResult
| True
= sbvFoldl $ tuple (base, l)
where sbvFoldl = smtHOFunction "sbv.foldl" (uncurry f . untuple)
$ \exs -> [sCase| exs of
(e, []) -> e
(e, h : t) -> sbvFoldl (tuple (e `f` h, 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 cls@Closure{closureEnv, closureFun} base l
| Just concResult <- concreteFoldl cls (closureFun closureEnv) base l
= literal concResult
| True
= sbvFoldl $ tuple (closureEnv, base, l)
where sbvFoldl = smtHOFunction "sbv.closureFoldl" closureFun
$ \envxs -> [sCase| envxs of
(_, e, []) -> e
(cEnv, e, h : t) -> sbvFoldl (tuple (cEnv, closureFun closureEnv e h, 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 _ f sb sas
| Just b <- unliteral sb, Just as <- unliteral sas
= go b as
| True
= Nothing
where go b [] = Just b
go b (e:es) = case go b es of
Nothing -> Nothing
Just res -> unliteral (literal e `f` literal 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 f base l
| Just concResult <- concreteFoldr f f base l
= literal concResult
| True
= sbvFoldr $ tuple (base, l)
where sbvFoldr = smtHOFunction "sbv.foldr" (uncurry f . untuple)
$ \exs -> [sCase| exs of
(e, []) -> e
(e, h : t) -> h `f` sbvFoldr (tuple (e, 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 cls@Closure{closureEnv, closureFun} base l
| Just concResult <- concreteFoldr cls (closureFun closureEnv) base l
= literal concResult
| True
= sbvFoldr $ tuple (closureEnv, base, l)
where sbvFoldr = smtHOFunction "sbv.closureFoldr" closureFun
$ \envxs -> [sCase| envxs of
(_, e, []) -> e
(cEnv, e, h : t) -> closureFun closureEnv h (sbvFoldr (tuple (cEnv, e, 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 xs ys
| Just xs' <- unliteral xs, Just ys' <- unliteral ys
= literal $ P.zip xs' ys'
| True
= def xs ys
where def = smtFunction "sbv.zip"
$ \x y -> [sCase| tuple (x, y) of
([], _ ) -> []
(_, [] ) -> []
(a:as, b:bs) -> tuple (a, b) .: def as 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 _ f sas sbs
| Just as <- unliteral sas, Just bs <- unliteral sbs
= go as bs
| True
= Nothing
where go [] _ = Just []
go _ [] = Just []
go (a:as) (b:bs) = (:) <$> unliteral (literal a `f` literal b) <*> go as 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 f xs ys
| Just concResult <- concreteZipWith f f xs ys
= literal concResult
| True
= sbvZipWith $ tuple (xs, ys)
where sbvZipWith = smtHOFunction "sbv.zipWith" (uncurry f . untuple)
$ \asbs -> [sCase| asbs of
([], _ ) -> []
(_, [] ) -> []
(a:as, b:bs) -> f a b .: sbvZipWith (tuple (as, 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 cls@Closure{closureEnv, closureFun} xs ys
| Just concResult <- concreteZipWith cls (closureFun closureEnv) xs ys
= literal concResult
| True
= sbvZipWith $ tuple (closureEnv, xs, ys)
where sbvZipWith = smtHOFunction "sbv.closureZipWith" closureFun
$ \envasbs -> [sCase| envasbs of
(_, [], _ ) -> []
(_, _, [] ) -> []
(cEnv, a:as, b:bs) -> closureFun cEnv a b .: sbvZipWith (tuple (cEnv, as, 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 = foldr (++) []
-- | 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 f = foldr ((.&&) . f) 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 f = foldr ((.||) . f) sFalse
-- | Conjunction of all the elements.
--
-- >>> and []
-- True
-- >>> prove $ \s -> and [s, sNot s] .== sFalse
-- Q.E.D.
and :: SList Bool -> SBool
and = all id
-- | Disjunction of all the elements.
--
-- >>> or []
-- False
-- >>> prove $ \s -> or [s, sNot s]
-- Q.E.D.
or :: SList Bool -> SBool
or = any 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 c e
| Just c' <- unliteral c, Just e' <- unliteral e
= literal (genericReplicate c' e')
| True
= def c e
where def = smtFunction "sbv.replicate"
$ \count elt -> [sCase| count of
_ | count .<= 0 -> []
_ -> elt .: def (count - 1) 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 xs
| Just xs' <- unliteral xs
= literal (L.inits xs')
| True
= def xs
where def = smtFunction "sbv.inits"
$ \l -> [sCase| l of
[] -> [[]]
_ : _ -> def (init l) ++ [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 xs
| Just xs' <- unliteral xs
= literal (L.tails xs')
| True
= def xs
where def = smtFunction "sbv.tails"
$ \l -> [sCase| l of
[] -> [[]]
_ : tl -> l .: def tl
|]
-- | Minimum of a list that has symbolic-ordering. If the list is empty, then
-- the result is underspecified, i.e., it is an arbitrary element of the element type.
--
-- >>> minimum ([1,2,3] :: SList Integer)
-- 1 :: SInteger
-- >>> sat $ 512 .== minimum (literal [] :: SList Integer)
-- Satisfiable. Model:
-- SList.minimum @Integer = 512 :: Integer
minimum :: forall a. (SymVal a, Ord a, OrdSymbolic (SBV a)) => SList a -> SBV a
minimum xs
| Just lxs@(_:_) <- unliteral xs
= literal (P.minimum lxs)
| True
= foldr (smin @(SBV a)) (some "SList.minimum" (const sTrue)) xs
-- | Maximum of a list that has symbolic-ordering. If the list is empty, then
-- the result is underspecified, i.e., it is an arbitrary element of the element type.
--
-- >>> maximum ([1,2,3] :: SList Integer)
-- 3 :: SInteger
-- >>> sat $ 512 .== maximum (literal [] :: SList Integer)
-- Satisfiable. Model:
-- SList.maximum @Integer = 512 :: Integer
maximum :: forall a. (SymVal a, Ord a, OrdSymbolic (SBV a)) => SList a -> SBV a
maximum xs
| Just lxs@(_:_) <- unliteral xs
= literal (P.maximum lxs)
| True
= foldr (smax @(SBV a)) (some "SList.maximum" (const sTrue)) xs
-- | 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
xs \\ ys
| Just xs' <- unliteral xs, Just ys' <- unliteral ys
= literal (xs' L.\\ ys')
| True
= def xs ys
where def = smtFunction "sbv.diff"
$ \x y -> [sCase| x of
[] -> []
h : t -> let r = def t y
in ite (h `elem` y) r (h .: 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 _ f sas
| Just as <- unliteral sas
= case P.map (unliteral . f . literal) as of
xs | P.any isNothing xs -> Nothing
| True -> Just [e | (True, e) <- P.zip (catMaybes xs) as]
| True
= 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 _ f l
| Just l' <- unliteral l
= case P.map (unliteral . f . literal) l' of
xs | P.any isNothing xs -> Nothing
| True -> let (ts, fs) = L.partition P.fst (P.zip (catMaybes xs) l')
in Just (P.map P.snd ts, P.map P.snd fs)
| True
= 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 _ f sas
| Just as <- unliteral sas
= case P.map (unliteral . f . literal) as of
xs | P.any isNothing xs -> Nothing
| True -> Just (P.map P.snd (P.takeWhile P.fst (P.zip (catMaybes xs) as)))
| True
= 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 _ f sas
| Just as <- unliteral sas
= case P.map (unliteral . f . literal) as of
xs | P.any isNothing xs -> Nothing
| True -> Just (P.map P.snd (P.dropWhile P.fst (P.zip (catMaybes xs) as)))
| True
= 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 f l
| Just concResult <- concreteFilter f f l
= literal concResult
| True
= sbvFilter l
where sbvFilter = smtHOFunction "sbv.filter" f
$ \xs -> [sCase| xs of
[] -> []
h : t -> let r = sbvFilter t
in ite (f h) (h .: r) 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 f l
| Just concResult <- concretePartition f f l
= literal concResult
| True
= sbvPartition l
where sbvPartition = smtHOFunction "sbv.partition" f
$ \xs -> [sCase| xs of
[] -> tuple ([], [])
h : t -> case sbvPartition t of
(as, bs) | f h -> tuple (h .: as, bs)
| True -> tuple (as, h .: bs)
|]
-- | @takeWhile f xs@ takes the prefix of @xs@ that satisfy the predicate.
takeWhile f l
| Just concResult <- concreteTakeWhile f f l
= literal concResult
| True
= sbvTakeWhile l
where sbvTakeWhile = smtHOFunction "sbv.takeWhile" f
$ \xs -> [sCase| xs of
[] -> []
h : t | f h -> h .: sbvTakeWhile t
| True -> []
|]
-- | @dropWhile f xs@ drops the prefix of @xs@ that satisfy the predicate.
dropWhile f l
| Just concResult <- concreteDropWhile f f l
= literal concResult
| True
= sbvDropWhile l
where sbvDropWhile = smtHOFunction "sbv.dropWhile" f
$ \xs -> [sCase| xs of
[] -> []
h : t | f h -> sbvDropWhile t
| True -> xs
|]
-- | Filtering with closures.
instance (SymVal env, SymVal a) => SFilter (Closure (SBV env) (SBV a -> SBool)) a where
filter cls@Closure{closureEnv, closureFun} l
| Just concResult <- concreteFilter cls (closureFun closureEnv) l
= literal concResult
| True
= sbvFilter (tuple (closureEnv, l))
where sbvFilter = smtHOFunction "sbv.closureFilter" closureFun
$ \envxs -> [sCase| envxs of
(_, []) -> []
(cEnv, h : t) -> let r = sbvFilter (tuple (cEnv, t))
in ite (closureFun cEnv h) (h .: r) r
|]
partition cls@Closure{closureEnv, closureFun} l
| Just concResult <- concretePartition cls (closureFun closureEnv) l
= literal concResult
| True
= sbvPartition (tuple (closureEnv, l))
where sbvPartition = smtHOFunction "sbv.closurePartition" closureFun
$ \envxs -> [sCase| envxs of
(_, []) -> tuple ([], [])
(cEnv, h : t) -> case sbvPartition (tuple (cEnv, t)) of
(as, bs) | closureFun cEnv h -> tuple (h .: as, bs)
| True -> tuple (as, h .: bs)
|]
takeWhile cls@Closure{closureEnv, closureFun} l
| Just concResult <- concreteTakeWhile cls (closureFun closureEnv) l
= literal concResult
| True
= sbvTakeWhile (tuple (closureEnv, l))
where sbvTakeWhile = smtHOFunction "sbv.closureTakeWhile" closureFun
$ \envxs -> [sCase| envxs of
(_, []) -> []
(cEnv, h : t) | closureFun cEnv h -> h .: sbvTakeWhile (tuple (cEnv, t))
| True -> []
|]
dropWhile cls@Closure{closureEnv, closureFun} l
| Just concResult <- concreteDropWhile cls (closureFun closureEnv) l
= literal concResult
| True
= sbvDropWhile (tuple (closureEnv, l))
where sbvDropWhile = smtHOFunction "sbv.closureDropWhile" closureFun
$ \envxs -> [sCase| envxs of
(_, []) -> []
(cEnv, lst@(h : t)) | closureFun cEnv h -> sbvDropWhile (tuple (cEnv, t))
| True -> lst
|]
-- | @`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 = foldr ((+) @(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 = foldr ((*) @(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
-- | @`enumFromThenTo`@ with an optionally statically-known integer step. The sEnum quasiquoter
-- supplies @`Just` d@ for @[m, m' .. n]@ when @m'@ is @m@ shifted by a compile-time integer
-- constant (e.g. @[m, m-1 .. n]@ gives @-1@); otherwise it supplies `Nothing`. Instances with
-- exact arithmetic (integers, reals) use the hint to constant-fold the step, so the @step == 0@
-- infinite-list branch (and its productive helper) drops out; every other instance ignores the
-- hint and falls back to 'enumFromThenTo', preserving its exact semantics. Not meant to be called
-- directly; the default is correct for any instance.
enumFromThenToH :: SymVal a => SBV a -> SBV a -> SBV a -> Maybe Integer -> SList a
enumFromThenToH from thn to _ = enumFromThenTo from thn to
-- | 'EnumSymbolic' instance for words
instance {-# OVERLAPPABLE #-} (SymVal a, Bounded a, Integral a, Num a, Num (SBV a)) => EnumSymbolic a where
succ = smtFunction "EnumSymbolic.succ" (\x -> ite (x .== maxBound) (some "EnumSymbolic.succ.maxBound" (const sTrue)) (x+1))
pred = smtFunction "EnumSymbolic.pred" (\x -> ite (x .== minBound) (some "EnumSymbolic.pred.minBound" (const sTrue)) (x-1))
toEnum = smtFunction "EnumSymbolic.toEnum" $ \x ->
ite (x .< sFromIntegral (minBound @(SBV a))) (some "EnumSymbolic.toEnum.<minBound" (const sTrue))
$ ite (x .> sFromIntegral (maxBound @(SBV a))) (some "EnumSymbolic.toEnum.>maxBound" (const sTrue))
$ sFromIntegral x
fromEnum = sFromIntegral
enumFrom n = map sFromIntegral (enumFromTo @Integer (sFromIntegral n) (sFromIntegral (maxBound @(SBV a))))
enumFromThen = smtFunction "EnumSymbolic.enumFromThen" $ \n1 n2 ->
let i_n1, i_n2 :: SInteger
i_n1 = sFromIntegral n1
i_n2 = sFromIntegral n2
in map sFromIntegral (ite (i_n2 .>= i_n1)
(enumFromThenTo i_n1 i_n2 (sFromIntegral (maxBound @(SBV a))))
(enumFromThenTo i_n1 i_n2 (sFromIntegral (minBound @(SBV a)))))
enumFromTo n m = map sFromIntegral (enumFromTo @Integer (sFromIntegral n) (sFromIntegral m))
enumFromThenTo n m t = map sFromIntegral (enumFromThenTo @Integer (sFromIntegral n) (sFromIntegral m) (sFromIntegral 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 x = x + 1
pred x = x - 1
toEnum = id
fromEnum = id
enumFrom n = enumFromThen n (n+1)
enumFromTo n m = enumFromThenToInteger n m 1
enumFromThen x y = go x (y-x)
where go = smtProductiveFunction "EnumSymbolic.Integer.enumFromThen" $ \start delta -> start .: go (start+delta) delta
enumFromThenTo x y z = enumFromThenToInteger x z (y - x)
enumFromThenToH x y z mStep = enumFromThenToInteger x z (maybe (y - x) fromIntegral mStep)
-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's
-- if x <= z, and the empty list otherwise. We mirror that here.
enumFromThenToInteger :: SInteger -> SInteger -> SInteger -> SList Integer
enumFromThenToInteger x z delta = ite (delta .== 0)
(ite (x .<= z) (enumFromThen x x) [])
$ ite (delta .> 0) (up x delta z) (down x delta z)
where -- The d==0 case is handled: 'up'/'down' are only *called* with d>0/d<0 (the d==0 case
-- is routed to the infinite-list branch above), and the guard's @d .<= 0@/@d .>= 0@ test
-- puts @d>0@/@d<0@ into the reaching condition, so measure verification never sees d==0.
-- (The integer measure does not divide by d, so there's no zero-denominator to worry about.)
up, down :: SInteger -> SInteger -> SInteger -> SList Integer
up = smtFunctionWithMeasure "EnumSymbolic.Integer.enumFromThenTo.up"
(\start _d end -> 0 `smax` (end - start + 1), [])
$ \start d end -> ite (start .> end .|| d .<= 0) [] (start .: up (start + d) d end)
down = smtFunctionWithMeasure "EnumSymbolic.Integer.enumFromThenTo.down"
(\start _d end -> 0 `smax` (start - end + 1), [])
$ \start d end -> ite (start .< end .|| d .>= 0) [] (start .: down (start + d) d 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 x = x + 1
pred x = x - 1
toEnum = sFromIntegral
fromEnum = fromSFloat sRTZ
enumFrom n = enumFromThen n (n+1)
enumFromTo n m = enumFromThenToFloat n m 1
enumFromThen x y = go 0 x (y-x)
where go = smtProductiveFunction "EnumSymbolic.Float.enumFromThen" $ \k n d -> (n + k * d) .: go (k+1) n d
enumFromThenTo x y zIn = enumFromThenToFloat x zIn (y - x)
-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's
-- if x <= z, and the empty list otherwise. We mirror that here.
enumFromThenToFloat :: SFloat -> SFloat -> SFloat -> SList Float
enumFromThenToFloat x zIn delta = ite (delta .== 0)
(ite (x .<= z) (enumFromThen x x) [])
$ ite (delta .> 0) (up 0 x delta z) (down 0 x delta z)
where z :: SFloat
z = zIn + delta / 2
-- Unlike the Integer/AlgReal instances, these are NOT given a termination measure:
-- floating-point enumeration is genuinely partial. The step @k * d@ can saturate (once
-- @k * d@ falls below the ULP of @n@, or once the float @k@ itself stops incrementing),
-- so for some inputs @n + k * d@ never exceeds @end@ and the recursion does not terminate
-- -- exactly as Haskell's own float enumeration diverges in those cases. A termination
-- measure would therefore be unsound: no measure can certify termination of a function
-- that does not always terminate. Instead we mark these productive -- each recursive call
-- is guarded by a cons, so the definition is well-formed corecursion (finite when the
-- enumeration terminates, infinite when it saturates). The d==0 case never reaches here:
-- it is routed to the infinite-list branch above.
up, down :: SFloat -> SFloat -> SFloat -> SFloat -> SList Float
up = smtProductiveFunction "EnumSymbolic.Float.enumFromThenTo.up"
$ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up (k+1) n d end)
down = smtProductiveFunction "EnumSymbolic.Float.enumFromThenTo.down"
$ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)
-- | 'EnumSymbolic instance for 'Double'
instance {-# OVERLAPPING #-} EnumSymbolic Double where
succ x = x + 1
pred x = x - 1
toEnum = sFromIntegral
fromEnum = fromSDouble sRTZ
enumFrom n = enumFromThen n (n+1)
enumFromTo n m = enumFromThenToDouble n m 1
enumFromThen x y = go 0 x (y-x)
where go = smtProductiveFunction "EnumSymbolic.Double.enumFromThen" $ \k n d -> (n + k * d) .: go (k+1) n d
enumFromThenTo x y zIn = enumFromThenToDouble x zIn (y - x)
-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's
-- if x <= z, and the empty list otherwise. We mirror that here.
enumFromThenToDouble :: SDouble -> SDouble -> SDouble -> SList Double
enumFromThenToDouble x zIn delta = ite (delta .== 0)
(ite (x .<= z) (enumFromThen x x) [])
$ ite (delta .> 0) (up 0 x delta z) (down 0 x delta z)
where z :: SDouble
z = zIn + delta / 2
-- See the Float instance for why these are productive rather than measured:
-- floating-point enumeration is genuinely partial (the @k * d@ step can saturate), so a
-- termination measure would be unsound. Each recursive call is guarded by a cons, so the
-- definition is well-formed corecursion. The d==0 case is routed to the branch above.
up, down :: SDouble -> SDouble -> SDouble -> SDouble -> SList Double
up = smtProductiveFunction "EnumSymbolic.Double.enumFromThenTo.up"
$ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up (k+1) n d end)
down = smtProductiveFunction "EnumSymbolic.Double.enumFromThenTo.down"
$ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)
-- | 'EnumSymbolic instance for arbitrary floats
instance {-# OVERLAPPING #-} ValidFloat eb sb => EnumSymbolic (FloatingPoint eb sb) where
succ x = x + 1
pred x = x - 1
toEnum = sFromIntegral
fromEnum = fromSFloatingPoint sRTZ
enumFrom n = enumFromThen n (n+1)
enumFromTo n m = enumFromThenToFloatingPoint n m 1
enumFromThen x y = go 0 x (y-x)
where go = smtProductiveFunction "EnumSymbolic.FloatingPoint.enumFromThen" $ \k n d -> (n + k * d) .: go (k+1) n d
enumFromThenTo x y zIn = enumFromThenToFloatingPoint x zIn (y - x)
-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's
-- if x <= z, and the empty list otherwise. We mirror that here.
enumFromThenToFloatingPoint :: forall eb sb. ValidFloat eb sb => SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SList (FloatingPoint eb sb)
enumFromThenToFloatingPoint x zIn delta = ite (delta .== 0)
(ite (x .<= z) (enumFromThen x x) [])
$ ite (delta .> 0) (up 0 x delta z) (down 0 x delta z)
where z :: SFloatingPoint eb sb
z = zIn + delta / 2
-- See the Float instance for why these are productive rather than measured:
-- floating-point enumeration is genuinely partial (the @k * d@ step can saturate), so a
-- termination measure would be unsound. Each recursive call is guarded by a cons, so the
-- definition is well-formed corecursion. The d==0 case is routed to the branch above.
up, down :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SList (FloatingPoint eb sb)
up = smtProductiveFunction "EnumSymbolic.FloatingPoint.enumFromThenTo.up"
$ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up (k+1) n d end)
down = smtProductiveFunction "EnumSymbolic.FloatingPoint.enumFromThenTo.down"
$ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d 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 x = x + 1
pred x = x - 1
toEnum = sFromIntegral
fromEnum = sRealToSIntegerTruncate
enumFrom n = enumFromThen n (n+1)
enumFromTo n m = enumFromThenToAlgReal n m 1
enumFromThen x y = go x (y-x)
where go = smtProductiveFunction "EnumSymbolic.AlgReal.enumFromThen" $ \start delta -> start .: go (start+delta) delta
enumFromThenTo x y zIn = enumFromThenToAlgReal x zIn (y - x)
enumFromThenToH x y zIn mStep = enumFromThenToAlgReal x zIn (maybe (y - x) fromIntegral mStep)
-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's
-- if x <= z, and the empty list otherwise. We mirror that here.
enumFromThenToAlgReal :: SReal -> SReal -> SReal -> SList AlgReal
enumFromThenToAlgReal x zIn delta = ite (delta .== 0)
(ite (x .<= z) (enumFromThen x x) [])
$ ite (delta .> 0) (up x delta z) (down x delta z)
where z :: SReal
z = zIn + delta / 2
-- The measure is the number of remaining recursive steps, which is an INTEGER:
-- @floor ((end - start) / d) + 1@ (clamped at 0). A real-valued measure would be
-- unsound here, since the reals are not well-ordered (an infinite descending chain
-- like 1, 1/2, 1/4, ... never reaches a minimum). 'sRealToSInteger' is @floor@, and
-- @(end - start) / d@ is non-negative in both the up (d>0) and down (d<0) regimes, so
-- the same expression serves both.
--
-- The d==0 case is handled: 'up'/'down' are only *called* with d>0/d<0 (the d==0 case is
-- routed to the infinite-list branch above), and for measure *verification* the guard's
-- @d .<= 0@/@d .>= 0@ test puts @d>0@/@d<0@ into the reaching condition, so the decrease
-- obligation never sees d==0; the @0 `smax`@ keeps non-negativity vacuously true even for
-- the unreachable zero-denominator value of @(end - start) / d@.
up, down :: SReal -> SReal -> SReal -> SList AlgReal
up = smtFunctionWithMeasure "EnumSymbolic.AlgReal.enumFromThenTo.up" (\start d end -> 0 `smax` (sRealToSInteger ((end - start) / d) + 1), [])
$ \start d end -> ite (start .> end .|| d .<= 0) [] (start .: up (start + d) d end)
down = smtFunctionWithMeasure "EnumSymbolic.AlgReal.enumFromThenTo.down" (\start d end -> 0 `smax` (sRealToSInteger ((end - start) / d) + 1), [])
$ \start d end -> ite (start .< end .|| d .>= 0) [] (start .: down (start + d) d 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:
-- sbv.lookup_notFound @Integer = 0 :: Integer
-- s0 = 1 :: Integer
lookup :: (SymVal k, SymVal v) => SBV k -> SList (k, v) -> SBV v
lookup = smtFunction "sbv.lookup"
$ \k lst -> [sCase| lst of
[] -> some "sbv.lookup_notFound" (const sTrue)
(k', v) : rest | k .== k' -> v
| True -> lookup k rest
|]
-- | @`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 s
| Just a <- unliteral s
= if P.all C.isDigit a && not (P.null a)
then literal (read a)
else -1
| True
= lift1Str StrStrToNat Nothing 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 i
| Just v <- unliteral i
= literal $ if v >= 0 then show v else ""
| True
= lift1Str StrNatToStr Nothing 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 simpleEq w mbOp a
| Just cv <- concEval1 simpleEq mbOp a
= cv
| True
= SBV $ SVal k $ Right $ cache r
where k = kindOf (Proxy @b)
r st = do sva <- sbvToSV st a
newExpr st k (SBVApp (SeqOp w) [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 simpleEq w mbOp a b
| Just cv <- concEval2 simpleEq mbOp a b
= cv
| True
= SBV $ SVal k $ Right $ cache r
where k = kindOf (Proxy @c)
r st = do sva <- sbvToSV st a
svb <- sbvToSV st b
newExpr st k (SBVApp (SeqOp w) [sva, 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 simpleEq w mbOp a b c
| Just cv <- concEval3 simpleEq mbOp a b c
= cv
| True
= SBV $ SVal k $ Right $ cache r
where k = kindOf (Proxy @d)
r st = do sva <- sbvToSV st a
svb <- sbvToSV st b
svc <- sbvToSV st c
newExpr st k (SBVApp (SeqOp w) [sva, svb, svc])
-- | Concrete evaluation for unary ops
concEval1 :: forall a b. (SymVal a, SymVal b) => Bool -> Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 simpleEq mbOp a
| not simpleEq || eqCheckIsObjectEq (kindOf (Proxy @a)) = literal <$> (mbOp <*> unliteral a)
| True = 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 simpleEq mbOp a b
| not simpleEq || eqCheckIsObjectEq (kindOf (Proxy @a)) = literal <$> (mbOp <*> unliteral a <*> unliteral b)
| True = 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 simpleEq mbOp a b c
| not simpleEq || eqCheckIsObjectEq (kindOf (Proxy @a)) = literal <$> (mbOp <*> unliteral a <*> unliteral b <*> unliteral c)
| True = Nothing
-- | Is the list concretely known empty?
isConcretelyEmpty :: SymVal a => SList a -> Bool
isConcretelyEmpty sl | Just l <- unliteral sl = P.null l
| True = False
-- | Lift a unary operator over strings.
lift1Str :: forall a b. (SymVal a, SymVal b) => StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1Str w mbOp a
| Just cv <- literal <$> (mbOp <*> unliteral a)
= cv
| True
= SBV $ SVal k $ Right $ cache r
where k = kindOf (Proxy @b)
r st = do sva <- sbvToSV st a
newExpr st k (SBVApp (StrOp w) [sva])
{- HLint ignore implode "Use :" -}
{- HLint ignore replicate "Use const" -}