{-|
Module: Data.Searchable 
Description: exhaustively searchable subsets
Maintainer: Olaf Klinke
Stability: experimental

There exist two packages for exhaustive search: 
[infinite-search](https://hackage.haskell.org/package/infinite-search)
and the 
[Select](https://hackage.haskell.org/package/transformers-0.6.1.2/docs/Control-Monad-Trans-Select.html)
monad transformer. 

This module extends the former (which has a much smaller dependency footprint) 
with the empty subset. 
The resulting monad 'K' does not only support unions 
but also intersections. 
-} 
module Data.Searchable (
    -- * Data types
    K(..),
    -- Set Operations
    restrict,
    intersection,
    -- * Queries
    exists,forevery,member,
    -- * Construction
    list2K) where
import Control.Applicative (Alternative(..))
import Control.Monad (MonadPlus(..),ap)
import Data.Set (Set)
import qualified Data.Set
import Data.List (intercalate)

-- | If sub-sets of a type admit 
-- continuous universal quantification ∀, 
-- then the empty sub-set is an isolated element: 
-- Indeed, for no other set should @∀ ('const' 'False')@ be true. 
-- 
-- Therefore it is sound to have a separate constructor for the empty set.
data K a = Emptyset 
    | Nonempty ((a -> Bool) -> a) -- ^ selection function

-- | The non-empty part of 'K'.
data S a = Finder {forall a. S a -> (a -> Bool) -> a
find :: (a -> Bool) -> a}

-- | existential quantification
exists :: K a -> (a -> Bool) -> Bool
exists :: forall a. K a -> (a -> Bool) -> Bool
exists K a
Emptyset a -> Bool
_ = Bool
False
exists (Nonempty (a -> Bool) -> a
f) a -> Bool
p = a -> Bool
p ((a -> Bool) -> a
f a -> Bool
p)

-- | universal quantification
forevery :: K a -> (a -> Bool) -> Bool
forevery :: forall a. K a -> (a -> Bool) -> Bool
forevery K a
k = \a -> Bool
p -> Bool -> Bool
not (K a -> (a -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
exists K a
k (Bool -> Bool
not(Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.a -> Bool
p))

s2k :: S a -> K a
s2k :: forall a. S a -> K a
s2k = ((a -> Bool) -> a) -> K a
forall a. ((a -> Bool) -> a) -> K a
Nonempty (((a -> Bool) -> a) -> K a)
-> (S a -> (a -> Bool) -> a) -> S a -> K a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. S a -> (a -> Bool) -> a
forall a. S a -> (a -> Bool) -> a
find

union :: K (K a) -> K a
union :: forall a. K (K a) -> K a
union K (K a)
Emptyset = K a
forall a. K a
Emptyset -- ⋃ ∅ = ∅
union (Nonempty (K a -> Bool) -> K a
ff) = case (K a -> Bool) -> K a
ff (Bool -> K a -> Bool
forall a b. a -> b -> a
const Bool
True) of
    K a
Emptyset   -> K a
forall a. K a
Emptyset -- ⋃ {∅} = ∅
    Nonempty (a -> Bool) -> a
f -> ((a -> Bool) -> a) -> K a
forall a. ((a -> Bool) -> a) -> K a
Nonempty (\a -> Bool
p -> case (K a -> Bool) -> K a
ff (\K a
k -> K a -> (a -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
exists K a
k a -> Bool
p) of
        K a
Emptyset       -> (a -> Bool) -> a
f     a -> Bool
p
        Nonempty (a -> Bool) -> a
find' -> (a -> Bool) -> a
find' a -> Bool
p)

instance Functor K where
    fmap :: forall a b. (a -> b) -> K a -> K b
fmap a -> b
_ K a
Emptyset = K b
forall a. K a
Emptyset
    fmap a -> b
h (Nonempty (a -> Bool) -> a
f) = ((b -> Bool) -> b) -> K b
forall a. ((a -> Bool) -> a) -> K a
Nonempty (\b -> Bool
p -> (a -> b
h(a -> b) -> ((a -> Bool) -> a) -> (a -> Bool) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(a -> Bool) -> a
f) (b -> Bool
p(b -> Bool) -> (a -> b) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.a -> b
h))
instance Functor S where
    fmap :: forall a b. (a -> b) -> S a -> S b
fmap a -> b
f S a
s = ((b -> Bool) -> b) -> S b
forall a. ((a -> Bool) -> a) -> S a
Finder (\b -> Bool
p -> (a -> b
f(a -> b) -> ((a -> Bool) -> a) -> (a -> Bool) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(S a -> (a -> Bool) -> a
forall a. S a -> (a -> Bool) -> a
find S a
s)) (b -> Bool
p(b -> Bool) -> (a -> b) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.a -> b
f))
instance Monad K where
    return :: forall a. a -> K a
return = a -> K a
forall a. a -> K a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    K a
s >>= :: forall a b. K a -> (a -> K b) -> K b
>>= a -> K b
k = K (K b) -> K b
forall a. K (K a) -> K a
union ((a -> K b) -> K a -> K (K b)
forall a b. (a -> b) -> K a -> K b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> K b
k K a
s)
instance Monad S where
    return :: forall a. a -> S a
return = a -> S a
forall a. a -> S a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    (Finder (a -> Bool) -> a
fnd) >>= :: forall a b. S a -> (a -> S b) -> S b
>>= a -> S b
k = ((b -> Bool) -> b) -> S b
forall a. ((a -> Bool) -> a) -> S a
Finder (\b -> Bool
p -> let 
        f :: a -> b
f = (a -> (b -> Bool) -> b) -> (b -> Bool) -> a -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (S b -> (b -> Bool) -> b
forall a. S a -> (a -> Bool) -> a
find(S b -> (b -> Bool) -> b) -> (a -> S b) -> a -> (b -> Bool) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
.a -> S b
k) b -> Bool
p
        in a -> b
f ((a -> Bool) -> a
fnd (b -> Bool
p(b -> Bool) -> (a -> b) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.a -> b
f)))
instance Alternative K where
    empty :: forall a. K a
empty = K a
forall a. K a
Emptyset
    K a
Emptyset <|> :: forall a. K a -> K a -> K a
<|> K a
k = K a
k
    k :: K a
k@(Nonempty (a -> Bool) -> a
_) <|> K a
Emptyset = K a
k
    (Nonempty (a -> Bool) -> a
f) <|> (Nonempty (a -> Bool) -> a
g) = ((a -> Bool) -> a) -> K a
forall a. ((a -> Bool) -> a) -> K a
Nonempty (\a -> Bool
p -> let a :: a
a = (a -> Bool) -> a
f a -> Bool
p in if a -> Bool
p a
a then a
a else (a -> Bool) -> a
g a -> Bool
p)
instance MonadPlus K where
    mzero :: forall a. K a
mzero = K a
forall a. K a
Emptyset
    mplus :: forall a. K a -> K a -> K a
mplus = K a -> K a -> K a
forall a. K a -> K a -> K a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>)
instance Applicative K where
    pure :: forall a. a -> K a
pure = ((a -> Bool) -> a) -> K a
forall a. ((a -> Bool) -> a) -> K a
Nonempty (((a -> Bool) -> a) -> K a) -> (a -> (a -> Bool) -> a) -> a -> K a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (a -> Bool) -> a
forall a b. a -> b -> a
const
    <*> :: forall a b. K (a -> b) -> K a -> K b
(<*>) = K (a -> b) -> K a -> K b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Applicative S where
    pure :: forall a. a -> S a
pure = ((a -> Bool) -> a) -> S a
forall a. ((a -> Bool) -> a) -> S a
Finder (((a -> Bool) -> a) -> S a) -> (a -> (a -> Bool) -> a) -> a -> S a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (a -> Bool) -> a
forall a b. a -> b -> a
const
    <*> :: forall a b. S (a -> b) -> S a -> S b
(<*>) = S (a -> b) -> S a -> S b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance (Ord a,Show a) => Show (K a) where
    show :: K a -> String
show K a
k = Char
'{'Char -> ShowS
forall a. a -> [a] -> [a]
:(String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ([String] -> String) -> (K a -> [String]) -> K a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show ([a] -> [String]) -> (K a -> [a]) -> K a -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
forall a. Set a -> [a]
Data.Set.toList (Set a -> [a]) -> (K a -> Set a) -> K a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K a -> Set a
forall a. Ord a => K a -> Set a
k2Set (K a -> String) -> K a -> String
forall a b. (a -> b) -> a -> b
$ K a
k)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
"}"
instance (Ord a,Show a) => Show (S a) where
    show :: S a -> String
show = K a -> String
forall a. Show a => a -> String
show(K a -> String) -> (S a -> K a) -> S a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.S a -> K a
forall a. S a -> K a
s2k
instance (Eq a) => Eq (K a) where
    == :: K a -> K a -> Bool
(==) = (a -> a -> Bool) -> K a -> K a -> Bool
forall a b. (a -> b -> Bool) -> K a -> K b -> Bool
egliMilner a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

-- | membership is decidable for discrete spaces
member :: Eq a => a -> K a -> Bool
member :: forall a. Eq a => a -> K a -> Bool
member = (K a -> a -> Bool) -> a -> K a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip K a -> a -> Bool
forall a. Eq a => K a -> a -> Bool
contains

-- | In a discrete space, compact sets are clopen. 
contains :: Eq a => K a -> a -> Bool
K a
k contains :: forall a. Eq a => K a -> a -> Bool
`contains` a
x = K a -> (a -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
exists K a
k (a
xa -> a -> Bool
forall a. Eq a => a -> a -> Bool
==)

-- | Intersect a compact with a clopen
restrict :: K a -> (a -> Bool) -> K a -- intersect a compact with a clopen.
restrict :: forall a. K a -> (a -> Bool) -> K a
restrict K a
Emptyset a -> Bool
_ = K a
forall a. K a
Emptyset
restrict k :: K a
k@(Nonempty (a -> Bool) -> a
f) a -> Bool
p = if K a -> (a -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
forevery K a
k (Bool -> Bool
not(Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.a -> Bool
p)
    then K a
forall a. K a
Emptyset
    else ((a -> Bool) -> a) -> K a
forall a. ((a -> Bool) -> a) -> K a
Nonempty (\a -> Bool
q -> (a -> Bool) -> a
f (\a
a -> a -> Bool
p a
a Bool -> Bool -> Bool
&& a -> Bool
q a
a))

-- | If every compact set is clopen, then the space is discrete. 
-- Indeed, discreteness means singletons are open. 
-- Singletons are always compact. 
intersection :: Eq a => K a -> K a -> K a
intersection :: forall a. Eq a => K a -> K a -> K a
intersection K a
Emptyset K a
_ = K a
forall a. K a
Emptyset
intersection K a
_ K a
Emptyset = K a
forall a. K a
Emptyset
intersection K a
k1 K a
k2 = K a -> (a -> Bool) -> K a
forall a. K a -> (a -> Bool) -> K a
restrict K a
k1 (K a -> a -> Bool
forall a. Eq a => K a -> a -> Bool
contains K a
k2)

-- | if k is compact, then so is {x} ∪ k
consK :: a -> K a -> K a
consK :: forall a. a -> K a -> K a
consK a
x K a
Emptyset = a -> K a
forall a. a -> K a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
consK a
x (Nonempty (a -> Bool) -> a
f) = ((a -> Bool) -> a) -> K a
forall a. ((a -> Bool) -> a) -> K a
Nonempty (\a -> Bool
p -> if a -> Bool
p a
x then a
x else (a -> Bool) -> a
f a -> Bool
p)

-- | convert lists
-- 
-- >>> list2K [4,2,2,2,3 :: Integer]
-- {2,3,4}
list2K :: Foldable f => f a -> K a
list2K :: forall (f :: * -> *) a. Foldable f => f a -> K a
list2K = (a -> K a -> K a) -> K a -> f a -> K a
forall a b. (a -> b -> b) -> b -> f a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> K a -> K a
forall a. a -> K a -> K a
consK K a
forall a. K a
Emptyset

k2Set :: Ord a => K a -> Set a
k2Set :: forall a. Ord a => K a -> Set a
k2Set K a
k = Set a -> K a -> Set a
forall {a}. Ord a => Set a -> K a -> Set a
go Set a
forall a. Set a
Data.Set.empty K a
k where
    go :: Set a -> K a -> Set a
go Set a
s K a
Emptyset = Set a
s
    go Set a
s (Nonempty (a -> Bool) -> a
f) = let x :: a
x = (a -> Bool) -> a
f ((a -> Set a -> Bool) -> Set a -> a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Data.Set.notMember Set a
s) in
        if a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> Bool) -> a
f (a
xa -> a -> Bool
forall a. Eq a => a -> a -> Bool
==)
            then let s' :: Set a
s' = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Data.Set.insert a
x Set a
s in Set a -> K a -> Set a
go 
                Set a
s'
                (K a -> (a -> Bool) -> K a
forall a. K a -> (a -> Bool) -> K a
restrict (((a -> Bool) -> a) -> K a
forall a. ((a -> Bool) -> a) -> K a
Nonempty (a -> Bool) -> a
f) ((a -> Set a -> Bool) -> Set a -> a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Data.Set.notMember Set a
s'))
            else Set a
s

-- * Relation liftings

-- | Smyth relation lifting
smyth :: (a -> b -> Bool) -> K a -> K b -> Bool
smyth :: forall a b. (a -> b -> Bool) -> K a -> K b -> Bool
smyth a -> b -> Bool
r K a
xs K b
ys = K b -> (b -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
forevery K b
ys ((K a -> (a -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
exists K a
xs)((a -> Bool) -> Bool) -> (b -> a -> Bool) -> b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.((a -> b -> Bool) -> b -> a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> b -> Bool
r))
-- | Hoare relation lifting
hoare :: (a -> b -> Bool) -> K a -> K b -> Bool
hoare :: forall a b. (a -> b -> Bool) -> K a -> K b -> Bool
hoare a -> b -> Bool
r K a
xs K b
ys = K a -> (a -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
forevery K a
xs ((K b -> (b -> Bool) -> Bool
forall a. K a -> (a -> Bool) -> Bool
exists K b
ys)((b -> Bool) -> Bool) -> (a -> b -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.a -> b -> Bool
r)
-- | Egli-Milner relation lifting
egliMilner :: (a -> b -> Bool) -> K a -> K b -> Bool
egliMilner :: forall a b. (a -> b -> Bool) -> K a -> K b -> Bool
egliMilner a -> b -> Bool
r K a
xs K b
ys = (a -> b -> Bool) -> K a -> K b -> Bool
forall a b. (a -> b -> Bool) -> K a -> K b -> Bool
hoare a -> b -> Bool
r K a
xs K b
ys Bool -> Bool -> Bool
&& (a -> b -> Bool) -> K a -> K b -> Bool
forall a b. (a -> b -> Bool) -> K a -> K b -> Bool
smyth a -> b -> Bool
r K a
xs K b
ys