-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Binary and exponential searches
--   
--   <b>Introduction</b>
--   
--   This package provides varieties of binary search functions. c.f.
--   <a>Numeric.Search</a> for the examples.
--   
--   These search function can search for pure and monadic predicates, of
--   type:
--   
--   <pre>
--   pred :: Eq b =&gt; a -&gt; b
--   pred :: (Eq b, Monad m) =&gt; a -&gt; m b
--   </pre>
--   
--   The predicates must satisfy that the domain range for any codomain
--   value is continuous; that is, <tt>∀x≦y≦z. pred x == pred z ⇒ pred y ==
--   pred x</tt> .
--   
--   For example, we can address the problem of finding the boundary of an
--   upward-closed set of integers, using a combination of exponential and
--   binary searches.
--   
--   Variants are provided for searching within bounded and unbounded
--   intervals of both <a>Integer</a> and bounded integral types.
--   
--   The package was created by Ross Paterson, and extended by Takayuki
--   Muranushi, to be used together with SMT solvers.
--   
--   <b>The Module Structure</b>
--   
--   <ul>
--   <li><a>Numeric.Search</a> provides the generic search combinator, to
--   search for pure and monadic predicates.</li>
--   <li><a>Numeric.Search.Bounded</a> , <a>Numeric.Search.Integer</a> ,
--   <a>Numeric.Search.Range</a> provides the various specialized
--   searchers, which means less number of function arguments, and easier
--   to use.</li>
--   </ul>
--   
@package binary-search
@version 2.0.0


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

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

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

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

-- | The <tt>Range k lo k' hi</tt> represents the search result that
--   <tt>pred x == k</tt> for <tt>lo &lt;= x &lt;= hi</tt>. The
--   <a>Range</a> type also holds the evidences for the lower and the upper
--   boundary.
data Range b a
Range :: b -> a -> b -> a -> Range b a
[loKey] :: Range b a -> b
[loVal] :: Range b a -> a
[hiKey] :: Range b a -> b
[hiVal] :: Range b a -> a

-- | 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 <tt>initializeSearchM</tt>
--   tries to find the first <tt>(lo, hi)</tt> such that <tt>pred lo /=
--   pred hi</tt>, by the breadth-first search.
initializeSearchM :: (Monad m, Eq b) => SearchRange a -> (a -> m b) -> m [Range b a]

-- | Start binary search from between <a>minBound</a> and <a>maxBound</a>.
minToMax :: Bounded a => SearchRange a

-- | Start binary search from between the given pair of boundaries.
fromTo :: a -> a -> SearchRange a

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

-- | Lower boundary is 1, upper boundary is from <tt>[2, 4, 8, 16,
--   ...]</tt>.
positiveExponential :: Num a => SearchRange a

-- | Lower boundary is 0, search upper boundary is from <tt>[1, 2, 4, 8,
--   ...]</tt>.
nonNegativeExponential :: Num a => SearchRange a

-- | Lower boundary is <tt>[0.5, 0.25, 0.125, ...]</tt>, upper boundary is
--   from <tt>[1, 2, 4, 8, ...]</tt>.
positiveFractionalExponential :: Fractional a => SearchRange a

-- | Lower boundary is from <tt>[-2, -4, -8, -16, ...]</tt>, upper boundary
--   is -1.
negativeExponential :: Num a => SearchRange a

-- | Lower boundary is from <tt>[-1, -2, -4, -8, ...]</tt>, upper boundary
--   is -0.
nonPositiveExponential :: Num a => SearchRange a

-- | Lower boundary is <tt>[-1, -2, -4, -8, ...]</tt>, upper boundary is
--   from <tt>[-0.5, -0.25, -0.125, ...]</tt>.
negativeFractionalExponential :: Fractional a => SearchRange a

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

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

-- | Perform splitting until <tt>hi - lo &lt;= eps</tt>.
divTill :: Integral a => a -> Splitter a

-- | Perform split forever, until we cannot find a mid-value due to machine
--   precision. This one uses <a>(/)</a> operator.
divideForever :: (Eq a, Fractional a) => Splitter a

-- | Perform splitting until <tt>hi - lo &lt;= eps</tt>.
divideTill :: (Ord a, Fractional a) => a -> Splitter a

-- | Perform search over pure predicates. The monadic version of this is
--   <a>searchM</a>.
search :: Eq b => SearchRange a -> Splitter a -> (a -> b) -> [Range b a]

-- | Mother of all search variations.
--   
--   <a>searchM</a> keeps track of the predicates found, so that it works
--   well with the <a>Evidence</a> type.
searchM :: forall a m b. (Functor m, Monad m, Eq b) => SearchRange a -> Splitter a -> (a -> m b) -> m [Range b a]

-- | Look up for the first <a>Range</a> with the given predicate.
lookupRanges :: Eq b => b -> [Range b a] -> Maybe (Range b a)

-- | Pick up the smallest <tt>a</tt> that satisfies <tt>pred a == b</tt>.
smallest :: Eq b => b -> [Range b a] -> Maybe a

-- | Pick up the largest <tt>a</tt> that satisfies <tt>pred a == b</tt>.
largest :: Eq b => b -> [Range b a] -> Maybe a

-- | Get the content of the evidence for the smallest <tt>a</tt> which
--   satisfies <tt>pred a</tt>.
evidenceForSmallest :: [Range (Evidence b1 b2) a] -> Maybe b2

-- | Get the content of the evidence for the largest <tt>a</tt> which
--   satisfies <tt>pred a</tt>.
evidenceForLargest :: [Range (Evidence b1 b2) a] -> Maybe b2

-- | Get the content of the counterEvidence for the smallest <tt>a</tt>
--   which does not satisfy <tt>pred a</tt>.
counterEvidenceForSmallest :: [Range (Evidence b1 b2) a] -> Maybe b1

-- | Get the content of the counterEvidence for the largest <tt>a</tt>
--   which does not satisfy <tt>pred a</tt>.
counterEvidenceForLargest :: [Range (Evidence b1 b2) a] -> Maybe b1
instance GHC.Internal.Base.Applicative (Numeric.Search.Evidence e)
instance GHC.Classes.Eq (Numeric.Search.Evidence b a)
instance (GHC.Classes.Eq b, GHC.Classes.Eq a) => GHC.Classes.Eq (Numeric.Search.Range b a)
instance GHC.Internal.Base.Functor (Numeric.Search.Evidence a)
instance GHC.Internal.Base.Monad (Numeric.Search.Evidence e)
instance GHC.Classes.Ord (Numeric.Search.Evidence b a)
instance (GHC.Classes.Ord b, GHC.Classes.Ord a) => GHC.Classes.Ord (Numeric.Search.Range b a)
instance (GHC.Internal.Read.Read a, GHC.Internal.Read.Read b) => GHC.Internal.Read.Read (Numeric.Search.Evidence a b)
instance (GHC.Internal.Read.Read b, GHC.Internal.Read.Read a) => GHC.Internal.Read.Read (Numeric.Search.Range b a)
instance (GHC.Internal.Show.Show a, GHC.Internal.Show.Show b) => GHC.Internal.Show.Show (Numeric.Search.Evidence a b)
instance (GHC.Internal.Show.Show b, GHC.Internal.Show.Show a) => GHC.Internal.Show.Show (Numeric.Search.Range b a)


-- | Searching unbounded intervals of integers for the boundary of an
--   upward-closed set, using a combination of exponential and binary
--   search.
module Numeric.Search.Integer

-- | <i>O(log(abs n))</i>. Search the integers.
--   
--   If <tt>p</tt> is an upward-closed predicate, <tt>search p</tt> returns
--   the least <tt>n</tt> satisfying <tt>p</tt>. If no such <tt>n</tt>
--   exists, either because no integer satisfies <tt>p</tt> or all do,
--   <tt>search p</tt> does not terminate.
--   
--   For example, the following function computes discrete logarithms (base
--   2):
--   
--   <pre>
--   discreteLog :: Integer -&gt; Integer
--   discreteLog n = search (\ k -&gt; 2^k &lt;= n)
--   </pre>
search :: (Integer -> Bool) -> Integer

-- | <i>O(log(n-l))</i>. Search the integers from a given lower bound.
--   
--   If <tt>p</tt> is an upward-closed predicate, <tt>searchFrom p l =
--   <a>search</a> (\ i -&gt; i &gt;= l &amp;&amp; p i)</tt>. If no such
--   <tt>n</tt> exists (because no integer satisfies <tt>p</tt>),
--   <tt>searchFrom p</tt> does not terminate.
searchFrom :: (Integer -> Bool) -> Integer -> Integer

-- | <i>O(log(h-n))</i>. Search the integers up to a given upper bound.
--   
--   If <tt>p</tt> is an upward-closed predicate, <tt>searchTo p h ==
--   <a>Just</a> n</tt> if and only if <tt>n</tt> is the least number <tt>n
--   &lt;= h</tt> satisfying <tt>p</tt>.
searchTo :: (Integer -> Bool) -> Integer -> Maybe Integer

-- | <i>O(m log(n/m))</i>. Two-dimensional search, using an algorithm due
--   described in
--   
--   <ul>
--   <li>Richard Bird, <i>Saddleback search: a lesson in algorithm
--   design</i>, in <i>Mathematics of Program Construction</i> 2006,
--   Springer LNCS vol. 4014, pp82-89.</li>
--   </ul>
--   
--   If <tt>p</tt> is closed upwards in each argument on non-negative
--   integers, <tt>search2 p</tt> returns the minimal non-negative pairs
--   satisfying <tt>p</tt>, listed in order of increasing x-coordinate.
--   
--   <i>m</i> and <i>n</i> refer to the smaller and larger dimensions of
--   the rectangle containing the boundary.
--   
--   For example,
--   
--   <pre>
--   search2 (\ x y -&gt; x^2 + y^2 &gt;= 25)  ==  [(0,5),(3,4),(4,3),(5,0)]
--   </pre>
search2 :: (Integer -> Integer -> Bool) -> [(Integer, Integer)]


-- | Binary search of a bounded interval of an integral type for the
--   boundary of an upward-closed set, using a combination of exponential
--   and binary search.
module Numeric.Search.Range

-- | <i>O(log(h-l))</i>. Search a bounded interval of some integral type.
--   
--   If <tt>p</tt> is an upward-closed predicate, <tt>searchFromTo p l h ==
--   Just n</tt> if and only if <tt>n</tt> is the least number <tt>l &lt;=
--   n &lt;= h</tt> satisfying <tt>p</tt>.
--   
--   For example, the following function determines the first index (if
--   any) at which a value occurs in an ordered array:
--   
--   <pre>
--   searchArray :: Ord a =&gt; a -&gt; Array Int a -&gt; Maybe Int
--   searchArray x array = do
--     let (lo, hi) = bounds array
--     k &lt;- searchFromTo (\ i -&gt; array!i &gt;= x) lo hi
--     guard (array!k == x)
--     return k
--   </pre>
searchFromTo :: Integral a => (a -> Bool) -> a -> a -> Maybe a


-- | Searching unbounded intervals within bounded integral types for the
--   boundary of an upward-closed set, using a combination of exponential
--   and binary search.
module Numeric.Search.Bounded

-- | <i>O(log(abs n))</i>. Search a bounded integral type.
--   
--   If <tt>p</tt> is an upward-closed predicate, <tt>search p</tt> returns
--   <tt>Just n</tt> if and only if <tt>n</tt> is the least such satisfying
--   <tt>p</tt>.
search :: (Bounded a, Integral a) => (a -> Bool) -> Maybe a

-- | <i>O(log(abs n))</i>. Search the part of a bounded integral type from
--   a given point.
--   
--   If <tt>p</tt> is an upward-closed predicate, <tt>searchFrom p l</tt>
--   returns <tt>Just n</tt> if and only if <tt>n</tt> is the least <tt>n
--   &gt;= l</tt> satisfying <tt>p</tt>.
searchFrom :: (Bounded a, Integral a) => (a -> Bool) -> a -> Maybe a

-- | <i>O(log(abs n))</i>. Search the part of a bounded integral type up to
--   a given point.
--   
--   If <tt>p</tt> is an upward-closed predicate, <tt>searchTo p h</tt>
--   returns <tt>Just n</tt> if and only if <tt>n</tt> is the least <tt>n
--   &lt;= h</tt> satisfying <tt>p</tt>.
searchTo :: (Bounded a, Integral a) => (a -> Bool) -> a -> Maybe a
