    {-# 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
    $cshowsPrec :: forall a b. (Show a, Show b) => Int -> Evidence a b -> ShowS
    showsPrec :: Int -> Evidence a b -> ShowS
    $cshow :: forall a b. (Show a, Show b) => Evidence a b -> String
    show :: Evidence a b -> String
    $cshowList :: forall a b. (Show a, Show b) => [Evidence a b] -> ShowS
    showList :: [Evidence a b] -> ShowS
    Show, ReadPrec [Evidence a b]
    ReadPrec (Evidence a b)
    Int -> ReadS (Evidence a b)
    ReadS [Evidence a b]
    (Int -> ReadS (Evidence a b))
    -> ReadS [Evidence a b]
    -> ReadPrec (Evidence a b)
    -> ReadPrec [Evidence a b]
    -> Read (Evidence a b)
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    forall a b. (Read a, Read b) => ReadPrec [Evidence a b]
    forall a b. (Read a, Read b) => ReadPrec (Evidence a b)
    forall a b. (Read a, Read b) => Int -> ReadS (Evidence a b)
    forall a b. (Read a, Read b) => ReadS [Evidence a b]
    $creadsPrec :: forall a b. (Read a, Read b) => Int -> ReadS (Evidence a b)
    readsPrec :: Int -> ReadS (Evidence a b)
    $creadList :: forall a b. (Read a, Read b) => ReadS [Evidence a b]
    readList :: ReadS [Evidence a b]
    $creadPrec :: forall a b. (Read a, Read b) => ReadPrec (Evidence a b)
    readPrec :: ReadPrec (Evidence a b)
    $creadListPrec :: forall a b. (Read a, Read b) => ReadPrec [Evidence a b]
    readListPrec :: ReadPrec [Evidence a b]
    Read, (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
    $cfmap :: forall a a b. (a -> b) -> Evidence a a -> Evidence a b
    fmap :: forall a b. (a -> b) -> Evidence a a -> Evidence a b
    $c<$ :: forall a a b. a -> Evidence a b -> Evidence a a
    <$ :: forall a b. a -> Evidence a b -> Evidence a a
    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 :: forall a. a -> Evidence e a
    pure                     = a -> Evidence e a
    forall e a. a -> Evidence e a
    Evidence
        CounterEvidence  e
    e <*> :: forall a b. 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 a b. (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

    instance Monad (Evidence e) where
        return :: forall a. a -> Evidence e a
    return                   = a -> Evidence e a
    forall e a. a -> Evidence e a
    Evidence
        CounterEvidence  e
    l >>= :: forall a b. 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 :: forall a b. 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 :: forall a b. 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 {forall b a. Range b a -> b
    loKey :: b, forall b a. Range b a -> a
    loVal :: a, forall b a. Range b a -> b
    hiKey :: b, forall b a. 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
    $cshowsPrec :: forall b a. (Show b, Show a) => Int -> Range b a -> ShowS
    showsPrec :: Int -> Range b a -> ShowS
    $cshow :: forall b a. (Show b, Show a) => Range b a -> String
    show :: Range b a -> String
    $cshowList :: forall b a. (Show b, Show a) => [Range b a] -> ShowS
    showList :: [Range b a] -> ShowS
    Show, ReadPrec [Range b a]
    ReadPrec (Range b a)
    Int -> ReadS (Range b a)
    ReadS [Range b a]
    (Int -> ReadS (Range b a))
    -> ReadS [Range b a]
    -> ReadPrec (Range b a)
    -> ReadPrec [Range b a]
    -> Read (Range b a)
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    forall b a. (Read b, Read a) => ReadPrec [Range b a]
    forall b a. (Read b, Read a) => ReadPrec (Range b a)
    forall b a. (Read b, Read a) => Int -> ReadS (Range b a)
    forall b a. (Read b, Read a) => ReadS [Range b a]
    $creadsPrec :: forall b a. (Read b, Read a) => Int -> ReadS (Range b a)
    readsPrec :: Int -> ReadS (Range b a)
    $creadList :: forall b a. (Read b, Read a) => ReadS [Range b a]
    readList :: ReadS [Range b a]
    $creadPrec :: forall b a. (Read b, Read a) => ReadPrec (Range b a)
    readPrec :: ReadPrec (Range b a)
    $creadListPrec :: forall b a. (Read b, Read a) => ReadPrec [Range b a]
    readListPrec :: ReadPrec [Range b 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
    $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
    /= :: 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
    $ccompare :: forall b a. (Ord b, Ord a) => Range b a -> Range b a -> Ordering
    compare :: Range b a -> Range b a -> Ordering
    $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
    >= :: Range b a -> Range b a -> Bool
    $cmax :: 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
    $cmin :: 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
    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 :: forall (m :: * -> *) b a.
    (Monad m, Eq b) =>
    SearchRange a -> (a -> m b) -> m [Range b a]
    initializeSearchM (a
    lo:[a]
    los,a
    hi:[a]
    his) a -> m b
    pred0 = do
      pLo <- a -> m b
    pred0 a
    lo
      pHi <- pred0 hi
      let
        pop (b
    p,a
    x, []) = (b, a, [a]) -> m (b, a, [a])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (b
    p,a
    x,[])
        pop (b
    p,a
    _, a
    x2:[a]
    xs) = do
          p2 <- a -> m b
    pred0 a
    x2
          return (p2, x2, xs)

        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 a. a -> m 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 a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [a]
    xs1 Bool -> Bool -> Bool
    && [a] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [a]
    xs2 = [Range b a] -> m [Range b a]
    forall a. a -> m 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
                pez1' <- (b, a, [a]) -> m (b, a, [a])
    pop (b, a, [a])
    pez1
                pez2' <- pop pez2
                go pez1' pez2'

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

    -- | Start binary search from between 'minBound' and 'maxBound'.
    minToMax :: Bounded a => SearchRange a
    minToMax :: forall a. Bounded a => 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 :: forall a. 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 :: forall a. Num a => 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 :: forall a. Num a => 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 :: forall a. Num a => 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 :: forall a. Fractional a => 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 :: forall a. Num a => 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 :: forall a. Num a => 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 :: forall a. Fractional a => 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 :: forall a. Integral a => 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 :: forall a. Integral a => 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 :: forall a. (Eq a, Fractional a) => 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 :: forall a. (Ord a, Fractional a) => 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 :: forall b a.
    Eq b =>
    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 :: 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 a -> m b
    pred0 = do
      ranges0 <- SearchRange a -> (a -> m b) -> m [Range b a]
    forall (m :: * -> *) b a.
    (Monad m, Eq b) =>
    SearchRange a -> (a -> m b) -> m [Range b a]
    initializeSearchM SearchRange a
    init0 a -> m b
    pred0
      go 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
              pMid <- a -> m b
    pred0 a
    mid1
              if | p1 == pMid -> go $ (Range p0 lo1 pMid mid1) : r2 : rest
                 | p2 == pMid -> go $ r1 : (Range pMid mid1 p3 hi2) : rest
                 | otherwise  -> go $ r1 : (Range pMid mid1 pMid mid1) : r2 : rest
          go [Range b a]
    xs = [Range b a] -> m [Range b a]
    forall a. a -> m 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 :: forall b a. Eq b => 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
    loKey :: forall b a. Range b a -> b
    loVal :: forall b a. Range b a -> a
    hiKey :: forall b a. Range b a -> b
    hiVal :: forall b a. Range b a -> a
    loKey :: b
    loVal :: a
    hiKey :: b
    hiVal :: a
    ..}:[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 :: forall b a. Eq b => 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 :: forall b a. Eq b => 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 :: forall b1 b2 a. [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 :: forall b1 b2 a. [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 :: forall b1 b2 a. [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 :: forall b1 b2 a. [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]