Safe Haskell	None
Language	Haskell98

Language.SMTLib2.Internals.Type

Synopsis

Documentation

data Type Source #

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
DataType a [Type]
ParameterType Nat

Instances

GCompare Type NumRepr Source #
Methods gcompare :: f a -> f b -> GOrdering NumRepr a b #
GCompare Type Repr Source #
Methods gcompare :: f a -> f b -> GOrdering Repr a b #
GCompare Type Value Source #
Methods gcompare :: f a -> f b -> GOrdering Value a b #
GCompare Type NoVar #
Methods gcompare :: f a -> f b -> GOrdering NoVar a b #
GEq Type NumRepr Source #
Methods geq :: f a -> f b -> Maybe ((NumRepr := a) b) #
GEq Type Repr Source #
Methods geq :: f a -> f b -> Maybe ((Repr := a) b) #
GEq Type Value Source #
Methods geq :: f a -> f b -> Maybe ((Value := a) b) #
GEq Type NoVar #
Methods geq :: f a -> f b -> Maybe ((NoVar := a) b) #
GShow Type NumRepr Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
GShow Type Repr Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
GShow Type Value Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
GShow Type NoVar #
Methods gshowsPrec :: Int -> t a -> ShowS #
GCompare Type (Field (DynamicValue l sig)) Source #
Methods gcompare :: f a -> f b -> GOrdering (Field (DynamicValue l sig)) a b #
GCompare ([Type], Type) fun => GCompare Type (EvalResult fun) #
Methods gcompare :: f a -> f b -> GOrdering (EvalResult fun) a b #
Ord v => GCompare Type (UntypedVar v) #
Methods gcompare :: f a -> f b -> GOrdering (UntypedVar v) a b #
GCompare Type (ValueExt m) #
Methods gcompare :: f a -> f b -> GOrdering (ValueExt m) a b #
GEq Type (Field (DynamicValue l sig)) Source #
Methods geq :: f a -> f b -> Maybe ((Field (DynamicValue l sig) := a) b) #
GEq ([Type], Type) fun => GEq Type (EvalResult fun) #
Methods geq :: f a -> f b -> Maybe ((EvalResult fun := a) b) #
Eq v => GEq Type (UntypedVar v) #
Methods geq :: f a -> f b -> Maybe ((UntypedVar v := a) b) #
GEq Type (ValueExt m) #
Methods geq :: f a -> f b -> Maybe ((ValueExt m := a) b) #
GShow ([Type], Type) fun => GShow Type (EvalResult fun) #
Methods gshowsPrec :: Int -> t a -> ShowS #
Show v => GShow Type (UntypedVar v) #
Methods gshowsPrec :: Int -> t a -> ShowS #
GShow Type (ValueExt m) #
Methods gshowsPrec :: Int -> t a -> ShowS #
(GCompare Type v, GCompare Type e) => GCompare Type (LetBinding v e) #
Methods gcompare :: f a -> f b -> GOrdering (LetBinding v e) a b #
(GEq Type v, GEq Type e) => GEq Type (LetBinding v e) #
Methods geq :: f a -> f b -> Maybe ((LetBinding v e := a) b) #
GShow ([Type], Type) fun => GShow Type (ArrayModel fun idx) #
Methods gshowsPrec :: Int -> t a -> ShowS #
(GCompare Type v, GCompare Type qv, GCompare ([Type], Type) fun, GCompare Type fv, GCompare Type lv, GCompare Type e) => GCompare Type (Expression v qv fun fv lv e) #
Methods gcompare :: f a -> f b -> GOrdering (Expression v qv fun fv lv e) a b #
(GEq Type v, GEq Type qv, GEq ([Type], Type) fun, GEq Type fv, GEq Type lv, GEq Type e) => GEq Type (Expression v qv fun fv lv e) #
Methods geq :: f a -> f b -> Maybe ((Expression v qv fun fv lv e := a) b) #
(GShow Type v, GShow Type qv, GShow ([Type], Type) fun, GShow Type fv, GShow Type lv, GShow Type e) => GShow Type (Expression v qv fun fv lv e) #
Methods gshowsPrec :: Int -> t a -> ShowS #
HasMonad (m (List Type e tp)) Source #
Associated Types type MatchMonad (m (List Type e tp)) (m :: * -> ) :: Constraint Source # type MonadResult (m (List Type e tp)) :: Source # Methods embedM :: (Applicative m, MatchMonad (m (List Type e tp)) m) => m (List Type e tp) -> m (MonadResult (m (List Type e tp))) Source #
GCompare [Type] (DynamicConstructor sig) Source #
Methods gcompare :: f a -> f b -> GOrdering (DynamicConstructor sig) a b #
GCompare [Type] (Constr (DynamicValue l sig)) Source #
Methods gcompare :: f a -> f b -> GOrdering (Constr (DynamicValue l sig)) a b #
GEq [Type] (DynamicConstructor sig) Source #
Methods geq :: f a -> f b -> Maybe ((DynamicConstructor sig := a) b) #
GEq [Type] (Constr (DynamicValue l sig)) Source #
Methods geq :: f a -> f b -> Maybe ((Constr (DynamicValue l sig) := a) b) #
GCompare ([Type], *) NoCon #
Methods gcompare :: f a -> f b -> GOrdering NoCon a b #
GCompare ([Type], Type) FunRepr Source #
Methods gcompare :: f a -> f b -> GOrdering FunRepr a b #
GCompare ([Type], Type) NoFun #
Methods gcompare :: f a -> f b -> GOrdering NoFun a b #
GCompare (*, Type) NoField #
Methods gcompare :: f a -> f b -> GOrdering NoField a b #
GEq ([Type], *) NoCon #
Methods geq :: f a -> f b -> Maybe ((NoCon := a) b) #
GEq ([Type], Type) FunRepr Source #
Methods geq :: f a -> f b -> Maybe ((FunRepr := a) b) #
GEq ([Type], Type) NoFun #
Methods geq :: f a -> f b -> Maybe ((NoFun := a) b) #
GEq (*, Type) NoField #
Methods geq :: f a -> f b -> Maybe ((NoField := a) b) #
GShow ([Type], *) NoCon #
Methods gshowsPrec :: Int -> t a -> ShowS #
GShow ([Type], Type) NoFun #
Methods gshowsPrec :: Int -> t a -> ShowS #
GShow (*, Type) NoField #
Methods gshowsPrec :: Int -> t a -> ShowS #
GCompare ([Type], Type) fun => GCompare ([Type], Type) (Function fun) #
Methods gcompare :: f a -> f b -> GOrdering (Function fun) a b #
Ord v => GCompare ([Type], Type) (UntypedFun v) #
Methods gcompare :: f a -> f b -> GOrdering (UntypedFun v) a b #
GEq ([Type], Type) fun => GEq ([Type], Type) (Function fun) #
Methods geq :: f a -> f b -> Maybe ((Function fun := a) b) #
Eq v => GEq ([Type], Type) (UntypedFun v) #
Methods geq :: f a -> f b -> Maybe ((UntypedFun v := a) b) #
GShow ([Type], Type) fun => GShow ([Type], Type) (Function fun) #
Methods gshowsPrec :: Int -> t a -> ShowS #
Show v => GShow ([Type], Type) (UntypedFun v) #
Methods gshowsPrec :: Int -> t a -> ShowS #
GCompare ([Type], Type) (UserFun m e) #
Methods gcompare :: f a -> f b -> GOrdering (UserFun m e) a b #
GEq ([Type], Type) (UserFun m e) #
Methods geq :: f a -> f b -> Maybe ((UserFun m e := a) b) #
GShow ([Type], Type) (UserFun m e) #
Methods gshowsPrec :: Int -> t a -> ShowS #
HasMonad (List Type e tp) Source #
Associated Types type MatchMonad (List Type e tp) (m :: * -> ) :: Constraint Source # type MonadResult (List Type e tp) :: Source # Methods embedM :: (Applicative m, MatchMonad (List Type e tp) m) => List Type e tp -> m (MonadResult (List Type e tp)) Source #
(Same ((:) Type tp tps), (~) Type tp (SameType ((:) Type tp tps))) => Same ((:) Type tp ((:) Type tp tps)) Source #
Associated Types type SameType ((:) Type tp ((:) Type tp tps) :: [Type]) :: Type Methods sameType :: List Type Repr ((Type ': tp) ((Type ': tp) tps)) -> Repr (SameType ((Type ': tp) ((Type ': tp) tps))) sameToAllEq :: List Type e ((Type ': tp) ((Type ': tp) tps)) -> List Type e (AllEq (SameType ((Type ': tp) ((Type ': tp) tps))) (Length Type ((Type ': tp) ((Type ': tp) tps))))
Same ((:) Type tp ([] Type)) Source #
Associated Types type SameType ((:) Type tp ([] Type) :: [Type]) :: Type Methods sameType :: List Type Repr ((Type ': tp) [Type]) -> Repr (SameType ((Type ': tp) [Type])) sameToAllEq :: List Type e ((Type ': tp) [Type]) -> List Type e (AllEq (SameType ((Type ': tp) [Type])) (Length Type ((Type ': tp) [Type])))
Unlift ((:) Type t2 ts) idx => Unlift ((:) Type t1 ((:) Type t2 ts)) idx Source #
Methods unliftType :: List Type Repr (Lifted ((Type ': t1) ((Type ': t2) ts)) idx) -> (List Type Repr ((Type ': t1) ((Type ': t2) ts)), List Type Repr idx) Source # unliftTypeWith :: List Type Repr (Lifted ((Type ': t1) ((Type ': t2) ts)) idx) -> List Type Repr ((Type ': t1) ((Type ': t2) ts)) -> List Type Repr idx Source #
Unlift ((:) Type tp ([] Type)) idx Source #
Methods unliftType :: List Type Repr (Lifted ((Type ': tp) [Type]) idx) -> (List Type Repr ((Type ': tp) [Type]), List Type Repr idx) Source # unliftTypeWith :: List Type Repr (Lifted ((Type ': tp) [Type]) idx) -> List Type Repr ((Type ': tp) [Type]) -> List Type Repr idx Source #
type MonadResult (m (List Type e tp)) Source #
type MonadResult (m (List Type e tp)) = List Type e tp
type MatchMonad (m (List Type e tp)) m' Source #
type MatchMonad (m (List Type e tp)) m' = (~) (* -> *) m m'
type MonadResult (List Type e tp) Source #
type MonadResult (List Type e tp) = List Type e tp
type MatchMonad (List Type e tp) m Source #
type MatchMonad (List Type e tp) m = ()

type family Lifted (tps :: [Type]) (idx :: [Type]) :: [Type] where ... Source #

Equations

Lifted '[] idx = '[]
Lifted (tp ': tps) idx = ArrayType idx tp ': Lifted tps idx

class Unlift tps idx where Source #

Minimal complete definition

unliftType, unliftTypeWith

Methods

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

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

Instances

Unlift ((:) Type t2 ts) idx => Unlift ((:) Type t1 ((:) Type t2 ts)) idx Source #
Methods unliftType :: List Type Repr (Lifted ((Type ': t1) ((Type ': t2) ts)) idx) -> (List Type Repr ((Type ': t1) ((Type ': t2) ts)), List Type Repr idx) Source # unliftTypeWith :: List Type Repr (Lifted ((Type ': t1) ((Type ': t2) ts)) idx) -> List Type Repr ((Type ': t1) ((Type ': t2) ts)) -> List Type Repr idx Source #
Unlift ((:) Type tp ([] Type)) idx Source #
Methods unliftType :: List Type Repr (Lifted ((Type ': tp) [Type]) idx) -> (List Type Repr ((Type ': tp) [Type]), List Type Repr idx) Source # unliftTypeWith :: List Type Repr (Lifted ((Type ': tp) [Type]) idx) -> List Type Repr ((Type ': tp) [Type]) -> List Type Repr idx Source #

type family Fst (a :: (p, q)) :: p where ... Source #

Equations

Fst '(x, y) = x

type family Snd (a :: (p, q)) :: q where ... Source #

Equations

Snd '(x, y) = y

class (Typeable dt, Ord (Datatype dt), GCompare (Constr dt), GCompare (Field dt)) => IsDatatype dt where Source #

Minimal complete definition

datatypeGet, parameters, datatypeName, constructors, constrName, test, fields, construct, deconstruct, fieldName, fieldType, fieldGet

Associated Types

type Parameters dt :: Nat Source #

type Signature dt :: [[Type]] Source #

data Datatype dt :: * Source #

data Constr dt (csig :: [Type]) Source #

data Field dt (tp :: Type) Source #

Methods

datatypeGet :: (GetType e, Length par ~ Parameters dt) => dt par e -> (Datatype dt, List Repr par) Source #

Get the data type from a value

parameters :: Datatype dt -> Natural (Parameters dt) Source #

How many polymorphic parameters does this datatype have

datatypeName :: Datatype dt -> String Source #

The name of the datatype. Must be unique.

constructors :: Datatype dt -> List (Constr dt) (Signature dt) Source #

Get all of the constructors of this datatype

constrName :: Constr dt csig -> String Source #

Get the name of a constructor

test :: dt par e -> Constr dt csig -> Bool Source #

Test if a value is constructed using a specific constructor

fields :: Constr dt csig -> List (Field dt) csig Source #

Get all the fields of a constructor

construct :: Length par ~ Parameters dt => List Repr par -> Constr dt csig -> List e (Instantiated csig par) -> dt par e Source #

Construct a value using a constructor

deconstruct :: GetType e => dt par e -> ConApp dt par e Source #

Deconstruct a value into a constructor and a list of arguments

fieldName :: Field dt tp -> String Source #

Get the name of a field

fieldType :: Field dt tp -> Repr tp Source #

Get the type of a field

fieldGet :: dt par e -> Field dt tp -> e (CType tp par) Source #

Extract a field value from a value

Instances

(Typeable Nat l, Typeable [[Type]] sig) => IsDatatype (DynamicValue l sig) Source #

type family CType (tp :: Type) (par :: [Type]) :: Type where ... Source #

Equations

CType BoolType par = BoolType
CType IntType par = IntType
CType RealType par = RealType
CType (BitVecType w) par = BitVecType w
CType (ArrayType idx el) par = ArrayType (Instantiated idx par) (CType el par)
CType (DataType dt arg) par = DataType dt (Instantiated arg par)
CType (ParameterType n) par = Index par n

type family Instantiated (sig :: [Type]) (par :: [Type]) :: [Type] where ... Source #

Equations

Instantiated '[] par = '[]
Instantiated (tp ': tps) par = CType tp par ': Instantiated tps par

data ConApp dt par e Source #

Constructors

Length par ~ Parameters dt => ConApp
Fields parameters' :: List Repr par constructor :: Constr dt csig arguments :: List e (Instantiated csig par)

data AnyDatatype Source #

Constructors

IsDatatype dt => AnyDatatype (Datatype dt)

Instances

Eq AnyDatatype Source #
Methods (==) :: AnyDatatype -> AnyDatatype -> Bool # (/=) :: AnyDatatype -> AnyDatatype -> Bool #
Ord AnyDatatype Source #
Methods compare :: AnyDatatype -> AnyDatatype -> Ordering # (<) :: AnyDatatype -> AnyDatatype -> Bool # (<=) :: AnyDatatype -> AnyDatatype -> Bool # (>) :: AnyDatatype -> AnyDatatype -> Bool # (>=) :: AnyDatatype -> AnyDatatype -> Bool # max :: AnyDatatype -> AnyDatatype -> AnyDatatype # min :: AnyDatatype -> AnyDatatype -> AnyDatatype #

data AnyConstr Source #

Constructors

IsDatatype dt => AnyConstr (Datatype dt) (Constr dt csig)

Instances

Eq AnyConstr Source #
Methods (==) :: AnyConstr -> AnyConstr -> Bool # (/=) :: AnyConstr -> AnyConstr -> Bool #
Ord AnyConstr Source #
Methods compare :: AnyConstr -> AnyConstr -> Ordering # (<) :: AnyConstr -> AnyConstr -> Bool # (<=) :: AnyConstr -> AnyConstr -> Bool # (>) :: AnyConstr -> AnyConstr -> Bool # (>=) :: AnyConstr -> AnyConstr -> Bool # max :: AnyConstr -> AnyConstr -> AnyConstr # min :: AnyConstr -> AnyConstr -> AnyConstr #

data AnyField Source #

Constructors

IsDatatype dt => AnyField (Datatype dt) (Field dt tp)

Instances

Eq AnyField Source #
Methods (==) :: AnyField -> AnyField -> Bool # (/=) :: AnyField -> AnyField -> Bool #
Ord AnyField Source #
Methods compare :: AnyField -> AnyField -> Ordering # (<) :: AnyField -> AnyField -> Bool # (<=) :: AnyField -> AnyField -> Bool # (>) :: AnyField -> AnyField -> Bool # (>=) :: AnyField -> AnyField -> Bool # max :: AnyField -> AnyField -> AnyField # min :: AnyField -> AnyField -> AnyField #

data TypeRegistry dt con field Source #

Constructors

TypeRegistry
Fields allDatatypes :: Map dt AnyDatatype revDatatypes :: Map AnyDatatype dt allConstructors :: Map con AnyConstr revConstructors :: Map AnyConstr con allFields :: Map field AnyField revFields :: Map AnyField field

emptyTypeRegistry :: TypeRegistry dt con field Source #

dependencies Source #

Arguments

:: IsDatatype dt
=> Set String	Already registered datatypes
-> Datatype dt
-> (Set String, [[AnyDatatype]])

signature :: IsDatatype dt => Datatype dt -> List (List Repr) (Signature dt) Source #

constrSig :: IsDatatype dt => Constr dt sig -> List Repr sig Source #

instantiate :: List Repr sig -> List Repr par -> (List Repr (Instantiated sig par), Length sig :~: Length (Instantiated sig par)) Source #

ctype :: Repr tp -> List Repr par -> Repr (CType tp par) Source #

determines :: IsDatatype dt => Datatype dt -> Constr dt sig -> Bool Source #

containedParameter :: Repr tp -> Set Integer -> Set Integer Source #

typeInference Source #

Arguments

:: Repr atp	The type containing parameters
-> Repr ctp	The concrete type without parameters
-> (forall n ntp. Natural n -> Repr ntp -> a -> Maybe a)	Action to execute when a parameter is assigned
-> a
-> Maybe a

typeInferences :: List Repr atps -> List Repr ctps -> (forall n ntp. Natural n -> Repr ntp -> a -> Maybe a) -> a -> Maybe a Source #

partialInstantiation :: Repr tp -> (forall n a. Natural n -> (forall ntp. Repr ntp -> a) -> Maybe a) -> (forall rtp. Repr rtp -> a) -> a Source #

partialInstantiations :: List Repr tp -> (forall n a. Natural n -> (forall ntp. Repr ntp -> a) -> Maybe a) -> (forall rtp. Length tp ~ Length rtp => List Repr rtp -> a) -> a Source #

registerType :: (Monad m, IsDatatype tp, Ord dt, Ord con, Ord field) => dt -> (forall sig. Constr tp sig -> m con) -> (forall sig tp'. Field tp tp' -> m field) -> Datatype tp -> TypeRegistry dt con field -> m (TypeRegistry dt con field) Source #

registerTypeName :: IsDatatype dt => Datatype dt -> TypeRegistry String String String -> TypeRegistry String String String Source #

data DynamicDatatype par sig Source #

Constructors

DynDatatype
Fields dynDatatypeParameters :: Natural par dynDatatypeSig :: List (DynamicConstructor sig) sig dynDatatypeName :: String

Instances

Eq (DynamicDatatype par sig) Source #
Methods (==) :: DynamicDatatype par sig -> DynamicDatatype par sig -> Bool # (/=) :: DynamicDatatype par sig -> DynamicDatatype par sig -> Bool #
Ord (DynamicDatatype par sig) Source #
Methods compare :: DynamicDatatype par sig -> DynamicDatatype par sig -> Ordering # (<) :: DynamicDatatype par sig -> DynamicDatatype par sig -> Bool # (<=) :: DynamicDatatype par sig -> DynamicDatatype par sig -> Bool # (>) :: DynamicDatatype par sig -> DynamicDatatype par sig -> Bool # (>=) :: DynamicDatatype par sig -> DynamicDatatype par sig -> Bool # max :: DynamicDatatype par sig -> DynamicDatatype par sig -> DynamicDatatype par sig # min :: DynamicDatatype par sig -> DynamicDatatype par sig -> DynamicDatatype par sig #

data DynamicConstructor sig csig where Source #

Constructors

DynConstructor :: Natural idx -> String -> List (DynamicField sig) (Index sig idx) -> DynamicConstructor sig (Index sig idx)

Instances

GCompare [Type] (DynamicConstructor sig) Source #
Methods gcompare :: f a -> f b -> GOrdering (DynamicConstructor sig) a b #
GEq [Type] (DynamicConstructor sig) Source #
Methods geq :: f a -> f b -> Maybe ((DynamicConstructor sig := a) b) #

data DynamicField sig tp where Source #

Constructors

DynField :: Natural idx -> Natural fidx -> String -> Repr (Index (Index sig idx) fidx) -> DynamicField sig (Index (Index sig idx) fidx)

data DynamicValue plen sig par e where Source #

Constructors

DynValue :: DynamicDatatype (Length par) sig -> List Repr par -> DynamicConstructor sig csig -> List e (Instantiated csig par) -> DynamicValue (Length par) sig par e

Instances

GCompare Type (Field (DynamicValue l sig)) Source #
Methods gcompare :: f a -> f b -> GOrdering (Field (DynamicValue l sig)) a b #
GEq Type (Field (DynamicValue l sig)) Source #
Methods geq :: f a -> f b -> Maybe ((Field (DynamicValue l sig) := a) b) #
Eq (Datatype (DynamicValue l sig)) Source #
Methods (==) :: Datatype (DynamicValue l sig) -> Datatype (DynamicValue l sig) -> Bool # (/=) :: Datatype (DynamicValue l sig) -> Datatype (DynamicValue l sig) -> Bool #
Ord (Datatype (DynamicValue l sig)) Source #
Methods compare :: Datatype (DynamicValue l sig) -> Datatype (DynamicValue l sig) -> Ordering # (<) :: Datatype (DynamicValue l sig) -> Datatype (DynamicValue l sig) -> Bool # (<=) :: Datatype (DynamicValue l sig) -> Datatype (DynamicValue l sig) -> Bool # (>) :: Datatype (DynamicValue l sig) -> Datatype (DynamicValue l sig) -> Bool # (>=) :: Datatype (DynamicValue l sig) -> Datatype (DynamicValue l sig) -> Bool # max :: Datatype (DynamicValue l sig) -> Datatype (DynamicValue l sig) -> Datatype (DynamicValue l sig) # min :: Datatype (DynamicValue l sig) -> Datatype (DynamicValue l sig) -> Datatype (DynamicValue l sig) #
Show (Datatype (DynamicValue l sig)) Source #
Methods showsPrec :: Int -> Datatype (DynamicValue l sig) -> ShowS # show :: Datatype (DynamicValue l sig) -> String # showList :: [Datatype (DynamicValue l sig)] -> ShowS #
GCompare [Type] (Constr (DynamicValue l sig)) Source #
Methods gcompare :: f a -> f b -> GOrdering (Constr (DynamicValue l sig)) a b #
GEq [Type] (Constr (DynamicValue l sig)) Source #
Methods geq :: f a -> f b -> Maybe ((Constr (DynamicValue l sig) := a) b) #
(Typeable Nat l, Typeable [[Type]] sig) => IsDatatype (DynamicValue l sig) Source #
Associated Types type Parameters (DynamicValue l sig :: [Type] -> (Type -> ) -> ) :: Nat Source # type Signature (DynamicValue l sig :: [Type] -> (Type -> ) -> ) :: [[Type]] Source # data Datatype (DynamicValue l sig :: [Type] -> (Type -> ) -> ) :: * Source # data Constr (DynamicValue l sig :: [Type] -> (Type -> ) -> ) (csig :: [Type]) :: * Source # data Field (DynamicValue l sig :: [Type] -> (Type -> ) -> ) (tp :: Type) :: * Source # Methods datatypeGet :: (GetType e, (Nat ~ Length Type par) (Parameters (DynamicValue l sig))) => DynamicValue l sig par e -> (Datatype (DynamicValue l sig), List Type Repr par) Source # parameters :: Datatype (DynamicValue l sig) -> Natural (Parameters (DynamicValue l sig)) Source # datatypeName :: Datatype (DynamicValue l sig) -> String Source # constructors :: Datatype (DynamicValue l sig) -> List [Type] (Constr (DynamicValue l sig)) (Signature (DynamicValue l sig)) Source # constrName :: Constr (DynamicValue l sig) csig -> String Source # test :: DynamicValue l sig par e -> Constr (DynamicValue l sig) csig -> Bool Source # fields :: Constr (DynamicValue l sig) csig -> List Type (Field (DynamicValue l sig)) csig Source # construct :: (Nat ~ Length Type par) (Parameters (DynamicValue l sig)) => List Type Repr par -> Constr (DynamicValue l sig) csig -> List Type e (Instantiated csig par) -> DynamicValue l sig par e Source # deconstruct :: GetType e => DynamicValue l sig par e -> ConApp (DynamicValue l sig) par e Source # fieldName :: Field (DynamicValue l sig) tp -> String Source # fieldType :: Field (DynamicValue l sig) tp -> Repr tp Source # fieldGet :: DynamicValue l sig par e -> Field (DynamicValue l sig) tp -> e (CType tp par) Source #
type Parameters (DynamicValue l sig) Source #
type Parameters (DynamicValue l sig) = l
type Signature (DynamicValue l sig) Source #
type Signature (DynamicValue l sig) = sig
data Datatype (DynamicValue l sig) Source #
data Datatype (DynamicValue l sig) = DynDatatypeInfo { dynDatatypeInfo :: DynamicDatatype l sig }
data Constr (DynamicValue l sig) Source #
data Constr (DynamicValue l sig) = DynConstr (DynamicDatatype l sig) (DynamicConstructor sig csig)
data Field (DynamicValue l sig) Source #
data Field (DynamicValue l sig) = DynField' (DynamicField sig tp)

newtype BitWidth bw Source #

Constructors

BitWidth
Fields bwSize :: Integer

Instances

GCompare Nat BitWidth Source #
Methods gcompare :: f a -> f b -> GOrdering BitWidth a b #
GEq Nat BitWidth Source #
Methods geq :: f a -> f b -> Maybe ((BitWidth := a) b) #
Eq (BitWidth bw) Source #
Methods (==) :: BitWidth bw -> BitWidth bw -> Bool # (/=) :: BitWidth bw -> BitWidth bw -> Bool #
Show (BitWidth bw) Source #
Methods showsPrec :: Int -> BitWidth bw -> ShowS # show :: BitWidth bw -> String # showList :: [BitWidth bw] -> ShowS #

getBw :: Integer -> (forall bw. KnownNat bw => BitWidth bw -> a) -> a Source #

data Value a where Source #

Values that can be used as constants in expressions.

Constructors

BoolValue :: Bool -> Value BoolType
IntValue :: Integer -> Value IntType
RealValue :: Rational -> Value RealType
BitVecValue :: Integer -> BitWidth bw -> Value (BitVecType bw)
DataValue :: (IsDatatype dt, Length par ~ Parameters dt) => dt par Value -> Value (DataType dt par)

Instances

GetType Value Source #
Methods getType :: Value tp -> Repr tp Source #
GCompare Type Value Source #
Methods gcompare :: f a -> f b -> GOrdering Value a b #
GEq Type Value Source #
Methods geq :: f a -> f b -> Maybe ((Value := a) b) #
GShow Type Value Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
Embed Identity Value Source #
Associated Types type EmVar (Identity :: * -> ) (Value :: Type -> ) :: Type -> * Source # type EmQVar (Identity :: * -> ) (Value :: Type -> ) :: Type -> * Source # type EmFun (Identity :: * -> ) (Value :: Type -> ) :: ([Type], Type) -> * Source # type EmFunArg (Identity :: * -> ) (Value :: Type -> ) :: Type -> * Source # type EmLVar (Identity :: * -> ) (Value :: Type -> ) :: Type -> * Source # Methods embed :: Identity (EmbedExpr Identity Value tp) -> Identity (Value tp) Source # embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (Value BoolType) Source # embedTypeOf :: Identity (Value tp -> Repr tp) Source #
Bounded (Value BoolType) Source #
Methods minBound :: Value BoolType # maxBound :: Value BoolType #
KnownNat bw => Bounded (Value (BitVecType bw)) Source #
Methods minBound :: Value (BitVecType bw) # maxBound :: Value (BitVecType bw) #
Enum (Value BoolType) Source #
Methods succ :: Value BoolType -> Value BoolType # pred :: Value BoolType -> Value BoolType # toEnum :: Int -> Value BoolType # fromEnum :: Value BoolType -> Int # enumFrom :: Value BoolType -> [Value BoolType] # enumFromThen :: Value BoolType -> Value BoolType -> [Value BoolType] # enumFromTo :: Value BoolType -> Value BoolType -> [Value BoolType] # enumFromThenTo :: Value BoolType -> Value BoolType -> Value BoolType -> [Value BoolType] #
Enum (Value IntType) Source #
Methods succ :: Value IntType -> Value IntType # pred :: Value IntType -> Value IntType # toEnum :: Int -> Value IntType # fromEnum :: Value IntType -> Int # enumFrom :: Value IntType -> [Value IntType] # enumFromThen :: Value IntType -> Value IntType -> [Value IntType] # enumFromTo :: Value IntType -> Value IntType -> [Value IntType] # enumFromThenTo :: Value IntType -> Value IntType -> Value IntType -> [Value IntType] #
KnownNat bw => Enum (Value (BitVecType bw)) Source #
Methods succ :: Value (BitVecType bw) -> Value (BitVecType bw) # pred :: Value (BitVecType bw) -> Value (BitVecType bw) # toEnum :: Int -> Value (BitVecType bw) # fromEnum :: Value (BitVecType bw) -> Int # enumFrom :: Value (BitVecType bw) -> [Value (BitVecType bw)] # enumFromThen :: Value (BitVecType bw) -> Value (BitVecType bw) -> [Value (BitVecType bw)] # enumFromTo :: Value (BitVecType bw) -> Value (BitVecType bw) -> [Value (BitVecType bw)] # enumFromThenTo :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) -> [Value (BitVecType bw)] #
Eq (Value t) Source #
Methods (==) :: Value t -> Value t -> Bool # (/=) :: Value t -> Value t -> Bool #
Fractional (Value RealType) Source #
Methods (/) :: Value RealType -> Value RealType -> Value RealType # recip :: Value RealType -> Value RealType # fromRational :: Rational -> Value RealType #
Integral (Value IntType) Source #
Methods quot :: Value IntType -> Value IntType -> Value IntType # rem :: Value IntType -> Value IntType -> Value IntType # div :: Value IntType -> Value IntType -> Value IntType # mod :: Value IntType -> Value IntType -> Value IntType # quotRem :: Value IntType -> Value IntType -> (Value IntType, Value IntType) # divMod :: Value IntType -> Value IntType -> (Value IntType, Value IntType) # toInteger :: Value IntType -> Integer #
KnownNat bw => Integral (Value (BitVecType bw)) Source #
Methods quot :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # rem :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # div :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # mod :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # quotRem :: Value (BitVecType bw) -> Value (BitVecType bw) -> (Value (BitVecType bw), Value (BitVecType bw)) # divMod :: Value (BitVecType bw) -> Value (BitVecType bw) -> (Value (BitVecType bw), Value (BitVecType bw)) # toInteger :: Value (BitVecType bw) -> Integer #
Num (Value IntType) Source #
Methods (+) :: Value IntType -> Value IntType -> Value IntType # (-) :: Value IntType -> Value IntType -> Value IntType # (*) :: Value IntType -> Value IntType -> Value IntType # negate :: Value IntType -> Value IntType # abs :: Value IntType -> Value IntType # signum :: Value IntType -> Value IntType # fromInteger :: Integer -> Value IntType #
Num (Value RealType) Source #
Methods (+) :: Value RealType -> Value RealType -> Value RealType # (-) :: Value RealType -> Value RealType -> Value RealType # (*) :: Value RealType -> Value RealType -> Value RealType # negate :: Value RealType -> Value RealType # abs :: Value RealType -> Value RealType # signum :: Value RealType -> Value RealType # fromInteger :: Integer -> Value RealType #
KnownNat bw => Num (Value (BitVecType bw)) Source #
Methods (+) :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # (-) :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # (*) :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # negate :: Value (BitVecType bw) -> Value (BitVecType bw) # abs :: Value (BitVecType bw) -> Value (BitVecType bw) # signum :: Value (BitVecType bw) -> Value (BitVecType bw) # fromInteger :: Integer -> Value (BitVecType bw) #
Ord (Value t) Source #
Methods compare :: Value t -> Value t -> Ordering # (<) :: Value t -> Value t -> Bool # (<=) :: Value t -> Value t -> Bool # (>) :: Value t -> Value t -> Bool # (>=) :: Value t -> Value t -> Bool # max :: Value t -> Value t -> Value t # min :: Value t -> Value t -> Value t #
Real (Value IntType) Source #
Methods toRational :: Value IntType -> Rational #
Real (Value RealType) Source #
Methods toRational :: Value RealType -> Rational #
KnownNat bw => Real (Value (BitVecType bw)) Source #
Methods toRational :: Value (BitVecType bw) -> Rational #
RealFrac (Value RealType) Source #
Methods properFraction :: Integral b => Value RealType -> (b, Value RealType) # truncate :: Integral b => Value RealType -> b # round :: Integral b => Value RealType -> b # ceiling :: Integral b => Value RealType -> b # floor :: Integral b => Value RealType -> b #
Show (Value tp) Source #
Methods showsPrec :: Int -> Value tp -> ShowS # show :: Value tp -> String # showList :: [Value tp] -> ShowS #
KnownNat bw => Bits (Value (BitVecType bw)) Source #
Methods (.&.) :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # (.\|.) :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # xor :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # complement :: Value (BitVecType bw) -> Value (BitVecType bw) # shift :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # rotate :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # zeroBits :: Value (BitVecType bw) # bit :: Int -> Value (BitVecType bw) # setBit :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # clearBit :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # complementBit :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # testBit :: Value (BitVecType bw) -> Int -> Bool # bitSizeMaybe :: Value (BitVecType bw) -> Maybe Int # bitSize :: Value (BitVecType bw) -> Int # isSigned :: Value (BitVecType bw) -> Bool # shiftL :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # unsafeShiftL :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # shiftR :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # unsafeShiftR :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # rotateL :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # rotateR :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # popCount :: Value (BitVecType bw) -> Int #
KnownNat bw => FiniteBits (Value (BitVecType bw)) Source #
Methods finiteBitSize :: Value (BitVecType bw) -> Int # countLeadingZeros :: Value (BitVecType bw) -> Int # countTrailingZeros :: Value (BitVecType bw) -> Int #
type EmVar Identity Value Source #
type EmVar Identity Value = NoVar
type EmQVar Identity Value Source #
type EmQVar Identity Value = NoVar
type EmFun Identity Value Source #
type EmFun Identity Value = UserFun Identity Value
type EmFunArg Identity Value Source #
type EmFunArg Identity Value = NoVar
type EmLVar Identity Value Source #
type EmLVar Identity Value = NoVar

pattern ConstrValue :: forall a. () => forall par dt csig. ((~) Nat (Length Type par) (Parameters dt), (~) Type a (DataType ([Type] -> (Type -> *) -> *) dt par), IsDatatype dt) => List Type Repr par -> Constr dt csig -> List Type Value (Instantiated csig par) -> Value a Source #

data AnyValue Source #

Constructors

AnyValue (Value t)

data Repr t where Source #

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 :: BitWidth bw -> Repr (BitVecType bw)
ArrayRepr :: List Repr idx -> Repr val -> Repr (ArrayType idx val)
DataRepr :: (IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Repr (DataType dt par)
ParameterRepr :: Natural p -> Repr (ParameterType p)

Instances

GetType Repr Source #
Methods getType :: Repr tp -> Repr tp Source #
GCompare Type Repr Source #
Methods gcompare :: f a -> f b -> GOrdering Repr a b #
GEq Type Repr Source #
Methods geq :: f a -> f b -> Maybe ((Repr := a) b) #
GShow Type Repr Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
Embed Identity Repr Source #
Associated Types type EmVar (Identity :: * -> ) (Repr :: Type -> ) :: Type -> * Source # type EmQVar (Identity :: * -> ) (Repr :: Type -> ) :: Type -> * Source # type EmFun (Identity :: * -> ) (Repr :: Type -> ) :: ([Type], Type) -> * Source # type EmFunArg (Identity :: * -> ) (Repr :: Type -> ) :: Type -> * Source # type EmLVar (Identity :: * -> ) (Repr :: Type -> ) :: Type -> * Source # Methods embed :: Identity (EmbedExpr Identity Repr tp) -> Identity (Repr tp) Source # embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (Repr BoolType) Source # embedTypeOf :: Identity (Repr tp -> Repr tp) Source #
Eq (Repr tp) Source #
Methods (==) :: Repr tp -> Repr tp -> Bool # (/=) :: Repr tp -> Repr tp -> Bool #
Ord (Repr tp) Source #
Methods compare :: Repr tp -> Repr tp -> Ordering # (<) :: Repr tp -> Repr tp -> Bool # (<=) :: Repr tp -> Repr tp -> Bool # (>) :: Repr tp -> Repr tp -> Bool # (>=) :: Repr tp -> Repr tp -> Bool # max :: Repr tp -> Repr tp -> Repr tp # min :: Repr tp -> Repr tp -> Repr tp #
Show (Repr t) Source #
Methods showsPrec :: Int -> Repr t -> ShowS # show :: Repr t -> String # showList :: [Repr t] -> ShowS #
type EmVar Identity Repr Source #
type EmVar Identity Repr = Repr
type EmQVar Identity Repr Source #
type EmQVar Identity Repr = Repr
type EmFun Identity Repr Source #
type EmFun Identity Repr = FunRepr
type EmFunArg Identity Repr Source #
type EmFunArg Identity Repr = Repr
type EmLVar Identity Repr Source #
type EmLVar Identity Repr = Repr

data NumRepr t where Source #

Constructors

NumInt :: NumRepr IntType
NumReal :: NumRepr RealType

Instances

GetType NumRepr Source #
Methods getType :: NumRepr tp -> Repr tp Source #
GCompare Type NumRepr Source #
Methods gcompare :: f a -> f b -> GOrdering NumRepr a b #
GEq Type NumRepr Source #
Methods geq :: f a -> f b -> Maybe ((NumRepr := a) b) #
GShow Type NumRepr Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
Show (NumRepr t) Source #
Methods showsPrec :: Int -> NumRepr t -> ShowS # show :: NumRepr t -> String # showList :: [NumRepr t] -> ShowS #

data FunRepr sig where Source #

Constructors

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

Instances

GCompare ([Type], Type) FunRepr Source #
Methods gcompare :: f a -> f b -> GOrdering FunRepr a b #
GEq ([Type], Type) FunRepr Source #
Methods geq :: f a -> f b -> Maybe ((FunRepr := a) b) #

class GetType v where Source #

Minimal complete definition

getType

Methods

getType :: v tp -> Repr tp Source #

Instances

GetType NumRepr Source #
Methods getType :: NumRepr tp -> Repr tp Source #
GetType Repr Source #
Methods getType :: Repr tp -> Repr tp Source #
GetType Value Source #
Methods getType :: Value tp -> Repr tp Source #
GetType NoVar Source #
Methods getType :: NoVar tp -> Repr tp Source #
GetFunType fun => GetType (EvalResult fun) Source #
Methods getType :: EvalResult fun tp -> Repr tp Source #
GetType (UntypedVar v) Source #
Methods getType :: UntypedVar v tp -> Repr tp Source #
GetType (ValueExt m) Source #
Methods getType :: ValueExt m tp -> Repr tp Source #
(GetType var, GetType qvar, GetFunType fun, GetType farg, GetType lvar) => GetType (SMTExpr var qvar fun farg lvar) Source #
Methods getType :: SMTExpr var qvar fun farg lvar tp -> Repr tp Source #
(GetType v, GetType qv, GetFunType fun, GetType fv, GetType lv, GetType e) => GetType (Expression v qv fun fv lv e) Source #
Methods getType :: Expression v qv fun fv lv e tp -> Repr tp Source #

class GetFunType fun where Source #

Minimal complete definition

getFunType

Methods

getFunType :: fun '(arg, res) -> (List Repr arg, Repr res) Source #

Instances

GetFunType NoFun Source #
Methods getFunType :: NoFun (([Type], Type) arg res) -> (List Type Repr arg, Repr res) Source #
GetFunType fun => GetFunType (Function fun) Source #
Methods getFunType :: Function fun (([Type], Type) arg res) -> (List Type Repr arg, Repr res) Source #
GetFunType (UntypedFun v) Source #
Methods getFunType :: UntypedFun v (([Type], Type) arg res) -> (List Type Repr arg, Repr res) Source #
GetFunType (UserFun m e) Source #
Methods getFunType :: UserFun m e (([Type], Type) arg res) -> (List Type Repr arg, Repr res) Source #

bw :: KnownNat bw => Proxy bw -> BitWidth bw Source #

bool :: Repr BoolType Source #

A representation of the SMT Bool type. Holds the values true or false. Constants can be created using cbool.

int :: Repr IntType Source #

A representation of the SMT Int type. Holds the unbounded positive and negative integers. Constants can be created using cint.

real :: Repr RealType Source #

A representation of the SMT Real type. Holds positive and negative reals x/y where x and y are integers. Constants can be created using creal.

bitvec Source #

Arguments

:: BitWidth bw	The width of the bitvector
-> Repr (BitVecType bw)

A typed representation of the SMT BitVec type. Holds bitvectors (a vector of booleans) of a certain bitwidth. Constants can be created using cbv.

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

A representation of the SMT Array type. Has a list of index types and an element type. Stores one value of the element type for each combination of the index types. Constants can be created using constArray.

dt :: (IsDatatype dt, Parameters dt ~ Z) => Datatype dt -> Repr (DataType dt '[]) Source #

A representation of a user-defined datatype without parameters.

dt' :: (IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Repr (DataType dt par) Source #

A representation of a user-defined datatype with parameters.

showBitVec :: Int -> Integer -> Integer -> ShowS Source #

valueType :: Value tp -> Repr tp Source #

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

numRepr :: NumRepr tp -> Repr tp Source #

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

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

typeSize :: Maybe (List Repr par) -> Repr tp -> Maybe Integer Source #

Determine the number of elements a type contains. Nothing means the type has infinite elements.

typeFiniteDomain :: Repr tp -> Maybe [Value tp] Source #

withBW :: KnownNat bw => (Proxy bw -> res (BitVecType bw)) -> res (BitVecType bw) Source #

bvAdd :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) Source #

bvSub :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) Source #

bvMul :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) Source #

bvDiv :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) Source #

bvMod :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) Source #

bvNegate :: Value (BitVecType bw) -> Value (BitVecType bw) Source #

bvSignum :: Value (BitVecType bw) -> Value (BitVecType bw) Source #

bvSucc :: Value (BitVecType bw) -> Value (BitVecType bw) Source #

Get the smallest bitvector value that is bigger than the given one. Also known as the successor.

bvPred :: Value (BitVecType bw) -> Value (BitVecType bw) Source #

Get the largest bitvector value that is smaller than the given one. Also known as the predecessor.

bvMinValue Source #

Arguments

:: Bool	Signed bitvector?
-> Repr (BitVecType bw)
-> Value (BitVecType bw)

Get the minimal value for a bitvector. If unsigned, the value is 0, otherwise 2^(bw-1).

bvMaxValue Source #

Arguments

:: Bool	Signed bitvector?
-> Repr (BitVecType bw)
-> Value (BitVecType bw)

Get the maximal value for a bitvector. If unsigned, the value is 2^(bw-1)-1, otherwise 2^bw-1.

bwAdd :: BitWidth bw1 -> BitWidth bw2 -> BitWidth (bw1 + bw2) Source #

datatypeEq :: (IsDatatype dt1, IsDatatype dt2) => Datatype dt1 -> Datatype dt2 -> Maybe (dt1 :~: dt2) Source #

datatypeCompare :: (IsDatatype dt1, IsDatatype dt2) => Datatype dt1 -> Datatype dt2 -> GOrdering dt1 dt2 Source #