Language.Hasmtlib.Type.SMTSort

Documentation

data SMTSort

Sorts in SMTLib2 - used as promoted type (data-kind).

Constructors

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

Instances

GCompare SSMTSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

gcompare :: forall (a :: k) (b :: k). SSMTSort a -> SSMTSort b -> GOrdering a b

GEq SSMTSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

geq :: forall (a :: k) (b :: k). SSMTSort a -> SSMTSort b -> Maybe (a :~: b)

type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where ...

Injective type-family that computes the Haskell Type of an SMTSort.

Equations

HaskellType IntSort = Integer

HaskellType RealSort = Double

HaskellType BoolSort = Bool

HaskellType (BvSort n) = Bitvec n

HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)

data SSMTSort (t :: SMTSort) where

Singleton for SMTSort.

Constructors

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)

Instances

GCompare SSMTSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

gcompare :: forall (a :: k) (b :: k). SSMTSort a -> SSMTSort b -> GOrdering a b

GEq SSMTSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

geq :: forall (a :: k) (b :: k). SSMTSort a -> SSMTSort b -> Maybe (a :~: b)

Show (SSMTSort t)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

showsPrec :: Int -> SSMTSort t -> ShowS

show :: SSMTSort t -> String

showList :: [SSMTSort t] -> ShowS

Eq (SSMTSort t)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

(==) :: SSMTSort t -> SSMTSort t -> Bool

(/=) :: SSMTSort t -> SSMTSort t -> Bool

Ord (SSMTSort t)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

compare :: SSMTSort t -> SSMTSort t -> Ordering

(<) :: SSMTSort t -> SSMTSort t -> Bool

(<=) :: SSMTSort t -> SSMTSort t -> Bool

(>) :: SSMTSort t -> SSMTSort t -> Bool

(>=) :: SSMTSort t -> SSMTSort t -> Bool

max :: SSMTSort t -> SSMTSort t -> SSMTSort t

min :: SSMTSort t -> SSMTSort t -> SSMTSort t

Render (SSMTSort t)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

render :: SSMTSort t -> Builder

class KnownSMTSort (t :: SMTSort) where

Compute singleton SSMTSort from it's promoted type SMTSort.

Methods

sortSing :: SSMTSort t

Instances

KnownSMTSort 'BoolSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort 'BoolSort

KnownSMTSort 'IntSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort 'IntSort

KnownSMTSort 'RealSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort 'RealSort

KnownNat n => KnownSMTSort ('BvSort n)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort ('BvSort n)

(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort ('ArraySort k v)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort ('ArraySort k v)

sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t

Wrapper for sortSing which takes a Proxy

type family AllC cs k :: Constraint where ...

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)

Equations

AllC '[] k = ()

AllC (c ': cs) k = (c k, AllC cs k)

data SomeSMTSort cs f where

An existential wrapper that hides some SMTSort and a list of Constraints holding for it.

Constructors

SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f