-- |
-- Module      :  $Header$
-- Copyright   :  (c) 2013-2015 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE Safe, PatternGuards #-}
module Cryptol.TypeCheck.Solver.CrySAT
  (debug
  , Prop(..)
  , Expr(..)
  , PropSet
  , noProps
  , assert
  , checkSat
  , Result(..)
  , InfNat(..)
  , Name
  , toName
  , fromName
  ) where

import qualified Data.Integer.SAT as SAT
import           Data.Set(Set)
import qualified Data.Set as Set
import           Data.Either (partitionEithers)
import           MonadLib
import           Control.Applicative

import           Cryptol.Utils.Panic

infixr 2 :||
infixr 3 :&&
infix  4 :==, :>, :>=
infixl 6 :+, :-
infixl 7 :*


data Name = UserName Int | SysName Int
            deriving (Show,Eq,Ord)

toName :: Int -> Name
toName = UserName

fromName :: Name -> Maybe Int
fromName (UserName x) = Just x
fromName (SysName _)  = Nothing


exportName :: Name -> SAT.Name
exportName n = SAT.toName $ case n of
                              UserName i -> 2 * i
                              SysName i  -> 2 * i + 1

satVar :: Name -> SAT.Expr
satVar = SAT.Var . exportName

importName :: Int -> Name
importName x = case divMod x 2 of
                 (q,r) | r == 0     -> UserName q
                       | otherwise  -> SysName q

satCheckSat :: SAT.PropSet -> Maybe [ (Name,Integer) ]
satCheckSat =  fmap (map imp) . SAT.checkSat
  where imp (x,v) = (importName x, v)


data Prop = Fin Expr
          | Expr :== Expr | Expr :/= Expr
          | Expr :>= Expr | Expr :> Expr
          | Prop :&& Prop | Prop :|| Prop
          | Not Prop
            deriving Show

data Expr = K InfNat
          | Var Name
          | Expr :+ Expr
          | Expr :- Expr
          | Expr :* Expr
          | Div Expr Expr
          | Mod Expr Expr
          | Expr :^^ Expr
          | Min Expr Expr
          | Max Expr Expr
          | Lg2 Expr
          | Width Expr
          | LenFromThen   Expr Expr Expr
          | LenFromThenTo Expr Expr Expr
            deriving Show

debug :: PropSet -> [S]
debug (PS m) = runId $ findAll m

newtype PropSet = PS (ChoiceT Id S)

noProps :: PropSet
noProps = PS $ return S { finVars   = Set.empty
                        , infVars   = Set.empty
                        , linear    = SAT.noProps
                        , nonLin    = []
                        , waitVars  = Set.empty
                        , changes   = False
                        , nextVar   = 0
                        }

assert :: Prop -> PropSet -> PropSet
assert p (PS m) =
  PS $ do s <- m
          (_,s1) <- runStateT s
                  $ unFM
                  $ cvt p >> checkConsistent
          return s1

  where
  cvt (p1 :&& p2) = cvt p1 `mkAnd` cvt p2
  cvt (p1 :|| p2) = cvt p1 `mkOr`  cvt p2
  cvt (Not p1)    = cvt (mkNot p1)
  cvt (Fin t)     = cryDefined t  `mkAnd` cryIsFin t
  cvt (t1 :== t2) = cryDefined t1 `mkAnd` cryDefined t2 `mkAnd` cryIsEq  t1 t2
  cvt (t1 :/= t2) = cryDefined t1 `mkAnd` cryDefined t2 `mkAnd` cryIsNeq t1 t2
  cvt (t1 :>= t2) = cryDefined t1 `mkAnd` cryDefined t2 `mkAnd` cryIsGeq t1 t2
  cvt (t1 :>  t2) = cryDefined t1 `mkAnd` cryDefined t2 `mkAnd` cryIsGt  t1 t2

  mkNot q = case q of
              p1 :&& p2 -> mkNot p1 :|| mkNot p2
              p1 :|| p2 -> mkNot p1 :&& mkNot p2
              Not p1    -> p1
              Fin e     -> e  :== K Inf
              t1 :== t2 -> t1 :/= t2
              t1 :/= t2 -> t1 :== t2
              t1 :>= t2 -> t2 :> t1
              t1 :>  t2 -> t2 :>= t1


data InfNat = Nat Integer | Inf
              deriving (Eq,Ord,Show)

data Result = Sat [(Int,InfNat)]
            | Unsat
            | Unknown
              deriving Show

checkSat :: PropSet -> Result
checkSat (PS ch) =
  runId $
  do mb <- runChoiceT ch
     return $ case mb of
                Nothing -> Unsat
                Just (s, more) ->
                  case getModel s of
                    Just m  -> Sat m
                    Nothing -> case checkSat (PS more) of
                                 Unsat -> Unknown
                                 x     -> x

getModel :: S -> Maybe [(Int,InfNat)]
getModel s =
  do let ps = linear s
     m  <- satCheckSat ps
     let exact = [ satVar x SAT.:== SAT.K v | (x,v) <- m ]
     m1 <- satCheckSat $ foldr SAT.assert SAT.noProps
                       $ exact ++
                         [ satVar x SAT.:== cvt m nl | (x,nl) <- nonLin s ]
     return [ (x,v) | (UserName x, v)
                          <- [ (x,Inf)  | x <- Set.toList (infVars s) ] ++
                             [ (x,Nat v) | (x,v) <- m1 ] ]

  where
  lkp m x = case lookup x m of
              Nothing -> 0
              Just n  -> n
  cvt m nl =
    case nl of
      NLDiv e x  -> SAT.Div e (lkp m x)
      NLMod e x  -> SAT.Mod e (lkp m x)
      NLExp x y  -> SAT.K $ lkp m x ^ lkp m y
      NLExpL k y -> SAT.K $ k ^ lkp m y
      NLExpR x k -> SAT.K $ lkp m x ^ k
      NLMul x y  -> SAT.K $ lkp m x * lkp m y
      NLLg2 x    -> SAT.K $ nLg2 (lkp m x)



--------------------------------------------------------------------------------

data NonLin = NLDiv SAT.Expr Name
            | NLMod SAT.Expr Name
            | NLExp Name Name
            | NLExpL Integer Name
            | NLExpR Name Integer
            | NLMul Name Name
            | NLLg2 Name
              deriving Show

setNL :: Name -> Integer -> (Name,NonLin) -> Either (Name,NonLin) SAT.Prop
setNL x n (v, nl) = case it of
                      Left nl1 -> Left (x,nl1)
                      Right e  -> Right (satVar v SAT.:== e)
  where
  it = case nl of
         NLDiv e y  | x == y            -> Right $ SAT.Div e n
         NLMod e y  | x == y            -> Right $ SAT.Mod e n
         NLMul y z  | y == z && x == y  -> Right $ SAT.K $ n * n
                    | x == y            -> Right $ n SAT.:* satVar z
                    | x == z            -> Right $ n SAT.:* satVar y
         NLExp y z  | y == z && x == y  -> Right $ SAT.K $ n ^ n
                    | x == y            -> Left  $ NLExpL n z
                    | x == z            -> Left  $ NLExpR y n
         NLExpL k z | x == z            -> Right $ SAT.K $ k ^ n
         NLExpR y k | x == y            -> Right $ SAT.K $ n ^ k
         NLLg2 y    | x == y            -> Right $ SAT.K $ nLg2 n
         _                              -> Left nl


data S = S
  { finVars   :: Set Name     -- all of these are ordinary finite vars
  , infVars   :: Set Name     -- these vars are all equal to Inf (XXX: subst?)
  , linear    :: SAT.PropSet  -- linear constraints
  , nonLin    :: [(Name,NonLin)] -- non-linear (delayed) constraints
  , waitVars  :: Set Name     -- waiting for improvements to these
                              -- improvements here may turn non-lin into lin
                              -- INV: these are a subset of finVars
  , changes   :: Bool         -- temp: did something improve last time?
                              -- if so we should restart.
  , nextVar   :: !Int         -- source of new variables
  }

newtype FM a = FM { unFM :: StateT S (ChoiceT Id) a }

instance Functor FM where
  fmap f (FM m) = FM (fmap f m)

instance Applicative FM where
  pure x          = FM (pure x)
  FM mf <*> FM mx = FM (mf <*> mx)

instance Alternative FM where
  empty = mzero
  (<|>) = mplus

instance Monad FM where
  return x        = FM (return x)
  FM mf >>= k     = FM (mf >>= unFM . k)

instance MonadPlus FM where
  mzero = FM mzero
  mplus (FM m1) (FM m2) = FM (mplus m1 m2)


noChanges :: F
noChanges = FM $ sets_ $ \s -> s { changes = False }

addLin :: SAT.Prop -> F
addLin p = FM $ sets_ $ \s -> s { linear = SAT.assert p (linear s)
                                , changes = True }


checkConsistent :: F
checkConsistent =
  do s <- FM get
     when (changes s) $
       case satCheckSat (linear s) of
         Nothing -> mzero
         Just m  ->
          do noChanges
             mapM_ tryImprove [ (x,v) | (x,v) <- m, x `Set.member` waitVars s ]
             checkConsistent

tryImprove :: (Name,Integer) -> F
tryImprove (x,n) =
  do s <- FM get
     case satCheckSat (SAT.assert (satVar x SAT.:/= SAT.K n) (linear s)) of
       Nothing -> doImprove x n
       Just _  -> return ()

doImprove :: Name -> Integer -> F
doImprove x n =
  do resumed <- FM $ sets $ \s ->
       let (stay, go) = partitionEithers $ map (setNL x n) (nonLin s)
       in (go, s { nonLin = stay, waitVars = Set.delete x (waitVars s) })
     mapM_ addLin resumed


getLin :: FM SAT.PropSet
getLin = FM $ linear `fmap` get

newName :: FM Name
newName = FM $ sets $ \s -> let x = nextVar s
                            in (SysName x, s { nextVar = x + 1 })

addNonLin :: NonLin -> FM SAT.Expr
addNonLin nl =
  do x <- newName
     FM $ sets_ $ \s -> s { nonLin = (x,nl) : nonLin s }
     isFin x
     return $ satVar x


type F = FM ()

mkAnd :: F -> F -> F
mkAnd f1 f2 = f1 >> f2

mkOr  :: F -> F -> F
mkOr f1 f2 = f1 `mplus` f2

tt :: F
tt = return ()

ff :: F
ff = mzero

isEq :: Expr -> Expr -> F
isEq t1 t2 = addLin =<< ((SAT.:==) <$> mkLin t1 <*> mkLin t2)

isGt :: Expr -> Expr -> F
isGt t1 t2 = addLin =<< ((SAT.:>) <$> mkLin t1 <*> mkLin t2)

isFin :: Name -> F
isFin x = do FM $ do s <- get
                     guard (Set.notMember x (infVars s))
                     set s { finVars = Set.insert x (finVars s) }
             addLin (satVar x SAT.:>= SAT.K 0)

isInf :: Name -> F
isInf x = FM $ do s <- get
                  guard (Set.notMember x (finVars s))
                  set s { infVars = Set.insert x (infVars s) }



--------------------------------------------------------------------------------


cryIsEq :: Expr -> Expr -> F
cryIsEq t1 t2 = (cryIsInf t1 `mkAnd` cryIsInf t2) `mkOr`
                (cryIsFin t1 `mkAnd` cryIsFin t2 `mkAnd` isEq t1 t2)

cryIsNeq :: Expr -> Expr -> F
cryIsNeq t1 t2 = cryIsGt t1 t2 `mkOr` cryIsGt t2 t1

cryIsGt :: Expr -> Expr -> F
cryIsGt t1 t2 = (cryIsInf t1 `mkAnd` cryIsFin t2) `mkOr`
                (cryIsFin t1 `mkAnd` cryIsFin t2  `mkAnd` isGt t1 t2)

cryIsGeq :: Expr -> Expr -> F
cryIsGeq t1 t2 = cryIsEq t1 t2 `mkOr` cryIsGt t1 t2

cryIsDifferent :: Expr -> Expr -> F
cryIsDifferent t1 t2 = cryIsGt t1 t2 `mkOr` cryIsGt t2 t1


{- XXX: Are we being a bit too strict here?
Some oprtations may be defined even if one of their arguments
is not.  For example, perhaps the following should not be rejected:
inf + undefined -> inf
0 - undefined   -> 0
0 * undefined   -> 0
mod undefined 1 -> 0
1 ^ undefined   -> 1
undefined ^ 0   -> 1`
min 0 undefined -> 0
max inf undefined -> inf
-}
cryDefined :: Expr -> F
cryDefined ty =
  case ty of
    K _        -> tt
    Var _      -> tt
    t1 :+ t2  -> cryDefined t1 `mkAnd` cryDefined t2
    t1 :- t2  -> cryDefined t1 `mkAnd` cryDefined t2 `mkAnd`
                 cryIsFin t2   `mkAnd` cryIsGeq t1 t2
    t1 :* t2  -> cryDefined t1 `mkAnd` cryDefined t2
    Div t1 t2  -> cryDefined t1 `mkAnd` cryDefined t2 `mkAnd`
                  cryIsFin t1   `mkAnd` cryIsGt t2 (K $ Nat 0)
    Mod t1 t2  -> cryDefined t1 `mkAnd` cryDefined t2 `mkAnd`
                  cryIsFin t1   `mkAnd` cryIsGt t2 (K $ Nat 0)

    t1 :^^ t2  -> cryDefined t1 `mkAnd` cryDefined t2
    Min t1 t2  -> cryDefined t1 `mkAnd` cryDefined t2
    Max t1 t2  -> cryDefined t1 `mkAnd` cryDefined t2
    Lg2 t1     -> cryDefined t1
    Width t1   -> cryDefined t1
    LenFromThen t1 t2 t3 ->
      cryDefined t1 `mkAnd` cryDefined t2 `mkAnd`
      cryDefined t3 `mkAnd` cryIsFin t1   `mkAnd`
      cryIsFin t2   `mkAnd` cryIsFin t3  `mkAnd`
      cryIsDifferent t1 t2
    LenFromThenTo t1 t2 t3 ->
      cryDefined t1 `mkAnd` cryDefined t2 `mkAnd`
      cryDefined t3 `mkAnd` cryIsFin t1   `mkAnd`
      cryIsFin t2   `mkAnd` cryIsFin t3  `mkAnd`
      cryIsDifferent t1 t2


-- Assuming a defined input.
cryIsInf :: Expr -> F
cryIsInf ty =
  case ty of
    K Inf               -> tt
    K (Nat _)           -> ff
    Var x               -> isInf x
    t1 :+ t2            -> cryIsInf t1 `mkOr` cryIsInf t2
    t1 :- _             -> cryIsInf t1
    t1 :* t2            -> (cryIsInf t1 `mkAnd` cryIsGt t2 (K $ Nat 0))`mkOr`
                           (cryIsInf t2 `mkAnd` cryIsGt t1 (K $ Nat 0))
    Div t1 _            -> cryIsInf t1
    Mod _  _            -> ff
    t1 :^^ t2           -> (cryIsInf t1 `mkAnd` cryIsGt t2 (K $ Nat 0))`mkOr`
                           (cryIsInf t2 `mkAnd` cryIsGt t1 (K $ Nat 1))
    Min t1 t2           -> cryIsInf t1  `mkAnd` cryIsInf t2
    Max t1 t2           -> cryIsInf t1 `mkOr` cryIsInf t2
    Lg2 t1              -> cryIsInf t1
    Width t1            -> cryIsInf t1
    LenFromThen _ _ _   -> ff
    LenFromThenTo _ _ _ -> ff


-- Assuming a defined input.
cryIsFin :: Expr -> F
cryIsFin ty =
  case ty of
    K Inf         -> ff
    K (Nat _)     -> tt
    Var x         -> isFin x
    t1 :+ t2      -> cryIsFin t1 `mkAnd` cryIsFin t2
    t1 :- _       -> cryIsFin t1
    t1 :* t2      -> (cryIsFin t1 `mkAnd` cryIsFin t2) `mkOr`
                      cryIsEq t1 (K $ Nat 0)       `mkOr`
                      cryIsEq t2 (K $ Nat 0)

    Div t1 _      -> cryIsFin t1
    Mod _ _       -> tt
    t1 :^^ t2     -> (cryIsFin t1 `mkAnd` cryIsFin t2) `mkOr`
                      cryIsEq t1 (K $ Nat 0)            `mkOr`
                      cryIsEq t1 (K $ Nat 1)            `mkOr`
                      cryIsEq t2 (K $ Nat 0)

    Min t1 t2     -> (cryIsFin t1 `mkAnd` cryIsGeq t2 t1) `mkOr`
                     (cryIsFin t2 `mkAnd` cryIsGeq t1 t2)

    Max t1 t2     -> cryIsFin t1 `mkAnd` cryIsFin t2
    Lg2 t1        -> cryIsFin t1
    Width t1      -> cryIsFin t1
    LenFromThen  _ _ _   -> tt
    LenFromThenTo  _ _ _ -> tt

-- eliminate Inf terms from finite values
cryNoInf :: Expr -> FM Expr
cryNoInf ty =
  case ty of
    K Inf :+ _   -> mzero
    _ :+ K Inf   -> mzero

    K Inf :- _   -> mzero
    _ :- K Inf   -> mzero

    K Inf :* t2  -> cryIsEq t2 (K $ Nat 0) >> return (K $ Nat 0)
    t1 :* K Inf  -> cryIsEq t1 (K $ Nat 0) >> return (K $ Nat 0)

    Div (K Inf) _    -> mzero
    Div _ (K Inf)    -> return $ K $ Nat 0

    Mod (K Inf) _    -> mzero
    Mod t1 (K Inf)   -> cryNoInf t1

    K Inf :^^ t2   -> cryIsEq t2 (K $ Nat 0) >> return (K $ Nat 1)
    t1 :^^ K Inf   -> msum [ cryIsEq t1 (K $ Nat 0) >> return (K $ Nat 0)
                           , cryIsEq t1 (K $ Nat 1) >> return (K $ Nat 1)
                           ]

    Min (K Inf) t2   -> cryNoInf t2
    Min t1 (K Inf)   -> cryNoInf t1

    Max (K Inf) _    -> mzero
    Max _ (K Inf)    -> mzero

    Lg2 (K Inf)      -> mzero

    Width (K Inf)    -> mzero

    LenFromThen (K Inf) _ _   -> mzero
    LenFromThen _ (K Inf) _   -> mzero
    LenFromThen _ _ (K Inf)   -> mzero

    LenFromThenTo (K Inf) _ _ -> mzero
    LenFromThenTo _ (K Inf) _ -> mzero
    LenFromThenTo _ _ (K Inf) -> mzero

    K Inf                    -> mzero

    _                        -> return ty


-- Assumes a finite, and defined input.
mkLin :: Expr -> FM SAT.Expr
mkLin ty0 =
  cryNoInf ty0 >>= \ty ->
  case ty of
    K Inf                  -> panic "Cryptol.TypeCheck.Solver.CrySAT.mkLin"
                                [ "K Inf after cryNoInf" ]
    K (Nat n)              -> return (SAT.K n)
    Var x                  -> isFin x >> return (satVar x)
    t1 :+ t2               -> (SAT.:+)            <$> mkLin t1 <*> mkLin t2
    t1 :- t2               -> (SAT.:-)            <$> mkLin t1 <*> mkLin t2
    t1 :* t2               -> join $ mkMul        <$> mkLin t1 <*> mkLin t2
    Div t1 t2              -> join $ mkDiv        <$> mkLin t1 <*> mkLin t2
    Mod t1 t2              -> join $ mkMod        <$> mkLin t1 <*> mkLin t2
    t1 :^^ t2              -> join $ mkExp        <$> mkLin t1 <*> mkLin t2
    Min t1 t2              -> mkMin               <$> mkLin t1 <*> mkLin t2
    Max t1 t2              -> mkMax               <$> mkLin t1 <*> mkLin t2
    Lg2 t1                 -> join $ mkLg2        <$> mkLin t1
    Width t1               -> join $ mkWidth       <$> mkLin t1
    LenFromThen t1 t2 t3   -> join $ mkLenFromThen <$> mkLin t1
                                                   <*> mkLin t2
                                                   <*> mkLin t3
    LenFromThenTo t1 t2 t3 -> join $ mkLenFromThenTo <$> mkLin t1
                                                     <*> mkLin t2
                                                     <*> mkLin t3
  where
  mkMin t1 t2 = SAT.If (t1 SAT.:< t2) t1 t2
  mkMax t1 t2 = SAT.If (t1 SAT.:< t2) t2 t1

  mkMul t1 t2 =
    do mb <- toConst t1
       case mb of
         Just n -> return (n SAT.:* t2)
         Nothing ->
            do mb1 <- toConst t2
               case mb1 of
                 Just n  -> return (n SAT.:* t1)
                 Nothing -> do x <- toVar t1
                               y <- toVar t2
                               addNonLin (NLMul x y)

  mkDiv t1 t2 =
    do mb <- toConst t2
       case mb of
         Just n  -> return (SAT.Div t1 n)
         Nothing -> do x <- toVar t2
                       addNonLin (NLDiv t1 x)

  mkMod t1 t2 =
    do mb <- toConst t2
       case mb of
         Just n  -> return (SAT.Mod t1 n)
         Nothing -> do x <- toVar t2
                       addNonLin (NLMod t1 x)

  mkLg2 t1 =
    do mb <- toConst t1
       case mb of
         Just n   -> return $ SAT.K $ nLg2 n
         Nothing  -> do x <- toVar t1
                        addNonLin (NLLg2 x)

  mkWidth t1 = mkLg2 (SAT.K 1 SAT.:+ t1)

  mkExp t1 t2 =
    do mb <- toConst t1
       case mb of
         Just n ->
           do mb1 <- toConst t2
              case mb1 of
                Just m  -> return $ SAT.K $ n ^ m
                Nothing -> do y <- toVar t2
                              addNonLin (NLExpL n y)
         Nothing -> do x <- toVar t1
                       y <- toVar t2
                       addNonLin (NLExp x y)



  -- derived
  mkLenFromThen x y w =
    do upTo <- msum [ do addLin (y SAT.:> x)
                         w1 <- mkExp (SAT.K 2) w
                         return (w1 SAT.:- SAT.K 1)
                    , do addLin (x SAT.:> y)
                         return (SAT.K 0)
                    ]
       mkLenFromThenTo x y upTo

  mkLenFromThenTo x y z =
    msum [ do addLin (x SAT.:> y)   -- going down
              msum [ addLin (z SAT.:> x)  >> return (SAT.K 0)
                   , addLin (z SAT.:== x) >> return (SAT.K 1)
                   , do addLin (z SAT.:< x)
                        t <- mkDiv (x SAT.:- z) (x SAT.:- y)
                        return (SAT.K 1 SAT.:+ t)
                   ]

         , do addLin (x SAT.:< y)   -- going up
              msum [ addLin (z SAT.:< x)  >> return (SAT.K 0)
                   , addLin (z SAT.:== x) >> return (SAT.K 1)
                   , do addLin (z SAT.:> x)
                        t <- mkDiv (z SAT.:- x) (y SAT.:- x)
                        return (SAT.K 1 SAT.:+ t)
                   ]

         ]

toConst :: SAT.Expr -> FM (Maybe Integer)
toConst (SAT.K n) = return (Just n)
toConst t = do l <- getLin
               case SAT.getExprRange t l of
                 Nothing -> return Nothing
                 Just vs -> msum $ map (return . Just) vs

toVar :: SAT.Expr -> FM Name
toVar (SAT.Var x) | Just n <- SAT.fromName x = return $ importName n
toVar e       = do x <- newName
                   addLin (satVar x SAT.:== e)
                   FM $ sets_ $ \s -> s { waitVars = Set.insert x (waitVars s) }
                   return x

--------------------------------------------------------------------------------

-- | Rounds up.
-- @lg2 x = y@, iff @y@ is the smallest number such that @x <= 2 ^ y@
nLg2 :: Integer -> Integer
nLg2 0  = 0
nLg2 n  = case genLog n 2 of
            Just (x,exact) | exact     -> x
                           | otherwise -> x + 1
            Nothing -> panic "Cryptol.TypeCheck.Solver.CrySAT.nLg2"
                         [ "genLog returned Nothing" ]



--------------------------------------------------------------------------------

-- | Compute the logarithm of a number in the given base, rounded down to the
-- closest integer.  The boolean indicates if we the result is exact
-- (i.e., True means no rounding happened, False means we rounded down).
-- The logarithm base is the second argument.
genLog :: Integer -> Integer -> Maybe (Integer, Bool)
genLog x 0    = if x == 1 then Just (0, True) else Nothing
genLog _ 1    = Nothing
genLog 0 _    = Nothing
genLog x base = Just (exactLoop 0 x)
  where
  exactLoop s i
    | i == 1     = (s,True)
    | i < base   = (s,False)
    | otherwise  =
        let s1 = s + 1
        in s1 `seq` case divMod i base of
                      (j,r)
                        | r == 0    -> exactLoop s1 j
                        | otherwise -> (underLoop s1 j, False)

  underLoop s i
    | i < base  = s
    | otherwise = let s1 = s + 1 in s1 `seq` underLoop s1 (div i base)