Language.SMTLib2.Internals.Type

Documentation

data Type

Describes the kind of all SMT types. It is only used in promoted form, for a concrete representation see Repr.

Constructors

BoolType

IntType

RealType

BitVecType Nat

ArrayType [Type] Type

forall a . DataType a

Instances

GCompare Type NumRepr

GCompare Type Repr

GCompare Type ConcreteValue

GCompare Type NoVar

GEq Type NumRepr

GEq Type Repr

GEq Type ConcreteValue

GEq Type NoVar

GShow Type NumRepr

GShow Type Repr

GShow Type ConcreteValue

GShow Type NoVar

GCompare ((,) [Type] *) con => GCompare Type (Value con)

Ord v => GCompare Type (UntypedVar v)

GEq ((,) [Type] *) con => GEq Type (Value con)

Eq v => GEq Type (UntypedVar v)

GShow ((,) [Type] *) con => GShow Type (Value con)

Show v => GShow Type (UntypedVar v)

(GCompare Type v, GCompare Type e) => GCompare Type (LetBinding v e)

(GEq Type v, GEq Type e) => GEq Type (LetBinding v e)

(GCompare Type v, GCompare Type qv, GCompare ((,) [Type] Type) fun, GCompare ((,) [Type] *) con, GCompare ((,) * Type) field, GCompare Type fv, GCompare Type lv, GCompare Type e) => GCompare Type (Expression v qv fun con field fv lv e)

(GEq Type v, GEq Type qv, GEq ((,) [Type] Type) fun, GEq ((,) [Type] *) con, GEq ((,) * Type) field, GEq Type fv, GEq Type lv, GEq Type e) => GEq Type (Expression v qv fun con field fv lv e)

(GShow Type v, GShow Type qv, GShow ((,) [Type] Type) fun, GShow ((,) [Type] *) con, GShow ((,) * Type) field, GShow Type fv, GShow Type lv, GShow Type e) => GShow Type (Expression v qv fun con field fv lv e)

HasMonad (m (List Type e tp))

GCompare ((,) [Type] *) NoCon

GCompare ((,) [Type] Type) FunRepr

GCompare ((,) [Type] Type) NoFun

GCompare ((,) * Type) NoField

GEq ((,) [Type] *) NoCon

GEq ((,) [Type] Type) FunRepr

GEq ((,) [Type] Type) NoFun

GEq ((,) * Type) NoField

GShow ((,) [[Type]] *) Datatype

GShow ((,) [Type] *) NoCon

GShow ((,) [Type] Type) NoFun

GShow ((,) * Type) NoField

Ord v => GCompare ((,) [Type] *) (UntypedCon v)

Ord v => GCompare ((,) [Type] Type) (UntypedFun v)

Ord v => GCompare ((,) * Type) (UntypedField v)

Eq v => GEq ((,) [Type] *) (UntypedCon v)

Eq v => GEq ((,) [Type] Type) (UntypedFun v)

Eq v => GEq ((,) * Type) (UntypedField v)

Show v => GShow ((,) [Type] *) (UntypedCon v)

Show v => GShow ((,) [Type] Type) (UntypedFun v)

Show v => GShow ((,) * Type) (UntypedField v)

(GCompare ((,) [Type] Type) fun, GCompare ((,) [Type] *) con, GCompare ((,) * Type) field) => GCompare ((,) [Type] Type) (Function fun con field)

(GEq ((,) [Type] Type) fun, GEq ((,) [Type] *) con, GEq ((,) * Type) field) => GEq ((,) [Type] Type) (Function fun con field)

(GShow ((,) [Type] Type) fun, GShow ((,) [Type] *) con, GShow ((,) * Type) field) => GShow ((,) [Type] Type) (Function fun con field)

HasMonad (List Type e tp)

(Same ((:) Type tp tps), (~) Type tp (SameType ((:) Type tp tps))) => Same ((:) Type tp ((:) Type tp tps))

Same ((:) Type tp ([] Type))

Unlift ((:) Type t2 ts) idx => Unlift ((:) Type t1 ((:) Type t2 ts)) idx

Unlift ((:) Type tp ([] Type)) idx

type MonadResult (m (List Type e tp)) = List Type e tp

type MatchMonad (m (List Type e tp)) m' = (~) (* -> *) m m'

type MonadResult (List Type e tp) = List Type e tp

type MatchMonad (List Type e tp) m = ()

type family Lifted tps idx :: [Type]

Equations

Lifted `[]` idx = `[]`

Lifted (tp : tps) idx = ArrayType idx tp : Lifted tps idx

class Unlift tps idx where

Methods

unliftType :: List Repr (Lifted tps idx) -> (List Repr tps, List Repr idx)

unliftTypeWith :: List Repr (Lifted tps idx) -> List Repr tps -> List Repr idx

Instances

Unlift ((:) Type t2 ts) idx => Unlift ((:) Type t1 ((:) Type t2 ts)) idx

Unlift ((:) Type tp ([] Type)) idx

type family Fst a :: p

Equations

Fst `(x, y)` = x

type family Snd a :: q

Equations

Snd `(x, y)` = y

class (Typeable t, Typeable (DatatypeSig t), Show t, Ord t) => IsDatatype t where

Associated Types

type DatatypeSig t :: [[Type]]

type TypeCollectionSig t :: [([[Type]], *)]

Methods

getDatatype :: e t -> Datatype `(DatatypeSig t, t)`

getTypeCollection :: e t -> TypeCollection (TypeCollectionSig t)

getConstructor :: t -> Constrs con (DatatypeSig t) t -> (forall arg. con `(arg, t)` -> List ConcreteValue arg -> a) -> a

type TypeCollection sigs = Datatypes Datatype sigs

data Datatype sig

Constructors

Datatype

Fields

datatypeName :: String

constructors :: Constrs Constr (Fst sig) (Snd sig)

Instances

Show (Datatype sig)

GShow ((,) [[Type]] *) Datatype

data Constr sig

Constructors

Constr

Fields

conName :: String

conFields :: List (Field (Snd sig)) (Fst sig)

construct :: List ConcreteValue (Fst sig) -> Snd sig

conTest :: Snd sig -> Bool

data Field a t

Constructors

Field

Fields

fieldName :: String

fieldType :: Repr t

fieldGet :: a -> ConcreteValue t

data Value con a where

Constructors

BoolValue :: Bool -> Value con BoolType

IntValue :: Integer -> Value con IntType

RealValue :: Rational -> Value con RealType

BitVecValue :: Integer -> Natural n -> Value con (BitVecType n)

ConstrValue :: (Typeable con, IsDatatype t) => con `(arg, t)` -> List (Value con) arg -> Value con (DataType t)

Instances

GCompare ((,) [Type] *) con => GCompare Type (Value con)

GEq ((,) [Type] *) con => GEq Type (Value con)

GShow ((,) [Type] *) con => GShow Type (Value con)

GetType (Value con)

GEq ((,) [Type] *) con => Eq (Value con t)

GShow ((,) [Type] *) con => Show (Value con tp)

data ConcreteValue a where

Constructors

BoolValueC :: Bool -> ConcreteValue BoolType

IntValueC :: Integer -> ConcreteValue IntType

RealValueC :: Rational -> ConcreteValue RealType

BitVecValueC :: Integer -> Natural n -> ConcreteValue (BitVecType n)

ConstrValueC :: IsDatatype t => t -> ConcreteValue (DataType t)

Instances

GetType ConcreteValue

GCompare Type ConcreteValue

GEq Type ConcreteValue

GShow Type ConcreteValue

Show (ConcreteValue t)

data AnyValue con

Constructors

forall t . AnyValue (Value con t)

data Repr t where

A concrete representation of an SMT type. For aesthetic reasons, it's recommended to use the functions bool, int, real, bitvec or array.

Constructors

BoolRepr :: Repr BoolType

IntRepr :: Repr IntType

RealRepr :: Repr RealType

BitVecRepr :: Natural n -> Repr (BitVecType n)

ArrayRepr :: List Repr idx -> Repr val -> Repr (ArrayType idx val)

DataRepr :: IsDatatype dt => Datatype `(DatatypeSig dt, dt)` -> Repr (DataType dt)

Instances

GetType Repr

GCompare Type Repr

GEq Type Repr

GShow Type Repr

Eq (Repr tp)

Ord (Repr tp)

Show (Repr t)

data NumRepr t where

Constructors

NumInt :: NumRepr IntType

NumReal :: NumRepr RealType

Instances

GCompare Type NumRepr

GEq Type NumRepr

GShow Type NumRepr

Show (NumRepr t)

data Constrs con a t where

Constructors

NoCon :: Constrs con `[]` t

ConsCon :: con `(arg, dt)` -> Constrs con args dt -> Constrs con (arg : args) dt

data Datatypes dts sigs where

Constructors

NoDts :: Datatypes dts `[]`

ConsDts :: IsDatatype dt => dts `(DatatypeSig dt, dt)` -> Datatypes dts sigs -> Datatypes dts (`(DatatypeSig dt, dt)` : sigs)

data FunRepr sig where

Constructors

FunRepr :: List Repr arg -> Repr tp -> FunRepr `(arg, tp)`

Instances

GCompare ((,) [Type] Type) FunRepr

GEq ((,) [Type] Type) FunRepr

class GetType v where

Methods

getType :: v tp -> Repr tp

Instances

GetType Repr

GetType ConcreteValue

GetType NoVar

GetType (Value con)

GetType (UntypedVar v)

(GetType var, GetType qvar, GetFunType fun, GetConType con, GetFieldType field, GetType farg, GetType lvar) => GetType (SMTExpr var qvar fun con field farg lvar)

(GetType v, GetType qv, GetFunType fun, GetConType con, GetFieldType field, GetType fv, GetType lv, GetType e) => GetType (Expression v qv fun con field fv lv e)

class GetFunType fun where

Methods

getFunType :: fun `(arg, res)` -> (List Repr arg, Repr res)

Instances

GetFunType NoFun

GetFunType (UntypedFun v)

(GetFunType fun, GetConType con, GetFieldType field) => GetFunType (Function fun con field)

class GetConType con where

Methods

getConType :: IsDatatype dt => con `(arg, dt)` -> (List Repr arg, Datatype `(DatatypeSig dt, dt)`)

Instances

GetConType NoCon

GetConType (UntypedCon v)

class GetFieldType field where

Methods

getFieldType :: IsDatatype dt => field `(dt, tp)` -> (Datatype `(DatatypeSig dt, dt)`, Repr tp)

Instances

GetFieldType NoField

GetFieldType (UntypedField v)

bool :: Repr BoolType

A representation of the SMT Bool type. Holds the values true or false.

int :: Repr IntType

real :: Repr RealType

bitvec :: Natural bw -> Repr (BitVecType bw)

array :: List Repr idx -> Repr el -> Repr (ArrayType idx el)

reifyType :: Type -> (forall tp. Repr tp -> a) -> a

Get a concrete representation for a type.

mapValue :: (Monad m, Typeable con2) => (forall arg dt. con1 `(arg, dt)` -> m (con2 `(arg, dt)`)) -> Value con1 a -> m (Value con2 a)

findConstrByName :: String -> Datatype `(cons, dt)` -> (forall arg. Constr `(arg, dt)` -> a) -> a

valueToConcrete :: Monad m => (forall arg tp. IsDatatype tp => con `(arg, tp)` -> List ConcreteValue arg -> m tp) -> Value con t -> m (ConcreteValue t)

valueFromConcrete :: (Monad m, Typeable con) => (forall tp a. IsDatatype tp => tp -> (forall arg. con `(arg, tp)` -> List ConcreteValue arg -> m a) -> m a) -> ConcreteValue t -> m (Value con t)

valueType :: Value con tp -> Repr tp

valueTypeC :: ConcreteValue tp -> Repr tp

liftType :: List Repr tps -> List Repr idx -> List Repr (Lifted tps idx)

numRepr :: NumRepr tp -> Repr tp

asNumRepr :: Repr tp -> Maybe (NumRepr tp)

getTypes :: GetType e => List e tps -> List Repr tps