{-# LANGUAGE UndecidableInstances #-}

module Language.Hasmtlib.Type.Value
( Value(..)
, wrapValue, unwrapValue
)
where

import Language.Hasmtlib.Type.SMTSort
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     :: KnownNat n => HaskellType (BvSort n) -> Value (BvSort 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 Double
HaskellType 'RealSort
x Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
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 n)
x) (BvValue HaskellType ('BvSort n)
y)       = case Bitvec n -> Bitvec 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 n
HaskellType ('BvSort n)
x Bitvec n
HaskellType ('BvSort n)
y of
    OrderingI n n
EQI -> if Bitvec n
HaskellType ('BvSort n)
x Bitvec n -> Bitvec n -> Bool
forall a. Eq a => a -> a -> Bool
== Bitvec n
HaskellType ('BvSort 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
$ Double -> Double -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Double
HaskellType 'RealSort
x Double
HaskellType 'RealSort
x'
  gcompare (BvValue HaskellType ('BvSort n)
x) (BvValue HaskellType ('BvSort n)
x')         = case Bitvec n -> Bitvec 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 n
HaskellType ('BvSort n)
x Bitvec n
HaskellType ('BvSort n)
x' of
    OrderingI n n
LTI -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
    OrderingI n n
EQI -> 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 n -> Bitvec n -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Bitvec n
HaskellType ('BvSort n)
x Bitvec n
HaskellType ('BvSort n)
x'
    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 n)
_) Value b
_                    = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
  gcompare Value a
_ (BvValue HaskellType ('BvSort 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

-- | 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 n)
v)   = HaskellType t
HaskellType ('BvSort 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
{-# INLINEABLE 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 n
_      -> HaskellType t -> Value t
HaskellType ('BvSort n) -> Value ('BvSort n)
forall (k :: Nat).
KnownNat k =>
HaskellType ('BvSort k) -> Value ('BvSort k)
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
{-# INLINEABLE wrapValue #-}