diff --git a/Numeric/Search.hs b/Numeric/Search.hs
--- a/Numeric/Search.hs
+++ b/Numeric/Search.hs
@@ -14,36 +14,20 @@
 
 
 module Numeric.Search (
--- * Pure combinators
--- $pureCombinators
-
--- ** Types
-Range,
--- ** Searchers
-
--- ** Combinators
-
--- * Monadic combinators
--- $monadicCombinators
-
--- ** Types
-BinarySearchM,
-PredicateM,
-InitializerM,
-CutterM,
+         -- * Evidence
+         Evidence(..),
+         -- * Search Range
+         Range,
+         InitializesSearch,
+         -- * Splitters
+         splitForever, splitTill,
 
--- ** Searchers
-searchWithM
--- ** Combinators
+         -- * Search
+         search, searchM,
+         -- * Postprocess
+         smallest, largest
 
 ) where
 
 import Numeric.Search.Combinator.Pure
 import Numeric.Search.Combinator.Monadic
-
-{- $pureCombinators
-   These are pure.
--}
-{- $monadicCombinators
-   These are monadic.
- -}
diff --git a/Numeric/Search/Combinator/Monadic.hs b/Numeric/Search/Combinator/Monadic.hs
--- a/Numeric/Search/Combinator/Monadic.hs
+++ b/Numeric/Search/Combinator/Monadic.hs
@@ -1,113 +1,149 @@
 -- | Monadic binary search combinators.
 
-{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DeriveFunctor, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, MultiWayIf, ScopedTypeVariables, TupleSections #-}
 
 module Numeric.Search.Combinator.Monadic where
 
 import           Control.Applicative((<$>))
-import           Data.Sequence as Seq
 import           Prelude hiding (init, pred)
 
--- | The generalized type for binary search functions.
-type BinarySearchM m a b =
-  InitializerM m a b ->
-  CutterM m a b ->
-  PredicateM m a b ->
-  m (Seq (Range a b))
+-- * Evidence
 
--- | 'BookEnd' comes in order [LEnd, REnd, LEnd, REnd ...], and
--- represents the ongoing state of the search results.
--- Two successive 'BookEnd' @LEnd x1 y1@, @REnd x2 y1@ represents a
--- claim that @pred x == y1@ for all @x@ such that @x1 <= x <= x2@ .
--- Like this:
---
--- > is (x^2 > 20000) ?
--- >
--- > LEnd    REnd  LEnd     REnd
--- > 0        100  200       300
--- > |_ False _|    |_ True  _|
+-- | The 'Evidence' datatype is similar to 'Either' , but differes in that all 'CounterExample' values are
+--   equal to each other, and all 'Example' values are also
+--   equal to each other. The 'Evidence' type is used to binary-searching for some predicate and meanwhile returning evidences for that.
 
-data BookEnd a b
-      = REnd !a !b
-      | LEnd !a !b
-      deriving (Eq, Show)
+data Evidence a b = CounterExample a | Example b
+                  deriving (Show, Read, Functor)
 
--- | 'Range' @((x1,x2),y)@ denotes that @pred x == y@ for all
--- @x1 <= x <= x2@ .
-type Range a b = ((a,a),b)
+instance Eq (Evidence b a) where
+  CounterExample _ == CounterExample _ = True
+  Example _        == Example _        = True
+  _                == _                = False
 
--- | 'PredicateM' @m a b@ calculates the predicate in the context @m@.
-type PredicateM m a b = a -> m b
+instance Ord (Evidence b a) where
+  CounterExample _ `compare` CounterExample _ = EQ
+  Example _        `compare` Example _        = EQ
+  CounterExample _ `compare` Example _        = GT
+  Example _        `compare` CounterExample _ = LT
 
--- | 'InitializerM' generates the initial set of ranges.
-type InitializerM m a b = PredicateM m a b -> m (Seq (BookEnd a b))
+instance Applicative (Evidence e) where
+    pure                    = Example
+    CounterExample  e <*> _ = CounterExample e
+    Example f <*> r         = fmap f r
 
--- | 'CutterM' @p x1 x2@ decides if we should further investigate the
--- gap between @x1@ and @x2@. If so, it gives a new value @x3@ wrapped
--- in a 'Just'. 'CutterM' may optionally use the predicate.
-type CutterM m a b = PredicateM m a b -> a -> a -> m (Maybe a)
+instance Monad (Evidence e) where
+    return                  = Example
+    CounterExample  l >>= _ = CounterExample l
+    Example r >>= k         = k r
 
+-- * Search range
 
--- | an initializer with the initial range specified.
-initConstM :: (Monad m) => a -> a -> InitializerM m a b
-initConstM x1 x2 pred = do
-  y1 <- pred x1
-  y2 <- pred x2
-  return $ Seq.fromList [LEnd x1 y1, REnd x1 y1,LEnd x2 y2, REnd x2 y2]
+-- | @(value, (lo,hi))@ represents the finding that @pred x == value@ for @lo <= x <= hi@.
+-- By using this type, we can readily 'lookup' a list of 'Range' .
 
--- | an initializer that searches for the full bound.
-initBoundedM :: (Monad m, Bounded a) => InitializerM m a b
-initBoundedM = initConstM minBound maxBound
+type Range b a = (b, (a,a))
 
--- | a cutter for integral types.
-cutIntegralM :: (Monad m, Integral a) => CutterM m a b
-cutIntegralM _ x1 x2
-  | x1+1 >= x2 = return Nothing
-  | otherwise  = return $ Just ((x1+1)`div`2 + x2 `div`2)
 
--- | The most generalized version of search.
-searchWithM :: forall m a b. (Functor m, Monad m, Eq b) => BinarySearchM m a b
-searchWithM init cut pred = do
-  seq0 <- init pred
-  finalize <$> go seq0
-  where
-    go :: Seq (BookEnd a b) -> m (Seq (BookEnd a b))
-    go seq0 = case viewl seq0 of
-      EmptyL -> return seq0
-      (x1 :< seq1) -> do
-        let skip = (x1 <|) <$> go seq1
-        case viewl seq1 of
-          EmptyL -> skip
-          (x2 :< seq2) -> case (x1,x2) of
-            (REnd a1 b1, LEnd a2 b2) -> case b1==b2 of
-              True  -> go seq2 -- merge the two regions
-              False ->  do
-                y1 <- drillDown a1 b1 a2 b2
-                y2 <- go seq2
-                return $ y1 >< y2
-            _ -> skip
+-- | A type @x@ is an instance of 'SearchInitializer' @a@, if @x@ can be used to set up the lower and upper inital values for
+-- binary search over values of type @a@.
+-- .
+-- 'initializeSearchM' should generate a list of 'Range' s, where each 'Range' has different -- predicate.
+class InitializesSearch a x where
+  initializeSearchM :: (Monad m, Eq b)=> x -> (a -> m b) -> m [Range b a]
 
-    -- precondition : b1 /= b2
-    drillDown :: a -> b -> a -> b -> m (Seq (BookEnd a b))
-    drillDown x1 y1 x2 y2 = do
-      mc <- cut pred x1 x2
-      case mc of
-        Nothing -> return $ Seq.fromList [REnd x1 y1, LEnd x2 y2]
-        Just x3 -> do
-          y3 <- pred x3
-          case () of
-            _ | y3==y1 -> drillDown x3 y3 x2 y2
-            _ | y3==y2 -> drillDown x1 y1 x3 y3
-            _ -> do
-              y1 <-  drillDown x1 y1 x3 y3
-              y2 <-  drillDown x3 y3 x2 y2
-              return $ y1 >< y2
+-- | Set the lower and upper boundary explicitly.
+instance InitializesSearch a (a,a) where
+  initializeSearchM (lo,hi) pred0 = do
+    pLo <- pred0 lo
+    pHi <- pred0 hi
+    return $ if | pLo == pHi -> [(,) pLo (lo,hi)]
+                | otherwise  -> [(,) pLo (lo,lo), (,) pHi (hi,hi)]
 
-    finalize :: Seq (BookEnd a b) -> Seq (Range a b)
-    finalize seqE = case viewl seqE of
-      EmptyL -> Seq.empty
-      (x1 :< seqE1) -> case viewl seqE1 of
-        EmptyL -> finalize seqE1
-        (x2 :< seqE2) -> case (x1,x2) of
-          (LEnd x1 y1, REnd x2 y2) | y1==y2 -> ((x1,x2), y1) <| finalize seqE2
-          _                                 -> finalize seqE1
+-- | Set the lower boundary explicitly and search for the upper boundary.
+instance InitializesSearch a (a,[a]) where
+  initializeSearchM (lo,his) = initializeSearchM ([lo],his)
+
+-- | Set the upper boundary explicitly and search for the lower boundary.
+instance InitializesSearch a ([a],a) where
+  initializeSearchM (los,hi) = initializeSearchM (los,[hi])
+
+
+-- | 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.
+instance InitializesSearch a ([a],[a]) where
+  initializeSearchM ([], []) _ = return []
+  initializeSearchM ([], x:_) pred0 = do
+    p <- pred0 x
+    return [(,) p (x,x)]
+  initializeSearchM (x:_, []) pred0 = do
+    p <- pred0 x
+    return [(,) p (x,x)]
+  initializeSearchM (lo:los,hi:his) pred0 = do
+    pLo <- pred0 lo
+    pHi <- pred0 hi
+    let
+      pop (p,x, []) = return (p,x,[])
+      pop (p,_, x2:xs) = do
+        p2 <- pred0 x2
+        return (p2, x2, xs)
+
+      go pez1@(p1,x1,xs1) pez2@(p2,x2,xs2)
+          | p1 /= p2             = return [(,)p1 (x1,x1), (,)p2 (x2,x2)]
+          | null xs1 && null xs2 = return [(,)p1 (x1,x2)]
+          | otherwise = do
+              pez1' <- pop pez1
+              pez2' <- pop pez2
+              go pez1' pez2'
+
+    go (pLo, lo,los) (pHi, hi, his)
+
+-- * Splitters
+
+type Splitter a = a -> a -> Maybe a
+
+-- | Perform split forever, until we cannot find a mid-value due to machine precision.
+splitForever :: Integral a => Splitter a
+splitForever lo hi = let mid = lo `div` 2 + hi `div` 2 in
+  if lo == mid || mid == hi then Nothing
+  else Just mid
+
+-- | Perform splitting until @hi - lo <= eps@ .
+splitTill :: Integral a => a -> Splitter a
+splitTill eps lo hi
+  | hi - lo <= eps = Nothing
+  | otherwise      = splitForever lo hi
+
+-- * Searching
+
+-- | Mother of all search variations.
+--
+-- 'searchM' carefully keeps track of the latest predicate found, so that it works well with the 'Evidence' class.
+
+searchM :: forall a m b init . (Monad m, InitializesSearch a init, Eq b) =>
+           init -> Splitter a -> (a -> m b) -> m [Range b a]
+searchM init0 split0 pred0 = do
+  ranges0 <- initializeSearchM init0 pred0
+  go ranges0
+    where
+      go :: [Range b a] -> m [Range b a]
+      go (r1@(p1, (lo1, hi1)):r2@(p2, (lo2, hi2)):rest) = case split0 hi1 lo2 of
+        Nothing   -> (r1:) <$> go (r2:rest)
+        Just mid1 -> do
+          pMid <- pred0 mid1
+          if | p1 == pMid -> go $ (pMid, (lo1,mid1)) : r2 : rest
+             | p2 == pMid -> go $ r1 : (pMid, (mid1,hi2)) : rest
+             | otherwise  -> go $ r1 : (pMid, (mid1,mid1)) : r2 : rest
+      go xs = return xs
+
+-- * Postprocess
+
+-- | Pick up the smallest @a@ that satisfies @pred a == b@ .
+smallest :: (Eq b) => b -> [Range b a] -> Maybe a
+smallest b rs = fst <$> lookup b rs
+
+
+-- | Pick up the largest @a@ that satisfies @pred a == b@ .
+largest :: (Eq b) => b -> [Range b a] -> Maybe a
+largest b rs = snd <$>lookup b rs
diff --git a/Numeric/Search/Combinator/Pure.hs b/Numeric/Search/Combinator/Pure.hs
--- a/Numeric/Search/Combinator/Pure.hs
+++ b/Numeric/Search/Combinator/Pure.hs
@@ -1,3 +1,26 @@
 -- | Pure counterpart for binary search.
 
-module Numeric.Search.Combinator.Pure where
+module Numeric.Search.Combinator.Pure
+       (
+         -- * Evidence
+         M.Evidence(..),
+         -- * Search Range
+         M.Range,
+         M.InitializesSearch,
+         -- * Splitters
+         M.splitForever, M.splitTill,
+
+         -- * Search
+         search,
+         -- * Postprocess
+         M.smallest, M.largest
+       )where
+
+import           Data.Functor.Identity
+import qualified Numeric.Search.Combinator.Monadic as M
+
+
+-- | Perform search over pure predicates. The monadic version of this is 'M.searchM' .
+search :: (M.InitializesSearch a init, Eq b) =>
+           init -> M.Splitter a -> (a -> b) -> [M.Range b a]
+search init0 split0 pred0 = runIdentity $ M.searchM init0 split0 (Identity . pred0)
diff --git a/Numeric/Search/Integer.hs b/Numeric/Search/Integer.hs
--- a/Numeric/Search/Integer.hs
+++ b/Numeric/Search/Integer.hs
@@ -14,10 +14,10 @@
 -----------------------------------------------------------------------------
 
 module Numeric.Search.Integer (
-	-- * One-dimensional searches
-	search, searchFrom, searchTo,
-	-- * Two-dimensional searches
-	search2) where
+        -- * One-dimensional searches
+        search, searchFrom, searchTo,
+        -- * Two-dimensional searches
+        search2) where
 
 import Data.Maybe (fromMaybe)
 
@@ -46,9 +46,9 @@
 searchFrom :: (Integer -> Bool) -> Integer -> Integer
 searchFrom p = search_from 1
   where search_from step l
-	  | p l' = searchIntegerRange p l (l'-1)
-	  | otherwise = search_from (2*step) (l'+1)
-	  where l' = l + step
+          | p l' = searchIntegerRange p l (l'-1)
+          | otherwise = search_from (2*step) (l'+1)
+          where l' = l + step
 
 -- | /O(log(h-n))/.
 -- Search the integers up to a given upper bound.
@@ -59,10 +59,10 @@
 searchTo p h0
   | p h0 = Just (search_to 1 h0)
   | otherwise = Nothing
-  where search_to step h		-- @step >= 1 && p h@
-	  | p h' = search_to (2*step) h'
-	  | otherwise = searchSafeRange p (h'+1) h
-	  where h' = h - step
+  where search_to step h                -- @step >= 1 && p h@
+          | p h' = search_to (2*step) h'
+          | otherwise = searchSafeRange p (h'+1) h
+          where h' = h - step
 
 -- | /O(m log(n\/m))/.
 -- Two-dimensional search, using an algorithm due described in
@@ -84,23 +84,24 @@
 --
 search2 :: (Integer -> Integer -> Bool) -> [(Integer,Integer)]
 search2 p = search2Rect p 0 0 hx hy []
-  where	hx = searchFrom (\ x -> p x 0) 0
-	hy = searchFrom (\ y -> p 0 y) 0
+  where
+    hx = searchFrom (\ x -> p x 0) 0
+    hy = searchFrom (\ y -> p 0 y) 0
 
 search2Rect :: (Integer -> Integer -> Bool) ->
-	Integer -> Integer -> Integer -> Integer ->
-	[(Integer,Integer)] -> [(Integer,Integer)]
+        Integer -> Integer -> Integer -> Integer ->
+        [(Integer,Integer)] -> [(Integer,Integer)]
 search2Rect p lx ly hx hy
   | lx > hx || ly > hy = id
   | lx == hx && ly == hy = if p lx ly then ((lx, ly) :) else id
   | hx-lx > hy-ly =
-	let	mx = (lx+hx) `div` 2
-		my = searchIntegerRange (\ y -> p mx y) ly hy
-	in search2Rect p lx my mx hy . search2Rect p (mx+1) ly hx (my-1)
+        let        mx = (lx+hx) `div` 2
+                   my = searchIntegerRange (\ y -> p mx y) ly hy
+        in search2Rect p lx my mx hy . search2Rect p (mx+1) ly hx (my-1)
   | otherwise =
-	let	mx = searchIntegerRange (\ x -> p x my) lx hx
-		my = (ly+hy) `div` 2
-	in search2Rect p lx (my+1) (mx-1) hy . search2Rect p mx ly hx my
+        let        mx = searchIntegerRange (\ x -> p x my) lx hx
+                   my = (ly+hy) `div` 2
+        in search2Rect p lx (my+1) (mx-1) hy . search2Rect p mx ly hx my
 
 -- | Search a bounded interval of integers.
 --
@@ -122,4 +123,4 @@
   | l == h = l
   | p m = searchSafeRange p l m
   | otherwise = searchSafeRange p (m+1) h
-  where m = (l + h) `div` 2	-- If l < h, then l <= m < h
+  where m = (l + h) `div` 2        -- If l < h, then l <= m < h
diff --git a/binary-search.cabal b/binary-search.cabal
--- a/binary-search.cabal
+++ b/binary-search.cabal
@@ -1,18 +1,42 @@
 Name:           binary-search
-Version:        0.1
-Build-Depends:  base
+Version:        0.9
 Build-Type:     Simple
 License:        BSD3
 license-file:   LICENSE
 Author:         Ross Paterson <ross@soi.city.ac.uk>, Takayuki Muranushi <muranushi@gmail.com>
-Maintainer:     Takayuki Muranushi <muranushi@gmail.com>   
+Maintainer:     Takayuki Muranushi <muranushi@gmail.com>
 Category:       Algorithms
 Synopsis:       Binary and exponential searches
-Description:    These modules 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 'Integer' and bounded integral types.
+Description:
+            __Introduction__
+            .
+            This package provides varieties of binary search functions.
+            .
+            These search function can search for predicates of the type
+            @pred :: (Integral a, Eq b) => a -> b@, or monadic predicates
+            @pred :: (Integral a, Eq b, Monad m) => a -> m b@.
+            The predicates must satisfy that the domain range for any codomain value
+            is continuous; that is, @∀x≦y≦z. pred x == pred z ⇒ pred y == pred x@ .
+            .
+            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 'Integer' and bounded integral types.
+            .
+            The package was created by Ross Paterson, and extended
+            by Takayuki Muranushi, to be used together with SMT solvers.
+            .
+            __The Module Structure__
+            .
+            *  "Numeric.Search.Combinator.Monadic" provides the most generic combinators. "Numeric.Search.Combinator.Pure" provides the pure version of them.
+            *  "Numeric.Search" exports both pure and monadic version.
+            *  "Numeric.Search.Bounded" ,  "Numeric.Search.Integer" ,  "Numeric.Search.Range" provides the various specialized searchers, which means less number of function arguments, and easier to use.
+            .
+            <<https://travis-ci.org/nushio3/binary-search.svg?branch=master>>
+
 cabal-version:      >=1.8
 
 library
@@ -44,7 +68,7 @@
   Ghc-Options: -Wall
   Main-Is: Spec.hs
   Other-Modules:    PureSpec
-                    
+
   Build-Depends:    base >=4.5 && < 5
                   , binary-search