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

module Language.Hasmtlib.Codec where

import Prelude hiding (not, (&&), (||), all, and)
import Language.Hasmtlib.Internal.Bitvec
import Language.Hasmtlib.Internal.Expr
import Language.Hasmtlib.Type.Solution
import Language.Hasmtlib.Type.ArrayMap
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Boolean
import Data.Kind
import Data.Coerce
import qualified Data.List as List
import Data.Map (Map)
import Data.Sequence (Seq)
import Data.IntMap as IM hiding (foldl)
import Data.Dependent.Map as DMap
import Data.Tree (Tree)
import qualified Data.Text as Text
import Data.Monoid (Sum, Product, First, Last, Dual)
import Data.Functor.Identity (Identity)
import qualified Data.Vector.Sized as V
import Control.Monad
import GHC.Generics
import GHC.TypeLits

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

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