-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Core.AlgReals
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Algebraic reals in Haskell.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric      #-}
{-# LANGUAGE FlexibleInstances  #-}

{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

module Data.SBV.Core.AlgReals (
             AlgReal(..)
           , AlgRealPoly(..)
           , RationalCV(..)
           , RealPoint(..), realPoint
           , mkPolyReal
           , algRealToSMTLib2
           , algRealToHaskell
           , algRealToRational
           , mergeAlgReals
           , isExactRational
           , algRealStructuralEqual
           , algRealStructuralCompare
           )
   where

import Control.DeepSeq (NFData)
import Data.Char       (isDigit)

import Data.List       (sortBy, isPrefixOf, partition)
import Data.Ratio      ((%), numerator, denominator)
import Data.Function   (on)
import System.Random
import Test.QuickCheck (Arbitrary(..))

import Numeric (readSigned, readFloat)

import Text.Read(readMaybe)

import qualified Data.Generics as G
import GHC.Generics

-- | Is the endpoint included in the interval?
data RealPoint a = OpenPoint   a -- ^ open: i.e., doesn't include the point
                 | ClosedPoint a -- ^ closed: i.e., includes the point
                 deriving (Int -> RealPoint a -> ShowS
[RealPoint a] -> ShowS
RealPoint a -> String
(Int -> RealPoint a -> ShowS)
-> (RealPoint a -> String)
-> ([RealPoint a] -> ShowS)
-> Show (RealPoint a)
forall a. Show a => Int -> RealPoint a -> ShowS
forall a. Show a => [RealPoint a] -> ShowS
forall a. Show a => RealPoint a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> RealPoint a -> ShowS
showsPrec :: Int -> RealPoint a -> ShowS
$cshow :: forall a. Show a => RealPoint a -> String
show :: RealPoint a -> String
$cshowList :: forall a. Show a => [RealPoint a] -> ShowS
showList :: [RealPoint a] -> ShowS
Show, RealPoint a -> RealPoint a -> Bool
(RealPoint a -> RealPoint a -> Bool)
-> (RealPoint a -> RealPoint a -> Bool) -> Eq (RealPoint a)
forall a. Eq a => RealPoint a -> RealPoint a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => RealPoint a -> RealPoint a -> Bool
== :: RealPoint a -> RealPoint a -> Bool
$c/= :: forall a. Eq a => RealPoint a -> RealPoint a -> Bool
/= :: RealPoint a -> RealPoint a -> Bool
Eq, Eq (RealPoint a)
Eq (RealPoint a) =>
(RealPoint a -> RealPoint a -> Ordering)
-> (RealPoint a -> RealPoint a -> Bool)
-> (RealPoint a -> RealPoint a -> Bool)
-> (RealPoint a -> RealPoint a -> Bool)
-> (RealPoint a -> RealPoint a -> Bool)
-> (RealPoint a -> RealPoint a -> RealPoint a)
-> (RealPoint a -> RealPoint a -> RealPoint a)
-> Ord (RealPoint a)
RealPoint a -> RealPoint a -> Bool
RealPoint a -> RealPoint a -> Ordering
RealPoint a -> RealPoint a -> RealPoint a
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
forall a. Ord a => Eq (RealPoint a)
forall a. Ord a => RealPoint a -> RealPoint a -> Bool
forall a. Ord a => RealPoint a -> RealPoint a -> Ordering
forall a. Ord a => RealPoint a -> RealPoint a -> RealPoint a
$ccompare :: forall a. Ord a => RealPoint a -> RealPoint a -> Ordering
compare :: RealPoint a -> RealPoint a -> Ordering
$c< :: forall a. Ord a => RealPoint a -> RealPoint a -> Bool
< :: RealPoint a -> RealPoint a -> Bool
$c<= :: forall a. Ord a => RealPoint a -> RealPoint a -> Bool
<= :: RealPoint a -> RealPoint a -> Bool
$c> :: forall a. Ord a => RealPoint a -> RealPoint a -> Bool
> :: RealPoint a -> RealPoint a -> Bool
$c>= :: forall a. Ord a => RealPoint a -> RealPoint a -> Bool
>= :: RealPoint a -> RealPoint a -> Bool
$cmax :: forall a. Ord a => RealPoint a -> RealPoint a -> RealPoint a
max :: RealPoint a -> RealPoint a -> RealPoint a
$cmin :: forall a. Ord a => RealPoint a -> RealPoint a -> RealPoint a
min :: RealPoint a -> RealPoint a -> RealPoint a
Ord, Typeable (RealPoint a)
Typeable (RealPoint a) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> RealPoint a -> c (RealPoint a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (RealPoint a))
-> (RealPoint a -> Constr)
-> (RealPoint a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (RealPoint a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (RealPoint a)))
-> ((forall b. Data b => b -> b) -> RealPoint a -> RealPoint a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RealPoint a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RealPoint a -> r)
-> (forall u. (forall d. Data d => d -> u) -> RealPoint a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> RealPoint a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a))
-> Data (RealPoint a)
RealPoint a -> Constr
RealPoint a -> DataType
(forall b. Data b => b -> b) -> RealPoint a -> RealPoint a
forall a. Data a => Typeable (RealPoint a)
forall a. Data a => RealPoint a -> Constr
forall a. Data a => RealPoint a -> DataType
forall a.
Data a =>
(forall b. Data b => b -> b) -> RealPoint a -> RealPoint a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> RealPoint a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> RealPoint a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RealPoint a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RealPoint a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (RealPoint a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RealPoint a -> c (RealPoint a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (RealPoint a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (RealPoint a))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> RealPoint a -> u
forall u. (forall d. Data d => d -> u) -> RealPoint a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RealPoint a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RealPoint a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (RealPoint a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RealPoint a -> c (RealPoint a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (RealPoint a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (RealPoint a))
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RealPoint a -> c (RealPoint a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RealPoint a -> c (RealPoint a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (RealPoint a)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (RealPoint a)
$ctoConstr :: forall a. Data a => RealPoint a -> Constr
toConstr :: RealPoint a -> Constr
$cdataTypeOf :: forall a. Data a => RealPoint a -> DataType
dataTypeOf :: RealPoint a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (RealPoint a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (RealPoint a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (RealPoint a))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (RealPoint a))
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> RealPoint a -> RealPoint a
gmapT :: (forall b. Data b => b -> b) -> RealPoint a -> RealPoint a
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RealPoint a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RealPoint a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RealPoint a -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RealPoint a -> r
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> RealPoint a -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> RealPoint a -> [u]
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> RealPoint a -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RealPoint a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RealPoint a -> m (RealPoint a)
G.Data, RealPoint a -> ()
(RealPoint a -> ()) -> NFData (RealPoint a)
forall a. NFData a => RealPoint a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall a. NFData a => RealPoint a -> ()
rnf :: RealPoint a -> ()
NFData, (forall x. RealPoint a -> Rep (RealPoint a) x)
-> (forall x. Rep (RealPoint a) x -> RealPoint a)
-> Generic (RealPoint a)
forall x. Rep (RealPoint a) x -> RealPoint a
forall x. RealPoint a -> Rep (RealPoint a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (RealPoint a) x -> RealPoint a
forall a x. RealPoint a -> Rep (RealPoint a) x
$cfrom :: forall a x. RealPoint a -> Rep (RealPoint a) x
from :: forall x. RealPoint a -> Rep (RealPoint a) x
$cto :: forall a x. Rep (RealPoint a) x -> RealPoint a
to :: forall x. Rep (RealPoint a) x -> RealPoint a
Generic)

-- | Extract the point associated with the open-closed point
realPoint :: RealPoint a -> a
realPoint :: forall a. RealPoint a -> a
realPoint (OpenPoint   a
a) = a
a
realPoint (ClosedPoint a
a) = a
a

-- | Algebraic reals. Note that the representation is left abstract. We represent
-- rational results explicitly, while the roots-of-polynomials are represented
-- implicitly by their defining equation
data AlgReal = AlgRational Bool Rational                             -- ^ bool says it's exact (i.e., SMT-solver did not return it with ? at the end.)
             | AlgPolyRoot (Integer,  AlgRealPoly) (Maybe String)    -- ^ which root of this polynomial and an approximate decimal representation with given precision, if available
             | AlgInterval (RealPoint Rational) (RealPoint Rational) -- ^ interval, with low and high bounds
             deriving (Typeable AlgReal
Typeable AlgReal =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> AlgReal -> c AlgReal)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c AlgReal)
-> (AlgReal -> Constr)
-> (AlgReal -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c AlgReal))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AlgReal))
-> ((forall b. Data b => b -> b) -> AlgReal -> AlgReal)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> AlgReal -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> AlgReal -> r)
-> (forall u. (forall d. Data d => d -> u) -> AlgReal -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> AlgReal -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> AlgReal -> m AlgReal)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AlgReal -> m AlgReal)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AlgReal -> m AlgReal)
-> Data AlgReal
AlgReal -> Constr
AlgReal -> DataType
(forall b. Data b => b -> b) -> AlgReal -> AlgReal
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> AlgReal -> u
forall u. (forall d. Data d => d -> u) -> AlgReal -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AlgReal -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AlgReal -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AlgReal -> m AlgReal
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AlgReal -> m AlgReal
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AlgReal
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AlgReal -> c AlgReal
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AlgReal)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AlgReal)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AlgReal -> c AlgReal
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AlgReal -> c AlgReal
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AlgReal
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AlgReal
$ctoConstr :: AlgReal -> Constr
toConstr :: AlgReal -> Constr
$cdataTypeOf :: AlgReal -> DataType
dataTypeOf :: AlgReal -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AlgReal)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AlgReal)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AlgReal)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AlgReal)
$cgmapT :: (forall b. Data b => b -> b) -> AlgReal -> AlgReal
gmapT :: (forall b. Data b => b -> b) -> AlgReal -> AlgReal
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AlgReal -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AlgReal -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AlgReal -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AlgReal -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> AlgReal -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> AlgReal -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> AlgReal -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> AlgReal -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AlgReal -> m AlgReal
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AlgReal -> m AlgReal
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AlgReal -> m AlgReal
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AlgReal -> m AlgReal
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AlgReal -> m AlgReal
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AlgReal -> m AlgReal
G.Data, (forall x. AlgReal -> Rep AlgReal x)
-> (forall x. Rep AlgReal x -> AlgReal) -> Generic AlgReal
forall x. Rep AlgReal x -> AlgReal
forall x. AlgReal -> Rep AlgReal x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AlgReal -> Rep AlgReal x
from :: forall x. AlgReal -> Rep AlgReal x
$cto :: forall x. Rep AlgReal x -> AlgReal
to :: forall x. Rep AlgReal x -> AlgReal
Generic, AlgReal -> ()
(AlgReal -> ()) -> NFData AlgReal
forall a. (a -> ()) -> NFData a
$crnf :: AlgReal -> ()
rnf :: AlgReal -> ()
NFData)

-- | Check whether a given argument is an exact rational
isExactRational :: AlgReal -> Bool
isExactRational :: AlgReal -> Bool
isExactRational (AlgRational Bool
True Rational
_) = Bool
True
isExactRational AlgReal
_                    = Bool
False

-- | A univariate polynomial, represented simply as a
-- coefficient list. For instance, "5x^3 + 2x - 5" is
-- represented as [(5, 3), (2, 1), (-5, 0)]
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
$c== :: AlgRealPoly -> AlgRealPoly -> Bool
== :: AlgRealPoly -> AlgRealPoly -> Bool
$c/= :: AlgRealPoly -> AlgRealPoly -> Bool
/= :: 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
$ccompare :: AlgRealPoly -> AlgRealPoly -> Ordering
compare :: AlgRealPoly -> AlgRealPoly -> Ordering
$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
>= :: AlgRealPoly -> AlgRealPoly -> Bool
$cmax :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly
max :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly
$cmin :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly
min :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly
Ord, Typeable AlgRealPoly
Typeable AlgRealPoly =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> AlgRealPoly -> c AlgRealPoly)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c AlgRealPoly)
-> (AlgRealPoly -> Constr)
-> (AlgRealPoly -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c AlgRealPoly))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c AlgRealPoly))
-> ((forall b. Data b => b -> b) -> AlgRealPoly -> AlgRealPoly)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> AlgRealPoly -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> AlgRealPoly -> r)
-> (forall u. (forall d. Data d => d -> u) -> AlgRealPoly -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> AlgRealPoly -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> AlgRealPoly -> m AlgRealPoly)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AlgRealPoly -> m AlgRealPoly)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AlgRealPoly -> m AlgRealPoly)
-> Data AlgRealPoly
AlgRealPoly -> Constr
AlgRealPoly -> DataType
(forall b. Data b => b -> b) -> AlgRealPoly -> AlgRealPoly
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> AlgRealPoly -> u
forall u. (forall d. Data d => d -> u) -> AlgRealPoly -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AlgRealPoly -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AlgRealPoly -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AlgRealPoly -> m AlgRealPoly
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AlgRealPoly -> m AlgRealPoly
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AlgRealPoly
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AlgRealPoly -> c AlgRealPoly
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AlgRealPoly)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AlgRealPoly)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AlgRealPoly -> c AlgRealPoly
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AlgRealPoly -> c AlgRealPoly
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AlgRealPoly
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AlgRealPoly
$ctoConstr :: AlgRealPoly -> Constr
toConstr :: AlgRealPoly -> Constr
$cdataTypeOf :: AlgRealPoly -> DataType
dataTypeOf :: AlgRealPoly -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AlgRealPoly)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AlgRealPoly)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AlgRealPoly)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AlgRealPoly)
$cgmapT :: (forall b. Data b => b -> b) -> AlgRealPoly -> AlgRealPoly
gmapT :: (forall b. Data b => b -> b) -> AlgRealPoly -> AlgRealPoly
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AlgRealPoly -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AlgRealPoly -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AlgRealPoly -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AlgRealPoly -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> AlgRealPoly -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> AlgRealPoly -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> AlgRealPoly -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> AlgRealPoly -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AlgRealPoly -> m AlgRealPoly
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AlgRealPoly -> m AlgRealPoly
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AlgRealPoly -> m AlgRealPoly
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AlgRealPoly -> m AlgRealPoly
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AlgRealPoly -> m AlgRealPoly
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AlgRealPoly -> m AlgRealPoly
G.Data, AlgRealPoly -> ()
(AlgRealPoly -> ()) -> NFData AlgRealPoly
forall a. (a -> ()) -> NFData a
$crnf :: AlgRealPoly -> ()
rnf :: AlgRealPoly -> ()
NFData, (forall x. AlgRealPoly -> Rep AlgRealPoly x)
-> (forall x. Rep AlgRealPoly x -> AlgRealPoly)
-> Generic AlgRealPoly
forall x. Rep AlgRealPoly x -> AlgRealPoly
forall x. AlgRealPoly -> Rep AlgRealPoly x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AlgRealPoly -> Rep AlgRealPoly x
from :: forall x. AlgRealPoly -> Rep AlgRealPoly x
$cto :: forall x. Rep AlgRealPoly x -> AlgRealPoly
to :: forall x. Rep AlgRealPoly x -> AlgRealPoly
Generic)

-- | Construct a poly-root real with a given approximate value (either as a decimal, or polynomial-root)
mkPolyReal :: Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
mkPolyReal :: Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
mkPolyReal (Left (Bool
exact, 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
== Char
'.') String
str) of
      (String
"", (String, String)
_)                                -> Bool -> Rational -> AlgReal
AlgRational Bool
exact Rational
0
      (String
_, (String
x, Char
'.':String
y)) | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit (String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
y) -> Bool -> Rational -> AlgReal
AlgRational Bool
exact (String -> Integer
forall a. Read a => String -> a
read (String
xString -> ShowS
forall a. [a] -> [a] -> [a]
++String
y) Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% (Integer
10 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
y))
      (String
_, (String
x, String
""))    | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit 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
% Integer
1)
      (String, (String, String))
_                                      ->
        -- CVC5 prints in division-rational form:
        case String -> Maybe Rational
forall a. Read a => String -> Maybe a
readMaybe ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
',') ((Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map (\Char
c -> if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'/' then Char
'%' else Char
c) String
str)) :: Maybe Rational of
          Just Rational
r  -> Bool -> Rational -> AlgReal
AlgRational Bool
exact Rational
r
          Maybe Rational
Nothing -> String -> AlgReal
forall a. HasCallStack => String -> a
error (String -> AlgReal) -> String -> AlgReal
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"*** Data.SBV.mkPolyReal: Unable to read a number from:"
                                     , String
"***"
                                     , String
"*** " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str
                                     , String
"***"
                                     , String
"*** Please report this as a bug."
                                     ]
mkPolyReal (Right (Integer
k, [(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 [(a, b)
x]                    = [(a, b)
x]
       merge ((a
a, b
b):r :: [(a, b)]
r@((a
c, b
d):[(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 [(Integer, Integer)]
xs) = ShowS
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@(Integer
_, Integer
x) <- [(Integer, Integer)]
xs, Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0])) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
c
     where c :: Integer
c  = case [Integer
k | (Integer
k, Integer
0) <- [(Integer, Integer)]
xs] of
                  Integer
h:[Integer]
_ -> -Integer
h
                  [Integer]
_   -> Integer
0

           term :: (a, a) -> [String]
term ( a
0, a
_) = []
           term ( a
1, a
1) = [ String
"x"]
           term ( a
1, a
p) = [ String
"x^" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p]
           term (-1, a
1) = [String
"-x"]
           term (-1, a
p) = [String
"-x^" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p]
           term (a
k,  a
1) = [a -> String
forall a. Show a => a -> String
show a
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"x"]
           term (a
k,  a
p) = [a -> String
forall a. Show a => a -> String
show a
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"x^" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p]
           join :: [String] -> String
join []      = String
""
           join (String
k:[String]
ks) = String
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
join [String]
ks
             where s :: String
s = case [String]
ks of
                        []    -> String
""
                        (String
y:[String]
_) | String
"-" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
y -> String
""
                              | String
"+" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
y -> String
""
                              | Bool
True               -> String
"+"
           chkEmpty :: ShowS
chkEmpty String
s = if String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s then String
"0" else String
s

instance Show AlgReal where
  show :: AlgReal -> String
show (AlgRational Bool
exact Rational
a)         = Bool -> Rational -> String
showRat Bool
exact Rational
a
  show (AlgPolyRoot (Integer
i, AlgRealPoly
p) Maybe String
mbApprox) = String
"root(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ AlgRealPoly -> String
forall a. Show a => a -> String
show AlgRealPoly
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> ShowS -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" ShowS
app Maybe String
mbApprox
     where app :: ShowS
app String
v | String -> Char
forall a. HasCallStack => [a] -> a
last String
v Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'?' = String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. HasCallStack => [a] -> [a]
init String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"..."
                 | Bool
True          = String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
v
  show (AlgInterval RealPoint Rational
a RealPoint Rational
b)         = case (RealPoint Rational
a, RealPoint Rational
b) of
                                     (OpenPoint   Rational
l, OpenPoint   Rational
h) -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
h String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
                                     (OpenPoint   Rational
l, ClosedPoint Rational
h) -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
h String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
                                     (ClosedPoint Rational
l, OpenPoint   Rational
h) -> String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
h String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
                                     (ClosedPoint Rational
l, ClosedPoint Rational
h) -> String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
h String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"

-- lift unary op through an exact rational, otherwise bail
lift1 :: String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 :: String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 String
_  Rational -> Rational
o (AlgRational Bool
e Rational
a) = Bool -> Rational -> AlgReal
AlgRational Bool
e (Rational -> Rational
o Rational
a)
lift1 String
nm Rational -> Rational
_ AlgReal
a                 = String -> AlgReal
forall a. HasCallStack => String -> a
error (String -> AlgReal) -> String -> AlgReal
forall a b. (a -> b) -> a -> b
$ String
"AlgReal." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": unsupported argument: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
forall a. Show a => a -> String
show AlgReal
a

-- lift binary op through exact rationals, otherwise bail
lift2 :: String -> (Rational -> Rational -> Rational) -> AlgReal -> AlgReal -> AlgReal
lift2 :: String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 String
_  Rational -> Rational -> Rational
o (AlgRational Bool
True Rational
a) (AlgRational Bool
True Rational
b) = Bool -> Rational -> AlgReal
AlgRational Bool
True (Rational
a Rational -> Rational -> Rational
`o` Rational
b)
lift2 String
nm Rational -> Rational -> Rational
_ AlgReal
a                    AlgReal
b                    = String -> AlgReal
forall a. HasCallStack => String -> a
error (String -> AlgReal) -> String -> AlgReal
forall a b. (a -> b) -> a -> b
$ String
"AlgReal." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": unsupported arguments: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (AlgReal, AlgReal) -> String
forall a. Show a => a -> String
show (AlgReal
a, AlgReal
b)

-- The idea in the instances below is that we will fully support operations
-- on "AlgRational" AlgReals, but leave everything else undefined. When we are
-- on the Haskell side, the AlgReal's are *not* reachable. They only represent
-- return values from SMT solvers, which we should *not* need to manipulate.
instance Eq AlgReal where
  AlgRational Bool
True Rational
a == :: AlgReal -> AlgReal -> Bool
== AlgRational Bool
True Rational
b = Rational
a Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
b
  AlgReal
a                  == AlgReal
b                  = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"AlgReal.==: unsupported arguments: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (AlgReal, AlgReal) -> String
forall a. Show a => a -> String
show (AlgReal
a, AlgReal
b)

instance Ord AlgReal where
  AlgRational Bool
True Rational
a compare :: AlgReal -> AlgReal -> Ordering
`compare` AlgRational Bool
True Rational
b = Rational
a Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Rational
b
  AlgReal
a                  `compare` AlgReal
b                  = String -> Ordering
forall a. HasCallStack => String -> a
error (String -> Ordering) -> String -> Ordering
forall a b. (a -> b) -> a -> b
$ String
"AlgReal.compare: unsupported arguments: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (AlgReal, AlgReal) -> String
forall a. Show a => a -> String
show (AlgReal
a, AlgReal
b)

-- | Structural equality for AlgReal; used when constants are Map keys
algRealStructuralEqual   :: AlgReal -> AlgReal -> Bool
AlgRational Bool
a Rational
b algRealStructuralEqual :: AlgReal -> AlgReal -> Bool
`algRealStructuralEqual` AlgRational Bool
c Rational
d = (Bool
a, Rational
b) (Bool, Rational) -> (Bool, Rational) -> Bool
forall a. Eq a => a -> a -> Bool
== (Bool
c, Rational
d)
AlgPolyRoot (Integer, AlgRealPoly)
a Maybe String
b `algRealStructuralEqual` AlgPolyRoot (Integer, AlgRealPoly)
c 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)
AlgReal
_               `algRealStructuralEqual` AlgReal
_               = Bool
False

-- | Structural comparisons for AlgReal; used when constants are Map keys
algRealStructuralCompare :: AlgReal -> AlgReal -> Ordering
AlgRational Bool
a Rational
b algRealStructuralCompare :: AlgReal -> AlgReal -> Ordering
`algRealStructuralCompare` AlgRational Bool
c Rational
d = (Bool
a, Rational
b) (Bool, Rational) -> (Bool, Rational) -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` (Bool
c, Rational
d)
AlgRational Bool
_ Rational
_ `algRealStructuralCompare` AlgPolyRoot (Integer, AlgRealPoly)
_ Maybe String
_ = Ordering
LT
AlgRational Bool
_ Rational
_ `algRealStructuralCompare` AlgInterval RealPoint Rational
_ RealPoint Rational
_ = Ordering
LT
AlgPolyRoot (Integer, AlgRealPoly)
_ Maybe String
_ `algRealStructuralCompare` AlgRational Bool
_ Rational
_ = Ordering
GT
AlgPolyRoot (Integer, AlgRealPoly)
a Maybe String
b `algRealStructuralCompare` AlgPolyRoot (Integer, AlgRealPoly)
c 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)
AlgPolyRoot (Integer, AlgRealPoly)
_ Maybe String
_ `algRealStructuralCompare` AlgInterval RealPoint Rational
_ RealPoint Rational
_ = Ordering
LT
AlgInterval RealPoint Rational
_ RealPoint Rational
_ `algRealStructuralCompare` AlgRational Bool
_ Rational
_ = Ordering
GT
AlgInterval RealPoint Rational
_ RealPoint Rational
_ `algRealStructuralCompare` AlgPolyRoot (Integer, AlgRealPoly)
_ Maybe String
_ = Ordering
GT
AlgInterval RealPoint Rational
a RealPoint Rational
b `algRealStructuralCompare` AlgInterval RealPoint Rational
c RealPoint Rational
d = (RealPoint Rational
a, RealPoint Rational
b) (RealPoint Rational, RealPoint Rational)
-> (RealPoint Rational, RealPoint Rational) -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` (RealPoint Rational
c, RealPoint Rational
d)

instance Num AlgReal where
  + :: AlgReal -> AlgReal -> AlgReal
(+)         = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 String
"+"      Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(+)
  * :: AlgReal -> AlgReal -> AlgReal
(*)         = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 String
"*"      Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(*)
  (-)         = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 String
"-"      (-)
  negate :: AlgReal -> AlgReal
negate      = String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 String
"negate" Rational -> Rational
forall a. Num a => a -> a
negate
  abs :: AlgReal -> AlgReal
abs         = String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 String
"abs"    Rational -> Rational
forall a. Num a => a -> a
abs
  signum :: AlgReal -> AlgReal
signum      = String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 String
"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

-- |  NB: Following the other types we have, we require `a/0` to be `0` for all a.
instance Fractional AlgReal where
  (AlgRational Bool
True Rational
_) / :: AlgReal -> AlgReal -> AlgReal
/ (AlgRational Bool
True Rational
b) | Rational
b Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
0 = AlgReal
0
  AlgReal
a                    / AlgReal
b                             = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 String
"/" 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 Bool
True Rational
v) = Rational
v
  toRational AlgReal
x                    = String -> Rational
forall a. HasCallStack => String -> a
error (String -> Rational) -> String -> Rational
forall a b. (a -> b) -> a -> b
$ String
"AlgReal.toRational: Argument cannot be represented as a rational value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
algRealToHaskell AlgReal
x

instance Random Rational where
  random :: forall g. RandomGen g => g -> (Rational, g)
random g
g = (Integer
a Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
b', g
g'')
     where (Integer
a, g
g')  = g -> (Integer, g)
forall g. RandomGen g => g -> (Integer, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
           (Integer
b, g
g'') = g -> (Integer, g)
forall g. RandomGen g => g -> (Integer, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g'
           b' :: Integer
b'       = if Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b then Integer
b else Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b -- ensures 0 < b

  randomR :: forall g. RandomGen g => (Rational, Rational) -> g -> (Rational, g)
randomR (Rational
l, Rational
h) 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 (Integer
b, g
g')  = g -> (Integer, g)
forall g. RandomGen g => g -> (Integer, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
           b' :: Integer
b'       = if Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b then Integer
b else Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b -- ensures 0 < b
           (Integer
a, g
g'') = (Integer, Integer) -> g -> (Integer, g)
forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
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 :: forall g. RandomGen g => g -> (AlgReal, g)
random g
g = let (Rational
a, g
g') = g -> (Rational, g)
forall g. RandomGen 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 :: forall g. RandomGen g => (AlgReal, AlgReal) -> g -> (AlgReal, g)
randomR (AlgRational Bool
True Rational
l, AlgRational Bool
True Rational
h) g
g = let (Rational
a, g
g') = (Rational, Rational) -> g -> (Rational, g)
forall g. RandomGen 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 (AlgReal, AlgReal)
lh                                       g
_ = String -> (AlgReal, g)
forall a. HasCallStack => String -> a
error (String -> (AlgReal, g)) -> String -> (AlgReal, g)
forall a b. (a -> b) -> a -> b
$ String
"AlgReal.randomR: unsupported bounds: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (AlgReal, AlgReal) -> String
forall a. Show a => a -> String
show (AlgReal, AlgReal)
lh

-- | Render an 'AlgReal' as an SMTLib2 value. Only supports rationals for the time being.
algRealToSMTLib2 :: AlgReal -> String
algRealToSMTLib2 :: AlgReal -> String
algRealToSMTLib2 (AlgRational Bool
True Rational
r)
   | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = String
"0.0"
   | Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0  = String
"(- (/ "  String -> ShowS
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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".0 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".0))"
   | Bool
True   =    String
"(/ "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
m       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".0 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".0)"
  where (Integer
m, 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 Bool
False Rational
_)
   = ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"SBV: Unexpected inexact rational to be converted to SMTLib2: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r
algRealToSMTLib2 (AlgPolyRoot (Integer
i, AlgRealPoly [(Integer, Integer)]
xs) Maybe String
_) = String
"(root-obj (+ " String -> ShowS
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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  where term :: (a, a) -> [String]
term (a
0, a
_) = []
        term (a
k, a
0) = [a -> String
forall {a}. (Ord a, Num a, Show a) => a -> String
coeff a
k]
        term (a
1, a
1) = [String
"x"]
        term (a
1, a
p) = [String
"(^ x " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"]
        term (a
k, a
1) = [String
"(* " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall {a}. (Ord a, Num a, Show a) => a -> String
coeff a
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" x)"]
        term (a
k, a
p) = [String
"(* " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall {a}. (Ord a, Num a, Show a) => a -> String
coeff a
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (^ x " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"))"]
        coeff :: a -> String
coeff a
n | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 = String
"(- " String -> ShowS
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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
                | Bool
True  = a -> String
forall a. Show a => a -> String
show a
n
algRealToSMTLib2 r :: AlgReal
r@AlgInterval{}
   = ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"SBV: Unexpected inexact rational to be converted to SMTLib2: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r

-- | Render an 'AlgReal' as a Haskell value. Only supports rationals, since there is no corresponding
-- standard Haskell type that can represent root-of-polynomial variety.
algRealToHaskell :: AlgReal -> String
algRealToHaskell :: AlgReal -> String
algRealToHaskell (AlgRational Bool
True Rational
r) = String
"((" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") :: Rational)"
algRealToHaskell AlgReal
r                    = ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                        , String
"SBV.algRealToHaskell: Unsupported argument:"
                                                        , String
""
                                                        , String
"   " String -> ShowS
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r
                                                        , String
""
                                                        , String
"represents an irrational number, and cannot be converted to a Haskell value."
                                                        ]

-- | Conversion from internal rationals to Haskell values
data RationalCV = RatIrreducible AlgReal                                   -- ^ Root of a polynomial, cannot be reduced
                | RatExact       Rational                                  -- ^ An exact rational
                | RatApprox      Rational                                  -- ^ An approximated value
                | RatInterval    (RealPoint Rational) (RealPoint Rational) -- ^ Interval. Can be open/closed on both ends.
                deriving Int -> RationalCV -> ShowS
[RationalCV] -> ShowS
RationalCV -> String
(Int -> RationalCV -> ShowS)
-> (RationalCV -> String)
-> ([RationalCV] -> ShowS)
-> Show RationalCV
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RationalCV -> ShowS
showsPrec :: Int -> RationalCV -> ShowS
$cshow :: RationalCV -> String
show :: RationalCV -> String
$cshowList :: [RationalCV] -> ShowS
showList :: [RationalCV] -> ShowS
Show

-- | Convert an 'AlgReal' to a 'Rational'. If the 'AlgReal' is exact, then you get a 'Left' value. Otherwise,
-- you get a 'Right' value which is simply an approximation.
algRealToRational :: AlgReal -> RationalCV
algRealToRational :: AlgReal -> RationalCV
algRealToRational AlgReal
a = case AlgReal
a of
                        AlgRational Bool
True  Rational
r        -> Rational -> RationalCV
RatExact Rational
r
                        AlgRational Bool
False Rational
r        -> Rational -> RationalCV
RatExact Rational
r
                        AlgPolyRoot (Integer, AlgRealPoly)
_     Maybe String
Nothing  -> AlgReal -> RationalCV
RatIrreducible AlgReal
a
                        AlgPolyRoot (Integer, AlgRealPoly)
_     (Just String
s) -> let trimmed :: String
trimmed = case ShowS
forall a. [a] -> [a]
reverse String
s of
                                                                     Char
'.':Char
'.':Char
'.':String
rest -> ShowS
forall a. [a] -> [a]
reverse String
rest
                                                                     String
_                -> String
s
                                                      in case ReadS Rational -> ReadS Rational
forall a. Real a => ReadS a -> ReadS a
readSigned ReadS Rational
forall a. RealFrac a => ReadS a
readFloat String
trimmed of
                                                           [(Rational
v, String
"")] -> Rational -> RationalCV
RatApprox Rational
v
                                                           [(Rational, String)]
_         -> String -> RationalCV
forall {b}. String -> b
bad String
"represents a value that cannot be converted to a rational"
                        AlgInterval RealPoint Rational
lo RealPoint Rational
hi          -> RealPoint Rational -> RealPoint Rational -> RationalCV
RatInterval RealPoint Rational
lo RealPoint Rational
hi
   where bad :: String -> b
bad String
w = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                 , String
"SBV.algRealToRational: Unsupported argument:"
                                 , String
""
                                 , String
"   " String -> ShowS
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
forall a. Show a => a -> String
show AlgReal
a
                                 , String
""
                                 , String
w
                                 ]

-- Try to show a rational precisely if we can, with finite number of
-- digits. Otherwise, show it as a rational value.
showRat :: Bool -> Rational -> String
showRat :: Bool -> Rational -> String
showRat Bool
exact Rational
r = ShowS
p ShowS -> ShowS
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
                       Maybe (Int, String)
Nothing               -> Rational -> String
forall a. Show a => a -> String
show Rational
r   -- bail out, not precisely representable with finite digits
                       Just (Int
noOfZeros, String
num) -> let present :: Int
present = String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
num
                                                in ShowS
neg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ case Int
noOfZeros Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Int
present of
                                                           Ordering
LT -> let (String
b, 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++ if String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
a then String
"0" else String
a
                                                           Ordering
EQ -> String
"0." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
num
                                                           Ordering
GT -> String
"0." String -> ShowS
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) Char
'0' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
num
  where p :: ShowS
p   = if Bool
exact then ShowS
forall a. a -> a
id else (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"...")
        neg :: ShowS
neg = if Rational
r Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
0 then (Char
'-'Char -> ShowS
forall a. a -> [a] -> [a]
:) else ShowS
forall a. a -> a
id
        -- factor a number in 2's and 5's if possible
        -- If so, it'll return the number of digits after the zero
        -- to reach the next power of 10, and the numerator value scaled
        -- appropriately and shown as a string
        f25 :: Integer -> [Integer] -> Maybe (Int, String)
        f25 :: Integer -> [Integer] -> Maybe (Int, String)
f25 Integer
1 [Integer]
sofar = let ([Integer]
ts, [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
== Integer
2) [Integer]
sofar
                          lts :: Int
lts        = [Integer] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Integer]
ts
                          lfs :: Int
lfs        = [Integer] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [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 {t} {t} {t}. Num t => [t] -> [t] -> t
factor [Integer]
ts [Integer]
fs))
        f25 Integer
v [Integer]
sofar = let (Integer
q2, Integer
r2) = Integer
v Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`quotRem` Integer
2
                          (Integer
q5, Integer
r5) = Integer
v Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`quotRem` Integer
5
                      in case (Integer
r2, Integer
r5) of
                           (Integer
0, Integer
_) -> Integer -> [Integer] -> Maybe (Int, String)
f25 Integer
q2 (Integer
2 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
sofar)
                           (Integer
_, Integer
0) -> Integer -> [Integer] -> Maybe (Int, String)
f25 Integer
q5 (Integer
5 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
sofar)
                           (Integer, Integer)
_      -> Maybe (Int, String)
forall a. Maybe a
Nothing
        -- compute the next power of 10 we need to get to
        factor :: [t] -> [t] -> t
factor []     [t]
fs     = [t] -> t
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [t
2 | t
_ <- [t]
fs]
        factor [t]
ts     []     = [t] -> t
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [t
5 | t
_ <- [t]
ts]
        factor (t
_:[t]
ts) (t
_:[t]
fs) = [t] -> [t] -> t
factor [t]
ts [t]
fs

-- | Merge the representation of two algebraic reals, one assumed to be
-- in polynomial form, the other in decimal. Arguments can be the same
-- kind, so long as they are both rationals and equivalent; if not there
-- must be one that is precise. It's an error to pass anything
-- else to this function! (Used in reconstructing SMT counter-example values with reals).
mergeAlgReals :: String -> AlgReal -> AlgReal -> AlgReal
mergeAlgReals :: String -> AlgReal -> AlgReal -> AlgReal
mergeAlgReals String
_ f :: AlgReal
f@(AlgRational Bool
exact Rational
r) (AlgPolyRoot (Integer, AlgRealPoly)
kp Maybe String
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 String
_ (AlgPolyRoot (Integer, AlgRealPoly)
kp Maybe String
Nothing) f :: AlgReal
f@(AlgRational Bool
exact 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 String
_ f :: AlgReal
f@(AlgRational Bool
e1 Rational
r1) s :: AlgReal
s@(AlgRational Bool
e2 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 String
m AlgReal
_ AlgReal
_ = String -> AlgReal
forall a. HasCallStack => String -> a
error String
m

-- Quickcheck instance
instance Arbitrary AlgReal where
  arbitrary :: Gen AlgReal
arbitrary = Bool -> Rational -> AlgReal
AlgRational Bool
True (Rational -> AlgReal) -> Gen Rational -> Gen AlgReal
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Gen Rational
forall a. Arbitrary a => Gen a
arbitrary