Bounded symbolic lists

BoundedLists.hs

{-# LANGUAGE OverloadedLists #-}

import Data.SBV
import Data.SBV.List ((.++), (.:))
import qualified Data.SBV.List as L

import Data.Typeable

lcase :: (Typeable a, SymWord a, Mergeable b) => SList a -> b -> (SBV a -> SList a -> b) -> b
lcase s e c = ite (L.null s) e (c (L.head s) (L.tail s))

bfold :: (Typeable a, SymWord a, SymWord b)
      => Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
bfold cnt f b = go cnt
  where go 0 _ = b
        go i s = lcase s b (\h t -> f h (go (i-1) t))

bsum    i   = bfold i (+) 0
bprod   i   = bfold i (*) 1
bmap    i f = bfold i (\x -> (f x .:)) []
bfilter i f = bfold i (\x y -> ite (f x) (x .: y) y) []
band    i   = bfold i (&&&) (true  :: SBool)
bor     i   = bfold i (|||) (false :: SBool)