module Language.Hasmtlib.Internal.Expr.Num where

import Prelude hiding (div, mod, quotRem, rem, quot, divMod)
import Language.Hasmtlib.Internal.Expr
import Language.Hasmtlib.Integraled
import Language.Hasmtlib.Iteable
import Language.Hasmtlib.Equatable
import Language.Hasmtlib.Orderable
import GHC.TypeNats

instance Num (Expr IntSort) where
   fromInteger :: Integer -> Expr 'IntSort
fromInteger = Value 'IntSort -> Expr 'IntSort
forall (t :: SMTSort). Value t -> Expr t
Constant (Value 'IntSort -> Expr 'IntSort)
-> (Integer -> Value 'IntSort) -> Integer -> Expr 'IntSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Value 'IntSort
HaskellType 'IntSort -> Value 'IntSort
IntValue
   {-# INLINE fromInteger #-}
   + :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
(+)         = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Plus
   {-# INLINE (+) #-}
   (-) Expr 'IntSort
x Expr 'IntSort
y     = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Plus Expr 'IntSort
x (Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Neg Expr 'IntSort
y)
   {-# INLINE (-) #-}
   * :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
(*)         = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Mul
   {-# INLINE (*) #-}
   negate :: Expr 'IntSort -> Expr 'IntSort
negate      = Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Neg
   {-# INLINE negate #-}
   abs :: Expr 'IntSort -> Expr 'IntSort
abs         = Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Abs
   {-# INLINE abs #-}
   signum :: Expr 'IntSort -> Expr 'IntSort
signum Expr 'IntSort
x    = Expr 'BoolSort -> Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'IntSort
x Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
=== Expr 'IntSort
0) Expr 'IntSort
0 (Expr 'IntSort -> Expr 'IntSort) -> Expr 'IntSort -> Expr 'IntSort
forall a b. (a -> b) -> a -> b
$ Expr 'BoolSort -> Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'IntSort
x Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
<? Expr 'IntSort
0) (-Expr 'IntSort
1) Expr 'IntSort
1
   {-# INLINE signum #-}

instance Num (Expr RealSort) where
   fromInteger :: Integer -> Expr 'RealSort
fromInteger = Value 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Value t -> Expr t
Constant (Value 'RealSort -> Expr 'RealSort)
-> (Integer -> Value 'RealSort) -> Integer -> Expr 'RealSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Value 'RealSort
HaskellType 'RealSort -> Value 'RealSort
RealValue (Double -> Value 'RealSort)
-> (Integer -> Double) -> Integer -> Value 'RealSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral
   {-# INLINE fromInteger #-}
   + :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
(+)         = Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Plus
   {-# INLINE (+) #-}
   Expr 'RealSort
x - :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
- Expr 'RealSort
y       = Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Plus Expr 'RealSort
x (Expr 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Neg Expr 'RealSort
y)
   {-# INLINE (-) #-}
   * :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
(*)         = Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Mul
   {-# INLINE (*) #-}
   negate :: Expr 'RealSort -> Expr 'RealSort
negate      = Expr 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Neg
   {-# INLINE negate #-}
   abs :: Expr 'RealSort -> Expr 'RealSort
abs         = Expr 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Abs
   {-# INLINE abs #-}
   signum :: Expr 'RealSort -> Expr 'RealSort
signum Expr 'RealSort
x    = Expr 'BoolSort
-> Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'RealSort
x Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
=== Expr 'RealSort
0) Expr 'RealSort
0 (Expr 'RealSort -> Expr 'RealSort)
-> Expr 'RealSort -> Expr 'RealSort
forall a b. (a -> b) -> a -> b
$ Expr 'BoolSort
-> Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'RealSort
x Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
<? Expr 'RealSort
0) (-Expr 'RealSort
1) Expr 'RealSort
1
   {-# INLINE signum #-}

instance KnownNat n => Num (Expr (BvSort n)) where
   fromInteger :: Integer -> Expr ('BvSort n)
fromInteger = Value ('BvSort n) -> Expr ('BvSort n)
forall (t :: SMTSort). Value t -> Expr t
Constant (Value ('BvSort n) -> Expr ('BvSort n))
-> (Integer -> Value ('BvSort n)) -> Integer -> Expr ('BvSort n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec n -> Value ('BvSort n)
HaskellType ('BvSort n) -> Value ('BvSort n)
forall (n :: Nat). HaskellType ('BvSort n) -> Value ('BvSort n)
BvValue (Bitvec n -> Value ('BvSort n))
-> (Integer -> Bitvec n) -> Integer -> Value ('BvSort n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Bitvec n
forall a. Num a => Integer -> a
fromInteger
   {-# INLINE fromInteger #-}
   + :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
(+)         = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvAdd
   {-# INLINE (+) #-}
   (-)         = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvSub
   {-# INLINE (-) #-}
   * :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
(*)         = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvMul
   {-# INLINE (*) #-}
   abs :: Expr ('BvSort n) -> Expr ('BvSort n)
abs         = Expr ('BvSort n) -> Expr ('BvSort n)
forall a. a -> a
id
   {-# INLINE abs #-}
   signum :: Expr ('BvSort n) -> Expr ('BvSort n)
signum Expr ('BvSort n)
_    = Expr ('BvSort n)
0
   {-# INLINE signum #-}

instance Fractional (Expr RealSort) where
  fromRational :: Rational -> Expr 'RealSort
fromRational = Value 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Value t -> Expr t
Constant (Value 'RealSort -> Expr 'RealSort)
-> (Rational -> Value 'RealSort) -> Rational -> Expr 'RealSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Value 'RealSort
HaskellType 'RealSort -> Value 'RealSort
RealValue (Double -> Value 'RealSort)
-> (Rational -> Double) -> Rational -> Value 'RealSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Double
forall a. Fractional a => Rational -> a
fromRational
  {-# INLINE fromRational #-}
  / :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
(/)          = Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
Div
  {-# INLINE (/) #-}

instance Floating (Expr RealSort) where
    pi :: Expr 'RealSort
pi    = Expr 'RealSort
Pi
    {-# INLINE pi #-}
    exp :: Expr 'RealSort -> Expr 'RealSort
exp   = Expr 'RealSort -> Expr 'RealSort
Exp
    {-# INLINE exp #-}
    log :: Expr 'RealSort -> Expr 'RealSort
log   = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solvers currently do not support log"
    sqrt :: Expr 'RealSort -> Expr 'RealSort
sqrt  = Expr 'RealSort -> Expr 'RealSort
Sqrt
    {-# INLINE sqrt #-}
    sin :: Expr 'RealSort -> Expr 'RealSort
sin   = Expr 'RealSort -> Expr 'RealSort
Sin
    {-# INLINE sin #-}
    cos :: Expr 'RealSort -> Expr 'RealSort
cos   = Expr 'RealSort -> Expr 'RealSort
Cos
    {-# INLINE cos #-}
    tan :: Expr 'RealSort -> Expr 'RealSort
tan   = Expr 'RealSort -> Expr 'RealSort
Tan
    {-# INLINE tan #-}
    asin :: Expr 'RealSort -> Expr 'RealSort
asin  = Expr 'RealSort -> Expr 'RealSort
Asin
    {-# INLINE asin #-}
    acos :: Expr 'RealSort -> Expr 'RealSort
acos  = Expr 'RealSort -> Expr 'RealSort
Acos
    {-# INLINE acos #-}
    atan :: Expr 'RealSort -> Expr 'RealSort
atan  = Expr 'RealSort -> Expr 'RealSort
Atan
    {-# INLINE atan #-}
    sinh :: Expr 'RealSort -> Expr 'RealSort
sinh  = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solver currently do not support sinh"
    cosh :: Expr 'RealSort -> Expr 'RealSort
cosh  = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solver currently do not support cosh"
    tanh :: Expr 'RealSort -> Expr 'RealSort
tanh  = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solver currently do not support tanh"
    asinh :: Expr 'RealSort -> Expr 'RealSort
asinh = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solver currently do not support asinh"
    acosh :: Expr 'RealSort -> Expr 'RealSort
acosh = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solver currently do not support acosh"
    atanh :: Expr 'RealSort -> Expr 'RealSort
atanh = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solver currently do not support atanh"

instance Integraled (Expr IntSort) where
  quot :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
quot = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
IDiv
  {-# INLINE quot #-}
  rem :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
rem  = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
Mod
  {-# INLINE rem #-}
  div :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
div  = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
IDiv
  {-# INLINE div #-}
  mod :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
mod  = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
Mod
  {-# INLINE mod #-}
  quotRem :: Expr 'IntSort -> Expr 'IntSort -> (Expr 'IntSort, Expr 'IntSort)
quotRem Expr 'IntSort
x Expr 'IntSort
y = (Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall a. Integraled a => a -> a -> a
quot Expr 'IntSort
x Expr 'IntSort
y, Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall a. Integraled a => a -> a -> a
rem Expr 'IntSort
x Expr 'IntSort
y)
  {-# INLINE quotRem #-}
  divMod :: Expr 'IntSort -> Expr 'IntSort -> (Expr 'IntSort, Expr 'IntSort)
divMod Expr 'IntSort
x Expr 'IntSort
y  = (Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall a. Integraled a => a -> a -> a
div Expr 'IntSort
x Expr 'IntSort
y, Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall a. Integraled a => a -> a -> a
mod Expr 'IntSort
x Expr 'IntSort
y)
  {-# INLINE divMod #-}

instance KnownNat n => Integraled (Expr (BvSort n)) where
  quot :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
quot        = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuDiv
  {-# INLINE quot #-}
  rem :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
rem         = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuRem
  {-# INLINE rem #-}
  div :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
div         = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuDiv
  {-# INLINE div #-}
  mod :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
mod         = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuRem
  {-# INLINE mod #-}
  quotRem :: Expr ('BvSort n)
-> Expr ('BvSort n) -> (Expr ('BvSort n), Expr ('BvSort n))
quotRem Expr ('BvSort n)
x Expr ('BvSort n)
y = (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall a. Integraled a => a -> a -> a
quot Expr ('BvSort n)
x Expr ('BvSort n)
y, Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall a. Integraled a => a -> a -> a
rem Expr ('BvSort n)
x Expr ('BvSort n)
y)
  {-# INLINE quotRem #-}
  divMod :: Expr ('BvSort n)
-> Expr ('BvSort n) -> (Expr ('BvSort n), Expr ('BvSort n))
divMod Expr ('BvSort n)
x Expr ('BvSort n)
y  = (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall a. Integraled a => a -> a -> a
div Expr ('BvSort n)
x Expr ('BvSort n)
y, Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall a. Integraled a => a -> a -> a
mod Expr ('BvSort n)
x Expr ('BvSort n)
y)
  {-# INLINE divMod #-}