{-
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 :: 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 (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
_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 (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 (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