{-# LANGUAGE UndecidableInstances #-}

{- |
This module provides the wrapper 'Value' for embedding Haskell-Values into the SMT-Context.

The Direction @Haskell-Value => SMT-Value@ is the creation of a constant in the SMT-Problem.

The other way around @SMT-Value => Haskell-Value@ is mainly used when decoding a solvers solutions for variables.
-}
module Language.Hasmtlib.Type.Value
(
  -- * Type
  Value(..)

  -- * Conversion
, wrapValue, unwrapValue
)
where

import Prelude hiding (not, (&&), (||))
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Type.Bitvec
import Language.Hasmtlib.Boolean
import Data.GADT.Compare
import Data.Proxy
import Control.Lens
import GHC.TypeLits

-- | A wrapper for values of 'SMTSort's.
--   This wraps a Haskell-value into the SMT-Context.
data Value (t :: SMTSort) where
  IntValue    :: HaskellType IntSort    -> Value IntSort
  RealValue   :: HaskellType RealSort   -> Value RealSort
  BoolValue   :: HaskellType BoolSort   -> Value BoolSort
  BvValue     :: (KnownBvEnc enc, KnownNat n) => HaskellType (BvSort enc n) -> Value (BvSort enc n)
  ArrayValue  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)
  StringValue :: HaskellType StringSort -> Value StringSort

deriving instance Eq (HaskellType t) => Eq (Value t)
deriving instance Ord (HaskellType t) => Ord (Value t)

instance GEq Value where
  geq :: forall (a :: SMTSort) (b :: SMTSort).
Value a -> Value b -> Maybe (a :~: b)
geq (BoolValue HaskellType 'BoolSort
x) (BoolValue HaskellType 'BoolSort
y)   = if Bool
HaskellType 'BoolSort
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
HaskellType 'BoolSort
y then (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl else Maybe (a :~: b)
forall a. Maybe a
Nothing
  geq (IntValue HaskellType 'IntSort
x) (IntValue HaskellType 'IntSort
y)     = if Integer
HaskellType 'IntSort
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
HaskellType 'IntSort
y then (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl else Maybe (a :~: b)
forall a. Maybe a
Nothing
  geq (RealValue HaskellType 'RealSort
x) (RealValue HaskellType 'RealSort
y)   = if Rational
HaskellType 'RealSort
x Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
HaskellType 'RealSort
y then (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl else Maybe (a :~: b)
forall a. Maybe a
Nothing
  geq (BvValue HaskellType ('BvSort enc n)
x) (BvValue HaskellType ('BvSort enc n)
y)       = case Bitvec enc n -> Bitvec enc n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat Bitvec enc n
HaskellType ('BvSort enc n)
x Bitvec enc n
HaskellType ('BvSort enc n)
y of
    OrderingI n n
EQI -> case SBvEnc enc -> SBvEnc enc -> Maybe (enc :~: enc)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BvEnc) (b :: BvEnc).
SBvEnc a -> SBvEnc b -> Maybe (a :~: b)
geq (Bitvec enc n -> SBvEnc enc
forall {k} (enc :: BvEnc) (a :: k) (prxy :: BvEnc -> k -> *).
KnownBvEnc enc =>
prxy enc a -> SBvEnc enc
bvEncSing'' Bitvec enc n
HaskellType ('BvSort enc n)
x) (Bitvec enc n -> SBvEnc enc
forall {k} (enc :: BvEnc) (a :: k) (prxy :: BvEnc -> k -> *).
KnownBvEnc enc =>
prxy enc a -> SBvEnc enc
bvEncSing'' Bitvec enc n
HaskellType ('BvSort enc n)
y) of
      Maybe (enc :~: enc)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
      Just enc :~: enc
Refl -> if Bitvec enc n
HaskellType ('BvSort enc n)
x Bitvec enc n -> Bitvec enc n -> Bool
forall a. Eq a => a -> a -> Bool
== Bitvec enc n
HaskellType ('BvSort enc n)
y then (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl else Maybe (a :~: b)
forall a. Maybe a
Nothing
    OrderingI n n
_   -> Maybe (a :~: b)
forall a. Maybe a
Nothing
  geq ax :: Value a
ax@(ArrayValue HaskellType ('ArraySort k v)
x) ay :: Value b
ay@(ArrayValue HaskellType ('ArraySort k v)
y) = case SSMTSort a -> SSMTSort b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: SMTSort) (b :: SMTSort).
SSMTSort a -> SSMTSort b -> Maybe (a :~: b)
geq (Value a -> SSMTSort a
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Value a
ax) (Value b -> SSMTSort b
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Value b
ay) of
    Maybe (a :~: b)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
    Just a :~: b
Refl -> if ConstArray (HaskellType k) (HaskellType v)
HaskellType ('ArraySort k v)
x ConstArray (HaskellType k) (HaskellType v)
-> ConstArray (HaskellType k) (HaskellType v) -> Bool
forall a. Eq a => a -> a -> Bool
== ConstArray (HaskellType k) (HaskellType v)
HaskellType ('ArraySort k v)
y then (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl else Maybe (a :~: b)
forall a. Maybe a
Nothing
  geq (StringValue HaskellType 'StringSort
x) (StringValue HaskellType 'StringSort
y) = if Text
HaskellType 'StringSort
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
HaskellType 'StringSort
y then (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl else Maybe (a :~: b)
forall a. Maybe a
Nothing
  geq Value a
_ Value b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

liftOrdering :: forall {k} {a :: k}. Ordering -> GOrdering a a
liftOrdering :: forall {k} {a :: k}. Ordering -> GOrdering a a
liftOrdering Ordering
LT = GOrdering a a
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
liftOrdering Ordering
EQ = GOrdering a a
forall {k} (a :: k). GOrdering a a
GEQ
liftOrdering Ordering
GT = GOrdering a a
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
{-# INLINE liftOrdering #-}

instance GCompare Value where
  gcompare :: forall (a :: SMTSort) (b :: SMTSort).
Value a -> Value b -> GOrdering a b
gcompare (BoolValue HaskellType 'BoolSort
x) (BoolValue HaskellType 'BoolSort
x')     = Ordering -> GOrdering a a
forall {k} {a :: k}. Ordering -> GOrdering a a
liftOrdering (Ordering -> GOrdering a a) -> Ordering -> GOrdering a a
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Bool
HaskellType 'BoolSort
x Bool
HaskellType 'BoolSort
x'
  gcompare (IntValue HaskellType 'IntSort
x)  (IntValue HaskellType 'IntSort
x')      = Ordering -> GOrdering a a
forall {k} {a :: k}. Ordering -> GOrdering a a
liftOrdering (Ordering -> GOrdering a a) -> Ordering -> GOrdering a a
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
HaskellType 'IntSort
x Integer
HaskellType 'IntSort
x'
  gcompare (RealValue HaskellType 'RealSort
x) (RealValue HaskellType 'RealSort
x')     = Ordering -> GOrdering a a
forall {k} {a :: k}. Ordering -> GOrdering a a
liftOrdering (Ordering -> GOrdering a a) -> Ordering -> GOrdering a a
forall a b. (a -> b) -> a -> b
$ Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Rational
HaskellType 'RealSort
x Rational
HaskellType 'RealSort
x'
  gcompare (BvValue HaskellType ('BvSort enc n)
x) (BvValue HaskellType ('BvSort enc n)
x')         = case Bitvec enc n -> Bitvec enc n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat Bitvec enc n
HaskellType ('BvSort enc n)
x Bitvec enc n
HaskellType ('BvSort enc n)
x' of
    OrderingI n n
LTI -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
    OrderingI n n
EQI -> case SBvEnc enc -> SBvEnc enc -> GOrdering enc enc
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
forall (a :: BvEnc) (b :: BvEnc).
SBvEnc a -> SBvEnc b -> GOrdering a b
gcompare (Bitvec enc n -> SBvEnc enc
forall {k} (enc :: BvEnc) (a :: k) (prxy :: BvEnc -> k -> *).
KnownBvEnc enc =>
prxy enc a -> SBvEnc enc
bvEncSing'' Bitvec enc n
HaskellType ('BvSort enc n)
x) (Bitvec enc n -> SBvEnc enc
forall {k} (enc :: BvEnc) (a :: k) (prxy :: BvEnc -> k -> *).
KnownBvEnc enc =>
prxy enc a -> SBvEnc enc
bvEncSing'' Bitvec enc n
HaskellType ('BvSort enc n)
x') of
      GOrdering enc enc
GLT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
      GOrdering enc enc
GEQ -> Ordering -> GOrdering a a
forall {k} {a :: k}. Ordering -> GOrdering a a
liftOrdering (Ordering -> GOrdering a a) -> Ordering -> GOrdering a a
forall a b. (a -> b) -> a -> b
$ Bitvec enc n -> Bitvec enc n -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Bitvec enc n
HaskellType ('BvSort enc n)
x Bitvec enc n
HaskellType ('BvSort enc n)
x'
      GOrdering enc enc
GGT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
    OrderingI n n
GTI -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
  gcompare (ArrayValue HaskellType ('ArraySort k v)
x) (ArrayValue HaskellType ('ArraySort k v)
x')   = case SSMTSort k -> SSMTSort k -> GOrdering k k
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
forall (a :: SMTSort) (b :: SMTSort).
SSMTSort a -> SSMTSort b -> GOrdering a b
gcompare (Proxy k -> SSMTSort k
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' (HaskellType ('ArraySort k v) -> Proxy k
forall (k :: SMTSort) (v :: SMTSort).
HaskellType ('ArraySort k v) -> Proxy k
pk HaskellType ('ArraySort k v)
x)) (Proxy k -> SSMTSort k
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' (HaskellType ('ArraySort k v) -> Proxy k
forall (k :: SMTSort) (v :: SMTSort).
HaskellType ('ArraySort k v) -> Proxy k
pk HaskellType ('ArraySort k v)
x')) of
    GOrdering k k
GLT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
    GOrdering k k
GEQ -> case SSMTSort v -> SSMTSort v -> GOrdering v v
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
forall (a :: SMTSort) (b :: SMTSort).
SSMTSort a -> SSMTSort b -> GOrdering a b
gcompare (Proxy v -> SSMTSort v
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' (HaskellType ('ArraySort k v) -> Proxy v
forall (k :: SMTSort) (v :: SMTSort).
HaskellType ('ArraySort k v) -> Proxy v
pv HaskellType ('ArraySort k v)
x)) (Proxy v -> SSMTSort v
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' (HaskellType ('ArraySort k v) -> Proxy v
forall (k :: SMTSort) (v :: SMTSort).
HaskellType ('ArraySort k v) -> Proxy v
pv HaskellType ('ArraySort k v)
HaskellType ('ArraySort k v)
x')) of
      GOrdering v v
GLT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
      GOrdering v v
GEQ -> Ordering -> GOrdering a a
forall {k} {a :: k}. Ordering -> GOrdering a a
liftOrdering (Ordering -> GOrdering a a) -> Ordering -> GOrdering a a
forall a b. (a -> b) -> a -> b
$ ConstArray (HaskellType k) (HaskellType v)
-> ConstArray (HaskellType k) (HaskellType v) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ConstArray (HaskellType k) (HaskellType v)
HaskellType ('ArraySort k v)
x ConstArray (HaskellType k) (HaskellType v)
HaskellType ('ArraySort k v)
x'
      GOrdering v v
GGT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
    GOrdering k k
GGT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
    where
      pk :: forall k v. HaskellType (ArraySort k v) -> Proxy k
      pk :: forall (k :: SMTSort) (v :: SMTSort).
HaskellType ('ArraySort k v) -> Proxy k
pk HaskellType ('ArraySort k v)
_ = forall {k} (t :: k). Proxy t
forall (t :: SMTSort). Proxy t
Proxy @k
      pv :: forall k v. HaskellType (ArraySort k v) -> Proxy v
      pv :: forall (k :: SMTSort) (v :: SMTSort).
HaskellType ('ArraySort k v) -> Proxy v
pv HaskellType ('ArraySort k v)
_ = forall {k} (t :: k). Proxy t
forall (t :: SMTSort). Proxy t
Proxy @v
  gcompare (StringValue HaskellType 'StringSort
x)(StringValue HaskellType 'StringSort
x')  = Ordering -> GOrdering a a
forall {k} {a :: k}. Ordering -> GOrdering a a
liftOrdering (Ordering -> GOrdering a a) -> Ordering -> GOrdering a a
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Text
HaskellType 'StringSort
x Text
HaskellType 'StringSort
x'
  gcompare (BoolValue HaskellType 'BoolSort
_) Value b
_                  = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
  gcompare Value a
_ (BoolValue HaskellType 'BoolSort
_)                  = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
  gcompare (IntValue HaskellType 'IntSort
_) Value b
_                   = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
  gcompare Value a
_ (IntValue HaskellType 'IntSort
_)                   = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
  gcompare (RealValue HaskellType 'RealSort
_) Value b
_                  = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
  gcompare Value a
_ (RealValue HaskellType 'RealSort
_)                  = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
  gcompare (BvValue HaskellType ('BvSort enc n)
_) Value b
_                    = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
  gcompare Value a
_ (BvValue HaskellType ('BvSort enc n)
_)                    = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
  gcompare (ArrayValue HaskellType ('ArraySort k v)
_) Value b
_                 = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
  gcompare Value a
_ (ArrayValue HaskellType ('ArraySort k v)
_)                 = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
  -- gcompare (StringValue _) _                = GLT
  -- gcompare _ (StringValue _)                = GGT

instance (KnownSMTSort t, Num (HaskellType t)) => Num (Value t) where
  fromInteger :: Integer -> Value t
fromInteger = HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue (HaskellType t -> Value t)
-> (Integer -> HaskellType t) -> Integer -> Value t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> HaskellType t
forall a. Num a => Integer -> a
fromInteger
  {-# INLINE fromInteger #-}
  Value t
x + :: Value t -> Value t -> Value t
+ Value t
y = HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue (HaskellType t -> Value t) -> HaskellType t -> Value t
forall a b. (a -> b) -> a -> b
$ Value t -> HaskellType t
forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue Value t
x HaskellType t -> HaskellType t -> HaskellType t
forall a. Num a => a -> a -> a
+ Value t -> HaskellType t
forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue Value t
y
  {-# INLINE (+) #-}
  Value t
x - :: Value t -> Value t -> Value t
- Value t
y = HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue (HaskellType t -> Value t) -> HaskellType t -> Value t
forall a b. (a -> b) -> a -> b
$ Value t -> HaskellType t
forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue Value t
x HaskellType t -> HaskellType t -> HaskellType t
forall a. Num a => a -> a -> a
- Value t -> HaskellType t
forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue Value t
y
  {-# INLINE (-) #-}
  Value t
x * :: Value t -> Value t -> Value t
* Value t
y = HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue (HaskellType t -> Value t) -> HaskellType t -> Value t
forall a b. (a -> b) -> a -> b
$ Value t -> HaskellType t
forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue Value t
x HaskellType t -> HaskellType t -> HaskellType t
forall a. Num a => a -> a -> a
* Value t -> HaskellType t
forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue Value t
y
  {-# INLINE (*) #-}
  negate :: Value t -> Value t
negate = HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue (HaskellType t -> Value t)
-> (Value t -> HaskellType t) -> Value t -> Value t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HaskellType t -> HaskellType t
forall a. Num a => a -> a
negate (HaskellType t -> HaskellType t)
-> (Value t -> HaskellType t) -> Value t -> HaskellType t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value t -> HaskellType t
forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue
  {-# INLINE negate #-}
  abs :: Value t -> Value t
abs = HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue (HaskellType t -> Value t)
-> (Value t -> HaskellType t) -> Value t -> Value t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HaskellType t -> HaskellType t
forall a. Num a => a -> a
abs (HaskellType t -> HaskellType t)
-> (Value t -> HaskellType t) -> Value t -> HaskellType t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value t -> HaskellType t
forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue
  {-# INLINE abs #-}
  signum :: Value t -> Value t
signum = HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue (HaskellType t -> Value t)
-> (Value t -> HaskellType t) -> Value t -> Value t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HaskellType t -> HaskellType t
forall a. Num a => a -> a
signum (HaskellType t -> HaskellType t)
-> (Value t -> HaskellType t) -> Value t -> HaskellType t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value t -> HaskellType t
forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue
  {-# INLINE signum #-}

instance Fractional (Value RealSort) where
  fromRational :: Rational -> Value 'RealSort
fromRational = Rational -> Value 'RealSort
HaskellType 'RealSort -> Value 'RealSort
RealValue (Rational -> Value 'RealSort)
-> (Rational -> Rational) -> Rational -> Value 'RealSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Fractional a => Rational -> a
fromRational
  {-# INLINE fromRational #-}
  (RealValue HaskellType 'RealSort
x) / :: Value 'RealSort -> Value 'RealSort -> Value 'RealSort
/ (RealValue HaskellType 'RealSort
y) = HaskellType 'RealSort -> Value 'RealSort
RealValue (HaskellType 'RealSort -> Value 'RealSort)
-> HaskellType 'RealSort -> Value 'RealSort
forall a b. (a -> b) -> a -> b
$ Rational
HaskellType 'RealSort
x Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
HaskellType 'RealSort
y
  {-# INLINE (/) #-}

instance Boolean (Value BoolSort) where
  bool :: Bool -> Value 'BoolSort
bool = Bool -> Value 'BoolSort
HaskellType 'BoolSort -> Value 'BoolSort
BoolValue
  {-# INLINE bool #-}
  (BoolValue HaskellType 'BoolSort
x) && :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort
&& (BoolValue HaskellType 'BoolSort
y) = HaskellType 'BoolSort -> Value 'BoolSort
BoolValue (HaskellType 'BoolSort -> Value 'BoolSort)
-> HaskellType 'BoolSort -> Value 'BoolSort
forall a b. (a -> b) -> a -> b
$ Bool
HaskellType 'BoolSort
x Bool -> Bool -> Bool
forall b. Boolean b => b -> b -> b
&& Bool
HaskellType 'BoolSort
y
  {-# INLINE (&&) #-}
  (BoolValue HaskellType 'BoolSort
x) || :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort
|| (BoolValue HaskellType 'BoolSort
y) = HaskellType 'BoolSort -> Value 'BoolSort
BoolValue (HaskellType 'BoolSort -> Value 'BoolSort)
-> HaskellType 'BoolSort -> Value 'BoolSort
forall a b. (a -> b) -> a -> b
$ Bool
HaskellType 'BoolSort
x Bool -> Bool -> Bool
forall b. Boolean b => b -> b -> b
|| Bool
HaskellType 'BoolSort
y
  {-# INLINE (||) #-}
  not :: Value 'BoolSort -> Value 'BoolSort
not (BoolValue HaskellType 'BoolSort
x) = HaskellType 'BoolSort -> Value 'BoolSort
BoolValue (HaskellType 'BoolSort -> Value 'BoolSort)
-> HaskellType 'BoolSort -> Value 'BoolSort
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
forall b. Boolean b => b -> b
not Bool
HaskellType 'BoolSort
x
  {-# INLINE not #-}
  xor :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort
xor (BoolValue HaskellType 'BoolSort
x) (BoolValue HaskellType 'BoolSort
y) = HaskellType 'BoolSort -> Value 'BoolSort
BoolValue (HaskellType 'BoolSort -> Value 'BoolSort)
-> HaskellType 'BoolSort -> Value 'BoolSort
forall a b. (a -> b) -> a -> b
$ Bool
HaskellType 'BoolSort
x Bool -> Bool -> Bool
forall b. Boolean b => b -> b -> b
`xor` Bool
HaskellType 'BoolSort
y
  {-# INLINE xor #-}

-- | Unwraps a Haskell-value from the SMT-Context-'Value'.
unwrapValue :: Value t -> HaskellType t
unwrapValue :: forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue (IntValue  HaskellType 'IntSort
v)   = HaskellType t
HaskellType 'IntSort
v
unwrapValue (RealValue HaskellType 'RealSort
v)   = HaskellType t
HaskellType 'RealSort
v
unwrapValue (BoolValue HaskellType 'BoolSort
v)   = HaskellType t
HaskellType 'BoolSort
v
unwrapValue (BvValue   HaskellType ('BvSort enc n)
v)   = HaskellType t
HaskellType ('BvSort enc n)
v
unwrapValue (ArrayValue HaskellType ('ArraySort k v)
v)  = HaskellType t
HaskellType ('ArraySort k v)
v
unwrapValue (StringValue HaskellType 'StringSort
v) = HaskellType t
HaskellType 'StringSort
v
{-# INLINE unwrapValue #-}

-- | Wraps a Haskell-value into the SMT-Context-'Value'.
wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t
wrapValue :: forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue = case forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t of
  SSMTSort t
SIntSort       -> HaskellType t -> Value t
HaskellType 'IntSort -> Value 'IntSort
IntValue
  SSMTSort t
SRealSort      -> HaskellType t -> Value t
HaskellType 'RealSort -> Value 'RealSort
RealValue
  SSMTSort t
SBoolSort      -> HaskellType t -> Value t
HaskellType 'BoolSort -> Value 'BoolSort
BoolValue
  SBvSort Proxy enc
_ Proxy n
_    -> HaskellType t -> Value t
HaskellType ('BvSort enc n) -> Value ('BvSort enc n)
forall (k :: BvEnc) (v :: Nat).
(KnownBvEnc k, KnownNat v) =>
HaskellType ('BvSort k v) -> Value ('BvSort k v)
BvValue
  SArraySort Proxy k
_ Proxy v
_ -> HaskellType t -> Value t
HaskellType ('ArraySort k v) -> Value ('ArraySort k v)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k),
 Ord (HaskellType v)) =>
HaskellType ('ArraySort k v) -> Value ('ArraySort k v)
ArrayValue
  SSMTSort t
SStringSort    -> HaskellType t -> Value t
HaskellType 'StringSort -> Value 'StringSort
StringValue
{-# INLINE wrapValue #-}