{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.AlgReal
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.AlgReal
  ( AlgRealPoly (..),
    UnsupportedAlgRealOperation (..),
    toSBVAlgReal,
    fromSBVAlgReal,
    RealPoint (..),
    AlgReal (..),
  )
where

import Control.DeepSeq (NFData)
import Control.Exception (Exception, throw)
import qualified Data.Binary as Binary
import Data.Bytes.Serial (Serial (deserialize, serialize))
import Data.Hashable (Hashable)
import qualified Data.SBV as SBV
import qualified Data.SBV.Internals as SBV
import qualified Data.Serialize as Cereal
import GHC.Generics (Generic)
import Grisette.Internal.Core.Data.Class.Function (Apply (FunType, apply))
import Language.Haskell.TH.Syntax (Lift)
import Test.QuickCheck (Arbitrary)
import Test.QuickCheck.Arbitrary (Arbitrary (arbitrary))

-- | A univariate polynomial with integer coefficients.
--
-- For instance, @5x^3+2x-5@ is represented as
-- @v'AlgRealPoly' [(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, (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, (forall (m :: * -> *). Quote m => AlgRealPoly -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    AlgRealPoly -> Code m AlgRealPoly)
-> Lift AlgRealPoly
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => AlgRealPoly -> m Exp
forall (m :: * -> *). Quote m => AlgRealPoly -> Code m AlgRealPoly
$clift :: forall (m :: * -> *). Quote m => AlgRealPoly -> m Exp
lift :: forall (m :: * -> *). Quote m => AlgRealPoly -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => AlgRealPoly -> Code m AlgRealPoly
liftTyped :: forall (m :: * -> *). Quote m => AlgRealPoly -> Code m AlgRealPoly
Lift)
  deriving newtype (Eq AlgRealPoly
Eq AlgRealPoly =>
(Int -> AlgRealPoly -> Int)
-> (AlgRealPoly -> Int) -> Hashable AlgRealPoly
Int -> AlgRealPoly -> Int
AlgRealPoly -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> AlgRealPoly -> Int
hashWithSalt :: Int -> AlgRealPoly -> Int
$chash :: AlgRealPoly -> Int
hash :: AlgRealPoly -> Int
Hashable, AlgRealPoly -> ()
(AlgRealPoly -> ()) -> NFData AlgRealPoly
forall a. (a -> ()) -> NFData a
$crnf :: AlgRealPoly -> ()
rnf :: AlgRealPoly -> ()
NFData)
  deriving anyclass ((forall (m :: * -> *). MonadPut m => AlgRealPoly -> m ())
-> (forall (m :: * -> *). MonadGet m => m AlgRealPoly)
-> Serial AlgRealPoly
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (m :: * -> *). MonadGet m => m AlgRealPoly
forall (m :: * -> *). MonadPut m => AlgRealPoly -> m ()
$cserialize :: forall (m :: * -> *). MonadPut m => AlgRealPoly -> m ()
serialize :: forall (m :: * -> *). MonadPut m => AlgRealPoly -> m ()
$cdeserialize :: forall (m :: * -> *). MonadGet m => m AlgRealPoly
deserialize :: forall (m :: * -> *). MonadGet m => m AlgRealPoly
Serial)

instance Cereal.Serialize AlgRealPoly where
  put :: Putter AlgRealPoly
put = Putter AlgRealPoly
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => AlgRealPoly -> m ()
serialize
  get :: Get AlgRealPoly
get = Get AlgRealPoly
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m AlgRealPoly
deserialize

instance Binary.Binary AlgRealPoly where
  put :: AlgRealPoly -> Put
put = AlgRealPoly -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => AlgRealPoly -> m ()
serialize
  get :: Get AlgRealPoly
get = Get AlgRealPoly
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m AlgRealPoly
deserialize

-- | Boundary point for real intervals.
data RealPoint
  = -- | Open point.
    OpenPoint Rational
  | -- | Closed point.
    ClosedPoint Rational
  deriving (RealPoint -> RealPoint -> Bool
(RealPoint -> RealPoint -> Bool)
-> (RealPoint -> RealPoint -> Bool) -> Eq RealPoint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RealPoint -> RealPoint -> Bool
== :: RealPoint -> RealPoint -> Bool
$c/= :: RealPoint -> RealPoint -> Bool
/= :: RealPoint -> RealPoint -> Bool
Eq, (forall x. RealPoint -> Rep RealPoint x)
-> (forall x. Rep RealPoint x -> RealPoint) -> Generic RealPoint
forall x. Rep RealPoint x -> RealPoint
forall x. RealPoint -> Rep RealPoint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RealPoint -> Rep RealPoint x
from :: forall x. RealPoint -> Rep RealPoint x
$cto :: forall x. Rep RealPoint x -> RealPoint
to :: forall x. Rep RealPoint x -> RealPoint
Generic, (forall (m :: * -> *). Quote m => RealPoint -> m Exp)
-> (forall (m :: * -> *). Quote m => RealPoint -> Code m RealPoint)
-> Lift RealPoint
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => RealPoint -> m Exp
forall (m :: * -> *). Quote m => RealPoint -> Code m RealPoint
$clift :: forall (m :: * -> *). Quote m => RealPoint -> m Exp
lift :: forall (m :: * -> *). Quote m => RealPoint -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => RealPoint -> Code m RealPoint
liftTyped :: forall (m :: * -> *). Quote m => RealPoint -> Code m RealPoint
Lift)
  deriving anyclass (Eq RealPoint
Eq RealPoint =>
(Int -> RealPoint -> Int)
-> (RealPoint -> Int) -> Hashable RealPoint
Int -> RealPoint -> Int
RealPoint -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> RealPoint -> Int
hashWithSalt :: Int -> RealPoint -> Int
$chash :: RealPoint -> Int
hash :: RealPoint -> Int
Hashable, RealPoint -> ()
(RealPoint -> ()) -> NFData RealPoint
forall a. (a -> ()) -> NFData a
$crnf :: RealPoint -> ()
rnf :: RealPoint -> ()
NFData, (forall (m :: * -> *). MonadPut m => RealPoint -> m ())
-> (forall (m :: * -> *). MonadGet m => m RealPoint)
-> Serial RealPoint
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (m :: * -> *). MonadGet m => m RealPoint
forall (m :: * -> *). MonadPut m => RealPoint -> m ()
$cserialize :: forall (m :: * -> *). MonadPut m => RealPoint -> m ()
serialize :: forall (m :: * -> *). MonadPut m => RealPoint -> m ()
$cdeserialize :: forall (m :: * -> *). MonadGet m => m RealPoint
deserialize :: forall (m :: * -> *). MonadGet m => m RealPoint
Serial)

instance Cereal.Serialize RealPoint where
  put :: Putter RealPoint
put = Putter RealPoint
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => RealPoint -> m ()
serialize
  get :: Get RealPoint
get = Get RealPoint
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m RealPoint
deserialize

instance Binary.Binary RealPoint where
  put :: RealPoint -> Put
put = RealPoint -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => RealPoint -> m ()
serialize
  get :: Get RealPoint
get = Get RealPoint
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m RealPoint
deserialize

toSBVRealPoint :: RealPoint -> SBV.RealPoint Rational
toSBVRealPoint :: RealPoint -> RealPoint Rational
toSBVRealPoint (OpenPoint Rational
r) = Rational -> RealPoint Rational
forall a. a -> RealPoint a
SBV.OpenPoint Rational
r
toSBVRealPoint (ClosedPoint Rational
r) = Rational -> RealPoint Rational
forall a. a -> RealPoint a
SBV.ClosedPoint Rational
r

fromSBVRealPoint :: SBV.RealPoint Rational -> RealPoint
fromSBVRealPoint :: RealPoint Rational -> RealPoint
fromSBVRealPoint (SBV.OpenPoint Rational
r) = Rational -> RealPoint
OpenPoint Rational
r
fromSBVRealPoint (SBV.ClosedPoint Rational
r) = Rational -> RealPoint
ClosedPoint Rational
r

-- | Algebraic real numbers. The representation can be abstract for
-- roots-of-polynomials or intervals.
data AlgReal where
  -- | Exact rational number.
  AlgExactRational :: Rational -> AlgReal
  -- | Inexact rational numbers. SMT-solver return it with ? at the end.
  AlgInexactRational :: Rational -> AlgReal
  -- | Algebraic real number as a root of a polynomial.
  AlgPolyRoot ::
    -- | Which root is it?
    Integer ->
    -- | Polynomial defining equation.
    AlgRealPoly ->
    -- | Approximate decimal representation.
    Maybe String ->
    AlgReal
  -- | Interval with low and high bounds.
  AlgInterval ::
    -- | Lower bound.
    RealPoint ->
    -- | Upper bound.
    RealPoint ->
    AlgReal
  deriving ((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, (forall (m :: * -> *). Quote m => AlgReal -> m Exp)
-> (forall (m :: * -> *). Quote m => AlgReal -> Code m AlgReal)
-> Lift AlgReal
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => AlgReal -> m Exp
forall (m :: * -> *). Quote m => AlgReal -> Code m AlgReal
$clift :: forall (m :: * -> *). Quote m => AlgReal -> m Exp
lift :: forall (m :: * -> *). Quote m => AlgReal -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => AlgReal -> Code m AlgReal
liftTyped :: forall (m :: * -> *). Quote m => AlgReal -> Code m AlgReal
Lift)
  deriving anyclass (Eq AlgReal
Eq AlgReal =>
(Int -> AlgReal -> Int) -> (AlgReal -> Int) -> Hashable AlgReal
Int -> AlgReal -> Int
AlgReal -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> AlgReal -> Int
hashWithSalt :: Int -> AlgReal -> Int
$chash :: AlgReal -> Int
hash :: AlgReal -> Int
Hashable, AlgReal -> ()
(AlgReal -> ()) -> NFData AlgReal
forall a. (a -> ()) -> NFData a
$crnf :: AlgReal -> ()
rnf :: AlgReal -> ()
NFData, (forall (m :: * -> *). MonadPut m => AlgReal -> m ())
-> (forall (m :: * -> *). MonadGet m => m AlgReal)
-> Serial AlgReal
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (m :: * -> *). MonadGet m => m AlgReal
forall (m :: * -> *). MonadPut m => AlgReal -> m ()
$cserialize :: forall (m :: * -> *). MonadPut m => AlgReal -> m ()
serialize :: forall (m :: * -> *). MonadPut m => AlgReal -> m ()
$cdeserialize :: forall (m :: * -> *). MonadGet m => m AlgReal
deserialize :: forall (m :: * -> *). MonadGet m => m AlgReal
Serial)

instance Cereal.Serialize AlgReal where
  put :: Putter AlgReal
put = Putter AlgReal
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => AlgReal -> m ()
serialize
  get :: Get AlgReal
get = Get AlgReal
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m AlgReal
deserialize

instance Binary.Binary AlgReal where
  put :: AlgReal -> Put
put = AlgReal -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => AlgReal -> m ()
serialize
  get :: Get AlgReal
get = Get AlgReal
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m AlgReal
deserialize

-- | Convert algebraic real numbers to SBV's algebraic real numbers.
toSBVAlgReal :: AlgReal -> SBV.AlgReal
toSBVAlgReal :: AlgReal -> AlgReal
toSBVAlgReal (AlgExactRational Rational
r) = Bool -> Rational -> AlgReal
SBV.AlgRational Bool
True Rational
r
toSBVAlgReal (AlgInexactRational Rational
r) = Bool -> Rational -> AlgReal
SBV.AlgRational Bool
False Rational
r
toSBVAlgReal (AlgPolyRoot Integer
i (AlgRealPoly [(Integer, Integer)]
ps) Maybe String
approx) =
  (Integer, AlgRealPoly) -> Maybe String -> AlgReal
SBV.AlgPolyRoot (Integer
i, [(Integer, Integer)] -> AlgRealPoly
SBV.AlgRealPoly [(Integer, Integer)]
ps) Maybe String
approx
toSBVAlgReal (AlgInterval RealPoint
l RealPoint
u) =
  RealPoint Rational -> RealPoint Rational -> AlgReal
SBV.AlgInterval (RealPoint -> RealPoint Rational
toSBVRealPoint RealPoint
l) (RealPoint -> RealPoint Rational
toSBVRealPoint RealPoint
u)

-- | Convert SBV's algebraic real numbers to algebraic real numbers.
fromSBVAlgReal :: SBV.AlgReal -> AlgReal
fromSBVAlgReal :: AlgReal -> AlgReal
fromSBVAlgReal (SBV.AlgRational Bool
True Rational
r) = Rational -> AlgReal
AlgExactRational Rational
r
fromSBVAlgReal (SBV.AlgRational Bool
False Rational
r) = Rational -> AlgReal
AlgInexactRational Rational
r
fromSBVAlgReal (SBV.AlgPolyRoot (Integer
i, SBV.AlgRealPoly [(Integer, Integer)]
ps) Maybe String
approx) =
  Integer -> AlgRealPoly -> Maybe String -> AlgReal
AlgPolyRoot Integer
i ([(Integer, Integer)] -> AlgRealPoly
AlgRealPoly [(Integer, Integer)]
ps) Maybe String
approx
fromSBVAlgReal (SBV.AlgInterval RealPoint Rational
l RealPoint Rational
u) =
  RealPoint -> RealPoint -> AlgReal
AlgInterval (RealPoint Rational -> RealPoint
fromSBVRealPoint RealPoint Rational
l) (RealPoint Rational -> RealPoint
fromSBVRealPoint RealPoint Rational
u)

instance Show AlgReal where
  show :: AlgReal -> String
show AlgReal
r = AlgReal -> String
forall a. Show a => a -> String
show (AlgReal -> String) -> AlgReal -> String
forall a b. (a -> b) -> a -> b
$ AlgReal -> AlgReal
toSBVAlgReal AlgReal
r

-- | Exception for unsupported operations on algebraic real numbers.
--
-- We only support operations on exact rationals.
data UnsupportedAlgRealOperation = UnsupportedAlgRealOperation
  { UnsupportedAlgRealOperation -> String
op :: String,
    UnsupportedAlgRealOperation -> String
msg :: String
  }
  deriving anyclass (Show UnsupportedAlgRealOperation
Typeable UnsupportedAlgRealOperation
(Typeable UnsupportedAlgRealOperation,
 Show UnsupportedAlgRealOperation) =>
(UnsupportedAlgRealOperation -> SomeException)
-> (SomeException -> Maybe UnsupportedAlgRealOperation)
-> (UnsupportedAlgRealOperation -> String)
-> (UnsupportedAlgRealOperation -> Bool)
-> Exception UnsupportedAlgRealOperation
SomeException -> Maybe UnsupportedAlgRealOperation
UnsupportedAlgRealOperation -> Bool
UnsupportedAlgRealOperation -> String
UnsupportedAlgRealOperation -> SomeException
forall e.
(Typeable e, Show e) =>
(e -> SomeException)
-> (SomeException -> Maybe e)
-> (e -> String)
-> (e -> Bool)
-> Exception e
$ctoException :: UnsupportedAlgRealOperation -> SomeException
toException :: UnsupportedAlgRealOperation -> SomeException
$cfromException :: SomeException -> Maybe UnsupportedAlgRealOperation
fromException :: SomeException -> Maybe UnsupportedAlgRealOperation
$cdisplayException :: UnsupportedAlgRealOperation -> String
displayException :: UnsupportedAlgRealOperation -> String
$cbacktraceDesired :: UnsupportedAlgRealOperation -> Bool
backtraceDesired :: UnsupportedAlgRealOperation -> Bool
Exception)

instance Show UnsupportedAlgRealOperation where
  show :: UnsupportedAlgRealOperation -> String
show (UnsupportedAlgRealOperation String
op String
msg) =
    String
"AlgReal."
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": unsupported operation on algebraic rationals, only support exact "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"rationals"
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg

op1 :: String -> (Rational -> Rational) -> AlgReal -> AlgReal
op1 :: String -> (Rational -> Rational) -> AlgReal -> AlgReal
op1 String
_ Rational -> Rational
f (AlgExactRational Rational
r) = Rational -> AlgReal
AlgExactRational (Rational -> AlgReal) -> Rational -> AlgReal
forall a b. (a -> b) -> a -> b
$ Rational -> Rational
f Rational
r
op1 String
name Rational -> Rational
_ AlgReal
r =
  UnsupportedAlgRealOperation -> AlgReal
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw
    UnsupportedAlgRealOperation {op :: String
op = String
name, msg :: String
msg = AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r}

op2 ::
  String ->
  (Rational -> Rational -> Rational) ->
  AlgReal ->
  AlgReal ->
  AlgReal
op2 :: String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
op2 String
_ Rational -> Rational -> Rational
f (AlgExactRational Rational
l) (AlgExactRational Rational
r) = Rational -> AlgReal
AlgExactRational (Rational -> AlgReal) -> Rational -> AlgReal
forall a b. (a -> b) -> a -> b
$ Rational -> Rational -> Rational
f Rational
l Rational
r
op2 String
name Rational -> Rational -> Rational
_ AlgReal
l AlgReal
r =
  UnsupportedAlgRealOperation -> AlgReal
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw
    UnsupportedAlgRealOperation
      { op :: String
op = String
name,
        msg :: String
msg = AlgReal -> String
forall a. Show a => a -> String
show AlgReal
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" and " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r
      }

instance Eq AlgReal where
  (AlgExactRational Rational
l) == :: AlgReal -> AlgReal -> Bool
== (AlgExactRational Rational
r) = Rational
l Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
r
  AlgReal
l == AlgReal
r =
    UnsupportedAlgRealOperation -> Bool
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw (UnsupportedAlgRealOperation -> Bool)
-> UnsupportedAlgRealOperation -> Bool
forall a b. (a -> b) -> a -> b
$
      String -> String -> UnsupportedAlgRealOperation
UnsupportedAlgRealOperation String
"==" (String -> UnsupportedAlgRealOperation)
-> String -> UnsupportedAlgRealOperation
forall a b. (a -> b) -> a -> b
$
        AlgReal -> String
forall a. Show a => a -> String
show AlgReal
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" and " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r

instance Ord AlgReal where
  compare :: AlgReal -> AlgReal -> Ordering
compare (AlgExactRational Rational
l) (AlgExactRational Rational
r) = Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Rational
l Rational
r
  compare AlgReal
l AlgReal
r =
    UnsupportedAlgRealOperation -> Ordering
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw (UnsupportedAlgRealOperation -> Ordering)
-> UnsupportedAlgRealOperation -> Ordering
forall a b. (a -> b) -> a -> b
$
      String -> String -> UnsupportedAlgRealOperation
UnsupportedAlgRealOperation String
"compare" (String -> UnsupportedAlgRealOperation)
-> String -> UnsupportedAlgRealOperation
forall a b. (a -> b) -> a -> b
$
        AlgReal -> String
forall a. Show a => a -> String
show AlgReal
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" and " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r

instance Num AlgReal where
  + :: AlgReal -> AlgReal -> AlgReal
(+) = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
op2 String
"+" Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(+)
  * :: AlgReal -> AlgReal -> AlgReal
(*) = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
op2 String
"*" Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(*)
  (-) = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
op2 String
"-" (-)
  negate :: AlgReal -> AlgReal
negate = String -> (Rational -> Rational) -> AlgReal -> AlgReal
op1 String
"negate" Rational -> Rational
forall a. Num a => a -> a
negate
  abs :: AlgReal -> AlgReal
abs = String -> (Rational -> Rational) -> AlgReal -> AlgReal
op1 String
"abs" Rational -> Rational
forall a. Num a => a -> a
abs
  signum :: AlgReal -> AlgReal
signum = String -> (Rational -> Rational) -> AlgReal -> AlgReal
op1 String
"signum" Rational -> Rational
forall a. Num a => a -> a
signum
  fromInteger :: Integer -> AlgReal
fromInteger = Rational -> AlgReal
AlgExactRational (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

-- | Unlike sbv, we throw the error when divided by zero happens
instance Fractional AlgReal where
  / :: AlgReal -> AlgReal -> AlgReal
(/) = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
op2 String
"/" Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
(/)
  fromRational :: Rational -> AlgReal
fromRational = Rational -> AlgReal
AlgExactRational

instance Real AlgReal where
  toRational :: AlgReal -> Rational
toRational (AlgExactRational Rational
r) = Rational
r
  toRational AlgReal
r =
    UnsupportedAlgRealOperation -> Rational
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw (UnsupportedAlgRealOperation -> Rational)
-> UnsupportedAlgRealOperation -> Rational
forall a b. (a -> b) -> a -> b
$
      String -> String -> UnsupportedAlgRealOperation
UnsupportedAlgRealOperation String
"toRational" (String -> UnsupportedAlgRealOperation)
-> String -> UnsupportedAlgRealOperation
forall a b. (a -> b) -> a -> b
$
        AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r

instance Arbitrary AlgReal where
  arbitrary :: Gen AlgReal
arbitrary = Rational -> AlgReal
AlgExactRational (Rational -> AlgReal) -> Gen Rational -> Gen AlgReal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Rational
forall a. Arbitrary a => Gen a
arbitrary

instance Apply AlgReal where
  type FunType AlgReal = AlgReal
  apply :: AlgReal -> FunType AlgReal
apply = AlgReal -> FunType AlgReal
AlgReal -> AlgReal
forall a. a -> a
id