{-# LANGUAGE UndecidableInstances #-}

module Language.Hasmtlib.Lens where

import Language.Hasmtlib.Internal.Expr
import Language.Hasmtlib.Type.Expr
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Equatable
import Language.Hasmtlib.Orderable
import Language.Hasmtlib.Iteable
import Data.GADT.Compare
import Control.Lens

type instance Index   (Expr StringSort) = Expr IntSort
type instance IxValue (Expr StringSort) = Expr StringSort

instance Ixed (Expr StringSort) where
  ix :: Index (Expr 'StringSort)
-> Traversal' (Expr 'StringSort) (IxValue (Expr 'StringSort))
ix Index (Expr 'StringSort)
i IxValue (Expr 'StringSort) -> f (IxValue (Expr 'StringSort))
f Expr 'StringSort
s = IxValue (Expr 'StringSort) -> f (IxValue (Expr 'StringSort))
f (Expr 'StringSort -> Expr 'IntSort -> Expr 'StringSort
strAt Expr 'StringSort
s Index (Expr 'StringSort)
Expr 'IntSort
i) f (Expr 'StringSort)
-> (Expr 'StringSort -> Expr 'StringSort) -> f (Expr 'StringSort)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Expr 'StringSort
a ->
    let l :: Expr 'StringSort
l = Expr 'StringSort
-> Expr 'IntSort -> Expr 'IntSort -> Expr 'StringSort
strSubstring Expr 'StringSort
a Expr 'IntSort
0 Index (Expr 'StringSort)
Expr 'IntSort
i
        r :: Expr 'StringSort
r = Expr 'StringSort
-> Expr 'IntSort -> Expr 'IntSort -> Expr 'StringSort
strSubstring Expr 'StringSort
a Index (Expr 'StringSort)
Expr 'IntSort
i (Expr 'StringSort -> Expr 'IntSort
strLength Expr 'StringSort
a)
     in Expr 'StringSort
l Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
forall a. Semigroup a => a -> a -> a
<> Expr 'StringSort
-> Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
strReplace Expr 'StringSort
r (Expr 'StringSort -> Expr 'IntSort -> Expr 'StringSort
strAt Expr 'StringSort
a Index (Expr 'StringSort)
Expr 'IntSort
i) Expr 'StringSort
s

instance AsEmpty (Expr StringSort) where
  _Empty :: Prism' (Expr 'StringSort) ()
_Empty = (() -> Expr 'StringSort)
-> (Expr 'StringSort -> Maybe ()) -> Prism' (Expr 'StringSort) ()
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    (Expr 'StringSort -> () -> Expr 'StringSort
forall a b. a -> b -> a
const Expr 'StringSort
forall a. Monoid a => a
mempty)
    (\Expr 'StringSort
s -> Expr 'BoolSort -> Maybe () -> Maybe () -> Maybe ()
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'StringSort
s Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
=== Expr 'StringSort
forall a. Monoid a => a
mempty) (() -> Maybe ()
forall a. a -> Maybe a
Just ()) Maybe ()
forall a. Maybe a
Nothing)

instance Prefixed (Expr StringSort) where
  prefixed :: Expr 'StringSort -> Prism' (Expr 'StringSort) (Expr 'StringSort)
prefixed Expr 'StringSort
p = (Expr 'StringSort -> Expr 'StringSort)
-> (Expr 'StringSort -> Maybe (Expr 'StringSort))
-> Prism' (Expr 'StringSort) (Expr 'StringSort)
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    (Expr 'StringSort
p <>)
    (\Expr 'StringSort
s -> Expr 'BoolSort
-> Maybe (Expr 'StringSort)
-> Maybe (Expr 'StringSort)
-> Maybe (Expr 'StringSort)
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'StringSort
p Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
`strPrefixOf` Expr 'StringSort
s) (Expr 'StringSort -> Maybe (Expr 'StringSort)
forall a. a -> Maybe a
Just (Expr 'StringSort -> Maybe (Expr 'StringSort))
-> Expr 'StringSort -> Maybe (Expr 'StringSort)
forall a b. (a -> b) -> a -> b
$ Expr 'StringSort
-> Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
strReplace Expr 'StringSort
s Expr 'StringSort
p Expr 'StringSort
forall a. Monoid a => a
mempty) Maybe (Expr 'StringSort)
forall a. Maybe a
Nothing)

instance Suffixed (Expr StringSort) where
  suffixed :: Expr 'StringSort -> Prism' (Expr 'StringSort) (Expr 'StringSort)
suffixed Expr 'StringSort
qs = (Expr 'StringSort -> Expr 'StringSort)
-> (Expr 'StringSort -> Maybe (Expr 'StringSort))
-> Prism' (Expr 'StringSort) (Expr 'StringSort)
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    (Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
forall a. Semigroup a => a -> a -> a
<> Expr 'StringSort
qs)
    (\Expr 'StringSort
s -> Expr 'BoolSort
-> Maybe (Expr 'StringSort)
-> Maybe (Expr 'StringSort)
-> Maybe (Expr 'StringSort)
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'StringSort
qs Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
`strSuffixOf` Expr 'StringSort
s) (Expr 'StringSort -> Maybe (Expr 'StringSort)
forall a. a -> Maybe a
Just (Expr 'StringSort -> Maybe (Expr 'StringSort))
-> Expr 'StringSort -> Maybe (Expr 'StringSort)
forall a b. (a -> b) -> a -> b
$ Expr 'StringSort
-> Expr 'IntSort -> Expr 'IntSort -> Expr 'StringSort
strSubstring Expr 'StringSort
s Expr 'IntSort
0 (Expr 'StringSort -> Expr 'IntSort
strLength Expr 'StringSort
s Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall a. Num a => a -> a -> a
- Expr 'StringSort -> Expr 'IntSort
strLength Expr 'StringSort
qs)) Maybe (Expr 'StringSort)
forall a. Maybe a
Nothing)

instance Cons (Expr StringSort) (Expr StringSort) (Expr StringSort) (Expr StringSort) where
  _Cons :: Prism
  (Expr 'StringSort)
  (Expr 'StringSort)
  (Expr 'StringSort, Expr 'StringSort)
  (Expr 'StringSort, Expr 'StringSort)
_Cons = ((Expr 'StringSort, Expr 'StringSort) -> Expr 'StringSort)
-> (Expr 'StringSort -> Maybe (Expr 'StringSort, Expr 'StringSort))
-> Prism
     (Expr 'StringSort)
     (Expr 'StringSort)
     (Expr 'StringSort, Expr 'StringSort)
     (Expr 'StringSort, Expr 'StringSort)
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    ((Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort)
-> (Expr 'StringSort, Expr 'StringSort) -> Expr 'StringSort
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
forall a. Semigroup a => a -> a -> a
(<>))
    (\Expr 'StringSort
s -> Expr 'BoolSort
-> Maybe (Expr 'StringSort, Expr 'StringSort)
-> Maybe (Expr 'StringSort, Expr 'StringSort)
-> Maybe (Expr 'StringSort, Expr 'StringSort)
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'StringSort -> Expr 'IntSort
strLength Expr 'StringSort
s Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
>? Expr 'IntSort
0) ((Expr 'StringSort, Expr 'StringSort)
-> Maybe (Expr 'StringSort, Expr 'StringSort)
forall a. a -> Maybe a
Just (Expr 'StringSort -> Expr 'IntSort -> Expr 'StringSort
strAt Expr 'StringSort
s Expr 'IntSort
0, Expr 'StringSort
-> Expr 'IntSort -> Expr 'IntSort -> Expr 'StringSort
strSubstring Expr 'StringSort
s Expr 'IntSort
1 (Expr 'StringSort -> Expr 'IntSort
strLength Expr 'StringSort
s))) Maybe (Expr 'StringSort, Expr 'StringSort)
forall a. Maybe a
Nothing)

instance Snoc (Expr StringSort) (Expr StringSort) (Expr StringSort) (Expr StringSort) where
  _Snoc :: Prism
  (Expr 'StringSort)
  (Expr 'StringSort)
  (Expr 'StringSort, Expr 'StringSort)
  (Expr 'StringSort, Expr 'StringSort)
_Snoc = ((Expr 'StringSort, Expr 'StringSort) -> Expr 'StringSort)
-> (Expr 'StringSort -> Maybe (Expr 'StringSort, Expr 'StringSort))
-> Prism
     (Expr 'StringSort)
     (Expr 'StringSort)
     (Expr 'StringSort, Expr 'StringSort)
     (Expr 'StringSort, Expr 'StringSort)
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    ((Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort)
-> (Expr 'StringSort, Expr 'StringSort) -> Expr 'StringSort
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
forall a. Semigroup a => a -> a -> a
(<>))
    (\Expr 'StringSort
s -> Expr 'BoolSort
-> Maybe (Expr 'StringSort, Expr 'StringSort)
-> Maybe (Expr 'StringSort, Expr 'StringSort)
-> Maybe (Expr 'StringSort, Expr 'StringSort)
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'StringSort -> Expr 'IntSort
strLength Expr 'StringSort
s Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
>? Expr 'IntSort
0) ((Expr 'StringSort, Expr 'StringSort)
-> Maybe (Expr 'StringSort, Expr 'StringSort)
forall a. a -> Maybe a
Just (Expr 'StringSort
-> Expr 'IntSort -> Expr 'IntSort -> Expr 'StringSort
strSubstring Expr 'StringSort
s Expr 'IntSort
0 (Expr 'StringSort -> Expr 'IntSort
strLength Expr 'StringSort
s Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall a. Num a => a -> a -> a
- Expr 'IntSort
1), Expr 'StringSort -> Expr 'IntSort -> Expr 'StringSort
strAt Expr 'StringSort
s (Expr 'StringSort -> Expr 'IntSort
strLength Expr 'StringSort
s Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall a. Num a => a -> a -> a
- Expr 'IntSort
1))) Maybe (Expr 'StringSort, Expr 'StringSort)
forall a. Maybe a
Nothing)

type instance Index   (Expr (ArraySort k v)) = Expr k
type instance IxValue (Expr (ArraySort k v)) = Expr v

instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Ixed (Expr (ArraySort k v)) where
  ix :: Index (Expr ('ArraySort k v))
-> Traversal'
     (Expr ('ArraySort k v)) (IxValue (Expr ('ArraySort k v)))
ix Index (Expr ('ArraySort k v))
i IxValue (Expr ('ArraySort k v))
-> f (IxValue (Expr ('ArraySort k v)))
f Expr ('ArraySort k v)
arr = IxValue (Expr ('ArraySort k v))
-> f (IxValue (Expr ('ArraySort k v)))
f (Expr ('ArraySort k v) -> Expr k -> Expr v
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Expr ('ArraySort k v) -> Expr k -> Expr v
select Expr ('ArraySort k v)
arr Index (Expr ('ArraySort k v))
Expr k
i) f (Expr v)
-> (Expr v -> Expr ('ArraySort k v)) -> f (Expr ('ArraySort k v))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
store Expr ('ArraySort k v)
arr Index (Expr ('ArraySort k v))
Expr k
i

-- | **Caution for quantified expressions:** 'plate-function' @f@ will only be applied if quantification already has taken place.(&&)
--   Therefore make sure 'quantify' has been run before.
--   Otherwise the quantified expression and therefore all it's sub-expressions will not have @f@ applied.
instance KnownSMTSort t => Plated (Expr t) where
  plate :: Traversal' (Expr t) (Expr t)
plate Expr t -> f (Expr t)
_ expr :: Expr t
expr@(Var SMTVar t
_)            = Expr t -> f (Expr t)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr t
expr
  plate Expr t -> f (Expr t)
_ expr :: Expr t
expr@(Constant Value t
_)       = Expr t -> f (Expr t)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr t
expr
  plate Expr t -> f (Expr t)
f (Plus Expr t
x Expr t
y)              = Expr t -> Expr t -> Expr t
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Plus (Expr t -> Expr t -> Expr t) -> f (Expr t) -> f (Expr t -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
x f (Expr t -> Expr t) -> f (Expr t) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
y
  plate Expr t -> f (Expr t)
f (Neg Expr t
x)                 = Expr t -> Expr t
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Neg (Expr t -> Expr t) -> f (Expr t) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
x
  plate Expr t -> f (Expr t)
f (Mul Expr t
x Expr t
y)               = Expr t -> Expr t -> Expr t
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Mul (Expr t -> Expr t -> Expr t) -> f (Expr t) -> f (Expr t -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
x f (Expr t -> Expr t) -> f (Expr t) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
y
  plate Expr t -> f (Expr t)
f (Abs Expr t
x)                 = Expr t -> Expr t
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Abs (Expr t -> Expr t) -> f (Expr t) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
x
  plate Expr t -> f (Expr t)
f (Mod Expr 'IntSort
x Expr 'IntSort
y)               = Expr 'IntSort -> Expr 'IntSort -> Expr t
Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
Mod (Expr 'IntSort -> Expr 'IntSort -> Expr t)
-> f (Expr 'IntSort) -> f (Expr 'IntSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'IntSort
x f (Expr 'IntSort -> Expr t) -> f (Expr 'IntSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr 'IntSort
y
  plate Expr t -> f (Expr t)
f (IDiv Expr 'IntSort
x Expr 'IntSort
y)              = Expr 'IntSort -> Expr 'IntSort -> Expr t
Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
IDiv (Expr 'IntSort -> Expr 'IntSort -> Expr t)
-> f (Expr 'IntSort) -> f (Expr 'IntSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'IntSort
x f (Expr 'IntSort -> Expr t) -> f (Expr 'IntSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr 'IntSort
y
  plate Expr t -> f (Expr t)
f (Div Expr 'RealSort
x Expr 'RealSort
y)               = Expr 'RealSort -> Expr 'RealSort -> Expr t
Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
Div (Expr 'RealSort -> Expr 'RealSort -> Expr t)
-> f (Expr 'RealSort) -> f (Expr 'RealSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'RealSort
x f (Expr 'RealSort -> Expr t) -> f (Expr 'RealSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr 'RealSort
y
  plate Expr t -> f (Expr t)
f (LTH Expr t1
x Expr t1
y)               = Expr t1 -> Expr t1 -> Expr t
Expr t1 -> Expr t1 -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
LTH (Expr t1 -> Expr t1 -> Expr t)
-> f (Expr t1) -> f (Expr t1 -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
x f (Expr t1 -> Expr t) -> f (Expr t1) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
y
  plate Expr t -> f (Expr t)
f (LTHE Expr t1
x Expr t1
y)              = Expr t1 -> Expr t1 -> Expr t
Expr t1 -> Expr t1 -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
LTHE (Expr t1 -> Expr t1 -> Expr t)
-> f (Expr t1) -> f (Expr t1 -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
x f (Expr t1 -> Expr t) -> f (Expr t1) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
y
  plate Expr t -> f (Expr t)
f (EQU Vector (n + 2) (Expr t1)
xs)                = Vector (n + 2) (Expr t1) -> Expr t
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
forall (t1 :: SMTSort) (n :: Nat).
(Eq (HaskellType t1), KnownSMTSort t1, KnownNat n) =>
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
EQU (Vector (n + 2) (Expr t1) -> Expr t)
-> f (Vector (n + 2) (Expr t1)) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t1 -> f (Expr t1))
-> Vector (n + 2) (Expr t1) -> f (Vector (n + 2) (Expr t1))
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)
-> Vector Vector (n + 2) a -> f (Vector Vector (n + 2) b)
traverse ((Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f) Vector (n + 2) (Expr t1)
xs
  plate Expr t -> f (Expr t)
f (Distinct Vector (n + 2) (Expr t1)
xs)           = Vector (n + 2) (Expr t1) -> Expr t
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
forall (t1 :: SMTSort) (n :: Nat).
(Eq (HaskellType t1), KnownSMTSort t1, KnownNat n) =>
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
Distinct (Vector (n + 2) (Expr t1) -> Expr t)
-> f (Vector (n + 2) (Expr t1)) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t1 -> f (Expr t1))
-> Vector (n + 2) (Expr t1) -> f (Vector (n + 2) (Expr t1))
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)
-> Vector Vector (n + 2) a -> f (Vector Vector (n + 2) b)
traverse ((Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f) Vector (n + 2) (Expr t1)
xs
  plate Expr t -> f (Expr t)
f (GTHE Expr t1
x Expr t1
y)              = Expr t1 -> Expr t1 -> Expr t
Expr t1 -> Expr t1 -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
GTHE (Expr t1 -> Expr t1 -> Expr t)
-> f (Expr t1) -> f (Expr t1 -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
x f (Expr t1 -> Expr t) -> f (Expr t1) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
y
  plate Expr t -> f (Expr t)
f (GTH Expr t1
x Expr t1
y)               = Expr t1 -> Expr t1 -> Expr t
Expr t1 -> Expr t1 -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
GTH (Expr t1 -> Expr t1 -> Expr t)
-> f (Expr t1) -> f (Expr t1 -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
x f (Expr t1 -> Expr t) -> f (Expr t1) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
y
  plate Expr t -> f (Expr t)
f (Not Expr t
x)                 = Expr t -> Expr t
forall (t :: SMTSort). Boolean (HaskellType t) => Expr t -> Expr t
Not (Expr t -> Expr t) -> f (Expr t) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t
x
  plate Expr t -> f (Expr t)
f (And Expr t
x Expr t
y)               = Expr t -> Expr t -> Expr t
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
And (Expr t -> Expr t -> Expr t) -> f (Expr t) -> f (Expr t -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t
x f (Expr t -> Expr t) -> f (Expr t) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t
y
  plate Expr t -> f (Expr t)
f (Or Expr t
x Expr t
y)                = Expr t -> Expr t -> Expr t
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
Or (Expr t -> Expr t -> Expr t) -> f (Expr t) -> f (Expr t -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t
x f (Expr t -> Expr t) -> f (Expr t) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t
y
  plate Expr t -> f (Expr t)
f (Impl Expr t
x Expr t
y)              = Expr t -> Expr t -> Expr t
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
Impl (Expr t -> Expr t -> Expr t) -> f (Expr t) -> f (Expr t -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t
x f (Expr t -> Expr t) -> f (Expr t) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t
y
  plate Expr t -> f (Expr t)
f (Xor Expr t
x Expr t
y)               = Expr t -> Expr t -> Expr t
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
Xor (Expr t -> Expr t -> Expr t) -> f (Expr t) -> f (Expr t -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t
x f (Expr t -> Expr t) -> f (Expr t) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t
y
  plate Expr t -> f (Expr t)
_ Expr t
Pi                      = Expr t -> f (Expr t)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr t
Expr 'RealSort
Pi
  plate Expr t -> f (Expr t)
f (Sqrt Expr 'RealSort
x)                = Expr 'RealSort -> Expr t
Expr 'RealSort -> Expr 'RealSort
Sqrt (Expr 'RealSort -> Expr t) -> f (Expr 'RealSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'RealSort
x
  plate Expr t -> f (Expr t)
f (Exp Expr 'RealSort
x)                 = Expr 'RealSort -> Expr t
Expr 'RealSort -> Expr 'RealSort
Exp (Expr 'RealSort -> Expr t) -> f (Expr 'RealSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'RealSort
x
  plate Expr t -> f (Expr t)
f (Sin Expr 'RealSort
x)                 = Expr 'RealSort -> Expr t
Expr 'RealSort -> Expr 'RealSort
Sin (Expr 'RealSort -> Expr t) -> f (Expr 'RealSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'RealSort
x
  plate Expr t -> f (Expr t)
f (Cos Expr 'RealSort
x)                 = Expr 'RealSort -> Expr t
Expr 'RealSort -> Expr 'RealSort
Cos (Expr 'RealSort -> Expr t) -> f (Expr 'RealSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'RealSort
x
  plate Expr t -> f (Expr t)
f (Tan Expr 'RealSort
x)                 = Expr 'RealSort -> Expr t
Expr 'RealSort -> Expr 'RealSort
Tan (Expr 'RealSort -> Expr t) -> f (Expr 'RealSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'RealSort
x
  plate Expr t -> f (Expr t)
f (Asin Expr 'RealSort
x)                = Expr 'RealSort -> Expr t
Expr 'RealSort -> Expr 'RealSort
Asin (Expr 'RealSort -> Expr t) -> f (Expr 'RealSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'RealSort
x
  plate Expr t -> f (Expr t)
f (Acos Expr 'RealSort
x)                = Expr 'RealSort -> Expr t
Expr 'RealSort -> Expr 'RealSort
Acos (Expr 'RealSort -> Expr t) -> f (Expr 'RealSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'RealSort
x
  plate Expr t -> f (Expr t)
f (Atan Expr 'RealSort
x)                = Expr 'RealSort -> Expr t
Expr 'RealSort -> Expr 'RealSort
Atan (Expr 'RealSort -> Expr t) -> f (Expr 'RealSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'RealSort
x
  plate Expr t -> f (Expr t)
f (ToReal Expr 'IntSort
x)              = Expr 'IntSort -> Expr t
Expr 'IntSort -> Expr 'RealSort
ToReal (Expr 'IntSort -> Expr t) -> f (Expr 'IntSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
x
  plate Expr t -> f (Expr t)
f (ToInt Expr 'RealSort
x)               = Expr 'RealSort -> Expr t
Expr 'RealSort -> Expr 'IntSort
ToInt (Expr 'RealSort -> Expr t) -> f (Expr 'RealSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x
  plate Expr t -> f (Expr t)
f (IsInt Expr 'RealSort
x)               = Expr 'RealSort -> Expr t
Expr 'RealSort -> Expr 'BoolSort
IsInt (Expr 'RealSort -> Expr t) -> f (Expr 'RealSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x
  plate Expr t -> f (Expr t)
f (Ite Expr 'BoolSort
p Expr t
t Expr t
n)             = Expr 'BoolSort -> Expr t -> Expr t -> Expr t
forall (t :: SMTSort). Expr 'BoolSort -> Expr t -> Expr t -> Expr t
Ite (Expr 'BoolSort -> Expr t -> Expr t -> Expr t)
-> f (Expr 'BoolSort) -> f (Expr t -> Expr t -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'BoolSort
p f (Expr t -> Expr t -> Expr t)
-> f (Expr t) -> f (Expr t -> Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
t f (Expr t -> Expr t) -> f (Expr t) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
n
  plate Expr t -> f (Expr t)
f (BvNot Expr ('BvSort n)
x)               = Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n)
BvNot (Expr ('BvSort n) -> Expr t) -> f (Expr ('BvSort n)) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x
  plate Expr t -> f (Expr t)
f (BvAnd Expr ('BvSort n)
x Expr ('BvSort n)
y)             = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvAnd (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvOr Expr ('BvSort n)
x Expr ('BvSort n)
y)              = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvOr (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvXor Expr ('BvSort n)
x Expr ('BvSort n)
y)             = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvXor (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvNand Expr ('BvSort n)
x Expr ('BvSort n)
y)            = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvNand (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvNor Expr ('BvSort n)
x Expr ('BvSort n)
y)             = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvNor (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvNeg Expr ('BvSort n)
x)               = Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n)
BvNeg (Expr ('BvSort n) -> Expr t) -> f (Expr ('BvSort n)) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x
  plate Expr t -> f (Expr t)
f (BvAdd Expr ('BvSort n)
x Expr ('BvSort n)
y)             = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvAdd (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvSub Expr ('BvSort n)
x Expr ('BvSort n)
y)             = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvSub (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvMul Expr ('BvSort n)
x Expr ('BvSort n)
y)             = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvMul (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvuDiv Expr ('BvSort n)
x Expr ('BvSort n)
y)            = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuDiv (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvuRem Expr ('BvSort n)
x Expr ('BvSort n)
y)            = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuRem (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvShL Expr ('BvSort n)
x Expr ('BvSort n)
y)             = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvShL (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvLShR Expr ('BvSort n)
x Expr ('BvSort n)
y)            = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvLShR (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvConcat Expr ('BvSort n)
x Expr ('BvSort m)
y)          = Expr ('BvSort n) -> Expr ('BvSort m) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort m) -> Expr ('BvSort (n + m))
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Expr ('BvSort n) -> Expr ('BvSort m) -> Expr ('BvSort (n + m))
BvConcat (Expr ('BvSort n) -> Expr ('BvSort m) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort m) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort m) -> Expr t)
-> f (Expr ('BvSort m)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort m)
y
  plate Expr t -> f (Expr t)
f (BvRotL Proxy i
i Expr ('BvSort n)
x)            = Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat) (i :: Nat).
(KnownNat n, KnownNat i, KnownNat (Mod i n)) =>
Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
BvRotL Proxy i
i (Expr ('BvSort n) -> Expr t) -> f (Expr ('BvSort n)) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x
  plate Expr t -> f (Expr t)
f (BvRotR Proxy i
i Expr ('BvSort n)
x)            = Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat) (i :: Nat).
(KnownNat n, KnownNat i, KnownNat (Mod i n)) =>
Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
BvRotR Proxy i
i (Expr ('BvSort n) -> Expr t) -> f (Expr ('BvSort n)) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr ('BvSort n)
x
  plate Expr t -> f (Expr t)
f (BvuLT Expr ('BvSort n)
x Expr ('BvSort n)
y)             = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
BvuLT (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvuLTHE Expr ('BvSort n)
x Expr ('BvSort n)
y)           = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
BvuLTHE (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvuGTHE Expr ('BvSort n)
x Expr ('BvSort n)
y)           = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
BvuGTHE (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (BvuGT Expr ('BvSort n)
x Expr ('BvSort n)
y)             = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
BvuGT (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr t)
-> f (Expr ('BvSort n)) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
  plate Expr t -> f (Expr t)
f (ArrSelect Expr ('ArraySort k t)
i Expr k
arr)       = Expr ('ArraySort k t) -> Expr k -> Expr t
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Expr ('ArraySort k v) -> Expr k -> Expr v
ArrSelect Expr ('ArraySort k t)
i (Expr k -> Expr t) -> f (Expr k) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr k
arr
  plate Expr t -> f (Expr t)
f (ArrStore Expr ('ArraySort k v)
i Expr k
x Expr v
arr)      = Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
ArrStore Expr ('ArraySort k v)
i (Expr k -> Expr v -> Expr t) -> f (Expr k) -> f (Expr v -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr k
x f (Expr v -> Expr t) -> f (Expr v) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr v
arr
  plate Expr t -> f (Expr t)
f (StrConcat Expr 'StringSort
x Expr 'StringSort
y)         = Expr 'StringSort -> Expr 'StringSort -> Expr t
Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
StrConcat (Expr 'StringSort -> Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'StringSort
x f (Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr 'StringSort
y
  plate Expr t -> f (Expr t)
f (StrLength Expr 'StringSort
x)           = Expr 'StringSort -> Expr t
Expr 'StringSort -> Expr 'IntSort
StrLength (Expr 'StringSort -> Expr t) -> f (Expr 'StringSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x
  plate Expr t -> f (Expr t)
f (StrLT Expr 'StringSort
x Expr 'StringSort
y)             = Expr 'StringSort -> Expr 'StringSort -> Expr t
Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
StrLT (Expr 'StringSort -> Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y
  plate Expr t -> f (Expr t)
f (StrLTHE Expr 'StringSort
x Expr 'StringSort
y)           = Expr 'StringSort -> Expr 'StringSort -> Expr t
Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
StrLTHE (Expr 'StringSort -> Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y
  plate Expr t -> f (Expr t)
f (StrAt Expr 'StringSort
x Expr 'IntSort
i)             = Expr 'StringSort -> Expr 'IntSort -> Expr t
Expr 'StringSort -> Expr 'IntSort -> Expr 'StringSort
StrAt (Expr 'StringSort -> Expr 'IntSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr 'IntSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'StringSort
x f (Expr 'IntSort -> Expr t) -> f (Expr 'IntSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
i
  plate Expr t -> f (Expr t)
f (StrSubstring Expr 'StringSort
x Expr 'IntSort
i Expr 'IntSort
j)    = Expr 'StringSort -> Expr 'IntSort -> Expr 'IntSort -> Expr t
Expr 'StringSort
-> Expr 'IntSort -> Expr 'IntSort -> Expr 'StringSort
StrSubstring (Expr 'StringSort -> Expr 'IntSort -> Expr 'IntSort -> Expr t)
-> f (Expr 'StringSort)
-> f (Expr 'IntSort -> Expr 'IntSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'StringSort
x f (Expr 'IntSort -> Expr 'IntSort -> Expr t)
-> f (Expr 'IntSort) -> f (Expr 'IntSort -> Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
i f (Expr 'IntSort -> Expr t) -> f (Expr 'IntSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
j
  plate Expr t -> f (Expr t)
f (StrPrefixOf Expr 'StringSort
x Expr 'StringSort
y)       = Expr 'StringSort -> Expr 'StringSort -> Expr t
Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
StrPrefixOf (Expr 'StringSort -> Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y
  plate Expr t -> f (Expr t)
f (StrSuffixOf Expr 'StringSort
x Expr 'StringSort
y)       = Expr 'StringSort -> Expr 'StringSort -> Expr t
Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
StrSuffixOf (Expr 'StringSort -> Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y
  plate Expr t -> f (Expr t)
f (StrContains Expr 'StringSort
x Expr 'StringSort
y)       = Expr 'StringSort -> Expr 'StringSort -> Expr t
Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
StrContains (Expr 'StringSort -> Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y
  plate Expr t -> f (Expr t)
f (StrIndexOf Expr 'StringSort
x Expr 'StringSort
y Expr 'IntSort
i)      = Expr 'StringSort -> Expr 'StringSort -> Expr 'IntSort -> Expr t
Expr 'StringSort
-> Expr 'StringSort -> Expr 'IntSort -> Expr 'IntSort
StrIndexOf (Expr 'StringSort -> Expr 'StringSort -> Expr 'IntSort -> Expr t)
-> f (Expr 'StringSort)
-> f (Expr 'StringSort -> Expr 'IntSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr 'IntSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr 'IntSort -> Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y f (Expr 'IntSort -> Expr t) -> f (Expr 'IntSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr 'IntSort
i
  plate Expr t -> f (Expr t)
f (StrReplace Expr 'StringSort
x Expr 'StringSort
y Expr 'StringSort
y')     = Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort -> Expr t
Expr 'StringSort
-> Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
StrReplace (Expr 'StringSort
 -> Expr 'StringSort -> Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort)
-> f (Expr 'StringSort -> Expr 'StringSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'StringSort
x f (Expr 'StringSort -> Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr 'StringSort
y f (Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr 'StringSort
y'
  plate Expr t -> f (Expr t)
f (StrReplaceAll Expr 'StringSort
x Expr 'StringSort
y Expr 'StringSort
y')  = Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort -> Expr t
Expr 'StringSort
-> Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
StrReplaceAll (Expr 'StringSort
 -> Expr 'StringSort -> Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort)
-> f (Expr 'StringSort -> Expr 'StringSort -> Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t -> f (Expr t)
f Expr t
Expr 'StringSort
x f (Expr 'StringSort -> Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr 'StringSort
y f (Expr 'StringSort -> Expr t)
-> f (Expr 'StringSort) -> f (Expr t)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr t -> f (Expr t)
f Expr t
Expr 'StringSort
y'
  plate Expr t -> f (Expr t)
f (ForAll (Just SMTVar t1
qv) Expr t1 -> Expr 'BoolSort
expr) = Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
forall (t1 :: SMTSort).
KnownSMTSort t1 =>
Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
ForAll (SMTVar t1 -> Maybe (SMTVar t1)
forall a. a -> Maybe a
Just SMTVar t1
qv) ((Expr t1 -> Expr 'BoolSort) -> Expr t)
-> (Expr 'BoolSort -> Expr t1 -> Expr 'BoolSort)
-> Expr 'BoolSort
-> Expr t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'BoolSort -> Expr t1 -> Expr 'BoolSort
forall a b. a -> b -> a
const (Expr 'BoolSort -> Expr t) -> f (Expr 'BoolSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f (Expr t1 -> Expr 'BoolSort
expr (SMTVar t1 -> Expr t1
forall (t :: SMTSort). SMTVar t -> Expr t
Var SMTVar t1
qv))
  plate Expr t -> f (Expr t)
_ (ForAll Maybe (SMTVar t1)
Nothing Expr t1 -> Expr 'BoolSort
expr)   = Expr 'BoolSort -> f (Expr 'BoolSort)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'BoolSort -> f (Expr 'BoolSort))
-> Expr 'BoolSort -> f (Expr 'BoolSort)
forall a b. (a -> b) -> a -> b
$ Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
forall (t1 :: SMTSort).
KnownSMTSort t1 =>
Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
ForAll Maybe (SMTVar t1)
forall a. Maybe a
Nothing Expr t1 -> Expr 'BoolSort
expr
  plate Expr t -> f (Expr t)
f (Exists (Just SMTVar t1
qv) Expr t1 -> Expr 'BoolSort
expr) = Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
forall (t1 :: SMTSort).
KnownSMTSort t1 =>
Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
Exists (SMTVar t1 -> Maybe (SMTVar t1)
forall a. a -> Maybe a
Just SMTVar t1
qv) ((Expr t1 -> Expr 'BoolSort) -> Expr t)
-> (Expr 'BoolSort -> Expr t1 -> Expr 'BoolSort)
-> Expr 'BoolSort
-> Expr t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'BoolSort -> Expr t1 -> Expr 'BoolSort
forall a b. a -> b -> a
const (Expr 'BoolSort -> Expr t) -> f (Expr 'BoolSort) -> f (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f (Expr t1 -> Expr 'BoolSort
expr (SMTVar t1 -> Expr t1
forall (t :: SMTSort). SMTVar t -> Expr t
Var SMTVar t1
qv))
  plate Expr t -> f (Expr t)
_ (Exists Maybe (SMTVar t1)
Nothing Expr t1 -> Expr 'BoolSort
expr)   = Expr 'BoolSort -> f (Expr 'BoolSort)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'BoolSort -> f (Expr 'BoolSort))
-> Expr 'BoolSort -> f (Expr 'BoolSort)
forall a b. (a -> b) -> a -> b
$ Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
forall (t1 :: SMTSort).
KnownSMTSort t1 =>
Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
Exists Maybe (SMTVar t1)
forall a. Maybe a
Nothing Expr t1 -> Expr 'BoolSort
expr

-- | Apply the 'plate'-function @f@ for given 'Expr' @expr@ if possible.
--   Otherwise try to apply @f@ for the children of @expr@.
--   **Caution for quantified expressions:** 'plate-function' @f@ will only be applied if quantification already has taken place.(&&)
--   Therefore make sure 'quantify' has been run before.
--   Otherwise the quantified expression and therefore all it's sub-expressions will not have @f@ applied.
somePlate :: forall t f. (KnownSMTSort t, Applicative f) => (Expr t -> f (Expr t)) -> (forall s. KnownSMTSort s => Expr s -> f (Expr s))
somePlate :: forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
expr = case SSMTSort t -> SSMTSort s -> Maybe (t :~: s)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: SMTSort) (b :: SMTSort).
SSMTSort a -> SSMTSort b -> Maybe (a :~: b)
geq (forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t) (Expr s -> SSMTSort s
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr s
expr) of
  Just t :~: s
Refl -> Expr t -> f (Expr t)
f Expr t
Expr s
expr
  Maybe (t :~: s)
Nothing   -> case Expr s
expr of
    Var SMTVar s
_                -> Expr s -> f (Expr s)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s
expr
    Constant Value s
_           -> Expr s -> f (Expr s)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s
expr
    Plus Expr s
x Expr s
y             -> Expr s -> Expr s -> Expr s
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Plus (Expr s -> Expr s -> Expr s) -> f (Expr s) -> f (Expr s -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
x f (Expr s -> Expr s) -> f (Expr s) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
y
    Neg Expr s
x                -> Expr s -> Expr s
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Neg  (Expr s -> Expr s) -> f (Expr s) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
x
    Mul Expr s
x Expr s
y              -> Expr s -> Expr s -> Expr s
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Mul  (Expr s -> Expr s -> Expr s) -> f (Expr s) -> f (Expr s -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
x f (Expr s -> Expr s) -> f (Expr s) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
y
    Abs Expr s
x                -> Expr s -> Expr s
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Abs  (Expr s -> Expr s) -> f (Expr s) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
x
    Mod Expr 'IntSort
x Expr 'IntSort
y              -> Expr 'IntSort -> Expr 'IntSort -> Expr s
Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
Mod  (Expr 'IntSort -> Expr 'IntSort -> Expr s)
-> f (Expr 'IntSort) -> f (Expr 'IntSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
x f (Expr 'IntSort -> Expr s) -> f (Expr 'IntSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
y
    IDiv Expr 'IntSort
x Expr 'IntSort
y             -> Expr 'IntSort -> Expr 'IntSort -> Expr s
Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
IDiv (Expr 'IntSort -> Expr 'IntSort -> Expr s)
-> f (Expr 'IntSort) -> f (Expr 'IntSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
x f (Expr 'IntSort -> Expr s) -> f (Expr 'IntSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
y
    Div Expr 'RealSort
x Expr 'RealSort
y              -> Expr 'RealSort -> Expr 'RealSort -> Expr s
Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
Div  (Expr 'RealSort -> Expr 'RealSort -> Expr s)
-> f (Expr 'RealSort) -> f (Expr 'RealSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x f (Expr 'RealSort -> Expr s) -> f (Expr 'RealSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
y
    LTH Expr t1
x Expr t1
y              -> Expr t1 -> Expr t1 -> Expr s
Expr t1 -> Expr t1 -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
LTH  (Expr t1 -> Expr t1 -> Expr s)
-> f (Expr t1) -> f (Expr t1 -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
x f (Expr t1 -> Expr s) -> f (Expr t1) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
y
    LTHE Expr t1
x Expr t1
y             -> Expr t1 -> Expr t1 -> Expr s
Expr t1 -> Expr t1 -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
LTHE (Expr t1 -> Expr t1 -> Expr s)
-> f (Expr t1) -> f (Expr t1 -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
x f (Expr t1 -> Expr s) -> f (Expr t1) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
y
    EQU Vector (n + 2) (Expr t1)
xs               -> Vector (n + 2) (Expr t1) -> Expr s
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
forall (t1 :: SMTSort) (n :: Nat).
(Eq (HaskellType t1), KnownSMTSort t1, KnownNat n) =>
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
EQU  (Vector (n + 2) (Expr t1) -> Expr s)
-> f (Vector (n + 2) (Expr t1)) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t1 -> f (Expr t1))
-> Vector (n + 2) (Expr t1) -> f (Vector (n + 2) (Expr t1))
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)
-> Vector Vector (n + 2) a -> f (Vector Vector (n + 2) b)
traverse ((Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f) Vector (n + 2) (Expr t1)
xs
    Distinct Vector (n + 2) (Expr t1)
xs          -> Vector (n + 2) (Expr t1) -> Expr s
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
forall (t1 :: SMTSort) (n :: Nat).
(Eq (HaskellType t1), KnownSMTSort t1, KnownNat n) =>
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
Distinct (Vector (n + 2) (Expr t1) -> Expr s)
-> f (Vector (n + 2) (Expr t1)) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t1 -> f (Expr t1))
-> Vector (n + 2) (Expr t1) -> f (Vector (n + 2) (Expr t1))
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)
-> Vector Vector (n + 2) a -> f (Vector Vector (n + 2) b)
traverse ((Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f) Vector (n + 2) (Expr t1)
xs
    GTHE Expr t1
x Expr t1
y             -> Expr t1 -> Expr t1 -> Expr s
Expr t1 -> Expr t1 -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
GTHE (Expr t1 -> Expr t1 -> Expr s)
-> f (Expr t1) -> f (Expr t1 -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
x f (Expr t1 -> Expr s) -> f (Expr t1) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
y
    GTH Expr t1
x Expr t1
y              -> Expr t1 -> Expr t1 -> Expr s
Expr t1 -> Expr t1 -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
GTH  (Expr t1 -> Expr t1 -> Expr s)
-> f (Expr t1) -> f (Expr t1 -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
x f (Expr t1 -> Expr s) -> f (Expr t1) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr t1
y
    Not Expr s
x                -> Expr s -> Expr s
forall (t :: SMTSort). Boolean (HaskellType t) => Expr t -> Expr t
Not  (Expr s -> Expr s) -> f (Expr s) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
x
    And Expr s
x Expr s
y              -> Expr s -> Expr s -> Expr s
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
And  (Expr s -> Expr s -> Expr s) -> f (Expr s) -> f (Expr s -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
x f (Expr s -> Expr s) -> f (Expr s) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
y
    Or Expr s
x Expr s
y               -> Expr s -> Expr s -> Expr s
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
Or   (Expr s -> Expr s -> Expr s) -> f (Expr s) -> f (Expr s -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
x f (Expr s -> Expr s) -> f (Expr s) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
y
    Impl Expr s
x Expr s
y             -> Expr s -> Expr s -> Expr s
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
Impl (Expr s -> Expr s -> Expr s) -> f (Expr s) -> f (Expr s -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
x f (Expr s -> Expr s) -> f (Expr s) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
y
    Xor Expr s
x Expr s
y              -> Expr s -> Expr s -> Expr s
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
Xor  (Expr s -> Expr s -> Expr s) -> f (Expr s) -> f (Expr s -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
x f (Expr s -> Expr s) -> f (Expr s) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
y
    Expr s
Pi                   -> Expr s -> f (Expr s)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s
Expr 'RealSort
Pi
    Sqrt Expr 'RealSort
x               -> Expr 'RealSort -> Expr s
Expr 'RealSort -> Expr 'RealSort
Sqrt (Expr 'RealSort -> Expr s) -> f (Expr 'RealSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x
    Exp Expr 'RealSort
x                -> Expr 'RealSort -> Expr s
Expr 'RealSort -> Expr 'RealSort
Exp  (Expr 'RealSort -> Expr s) -> f (Expr 'RealSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x
    Sin Expr 'RealSort
x                -> Expr 'RealSort -> Expr s
Expr 'RealSort -> Expr 'RealSort
Sin  (Expr 'RealSort -> Expr s) -> f (Expr 'RealSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x
    Cos Expr 'RealSort
x                -> Expr 'RealSort -> Expr s
Expr 'RealSort -> Expr 'RealSort
Cos  (Expr 'RealSort -> Expr s) -> f (Expr 'RealSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x
    Tan Expr 'RealSort
x                -> Expr 'RealSort -> Expr s
Expr 'RealSort -> Expr 'RealSort
Tan  (Expr 'RealSort -> Expr s) -> f (Expr 'RealSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x
    Asin Expr 'RealSort
x               -> Expr 'RealSort -> Expr s
Expr 'RealSort -> Expr 'RealSort
Asin (Expr 'RealSort -> Expr s) -> f (Expr 'RealSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x
    Acos Expr 'RealSort
x               -> Expr 'RealSort -> Expr s
Expr 'RealSort -> Expr 'RealSort
Acos (Expr 'RealSort -> Expr s) -> f (Expr 'RealSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x
    Atan Expr 'RealSort
x               -> Expr 'RealSort -> Expr s
Expr 'RealSort -> Expr 'RealSort
Atan (Expr 'RealSort -> Expr s) -> f (Expr 'RealSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x
    ToReal Expr 'IntSort
x             -> Expr 'IntSort -> Expr s
Expr 'IntSort -> Expr 'RealSort
ToReal (Expr 'IntSort -> Expr s) -> f (Expr 'IntSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
x
    ToInt Expr 'RealSort
x              -> Expr 'RealSort -> Expr s
Expr 'RealSort -> Expr 'IntSort
ToInt  (Expr 'RealSort -> Expr s) -> f (Expr 'RealSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x
    IsInt Expr 'RealSort
x              -> Expr 'RealSort -> Expr s
Expr 'RealSort -> Expr 'BoolSort
IsInt  (Expr 'RealSort -> Expr s) -> f (Expr 'RealSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'RealSort
x
    Ite Expr 'BoolSort
p Expr s
t Expr s
n            -> Expr 'BoolSort -> Expr s -> Expr s -> Expr s
forall (t :: SMTSort). Expr 'BoolSort -> Expr t -> Expr t -> Expr t
Ite    (Expr 'BoolSort -> Expr s -> Expr s -> Expr s)
-> f (Expr 'BoolSort) -> f (Expr s -> Expr s -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'BoolSort
p f (Expr s -> Expr s -> Expr s)
-> f (Expr s) -> f (Expr s -> Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
t f (Expr s -> Expr s) -> f (Expr s) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr s
n
    BvNot Expr ('BvSort n)
x              -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n)
BvNot  (Expr ('BvSort n) -> Expr s) -> f (Expr ('BvSort n)) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x
    BvAnd Expr ('BvSort n)
x Expr ('BvSort n)
y            -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvAnd  (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvOr Expr ('BvSort n)
x Expr ('BvSort n)
y             -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvOr   (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvXor Expr ('BvSort n)
x Expr ('BvSort n)
y            -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvXor  (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvNand Expr ('BvSort n)
x Expr ('BvSort n)
y           -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvNand (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvNor Expr ('BvSort n)
x Expr ('BvSort n)
y            -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvNor  (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvNeg Expr ('BvSort n)
x              -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n)
BvNeg  (Expr ('BvSort n) -> Expr s) -> f (Expr ('BvSort n)) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x
    BvAdd Expr ('BvSort n)
x Expr ('BvSort n)
y            -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvAdd  (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvSub Expr ('BvSort n)
x Expr ('BvSort n)
y            -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvSub  (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvMul Expr ('BvSort n)
x Expr ('BvSort n)
y            -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvMul  (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvuDiv Expr ('BvSort n)
x Expr ('BvSort n)
y           -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuDiv (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvuRem Expr ('BvSort n)
x Expr ('BvSort n)
y           -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuRem (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvShL Expr ('BvSort n)
x Expr ('BvSort n)
y            -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvShL  (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvLShR Expr ('BvSort n)
x Expr ('BvSort n)
y           -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvLShR (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvConcat Expr ('BvSort n)
x Expr ('BvSort m)
y         -> Expr ('BvSort n) -> Expr ('BvSort m) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort m) -> Expr ('BvSort (n + m))
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Expr ('BvSort n) -> Expr ('BvSort m) -> Expr ('BvSort (n + m))
BvConcat (Expr ('BvSort n) -> Expr ('BvSort m) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort m) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort m) -> Expr s)
-> f (Expr ('BvSort m)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort m)
y
    BvRotL Proxy i
i Expr ('BvSort n)
x           -> Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat) (i :: Nat).
(KnownNat n, KnownNat i, KnownNat (Mod i n)) =>
Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
BvRotL Proxy i
i (Expr ('BvSort n) -> Expr s) -> f (Expr ('BvSort n)) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x
    BvRotR Proxy i
i Expr ('BvSort n)
x           -> Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat) (i :: Nat).
(KnownNat n, KnownNat i, KnownNat (Mod i n)) =>
Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
BvRotR Proxy i
i (Expr ('BvSort n) -> Expr s) -> f (Expr ('BvSort n)) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x
    BvuLT Expr ('BvSort n)
x Expr ('BvSort n)
y            -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
BvuLT    (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvuLTHE Expr ('BvSort n)
x Expr ('BvSort n)
y          -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
BvuLTHE  (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvuGTHE Expr ('BvSort n)
x Expr ('BvSort n)
y          -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
BvuGTHE  (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    BvuGT Expr ('BvSort n)
x Expr ('BvSort n)
y            -> Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
BvuGT    (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr ('BvSort n) -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
x f (Expr ('BvSort n) -> Expr s)
-> f (Expr ('BvSort n)) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr ('BvSort n)
y
    ArrSelect Expr ('ArraySort k s)
i Expr k
arr      -> Expr ('ArraySort k s) -> Expr k -> Expr s
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Expr ('ArraySort k v) -> Expr k -> Expr v
ArrSelect Expr ('ArraySort k s)
i   (Expr k -> Expr s) -> f (Expr k) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr k
arr
    ArrStore Expr ('ArraySort k v)
i Expr k
x Expr v
arr     -> Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
ArrStore Expr ('ArraySort k v)
i    (Expr k -> Expr v -> Expr s) -> f (Expr k) -> f (Expr v -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr k
x f (Expr v -> Expr s) -> f (Expr v) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr v
arr
    StrConcat Expr 'StringSort
x Expr 'StringSort
y        -> Expr 'StringSort -> Expr 'StringSort -> Expr s
Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
StrConcat     (Expr 'StringSort -> Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y
    StrLength Expr 'StringSort
x          -> Expr 'StringSort -> Expr s
Expr 'StringSort -> Expr 'IntSort
StrLength     (Expr 'StringSort -> Expr s) -> f (Expr 'StringSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x
    StrLT Expr 'StringSort
x Expr 'StringSort
y            -> Expr 'StringSort -> Expr 'StringSort -> Expr s
Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
StrLT         (Expr 'StringSort -> Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y
    StrLTHE Expr 'StringSort
x Expr 'StringSort
y          -> Expr 'StringSort -> Expr 'StringSort -> Expr s
Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
StrLTHE       (Expr 'StringSort -> Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y
    StrAt Expr 'StringSort
x Expr 'IntSort
i            -> Expr 'StringSort -> Expr 'IntSort -> Expr s
Expr 'StringSort -> Expr 'IntSort -> Expr 'StringSort
StrAt         (Expr 'StringSort -> Expr 'IntSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr 'IntSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'IntSort -> Expr s) -> f (Expr 'IntSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
i
    StrSubstring Expr 'StringSort
x Expr 'IntSort
i Expr 'IntSort
j   -> Expr 'StringSort -> Expr 'IntSort -> Expr 'IntSort -> Expr s
Expr 'StringSort
-> Expr 'IntSort -> Expr 'IntSort -> Expr 'StringSort
StrSubstring  (Expr 'StringSort -> Expr 'IntSort -> Expr 'IntSort -> Expr s)
-> f (Expr 'StringSort)
-> f (Expr 'IntSort -> Expr 'IntSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'IntSort -> Expr 'IntSort -> Expr s)
-> f (Expr 'IntSort) -> f (Expr 'IntSort -> Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
i f (Expr 'IntSort -> Expr s) -> f (Expr 'IntSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
j
    StrPrefixOf Expr 'StringSort
x Expr 'StringSort
y      -> Expr 'StringSort -> Expr 'StringSort -> Expr s
Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
StrPrefixOf   (Expr 'StringSort -> Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y
    StrSuffixOf Expr 'StringSort
x Expr 'StringSort
y      -> Expr 'StringSort -> Expr 'StringSort -> Expr s
Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
StrSuffixOf   (Expr 'StringSort -> Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y
    StrContains Expr 'StringSort
x Expr 'StringSort
y      -> Expr 'StringSort -> Expr 'StringSort -> Expr s
Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
StrContains   (Expr 'StringSort -> Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y
    StrIndexOf Expr 'StringSort
x Expr 'StringSort
y Expr 'IntSort
i     -> Expr 'StringSort -> Expr 'StringSort -> Expr 'IntSort -> Expr s
Expr 'StringSort
-> Expr 'StringSort -> Expr 'IntSort -> Expr 'IntSort
StrIndexOf    (Expr 'StringSort -> Expr 'StringSort -> Expr 'IntSort -> Expr s)
-> f (Expr 'StringSort)
-> f (Expr 'StringSort -> Expr 'IntSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr 'IntSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr 'IntSort -> Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y f (Expr 'IntSort -> Expr s) -> f (Expr 'IntSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'IntSort
i
    StrReplace Expr 'StringSort
x Expr 'StringSort
y Expr 'StringSort
y'    -> Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort -> Expr s
Expr 'StringSort
-> Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
StrReplace    (Expr 'StringSort
 -> Expr 'StringSort -> Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort)
-> f (Expr 'StringSort -> Expr 'StringSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y f (Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y'
    StrReplaceAll Expr 'StringSort
x Expr 'StringSort
y Expr 'StringSort
y' -> Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort -> Expr s
Expr 'StringSort
-> Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
StrReplaceAll (Expr 'StringSort
 -> Expr 'StringSort -> Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort)
-> f (Expr 'StringSort -> Expr 'StringSort -> Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
x f (Expr 'StringSort -> Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr 'StringSort -> Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y f (Expr 'StringSort -> Expr s)
-> f (Expr 'StringSort) -> f (Expr s)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f Expr 'StringSort
y'
    ForAll (Just SMTVar t1
qv) Expr t1 -> Expr 'BoolSort
qexpr -> Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
forall (t1 :: SMTSort).
KnownSMTSort t1 =>
Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
ForAll (SMTVar t1 -> Maybe (SMTVar t1)
forall a. a -> Maybe a
Just SMTVar t1
qv) ((Expr t1 -> Expr 'BoolSort) -> Expr s)
-> (Expr 'BoolSort -> Expr t1 -> Expr 'BoolSort)
-> Expr 'BoolSort
-> Expr s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'BoolSort -> Expr t1 -> Expr 'BoolSort
forall a b. a -> b -> a
const (Expr 'BoolSort -> Expr s) -> f (Expr 'BoolSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f (Expr t1 -> Expr 'BoolSort
qexpr (SMTVar t1 -> Expr t1
forall (t :: SMTSort). SMTVar t -> Expr t
Var SMTVar t1
qv))
    ForAll Maybe (SMTVar t1)
Nothing Expr t1 -> Expr 'BoolSort
qexpr   -> Expr 'BoolSort -> f (Expr 'BoolSort)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'BoolSort -> f (Expr 'BoolSort))
-> Expr 'BoolSort -> f (Expr 'BoolSort)
forall a b. (a -> b) -> a -> b
$ Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
forall (t1 :: SMTSort).
KnownSMTSort t1 =>
Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
ForAll Maybe (SMTVar t1)
forall a. Maybe a
Nothing Expr t1 -> Expr 'BoolSort
qexpr
    Exists (Just SMTVar t1
qv) Expr t1 -> Expr 'BoolSort
qexpr -> Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
forall (t1 :: SMTSort).
KnownSMTSort t1 =>
Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
Exists (SMTVar t1 -> Maybe (SMTVar t1)
forall a. a -> Maybe a
Just SMTVar t1
qv) ((Expr t1 -> Expr 'BoolSort) -> Expr s)
-> (Expr 'BoolSort -> Expr t1 -> Expr 'BoolSort)
-> Expr 'BoolSort
-> Expr s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'BoolSort -> Expr t1 -> Expr 'BoolSort
forall a b. a -> b -> a
const (Expr 'BoolSort -> Expr s) -> f (Expr 'BoolSort) -> f (Expr s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
forall (t :: SMTSort) (f :: * -> *).
(KnownSMTSort t, Applicative f) =>
(Expr t -> f (Expr t))
-> forall (s :: SMTSort). KnownSMTSort s => Expr s -> f (Expr s)
somePlate Expr t -> f (Expr t)
f (Expr t1 -> Expr 'BoolSort
qexpr (SMTVar t1 -> Expr t1
forall (t :: SMTSort). SMTVar t -> Expr t
Var SMTVar t1
qv))
    Exists Maybe (SMTVar t1)
Nothing Expr t1 -> Expr 'BoolSort
qexpr   -> Expr 'BoolSort -> f (Expr 'BoolSort)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'BoolSort -> f (Expr 'BoolSort))
-> Expr 'BoolSort -> f (Expr 'BoolSort)
forall a b. (a -> b) -> a -> b
$ Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
forall (t1 :: SMTSort).
KnownSMTSort t1 =>
Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
Exists Maybe (SMTVar t1)
forall a. Maybe a
Nothing Expr t1 -> Expr 'BoolSort
qexpr