content: {-
  Module           : What4.Utils.ReadDecimal
  Description      : Parsing for decimal values
  Copyright        : (c) Galois, Inc 2014-2020
  License          : BSD3
  Maintainer       : Joe Hendrix <jhendrix@galois.com>
  
  Provides a function for reading decimal numbers returned
  by Z3 or Yices.
  -}
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE PatternGuards #-}
  module What4.Protocol.ReadDecimal
    ( readDecimal
    ) where
  
  #if !MIN_VERSION_base(4,13,0)
  import Control.Monad.Fail( MonadFail )
  #endif
  
  import Control.Lens (over, _1)
  import Data.Ratio
  
  -- | Read decimal number, returning rational and rest of string, or a failure
  -- message if first character is not a digit.
  --
  -- A decimal number has the form (-)([0..9])+([0..9])+'.'([0.9]'*('?')?
  readDecimal :: MonadFail m => String -> m (Rational, String)
  readDecimal ('-':c:r) | Just i <- asDigit c =
    return $! over _1 negate $ readDecimal' (toRational i) r
  readDecimal (c:r) | Just i <- asDigit c =
    return $ readDecimal' (toRational i) r
  readDecimal _ = fail "Could not parse string."
  
  readDecimal' :: Rational -- ^ Value so far
               -> String -- ^ String so far
               -> (Rational, String)
  readDecimal' v (c:r) | Just i <- asDigit c =
    let v' = 10 * v + toRational i
     in readDecimal' v' r
  readDecimal' v ('.':r) = readDigits v r 10
  readDecimal' v d = (v,d)
  
  readDigits :: Rational
             -> String
             -> Integer -- ^ Value to divide next digit by.
             -> (Rational, String)
  readDigits v (c:r) d
    | Just i <- asDigit c =
       let v' = v + (toInteger i%d)
        in readDigits v' r (10*d)
  readDigits v ('?':r) _ = (v,r)
  readDigits v r _ = (v,r)
  
  asDigit :: Char -> Maybe Int
  asDigit c | fromEnum '0' <= i && i <= fromEnum '9' = Just (i - fromEnum '0')
            | otherwise = Nothing
    where i = fromEnum c
  