{-# LANGUAGE FlexibleInstances #-}
{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}
module Data.SBV.Core.AlgReals (
AlgReal(..)
, AlgRealPoly(..)
, mkPolyReal
, algRealToSMTLib2
, algRealToHaskell
, mergeAlgReals
, isExactRational
, algRealStructuralEqual
, algRealStructuralCompare
)
where
import Data.List (sortBy, isPrefixOf, partition)
import Data.Ratio ((%), numerator, denominator)
import Data.Function (on)
import System.Random
import Test.QuickCheck (Arbitrary(..))
data AlgReal = AlgRational Bool Rational
| AlgPolyRoot (Integer, AlgRealPoly) (Maybe String)
isExactRational :: AlgReal -> Bool
isExactRational :: AlgReal -> Bool
isExactRational (AlgRational True _) = Bool
True
isExactRational _ = Bool
False
newtype AlgRealPoly = AlgRealPoly [(Integer, Integer)]
deriving (AlgRealPoly -> AlgRealPoly -> Bool
(AlgRealPoly -> AlgRealPoly -> Bool)
-> (AlgRealPoly -> AlgRealPoly -> Bool) -> Eq AlgRealPoly
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AlgRealPoly -> AlgRealPoly -> Bool
$c/= :: AlgRealPoly -> AlgRealPoly -> Bool
== :: AlgRealPoly -> AlgRealPoly -> Bool
$c== :: AlgRealPoly -> AlgRealPoly -> Bool
Eq, Eq AlgRealPoly
Eq AlgRealPoly =>
(AlgRealPoly -> AlgRealPoly -> Ordering)
-> (AlgRealPoly -> AlgRealPoly -> Bool)
-> (AlgRealPoly -> AlgRealPoly -> Bool)
-> (AlgRealPoly -> AlgRealPoly -> Bool)
-> (AlgRealPoly -> AlgRealPoly -> Bool)
-> (AlgRealPoly -> AlgRealPoly -> AlgRealPoly)
-> (AlgRealPoly -> AlgRealPoly -> AlgRealPoly)
-> Ord AlgRealPoly
AlgRealPoly -> AlgRealPoly -> Bool
AlgRealPoly -> AlgRealPoly -> Ordering
AlgRealPoly -> AlgRealPoly -> AlgRealPoly
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly
$cmin :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly
max :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly
$cmax :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly
>= :: AlgRealPoly -> AlgRealPoly -> Bool
$c>= :: AlgRealPoly -> AlgRealPoly -> Bool
> :: AlgRealPoly -> AlgRealPoly -> Bool
$c> :: AlgRealPoly -> AlgRealPoly -> Bool
<= :: AlgRealPoly -> AlgRealPoly -> Bool
$c<= :: AlgRealPoly -> AlgRealPoly -> Bool
< :: AlgRealPoly -> AlgRealPoly -> Bool
$c< :: AlgRealPoly -> AlgRealPoly -> Bool
compare :: AlgRealPoly -> AlgRealPoly -> Ordering
$ccompare :: AlgRealPoly -> AlgRealPoly -> Ordering
$cp1Ord :: Eq AlgRealPoly
Ord)
mkPolyReal :: Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
mkPolyReal :: Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
mkPolyReal (Left (exact :: Bool
exact, str :: String
str))
= case (String
str, (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '.') String
str) of
("", (_, _)) -> Bool -> Rational -> AlgReal
AlgRational Bool
exact 0
(_, (x :: String
x, '.':y :: String
y)) -> Bool -> Rational -> AlgReal
AlgRational Bool
exact (String -> Integer
forall a. Read a => String -> a
read (String
xString -> String -> String
forall a. [a] -> [a] -> [a]
++String
y) Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% (10 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
y))
(_, (x :: String
x, _)) -> Bool -> Rational -> AlgReal
AlgRational Bool
exact (String -> Integer
forall a. Read a => String -> a
read String
x Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% 1)
mkPolyReal (Right (k :: Integer
k, coeffs :: [(Integer, Integer)]
coeffs))
= (Integer, AlgRealPoly) -> Maybe String -> AlgReal
AlgPolyRoot (Integer
k, [(Integer, Integer)] -> AlgRealPoly
AlgRealPoly ([(Integer, Integer)] -> [(Integer, Integer)]
normalize [(Integer, Integer)]
coeffs)) Maybe String
forall a. Maybe a
Nothing
where normalize :: [(Integer, Integer)] -> [(Integer, Integer)]
normalize :: [(Integer, Integer)] -> [(Integer, Integer)]
normalize = [(Integer, Integer)] -> [(Integer, Integer)]
forall b a. (Eq b, Num a) => [(a, b)] -> [(a, b)]
merge ([(Integer, Integer)] -> [(Integer, Integer)])
-> ([(Integer, Integer)] -> [(Integer, Integer)])
-> [(Integer, Integer)]
-> [(Integer, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Integer, Integer) -> (Integer, Integer) -> Ordering)
-> [(Integer, Integer)] -> [(Integer, Integer)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Integer -> Integer -> Ordering) -> Integer -> Integer -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer -> Integer -> Ordering)
-> ((Integer, Integer) -> Integer)
-> (Integer, Integer)
-> (Integer, Integer)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Integer, Integer) -> Integer
forall a b. (a, b) -> b
snd)
merge :: [(a, b)] -> [(a, b)]
merge [] = []
merge [x :: (a, b)
x] = [(a, b)
x]
merge ((a :: a
a, b :: b
b):r :: [(a, b)]
r@((c :: a
c, d :: b
d):xs :: [(a, b)]
xs))
| b
b b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
d = [(a, b)] -> [(a, b)]
merge ((a
aa -> a -> a
forall a. Num a => a -> a -> a
+a
c, b
b)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
xs)
| Bool
True = (a
a, b
b) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)]
merge [(a, b)]
r
instance Show AlgRealPoly where
show :: AlgRealPoly -> String
show (AlgRealPoly xs :: [(Integer, Integer)]
xs) = String -> String
chkEmpty ([String] -> String
join ([[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [(Integer, Integer) -> [String]
forall a a.
(Eq a, Eq a, Num a, Num a, Show a, Show a) =>
(a, a) -> [String]
term (Integer, Integer)
p | p :: (Integer, Integer)
p@(_, x :: Integer
x) <- [(Integer, Integer)]
xs, Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= 0])) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
c
where c :: Integer
c = -1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* [Integer] -> Integer
forall a. [a] -> a
head ([Integer
k | (k :: Integer
k, 0) <- [(Integer, Integer)]
xs] [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ [0])
term :: (a, a) -> [String]
term ( 0, _) = []
term ( 1, 1) = [ "x"]
term ( 1, p :: a
p) = [ "x^" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p]
term (-1, 1) = ["-x"]
term (-1, p :: a
p) = ["-x^" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p]
term (k :: a
k, 1) = [a -> String
forall a. Show a => a -> String
show a
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ "x"]
term (k :: a
k, p :: a
p) = [a -> String
forall a. Show a => a -> String
show a
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ "x^" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p]
join :: [String] -> String
join [] = ""
join (k :: String
k:ks :: [String]
ks) = String
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
join [String]
ks
where s :: String
s = case [String]
ks of
[] -> ""
(y :: String
y:_) | "-" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
y -> ""
| "+" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
y -> ""
| Bool
True -> "+"
chkEmpty :: String -> String
chkEmpty s :: String
s = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s then "0" else String
s
instance Show AlgReal where
show :: AlgReal -> String
show (AlgRational exact :: Bool
exact a :: Rational
a) = Bool -> Rational -> String
showRat Bool
exact Rational
a
show (AlgPolyRoot (i :: Integer
i, p :: AlgRealPoly
p) mbApprox :: Maybe String
mbApprox) = "root(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ ", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AlgRealPoly -> String
forall a. Show a => a -> String
show AlgRealPoly
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" String -> String
app Maybe String
mbApprox
where app :: String -> String
app v :: String
v | String -> Char
forall a. [a] -> a
last String
v Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '?' = " = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. [a] -> [a]
init String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "..."
| Bool
True = " = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v
lift1 :: String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 :: String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 _ o :: Rational -> Rational
o (AlgRational e :: Bool
e a :: Rational
a) = Bool -> Rational -> AlgReal
AlgRational Bool
e (Rational -> Rational
o Rational
a)
lift1 nm :: String
nm _ a :: AlgReal
a = String -> AlgReal
forall a. HasCallStack => String -> a
error (String -> AlgReal) -> String -> AlgReal
forall a b. (a -> b) -> a -> b
$ "AlgReal." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": unsupported argument: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
forall a. Show a => a -> String
show AlgReal
a
lift2 :: String -> (Rational -> Rational -> Rational) -> AlgReal -> AlgReal -> AlgReal
lift2 :: String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 _ o :: Rational -> Rational -> Rational
o (AlgRational True a :: Rational
a) (AlgRational True b :: Rational
b) = Bool -> Rational -> AlgReal
AlgRational Bool
True (Rational
a Rational -> Rational -> Rational
`o` Rational
b)
lift2 nm :: String
nm _ a :: AlgReal
a b :: AlgReal
b = String -> AlgReal
forall a. HasCallStack => String -> a
error (String -> AlgReal) -> String -> AlgReal
forall a b. (a -> b) -> a -> b
$ "AlgReal." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": unsupported arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (AlgReal, AlgReal) -> String
forall a. Show a => a -> String
show (AlgReal
a, AlgReal
b)
instance Eq AlgReal where
AlgRational True a :: Rational
a == :: AlgReal -> AlgReal -> Bool
== AlgRational True b :: Rational
b = Rational
a Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
b
a :: AlgReal
a == b :: AlgReal
b = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "AlgReal.==: unsupported arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (AlgReal, AlgReal) -> String
forall a. Show a => a -> String
show (AlgReal
a, AlgReal
b)
instance Ord AlgReal where
AlgRational True a :: Rational
a compare :: AlgReal -> AlgReal -> Ordering
`compare` AlgRational True b :: Rational
b = Rational
a Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Rational
b
a :: AlgReal
a `compare` b :: AlgReal
b = String -> Ordering
forall a. HasCallStack => String -> a
error (String -> Ordering) -> String -> Ordering
forall a b. (a -> b) -> a -> b
$ "AlgReal.compare: unsupported arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (AlgReal, AlgReal) -> String
forall a. Show a => a -> String
show (AlgReal
a, AlgReal
b)
algRealStructuralEqual :: AlgReal -> AlgReal -> Bool
AlgRational a :: Bool
a b :: Rational
b algRealStructuralEqual :: AlgReal -> AlgReal -> Bool
`algRealStructuralEqual` AlgRational c :: Bool
c d :: Rational
d = (Bool
a, Rational
b) (Bool, Rational) -> (Bool, Rational) -> Bool
forall a. Eq a => a -> a -> Bool
== (Bool
c, Rational
d)
AlgPolyRoot a :: (Integer, AlgRealPoly)
a b :: Maybe String
b `algRealStructuralEqual` AlgPolyRoot c :: (Integer, AlgRealPoly)
c d :: Maybe String
d = ((Integer, AlgRealPoly)
a, Maybe String
b) ((Integer, AlgRealPoly), Maybe String)
-> ((Integer, AlgRealPoly), Maybe String) -> Bool
forall a. Eq a => a -> a -> Bool
== ((Integer, AlgRealPoly)
c, Maybe String
d)
_ `algRealStructuralEqual` _ = Bool
False
algRealStructuralCompare :: AlgReal -> AlgReal -> Ordering
AlgRational a :: Bool
a b :: Rational
b algRealStructuralCompare :: AlgReal -> AlgReal -> Ordering
`algRealStructuralCompare` AlgRational c :: Bool
c d :: Rational
d = (Bool
a, Rational
b) (Bool, Rational) -> (Bool, Rational) -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` (Bool
c, Rational
d)
AlgRational _ _ `algRealStructuralCompare` AlgPolyRoot _ _ = Ordering
LT
AlgPolyRoot _ _ `algRealStructuralCompare` AlgRational _ _ = Ordering
GT
AlgPolyRoot a :: (Integer, AlgRealPoly)
a b :: Maybe String
b `algRealStructuralCompare` AlgPolyRoot c :: (Integer, AlgRealPoly)
c d :: Maybe String
d = ((Integer, AlgRealPoly)
a, Maybe String
b) ((Integer, AlgRealPoly), Maybe String)
-> ((Integer, AlgRealPoly), Maybe String) -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` ((Integer, AlgRealPoly)
c, Maybe String
d)
instance Num AlgReal where
+ :: AlgReal -> AlgReal -> AlgReal
(+) = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 "+" Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(+)
* :: AlgReal -> AlgReal -> AlgReal
(*) = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 "*" Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(*)
(-) = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 "-" (-)
negate :: AlgReal -> AlgReal
negate = String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 "negate" Rational -> Rational
forall a. Num a => a -> a
negate
abs :: AlgReal -> AlgReal
abs = String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 "abs" Rational -> Rational
forall a. Num a => a -> a
abs
signum :: AlgReal -> AlgReal
signum = String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 "signum" Rational -> Rational
forall a. Num a => a -> a
signum
fromInteger :: Integer -> AlgReal
fromInteger = Bool -> Rational -> AlgReal
AlgRational Bool
True (Rational -> AlgReal)
-> (Integer -> Rational) -> Integer -> AlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Rational
forall a. Num a => Integer -> a
fromInteger
instance Fractional AlgReal where
(AlgRational True _) / :: AlgReal -> AlgReal -> AlgReal
/ (AlgRational True b :: Rational
b) | Rational
b Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = 0
a :: AlgReal
a / b :: AlgReal
b = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 "/" Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
(/) AlgReal
a AlgReal
b
fromRational :: Rational -> AlgReal
fromRational = Bool -> Rational -> AlgReal
AlgRational Bool
True
instance Real AlgReal where
toRational :: AlgReal -> Rational
toRational (AlgRational True v :: Rational
v) = Rational
v
toRational x :: AlgReal
x = String -> Rational
forall a. HasCallStack => String -> a
error (String -> Rational) -> String -> Rational
forall a b. (a -> b) -> a -> b
$ "AlgReal.toRational: Argument cannot be represented as a rational value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
algRealToHaskell AlgReal
x
instance Random Rational where
random :: g -> (Rational, g)
random g :: g
g = (Integer
a Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
b', g
g'')
where (a :: Integer
a, g' :: g
g') = g -> (Integer, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
(b :: Integer
b, g'' :: g
g'') = g -> (Integer, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g'
b' :: Integer
b' = if 0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b then Integer
b else 1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b
randomR :: (Rational, Rational) -> g -> (Rational, g)
randomR (l :: Rational
l, h :: Rational
h) g :: g
g = (Rational
r Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
d Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
l, g
g'')
where (b :: Integer
b, g' :: g
g') = g -> (Integer, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
b' :: Integer
b' = if 0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b then Integer
b else 1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b
(a :: Integer
a, g'' :: g
g'') = (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (0, Integer
b') g
g'
r :: Rational
r = Integer
a Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
b'
d :: Rational
d = Rational
h Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
l
instance Random AlgReal where
random :: g -> (AlgReal, g)
random g :: g
g = let (a :: Rational
a, g' :: g
g') = g -> (Rational, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g in (Bool -> Rational -> AlgReal
AlgRational Bool
True Rational
a, g
g')
randomR :: (AlgReal, AlgReal) -> g -> (AlgReal, g)
randomR (AlgRational True l :: Rational
l, AlgRational True h :: Rational
h) g :: g
g = let (a :: Rational
a, g' :: g
g') = (Rational, Rational) -> g -> (Rational, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Rational
l, Rational
h) g
g in (Bool -> Rational -> AlgReal
AlgRational Bool
True Rational
a, g
g')
randomR lh :: (AlgReal, AlgReal)
lh _ = String -> (AlgReal, g)
forall a. HasCallStack => String -> a
error (String -> (AlgReal, g)) -> String -> (AlgReal, g)
forall a b. (a -> b) -> a -> b
$ "AlgReal.randomR: unsupported bounds: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (AlgReal, AlgReal) -> String
forall a. Show a => a -> String
show (AlgReal, AlgReal)
lh
algRealToSMTLib2 :: AlgReal -> String
algRealToSMTLib2 :: AlgReal -> String
algRealToSMTLib2 (AlgRational True r :: Rational
r)
| Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = "0.0"
| Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = "(- (/ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Integer -> Integer
forall a. Num a => a -> a
abs Integer
m) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".0 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".0))"
| Bool
True = "(/ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".0 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".0)"
where (m :: Integer
m, n :: Integer
n) = (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r, Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r)
algRealToSMTLib2 r :: AlgReal
r@(AlgRational False _)
= String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "SBV: Unexpected inexact rational to be converted to SMTLib2: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r
algRealToSMTLib2 (AlgPolyRoot (i :: Integer
i, AlgRealPoly xs :: [(Integer, Integer)]
xs) _) = "(root-obj (+ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (((Integer, Integer) -> [String])
-> [(Integer, Integer)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Integer, Integer) -> [String]
forall a a.
(Eq a, Num a, Num a, Ord a, Show a, Show a) =>
(a, a) -> [String]
term [(Integer, Integer)]
xs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
where term :: (a, a) -> [String]
term (0, _) = []
term (k :: a
k, 0) = [a -> String
forall a. (Ord a, Num a, Show a) => a -> String
coeff a
k]
term (1, 1) = ["x"]
term (1, p :: a
p) = ["(^ x " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"]
term (k :: a
k, 1) = ["(* " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. (Ord a, Num a, Show a) => a -> String
coeff a
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ " x)"]
term (k :: a
k, p :: a
p) = ["(* " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. (Ord a, Num a, Show a) => a -> String
coeff a
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (^ x " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"]
coeff :: a -> String
coeff n :: a
n | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = "(- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (a -> a
forall a. Num a => a -> a
abs a
n) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
| Bool
True = a -> String
forall a. Show a => a -> String
show a
n
algRealToHaskell :: AlgReal -> String
algRealToHaskell :: AlgReal -> String
algRealToHaskell (AlgRational True r :: Rational
r) = "((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") :: Rational)"
algRealToHaskell r :: AlgReal
r = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "SBV.algRealToHaskell: Unsupported argument: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r
showRat :: Bool -> Rational -> String
showRat :: Bool -> Rational -> String
showRat exact :: Bool
exact r :: Rational
r = String -> String
p (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ case Integer -> [Integer] -> Maybe (Int, String)
f25 (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r) [] of
Nothing -> Rational -> String
forall a. Show a => a -> String
show Rational
r
Just (noOfZeros :: Int
noOfZeros, num :: String
num) -> let present :: Int
present = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
num
in String -> String
neg (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ case Int
noOfZeros Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Int
present of
LT -> let (b :: String
b, a :: String
a) = Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
present Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
noOfZeros) String
num in String
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ "." String -> String -> String
forall a. [a] -> [a] -> [a]
++ if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
a then "0" else String
a
EQ -> "0." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
num
GT -> "0." String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
noOfZeros Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
present) '0' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
num
where p :: String -> String
p = if Bool
exact then String -> String
forall a. a -> a
id else (String -> String -> String
forall a. [a] -> [a] -> [a]
++ "...")
neg :: String -> String
neg = if Rational
r Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then ('-'Char -> String -> String
forall a. a -> [a] -> [a]
:) else String -> String
forall a. a -> a
id
f25 :: Integer -> [Integer] -> Maybe (Int, String)
f25 :: Integer -> [Integer] -> Maybe (Int, String)
f25 1 sofar :: [Integer]
sofar = let (ts :: [Integer]
ts, fs :: [Integer]
fs) = (Integer -> Bool) -> [Integer] -> ([Integer], [Integer])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 2) [Integer]
sofar
[lts :: Int
lts, lfs :: Int
lfs] = ([Integer] -> Int) -> [[Integer]] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map [Integer] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Integer]
ts, [Integer]
fs]
noOfZeros :: Int
noOfZeros = Int
lts Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` Int
lfs
in (Int, String) -> Maybe (Int, String)
forall a. a -> Maybe a
Just (Int
noOfZeros, Integer -> String
forall a. Show a => a -> String
show (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* [Integer] -> [Integer] -> Integer
forall p t t. Num p => [t] -> [t] -> p
factor [Integer]
ts [Integer]
fs))
f25 v :: Integer
v sofar :: [Integer]
sofar = let (q2 :: Integer
q2, r2 :: Integer
r2) = Integer
v Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`quotRem` 2
(q5 :: Integer
q5, r5 :: Integer
r5) = Integer
v Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`quotRem` 5
in case (Integer
r2, Integer
r5) of
(0, _) -> Integer -> [Integer] -> Maybe (Int, String)
f25 Integer
q2 (2 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
sofar)
(_, 0) -> Integer -> [Integer] -> Maybe (Int, String)
f25 Integer
q5 (5 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
sofar)
_ -> Maybe (Int, String)
forall a. Maybe a
Nothing
factor :: [t] -> [t] -> p
factor [] fs :: [t]
fs = [p] -> p
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [2 | t
_ <- [t]
fs]
factor ts :: [t]
ts [] = [p] -> p
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [5 | t
_ <- [t]
ts]
factor (_:ts :: [t]
ts) (_:fs :: [t]
fs) = [t] -> [t] -> p
factor [t]
ts [t]
fs
mergeAlgReals :: String -> AlgReal -> AlgReal -> AlgReal
mergeAlgReals :: String -> AlgReal -> AlgReal -> AlgReal
mergeAlgReals _ f :: AlgReal
f@(AlgRational exact :: Bool
exact r :: Rational
r) (AlgPolyRoot kp :: (Integer, AlgRealPoly)
kp Nothing)
| Bool
exact = AlgReal
f
| Bool
True = (Integer, AlgRealPoly) -> Maybe String -> AlgReal
AlgPolyRoot (Integer, AlgRealPoly)
kp (String -> Maybe String
forall a. a -> Maybe a
Just (Bool -> Rational -> String
showRat Bool
False Rational
r))
mergeAlgReals _ (AlgPolyRoot kp :: (Integer, AlgRealPoly)
kp Nothing) f :: AlgReal
f@(AlgRational exact :: Bool
exact r :: Rational
r)
| Bool
exact = AlgReal
f
| Bool
True = (Integer, AlgRealPoly) -> Maybe String -> AlgReal
AlgPolyRoot (Integer, AlgRealPoly)
kp (String -> Maybe String
forall a. a -> Maybe a
Just (Bool -> Rational -> String
showRat Bool
False Rational
r))
mergeAlgReals _ f :: AlgReal
f@(AlgRational e1 :: Bool
e1 r1 :: Rational
r1) s :: AlgReal
s@(AlgRational e2 :: Bool
e2 r2 :: Rational
r2)
| (Bool
e1, Rational
r1) (Bool, Rational) -> (Bool, Rational) -> Bool
forall a. Eq a => a -> a -> Bool
== (Bool
e2, Rational
r2) = AlgReal
f
| Bool
e1 = AlgReal
f
| Bool
e2 = AlgReal
s
mergeAlgReals m :: String
m _ _ = String -> AlgReal
forall a. HasCallStack => String -> a
error String
m
instance Arbitrary AlgReal where
arbitrary :: Gen AlgReal
arbitrary = Bool -> Rational -> AlgReal
AlgRational Bool
True (Rational -> AlgReal) -> Gen Rational -> Gen AlgReal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Gen Rational
forall a. Arbitrary a => Gen a
arbitrary