Language.Hasmtlib.Type.SMTSort

This module provides the data-type SMTSort and some singleton-operations for it.

The type SMTSort is only used as promoted type (data-kind) in dependent-like contexts such as GADTs.

Type

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 BvEnc Nat

Sort of BitVec with type of encoding enc and length n

ArraySort SMTSort SMTSort

Sort of Array with indices k and values v

StringSort

Sort of String

Instances

GNFData Expr

Defined in Language.Hasmtlib.Type.Expr

Methods

grnf :: forall (a :: k). Expr a -> ()

GCompare Expr

Defined in Language.Hasmtlib.Type.Expr

Methods

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

GCompare SSMTSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

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

GCompare Value

Defined in Language.Hasmtlib.Type.Value

Methods

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

GEq Expr

Defined in Language.Hasmtlib.Type.Expr

Methods

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

GEq SSMTSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

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

GEq Value

Defined in Language.Hasmtlib.Type.Value

Methods

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

Uniplate1 Expr '[KnownSMTSort]

Caution for quantified expressions: uniplate1 will only be applied if quantification has taken place already.

Defined in Language.Hasmtlib.Type.Expr

Methods

uniplate1 :: forall m (b :: k). (Applicative m, AllC '[KnownSMTSort] b) => (forall (a :: k). AllC '[KnownSMTSort] a => Expr a -> m (Expr a)) -> Expr b -> m (Expr 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 = Rational

HaskellType BoolSort = Bool

HaskellType (BvSort enc n) = Bitvec enc n

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

HaskellType StringSort = Text

Singleton

data SSMTSort (t :: SMTSort) where

Singleton for SMTSort.

Constructors

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

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.Internal.Render

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

KnownSMTSort 'StringSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort 'StringSort

Uniplate1 Expr '[KnownSMTSort]

Caution for quantified expressions: uniplate1 will only be applied if quantification has taken place already.

Defined in Language.Hasmtlib.Type.Expr

Methods

uniplate1 :: forall m (b :: k). (Applicative m, AllC '[KnownSMTSort] b) => (forall (a :: k). AllC '[KnownSMTSort] a => Expr a -> m (Expr a)) -> Expr b -> m (Expr b)

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

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort ('ArraySort k v)

(KnownBvEnc enc, KnownNat n) => KnownSMTSort ('BvSort enc n)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort ('BvSort enc n)

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

Wrapper for sortSing which takes a Proxy.

Existential

type SomeKnownSMTSort f = Some1 ((~) f) KnownSMTSort

An existential wrapper that hides some known SMTSort.