    {-
    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 :: forall (m :: Type -> Type).
    MonadFail m =>
    String -> m (Rational, String)
    readDecimal (Char
    '-':Char
    c:String
    r) | Just Int
    i <- Char -> Maybe Int
    asDigit Char
    c =
      (Rational, String) -> m (Rational, String)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ((Rational, String) -> m (Rational, String))
    -> (Rational, String) -> m (Rational, String)
    forall a b. (a -> b) -> a -> b
    $! ASetter (Rational, String) (Rational, String) Rational Rational
    -> (Rational -> Rational)
    -> (Rational, String)
    -> (Rational, String)
    forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
    over ASetter (Rational, String) (Rational, String) Rational Rational
    forall s t a b. Field1 s t a b => Lens s t a b
    Lens (Rational, String) (Rational, String) Rational Rational
    _1 Rational -> Rational
    forall a. Num a => a -> a
    negate ((Rational, String) -> (Rational, String))
    -> (Rational, String) -> (Rational, String)
    forall a b. (a -> b) -> a -> b
    $ Rational -> String -> (Rational, String)
    readDecimal' (Int -> Rational
    forall a. Real a => a -> Rational
    toRational Int
    i) String
    r
    readDecimal (Char
    c:String
    r) | Just Int
    i <- Char -> Maybe Int
    asDigit Char
    c =
      (Rational, String) -> m (Rational, String)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ((Rational, String) -> m (Rational, String))
    -> (Rational, String) -> m (Rational, String)
    forall a b. (a -> b) -> a -> b
    $ Rational -> String -> (Rational, String)
    readDecimal' (Int -> Rational
    forall a. Real a => a -> Rational
    toRational Int
    i) String
    r
    readDecimal String
    _ = String -> m (Rational, String)
    forall a. String -> m a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "Could not parse string."

    readDecimal' :: Rational -- ^ Value so far
                 -> String -- ^ String so far
                 -> (Rational, String)
    readDecimal' :: Rational -> String -> (Rational, String)
    readDecimal' Rational
    v (Char
    c:String
    r) | Just Int
    i <- Char -> Maybe Int
    asDigit Char
    c =
      let v' :: Rational
    v' = Rational
    10 Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    * Rational
    v Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    + Int -> Rational
    forall a. Real a => a -> Rational
    toRational Int
    i
       in Rational -> String -> (Rational, String)
    readDecimal' Rational
    v' String
    r
    readDecimal' Rational
    v (Char
    '.':String
    r) = Rational -> String -> Integer -> (Rational, String)
    readDigits Rational
    v String
    r Integer
    10
    readDecimal' Rational
    v String
    d = (Rational
    v,String
    d)

    readDigits :: Rational
               -> String
               -> Integer -- ^ Value to divide next digit by.
               -> (Rational, String)
    readDigits :: Rational -> String -> Integer -> (Rational, String)
    readDigits Rational
    v (Char
    c:String
    r) Integer
    d
      | Just Int
    i <- Char -> Maybe Int
    asDigit Char
    c =
         let v' :: Rational
    v' = Rational
    v Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    + (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    iInteger -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    %Integer
    d)
          in Rational -> String -> Integer -> (Rational, String)
    readDigits Rational
    v' String
    r (Integer
    10Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    d)
    readDigits Rational
    v (Char
    '?':String
    r) Integer
    _ = (Rational
    v,String
    r)
    readDigits Rational
    v String
    r Integer
    _ = (Rational
    v,String
    r)

    asDigit :: Char -> Maybe Int
    asDigit :: Char -> Maybe Int
    asDigit Char
    c | Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    '0' Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    i Bool -> Bool -> Bool
    && Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    '9' = Int -> Maybe Int
    forall a. a -> Maybe a
    Just (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    '0')
              | Bool
    otherwise = Maybe Int
    forall a. Maybe a
    Nothing
      where i :: Int
    i = Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    c