{-# 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 Data.Word
import Data.Int
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)          = Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
(/)   (Rational -> Rational -> Rational)
-> Maybe Rational -> Maybe (Rational -> Rational)
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 (Rational -> Rational) -> Maybe Rational -> Maybe Rational
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                   = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$ Double -> Rational
forall a. Real a => a -> Rational
toRational Double
forall a. Floating a => a
pi
  decode Solution
sol (Sqrt Expr 'RealSort
x)           = (Rational -> Rational) -> Maybe Rational -> Maybe Rational
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Double -> Rational
forall a. Real a => a -> Rational
toRational (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
sqrt (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational @Double)  (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)            = (Rational -> Rational) -> Maybe Rational -> Maybe Rational
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Double -> Rational
forall a. Real a => a -> Rational
toRational (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
exp (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational @Double)   (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)            = (Rational -> Rational) -> Maybe Rational -> Maybe Rational
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Double -> Rational
forall a. Real a => a -> Rational
toRational (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
sin (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational @Double)   (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)            = (Rational -> Rational) -> Maybe Rational -> Maybe Rational
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Double -> Rational
forall a. Real a => a -> Rational
toRational (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
cos (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational @Double)   (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)            = (Rational -> Rational) -> Maybe Rational -> Maybe Rational
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Double -> Rational
forall a. Real a => a -> Rational
toRational (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
tan (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational @Double)   (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)           = (Rational -> Rational) -> Maybe Rational -> Maybe Rational
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Double -> Rational
forall a. Real a => a -> Rational
toRational (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
asin (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational @Double)  (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)           = (Rational -> Rational) -> Maybe Rational -> Maybe Rational
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Double -> Rational
forall a. Real a => a -> Rational
toRational (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
acos (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational @Double)  (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)           = (Rational -> Rational) -> Maybe Rational -> Maybe Rational
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Double -> Rational
forall a. Real a => a -> Rational
toRational (Double -> Rational)
-> (Rational -> Double) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
forall a. Floating a => a -> a
atan (Double -> Double) -> (Rational -> Double) -> Rational -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational @Double)  (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 -> Rational) -> Maybe Integer -> Maybe Rational
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Rational
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)          = (Rational -> Integer) -> Maybe Rational -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rational -> Integer
forall b. Integral b => Rational -> 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)          = (Rational -> Bool) -> Maybe Rational -> Maybe Bool
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Rational
0 ==) (Rational -> Bool) -> (Rational -> Rational) -> Rational -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, Rational) -> Rational
forall a b. (a, b) -> b
snd ((Integer, Rational) -> Rational)
-> (Rational -> (Integer, Rational)) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> (Integer, Rational)
forall b. Integral b => Rational -> (b, Rational)
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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