```{-# LANGUAGE DeriveFunctor, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, MultiWayIf, RecordWildCards, ScopedTypeVariables, TupleSections #-}

-- | This package provides combinators to construct many variants of
-- binary search.  Most generally, it provides the binary search over
-- predicate of the form @('Eq' b, 'Monad' m) => a -> m b@. The other
-- searches are derived as special cases of this function.
--
-- 'BinarySearch' assumes two things;
--
-- 1. @b@, the codomain of 'PredicateM' belongs to type class 'Eq'.
--
-- 2. Each value of @b@ form a convex set in the codomain space of the
-- PredicateM. That is, if for certain pair @(left, right) :: (a, a)@
-- satisfies @pred left == val && pred right == val@, then also @pred
-- x == val@ for all @x@ such that @left <= x <= right@.
--
-- __Example 1.__ Find the approximate square root of 3.
--
-- >>> largest  True  \$ search positiveExponential divForever (\x -> x^2 < 3000000)
-- Just 1732
-- >>> smallest False \$ search positiveExponential divForever (\x -> x^2 < 3000000)
-- Just 1733
-- >>> largest  True  \$ search positiveExponential divideForever (\x -> x^2 < (3::Double))
-- Just 1.7320508075688772
-- >>> largest  True  \$ search positiveExponential (divideTill 0.125) (\x -> x^2 < (3::Double))
-- Just 1.625
-- >>> smallest False \$ search positiveExponential (divideTill 0.125) (\x -> x^2 < (3::Double))
-- Just 1.75
--
-- Pay attention to use the appropriate exponential search combinator to set up the initial search range.
-- For example, the following code works as expected:
--
-- >>> largest  True  \$ search nonNegativeExponential divideForever (\x -> x^2 < (0.5::Double))
-- Just 0.7071067811865475
--
-- But this one does not terminate:
--
-- @
-- __> largest  True  \$ search positiveExponential divideForever (\x -> x^2 < (0.5::Double))__
-- ... runs forever ...
-- @
--
-- __Example 2.__ Find the range of integers whose quotinent 7 is equal to 6.
--
-- This is an example of how we can 'search' for discete and multi-valued predicate.
--
-- >>> smallest 6 \$ search (fromTo 0 100) divForever (\x -> x `div` 7)
-- Just 42
-- >>> largest  6 \$ search (fromTo 0 100) divForever (\x -> x `div` 7)
-- Just 48
--
-- __Example 3.__ Find the minimum size of the container that can fit three bars of length 4,
-- and find an actual way to fit them.
--
-- We will solve this using a satisfiability modulo theory (SMT) solver. Since we need to evoke 'IO'
-- to call for the SMT solver,
-- This is a usecase for a monadic binary search.
--
-- >>> import Data.List (isPrefixOf)
-- >>> :{
-- do
--   -- x fits within the container
--   let x ⊂ r = (0 .<= x &&& x .<= r-4)
--   -- x and y does not collide
--   let x ∅ y = (x+4 .<= y )
--   let contain3 :: Integer -> IO (Evidence () String)
--       contain3 r' = do
--         let r = fromInteger r' :: SInteger
--         ret <- show <\$> sat (\x y z -> bAnd [x ⊂ r, y ⊂ r, z ⊂ r, x ∅ y, y ∅ z])
--         if "Satisfiable" `isPrefixOf` ret
--           then return \$ Evidence ret
--           else return \$ CounterEvidence ()
--   Just sz  <- smallest evidence <\$> searchM positiveExponential divForever contain3
--   putStrLn \$ "Size of the container: " ++ show sz
--   Just msg <- evidenceForSmallest <\$> searchM positiveExponential divForever contain3
--   putStrLn msg
-- :}
-- Size of the container: 12
-- Satisfiable. Model:
--   s0 = 0 :: Integer
--   s1 = 4 :: Integer
--   s2 = 8 :: Integer

module Numeric.Search where

import           Control.Applicative
import           Data.Functor.Identity
import           Data.Maybe (fromJust, listToMaybe)
import           Prelude hiding (init, pred)

-- \$setup
-- All the doctests in this document assume:
--
-- >>> :set -XFlexibleContexts
-- >>> import Data.SBV

-- * Evidence

-- | The 'Evidence' datatype is similar to 'Either' , but differes in that all 'CounterEvidence' values are
--   equal to each other, and all 'Evidence' values are also
--   equal to each other. The 'Evidence' type is used to binary-searching for some predicate and meanwhile returning evidences for that.
--
-- In other words, 'Evidence' is a 'Bool' with additional information why it is 'True' or 'False'.
--
-- >>> Evidence "He owns the gun" == Evidence "He was at the scene"
-- True
-- >>> Evidence "He loved her" == CounterEvidence "He loved her"
-- False

data Evidence a b = CounterEvidence a | Evidence b
deriving (Int -> Evidence a b -> ShowS
[Evidence a b] -> ShowS
Evidence a b -> String
(Int -> Evidence a b -> ShowS)
-> (Evidence a b -> String)
-> ([Evidence a b] -> ShowS)
-> Show (Evidence a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> Evidence a b -> ShowS
forall a b. (Show a, Show b) => [Evidence a b] -> ShowS
forall a b. (Show a, Show b) => Evidence a b -> String
showList :: [Evidence a b] -> ShowS
\$cshowList :: forall a b. (Show a, Show b) => [Evidence a b] -> ShowS
show :: Evidence a b -> String
\$cshow :: forall a b. (Show a, Show b) => Evidence a b -> String
showsPrec :: Int -> Evidence a b -> ShowS
\$cshowsPrec :: forall a b. (Show a, Show b) => Int -> Evidence a b -> ShowS
Int -> ReadS (Evidence a b)
(Int -> ReadS (Evidence a b))
forall a.
Read, a -> Evidence a b -> Evidence a a
(a -> b) -> Evidence a a -> Evidence a b
(forall a b. (a -> b) -> Evidence a a -> Evidence a b)
-> (forall a b. a -> Evidence a b -> Evidence a a)
-> Functor (Evidence a)
forall a b. a -> Evidence a b -> Evidence a a
forall a b. (a -> b) -> Evidence a a -> Evidence a b
forall a a b. a -> Evidence a b -> Evidence a a
forall a a b. (a -> b) -> Evidence a a -> Evidence a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<\$ :: a -> Evidence a b -> Evidence a a
\$c<\$ :: forall a a b. a -> Evidence a b -> Evidence a a
fmap :: (a -> b) -> Evidence a a -> Evidence a b
\$cfmap :: forall a a b. (a -> b) -> Evidence a a -> Evidence a b
Functor)

instance Eq (Evidence b a) where
CounterEvidence b
_ == :: Evidence b a -> Evidence b a -> Bool
== CounterEvidence b
_ = Bool
True
Evidence a
_        == Evidence a
_        = Bool
True
Evidence b a
_                 == Evidence b a
_                 = Bool
False

instance Ord (Evidence b a) where
CounterEvidence b
_ compare :: Evidence b a -> Evidence b a -> Ordering
`compare` CounterEvidence b
_ = Ordering
EQ
Evidence a
_        `compare` Evidence a
_        = Ordering
EQ
CounterEvidence b
_ `compare` Evidence a
_        = Ordering
GT
Evidence a
_        `compare` CounterEvidence b
_ = Ordering
LT

instance Applicative (Evidence e) where
pure :: a -> Evidence e a
pure                     = a -> Evidence e a
forall e a. a -> Evidence e a
Evidence
CounterEvidence  e
e <*> :: Evidence e (a -> b) -> Evidence e a -> Evidence e b
<*> Evidence e a
_ = e -> Evidence e b
forall a b. a -> Evidence a b
CounterEvidence e
e
Evidence a -> b
f <*> Evidence e a
r         = (a -> b) -> Evidence e a -> Evidence e b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Evidence e a
r

return :: a -> Evidence e a
return                   = a -> Evidence e a
forall e a. a -> Evidence e a
Evidence
CounterEvidence  e
l >>= :: Evidence e a -> (a -> Evidence e b) -> Evidence e b
>>= a -> Evidence e b
_ = e -> Evidence e b
forall a b. a -> Evidence a b
CounterEvidence e
l
Evidence a
r >>= a -> Evidence e b
k         = a -> Evidence e b
k a
r

-- | 'evidence' = 'Evidence' 'undefined'. We can use this combinator to look up for some 'Evidence',
-- since all 'Evidence's are equal.
evidence :: Evidence a b
evidence :: Evidence a b
evidence = b -> Evidence a b
forall e a. a -> Evidence e a
Evidence b
forall a. HasCallStack => a
undefined

-- | 'counterEvidence' = 'CounterEvidence' 'undefined'. We can use this combinator to look up for any 'CounterEvidence',
-- since all 'CounterEvidence's are equal.
counterEvidence :: Evidence a b
counterEvidence :: Evidence a b
counterEvidence = a -> Evidence a b
forall a b. a -> Evidence a b
CounterEvidence a
forall a. HasCallStack => a
undefined

-- * Search range

-- | The @Range k lo  k' hi@ represents the search result that @pred x == k@ for @lo <= x <= hi@.
-- The 'Range' type also holds the evidences for the lower and the upper boundary.

data Range b a = Range {Range b a -> b
loKey :: b, Range b a -> a
loVal :: a, Range b a -> b
hiKey :: b, Range b a -> a
hiVal :: a}
deriving (Int -> Range b a -> ShowS
[Range b a] -> ShowS
Range b a -> String
(Int -> Range b a -> ShowS)
-> (Range b a -> String)
-> ([Range b a] -> ShowS)
-> Show (Range b a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall b a. (Show b, Show a) => Int -> Range b a -> ShowS
forall b a. (Show b, Show a) => [Range b a] -> ShowS
forall b a. (Show b, Show a) => Range b a -> String
showList :: [Range b a] -> ShowS
\$cshowList :: forall b a. (Show b, Show a) => [Range b a] -> ShowS
show :: Range b a -> String
\$cshow :: forall b a. (Show b, Show a) => Range b a -> String
showsPrec :: Int -> Range b a -> ShowS
\$cshowsPrec :: forall b a. (Show b, Show a) => Int -> Range b a -> ShowS
Int -> ReadS (Range b a)
(Int -> ReadS (Range b a))
forall a.
Read, Range b a -> Range b a -> Bool
(Range b a -> Range b a -> Bool)
-> (Range b a -> Range b a -> Bool) -> Eq (Range b a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall b a. (Eq b, Eq a) => Range b a -> Range b a -> Bool
/= :: Range b a -> Range b a -> Bool
\$c/= :: forall b a. (Eq b, Eq a) => Range b a -> Range b a -> Bool
== :: Range b a -> Range b a -> Bool
\$c== :: forall b a. (Eq b, Eq a) => Range b a -> Range b a -> Bool
Eq, Eq (Range b a)
Eq (Range b a)
-> (Range b a -> Range b a -> Ordering)
-> (Range b a -> Range b a -> Bool)
-> (Range b a -> Range b a -> Bool)
-> (Range b a -> Range b a -> Bool)
-> (Range b a -> Range b a -> Bool)
-> (Range b a -> Range b a -> Range b a)
-> (Range b a -> Range b a -> Range b a)
-> Ord (Range b a)
Range b a -> Range b a -> Bool
Range b a -> Range b a -> Ordering
Range b a -> Range b a -> Range b a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall b a. (Ord b, Ord a) => Eq (Range b a)
forall b a. (Ord b, Ord a) => Range b a -> Range b a -> Bool
forall b a. (Ord b, Ord a) => Range b a -> Range b a -> Ordering
forall b a. (Ord b, Ord a) => Range b a -> Range b a -> Range b a
min :: Range b a -> Range b a -> Range b a
\$cmin :: forall b a. (Ord b, Ord a) => Range b a -> Range b a -> Range b a
max :: Range b a -> Range b a -> Range b a
\$cmax :: forall b a. (Ord b, Ord a) => Range b a -> Range b a -> Range b a
>= :: Range b a -> Range b a -> Bool
\$c>= :: forall b a. (Ord b, Ord a) => Range b a -> Range b a -> Bool
> :: Range b a -> Range b a -> Bool
\$c> :: forall b a. (Ord b, Ord a) => Range b a -> Range b a -> Bool
<= :: Range b a -> Range b a -> Bool
\$c<= :: forall b a. (Ord b, Ord a) => Range b a -> Range b a -> Bool
< :: Range b a -> Range b a -> Bool
\$c< :: forall b a. (Ord b, Ord a) => Range b a -> Range b a -> Bool
compare :: Range b a -> Range b a -> Ordering
\$ccompare :: forall b a. (Ord b, Ord a) => Range b a -> Range b a -> Ordering
\$cp1Ord :: forall b a. (Ord b, Ord a) => Eq (Range b a)
Ord)

-- | The (possibly infinite) lists of candidates for lower and upper bounds from which the search may be started.
type SearchRange a = ([a], [a])

-- | Set the lower and upper boundary from those available from the candidate lists.
-- From the pair of list, the @initializeSearchM@ tries to find the first @(lo, hi)@
-- such that @pred lo /= pred hi@, by the breadth-first search.

initializeSearchM :: (Monad m, Eq b)=> SearchRange a -> (a -> m b) -> m [Range b a]
initializeSearchM :: SearchRange a -> (a -> m b) -> m [Range b a]
initializeSearchM (a
lo:[a]
los,a
hi:[a]
his) a -> m b
pred0 = do
b
pLo <- a -> m b
pred0 a
lo
b
pHi <- a -> m b
pred0 a
hi
let
pop :: (b, a, [a]) -> m (b, a, [a])
pop (b
p,a
x, []) = (b, a, [a]) -> m (b, a, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return (b
p,a
x,[])
pop (b
p,a
_, a
x2:[a]
xs) = do
b
p2 <- a -> m b
pred0 a
x2
(b, a, [a]) -> m (b, a, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return (b
p2, a
x2, [a]
xs)

go :: (b, a, [a]) -> (b, a, [a]) -> m [Range b a]
go pez1 :: (b, a, [a])
pez1@(b
p1,a
x1,[a]
xs1) pez2 :: (b, a, [a])
pez2@(b
p2,a
x2,[a]
xs2)
| b
p1 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
/= b
p2             = [Range b a] -> m [Range b a]
forall (m :: * -> *) a. Monad m => a -> m a
return [b -> a -> b -> a -> Range b a
forall b a. b -> a -> b -> a -> Range b a
Range b
p1 a
x1 b
p1 a
x1, b -> a -> b -> a -> Range b a
forall b a. b -> a -> b -> a -> Range b a
Range b
p2 a
x2 b
p2 a
x2]
| [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
xs1 Bool -> Bool -> Bool
&& [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
xs2 = [Range b a] -> m [Range b a]
forall (m :: * -> *) a. Monad m => a -> m a
return [b -> a -> b -> a -> Range b a
forall b a. b -> a -> b -> a -> Range b a
Range b
p1 a
x1 b
p2 a
x2]
| Bool
otherwise = do
(b, a, [a])
pez1' <- (b, a, [a]) -> m (b, a, [a])
pop (b, a, [a])
pez1
(b, a, [a])
pez2' <- (b, a, [a]) -> m (b, a, [a])
pop (b, a, [a])
pez2
(b, a, [a]) -> (b, a, [a]) -> m [Range b a]
go (b, a, [a])
pez1' (b, a, [a])
pez2'

(b, a, [a]) -> (b, a, [a]) -> m [Range b a]
go (b
pLo, a
lo,[a]
los) (b
pHi, a
hi, [a]
his)
initializeSearchM SearchRange a
_ a -> m b
_ = [Range b a] -> m [Range b a]
forall (m :: * -> *) a. Monad m => a -> m a
return []

-- | Start binary search from between 'minBound' and 'maxBound'.
minToMax :: Bounded a => SearchRange a
minToMax :: SearchRange a
minToMax = ([a
forall a. Bounded a => a
minBound], [a
forall a. Bounded a => a
maxBound])

-- | Start binary search from between the given pair of boundaries.
fromTo :: a -> a -> SearchRange a
fromTo :: a -> a -> SearchRange a
fromTo a
x a
y= ([a
x], [a
y])

-- | Exponentially search for lower boundary from @[-1, -2, -4, -8, ...]@, upper boundary from @[0, 1, 2, 4, 8, ...]@.
-- Move on to the binary search once the first @(lo, hi)@ is found
-- such that @pred lo /= pred hi@.
exponential :: Num a => SearchRange a
exponential :: SearchRange a
exponential = ((a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (a -> a -> a
forall a. Num a => a -> a -> a
*a
2) (-a
1), a
0 a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (a -> a -> a
forall a. Num a => a -> a -> a
*a
2) a
1)

-- | Lower boundary is 1, upper boundary is from @[2, 4, 8, 16, ...]@.
positiveExponential :: Num a => SearchRange a
positiveExponential :: SearchRange a
positiveExponential = ([a
1], (a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (a -> a -> a
forall a. Num a => a -> a -> a
*a
2) a
2)

-- | Lower boundary is 0, search upper boundary is from @[1, 2, 4, 8, ...]@.
nonNegativeExponential :: Num a => SearchRange a
nonNegativeExponential :: SearchRange a
nonNegativeExponential = ([a
0], (a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (a -> a -> a
forall a. Num a => a -> a -> a
*a
2) a
1)

-- | Lower boundary is @[0.5, 0.25, 0.125, ...]@, upper boundary is from @[1, 2, 4, 8, ...]@.
positiveFractionalExponential :: Fractional a => SearchRange a
positiveFractionalExponential :: SearchRange a
positiveFractionalExponential = ((a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (a -> a -> a
forall a. Fractional a => a -> a -> a
/a
2) a
0.5, (a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (a -> a -> a
forall a. Num a => a -> a -> a
*a
2) a
1)

-- | Lower boundary is from @[-2, -4, -8, -16, ...]@, upper boundary is -1.
negativeExponential :: Num a => SearchRange a
negativeExponential :: SearchRange a
negativeExponential = ((a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (a -> a -> a
forall a. Num a => a -> a -> a
*a
2) (-a
2), [-a
1])

-- | Lower boundary is from @[-1, -2, -4, -8, ...]@, upper boundary is -0.
nonPositiveExponential :: Num a => SearchRange a
nonPositiveExponential :: SearchRange a
nonPositiveExponential = ((a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (a -> a -> a
forall a. Num a => a -> a -> a
*a
2) (-a
1), [a
0])

-- | Lower boundary is @[-1, -2, -4, -8, ...]@, upper boundary is from @[-0.5, -0.25, -0.125, ...]@.
negativeFractionalExponential :: Fractional a => SearchRange a
negativeFractionalExponential :: SearchRange a
negativeFractionalExponential = ((a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (a -> a -> a
forall a. Num a => a -> a -> a
*a
2) (-a
1), (a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (a -> a -> a
forall a. Fractional a => a -> a -> a
/a
2) (-a
0.5))

-- * Splitters

-- | The type of function that returns a value between @(lo, hi)@ as long as one is available.
type Splitter a = a -> a -> Maybe a

-- | Perform split forever, until we cannot find a mid-value because @hi-lo < 2@.
-- This splitter assumes that the arguments are Integral, and uses the `div` funtion.
--
-- Note that our dividing algorithm always find the mid value for any  @hi-lo >= 2@.
--
-- >>> prove \$ \x y -> (y .>= x+2 &&& x+2 .> x) ==> let z = (x+1) `sDiv` 2 + y `sDiv` 2  in x .< z &&& z .< (y::SInt32)
-- Q.E.D.

divForever :: Integral a => Splitter a
divForever :: Splitter a
divForever a
lo a
hi = let mid :: a
mid = (a
loa -> a -> a
forall a. Num a => a -> a -> a
+a
1) a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
2 a -> a -> a
forall a. Num a => a -> a -> a
+ a
hi a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
2 in
if a
lo a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
mid Bool -> Bool -> Bool
|| a
mid a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
hi then Maybe a
forall a. Maybe a
Nothing
else a -> Maybe a
forall a. a -> Maybe a
Just a
mid

-- | Perform splitting until @hi - lo <= eps@.
divTill :: Integral a => a -> Splitter a
divTill :: a -> Splitter a
divTill a
eps a
lo a
hi
| a
hi a -> a -> a
forall a. Num a => a -> a -> a
- a
lo a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
eps = Maybe a
forall a. Maybe a
Nothing
| Bool
otherwise      = Splitter a
forall a. Integral a => Splitter a
divForever a
lo a
hi

-- | Perform split forever, until we cannot find a mid-value due to machine precision.
-- This one uses `(/)` operator.
divideForever :: (Eq a,Fractional a) => Splitter a
divideForever :: Splitter a
divideForever a
lo a
hi = let mid :: a
mid = a
lo a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
2 a -> a -> a
forall a. Num a => a -> a -> a
+ a
hi a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
2 in
if a
lo a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
mid Bool -> Bool -> Bool
|| a
mid a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
hi then Maybe a
forall a. Maybe a
Nothing
else a -> Maybe a
forall a. a -> Maybe a
Just a
mid

-- | Perform splitting until @hi - lo <= eps@.
divideTill :: (Ord a, Fractional a) => a -> Splitter a
divideTill :: a -> Splitter a
divideTill a
eps a
lo a
hi
| a
hi a -> a -> a
forall a. Num a => a -> a -> a
- a
lo a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
eps = Maybe a
forall a. Maybe a
Nothing
| Bool
otherwise      = Splitter a
forall a. (Eq a, Fractional a) => Splitter a
divideForever a
lo a
hi

-- * Searching

-- | Perform search over pure predicates. The monadic version of this is 'searchM'.
search :: (Eq b) =>
SearchRange a -> Splitter a -> (a -> b) -> [Range b a]
search :: SearchRange a -> Splitter a -> (a -> b) -> [Range b a]
search SearchRange a
init0 Splitter a
split0 a -> b
pred0 = Identity [Range b a] -> [Range b a]
forall a. Identity a -> a
runIdentity (Identity [Range b a] -> [Range b a])
-> Identity [Range b a] -> [Range b a]
forall a b. (a -> b) -> a -> b
\$ SearchRange a
-> Splitter a -> (a -> Identity b) -> Identity [Range b a]
forall a (m :: * -> *) b.
(Functor m, Monad m, Eq b) =>
SearchRange a -> Splitter a -> (a -> m b) -> m [Range b a]
searchM SearchRange a
init0 Splitter a
split0 (b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> (a -> b) -> a -> Identity b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
pred0)

-- | Mother of all search variations.
--
-- 'searchM' keeps track of the predicates found, so that it works well with the 'Evidence' type.

searchM :: forall a m b . (Functor m, Monad m, Eq b) =>
SearchRange a -> Splitter a -> (a -> m b) -> m [Range b a]
searchM :: SearchRange a -> Splitter a -> (a -> m b) -> m [Range b a]
searchM SearchRange a
init0 Splitter a
split0 a -> m b
pred0 = do
[Range b a]
ranges0 <- SearchRange a -> (a -> m b) -> m [Range b a]
forall (m :: * -> *) b a.
SearchRange a -> (a -> m b) -> m [Range b a]
initializeSearchM SearchRange a
init0 a -> m b
pred0
[Range b a] -> m [Range b a]
go [Range b a]
ranges0
where
go :: [Range b a] -> m [Range b a]
go :: [Range b a] -> m [Range b a]
go (r1 :: Range b a
r1@(Range b
p0 a
lo1 b
p1 a
hi1):r2 :: Range b a
r2@(Range b
p2 a
lo2 b
p3 a
hi2):[Range b a]
rest) = case Splitter a
split0 a
hi1 a
lo2 of
Maybe a
Nothing   -> (Range b a
r1Range b a -> [Range b a] -> [Range b a]
forall a. a -> [a] -> [a]
:) ([Range b a] -> [Range b a]) -> m [Range b a] -> m [Range b a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<\$> [Range b a] -> m [Range b a]
go (Range b a
r2Range b a -> [Range b a] -> [Range b a]
forall a. a -> [a] -> [a]
:[Range b a]
rest)
Just a
mid1 -> do
b
pMid <- a -> m b
pred0 a
mid1
if | b
p1 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
pMid -> [Range b a] -> m [Range b a]
go ([Range b a] -> m [Range b a]) -> [Range b a] -> m [Range b a]
forall a b. (a -> b) -> a -> b
\$ (b -> a -> b -> a -> Range b a
forall b a. b -> a -> b -> a -> Range b a
Range b
p0 a
lo1 b
pMid a
mid1) Range b a -> [Range b a] -> [Range b a]
forall a. a -> [a] -> [a]
: Range b a
r2 Range b a -> [Range b a] -> [Range b a]
forall a. a -> [a] -> [a]
: [Range b a]
rest
| b
p2 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
pMid -> [Range b a] -> m [Range b a]
go ([Range b a] -> m [Range b a]) -> [Range b a] -> m [Range b a]
forall a b. (a -> b) -> a -> b
\$ Range b a
r1 Range b a -> [Range b a] -> [Range b a]
forall a. a -> [a] -> [a]
: (b -> a -> b -> a -> Range b a
forall b a. b -> a -> b -> a -> Range b a
Range b
pMid a
mid1 b
p3 a
hi2) Range b a -> [Range b a] -> [Range b a]
forall a. a -> [a] -> [a]
: [Range b a]
rest
| Bool
otherwise  -> [Range b a] -> m [Range b a]
go ([Range b a] -> m [Range b a]) -> [Range b a] -> m [Range b a]
forall a b. (a -> b) -> a -> b
\$ Range b a
r1 Range b a -> [Range b a] -> [Range b a]
forall a. a -> [a] -> [a]
: (b -> a -> b -> a -> Range b a
forall b a. b -> a -> b -> a -> Range b a
Range b
pMid a
mid1 b
pMid a
mid1) Range b a -> [Range b a] -> [Range b a]
forall a. a -> [a] -> [a]
: Range b a
r2 Range b a -> [Range b a] -> [Range b a]
forall a. a -> [a] -> [a]
: [Range b a]
rest
go [Range b a]
xs = [Range b a] -> m [Range b a]
forall (m :: * -> *) a. Monad m => a -> m a
return [Range b a]
xs

-- * Postprocess

-- | Look up for the first 'Range' with the given predicate.
lookupRanges :: (Eq b) => b -> [Range b a] -> Maybe (Range b a)
lookupRanges :: b -> [Range b a] -> Maybe (Range b a)
lookupRanges b
k [] = Maybe (Range b a)
forall a. Maybe a
Nothing
lookupRanges b
k (r :: Range b a
r@Range{b
a
hiVal :: a
hiKey :: b
loVal :: a
loKey :: b
hiVal :: forall b a. Range b a -> a
hiKey :: forall b a. Range b a -> b
loVal :: forall b a. Range b a -> a
loKey :: forall b a. Range b a -> b
..}:[Range b a]
rs)
| b
loKey b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
k  = Range b a -> Maybe (Range b a)
forall a. a -> Maybe a
Just Range b a
r
| Bool
otherwise   = b -> [Range b a] -> Maybe (Range b a)
forall b a. Eq b => b -> [Range b a] -> Maybe (Range b a)
lookupRanges b
k [Range b a]
rs

-- | Pick up the smallest @a@ that satisfies @pred a == b@.
smallest :: (Eq b) => b -> [Range b a] -> Maybe a
smallest :: b -> [Range b a] -> Maybe a
smallest b
b [Range b a]
rs = Range b a -> a
forall b a. Range b a -> a
loVal (Range b a -> a) -> Maybe (Range b a) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<\$> b -> [Range b a] -> Maybe (Range b a)
forall b a. Eq b => b -> [Range b a] -> Maybe (Range b a)
lookupRanges b
b [Range b a]
rs

-- | Pick up the largest @a@ that satisfies @pred a == b@.
largest :: (Eq b) => b -> [Range b a] -> Maybe a
largest :: b -> [Range b a] -> Maybe a
largest b
b [Range b a]
rs = Range b a -> a
forall b a. Range b a -> a
hiVal (Range b a -> a) -> Maybe (Range b a) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<\$> b -> [Range b a] -> Maybe (Range b a)
forall b a. Eq b => b -> [Range b a] -> Maybe (Range b a)
lookupRanges b
b [Range b a]
rs

-- | Get the content of the evidence for the smallest @a@ which satisfies @pred a@.
evidenceForSmallest :: [Range (Evidence b1 b2) a] -> Maybe b2
evidenceForSmallest :: [Range (Evidence b1 b2) a] -> Maybe b2
evidenceForSmallest [Range (Evidence b1 b2) a]
rs = [b2] -> Maybe b2
forall a. [a] -> Maybe a
listToMaybe [b2
e | Evidence b2
e <- (Range (Evidence b1 b2) a -> Evidence b1 b2)
-> [Range (Evidence b1 b2) a] -> [Evidence b1 b2]
forall a b. (a -> b) -> [a] -> [b]
map Range (Evidence b1 b2) a -> Evidence b1 b2
forall b a. Range b a -> b
loKey [Range (Evidence b1 b2) a]
rs]

-- | Get the content of the evidence for the largest @a@ which satisfies @pred a@.
evidenceForLargest :: [Range (Evidence b1 b2) a] -> Maybe b2
evidenceForLargest :: [Range (Evidence b1 b2) a] -> Maybe b2
evidenceForLargest [Range (Evidence b1 b2) a]
rs = [b2] -> Maybe b2
forall a. [a] -> Maybe a
listToMaybe [b2
e | Evidence b2
e <- (Range (Evidence b1 b2) a -> Evidence b1 b2)
-> [Range (Evidence b1 b2) a] -> [Evidence b1 b2]
forall a b. (a -> b) -> [a] -> [b]
map Range (Evidence b1 b2) a -> Evidence b1 b2
forall b a. Range b a -> b
hiKey [Range (Evidence b1 b2) a]
rs]

-- | Get the content of the counterEvidence for the smallest @a@ which does not satisfy @pred a@.
counterEvidenceForSmallest :: [Range (Evidence b1 b2) a] -> Maybe b1
counterEvidenceForSmallest :: [Range (Evidence b1 b2) a] -> Maybe b1
counterEvidenceForSmallest [Range (Evidence b1 b2) a]
rs = [b1] -> Maybe b1
forall a. [a] -> Maybe a
listToMaybe [b1
e | CounterEvidence b1
e <- (Range (Evidence b1 b2) a -> Evidence b1 b2)
-> [Range (Evidence b1 b2) a] -> [Evidence b1 b2]
forall a b. (a -> b) -> [a] -> [b]
map Range (Evidence b1 b2) a -> Evidence b1 b2
forall b a. Range b a -> b
loKey [Range (Evidence b1 b2) a]
rs]

-- | Get the content of the counterEvidence for the largest @a@ which does not satisfy @pred a@.
counterEvidenceForLargest :: [Range (Evidence b1 b2) a] -> Maybe b1
counterEvidenceForLargest :: [Range (Evidence b1 b2) a] -> Maybe b1
counterEvidenceForLargest [Range (Evidence b1 b2) a]
rs = [b1] -> Maybe b1
forall a. [a] -> Maybe a
listToMaybe [b1
e | CounterEvidence b1
e <- (Range (Evidence b1 b2) a -> Evidence b1 b2)
-> [Range (Evidence b1 b2) a] -> [Evidence b1 b2]
forall a b. (a -> b) -> [a] -> [b]
map Range (Evidence b1 b2) a -> Evidence b1 b2
forall b a. Range b a -> b
hiKey [Range (Evidence b1 b2) a]
rs]
```