Language.Hasmtlib.Codec

Documentation

type family DefaultDecoded a :: Type where ...

Computes a default Decoded Type by distributing Decoded to it's type arguments.

Equations

DefaultDecoded (t a b c d e f g h) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d) (Decoded e) (Decoded f) (Decoded g) (Decoded h)

DefaultDecoded (t a b c d e f g) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d) (Decoded e) (Decoded f) (Decoded g)

DefaultDecoded (t a b c d e f) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d) (Decoded e) (Decoded f)

DefaultDecoded (t a b c d e) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d) (Decoded e)

DefaultDecoded (t a b c d) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d)

DefaultDecoded (t a b c) = t (Decoded a) (Decoded b) (Decoded c)

DefaultDecoded (t a b) = t (Decoded a) (Decoded b)

DefaultDecoded (t a) = t (Decoded a)

DefaultDecoded x = TypeError (((((Text "DefaultDecoded (" :<>: ShowType x) :<>: Text ") is not allowed.") :$$: ((Text "Try providing the associated Type Decoded (" :<>: ShowType x) :<>: Text ") manually:")) :$$: ((Text "instance Codec (" :<>: ShowType x) :<>: Text ") where ")) :$$: ((Text " type Decoded (" :<>: ShowType x) :<>: Text ") = ... "))

class Codec a where

Lift values to SMT-Values or decode them.

You can derive an instance of this class if your type is Generic.

Minimal complete definition

Nothing

Associated Types

type Decoded a :: Type

Result of decoding a.

type Decoded a = DefaultDecoded a

Methods

decode :: Solution -> a -> Maybe (Decoded a)

Decode a value using given solution.

default decode :: (Generic a, Generic (Decoded a), GCodec (Rep a), GDecoded (Rep a) x ~ Rep (Decoded a) x) => Solution -> a -> Maybe (Decoded a)

encode :: Decoded a -> a

Encode a value as constant.

default encode :: (Generic a, Generic (Decoded a), GCodec (Rep a), GDecoded (Rep a) x ~ Rep (Decoded a) x) => Decoded a -> a

Instances

Codec ()

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded ()

Methods

decode :: Solution -> () -> Maybe (Decoded ())

encode :: Decoded () -> ()

Codec a => Codec (Identity a)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Identity a)

Methods

decode :: Solution -> Identity a -> Maybe (Decoded (Identity a))

encode :: Decoded (Identity a) -> Identity a

Codec a => Codec (First a)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (First a)

Methods

decode :: Solution -> First a -> Maybe (Decoded (First a))

encode :: Decoded (First a) -> First a

Codec a => Codec (Last a)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Last a)

Methods

decode :: Solution -> Last a -> Maybe (Decoded (Last a))

encode :: Decoded (Last a) -> Last a

Codec a => Codec (Dual a)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Dual a)

Methods

decode :: Solution -> Dual a -> Maybe (Decoded (Dual a))

encode :: Decoded (Dual a) -> Dual a

Codec a => Codec (Product a)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Product a)

Methods

decode :: Solution -> Product a -> Maybe (Decoded (Product a))

encode :: Decoded (Product a) -> Product a

Codec a => Codec (Sum a)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Sum a)

Methods

decode :: Solution -> Sum a -> Maybe (Decoded (Sum a))

encode :: Decoded (Sum a) -> Sum a

Codec a => Codec (IntMap a)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (IntMap a)

Methods

decode :: Solution -> IntMap a -> Maybe (Decoded (IntMap a))

encode :: Decoded (IntMap a) -> IntMap a

Codec a => Codec (Seq a)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Seq a)

Methods

decode :: Solution -> Seq a -> Maybe (Decoded (Seq a))

encode :: Decoded (Seq a) -> Seq a

Codec a => Codec (Tree a)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Tree a)

Methods

decode :: Solution -> Tree a -> Maybe (Decoded (Tree a))

encode :: Decoded (Tree a) -> Tree a

KnownSMTSort t => Codec (Expr t)

Decode and evaluate expressions

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Expr t)

Methods

decode :: Solution -> Expr t -> Maybe (Decoded (Expr t))

encode :: Decoded (Expr t) -> Expr t

Codec a => Codec (Maybe a)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Maybe a)

Methods

decode :: Solution -> Maybe a -> Maybe (Decoded (Maybe a))

encode :: Decoded (Maybe a) -> Maybe a

Codec a => Codec [a]

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded [a]

Methods

decode :: Solution -> [a] -> Maybe (Decoded [a])

encode :: Decoded [a] -> [a]

(Codec a, Codec b) => Codec (Either a b)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Either a b)

Methods

decode :: Solution -> Either a b -> Maybe (Decoded (Either a b))

encode :: Decoded (Either a b) -> Either a b

Codec a => Codec (Map k a)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Map k a)

Methods

decode :: Solution -> Map k a -> Maybe (Decoded (Map k a))

encode :: Decoded (Map k a) -> Map k a

(Codec a, Codec b) => Codec (a, b)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (a, b)

Methods

decode :: Solution -> (a, b) -> Maybe (Decoded (a, b))

encode :: Decoded (a, b) -> (a, b)

(Codec a, Codec b, Codec c) => Codec (a, b, c)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (a, b, c)

Methods

decode :: Solution -> (a, b, c) -> Maybe (Decoded (a, b, c))

encode :: Decoded (a, b, c) -> (a, b, c)

(Codec a, Codec b, Codec c, Codec d) => Codec (a, b, c, d)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (a, b, c, d)

Methods

decode :: Solution -> (a, b, c, d) -> Maybe (Decoded (a, b, c, d))

encode :: Decoded (a, b, c, d) -> (a, b, c, d)

(Codec a, Codec b, Codec c, Codec d, Codec e) => Codec (a, b, c, d, e)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (a, b, c, d, e)

Methods

decode :: Solution -> (a, b, c, d, e) -> Maybe (Decoded (a, b, c, d, e))

encode :: Decoded (a, b, c, d, e) -> (a, b, c, d, e)

(Codec a, Codec b, Codec c, Codec d, Codec e, Codec f) => Codec (a, b, c, d, e, f)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (a, b, c, d, e, f)

Methods

decode :: Solution -> (a, b, c, d, e, f) -> Maybe (Decoded (a, b, c, d, e, f))

encode :: Decoded (a, b, c, d, e, f) -> (a, b, c, d, e, f)

(Codec a, Codec b, Codec c, Codec d, Codec e, Codec f, Codec g) => Codec (a, b, c, d, e, f, g)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (a, b, c, d, e, f, g)

Methods

decode :: Solution -> (a, b, c, d, e, f, g) -> Maybe (Decoded (a, b, c, d, e, f, g))

encode :: Decoded (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g)

(Codec a, Codec b, Codec c, Codec d, Codec e, Codec f, Codec g, Codec h) => Codec (a, b, c, d, e, f, g, h)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (a, b, c, d, e, f, g, h)

Methods

decode :: Solution -> (a, b, c, d, e, f, g, h) -> Maybe (Decoded (a, b, c, d, e, f, g, h))

encode :: Decoded (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h)

class GCodec f where

Associated Types

type GDecoded f :: Type -> Type

Methods

gdecode :: Solution -> f a -> Maybe (GDecoded f a)

gencode :: GDecoded f a -> f a

Instances

GCodec (U1 :: Type -> Type)

Defined in Language.Hasmtlib.Codec

Associated Types

type GDecoded U1 :: Type -> Type

Methods

gdecode :: Solution -> U1 a -> Maybe (GDecoded U1 a)

gencode :: GDecoded U1 a -> U1 a

GCodec (V1 :: Type -> Type)

Defined in Language.Hasmtlib.Codec

Associated Types

type GDecoded V1 :: Type -> Type

Methods

gdecode :: Solution -> V1 a -> Maybe (GDecoded V1 a)

gencode :: GDecoded V1 a -> V1 a

(GCodec f, GCodec g) => GCodec (f :*: g)

Defined in Language.Hasmtlib.Codec

Associated Types

type GDecoded (f :*: g) :: Type -> Type

Methods

gdecode :: Solution -> (f :*: g) a -> Maybe (GDecoded (f :*: g) a)

gencode :: GDecoded (f :*: g) a -> (f :*: g) a

(GCodec f, GCodec g) => GCodec (f :+: g)

Defined in Language.Hasmtlib.Codec

Associated Types

type GDecoded (f :+: g) :: Type -> Type

Methods

gdecode :: Solution -> (f :+: g) a -> Maybe (GDecoded (f :+: g) a)

gencode :: GDecoded (f :+: g) a -> (f :+: g) a

Codec a => GCodec (K1 i a :: Type -> Type)

Defined in Language.Hasmtlib.Codec

Associated Types

type GDecoded (K1 i a) :: Type -> Type

Methods

gdecode :: Solution -> K1 i a a0 -> Maybe (GDecoded (K1 i a) a0)

gencode :: GDecoded (K1 i a) a0 -> K1 i a a0

GCodec f => GCodec (M1 i c f)

Defined in Language.Hasmtlib.Codec

Associated Types

type GDecoded (M1 i c f) :: Type -> Type

Methods

gdecode :: Solution -> M1 i c f a -> Maybe (GDecoded (M1 i c f) a)

gencode :: GDecoded (M1 i c f) a -> M1 i c f a