Language.Hasmtlib.Codec

This module provides the class Codec which takes care of marshalling data to and from external SMT-Solvers.

A generic default implementation with GCodec is possible.

Example

data V3 a = V3 a a a deriving Generic
instance Codec a => Codec (V3 a)

constantV3 :: V3 (Expr RealSort)
constantV3 = encode $ V3 7 69 42

Class

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 Int16

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Int16

Methods

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

encode :: Decoded Int16 -> Int16

Codec Int32

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Int32

Methods

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

encode :: Decoded Int32 -> Int32

Codec Int64

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Int64

Methods

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

encode :: Decoded Int64 -> Int64

Codec Int8

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Int8

Methods

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

encode :: Decoded Int8 -> Int8

Codec Word16

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Word16

Methods

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

encode :: Decoded Word16 -> Word16

Codec Word32

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Word32

Methods

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

encode :: Decoded Word32 -> Word32

Codec Word64

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Word64

Methods

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

encode :: Decoded Word64 -> Word64

Codec Word8

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Word8

Methods

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

encode :: Decoded Word8 -> Word8

Codec Ordering

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Ordering

Methods

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

encode :: Decoded Ordering -> Ordering

Codec Integer

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Integer

Methods

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

encode :: Decoded Integer -> Integer

Codec Natural

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Natural

Methods

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

encode :: Decoded Natural -> Natural

Codec ()

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded ()

Methods

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

encode :: Decoded () -> ()

Codec Bool

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Bool

Methods

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

encode :: Decoded Bool -> Bool

Codec Char

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Char

Methods

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

encode :: Decoded Char -> Char

Codec Double

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Double

Methods

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

encode :: Decoded Double -> Double

Codec Float

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Float

Methods

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

encode :: Decoded Float -> Float

Codec Int

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Int

Methods

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

encode :: Decoded Int -> Int

Codec Word

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded Word

Methods

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

encode :: Decoded Word -> Word

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

(Ix i, Codec e) => Codec (Array i e)

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Array i e)

Methods

decode :: Solution -> Array i e -> Maybe (Decoded (Array i e))

encode :: Decoded (Array i e) -> Array i e

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

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

Defined in Language.Hasmtlib.Type.Relation

Associated Types

type Decoded (Relation a b)

Methods

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

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

(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)

Generics

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

type family DefaultDecoded a :: Type where ...

Computes a default Decoded Type by distributing Decoded over 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 ") = ... "))