Language.SMTLib2.Internals.Type

Synopsis

• data Type
  • = BoolType
  • | IntType
  • | RealType
  • | BitVecType Nat
  • | ArrayType [Type] Type
  • | forall a . DataType a
• type family Lifted tps idx :: [Type]
• class Unlift tps idx where
  • unliftType :: List Repr (Lifted tps idx) -> (List Repr tps, List Repr idx)
  • unliftTypeWith :: List Repr (Lifted tps idx) -> List Repr tps -> List Repr idx
• type family Fst a :: p
• type family Snd a :: q
• class (Typeable t, Typeable (DatatypeSig t), Show t, Ord t) => IsDatatype t where
  • type DatatypeSig t :: [[Type]]
  • type TypeCollectionSig t :: [([[Type]], *)]
  • 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 = Datatype {
  • datatypeName :: String
  • constructors :: Constrs Constr (Fst sig) (Snd sig)
  }
• data Constr sig = Constr {
  • conName :: String
  • conFields :: List (Field (Snd sig)) (Fst sig)
  • construct :: List ConcreteValue (Fst sig) -> Snd sig
  • conTest :: Snd sig -> Bool
  }
• data Field a t = Field {
  • fieldName :: String
  • fieldType :: Repr t
  • fieldGet :: a -> ConcreteValue t
  }
• data Value con a where
  • 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)
• data ConcreteValue a where
  • 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)
• data AnyValue con = forall t . AnyValue (Value con t)
• data Repr t where
  • 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)
• data NumRepr t where
  • NumInt :: NumRepr IntType
  • NumReal :: NumRepr RealType
• data Constrs con a t where
  • NoCon :: Constrs con `[]` t
  • ConsCon :: con `(arg, dt)` -> Constrs con args dt -> Constrs con (arg : args) dt
• data Datatypes dts sigs where
  • NoDts :: Datatypes dts `[]`
  • ConsDts :: IsDatatype dt => dts `(DatatypeSig dt, dt)` -> Datatypes dts sigs -> Datatypes dts (`(DatatypeSig dt, dt)` : sigs)
• data FunRepr sig where
  • FunRepr :: List Repr arg -> Repr tp -> FunRepr `(arg, tp)`
• class GetType v where
  • getType :: v tp -> Repr tp
• class GetFunType fun where
  • getFunType :: fun `(arg, res)` -> (List Repr arg, Repr res)
• class GetConType con where
  • getConType :: IsDatatype dt => con `(arg, dt)` -> (List Repr arg, Datatype `(DatatypeSig dt, dt)`)
• class GetFieldType field where
  • getFieldType :: IsDatatype dt => field `(dt, tp)` -> (Datatype `(DatatypeSig dt, dt)`, Repr tp)
• bool :: Repr BoolType
• 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
• 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

Documentation