{-
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 =
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over forall s t a b. Field1 s t a b => Lens s t a b
_1 forall a. Num a => a -> a
negate forall a b. (a -> b) -> a -> b
$ Rational -> String -> (Rational, String)
readDecimal' (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 =
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Rational -> String -> (Rational, String)
readDecimal' (forall a. Real a => a -> Rational
toRational Int
i) String
r
readDecimal String
_ = 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 forall a. Num a => a -> a -> a
* Rational
v forall a. Num a => a -> a -> a
+ 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 forall a. Num a => a -> a -> a
+ (forall a. Integral a => a -> Integer
toInteger Int
iforall a. Integral a => a -> a -> Ratio a
%Integer
d)
      in Rational -> String -> Integer -> (Rational, String)
readDigits Rational
v' String
r (Integer
10forall 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 | forall a. Enum a => a -> Int
fromEnum Char
'0' forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
<= forall a. Enum a => a -> Int
fromEnum Char
'9' = forall a. a -> Maybe a
Just (Int
i forall a. Num a => a -> a -> a
- forall a. Enum a => a -> Int
fromEnum Char
'0')
          | Bool
otherwise = forall a. Maybe a
Nothing
  where i :: Int
i = forall a. Enum a => a -> Int
fromEnum Char
c