{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Language.Hasmtlib.Type.SMTSort
(
SMTSort(..)
, HaskellType
, SSMTSort(..)
, KnownSMTSort(..), sortSing'
, SomeKnownSMTSort
)
where
import Language.Hasmtlib.Type.Bitvec
import Language.Hasmtlib.Type.ArrayMap
import Data.GADT.Compare
import Data.Kind
import Data.Proxy
import Data.Some.Constraint
import qualified Data.Text as Text
import Control.Lens
import GHC.TypeLits
data SMTSort =
BoolSort
| IntSort
| RealSort
| BvSort BvEnc Nat
| ArraySort SMTSort SMTSort
| StringSort
type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where
HaskellType IntSort = Integer
HaskellType RealSort = Rational
HaskellType BoolSort = Bool
HaskellType (BvSort enc n) = Bitvec enc n
HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)
HaskellType StringSort = Text.Text
data SSMTSort (t :: SMTSort) where
SIntSort :: SSMTSort IntSort
SRealSort :: SSMTSort RealSort
SBoolSort :: SSMTSort BoolSort
SBvSort :: (KnownBvEnc enc, KnownNat n) => Proxy enc -> Proxy n -> SSMTSort (BvSort enc n)
SArraySort :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)
SStringSort :: SSMTSort StringSort
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 enc
enc Proxy n
n) (SBvSort Proxy enc
emc 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
Maybe (n :~: n)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
Just n :~: n
Refl -> 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 (Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
enc) (Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
emc) of
Maybe (enc :~: enc)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
Just enc :~: enc
Refl -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
geq (SArraySort Proxy k
k Proxy v
v) (SArraySort Proxy k
k' Proxy v
v') = case SSMTSort k -> SSMTSort k -> Maybe (k :~: k)
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 (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
Maybe (k :~: k)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
Just k :~: k
Refl -> case SSMTSort v -> SSMTSort v -> Maybe (v :~: v)
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 (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
Maybe (v :~: v)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
Just v :~: v
Refl -> (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
SStringSort SSMTSort b
SStringSort = (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
_ 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 enc
enc Proxy n
n) (SBvSort Proxy enc
emc 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 -> 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 (Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
enc) (Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
emc) of
GOrdering enc enc
GLT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
GOrdering enc enc
GEQ -> GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
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 (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
SStringSort SSMTSort b
SStringSort = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
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
gcompare SSMTSort a
SStringSort SSMTSort b
_ = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
gcompare SSMTSort a
_ SSMTSort b
SStringSort = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
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 (KnownBvEnc enc, KnownNat n) => KnownSMTSort (BvSort enc n) where sortSing :: SSMTSort ('BvSort enc n)
sortSing = Proxy enc -> Proxy n -> SSMTSort ('BvSort enc n)
forall (k :: BvEnc) (v :: Nat).
(KnownBvEnc k, KnownNat v) =>
Proxy k -> Proxy v -> SSMTSort ('BvSort k v)
SBvSort (forall {k} (t :: k). Proxy t
forall (t :: BvEnc). Proxy t
Proxy @enc) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => 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),
Ord (HaskellType v)) =>
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)
instance KnownSMTSort StringSort where sortSing :: SSMTSort 'StringSort
sortSing = SSMTSort 'StringSort
SStringSort
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
type SomeKnownSMTSort f = Some1 ((~) f) KnownSMTSort