{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}

module Language.Hasmtlib.Type.SMTSort where

import Language.Hasmtlib.Internal.Bitvec
import Language.Hasmtlib.Internal.Render
import Language.Hasmtlib.Type.ArrayMap
import Data.GADT.Compare
import Data.Kind
import Data.Proxy
import Data.ByteString.Builder
import Control.Lens
import GHC.TypeLits

-- | Sorts in SMTLib2 - used as promoted type (data-kind).
data SMTSort =
    BoolSort                      -- ^ Sort of Bool
  | IntSort                       -- ^ Sort of Int
  | RealSort                      -- ^ Sort of Real
  | BvSort Nat                    -- ^ Sort of BitVec with length n
  | ArraySort SMTSort SMTSort     -- ^ Sort of Array with indices k and values v

-- | Injective type-family that computes the Haskell 'Type' of an 'SMTSort'.
type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where
  HaskellType IntSort         = Integer
  HaskellType RealSort        = Double
  HaskellType BoolSort        = Bool
  HaskellType (BvSort n)      = Bitvec n
  HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)

-- | Singleton for 'SMTSort'.
data SSMTSort (t :: SMTSort) where
  SIntSort   :: SSMTSort IntSort
  SRealSort  :: SSMTSort RealSort
  SBoolSort  :: SSMTSort BoolSort
  SBvSort    :: KnownNat n => Proxy n -> SSMTSort (BvSort n)
  SArraySort :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)

deriving instance Show (SSMTSort t)
deriving instance Eq   (SSMTSort t)
deriving instance Ord  (SSMTSort t)

instance GEq SSMTSort where
  geq :: forall (a :: SMTSort) (b :: SMTSort).
SSMTSort a -> SSMTSort b -> Maybe (a :~: b)
geq SSMTSort a
SIntSort SSMTSort b
SIntSort       = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geq SSMTSort a
SRealSort SSMTSort b
SRealSort     = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geq SSMTSort a
SBoolSort SSMTSort b
SBoolSort     = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geq (SBvSort Proxy n
n) (SBvSort Proxy n
m) = case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat Proxy n
n Proxy n
m of
    Just n :~: n
Refl -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    Maybe (n :~: n)
Nothing   -> Maybe (a :~: b)
forall a. Maybe a
Nothing
  geq SSMTSort a
_ SSMTSort b
_                     = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance GCompare SSMTSort where
  gcompare :: forall (a :: SMTSort) (b :: SMTSort).
SSMTSort a -> SSMTSort b -> GOrdering a b
gcompare SSMTSort a
SBoolSort SSMTSort b
SBoolSort     = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
  gcompare SSMTSort a
SIntSort SSMTSort b
SIntSort       = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
  gcompare SSMTSort a
SRealSort SSMTSort b
SRealSort     = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
  gcompare (SBvSort Proxy n
n) (SBvSort Proxy n
m) = case Proxy n -> Proxy 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 Proxy n
n Proxy n
m of
    OrderingI n n
LTI -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
    OrderingI n n
EQI -> GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
    OrderingI n n
GTI -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
  gcompare (SArraySort Proxy k
k Proxy v
v) (SArraySort Proxy k
k' Proxy v
v') = 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' Proxy k
k) (Proxy k -> SSMTSort k
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Proxy k
k') 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' Proxy v
v) (Proxy v -> SSMTSort v
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Proxy v
v') of
      GOrdering v v
GLT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
      GOrdering v v
GEQ -> GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
      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
  gcompare SSMTSort a
SBoolSort SSMTSort b
_        = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
  gcompare SSMTSort a
_ SSMTSort b
SBoolSort        = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
  gcompare SSMTSort a
SIntSort SSMTSort b
_         = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
  gcompare SSMTSort a
_ SSMTSort b
SIntSort         = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
  gcompare SSMTSort a
SRealSort SSMTSort b
_        = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
  gcompare SSMTSort a
_ SSMTSort b
SRealSort        = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
  gcompare (SArraySort Proxy k
_ Proxy v
_) SSMTSort b
_ = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
  gcompare SSMTSort a
_ (SArraySort Proxy k
_ Proxy v
_) = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT

-- | Compute singleton 'SSMTSort' from it's promoted type 'SMTSort'.
class    KnownSMTSort (t :: SMTSort)           where sortSing :: SSMTSort t
instance KnownSMTSort IntSort                  where sortSing :: SSMTSort 'IntSort
sortSing = SSMTSort 'IntSort
SIntSort
instance KnownSMTSort RealSort                 where sortSing :: SSMTSort 'RealSort
sortSing = SSMTSort 'RealSort
SRealSort
instance KnownSMTSort BoolSort                 where sortSing :: SSMTSort 'BoolSort
sortSing = SSMTSort 'BoolSort
SBoolSort
instance KnownNat n => KnownSMTSort (BvSort n) where sortSing :: SSMTSort ('BvSort n)
sortSing = Proxy n -> SSMTSort ('BvSort n)
forall (k :: Nat). KnownNat k => Proxy k -> SSMTSort ('BvSort k)
SBvSort (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort (ArraySort k v) where
   sortSing :: SSMTSort ('ArraySort k v)
sortSing = Proxy k -> Proxy v -> SSMTSort ('ArraySort k v)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Proxy k -> Proxy v -> SSMTSort ('ArraySort k v)
SArraySort (forall {k} (t :: k). Proxy t
forall (t :: SMTSort). Proxy t
Proxy @k) (forall {k} (t :: k). Proxy t
forall (t :: SMTSort). Proxy t
Proxy @v)

-- | Wrapper for 'sortSing' which takes a 'Proxy'
sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t
sortSing' :: forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' prxy t
_ = forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t

-- | AllC ensures that a list of constraints is applied to a poly-kinded 'Type' k
--
-- @
-- AllC '[]       k = ()
-- AllC (c ': cs) k = (c k, AllC cs k)
-- @
type AllC :: [k -> Constraint] -> k -> Constraint
type family AllC cs k :: Constraint where
  AllC '[]       k = ()
  AllC (c ': cs) k = (c k, AllC cs k)

-- | An existential wrapper that hides some 'SMTSort' and a list of 'Constraint's holding for it.
data SomeSMTSort cs f where
  SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f

instance Render (SSMTSort t) where
  render :: SSMTSort t -> Builder
render SSMTSort t
SBoolSort   = Builder
"Bool"
  render SSMTSort t
SIntSort    = Builder
"Int"
  render SSMTSort t
SRealSort   = Builder
"Real"
  render (SBvSort Proxy n
p) = Builder -> Builder -> Integer -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"_" (Builder
"BitVec" :: Builder) (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Proxy n
p)
  render (SArraySort Proxy k
k Proxy v
v) = Builder -> SSMTSort k -> SSMTSort v -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"Array" (Proxy k -> SSMTSort k
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Proxy k
k) (Proxy v -> SSMTSort v
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Proxy v
v)
  {-# INLINEABLE render #-}