Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Language.Hasmtlib.Type.SMTSort
Synopsis
- data SMTSort
- type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where ...
- data SSMTSort (t :: SMTSort) where
- class KnownSMTSort (t :: SMTSort) where
- sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t
- type family AllC cs k :: Constraint where ...
- data SomeSMTSort cs f where
- SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f
Documentation
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 |
type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where ... Source #
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 Source #
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 Source # | |
GEq SSMTSort Source # | |
Show (SSMTSort t) Source # | |
Eq (SSMTSort t) Source # | |
Ord (SSMTSort t) Source # | |
Defined in Language.Hasmtlib.Type.SMTSort | |
Render (SSMTSort t) Source # | |
class KnownSMTSort (t :: SMTSort) where Source #
Instances
KnownSMTSort 'BoolSort Source # | |
KnownSMTSort 'IntSort Source # | |
KnownSMTSort 'RealSort Source # | |
KnownNat n => KnownSMTSort ('BvSort n) Source # | |
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort ('ArraySort k v) Source # | |
sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t Source #
type family AllC cs k :: Constraint where ... Source #
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)
data SomeSMTSort cs f where Source #
An existential wrapper that hides some SMTSort
and a list of Constraint
s holding for it.
Constructors
SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f |