{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Language.Hasmtlib.Codec
(
Codec(..)
, 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
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 ") = ... "
)
class Codec a where
type Decoded a :: Type
type Decoded a = DefaultDecoded a
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 :: 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
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
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