Language.Hasmtlib.Codec

Documentation

type family DefaultDecoded a :: Type where ...

Compute the default Decoded Type for every functor-wrapper. Useful for instances using default signatures.

Equations

DefaultDecoded (f a) = f (Decoded a)

class Codec a where

Lift values to SMT-Values or decode them.

Minimal complete definition

Nothing

Associated Types

type Decoded a :: Type

type Decoded a = DefaultDecoded a

Methods

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

Decode a value using given solution.

default decode :: (Traversable f, Codec b, a ~ f b, Decoded a ~ f (Decoded b)) => Solution -> a -> Maybe (Decoded a)

encode :: Decoded a -> a

Encode a value as constant.

default encode :: (Functor f, Codec b, a ~ f b, Decoded a ~ f (Decoded b)) => Decoded a -> a

Instances

Codec ()

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded ()

Methods

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

encode :: Decoded () -> ()

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)