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 Data.Proxy
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 #-}

-- | Bitvector shift left
bvShL    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
bvShL :: forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
bvShL    = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvShL
{-# INLINE bvShL #-}

-- | Bitvector logical shift right
bvLShR   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
bvLShR :: forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
bvLShR   = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvLShR
{-# INLINE bvLShR #-}

-- | Concat two bitvectors
bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
bvConcat :: forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Expr ('BvSort n) -> Expr ('BvSort m) -> Expr ('BvSort (n + m))
bvConcat = Expr ('BvSort n) -> Expr ('BvSort m) -> Expr ('BvSort (n + m))
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Expr ('BvSort n) -> Expr ('BvSort m) -> Expr ('BvSort (n + m))
BvConcat
{-# INLINE bvConcat #-}

-- | Rotate bitvector left
bvRotL   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
bvRotL :: forall (n :: Nat) (i :: Nat).
(KnownNat n, KnownNat i, KnownNat (Mod i n)) =>
Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
bvRotL   = Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat) (i :: Nat).
(KnownNat n, KnownNat i, KnownNat (Mod i n)) =>
Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
BvRotL
{-# INLINE bvRotL #-}

-- | Rotate bitvector right
bvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
bvRotR :: forall (n :: Nat) (i :: Nat).
(KnownNat n, KnownNat i, KnownNat (Mod i n)) =>
Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
bvRotR   = Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat) (i :: Nat).
(KnownNat n, KnownNat i, KnownNat (Mod i n)) =>
Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
BvRotR
{-# INLINE bvRotR #-}