Skip to content

Instantly share code, notes, and snippets.

@LeventErkok
Created September 19, 2018 03:57
Show Gist options
  • Save LeventErkok/78fd03ec4f2199a0806fe7ffc6e48e78 to your computer and use it in GitHub Desktop.
Save LeventErkok/78fd03ec4f2199a0806fe7ffc6e48e78 to your computer and use it in GitHub Desktop.
Bounded symbolic lists
{-# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment