{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

{- |
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
@
-}
module Language.Hasmtlib.Codec
(
  -- * Class
  Codec(..)

  -- * Generics
, GCodec(..)
, DefaultDecoded
)
where

import Prelude hiding (not, (&&), (||), all, and)
import Language.Hasmtlib.Type.Bitvec
import Language.Hasmtlib.Type.Expr (Expr(..), SMTVar(..))
import Language.Hasmtlib.Type.Solution
import Language.Hasmtlib.Type.ArrayMap
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Type.Value
import Language.Hasmtlib.Boolean
import Data.Kind
import Data.Proxy
import Data.Coerce
import qualified Data.List as List
import Data.Bits hiding (And, Xor, xor)
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 Data.Array (Array, Ix)
import qualified Data.Text as Text
import Data.Monoid (Sum, Product, First, Last, Dual)
import qualified Data.Vector.Sized as V
import Control.Monad
import Control.Lens hiding (from, to)
import GHC.Generics
import GHC.TypeLits

-- | Computes a default 'Decoded' 'Type' by distributing 'Decoded' over it's type arguments.
type family DefaultDecoded a :: Type where
  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 ") = ... "
    )

-- | Lift values to SMT-Values or decode them.
--
--   You can derive an instance of this class if your type is 'Generic'.
class Codec a where
  -- | Result of decoding @a@.
  type Decoded a :: Type
  type Decoded a = DefaultDecoded a

  -- | Decode a value using given solution.
  decode :: Solution -> a -> Maybe (Decoded a)
  default decode :: (Generic a, Generic (Decoded a), GCodec (Rep a), GDecoded (Rep a) x ~ Rep (Decoded a) x) => Solution -> a -> Maybe (Decoded a)
  decode Solution
sol a
x = do
    GDecoded (Rep a) Any
gdecodedx <- Solution -> Rep a Any -> Maybe (GDecoded (Rep a) Any)
forall a. Solution -> Rep a a -> Maybe (GDecoded (Rep a) a)
forall (f :: * -> *) a.
GCodec f =>
Solution -> f a -> Maybe (GDecoded f a)
gdecode Solution
sol (Rep a Any -> Maybe (GDecoded (Rep a) Any))
-> Rep a Any -> Maybe (GDecoded (Rep a) Any)
forall a b. (a -> b) -> a -> b
$ a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x
    Decoded a -> Maybe (Decoded a)
forall a. a -> Maybe a
Just (Decoded a -> Maybe (Decoded a)) -> Decoded a -> Maybe (Decoded a)
forall a b. (a -> b) -> a -> b
$ Rep (Decoded a) Any -> Decoded a
forall a x. Generic a => Rep a x -> a
forall x. Rep (Decoded a) x -> Decoded a
to Rep (Decoded a) Any
GDecoded (Rep a) Any
gdecodedx

  -- | Encode a value as constant.
  encode :: Decoded a -> a
  default encode :: (Generic a, Generic (Decoded a), GCodec (Rep a), GDecoded (Rep a) x ~ Rep (Decoded a) x) => Decoded a -> a
  encode = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> (Decoded a -> Rep a Any) -> Decoded a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep (Decoded a) Any -> Rep a Any
GDecoded (Rep a) Any -> Rep a Any
forall a. GDecoded (Rep a) a -> Rep a a
forall (f :: * -> *) a. GCodec f => GDecoded f a -> f a
gencode (Rep (Decoded a) Any -> Rep a Any)
-> (Decoded a -> Rep (Decoded a) Any) -> Decoded a -> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decoded a -> Rep (Decoded a) Any
forall a x. Generic a => a -> Rep a x
forall x. Decoded a -> Rep (Decoded a) x
from

-- | 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
    let sungSort :: SSMTSort t
sungSort = forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t
    (IntValueMap IntMap (Value t)
m) <- case SSMTSort t
sungSort of
      SBvSort Proxy enc
enc Proxy n
n -> case Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
enc of
      -- Solution contains all BV as unsigned, if we have a Signed one we check the Unsigned ones and flip BvEnc
        SBvEnc enc
SUnsigned -> 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 SSMTSort t
sungSort Solution
sol
        SBvEnc enc
SSigned -> SSMTSort ('BvSort 'Unsigned n)
-> Solution -> Maybe (IntValueMap ('BvSort 'Unsigned n))
forall {k1} (k2 :: k1 -> *) (f :: k1 -> *) (v :: k1).
GCompare k2 =>
k2 v -> DMap k2 f -> Maybe (f v)
DMap.lookup (Proxy 'Unsigned -> Proxy n -> SSMTSort ('BvSort 'Unsigned n)
forall (enc :: BvEnc) (n :: Nat).
(KnownBvEnc enc, KnownNat n) =>
Proxy enc -> Proxy n -> SSMTSort ('BvSort enc n)
SBvSort (forall {k} (t :: k). Proxy t
forall (t :: BvEnc). Proxy t
Proxy @Unsigned) Proxy n
n) Solution
sol Maybe (IntValueMap ('BvSort 'Unsigned n))
-> (IntValueMap ('BvSort 'Unsigned n) -> IntValueMap t)
-> Maybe (IntValueMap t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
          \case (IntValueMap IntMap (Value ('BvSort 'Unsigned n))
ubvs) -> IntMap (Value ('BvSort 'Signed n))
-> IntValueMap ('BvSort 'Signed n)
forall (t :: SMTSort). IntMap (Value t) -> IntValueMap t
IntValueMap (IntMap (Value ('BvSort 'Signed n))
 -> IntValueMap ('BvSort 'Signed n))
-> IntMap (Value ('BvSort 'Signed n))
-> IntValueMap ('BvSort 'Signed n)
forall a b. (a -> b) -> a -> b
$ (Value ('BvSort 'Unsigned n) -> Value ('BvSort 'Signed n))
-> IntMap (Value ('BvSort 'Unsigned n))
-> IntMap (Value ('BvSort 'Signed n))
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\case (BvValue HaskellType ('BvSort enc n)
ubv) -> HaskellType ('BvSort 'Signed n) -> Value ('BvSort 'Signed n)
forall (enc :: BvEnc) (n :: Nat).
(KnownBvEnc enc, KnownNat n) =>
HaskellType ('BvSort enc n) -> Value ('BvSort enc n)
BvValue (HaskellType ('BvSort 'Signed n) -> Value ('BvSort 'Signed n))
-> HaskellType ('BvSort 'Signed n) -> Value ('BvSort 'Signed n)
forall a b. (a -> b) -> a -> b
$ Bitvec 'Unsigned n -> Bitvec 'Signed n
forall (enc :: BvEnc) (n :: Nat). Bitvec enc n -> Bitvec 'Signed n
asSigned Bitvec 'Unsigned n
HaskellType ('BvSort enc n)
ubv) IntMap (Value ('BvSort 'Unsigned n))
ubvs
      SSMTSort t
_ -> 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 SSMTSort t
sungSort 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
forall a. Num a => a -> a -> a
(+)   (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t -> HaskellType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x Maybe (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 (Minus Expr t
x Expr t
y)        = (-)   (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t -> HaskellType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x Maybe (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
forall a. Num a => a -> a -> a
(*)   (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t -> HaskellType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x Maybe (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 t
x Expr t
y)          = HaskellType t -> HaskellType t -> HaskellType t
forall a. Integral a => a -> a -> a
mod   (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t -> HaskellType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x Maybe (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 (Rem Expr t
x Expr t
y)          = HaskellType t -> HaskellType t -> HaskellType t
forall a. Integral a => a -> a -> a
rem   (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t -> HaskellType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x Maybe (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 (IDiv Expr t
x Expr t
y)         = HaskellType t -> HaskellType t -> HaskellType t
forall a. Integral a => a -> a -> a
div   (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t -> HaskellType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x Maybe (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 (Div Expr 'RealSort
x Expr 'RealSort
y)          = Double -> Double -> Double
forall a. Fractional a => a -> a -> a
(/)   (Double -> Double -> Double)
-> Maybe Double -> Maybe (Double -> Double)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr 'RealSort -> Maybe (Decoded (Expr 'RealSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'RealSort
x Maybe (Double -> Double) -> Maybe Double -> Maybe Double
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
forall a. Ord a => a -> a -> Bool
(<)   (HaskellType t1 -> HaskellType t1 -> Bool)
-> Maybe (HaskellType t1) -> Maybe (HaskellType t1 -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t1 -> Maybe (Decoded (Expr t1))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t1
x Maybe (HaskellType t1 -> Bool)
-> Maybe (HaskellType t1) -> Maybe Bool
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
forall a. Ord a => a -> a -> Bool
(<=)  (HaskellType t1 -> HaskellType t1 -> Bool)
-> Maybe (HaskellType t1) -> Maybe (HaskellType t1 -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t1 -> Maybe (Decoded (Expr t1))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t1
x Maybe (HaskellType t1 -> Bool)
-> Maybe (HaskellType t1) -> Maybe Bool
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
forall a. Ord a => a -> a -> Bool
(>=)  (HaskellType t1 -> HaskellType t1 -> Bool)
-> Maybe (HaskellType t1) -> Maybe (HaskellType t1 -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t1 -> Maybe (Decoded (Expr t1))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t1
x Maybe (HaskellType t1 -> Bool)
-> Maybe (HaskellType t1) -> Maybe Bool
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
forall a. Ord a => a -> a -> Bool
(>)   (HaskellType t1 -> HaskellType t1 -> Bool)
-> Maybe (HaskellType t1) -> Maybe (HaskellType t1 -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t1 -> Maybe (Decoded (Expr t1))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t1
x Maybe (HaskellType t1 -> Bool)
-> Maybe (HaskellType t1) -> Maybe Bool
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
forall b. Boolean b => b -> b -> b
(&&) (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t -> HaskellType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x Maybe (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
forall b. Boolean b => b -> b -> b
(||) (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t -> HaskellType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x Maybe (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
forall b. Boolean b => b -> b -> b
(==>) (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t -> HaskellType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x Maybe (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
forall b. Boolean b => b -> b -> b
xor   (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t -> HaskellType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
x Maybe (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
p' HaskellType t
t' HaskellType t
f' -> if Bool
p' then HaskellType t
t' else HaskellType t
f') (Bool -> HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe Bool
-> Maybe (HaskellType t -> HaskellType t -> HaskellType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr 'BoolSort -> Maybe (Decoded (Expr 'BoolSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'BoolSort
p Maybe (HaskellType t -> HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t -> HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
t Maybe (HaskellType t -> HaskellType t)
-> Maybe (HaskellType t) -> Maybe (HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 (BvNand Expr ('BvSort enc n)
x Expr ('BvSort enc n)
y)       = [Bitvec enc n] -> Bitvec enc n
forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
nand ([Bitvec enc n] -> Bitvec enc n)
-> Maybe [Bitvec enc n] -> Maybe (Bitvec enc n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe (Bitvec enc n)] -> Maybe [Bitvec enc 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 enc n) -> Maybe (Decoded (Expr ('BvSort enc n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort enc n)
x, Solution
-> Expr ('BvSort enc n) -> Maybe (Decoded (Expr ('BvSort enc n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort enc n)
y]
  decode Solution
sol (BvNor Expr ('BvSort enc n)
x Expr ('BvSort enc n)
y)        = [Bitvec enc n] -> Bitvec enc n
forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
nor  ([Bitvec enc n] -> Bitvec enc n)
-> Maybe [Bitvec enc n] -> Maybe (Bitvec enc n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe (Bitvec enc n)] -> Maybe [Bitvec enc 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 enc n) -> Maybe (Decoded (Expr ('BvSort enc n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort enc n)
x, Solution
-> Expr ('BvSort enc n) -> Maybe (Decoded (Expr ('BvSort enc n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort enc n)
y]
  decode Solution
sol (BvShL Expr ('BvSort enc n)
x Expr ('BvSort enc n)
y)        = do
    Bitvec enc n
x' <- Solution
-> Expr ('BvSort enc n) -> Maybe (Decoded (Expr ('BvSort enc n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort enc n)
x
    Bitvec enc n
y' <- Solution
-> Expr ('BvSort enc n) -> Maybe (Decoded (Expr ('BvSort enc n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort enc n)
y
    Bitvec enc n -> Maybe (Bitvec enc n)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bitvec enc n -> Maybe (Bitvec enc n))
-> Bitvec enc n -> Maybe (Bitvec enc n)
forall a b. (a -> b) -> a -> b
$ Bitvec enc n -> Key -> Bitvec enc n
forall a. Bits a => a -> Key -> a
shiftL Bitvec enc n
x' (Key -> Bitvec enc n) -> Key -> Bitvec enc n
forall a b. (a -> b) -> a -> b
$ Integer -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Bitvec enc n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec enc n
y')
  decode Solution
sol (BvLShR Expr ('BvSort 'Unsigned n)
x Expr ('BvSort 'Unsigned n)
y)       = do
    Bitvec 'Unsigned n
x' <- Solution
-> Expr ('BvSort 'Unsigned n)
-> Maybe (Decoded (Expr ('BvSort 'Unsigned n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort 'Unsigned n)
x
    Bitvec 'Unsigned n
y' <- Solution
-> Expr ('BvSort 'Unsigned n)
-> Maybe (Decoded (Expr ('BvSort 'Unsigned n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort 'Unsigned n)
y
    Bitvec 'Unsigned n -> Maybe (Bitvec 'Unsigned n)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bitvec 'Unsigned n -> Maybe (Bitvec 'Unsigned n))
-> Bitvec 'Unsigned n -> Maybe (Bitvec 'Unsigned n)
forall a b. (a -> b) -> a -> b
$ Bitvec 'Unsigned n -> Key -> Bitvec 'Unsigned n
forall a. Bits a => a -> Key -> a
shiftR Bitvec 'Unsigned n
x' (Key -> Bitvec 'Unsigned n) -> Key -> Bitvec 'Unsigned n
forall a b. (a -> b) -> a -> b
$ Integer -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Bitvec 'Unsigned n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec 'Unsigned n
y')
  decode Solution
sol (BvAShR Expr ('BvSort 'Signed n)
x Expr ('BvSort 'Signed n)
y)       = do
    Bitvec 'Signed n
x' <- Solution
-> Expr ('BvSort 'Signed n)
-> Maybe (Decoded (Expr ('BvSort 'Signed n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort 'Signed n)
x
    Bitvec 'Signed n
y' <- Solution
-> Expr ('BvSort 'Signed n)
-> Maybe (Decoded (Expr ('BvSort 'Signed n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort 'Signed n)
y
    Bitvec 'Signed n -> Maybe (Bitvec 'Signed n)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bitvec 'Signed n -> Maybe (Bitvec 'Signed n))
-> Bitvec 'Signed n -> Maybe (Bitvec 'Signed n)
forall a b. (a -> b) -> a -> b
$ Bitvec 'Signed n -> Key -> Bitvec 'Signed n
forall a. Bits a => a -> Key -> a
shiftR Bitvec 'Signed n
x' (Key -> Bitvec 'Signed n) -> Key -> Bitvec 'Signed n
forall a b. (a -> b) -> a -> b
$ Integer -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Bitvec 'Signed n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec 'Signed n
y')
  decode Solution
sol (BvConcat Expr ('BvSort enc n)
x Expr ('BvSort enc m)
y)     = Bitvec enc n -> Bitvec enc m -> Bitvec enc (n + m)
forall (enc :: BvEnc) (n :: Nat) (m :: Nat).
Bitvec enc n -> Bitvec enc m -> Bitvec enc (n + m)
bitvecConcat (Bitvec enc n -> Bitvec enc m -> Bitvec enc (n + m))
-> Maybe (Bitvec enc n)
-> Maybe (Bitvec enc m -> Bitvec enc (n + m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution
-> Expr ('BvSort enc n) -> Maybe (Decoded (Expr ('BvSort enc n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort enc n)
x Maybe (Bitvec enc m -> Bitvec enc (n + m))
-> Maybe (Bitvec enc m) -> Maybe (Bitvec enc (n + m))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution
-> Expr ('BvSort enc m) -> Maybe (Decoded (Expr ('BvSort enc m)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort enc m)
y
  decode Solution
sol (BvRotL a
i Expr ('BvSort enc n)
x)       = Bitvec enc n -> Key -> Bitvec enc n
forall a. Bits a => a -> Key -> a
rotateL (Bitvec enc n -> Key -> Bitvec enc n)
-> Maybe (Bitvec enc n) -> Maybe (Key -> Bitvec enc n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution
-> Expr ('BvSort enc n) -> Maybe (Decoded (Expr ('BvSort enc n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort enc n)
x Maybe (Key -> Bitvec enc n) -> Maybe Key -> Maybe (Bitvec enc n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Key -> Maybe Key
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
i)
  decode Solution
sol (BvRotR a
i Expr ('BvSort enc n)
x)       = Bitvec enc n -> Key -> Bitvec enc n
forall a. Bits a => a -> Key -> a
rotateR (Bitvec enc n -> Key -> Bitvec enc n)
-> Maybe (Bitvec enc n) -> Maybe (Key -> Bitvec enc n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution
-> Expr ('BvSort enc n) -> Maybe (Decoded (Expr ('BvSort enc n)))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr ('BvSort enc n)
x Maybe (Key -> Bitvec enc n) -> Maybe Key -> Maybe (Bitvec enc n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Key -> Maybe Key
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
i)
  decode Solution
sol (ArrSelect Expr ('ArraySort k t)
i Expr k
arr)  = ConstArray (HaskellType k) (HaskellType t)
-> HaskellType k -> HaskellType t
forall (f :: * -> * -> *) k v. ArrayMap f k v => f k v -> k -> v
arrSelect (ConstArray (HaskellType k) (HaskellType t)
 -> HaskellType k -> HaskellType t)
-> Maybe (ConstArray (HaskellType k) (HaskellType t))
-> Maybe (HaskellType k -> HaskellType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 Maybe (HaskellType k -> HaskellType t)
-> Maybe (HaskellType k) -> Maybe (HaskellType t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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)
forall (f :: * -> * -> *) k v.
ArrayMap f k v =>
f k v -> k -> v -> f k v
arrStore (ConstArray (HaskellType k) (HaskellType v)
 -> HaskellType k
 -> HaskellType v
 -> ConstArray (HaskellType k) (HaskellType v))
-> Maybe (ConstArray (HaskellType k) (HaskellType v))
-> Maybe
     (HaskellType k
      -> HaskellType v -> ConstArray (HaskellType k) (HaskellType v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 Maybe
  (HaskellType k
   -> HaskellType v -> ConstArray (HaskellType k) (HaskellType v))
-> Maybe (HaskellType k)
-> Maybe
     (HaskellType v -> ConstArray (HaskellType k) (HaskellType v))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr k -> Maybe (Decoded (Expr k))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr k
x Maybe (HaskellType v -> ConstArray (HaskellType k) (HaskellType v))
-> Maybe (HaskellType v)
-> Maybe (ConstArray (HaskellType k) (HaskellType v))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr v -> Maybe (Decoded (Expr v))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr v
arr
  decode Solution
sol (StrConcat Expr 'StringSort
x Expr 'StringSort
y)         = Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
(<>) (Text -> Text -> Text) -> Maybe Text -> Maybe (Text -> Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
x Maybe (Text -> Text) -> Maybe Text -> Maybe Text
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
y
  decode Solution
sol (StrLength Expr 'StringSort
x)           = Key -> Integer
forall a. Integral a => a -> Integer
toInteger (Key -> Integer) -> (Text -> Key) -> Text -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Key
Text.length (Text -> Integer) -> Maybe Text -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
x
  decode Solution
sol (StrAt Expr 'StringSort
x Expr 'IntSort
i)             = (\Text
x' Integer
i' -> Char -> Text
Text.singleton (Char -> Text) -> Char -> Text
forall a b. (a -> b) -> a -> b
$ HasCallStack => Text -> Key -> Char
Text -> Key -> Char
Text.index Text
x' (Integer -> Key
forall a. Num a => Integer -> a
fromInteger Integer
i')) (Text -> Integer -> Text) -> Maybe Text -> Maybe (Integer -> Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
x Maybe (Integer -> Text) -> Maybe Integer -> Maybe Text
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'IntSort -> Maybe (Decoded (Expr 'IntSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'IntSort
i
  decode Solution
sol (StrSubstring Expr 'StringSort
x Expr 'IntSort
i Expr 'IntSort
j)    = (\Text
x' (Integer -> Key
forall a. Num a => Integer -> a
fromInteger -> Key
i') (Integer -> Key
forall a. Num a => Integer -> a
fromInteger -> Key
j') -> Key -> Text -> Text
Text.take (Key
j' Key -> Key -> Key
forall a. Num a => a -> a -> a
- Key
i') (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Key -> Text -> Text
Text.drop Key
i' Text
x') (Text -> Integer -> Integer -> Text)
-> Maybe Text -> Maybe (Integer -> Integer -> Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
x Maybe (Integer -> Integer -> Text)
-> Maybe Integer -> Maybe (Integer -> Text)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'IntSort -> Maybe (Decoded (Expr 'IntSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'IntSort
i Maybe (Integer -> Text) -> Maybe Integer -> Maybe Text
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'IntSort -> Maybe (Decoded (Expr 'IntSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'IntSort
j
  decode Solution
sol (StrPrefixOf Expr 'StringSort
x Expr 'StringSort
y)       = Text -> Text -> Bool
Text.isPrefixOf (Text -> Text -> Bool) -> Maybe Text -> Maybe (Text -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
x Maybe (Text -> Bool) -> Maybe Text -> Maybe Bool
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
y
  decode Solution
sol (StrSuffixOf Expr 'StringSort
x Expr 'StringSort
y)       = Text -> Text -> Bool
Text.isSuffixOf (Text -> Text -> Bool) -> Maybe Text -> Maybe (Text -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
x Maybe (Text -> Bool) -> Maybe Text -> Maybe Bool
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
y
  decode Solution
sol (StrContains Expr 'StringSort
x Expr 'StringSort
y)       = (Text -> Text -> Bool) -> Text -> Text -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Text -> Text -> Bool
Text.isInfixOf (Text -> Text -> Bool) -> Maybe Text -> Maybe (Text -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
x Maybe (Text -> Bool) -> Maybe Text -> Maybe Bool
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
y
  decode Solution
sol (StrIndexOf Expr 'StringSort
x Expr 'StringSort
y Expr 'IntSort
i)      = 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
$ (\Text
x' Text
y' (Integer -> Key
forall a. Num a => Integer -> a
fromInteger -> Key
i') -> (Char -> Bool) -> Text -> Maybe Key
Text.findIndex ((Text
y' ==) (Text -> Bool) -> (Char -> Text) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Text
Text.singleton) (Key -> Text -> Text
Text.drop Key
i' Text
x') Maybe Key -> (Key -> Maybe Integer) -> Maybe Integer
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer)
-> (Key -> Integer) -> Key -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Key -> Integer
forall a. Integral a => a -> Integer
toInteger) (Text -> Text -> Integer -> Maybe Integer)
-> Maybe Text -> Maybe (Text -> Integer -> Maybe Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
x Maybe (Text -> Integer -> Maybe Integer)
-> Maybe Text -> Maybe (Integer -> Maybe Integer)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
y Maybe (Integer -> Maybe Integer)
-> Maybe Integer -> Maybe (Maybe Integer)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'IntSort -> Maybe (Decoded (Expr 'IntSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'IntSort
i
  decode Solution
sol (StrReplace Expr 'StringSort
src Expr 'StringSort
target Expr 'StringSort
replacement) = (\Text
src' Text
target' Text
replacement' -> Text -> Text -> Text -> Text
replaceOne Text
target' Text
replacement' Text
src') (Text -> Text -> Text -> Text)
-> Maybe Text -> Maybe (Text -> Text -> Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
target Maybe (Text -> Text -> Text) -> Maybe Text -> Maybe (Text -> Text)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
src Maybe (Text -> Text) -> Maybe Text -> Maybe Text
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
replacement
    where
      replaceOne :: Text -> Text -> Text -> Text
replaceOne Text
pattern Text
substitution Text
text
        | Text -> Bool
Text.null Text
back = Text
text
        | Bool
otherwise = [Text] -> Text
Text.concat [Text
front, Text
substitution, Key -> Text -> Text
Text.drop (Text -> Key
Text.length Text
pattern) Text
back]
          where
            (Text
front, Text
back) = HasCallStack => Text -> Text -> (Text, Text)
Text -> Text -> (Text, Text)
Text.breakOn Text
pattern Text
text
  decode Solution
sol (StrReplaceAll Expr 'StringSort
src Expr 'StringSort
target Expr 'StringSort
replacement) = (\Text
src' Text
target' Text
replacement' -> HasCallStack => Text -> Text -> Text -> Text
Text -> Text -> Text -> Text
Text.replace Text
target' Text
replacement' Text
src') (Text -> Text -> Text -> Text)
-> Maybe Text -> Maybe (Text -> Text -> Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
target Maybe (Text -> Text -> Text) -> Maybe Text -> Maybe (Text -> Text)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
src Maybe (Text -> Text) -> Maybe Text -> Maybe Text
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> Expr 'StringSort -> Maybe (Decoded (Expr 'StringSort))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr 'StringSort
replacement
  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 () = ()
instance (Codec a, Codec b) => Codec (a,b)
instance (Codec a, Codec b, Codec c) => Codec (a,b,c)
instance (Codec a, Codec b, Codec c, Codec d) => Codec (a,b,c,d)
instance (Codec a, Codec b, Codec c, Codec d, Codec e) => Codec (a,b,c,d,e)
instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f) => Codec (a,b,c,d,e,f)
instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f, Codec g) => Codec (a,b,c,d,e,f,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)
instance Codec a => Codec [a]
instance Codec a => Codec (Maybe a)
instance Codec a => Codec (Tree a)
instance (Codec a, Codec b) => Codec (Either a b)
instance Codec a => Codec (Sum a)
instance Codec a => Codec (Product a)
instance Codec a => Codec (First a)
instance Codec a => Codec (Last a)
instance Codec a => Codec (Dual a)
instance Codec a => Codec (Identity a)

instance Codec a => Codec (IntMap a) where
  decode :: Solution -> IntMap a -> Maybe (Decoded (IntMap a))
decode = (a -> Maybe (Decoded a)) -> IntMap a -> Maybe (IntMap (Decoded a))
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) -> IntMap a -> f (IntMap b)
traverse ((a -> Maybe (Decoded a))
 -> IntMap a -> Maybe (IntMap (Decoded a)))
-> (Solution -> a -> Maybe (Decoded a))
-> Solution
-> IntMap a
-> Maybe (IntMap (Decoded a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode
  encode :: Decoded (IntMap a) -> IntMap a
encode = (Decoded a -> a) -> IntMap (Decoded a) -> IntMap a
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Decoded a -> a
forall a. Codec a => Decoded a -> a
encode

instance Codec a => Codec (Seq a) where
  decode :: Solution -> Seq a -> Maybe (Decoded (Seq a))
decode = (a -> Maybe (Decoded a)) -> Seq a -> Maybe (Seq (Decoded a))
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) -> Seq a -> f (Seq b)
traverse ((a -> Maybe (Decoded a)) -> Seq a -> Maybe (Seq (Decoded a)))
-> (Solution -> a -> Maybe (Decoded a))
-> Solution
-> Seq a
-> Maybe (Seq (Decoded a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode
  encode :: Decoded (Seq a) -> Seq a
encode = (Decoded a -> a) -> Seq (Decoded a) -> Seq a
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Decoded a -> a
forall a. Codec a => Decoded a -> a
encode

instance Codec a => Codec (Map k a) where
  type Decoded (Map k a) = Map k (Decoded a)
  decode :: Solution -> Map k a -> Maybe (Decoded (Map k a))
decode = (a -> Maybe (Decoded a)) -> Map k a -> Maybe (Map k (Decoded a))
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) -> Map k a -> f (Map k b)
traverse ((a -> Maybe (Decoded a)) -> Map k a -> Maybe (Map k (Decoded a)))
-> (Solution -> a -> Maybe (Decoded a))
-> Solution
-> Map k a
-> Maybe (Map k (Decoded a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode
  encode :: Decoded (Map k a) -> Map k a
encode = (Decoded a -> a) -> Map k (Decoded a) -> Map k a
forall a b. (a -> b) -> Map k a -> Map k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Decoded a -> a
forall a. Codec a => Decoded a -> a
encode

instance (Ix i, Codec e) => Codec (Array i e) where
  type Decoded (Array i e) = Array i (Decoded e)
  decode :: Solution -> Array i e -> Maybe (Decoded (Array i e))
decode = (e -> Maybe (Decoded e))
-> Array i e -> Maybe (Array i (Decoded e))
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) -> Array i a -> f (Array i b)
traverse ((e -> Maybe (Decoded e))
 -> Array i e -> Maybe (Array i (Decoded e)))
-> (Solution -> e -> Maybe (Decoded e))
-> Solution
-> Array i e
-> Maybe (Array i (Decoded e))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Solution -> e -> Maybe (Decoded e)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode
  encode :: Decoded (Array i e) -> Array i e
encode = (Decoded e -> e) -> Array i (Decoded e) -> Array i e
forall a b. (a -> b) -> Array i a -> Array i b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Decoded e -> e
forall a. Codec a => Decoded a -> a
encode

class GCodec f where
  type GDecoded f :: Type -> Type
  gdecode :: Solution -> f a -> Maybe (GDecoded f a)
  gencode :: GDecoded f a -> f a

instance GCodec U1 where
  type GDecoded U1 = U1
  gdecode :: forall a. Solution -> U1 a -> Maybe (GDecoded U1 a)
gdecode Solution
_ U1 a
U1     = U1 a -> Maybe (U1 a)
forall a. a -> Maybe a
Just U1 a
forall k (p :: k). U1 p
U1
  gencode :: forall a. GDecoded U1 a -> U1 a
gencode          = U1 a -> U1 a
GDecoded U1 a -> U1 a
forall a. a -> a
id

instance GCodec V1 where
  type GDecoded V1 = V1
  gdecode :: forall a. Solution -> V1 a -> Maybe (GDecoded V1 a)
gdecode Solution
_        = V1 a -> Maybe (V1 a)
V1 a -> Maybe (GDecoded V1 a)
forall a. a -> Maybe a
Just
  gencode :: forall a. GDecoded V1 a -> V1 a
gencode          = V1 a -> V1 a
GDecoded V1 a -> V1 a
forall a. a -> a
id

instance (GCodec f, GCodec g) => GCodec (f :*: g) where
  type GDecoded (f :*: g) = (GDecoded f :*: GDecoded g)
  gdecode :: forall a. Solution -> (:*:) f g a -> Maybe (GDecoded (f :*: g) a)
gdecode Solution
sol (f a
a :*: g a
b)   = GDecoded f a -> GDecoded g a -> (:*:) (GDecoded f) (GDecoded g) a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (GDecoded f a -> GDecoded g a -> (:*:) (GDecoded f) (GDecoded g) a)
-> Maybe (GDecoded f a)
-> Maybe (GDecoded g a -> (:*:) (GDecoded f) (GDecoded g) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> f a -> Maybe (GDecoded f a)
forall a. Solution -> f a -> Maybe (GDecoded f a)
forall (f :: * -> *) a.
GCodec f =>
Solution -> f a -> Maybe (GDecoded f a)
gdecode Solution
sol f a
a Maybe (GDecoded g a -> (:*:) (GDecoded f) (GDecoded g) a)
-> Maybe (GDecoded g a)
-> Maybe ((:*:) (GDecoded f) (GDecoded g) a)
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 a -> Maybe (GDecoded g a)
forall a. Solution -> g a -> Maybe (GDecoded g a)
forall (f :: * -> *) a.
GCodec f =>
Solution -> f a -> Maybe (GDecoded f a)
gdecode Solution
sol g a
b
  gencode :: forall a. GDecoded (f :*: g) a -> (:*:) f g a
gencode (GDecoded f a
a :*: GDecoded g a
b)       = GDecoded f a -> f a
forall a. GDecoded f a -> f a
forall (f :: * -> *) a. GCodec f => GDecoded f a -> f a
gencode GDecoded f a
a f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: GDecoded g a -> g a
forall a. GDecoded g a -> g a
forall (f :: * -> *) a. GCodec f => GDecoded f a -> f a
gencode GDecoded g a
b

instance (GCodec f, GCodec g) => GCodec (f :+: g) where
  type GDecoded (f :+: g) = (GDecoded f :+: GDecoded g)
  gdecode :: forall a. Solution -> (:+:) f g a -> Maybe (GDecoded (f :+: g) a)
gdecode Solution
sol (L1 f a
a)      = GDecoded f a -> (:+:) (GDecoded f) (GDecoded g) a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (GDecoded f a -> (:+:) (GDecoded f) (GDecoded g) a)
-> Maybe (GDecoded f a)
-> Maybe ((:+:) (GDecoded f) (GDecoded g) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> f a -> Maybe (GDecoded f a)
forall a. Solution -> f a -> Maybe (GDecoded f a)
forall (f :: * -> *) a.
GCodec f =>
Solution -> f a -> Maybe (GDecoded f a)
gdecode Solution
sol f a
a
  gdecode Solution
sol (R1 g a
a)      = GDecoded g a -> (:+:) (GDecoded f) (GDecoded g) a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (GDecoded g a -> (:+:) (GDecoded f) (GDecoded g) a)
-> Maybe (GDecoded g a)
-> Maybe ((:+:) (GDecoded f) (GDecoded g) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> g a -> Maybe (GDecoded g a)
forall a. Solution -> g a -> Maybe (GDecoded g a)
forall (f :: * -> *) a.
GCodec f =>
Solution -> f a -> Maybe (GDecoded f a)
gdecode Solution
sol g a
a
  gencode :: forall a. GDecoded (f :+: g) a -> (:+:) f g a
gencode (L1 GDecoded f a
a)          = f a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f a -> (:+:) f g a) -> f a -> (:+:) f g a
forall a b. (a -> b) -> a -> b
$ GDecoded f a -> f a
forall a. GDecoded f a -> f a
forall (f :: * -> *) a. GCodec f => GDecoded f a -> f a
gencode GDecoded f a
a
  gencode (R1 GDecoded g a
a)          = g a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g a -> (:+:) f g a) -> g a -> (:+:) f g a
forall a b. (a -> b) -> a -> b
$ GDecoded g a -> g a
forall a. GDecoded g a -> g a
forall (f :: * -> *) a. GCodec f => GDecoded f a -> f a
gencode GDecoded g a
a

instance GCodec f => GCodec (M1 i c f) where
  type GDecoded (M1 i c f) = (M1 i c (GDecoded f))
  gdecode :: forall a. Solution -> M1 i c f a -> Maybe (GDecoded (M1 i c f) a)
gdecode Solution
sol (M1 f a
x)       = GDecoded f a -> M1 i c (GDecoded f) a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (GDecoded f a -> M1 i c (GDecoded f) a)
-> Maybe (GDecoded f a) -> Maybe (M1 i c (GDecoded f) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solution -> f a -> Maybe (GDecoded f a)
forall a. Solution -> f a -> Maybe (GDecoded f a)
forall (f :: * -> *) a.
GCodec f =>
Solution -> f a -> Maybe (GDecoded f a)
gdecode Solution
sol f a
x
  gencode :: forall a. GDecoded (M1 i c f) a -> M1 i c f a
gencode (M1 GDecoded f a
x)           = f a -> M1 i c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f a -> M1 i c f a) -> f a -> M1 i c f a
forall a b. (a -> b) -> a -> b
$ GDecoded f a -> f a
forall a. GDecoded f a -> f a
forall (f :: * -> *) a. GCodec f => GDecoded f a -> f a
gencode GDecoded f a
x

instance Codec a => GCodec (K1 i a) where
  type GDecoded (K1 i a) = K1 i (Decoded a)
  gdecode :: forall a. Solution -> K1 i a a -> Maybe (GDecoded (K1 i a) a)
gdecode Solution
sol (K1 a
a)     = Decoded a -> K1 i (Decoded a) a
forall k i c (p :: k). c -> K1 i c p
K1 (Decoded a -> K1 i (Decoded a) a)
-> Maybe (Decoded a) -> Maybe (K1 i (Decoded a) a)
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
sol a
a
  gencode :: forall a. GDecoded (K1 i a) a -> K1 i a a
gencode (K1 Decoded a
a)         = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> a -> K1 i a a
forall a b. (a -> b) -> a -> b
$ Decoded a -> a
forall a. Codec a => Decoded a -> a
encode Decoded a
a