{-# LANGUAGE DefaultSignatures #-}
-- required for DefaultEncoded a
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE LambdaCase #-}

module Language.Hasmtlib.Codec where

import Prelude hiding (not, (&&), (||), all, and)
import Language.Hasmtlib.Internal.Bitvec
import Language.Hasmtlib.Internal.Expr
import Language.Hasmtlib.Type.Solution
import Language.Hasmtlib.Type.ArrayMap
import Language.Hasmtlib.Boolean
import Data.Kind
import Data.Coerce
import qualified Data.List as List
import Data.Map (Map)
import Data.Sequence (Seq)
import Data.IntMap as IM hiding (foldl)
import Data.Dependent.Map as DMap
import Data.Tree (Tree)
import qualified Data.Vector.Sized as V
import Control.Monad

-- | Compute the default 'Decoded' 'Type' for every functor-wrapper.
--   Useful for instances using default signatures.
type family DefaultDecoded a :: Type where
  DefaultDecoded (f a) = f (Decoded a)

-- | Lift values to SMT-Values or decode them.
class Codec a where
  type Decoded a :: Type
  type Decoded a = DefaultDecoded a

  -- | Decode a value using given solution.
  decode :: Solution -> a -> Maybe (Decoded a)
  default decode :: (Traversable f, Codec b, a ~ f b, Decoded a ~ f (Decoded b)) => Solution -> a -> Maybe (Decoded a)
  decode Solution
sol = (b -> Maybe (Decoded b)) -> f b -> Maybe (f (Decoded b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse (Solution -> b -> Maybe (Decoded b)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol)

  -- | Encode a value as constant.
  encode :: Decoded a -> a
  default encode :: (Functor f, Codec b, a ~ f b, Decoded a ~ f (Decoded b)) => Decoded a -> a
  encode = (Decoded b -> b) -> f (Decoded b) -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Decoded b -> b
forall a. Codec a => Decoded a -> a
encode

-- | Decode and evaluate expressions
instance KnownSMTSort t => Codec (Expr t) where
  type Decoded (Expr t) = HaskellType t
  decode :: Solution -> Expr t -> Maybe (Decoded (Expr t))
decode Solution
sol (Var SMTVar t
var)  = do
    (IntValueMap IntMap (Value t)
m) <- SSMTSort t -> Solution -> Maybe (IntValueMap t)
forall {k1} (k2 :: k1 -> *) (f :: k1 -> *) (v :: k1).
GCompare k2 =>
k2 v -> DMap k2 f -> Maybe (f v)
DMap.lookup (forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t) Solution
sol
    Value t
val <- Key -> IntMap (Value t) -> Maybe (Value t)
forall a. Key -> IntMap a -> Maybe a
IM.lookup (SMTVar t -> Key
forall a b. Coercible a b => a -> b
coerce SMTVar t
var) IntMap (Value t)
m
    HaskellType t -> Maybe (HaskellType t)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (HaskellType t -> Maybe (HaskellType t))
-> HaskellType t -> Maybe (HaskellType t)
forall a b. (a -> b) -> a -> b
$ Value t -> HaskellType t
forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue Value t
val
  decode Solution
_ (Constant Value t
v)         = Decoded (Expr t) -> Maybe (Decoded (Expr t))
forall a. a -> Maybe a
Just (Decoded (Expr t) -> Maybe (Decoded (Expr t)))
-> Decoded (Expr t) -> Maybe (Decoded (Expr t))
forall a b. (a -> b) -> a -> b
$ Value t -> HaskellType t
forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue Value t
v
  decode Solution
sol (Plus Expr t
x Expr t
y)         = (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 HaskellType t -> HaskellType t -> HaskellType t
forall a. Num a => a -> a -> a
(+)   (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x) (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
y)
  decode Solution
sol (Neg Expr t
x)            = (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HaskellType t -> HaskellType t
forall a. Num a => a -> a
negate  (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x)
  decode Solution
sol (Mul Expr t
x Expr t
y)          = (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 HaskellType t -> HaskellType t -> HaskellType t
forall a. Num a => a -> a -> a
(*)   (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x) (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
y)
  decode Solution
sol (Abs Expr t
x)            = (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HaskellType t -> HaskellType t
forall a. Num a => a -> a
abs     (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x)
  decode Solution
sol (Mod Expr 'IntSort
x Expr 'IntSort
y)          = (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod   (Solution -> Expr 'IntSort -> Maybe (Decoded (Expr 'IntSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'IntSort
x) (Solution -> Expr 'IntSort -> Maybe (Decoded (Expr 'IntSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'IntSort
y)
  decode Solution
sol (IDiv Expr 'IntSort
x Expr 'IntSort
y)         = (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div   (Solution -> Expr 'IntSort -> Maybe (Decoded (Expr 'IntSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'IntSort
x) (Solution -> Expr 'IntSort -> Maybe (Decoded (Expr 'IntSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'IntSort
y)
  decode Solution
sol (Div Expr 'RealSort
x Expr 'RealSort
y)          = (Double -> Double -> Double)
-> Maybe Double -> Maybe Double -> Maybe Double
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
(/)   (Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
x) (Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
y)
  decode Solution
sol (LTH Expr t1
x Expr t1
y)          = (HaskellType t1 -> HaskellType t1 -> Bool)
-> Maybe (HaskellType t1) -> Maybe (HaskellType t1) -> Maybe Bool
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 HaskellType t1 -> HaskellType t1 -> Bool
forall a. Ord a => a -> a -> Bool
(<)   (Solution -> Expr t1 -> Maybe (Decoded (Expr t1))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t1
x) (Solution -> Expr t1 -> Maybe (Decoded (Expr t1))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t1
y)
  decode Solution
sol (LTHE Expr t1
x Expr t1
y)         = (HaskellType t1 -> HaskellType t1 -> Bool)
-> Maybe (HaskellType t1) -> Maybe (HaskellType t1) -> Maybe Bool
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 HaskellType t1 -> HaskellType t1 -> Bool
forall a. Ord a => a -> a -> Bool
(<=)  (Solution -> Expr t1 -> Maybe (Decoded (Expr t1))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t1
x) (Solution -> Expr t1 -> Maybe (Decoded (Expr t1))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t1
y)
  decode Solution
sol (EQU Vector (n + 2) (Expr t1)
xs)           = do
    [HaskellType t1]
xs' <- Solution -> [Expr t1] -> Maybe (Decoded [Expr t1])
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol (Vector (n + 2) (Expr t1) -> [Expr t1]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vector (n + 2) (Expr t1)
xs)
    case [HaskellType t1]
xs' of
      []   -> Bool -> Maybe Bool
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
forall b. Boolean b => b
true
      (HaskellType t1
x:[HaskellType t1]
xs'') -> Bool -> Maybe Bool
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ (HaskellType t1 -> Bool) -> [HaskellType t1] -> Bool
forall (t :: * -> *) b a.
(Foldable t, Boolean b) =>
(a -> b) -> t a -> b
all (HaskellType t1
x ==) [HaskellType t1]
xs''
  decode Solution
sol (Distinct Vector (n + 2) (Expr t1)
xs)      = do
    [HaskellType t1]
xs' <- Solution -> [Expr t1] -> Maybe (Decoded [Expr t1])
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol (Vector (n + 2) (Expr t1) -> [Expr t1]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vector (n + 2) (Expr t1)
xs)
    let xss :: [[HaskellType t1]]
xss = ([HaskellType t1] -> Bool)
-> [[HaskellType t1]] -> [[HaskellType t1]]
forall a. (a -> Bool) -> [a] -> [a]
List.filter ((Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
==Key
2) (Key -> Bool)
-> ([HaskellType t1] -> Key) -> [HaskellType t1] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [HaskellType t1] -> Key
forall a. [a] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length) ([[HaskellType t1]] -> [[HaskellType t1]])
-> [[HaskellType t1]] -> [[HaskellType t1]]
forall a b. (a -> b) -> a -> b
$ [HaskellType t1] -> [[HaskellType t1]]
forall a. [a] -> [[a]]
List.permutations [HaskellType t1]
xs'
    Bool -> Maybe Bool
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ ([HaskellType t1] -> Bool) -> [[HaskellType t1]] -> Bool
forall (t :: * -> *) b a.
(Foldable t, Boolean b) =>
(a -> b) -> t a -> b
all (\case (HaskellType t1
a:HaskellType t1
b:[HaskellType t1]
_) -> HaskellType t1
a HaskellType t1 -> HaskellType t1 -> Bool
forall a. Eq a => a -> a -> Bool
/= HaskellType t1
b ; [HaskellType t1]
_ -> Bool
forall b. Boolean b => b
true) [[HaskellType t1]]
xss
  decode Solution
sol (GTHE Expr t1
x Expr t1
y)         = (HaskellType t1 -> HaskellType t1 -> Bool)
-> Maybe (HaskellType t1) -> Maybe (HaskellType t1) -> Maybe Bool
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 HaskellType t1 -> HaskellType t1 -> Bool
forall a. Ord a => a -> a -> Bool
(>=)  (Solution -> Expr t1 -> Maybe (Decoded (Expr t1))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t1
x) (Solution -> Expr t1 -> Maybe (Decoded (Expr t1))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t1
y)
  decode Solution
sol (GTH Expr t1
x Expr t1
y)          = (HaskellType t1 -> HaskellType t1 -> Bool)
-> Maybe (HaskellType t1) -> Maybe (HaskellType t1) -> Maybe Bool
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 HaskellType t1 -> HaskellType t1 -> Bool
forall a. Ord a => a -> a -> Bool
(>)   (Solution -> Expr t1 -> Maybe (Decoded (Expr t1))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t1
x) (Solution -> Expr t1 -> Maybe (Decoded (Expr t1))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t1
y)
  decode Solution
sol (Not Expr t
x)            = (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap   HaskellType t -> HaskellType t
forall b. Boolean b => b -> b
not  (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x)
  decode Solution
sol (And Expr t
x Expr t
y)          = (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 HaskellType t -> HaskellType t -> HaskellType t
forall b. Boolean b => b -> b -> b
(&&) (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x) (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
y)
  decode Solution
sol (Or Expr t
x Expr t
y)           = (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 HaskellType t -> HaskellType t -> HaskellType t
forall b. Boolean b => b -> b -> b
(||) (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x) (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
y)
  decode Solution
sol (Impl Expr t
x Expr t
y)         = (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 HaskellType t -> HaskellType t -> HaskellType t
forall b. Boolean b => b -> b -> b
(==>) (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x) (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
y)
  decode Solution
sol (Xor Expr t
x Expr t
y)          = (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 HaskellType t -> HaskellType t -> HaskellType t
forall b. Boolean b => b -> b -> b
xor   (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x) (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
y)
  decode Solution
_ Expr t
Pi                   = Double -> Maybe Double
forall a. a -> Maybe a
Just Double
forall a. Floating a => a
pi
  decode Solution
sol (Sqrt Expr 'RealSort
x)           = (Double -> Double) -> Maybe Double -> Maybe Double
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Double -> Double
forall a. Floating a => a -> a
sqrt  (Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
x)
  decode Solution
sol (Exp Expr 'RealSort
x)            = (Double -> Double) -> Maybe Double -> Maybe Double
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Double -> Double
forall a. Floating a => a -> a
exp   (Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
x)
  decode Solution
sol (Sin Expr 'RealSort
x)            = (Double -> Double) -> Maybe Double -> Maybe Double
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Double -> Double
forall a. Floating a => a -> a
sin   (Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
x)
  decode Solution
sol (Cos Expr 'RealSort
x)            = (Double -> Double) -> Maybe Double -> Maybe Double
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Double -> Double
forall a. Floating a => a -> a
cos   (Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
x)
  decode Solution
sol (Tan Expr 'RealSort
x)            = (Double -> Double) -> Maybe Double -> Maybe Double
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Double -> Double
forall a. Floating a => a -> a
tan   (Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
x)
  decode Solution
sol (Asin Expr 'RealSort
x)           = (Double -> Double) -> Maybe Double -> Maybe Double
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Double -> Double
forall a. Floating a => a -> a
asin  (Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
x)
  decode Solution
sol (Acos Expr 'RealSort
x)           = (Double -> Double) -> Maybe Double -> Maybe Double
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Double -> Double
forall a. Floating a => a -> a
acos  (Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
x)
  decode Solution
sol (Atan Expr 'RealSort
x)           = (Double -> Double) -> Maybe Double -> Maybe Double
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Double -> Double
forall a. Floating a => a -> a
atan  (Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
x)
  decode Solution
sol (ToReal Expr 'IntSort
x)         = (Integer -> Double) -> Maybe Integer -> Maybe Double
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Solution -> Expr 'IntSort -> Maybe (Decoded (Expr 'IntSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'IntSort
x)
  decode Solution
sol (ToInt Expr 'RealSort
x)          = (Double -> Integer) -> Maybe Double -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Double -> Integer
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
truncate   (Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
x)
  decode Solution
sol (IsInt Expr 'RealSort
x)          = (Double -> Bool) -> Maybe Double -> Maybe Bool
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Double
0 ==) (Double -> Bool) -> (Double -> Double) -> Double -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, Double) -> Double
forall a b. (a, b) -> b
snd ((Integer, Double) -> Double)
-> (Double -> (Integer, Double)) -> Double -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> (Integer, Double)
forall b. Integral b => Double -> (b, Double)
forall a b. (RealFrac a, Integral b) => a -> (b, a)
properFraction) (Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
x)
  decode Solution
sol (Ite Expr 'BoolSort
p Expr t
t Expr t
f)        = (Bool -> HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe Bool
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
-> Maybe (HaskellType t)
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (\Bool
p' HaskellType t
t' HaskellType t
f' -> if Bool
p' then HaskellType t
t' else HaskellType t
f') (Solution -> Expr 'BoolSort -> Maybe (Decoded (Expr 'BoolSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'BoolSort
p) (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
t) (Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
f)
  decode Solution
sol (BvNot Expr ('BvSort n)
x)          = (Bitvec n -> Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bitvec n -> Bitvec n
forall b. Boolean b => b -> b
not (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x)
  decode Solution
sol (BvAnd Expr ('BvSort n)
x Expr ('BvSort n)
y)        = (Bitvec n -> Bitvec n -> Bitvec n)
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Bitvec n
forall b. Boolean b => b -> b -> b
(&&) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvOr Expr ('BvSort n)
x Expr ('BvSort n)
y)         = (Bitvec n -> Bitvec n -> Bitvec n)
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Bitvec n
forall b. Boolean b => b -> b -> b
(||) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvXor Expr ('BvSort n)
x Expr ('BvSort n)
y)        = (Bitvec n -> Bitvec n -> Bitvec n)
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Bitvec n
forall b. Boolean b => b -> b -> b
xor (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvNand Expr ('BvSort n)
x Expr ('BvSort n)
y)       = [Bitvec n] -> Bitvec n
forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
nand ([Bitvec n] -> Bitvec n) -> Maybe [Bitvec n] -> Maybe (Bitvec n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe (Bitvec n)] -> Maybe [Bitvec n]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA [Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x, Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y]
  decode Solution
sol (BvNor Expr ('BvSort n)
x Expr ('BvSort n)
y)        = [Bitvec n] -> Bitvec n
forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
nor  ([Bitvec n] -> Bitvec n) -> Maybe [Bitvec n] -> Maybe (Bitvec n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe (Bitvec n)] -> Maybe [Bitvec n]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA [Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x, Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y]
  decode Solution
sol (BvNeg Expr ('BvSort n)
x)          = (Bitvec n -> Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bitvec n -> Bitvec n
forall a. Num a => a -> a
negate (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x)
  decode Solution
sol (BvAdd Expr ('BvSort n)
x Expr ('BvSort n)
y)        = (Bitvec n -> Bitvec n -> Bitvec n)
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Bitvec n
forall a. Num a => a -> a -> a
(+) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvSub Expr ('BvSort n)
x Expr ('BvSort n)
y)        = (Bitvec n -> Bitvec n -> Bitvec n)
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (-) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvMul Expr ('BvSort n)
x Expr ('BvSort n)
y)        = (Bitvec n -> Bitvec n -> Bitvec n)
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Bitvec n
forall a. Num a => a -> a -> a
(*) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvuDiv Expr ('BvSort n)
x Expr ('BvSort n)
y)       = (Bitvec n -> Bitvec n -> Bitvec n)
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Bitvec n
forall a. Integral a => a -> a -> a
div (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvuRem Expr ('BvSort n)
x Expr ('BvSort n)
y)       = (Bitvec n -> Bitvec n -> Bitvec n)
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Bitvec n
forall a. Integral a => a -> a -> a
rem (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvShL Expr ('BvSort n)
x Expr ('BvSort n)
y)        = Maybe (Maybe (Decoded (Expr t))) -> Maybe (Decoded (Expr t))
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe (Decoded (Expr t))) -> Maybe (Decoded (Expr t)))
-> Maybe (Maybe (Decoded (Expr t))) -> Maybe (Decoded (Expr t))
forall a b. (a -> b) -> a -> b
$ (Bitvec n -> Bitvec n -> Maybe (Bitvec n))
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe (Maybe (Bitvec n))
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Maybe (Bitvec n)
forall (n :: Nat).
KnownNat n =>
Bitvec n -> Bitvec n -> Maybe (Bitvec n)
bvShL (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvLShR Expr ('BvSort n)
x Expr ('BvSort n)
y)       = Maybe (Maybe (Decoded (Expr t))) -> Maybe (Decoded (Expr t))
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe (Decoded (Expr t))) -> Maybe (Decoded (Expr t)))
-> Maybe (Maybe (Decoded (Expr t))) -> Maybe (Decoded (Expr t))
forall a b. (a -> b) -> a -> b
$ (Bitvec n -> Bitvec n -> Maybe (Bitvec n))
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe (Maybe (Bitvec n))
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Maybe (Bitvec n)
forall (n :: Nat).
KnownNat n =>
Bitvec n -> Bitvec n -> Maybe (Bitvec n)
bvLShR (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvConcat Expr ('BvSort n)
x Expr ('BvSort m)
y)     = (Bitvec n -> Bitvec m -> Bitvec (n + m))
-> Maybe (Bitvec n) -> Maybe (Bitvec m) -> Maybe (Bitvec (n + m))
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec m -> Bitvec (n + m)
forall (n :: Nat) (m :: Nat).
Bitvec n -> Bitvec m -> Bitvec (n + m)
bvConcat (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort m) -> Maybe (Decoded (Expr ('BvSort m)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort m)
y)
  decode Solution
sol (BvRotL Proxy i
i Expr ('BvSort n)
x)       = Proxy i -> Bitvec n -> Bitvec n
forall (n :: Nat) (i :: Nat).
KnownNat (Mod i n) =>
Proxy i -> Bitvec n -> Bitvec n
bvRotL Proxy i
i (Bitvec n -> Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x
  decode Solution
sol (BvRotR Proxy i
i Expr ('BvSort n)
x)       = Proxy i -> Bitvec n -> Bitvec n
forall (n :: Nat) (i :: Nat).
KnownNat (Mod i n) =>
Proxy i -> Bitvec n -> Bitvec n
bvRotR Proxy i
i (Bitvec n -> Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x
  decode Solution
sol (BvuLT Expr ('BvSort n)
x Expr ('BvSort n)
y)        = (Bitvec n -> Bitvec n -> Bool)
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe Bool
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Bool
forall a. Ord a => a -> a -> Bool
(<) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvuLTHE Expr ('BvSort n)
x Expr ('BvSort n)
y)      = (Bitvec n -> Bitvec n -> Bool)
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe Bool
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Bool
forall a. Ord a => a -> a -> Bool
(<=) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvuGTHE Expr ('BvSort n)
x Expr ('BvSort n)
y)      = (Bitvec n -> Bitvec n -> Bool)
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe Bool
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Bool
forall a. Ord a => a -> a -> Bool
(>=) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (BvuGT Expr ('BvSort n)
x Expr ('BvSort n)
y)        = (Bitvec n -> Bitvec n -> Bool)
-> Maybe (Bitvec n) -> Maybe (Bitvec n) -> Maybe Bool
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bitvec n -> Bitvec n -> Bool
forall a. Ord a => a -> a -> Bool
(>) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
x) (Solution -> Expr ('BvSort n) -> Maybe (Decoded (Expr ('BvSort n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort n)
y)
  decode Solution
sol (ArrSelect Expr ('ArraySort k t)
i Expr k
arr)  = (ConstArray (HaskellType k) (HaskellType t)
 -> HaskellType k -> HaskellType t)
-> Maybe (ConstArray (HaskellType k) (HaskellType t))
-> Maybe (HaskellType k)
-> Maybe (HaskellType t)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ConstArray (HaskellType k) (HaskellType t)
-> HaskellType k -> HaskellType t
forall (f :: * -> * -> *) k v. ArrayMap f k v => f k v -> k -> v
arrSelect (Solution
-> Expr ('ArraySort k t) -> Maybe (Decoded (Expr ('ArraySort k t)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('ArraySort k t)
i) (Solution -> Expr k -> Maybe (Decoded (Expr k))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr k
arr)
  decode Solution
sol (ArrStore Expr ('ArraySort k v)
i Expr k
x Expr v
arr) = (ConstArray (HaskellType k) (HaskellType v)
 -> HaskellType k
 -> HaskellType v
 -> ConstArray (HaskellType k) (HaskellType v))
-> Maybe (ConstArray (HaskellType k) (HaskellType v))
-> Maybe (HaskellType k)
-> Maybe (HaskellType v)
-> Maybe (ConstArray (HaskellType k) (HaskellType v))
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 ConstArray (HaskellType k) (HaskellType v)
-> HaskellType k
-> HaskellType v
-> ConstArray (HaskellType k) (HaskellType v)
forall (f :: * -> * -> *) k v.
ArrayMap f k v =>
f k v -> k -> v -> f k v
arrStore (Solution
-> Expr ('ArraySort k v) -> Maybe (Decoded (Expr ('ArraySort k v)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('ArraySort k v)
i) (Solution -> Expr k -> Maybe (Decoded (Expr k))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr k
x) (Solution -> Expr v -> Maybe (Decoded (Expr v))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr v
arr)
  decode Solution
_ (ForAll Maybe (SMTVar t1)
_ Expr t1 -> Expr 'BoolSort
_)         = Maybe Bool
Maybe (Decoded (Expr t))
forall a. Maybe a
Nothing
  decode Solution
_ (Exists Maybe (SMTVar t1)
_ Expr t1 -> Expr 'BoolSort
_)         = Maybe Bool
Maybe (Decoded (Expr t))
forall a. Maybe a
Nothing

  encode :: Decoded (Expr t) -> Expr t
encode = Value t -> Expr t
forall (t :: SMTSort). Value t -> Expr t
Constant (Value t -> Expr t)
-> (HaskellType t -> Value t) -> HaskellType t -> Expr t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue

instance Codec () where
  type Decoded () = ()
  decode :: Solution -> () -> Maybe (Decoded ())
decode Solution
_ ()
_ = () -> Maybe ()
forall a. a -> Maybe a
Just ()
  encode :: Decoded () -> ()
encode Decoded ()
_   = ()

instance (Codec a, Codec b) => Codec (a,b) where
  type Decoded (a,b) = (Decoded a, Decoded b)
  decode :: Solution -> (a, b) -> Maybe (Decoded (a, b))
decode Solution
s (a
a,b
b) = (,) (Decoded a -> Decoded b -> (Decoded a, Decoded b))
-> Maybe (Decoded a) -> Maybe (Decoded b -> (Decoded a, Decoded b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s a
a Maybe (Decoded b -> (Decoded a, Decoded b))
-> Maybe (Decoded b) -> Maybe (Decoded a, Decoded b)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> b -> Maybe (Decoded b)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s b
b
  encode :: Decoded (a, b) -> (a, b)
encode   (Decoded a
a,Decoded b
b) = (Decoded a -> a
forall a. Codec a => Decoded a -> a
encode Decoded a
a, Decoded b -> b
forall a. Codec a => Decoded a -> a
encode Decoded b
b)

instance (Codec a, Codec b, Codec c) => Codec (a,b,c) where
  type Decoded (a,b,c) = (Decoded a, Decoded b, Decoded c)
  decode :: Solution -> (a, b, c) -> Maybe (Decoded (a, b, c))
decode Solution
s (a
a,b
b,c
c) = (,,) (Decoded a
 -> Decoded b -> Decoded c -> (Decoded a, Decoded b, Decoded c))
-> Maybe (Decoded a)
-> Maybe
     (Decoded b -> Decoded c -> (Decoded a, Decoded b, Decoded c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s a
a Maybe (Decoded b -> Decoded c -> (Decoded a, Decoded b, Decoded c))
-> Maybe (Decoded b)
-> Maybe (Decoded c -> (Decoded a, Decoded b, Decoded c))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> b -> Maybe (Decoded b)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s b
b Maybe (Decoded c -> (Decoded a, Decoded b, Decoded c))
-> Maybe (Decoded c) -> Maybe (Decoded a, Decoded b, Decoded c)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> c -> Maybe (Decoded c)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s c
c
  encode :: Decoded (a, b, c) -> (a, b, c)
encode   (Decoded a
a,Decoded b
b,Decoded c
c) = (Decoded a -> a
forall a. Codec a => Decoded a -> a
encode Decoded a
a, Decoded b -> b
forall a. Codec a => Decoded a -> a
encode Decoded b
b, Decoded c -> c
forall a. Codec a => Decoded a -> a
encode Decoded c
c)

instance (Codec a, Codec b, Codec c, Codec d) => Codec (a,b,c,d) where
  type Decoded (a,b,c,d) = (Decoded a, Decoded b, Decoded c, Decoded d)
  decode :: Solution -> (a, b, c, d) -> Maybe (Decoded (a, b, c, d))
decode Solution
s (a
a,b
b,c
c,d
d) = (,,,) (Decoded a
 -> Decoded b
 -> Decoded c
 -> Decoded d
 -> (Decoded a, Decoded b, Decoded c, Decoded d))
-> Maybe (Decoded a)
-> Maybe
     (Decoded b
      -> Decoded c
      -> Decoded d
      -> (Decoded a, Decoded b, Decoded c, Decoded d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s a
a Maybe
  (Decoded b
   -> Decoded c
   -> Decoded d
   -> (Decoded a, Decoded b, Decoded c, Decoded d))
-> Maybe (Decoded b)
-> Maybe
     (Decoded c
      -> Decoded d -> (Decoded a, Decoded b, Decoded c, Decoded d))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> b -> Maybe (Decoded b)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s b
b Maybe
  (Decoded c
   -> Decoded d -> (Decoded a, Decoded b, Decoded c, Decoded d))
-> Maybe (Decoded c)
-> Maybe
     (Decoded d -> (Decoded a, Decoded b, Decoded c, Decoded d))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> c -> Maybe (Decoded c)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s c
c Maybe (Decoded d -> (Decoded a, Decoded b, Decoded c, Decoded d))
-> Maybe (Decoded d)
-> Maybe (Decoded a, Decoded b, Decoded c, Decoded d)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> d -> Maybe (Decoded d)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s d
d
  encode :: Decoded (a, b, c, d) -> (a, b, c, d)
encode   (Decoded a
a,Decoded b
b,Decoded c
c,Decoded d
d) = (Decoded a -> a
forall a. Codec a => Decoded a -> a
encode Decoded a
a, Decoded b -> b
forall a. Codec a => Decoded a -> a
encode Decoded b
b, Decoded c -> c
forall a. Codec a => Decoded a -> a
encode Decoded c
c, Decoded d -> d
forall a. Codec a => Decoded a -> a
encode Decoded d
d)

instance (Codec a, Codec b, Codec c, Codec d, Codec e) => Codec (a,b,c,d,e) where
  type Decoded (a,b,c,d,e) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e)
  decode :: Solution -> (a, b, c, d, e) -> Maybe (Decoded (a, b, c, d, e))
decode Solution
s (a
a,b
b,c
c,d
d,e
e) = (,,,,) (Decoded a
 -> Decoded b
 -> Decoded c
 -> Decoded d
 -> Decoded e
 -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e))
-> Maybe (Decoded a)
-> Maybe
     (Decoded b
      -> Decoded c
      -> Decoded d
      -> Decoded e
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s a
a Maybe
  (Decoded b
   -> Decoded c
   -> Decoded d
   -> Decoded e
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e))
-> Maybe (Decoded b)
-> Maybe
     (Decoded c
      -> Decoded d
      -> Decoded e
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> b -> Maybe (Decoded b)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s b
b Maybe
  (Decoded c
   -> Decoded d
   -> Decoded e
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e))
-> Maybe (Decoded c)
-> Maybe
     (Decoded d
      -> Decoded e
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> c -> Maybe (Decoded c)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s c
c Maybe
  (Decoded d
   -> Decoded e
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e))
-> Maybe (Decoded d)
-> Maybe
     (Decoded e
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> d -> Maybe (Decoded d)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s d
d Maybe
  (Decoded e
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e))
-> Maybe (Decoded e)
-> Maybe (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> e -> Maybe (Decoded e)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s e
e
  encode :: Decoded (a, b, c, d, e) -> (a, b, c, d, e)
encode   (Decoded a
a,Decoded b
b,Decoded c
c,Decoded d
d,Decoded e
e) = (Decoded a -> a
forall a. Codec a => Decoded a -> a
encode Decoded a
a, Decoded b -> b
forall a. Codec a => Decoded a -> a
encode Decoded b
b, Decoded c -> c
forall a. Codec a => Decoded a -> a
encode Decoded c
c, Decoded d -> d
forall a. Codec a => Decoded a -> a
encode Decoded d
d, Decoded e -> e
forall a. Codec a => Decoded a -> a
encode Decoded e
e)

instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f) => Codec (a,b,c,d,e,f) where
  type Decoded (a,b,c,d,e,f) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f)
  decode :: Solution
-> (a, b, c, d, e, f) -> Maybe (Decoded (a, b, c, d, e, f))
decode Solution
s (a
a,b
b,c
c,d
d,e
e,f
f) = (,,,,,) (Decoded a
 -> Decoded b
 -> Decoded c
 -> Decoded d
 -> Decoded e
 -> Decoded f
 -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
     Decoded f))
-> Maybe (Decoded a)
-> Maybe
     (Decoded b
      -> Decoded c
      -> Decoded d
      -> Decoded e
      -> Decoded f
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s a
a Maybe
  (Decoded b
   -> Decoded c
   -> Decoded d
   -> Decoded e
   -> Decoded f
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f))
-> Maybe (Decoded b)
-> Maybe
     (Decoded c
      -> Decoded d
      -> Decoded e
      -> Decoded f
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> b -> Maybe (Decoded b)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s b
b Maybe
  (Decoded c
   -> Decoded d
   -> Decoded e
   -> Decoded f
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f))
-> Maybe (Decoded c)
-> Maybe
     (Decoded d
      -> Decoded e
      -> Decoded f
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> c -> Maybe (Decoded c)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s c
c Maybe
  (Decoded d
   -> Decoded e
   -> Decoded f
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f))
-> Maybe (Decoded d)
-> Maybe
     (Decoded e
      -> Decoded f
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> d -> Maybe (Decoded d)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s d
d Maybe
  (Decoded e
   -> Decoded f
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f))
-> Maybe (Decoded e)
-> Maybe
     (Decoded f
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> e -> Maybe (Decoded e)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s e
e Maybe
  (Decoded f
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f))
-> Maybe (Decoded f)
-> Maybe
     (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> f -> Maybe (Decoded f)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s f
f
  encode :: Decoded (a, b, c, d, e, f) -> (a, b, c, d, e, f)
encode   (Decoded a
a,Decoded b
b,Decoded c
c,Decoded d
d,Decoded e
e,Decoded f
f) = (Decoded a -> a
forall a. Codec a => Decoded a -> a
encode Decoded a
a, Decoded b -> b
forall a. Codec a => Decoded a -> a
encode Decoded b
b, Decoded c -> c
forall a. Codec a => Decoded a -> a
encode Decoded c
c, Decoded d -> d
forall a. Codec a => Decoded a -> a
encode Decoded d
d, Decoded e -> e
forall a. Codec a => Decoded a -> a
encode Decoded e
e, Decoded f -> f
forall a. Codec a => Decoded a -> a
encode Decoded f
f)

instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f, Codec g) => Codec (a,b,c,d,e,f,g) where
  type Decoded (a,b,c,d,e,f,g) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f, Decoded g)
  decode :: Solution
-> (a, b, c, d, e, f, g) -> Maybe (Decoded (a, b, c, d, e, f, g))
decode Solution
s (a
a,b
b,c
c,d
d,e
e,f
f,g
g) = (,,,,,,) (Decoded a
 -> Decoded b
 -> Decoded c
 -> Decoded d
 -> Decoded e
 -> Decoded f
 -> Decoded g
 -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
     Decoded f, Decoded g))
-> Maybe (Decoded a)
-> Maybe
     (Decoded b
      -> Decoded c
      -> Decoded d
      -> Decoded e
      -> Decoded f
      -> Decoded g
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s a
a Maybe
  (Decoded b
   -> Decoded c
   -> Decoded d
   -> Decoded e
   -> Decoded f
   -> Decoded g
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g))
-> Maybe (Decoded b)
-> Maybe
     (Decoded c
      -> Decoded d
      -> Decoded e
      -> Decoded f
      -> Decoded g
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> b -> Maybe (Decoded b)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s b
b Maybe
  (Decoded c
   -> Decoded d
   -> Decoded e
   -> Decoded f
   -> Decoded g
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g))
-> Maybe (Decoded c)
-> Maybe
     (Decoded d
      -> Decoded e
      -> Decoded f
      -> Decoded g
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> c -> Maybe (Decoded c)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s c
c Maybe
  (Decoded d
   -> Decoded e
   -> Decoded f
   -> Decoded g
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g))
-> Maybe (Decoded d)
-> Maybe
     (Decoded e
      -> Decoded f
      -> Decoded g
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> d -> Maybe (Decoded d)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s d
d Maybe
  (Decoded e
   -> Decoded f
   -> Decoded g
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g))
-> Maybe (Decoded e)
-> Maybe
     (Decoded f
      -> Decoded g
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> e -> Maybe (Decoded e)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s e
e Maybe
  (Decoded f
   -> Decoded g
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g))
-> Maybe (Decoded f)
-> Maybe
     (Decoded g
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> f -> Maybe (Decoded f)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s f
f Maybe
  (Decoded g
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g))
-> Maybe (Decoded g)
-> Maybe
     (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f,
      Decoded g)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> g -> Maybe (Decoded g)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s g
g
  encode :: Decoded (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g)
encode   (Decoded a
a,Decoded b
b,Decoded c
c,Decoded d
d,Decoded e
e,Decoded f
f,Decoded g
g) = (Decoded a -> a
forall a. Codec a => Decoded a -> a
encode Decoded a
a, Decoded b -> b
forall a. Codec a => Decoded a -> a
encode Decoded b
b, Decoded c -> c
forall a. Codec a => Decoded a -> a
encode Decoded c
c, Decoded d -> d
forall a. Codec a => Decoded a -> a
encode Decoded d
d, Decoded e -> e
forall a. Codec a => Decoded a -> a
encode Decoded e
e, Decoded f -> f
forall a. Codec a => Decoded a -> a
encode Decoded f
f, Decoded g -> g
forall a. Codec a => Decoded a -> a
encode Decoded g
g)

instance (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) where
  type Decoded (a,b,c,d,e,f,g,h) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f, Decoded g, Decoded h)
  decode :: Solution
-> (a, b, c, d, e, f, g, h)
-> Maybe (Decoded (a, b, c, d, e, f, g, h))
decode Solution
s (a
a,b
b,c
c,d
d,e
e,f
f,g
g,h
h) = (,,,,,,,) (Decoded a
 -> Decoded b
 -> Decoded c
 -> Decoded d
 -> Decoded e
 -> Decoded f
 -> Decoded g
 -> Decoded h
 -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
     Decoded f, Decoded g, Decoded h))
-> Maybe (Decoded a)
-> Maybe
     (Decoded b
      -> Decoded c
      -> Decoded d
      -> Decoded e
      -> Decoded f
      -> Decoded g
      -> Decoded h
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g, Decoded h))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s a
a Maybe
  (Decoded b
   -> Decoded c
   -> Decoded d
   -> Decoded e
   -> Decoded f
   -> Decoded g
   -> Decoded h
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g, Decoded h))
-> Maybe (Decoded b)
-> Maybe
     (Decoded c
      -> Decoded d
      -> Decoded e
      -> Decoded f
      -> Decoded g
      -> Decoded h
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g, Decoded h))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> b -> Maybe (Decoded b)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s b
b Maybe
  (Decoded c
   -> Decoded d
   -> Decoded e
   -> Decoded f
   -> Decoded g
   -> Decoded h
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g, Decoded h))
-> Maybe (Decoded c)
-> Maybe
     (Decoded d
      -> Decoded e
      -> Decoded f
      -> Decoded g
      -> Decoded h
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g, Decoded h))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> c -> Maybe (Decoded c)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s c
c Maybe
  (Decoded d
   -> Decoded e
   -> Decoded f
   -> Decoded g
   -> Decoded h
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g, Decoded h))
-> Maybe (Decoded d)
-> Maybe
     (Decoded e
      -> Decoded f
      -> Decoded g
      -> Decoded h
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g, Decoded h))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> d -> Maybe (Decoded d)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s d
d Maybe
  (Decoded e
   -> Decoded f
   -> Decoded g
   -> Decoded h
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g, Decoded h))
-> Maybe (Decoded e)
-> Maybe
     (Decoded f
      -> Decoded g
      -> Decoded h
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g, Decoded h))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> e -> Maybe (Decoded e)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s e
e Maybe
  (Decoded f
   -> Decoded g
   -> Decoded h
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g, Decoded h))
-> Maybe (Decoded f)
-> Maybe
     (Decoded g
      -> Decoded h
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g, Decoded h))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> f -> Maybe (Decoded f)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s f
f Maybe
  (Decoded g
   -> Decoded h
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g, Decoded h))
-> Maybe (Decoded g)
-> Maybe
     (Decoded h
      -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
          Decoded f, Decoded g, Decoded h))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> g -> Maybe (Decoded g)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s g
g Maybe
  (Decoded h
   -> (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e,
       Decoded f, Decoded g, Decoded h))
-> Maybe (Decoded h)
-> Maybe
     (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f,
      Decoded g, Decoded h)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> h -> Maybe (Decoded h)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s h
h
  encode :: Decoded (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h)
encode   (Decoded a
a,Decoded b
b,Decoded c
c,Decoded d
d,Decoded e
e,Decoded f
f,Decoded g
g,Decoded h
h) = (Decoded a -> a
forall a. Codec a => Decoded a -> a
encode Decoded a
a, Decoded b -> b
forall a. Codec a => Decoded a -> a
encode Decoded b
b, Decoded c -> c
forall a. Codec a => Decoded a -> a
encode Decoded c
c, Decoded d -> d
forall a. Codec a => Decoded a -> a
encode Decoded d
d, Decoded e -> e
forall a. Codec a => Decoded a -> a
encode Decoded e
e, Decoded f -> f
forall a. Codec a => Decoded a -> a
encode Decoded f
f, Decoded g -> g
forall a. Codec a => Decoded a -> a
encode Decoded g
g, Decoded h -> h
forall a. Codec a => Decoded a -> a
encode Decoded h
h)

instance Codec a => Codec [a]
instance Codec a => Codec (IntMap a)
instance Codec a => Codec (Map k a)
instance Codec a => Codec (Maybe a)
instance Codec a => Codec (Seq a)
instance Codec a => Codec (Tree a)

instance (Codec a, Codec b) => Codec (Either a b) where
  type Decoded (Either a b) = Either (Decoded a) (Decoded b)
  decode :: Solution -> Either a b -> Maybe (Decoded (Either a b))
decode Solution
s (Left  a
a) = Decoded a -> Either (Decoded a) (Decoded b)
forall a b. a -> Either a b
Left  (Decoded a -> Either (Decoded a) (Decoded b))
-> Maybe (Decoded a) -> Maybe (Either (Decoded a) (Decoded b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s a
a
  decode Solution
s (Right b
b) = Decoded b -> Either (Decoded a) (Decoded b)
forall a b. b -> Either a b
Right (Decoded b -> Either (Decoded a) (Decoded b))
-> Maybe (Decoded b) -> Maybe (Either (Decoded a) (Decoded b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> b -> Maybe (Decoded b)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
s b
b
  encode :: Decoded (Either a b) -> Either a b
encode   (Left  Decoded a
a) = a -> Either a b
forall a b. a -> Either a b
Left  (Decoded a -> a
forall a. Codec a => Decoded a -> a
encode Decoded a
a)
  encode   (Right Decoded b
b) = b -> Either a b
forall a b. b -> Either a b
Right (Decoded b -> b
forall a. Codec a => Decoded a -> a
encode Decoded b
b)