{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Core.Data.Class.GenSym
(
FreshIndex (..),
FreshIdent (..),
name,
nameWithInfo,
MonadFresh (..),
FreshT,
Fresh,
runFreshT,
runFresh,
GenSym (..),
GenSymSimple (..),
genSym,
genSymSimple,
derivedNoSpecFresh,
derivedNoSpecSimpleFresh,
derivedSameShapeSimpleFresh,
chooseFresh,
chooseSimpleFresh,
chooseUnionFresh,
choose,
chooseSimple,
chooseUnion,
ListSpec (..),
SimpleListSpec (..),
EnumGenBound (..),
EnumGenUpperBound (..),
)
where
import Control.DeepSeq (NFData (rnf))
import Control.Monad.Except
( ExceptT (ExceptT),
MonadError (catchError, throwError),
)
import Control.Monad.Identity (Identity (runIdentity))
import Control.Monad.RWS.Class
( MonadRWS,
MonadReader (ask, local),
MonadState (get, put),
MonadWriter (listen, pass, writer),
asks,
gets,
)
import qualified Control.Monad.RWS.Lazy as RWSLazy
import qualified Control.Monad.RWS.Strict as RWSStrict
import Control.Monad.Reader (ReaderT (ReaderT))
import Control.Monad.Signatures (Catch)
import qualified Control.Monad.State.Lazy as StateLazy
import qualified Control.Monad.State.Strict as StateStrict
import Control.Monad.Trans.Class
( MonadTrans (lift),
)
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import Data.Bifunctor (Bifunctor (first))
import qualified Data.ByteString as B
import Data.Hashable (Hashable (hashWithSalt))
import Data.Int (Int16, Int32, Int64, Int8)
import Data.String (IsString (fromString))
import qualified Data.Text as T
import Data.Typeable
( Proxy (Proxy),
Typeable,
eqT,
typeRep,
type (:~:) (Refl),
)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeNats (KnownNat, Nat, type (<=))
import Generics.Deriving
( Generic (Rep, from, to),
K1 (K1),
M1 (M1),
U1 (U1),
type (:*:) ((:*:)),
type (:+:) (L1, R1),
)
import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM (UnionM)
import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)
import Grisette.Core.Data.Class.Mergeable
( Mergeable (rootStrategy),
Mergeable1 (liftRootStrategy),
Mergeable2 (liftRootStrategy2),
MergingStrategy (SimpleStrategy),
rootStrategy1,
wrapStrategy,
)
import Grisette.Core.Data.Class.SimpleMergeable
( SimpleMergeable (mrgIte),
SimpleMergeable1 (liftMrgIte),
UnionLike (mergeWithStrategy, mrgIfWithStrategy, single, unionIf),
merge,
mrgIf,
mrgSingle,
)
import Grisette.Core.Data.Class.Solvable
( Solvable (iinfosym, isym),
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
( LinkedRep,
SupportedPrim,
)
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
( SomeSymIntN (SomeSymIntN),
SomeSymWordN (SomeSymWordN),
SymBool,
SymIntN,
SymInteger,
SymWordN,
type (-~>),
type (=~>),
)
import Grisette.Utils.Parameterized
( KnownProof (KnownProof),
LeqProof (LeqProof),
unsafeKnownProof,
unsafeLeqProof,
)
import Language.Haskell.TH.Syntax (Lift (liftTyped))
newtype FreshIndex = FreshIndex Int
deriving (Int -> FreshIndex -> ShowS
[FreshIndex] -> ShowS
FreshIndex -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FreshIndex] -> ShowS
$cshowList :: [FreshIndex] -> ShowS
show :: FreshIndex -> String
$cshow :: FreshIndex -> String
showsPrec :: Int -> FreshIndex -> ShowS
$cshowsPrec :: Int -> FreshIndex -> ShowS
Show)
deriving (FreshIndex -> FreshIndex -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FreshIndex -> FreshIndex -> Bool
$c/= :: FreshIndex -> FreshIndex -> Bool
== :: FreshIndex -> FreshIndex -> Bool
$c== :: FreshIndex -> FreshIndex -> Bool
Eq, Eq FreshIndex
FreshIndex -> FreshIndex -> Bool
FreshIndex -> FreshIndex -> Ordering
FreshIndex -> FreshIndex -> FreshIndex
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FreshIndex -> FreshIndex -> FreshIndex
$cmin :: FreshIndex -> FreshIndex -> FreshIndex
max :: FreshIndex -> FreshIndex -> FreshIndex
$cmax :: FreshIndex -> FreshIndex -> FreshIndex
>= :: FreshIndex -> FreshIndex -> Bool
$c>= :: FreshIndex -> FreshIndex -> Bool
> :: FreshIndex -> FreshIndex -> Bool
$c> :: FreshIndex -> FreshIndex -> Bool
<= :: FreshIndex -> FreshIndex -> Bool
$c<= :: FreshIndex -> FreshIndex -> Bool
< :: FreshIndex -> FreshIndex -> Bool
$c< :: FreshIndex -> FreshIndex -> Bool
compare :: FreshIndex -> FreshIndex -> Ordering
$ccompare :: FreshIndex -> FreshIndex -> Ordering
Ord, Integer -> FreshIndex
FreshIndex -> FreshIndex
FreshIndex -> FreshIndex -> FreshIndex
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> FreshIndex
$cfromInteger :: Integer -> FreshIndex
signum :: FreshIndex -> FreshIndex
$csignum :: FreshIndex -> FreshIndex
abs :: FreshIndex -> FreshIndex
$cabs :: FreshIndex -> FreshIndex
negate :: FreshIndex -> FreshIndex
$cnegate :: FreshIndex -> FreshIndex
* :: FreshIndex -> FreshIndex -> FreshIndex
$c* :: FreshIndex -> FreshIndex -> FreshIndex
- :: FreshIndex -> FreshIndex -> FreshIndex
$c- :: FreshIndex -> FreshIndex -> FreshIndex
+ :: FreshIndex -> FreshIndex -> FreshIndex
$c+ :: FreshIndex -> FreshIndex -> FreshIndex
Num) via Int
instance Mergeable FreshIndex where
rootStrategy :: MergingStrategy FreshIndex
rootStrategy = forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy forall a b. (a -> b) -> a -> b
$ \SymBool
_ FreshIndex
t FreshIndex
f -> forall a. Ord a => a -> a -> a
max FreshIndex
t FreshIndex
f
instance SimpleMergeable FreshIndex where
mrgIte :: SymBool -> FreshIndex -> FreshIndex -> FreshIndex
mrgIte SymBool
_ = forall a. Ord a => a -> a -> a
max
data FreshIdent where
FreshIdent :: String -> FreshIdent
FreshIdentWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent
instance Show FreshIdent where
show :: FreshIdent -> String
show (FreshIdent String
i) = String
i
show (FreshIdentWithInfo String
s a
i) = String
s forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
i
instance IsString FreshIdent where
fromString :: String -> FreshIdent
fromString = String -> FreshIdent
name
instance Eq FreshIdent where
FreshIdent String
l == :: FreshIdent -> FreshIdent -> Bool
== FreshIdent String
r = String
l forall a. Eq a => a -> a -> Bool
== String
r
FreshIdentWithInfo String
l (a
linfo :: linfo) == FreshIdentWithInfo String
r (a
rinfo :: rinfo) = case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @linfo @rinfo of
Just a :~: a
Refl -> String
l forall a. Eq a => a -> a -> Bool
== String
r Bool -> Bool -> Bool
&& a
linfo forall a. Eq a => a -> a -> Bool
== a
rinfo
Maybe (a :~: a)
_ -> Bool
False
FreshIdent
_ == FreshIdent
_ = Bool
False
instance Ord FreshIdent where
FreshIdent String
l <= :: FreshIdent -> FreshIdent -> Bool
<= FreshIdent String
r = String
l forall a. Ord a => a -> a -> Bool
<= String
r
FreshIdent String
_ <= FreshIdent
_ = Bool
True
FreshIdent
_ <= FreshIdent String
_ = Bool
False
FreshIdentWithInfo String
l (a
linfo :: linfo) <= FreshIdentWithInfo String
r (a
rinfo :: rinfo) =
String
l forall a. Ord a => a -> a -> Bool
< String
r
Bool -> Bool -> Bool
|| ( String
l forall a. Eq a => a -> a -> Bool
== String
r
Bool -> Bool -> Bool
&& ( case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @linfo @rinfo of
Just a :~: a
Refl -> a
linfo forall a. Ord a => a -> a -> Bool
<= a
rinfo
Maybe (a :~: a)
_ -> forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @linfo) forall a. Ord a => a -> a -> Bool
<= forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @rinfo)
)
)
instance Hashable FreshIdent where
hashWithSalt :: Int -> FreshIdent -> Int
hashWithSalt Int
s (FreshIdent String
n) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` String
n
hashWithSalt Int
s (FreshIdentWithInfo String
n a
i) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` String
n forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
i
instance Lift FreshIdent where
liftTyped :: forall (m :: * -> *). Quote m => FreshIdent -> Code m FreshIdent
liftTyped (FreshIdent String
n) = [||FreshIdent n||]
liftTyped (FreshIdentWithInfo String
n a
i) = [||FreshIdentWithInfo n i||]
instance NFData FreshIdent where
rnf :: FreshIdent -> ()
rnf (FreshIdent String
n) = forall a. NFData a => a -> ()
rnf String
n
rnf (FreshIdentWithInfo String
n a
i) = forall a. NFData a => a -> ()
rnf String
n seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf a
i
name :: String -> FreshIdent
name :: String -> FreshIdent
name = String -> FreshIdent
FreshIdent
nameWithInfo :: forall a. (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent
nameWithInfo :: forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
String -> a -> FreshIdent
nameWithInfo = forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
String -> a -> FreshIdent
FreshIdentWithInfo
class (Monad m) => MonadFresh m where
nextFreshIndex :: m FreshIndex
getFreshIdent :: m FreshIdent
newtype FreshT m a = FreshT {forall (m :: * -> *) a.
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
runFreshT' :: FreshIdent -> FreshIndex -> m (a, FreshIndex)}
instance
(Mergeable a, Mergeable1 m) =>
Mergeable (FreshT m a)
where
rootStrategy :: MergingStrategy (FreshT m a)
rootStrategy =
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy forall a (u :: * -> *).
(Mergeable a, Mergeable1 u) =>
MergingStrategy (u a)
rootStrategy1)) forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall (m :: * -> *) a.
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
runFreshT'
instance (Mergeable1 m) => Mergeable1 (FreshT m) where
liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (FreshT m a)
liftRootStrategy MergingStrategy a
m =
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy
(forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (forall (u :: * -> * -> *) a b.
Mergeable2 u =>
MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
liftRootStrategy2 MergingStrategy a
m forall a. Mergeable a => MergingStrategy a
rootStrategy))))
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT
forall (m :: * -> *) a.
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
runFreshT'
instance
(UnionLike m, Mergeable a) =>
SimpleMergeable (FreshT m a)
where
mrgIte :: SymBool -> FreshT m a -> FreshT m a -> FreshT m a
mrgIte = forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
instance
(UnionLike m) =>
SimpleMergeable1 (FreshT m)
where
liftMrgIte :: forall a.
(SymBool -> a -> a -> a)
-> SymBool -> FreshT m a -> FreshT m a -> FreshT m a
liftMrgIte SymBool -> a -> a -> a
m = forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy (forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> a -> a -> a
m)
instance
(UnionLike m) =>
UnionLike (FreshT m)
where
mergeWithStrategy :: forall a. MergingStrategy a -> FreshT m a -> FreshT m a
mergeWithStrategy MergingStrategy a
s (FreshT FreshIdent -> FreshIndex -> m (a, FreshIndex)
f) =
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy (forall (u :: * -> * -> *) a b.
Mergeable2 u =>
MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
liftRootStrategy2 MergingStrategy a
s forall a. Mergeable a => MergingStrategy a
rootStrategy) forall a b. (a -> b) -> a -> b
$ FreshIdent -> FreshIndex -> m (a, FreshIndex)
f FreshIdent
ident FreshIndex
index
mrgIfWithStrategy :: forall a.
MergingStrategy a
-> SymBool -> FreshT m a -> FreshT m a -> FreshT m a
mrgIfWithStrategy MergingStrategy a
s SymBool
cond (FreshT FreshIdent -> FreshIndex -> m (a, FreshIndex)
t) (FreshT FreshIdent -> FreshIndex -> m (a, FreshIndex)
f) =
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy (forall (u :: * -> * -> *) a b.
Mergeable2 u =>
MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
liftRootStrategy2 MergingStrategy a
s forall a. Mergeable a => MergingStrategy a
rootStrategy) SymBool
cond (FreshIdent -> FreshIndex -> m (a, FreshIndex)
t FreshIdent
ident FreshIndex
index) (FreshIdent -> FreshIndex -> m (a, FreshIndex)
f FreshIdent
ident FreshIndex
index)
single :: forall a. a -> FreshT m a
single a
x = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
i -> forall (u :: * -> *) a. UnionLike u => a -> u a
single (a
x, FreshIndex
i)
unionIf :: forall a. SymBool -> FreshT m a -> FreshT m a -> FreshT m a
unionIf SymBool
cond (FreshT FreshIdent -> FreshIndex -> m (a, FreshIndex)
t) (FreshT FreshIdent -> FreshIndex -> m (a, FreshIndex)
f) =
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond (FreshIdent -> FreshIndex -> m (a, FreshIndex)
t FreshIdent
ident FreshIndex
index) (FreshIdent -> FreshIndex -> m (a, FreshIndex)
f FreshIdent
ident FreshIndex
index)
runFreshT :: (Monad m) => FreshT m a -> FreshIdent -> m a
runFreshT :: forall (m :: * -> *) a. Monad m => FreshT m a -> FreshIdent -> m a
runFreshT FreshT m a
m FreshIdent
ident = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
runFreshT' FreshT m a
m FreshIdent
ident (Int -> FreshIndex
FreshIndex Int
0)
instance (Functor f) => Functor (FreshT f) where
fmap :: forall a b. (a -> b) -> FreshT f a -> FreshT f b
fmap a -> b
f (FreshT FreshIdent -> FreshIndex -> f (a, FreshIndex)
s) = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
idx -> forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreshIdent -> FreshIndex -> f (a, FreshIndex)
s FreshIdent
ident FreshIndex
idx
instance (Applicative m, Monad m) => Applicative (FreshT m) where
pure :: forall a. a -> FreshT m a
pure a
a = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
idx -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, FreshIndex
idx)
FreshT FreshIdent -> FreshIndex -> m (a -> b, FreshIndex)
fs <*> :: forall a b. FreshT m (a -> b) -> FreshT m a -> FreshT m b
<*> FreshT FreshIdent -> FreshIndex -> m (a, FreshIndex)
as = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
idx -> do
(a -> b
f, FreshIndex
idx') <- FreshIdent -> FreshIndex -> m (a -> b, FreshIndex)
fs FreshIdent
ident FreshIndex
idx
(a
a, FreshIndex
idx'') <- FreshIdent -> FreshIndex -> m (a, FreshIndex)
as FreshIdent
ident FreshIndex
idx'
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> b
f a
a, FreshIndex
idx'')
instance (Monad m) => Monad (FreshT m) where
(FreshT FreshIdent -> FreshIndex -> m (a, FreshIndex)
s) >>= :: forall a b. FreshT m a -> (a -> FreshT m b) -> FreshT m b
>>= a -> FreshT m b
f = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
idx -> do
(a
a, FreshIndex
idx') <- FreshIdent -> FreshIndex -> m (a, FreshIndex)
s FreshIdent
ident FreshIndex
idx
forall (m :: * -> *) a.
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
runFreshT' (a -> FreshT m b
f a
a) FreshIdent
ident FreshIndex
idx'
instance MonadTrans FreshT where
lift :: forall (m :: * -> *) a. Monad m => m a -> FreshT m a
lift m a
x = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
index -> (,FreshIndex
index) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
x
liftFreshTCache :: (Functor m) => Catch e m (a, FreshIndex) -> Catch e (FreshT m) a
liftFreshTCache :: forall (m :: * -> *) e a.
Functor m =>
Catch e m (a, FreshIndex) -> Catch e (FreshT m) a
liftFreshTCache Catch e m (a, FreshIndex)
catchE (FreshT FreshIdent -> FreshIndex -> m (a, FreshIndex)
m) e -> FreshT m a
h =
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
m FreshIdent
ident FreshIndex
index Catch e m (a, FreshIndex)
`catchE` \e
e -> forall (m :: * -> *) a.
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
runFreshT' (e -> FreshT m a
h e
e) FreshIdent
ident FreshIndex
index
instance (MonadError e m) => MonadError e (FreshT m) where
throwError :: forall a. e -> FreshT m a
throwError = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
catchError :: forall a. FreshT m a -> (e -> FreshT m a) -> FreshT m a
catchError = forall (m :: * -> *) e a.
Functor m =>
Catch e m (a, FreshIndex) -> Catch e (FreshT m) a
liftFreshTCache forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError
instance (MonadWriter w m) => MonadWriter w (FreshT m) where
writer :: forall a. (a, w) -> FreshT m a
writer (a, w)
p = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
index -> (,FreshIndex
index) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall w (m :: * -> *) a. MonadWriter w m => (a, w) -> m a
writer (a, w)
p
listen :: forall a. FreshT m a -> FreshT m (a, w)
listen (FreshT FreshIdent -> FreshIndex -> m (a, FreshIndex)
r) = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> (\((a
a, FreshIndex
b), w
c) -> ((a
a, w
c), FreshIndex
b)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen (FreshIdent -> FreshIndex -> m (a, FreshIndex)
r FreshIdent
ident FreshIndex
index)
pass :: forall a. FreshT m (a, w -> w) -> FreshT m a
pass (FreshT FreshIdent -> FreshIndex -> m ((a, w -> w), FreshIndex)
r) = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> forall w (m :: * -> *) a. MonadWriter w m => m (a, w -> w) -> m a
pass forall a b. (a -> b) -> a -> b
$ (\((a
a, w -> w
b), FreshIndex
c) -> ((a
a, FreshIndex
c), w -> w
b)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreshIdent -> FreshIndex -> m ((a, w -> w), FreshIndex)
r FreshIdent
ident FreshIndex
index
instance (MonadState s m) => MonadState s (FreshT m) where
get :: FreshT m s
get = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
index -> forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (,FreshIndex
index)
put :: s -> FreshT m ()
put s
s = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
index -> (,FreshIndex
index) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => s -> m ()
put s
s
instance (MonadReader r m) => MonadReader r (FreshT m) where
local :: forall a. (r -> r) -> FreshT m a -> FreshT m a
local r -> r
t (FreshT FreshIdent -> FreshIndex -> m (a, FreshIndex)
r) = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local r -> r
t (FreshIdent -> FreshIndex -> m (a, FreshIndex)
r FreshIdent
ident FreshIndex
index)
ask :: FreshT m r
ask = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
index -> forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (,FreshIndex
index)
instance (MonadRWS r w s m) => MonadRWS r w s (FreshT m)
instance (MonadFresh m) => MonadFresh (ExceptT e m) where
nextFreshIndex :: ExceptT e m FreshIndex
nextFreshIndex = forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
getFreshIdent :: ExceptT e m FreshIdent
getFreshIdent = forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m, Monoid w) => MonadFresh (WriterLazy.WriterT w m) where
nextFreshIndex :: WriterT w m FreshIndex
nextFreshIndex = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT forall a b. (a -> b) -> a -> b
$ (,forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
getFreshIdent :: WriterT w m FreshIdent
getFreshIdent = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT forall a b. (a -> b) -> a -> b
$ (,forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m, Monoid w) => MonadFresh (WriterStrict.WriterT w m) where
nextFreshIndex :: WriterT w m FreshIndex
nextFreshIndex = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT forall a b. (a -> b) -> a -> b
$ (,forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
getFreshIdent :: WriterT w m FreshIdent
getFreshIdent = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT forall a b. (a -> b) -> a -> b
$ (,forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m) => MonadFresh (StateLazy.StateT s m) where
nextFreshIndex :: StateT s m FreshIndex
nextFreshIndex = forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateLazy.StateT forall a b. (a -> b) -> a -> b
$ \s
s -> (,s
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
getFreshIdent :: StateT s m FreshIdent
getFreshIdent = forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateLazy.StateT forall a b. (a -> b) -> a -> b
$ \s
s -> (,s
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m) => MonadFresh (StateStrict.StateT s m) where
nextFreshIndex :: StateT s m FreshIndex
nextFreshIndex = forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateStrict.StateT forall a b. (a -> b) -> a -> b
$ \s
s -> (,s
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
getFreshIdent :: StateT s m FreshIdent
getFreshIdent = forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateStrict.StateT forall a b. (a -> b) -> a -> b
$ \s
s -> (,s
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m) => MonadFresh (ReaderT r m) where
nextFreshIndex :: ReaderT r m FreshIndex
nextFreshIndex = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
getFreshIdent :: ReaderT r m FreshIdent
getFreshIdent = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m, Monoid w) => MonadFresh (RWSLazy.RWST r w s m) where
nextFreshIndex :: RWST r w s m FreshIndex
nextFreshIndex = forall r w s (m :: * -> *) a.
(r -> s -> m (a, s, w)) -> RWST r w s m a
RWSLazy.RWST forall a b. (a -> b) -> a -> b
$ \r
_ s
s -> (,s
s,forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
getFreshIdent :: RWST r w s m FreshIdent
getFreshIdent = forall r w s (m :: * -> *) a.
(r -> s -> m (a, s, w)) -> RWST r w s m a
RWSLazy.RWST forall a b. (a -> b) -> a -> b
$ \r
_ s
s -> (,s
s,forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m, Monoid w) => MonadFresh (RWSStrict.RWST r w s m) where
nextFreshIndex :: RWST r w s m FreshIndex
nextFreshIndex = forall r w s (m :: * -> *) a.
(r -> s -> m (a, s, w)) -> RWST r w s m a
RWSStrict.RWST forall a b. (a -> b) -> a -> b
$ \r
_ s
s -> (,s
s,forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
getFreshIdent :: RWST r w s m FreshIdent
getFreshIdent = forall r w s (m :: * -> *) a.
(r -> s -> m (a, s, w)) -> RWST r w s m a
RWSStrict.RWST forall a b. (a -> b) -> a -> b
$ \r
_ s
s -> (,s
s,forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
type Fresh = FreshT Identity
runFresh :: Fresh a -> FreshIdent -> a
runFresh :: forall a. Fresh a -> FreshIdent -> a
runFresh Fresh a
m FreshIdent
ident = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => FreshT m a -> FreshIdent -> m a
runFreshT Fresh a
m FreshIdent
ident
instance (Monad m) => MonadFresh (FreshT m) where
nextFreshIndex :: FreshT m FreshIndex
nextFreshIndex = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
idx -> forall (m :: * -> *) a. Monad m => a -> m a
return (FreshIndex
idx, FreshIndex
idx forall a. Num a => a -> a -> a
+ FreshIndex
1)
getFreshIdent :: FreshT m FreshIdent
getFreshIdent = forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT forall a b. (a -> b) -> a -> b
$ forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall (m :: * -> *) a. Monad m => a -> m a
return
class (Mergeable a) => GenSym spec a where
fresh ::
(MonadFresh m) =>
spec ->
m (UnionM a)
default fresh ::
(GenSymSimple spec a) =>
( MonadFresh m
) =>
spec ->
m (UnionM a)
fresh spec
spec = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh spec
spec
genSym :: (GenSym spec a) => spec -> FreshIdent -> UnionM a
genSym :: forall spec a. GenSym spec a => spec -> FreshIdent -> UnionM a
genSym = forall a. Fresh a -> FreshIdent -> a
runFresh forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh
class GenSymSimple spec a where
simpleFresh ::
( MonadFresh m
) =>
spec ->
m a
genSymSimple :: forall spec a. (GenSymSimple spec a) => spec -> FreshIdent -> a
genSymSimple :: forall spec a. GenSymSimple spec a => spec -> FreshIdent -> a
genSymSimple = forall a. Fresh a -> FreshIdent -> a
runFresh forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh
class GenSymNoSpec a where
freshNoSpec ::
( MonadFresh m
) =>
m (UnionM (a c))
instance GenSymNoSpec U1 where
freshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (UnionM (U1 c))
freshNoSpec = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall k (p :: k). U1 p
U1
instance (GenSym () c) => GenSymNoSpec (K1 i c) where
freshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (UnionM (K1 i c c))
freshNoSpec = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i c (p :: k). c -> K1 i c p
K1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh ()
instance (GenSymNoSpec a) => GenSymNoSpec (M1 i c a) where
freshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (UnionM (M1 i c a c))
freshNoSpec = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
freshNoSpec
instance
( GenSymNoSpec a,
GenSymNoSpec b,
forall x. Mergeable (a x),
forall x. Mergeable (b x)
) =>
GenSymNoSpec (a :+: b)
where
freshNoSpec ::
forall m c.
( MonadFresh m
) =>
m (UnionM ((a :+: b) c))
freshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (UnionM ((:+:) a b c))
freshNoSpec = do
SymBool
cond :: bool <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh ()
UnionM (a c)
l :: UnionM (a c) <- forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
freshNoSpec
UnionM (b c)
r :: UnionM (b c) <- forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
freshNoSpec
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 UnionM (a c)
l) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 UnionM (b c)
r)
instance
(GenSymNoSpec a, GenSymNoSpec b) =>
GenSymNoSpec (a :*: b)
where
freshNoSpec ::
forall m c.
( MonadFresh m
) =>
m (UnionM ((a :*: b) c))
freshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (UnionM ((:*:) a b c))
freshNoSpec = do
UnionM (a c)
l :: UnionM (a c) <- forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
freshNoSpec
UnionM (b c)
r :: UnionM (b c) <- forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
freshNoSpec
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
a c
l1 <- UnionM (a c)
l
b c
r1 <- UnionM (b c)
r
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a c
l1 forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b c
r1
derivedNoSpecFresh ::
forall a m.
( Generic a,
GenSymNoSpec (Rep a),
Mergeable a,
MonadFresh m
) =>
() ->
m (UnionM a)
derivedNoSpecFresh :: forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh ()
_ = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a x. Generic a => Rep a x -> a
to forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
freshNoSpec
class GenSymSimpleNoSpec a where
simpleFreshNoSpec :: (MonadFresh m) => m (a c)
instance GenSymSimpleNoSpec U1 where
simpleFreshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (U1 c)
simpleFreshNoSpec = forall (m :: * -> *) a. Monad m => a -> m a
return forall k (p :: k). U1 p
U1
instance (GenSymSimple () c) => GenSymSimpleNoSpec (K1 i c) where
simpleFreshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (K1 i c c)
simpleFreshNoSpec = forall k i c (p :: k). c -> K1 i c p
K1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh ()
instance (GenSymSimpleNoSpec a) => GenSymSimpleNoSpec (M1 i c a) where
simpleFreshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (M1 i c a c)
simpleFreshNoSpec = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) c.
(GenSymSimpleNoSpec a, MonadFresh m) =>
m (a c)
simpleFreshNoSpec
instance
(GenSymSimpleNoSpec a, GenSymSimpleNoSpec b) =>
GenSymSimpleNoSpec (a :*: b)
where
simpleFreshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m ((:*:) a b c)
simpleFreshNoSpec = do
a c
l :: a c <- forall (a :: * -> *) (m :: * -> *) c.
(GenSymSimpleNoSpec a, MonadFresh m) =>
m (a c)
simpleFreshNoSpec
b c
r :: b c <- forall (a :: * -> *) (m :: * -> *) c.
(GenSymSimpleNoSpec a, MonadFresh m) =>
m (a c)
simpleFreshNoSpec
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a c
l forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b c
r
derivedNoSpecSimpleFresh ::
forall a m.
( Generic a,
GenSymSimpleNoSpec (Rep a),
MonadFresh m
) =>
() ->
m a
derivedNoSpecSimpleFresh :: forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh ()
_ = forall a x. Generic a => Rep a x -> a
to forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) c.
(GenSymSimpleNoSpec a, MonadFresh m) =>
m (a c)
simpleFreshNoSpec
class GenSymSameShape a where
genSymSameShapeFresh ::
( MonadFresh m
) =>
a c ->
m (a c)
instance GenSymSameShape U1 where
genSymSameShapeFresh :: forall (m :: * -> *) c. MonadFresh m => U1 c -> m (U1 c)
genSymSameShapeFresh U1 c
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall k (p :: k). U1 p
U1
instance (GenSymSimple c c) => GenSymSameShape (K1 i c) where
genSymSameShapeFresh :: forall (m :: * -> *) c. MonadFresh m => K1 i c c -> m (K1 i c c)
genSymSameShapeFresh (K1 c
c) = forall k i c (p :: k). c -> K1 i c p
K1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh c
c
instance (GenSymSameShape a) => GenSymSameShape (M1 i c a) where
genSymSameShapeFresh :: forall (m :: * -> *) c.
MonadFresh m =>
M1 i c a c -> m (M1 i c a c)
genSymSameShapeFresh (M1 a c
a) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
genSymSameShapeFresh a c
a
instance
(GenSymSameShape a, GenSymSameShape b) =>
GenSymSameShape (a :+: b)
where
genSymSameShapeFresh :: forall (m :: * -> *) c.
MonadFresh m =>
(:+:) a b c -> m ((:+:) a b c)
genSymSameShapeFresh (L1 a c
a) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
genSymSameShapeFresh a c
a
genSymSameShapeFresh (R1 b c
a) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
genSymSameShapeFresh b c
a
instance
(GenSymSameShape a, GenSymSameShape b) =>
GenSymSameShape (a :*: b)
where
genSymSameShapeFresh :: forall (m :: * -> *) c.
MonadFresh m =>
(:*:) a b c -> m ((:*:) a b c)
genSymSameShapeFresh (a c
a :*: b c
b) = do
a c
l :: a c <- forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
genSymSameShapeFresh a c
a
b c
r :: b c <- forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
genSymSameShapeFresh b c
b
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a c
l forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b c
r
derivedSameShapeSimpleFresh ::
forall a m.
( Generic a,
GenSymSameShape (Rep a),
MonadFresh m
) =>
a ->
m a
derivedSameShapeSimpleFresh :: forall a (m :: * -> *).
(Generic a, GenSymSameShape (Rep a), MonadFresh m) =>
a -> m a
derivedSameShapeSimpleFresh a
a = forall a x. Generic a => Rep a x -> a
to forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
genSymSameShapeFresh (forall a x. Generic a => a -> Rep a x
from a
a)
chooseFresh ::
forall a m.
( Mergeable a,
MonadFresh m
) =>
[a] ->
m (UnionM a)
chooseFresh :: forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh [a
x] = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
x
chooseFresh (a
r : [a]
rs) = do
SymBool
b <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh ()
UnionM a
res <- forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh [a]
rs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
b (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
r) UnionM a
res
chooseFresh [] = forall a. HasCallStack => String -> a
error String
"chooseFresh expects at least one value"
choose ::
forall a.
( Mergeable a
) =>
[a] ->
FreshIdent ->
UnionM a
choose :: forall a. Mergeable a => [a] -> FreshIdent -> UnionM a
choose = forall a. Fresh a -> FreshIdent -> a
runFresh forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh
chooseSimpleFresh ::
forall a m.
( SimpleMergeable a,
MonadFresh m
) =>
[a] ->
m a
chooseSimpleFresh :: forall a (m :: * -> *).
(SimpleMergeable a, MonadFresh m) =>
[a] -> m a
chooseSimpleFresh [a
x] = forall (m :: * -> *) a. Monad m => a -> m a
return a
x
chooseSimpleFresh (a
r : [a]
rs) = do
SymBool
b :: bool <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh ()
a
res <- forall a (m :: * -> *).
(SimpleMergeable a, MonadFresh m) =>
[a] -> m a
chooseSimpleFresh [a]
rs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. SimpleMergeable a => SymBool -> a -> a -> a
mrgIte SymBool
b a
r a
res
chooseSimpleFresh [] = forall a. HasCallStack => String -> a
error String
"chooseSimpleFresh expects at least one value"
chooseSimple ::
forall a.
( SimpleMergeable a
) =>
[a] ->
FreshIdent ->
a
chooseSimple :: forall a. SimpleMergeable a => [a] -> FreshIdent -> a
chooseSimple = forall a. Fresh a -> FreshIdent -> a
runFresh forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *).
(SimpleMergeable a, MonadFresh m) =>
[a] -> m a
chooseSimpleFresh
chooseUnionFresh ::
forall a m.
( Mergeable a,
MonadFresh m
) =>
[UnionM a] ->
m (UnionM a)
chooseUnionFresh :: forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh [UnionM a
x] = forall (m :: * -> *) a. Monad m => a -> m a
return UnionM a
x
chooseUnionFresh (UnionM a
r : [UnionM a]
rs) = do
SymBool
b <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh ()
UnionM a
res <- forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh [UnionM a]
rs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
b UnionM a
r UnionM a
res
chooseUnionFresh [] = forall a. HasCallStack => String -> a
error String
"chooseUnionFresh expects at least one value"
chooseUnion ::
forall a.
( Mergeable a
) =>
[UnionM a] ->
FreshIdent ->
UnionM a
chooseUnion :: forall a. Mergeable a => [UnionM a] -> FreshIdent -> UnionM a
chooseUnion = forall a. Fresh a -> FreshIdent -> a
runFresh forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh
#define CONCRETE_GENSYM_SAME_SHAPE(type) \
instance GenSym type type where fresh = return . mrgSingle
#define CONCRETE_GENSYMSIMPLE_SAME_SHAPE(type) \
instance GenSymSimple type type where simpleFresh = return
#define CONCRETE_GENSYM_SAME_SHAPE_BV(type) \
instance (KnownNat n, 1 <= n) => GenSym (type n) (type n) where fresh = return . mrgSingle
#define CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(type) \
instance (KnownNat n, 1 <= n) => GenSymSimple (type n) (type n) where simpleFresh = return
#if 1
CONCRETE_GENSYM_SAME_SHAPE(Bool)
CONCRETE_GENSYM_SAME_SHAPE(Integer)
CONCRETE_GENSYM_SAME_SHAPE(Char)
CONCRETE_GENSYM_SAME_SHAPE(Int)
CONCRETE_GENSYM_SAME_SHAPE(Int8)
CONCRETE_GENSYM_SAME_SHAPE(Int16)
CONCRETE_GENSYM_SAME_SHAPE(Int32)
CONCRETE_GENSYM_SAME_SHAPE(Int64)
CONCRETE_GENSYM_SAME_SHAPE(Word)
CONCRETE_GENSYM_SAME_SHAPE(Word8)
CONCRETE_GENSYM_SAME_SHAPE(Word16)
CONCRETE_GENSYM_SAME_SHAPE(Word32)
CONCRETE_GENSYM_SAME_SHAPE(Word64)
CONCRETE_GENSYM_SAME_SHAPE(SomeWordN)
CONCRETE_GENSYM_SAME_SHAPE(SomeIntN)
CONCRETE_GENSYM_SAME_SHAPE(B.ByteString)
CONCRETE_GENSYM_SAME_SHAPE(T.Text)
CONCRETE_GENSYM_SAME_SHAPE_BV(WordN)
CONCRETE_GENSYM_SAME_SHAPE_BV(IntN)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Bool)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Integer)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Char)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Int)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Int8)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Int16)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Int32)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Int64)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word8)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word16)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word32)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word64)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(SomeWordN)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(SomeIntN)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(B.ByteString)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(T.Text)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(WordN)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(IntN)
#endif
instance GenSym () Bool where
fresh :: forall (m :: * -> *). MonadFresh m => () -> m (UnionM Bool)
fresh = forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh
newtype EnumGenUpperBound a = EnumGenUpperBound a
instance (Enum v, Mergeable v) => GenSym (EnumGenUpperBound v) v where
fresh :: forall (m :: * -> *).
MonadFresh m =>
EnumGenUpperBound v -> m (UnionM v)
fresh (EnumGenUpperBound v
u) = forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh (forall a. Enum a => Int -> a
toEnum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0 .. forall a. Enum a => a -> Int
fromEnum v
u forall a. Num a => a -> a -> a
- Int
1])
data EnumGenBound a = EnumGenBound a a
instance (Enum v, Mergeable v) => GenSym (EnumGenBound v) v where
fresh :: forall (m :: * -> *).
MonadFresh m =>
EnumGenBound v -> m (UnionM v)
fresh (EnumGenBound v
l v
u) = forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh (forall a. Enum a => Int -> a
toEnum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [forall a. Enum a => a -> Int
fromEnum v
l .. forall a. Enum a => a -> Int
fromEnum v
u forall a. Num a => a -> a -> a
- Int
1])
instance
( GenSym aspec a,
Mergeable a,
GenSym bspec b,
Mergeable b
) =>
GenSym (Either aspec bspec) (Either a b)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
Either aspec bspec -> m (UnionM (Either a b))
fresh (Left aspec
aspec) = (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh aspec
aspec
fresh (Right bspec
bspec) = (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh bspec
bspec
instance
( GenSymSimple aspec a,
GenSymSimple bspec b
) =>
GenSymSimple (Either aspec bspec) (Either a b)
where
simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
Either aspec bspec -> m (Either a b)
simpleFresh (Left aspec
a) = forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh aspec
a
simpleFresh (Right bspec
b) = forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh bspec
b
instance
(GenSym () a, Mergeable a, GenSym () b, Mergeable b) =>
GenSym () (Either a b)
where
fresh :: forall (m :: * -> *). MonadFresh m => () -> m (UnionM (Either a b))
fresh = forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh
instance
( GenSym aspec a,
Mergeable a,
GenSym bspec b,
Mergeable b
) =>
GenSym (aspec, bspec) (Either a b)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec) -> m (UnionM (Either a b))
fresh (aspec
aspec, bspec
bspec) = do
UnionM a
l :: UnionM a <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh aspec
aspec
UnionM b
r :: UnionM b <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh bspec
bspec
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh [forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnionM a
l, forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnionM b
r]
instance
(GenSym aspec a, Mergeable a) =>
GenSym (Maybe aspec) (Maybe a)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
Maybe aspec -> m (UnionM (Maybe a))
fresh Maybe aspec
Nothing = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a. Maybe a
Nothing
fresh (Just aspec
aspec) = (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh aspec
aspec
instance
(GenSymSimple aspec a) =>
GenSymSimple (Maybe aspec) (Maybe a)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => Maybe aspec -> m (Maybe a)
simpleFresh Maybe aspec
Nothing = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
simpleFresh (Just aspec
aspec) = forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh aspec
aspec
instance (GenSym aspec a, Mergeable a) => GenSym aspec (Maybe a) where
fresh :: forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM (Maybe a))
fresh aspec
aspec = do
UnionM a
a :: UnionM a <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh aspec
aspec
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh [forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing, forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnionM a
a]
instance
(GenSym () a, Mergeable a) =>
GenSym Integer [a]
where
fresh :: forall (m :: * -> *). MonadFresh m => Integer -> m (UnionM [a])
fresh Integer
v = do
[UnionM a]
l <- forall (m :: * -> *). MonadFresh m => Integer -> m [UnionM a]
gl Integer
v
let xs :: [[UnionM a]]
xs = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr (:) [] [UnionM a]
l
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[UnionM a]]
xs
where
gl :: (MonadFresh m) => Integer -> m [UnionM a]
gl :: forall (m :: * -> *). MonadFresh m => Integer -> m [UnionM a]
gl Integer
v1
| Integer
v1 forall a. Ord a => a -> a -> Bool
<= Integer
0 = forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do
UnionM a
l <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh ()
[UnionM a]
r <- forall (m :: * -> *). MonadFresh m => Integer -> m [UnionM a]
gl (Integer
v1 forall a. Num a => a -> a -> a
- Integer
1)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UnionM a
l forall a. a -> [a] -> [a]
: [UnionM a]
r
data ListSpec spec = ListSpec
{
forall spec. ListSpec spec -> Int
genListMinLength :: Int,
forall spec. ListSpec spec -> Int
genListMaxLength :: Int,
forall spec. ListSpec spec -> spec
genListSubSpec :: spec
}
deriving (Int -> ListSpec spec -> ShowS
forall spec. Show spec => Int -> ListSpec spec -> ShowS
forall spec. Show spec => [ListSpec spec] -> ShowS
forall spec. Show spec => ListSpec spec -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ListSpec spec] -> ShowS
$cshowList :: forall spec. Show spec => [ListSpec spec] -> ShowS
show :: ListSpec spec -> String
$cshow :: forall spec. Show spec => ListSpec spec -> String
showsPrec :: Int -> ListSpec spec -> ShowS
$cshowsPrec :: forall spec. Show spec => Int -> ListSpec spec -> ShowS
Show)
instance
(GenSym spec a, Mergeable a) =>
GenSym (ListSpec spec) [a]
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
ListSpec spec -> m (UnionM [a])
fresh (ListSpec Int
minLen Int
maxLen spec
subSpec) =
if Int
minLen forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
maxLen forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
minLen forall a. Ord a => a -> a -> Bool
>= Int
maxLen
then forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Bad lengths: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Int
minLen, Int
maxLen)
else do
[UnionM a]
l <- forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl Int
maxLen
let xs :: [[UnionM a]]
xs = forall a. Int -> [a] -> [a]
drop Int
minLen forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr (:) [] [UnionM a]
l
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[UnionM a]]
xs
where
gl :: (MonadFresh m) => Int -> m [UnionM a]
gl :: forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl Int
currLen
| Int
currLen forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do
UnionM a
l <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
subSpec
[UnionM a]
r <- forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl (Int
currLen forall a. Num a => a -> a -> a
- Int
1)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UnionM a
l forall a. a -> [a] -> [a]
: [UnionM a]
r
instance
(GenSym a a, Mergeable a) =>
GenSym [a] [a]
where
fresh :: forall (m :: * -> *). MonadFresh m => [a] -> m (UnionM [a])
fresh [a]
l = do
[UnionM a]
r :: [UnionM a] <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh [a]
l
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [UnionM a]
r
instance
(GenSymSimple a a) =>
GenSymSimple [a] [a]
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => [a] -> m [a]
simpleFresh = forall a (m :: * -> *).
(Generic a, GenSymSameShape (Rep a), MonadFresh m) =>
a -> m a
derivedSameShapeSimpleFresh
data SimpleListSpec spec = SimpleListSpec
{
forall spec. SimpleListSpec spec -> Int
genSimpleListLength :: Int,
forall spec. SimpleListSpec spec -> spec
genSimpleListSubSpec :: spec
}
deriving (Int -> SimpleListSpec spec -> ShowS
forall spec. Show spec => Int -> SimpleListSpec spec -> ShowS
forall spec. Show spec => [SimpleListSpec spec] -> ShowS
forall spec. Show spec => SimpleListSpec spec -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SimpleListSpec spec] -> ShowS
$cshowList :: forall spec. Show spec => [SimpleListSpec spec] -> ShowS
show :: SimpleListSpec spec -> String
$cshow :: forall spec. Show spec => SimpleListSpec spec -> String
showsPrec :: Int -> SimpleListSpec spec -> ShowS
$cshowsPrec :: forall spec. Show spec => Int -> SimpleListSpec spec -> ShowS
Show)
instance
(GenSym spec a, Mergeable a) =>
GenSym (SimpleListSpec spec) [a]
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
SimpleListSpec spec -> m (UnionM [a])
fresh (SimpleListSpec Int
len spec
subSpec) =
if Int
len forall a. Ord a => a -> a -> Bool
< Int
0
then forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Bad lengths: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
len
else do
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl Int
len
where
gl :: (MonadFresh m) => Int -> m [UnionM a]
gl :: forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl Int
currLen
| Int
currLen forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do
UnionM a
l <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
subSpec
[UnionM a]
r <- forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl (Int
currLen forall a. Num a => a -> a -> a
- Int
1)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UnionM a
l forall a. a -> [a] -> [a]
: [UnionM a]
r
instance
(GenSymSimple spec a) =>
GenSymSimple (SimpleListSpec spec) [a]
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => SimpleListSpec spec -> m [a]
simpleFresh (SimpleListSpec Int
len spec
subSpec) =
if Int
len forall a. Ord a => a -> a -> Bool
< Int
0
then forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Bad lengths: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
len
else do
forall (m :: * -> *). MonadFresh m => Int -> m [a]
gl Int
len
where
gl :: (MonadFresh m) => Int -> m [a]
gl :: forall (m :: * -> *). MonadFresh m => Int -> m [a]
gl Int
currLen
| Int
currLen forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do
a
l <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh spec
subSpec
[a]
r <- forall (m :: * -> *). MonadFresh m => Int -> m [a]
gl (Int
currLen forall a. Num a => a -> a -> a
- Int
1)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a
l forall a. a -> [a] -> [a]
: [a]
r
instance GenSym () ()
instance GenSymSimple () () where
simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m ()
simpleFresh = forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh
instance
( GenSym aspec a,
Mergeable a,
GenSym bspec b,
Mergeable b
) =>
GenSym (aspec, bspec) (a, b)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec) -> m (UnionM (a, b))
fresh (aspec
aspec, bspec
bspec) = do
UnionM a
a1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh bspec
bspec
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx)
instance
( GenSymSimple aspec a,
GenSymSimple bspec b
) =>
GenSymSimple (aspec, bspec) (a, b)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => (aspec, bspec) -> m (a, b)
simpleFresh (aspec
aspec, bspec
bspec) = do
(,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh bspec
bspec
instance
(GenSym () a, Mergeable a, GenSym () b, Mergeable b) =>
GenSym () (a, b)
where
fresh :: forall (m :: * -> *). MonadFresh m => () -> m (UnionM (a, b))
fresh = forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh
instance
( GenSymSimple () a,
GenSymSimple () b
) =>
GenSymSimple () (a, b)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m (a, b)
simpleFresh = forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh
instance
( GenSym aspec a,
Mergeable a,
GenSym bspec b,
Mergeable b,
GenSym cspec c,
Mergeable c
) =>
GenSym (aspec, bspec, cspec) (a, b, c)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec) -> m (UnionM (a, b, c))
fresh (aspec
aspec, bspec
bspec, cspec
cspec) = do
UnionM a
a1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh bspec
bspec
UnionM c
c1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh cspec
cspec
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx)
instance
( GenSymSimple aspec a,
GenSymSimple bspec b,
GenSymSimple cspec c
) =>
GenSymSimple (aspec, bspec, cspec) (a, b, c)
where
simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec) -> m (a, b, c)
simpleFresh (aspec
aspec, bspec
bspec, cspec
cspec) = do
(,,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh bspec
bspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh cspec
cspec
instance
( GenSym () a,
Mergeable a,
GenSym () b,
Mergeable b,
GenSym () c,
Mergeable c
) =>
GenSym () (a, b, c)
where
fresh :: forall (m :: * -> *). MonadFresh m => () -> m (UnionM (a, b, c))
fresh = forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh
instance
( GenSymSimple () a,
GenSymSimple () b,
GenSymSimple () c
) =>
GenSymSimple () (a, b, c)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m (a, b, c)
simpleFresh = forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh
instance
( GenSym aspec a,
Mergeable a,
GenSym bspec b,
Mergeable b,
GenSym cspec c,
Mergeable c,
GenSym dspec d,
Mergeable d
) =>
GenSym (aspec, bspec, cspec, dspec) (a, b, c, d)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec) -> m (UnionM (a, b, c, d))
fresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec) = do
UnionM a
a1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh bspec
bspec
UnionM c
c1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh cspec
cspec
UnionM d
d1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh dspec
dspec
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
d
dx <- UnionM d
d1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx)
instance
( GenSymSimple aspec a,
GenSymSimple bspec b,
GenSymSimple cspec c,
GenSymSimple dspec d
) =>
GenSymSimple (aspec, bspec, cspec, dspec) (a, b, c, d)
where
simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec) -> m (a, b, c, d)
simpleFresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec) = do
(,,,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh bspec
bspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh cspec
cspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh dspec
dspec
instance
( GenSym () a,
Mergeable a,
GenSym () b,
Mergeable b,
GenSym () c,
Mergeable c,
GenSym () d,
Mergeable d
) =>
GenSym () (a, b, c, d)
where
fresh :: forall (m :: * -> *). MonadFresh m => () -> m (UnionM (a, b, c, d))
fresh = forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh
instance
( GenSymSimple () a,
GenSymSimple () b,
GenSymSimple () c,
GenSymSimple () d
) =>
GenSymSimple () (a, b, c, d)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m (a, b, c, d)
simpleFresh = forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh
instance
( GenSym aspec a,
Mergeable a,
GenSym bspec b,
Mergeable b,
GenSym cspec c,
Mergeable c,
GenSym dspec d,
Mergeable d,
GenSym espec e,
Mergeable e
) =>
GenSym (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec) -> m (UnionM (a, b, c, d, e))
fresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec) = do
UnionM a
a1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh bspec
bspec
UnionM c
c1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh cspec
cspec
UnionM d
d1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh dspec
dspec
UnionM e
e1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh espec
espec
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
d
dx <- UnionM d
d1
e
ex <- UnionM e
e1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex)
instance
( GenSymSimple aspec a,
GenSymSimple bspec b,
GenSymSimple cspec c,
GenSymSimple dspec d,
GenSymSimple espec e
) =>
GenSymSimple (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)
where
simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec) -> m (a, b, c, d, e)
simpleFresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec) = do
(,,,,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh bspec
bspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh cspec
cspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh dspec
dspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh espec
espec
instance
( GenSym () a,
Mergeable a,
GenSym () b,
Mergeable b,
GenSym () c,
Mergeable c,
GenSym () d,
Mergeable d,
GenSym () e,
Mergeable e
) =>
GenSym () (a, b, c, d, e)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
() -> m (UnionM (a, b, c, d, e))
fresh = forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh
instance
( GenSymSimple () a,
GenSymSimple () b,
GenSymSimple () c,
GenSymSimple () d,
GenSymSimple () e
) =>
GenSymSimple () (a, b, c, d, e)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m (a, b, c, d, e)
simpleFresh = forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh
instance
( GenSym aspec a,
Mergeable a,
GenSym bspec b,
Mergeable b,
GenSym cspec c,
Mergeable c,
GenSym dspec d,
Mergeable d,
GenSym espec e,
Mergeable e,
GenSym fspec f,
Mergeable f
) =>
GenSym (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec, fspec)
-> m (UnionM (a, b, c, d, e, f))
fresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec) = do
UnionM a
a1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh bspec
bspec
UnionM c
c1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh cspec
cspec
UnionM d
d1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh dspec
dspec
UnionM e
e1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh espec
espec
UnionM f
f1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh fspec
fspec
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
d
dx <- UnionM d
d1
e
ex <- UnionM e
e1
f
fx <- UnionM f
f1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex, f
fx)
instance
( GenSymSimple aspec a,
GenSymSimple bspec b,
GenSymSimple cspec c,
GenSymSimple dspec d,
GenSymSimple espec e,
GenSymSimple fspec f
) =>
GenSymSimple (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)
where
simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec, fspec) -> m (a, b, c, d, e, f)
simpleFresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec) = do
(,,,,,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh bspec
bspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh cspec
cspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh dspec
dspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh espec
espec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh fspec
fspec
instance
( GenSym () a,
Mergeable a,
GenSym () b,
Mergeable b,
GenSym () c,
Mergeable c,
GenSym () d,
Mergeable d,
GenSym () e,
Mergeable e,
GenSym () f,
Mergeable f
) =>
GenSym () (a, b, c, d, e, f)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
() -> m (UnionM (a, b, c, d, e, f))
fresh = forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh
instance
( GenSymSimple () a,
GenSymSimple () b,
GenSymSimple () c,
GenSymSimple () d,
GenSymSimple () e,
GenSymSimple () f
) =>
GenSymSimple () (a, b, c, d, e, f)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m (a, b, c, d, e, f)
simpleFresh = forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh
instance
( GenSym aspec a,
Mergeable a,
GenSym bspec b,
Mergeable b,
GenSym cspec c,
Mergeable c,
GenSym dspec d,
Mergeable d,
GenSym espec e,
Mergeable e,
GenSym fspec f,
Mergeable f,
GenSym gspec g,
Mergeable g
) =>
GenSym (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec, fspec, gspec)
-> m (UnionM (a, b, c, d, e, f, g))
fresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec) = do
UnionM a
a1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh bspec
bspec
UnionM c
c1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh cspec
cspec
UnionM d
d1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh dspec
dspec
UnionM e
e1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh espec
espec
UnionM f
f1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh fspec
fspec
UnionM g
g1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh gspec
gspec
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
d
dx <- UnionM d
d1
e
ex <- UnionM e
e1
f
fx <- UnionM f
f1
g
gx <- UnionM g
g1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex, f
fx, g
gx)
instance
( GenSymSimple aspec a,
GenSymSimple bspec b,
GenSymSimple cspec c,
GenSymSimple dspec d,
GenSymSimple espec e,
GenSymSimple fspec f,
GenSymSimple gspec g
) =>
GenSymSimple (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)
where
simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec, fspec, gspec)
-> m (a, b, c, d, e, f, g)
simpleFresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec) = do
(,,,,,,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh bspec
bspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh cspec
cspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh dspec
dspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh espec
espec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh fspec
fspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh gspec
gspec
instance
( GenSym () a,
Mergeable a,
GenSym () b,
Mergeable b,
GenSym () c,
Mergeable c,
GenSym () d,
Mergeable d,
GenSym () e,
Mergeable e,
GenSym () f,
Mergeable f,
GenSym () g,
Mergeable g
) =>
GenSym () (a, b, c, d, e, f, g)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
() -> m (UnionM (a, b, c, d, e, f, g))
fresh = forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh
instance
( GenSymSimple () a,
GenSymSimple () b,
GenSymSimple () c,
GenSymSimple () d,
GenSymSimple () e,
GenSymSimple () f,
GenSymSimple () g
) =>
GenSymSimple () (a, b, c, d, e, f, g)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m (a, b, c, d, e, f, g)
simpleFresh = forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh
instance
( GenSym aspec a,
Mergeable a,
GenSym bspec b,
Mergeable b,
GenSym cspec c,
Mergeable c,
GenSym dspec d,
Mergeable d,
GenSym espec e,
Mergeable e,
GenSym fspec f,
Mergeable f,
GenSym gspec g,
Mergeable g,
GenSym hspec h,
Mergeable h
) =>
GenSym (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec)
-> m (UnionM (a, b, c, d, e, f, g, h))
fresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec, hspec
hspec) = do
UnionM a
a1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh bspec
bspec
UnionM c
c1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh cspec
cspec
UnionM d
d1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh dspec
dspec
UnionM e
e1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh espec
espec
UnionM f
f1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh fspec
fspec
UnionM g
g1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh gspec
gspec
UnionM h
h1 <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh hspec
hspec
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
d
dx <- UnionM d
d1
e
ex <- UnionM e
e1
f
fx <- UnionM f
f1
g
gx <- UnionM g
g1
h
hx <- UnionM h
h1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex, f
fx, g
gx, h
hx)
instance
( GenSymSimple aspec a,
GenSymSimple bspec b,
GenSymSimple cspec c,
GenSymSimple dspec d,
GenSymSimple espec e,
GenSymSimple fspec f,
GenSymSimple gspec g,
GenSymSimple hspec h
) =>
GenSymSimple (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)
where
simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec)
-> m (a, b, c, d, e, f, g, h)
simpleFresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec, hspec
hspec) = do
(,,,,,,,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh bspec
bspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh cspec
cspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh dspec
dspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh espec
espec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh fspec
fspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh gspec
gspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh hspec
hspec
instance
( GenSym () a,
Mergeable a,
GenSym () b,
Mergeable b,
GenSym () c,
Mergeable c,
GenSym () d,
Mergeable d,
GenSym () e,
Mergeable e,
GenSym () f,
Mergeable f,
GenSym () g,
Mergeable g,
GenSym () h,
Mergeable h
) =>
GenSym () (a, b, c, d, e, f, g, h)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
() -> m (UnionM (a, b, c, d, e, f, g, h))
fresh = forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh
instance
( GenSymSimple () a,
GenSymSimple () b,
GenSymSimple () c,
GenSymSimple () d,
GenSymSimple () e,
GenSymSimple () f,
GenSymSimple () g,
GenSymSimple () h
) =>
GenSymSimple () (a, b, c, d, e, f, g, h)
where
simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
() -> m (a, b, c, d, e, f, g, h)
simpleFresh = forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh
instance
{-# OVERLAPPABLE #-}
( GenSym spec (m (Maybe a)),
Mergeable1 m,
Mergeable a
) =>
GenSym spec (MaybeT m a)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
spec -> m (UnionM (MaybeT m a))
fresh spec
v = do
UnionM (m (Maybe a))
x <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
v
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ UnionM (m (Maybe a))
x
instance
{-# OVERLAPPABLE #-}
( GenSymSimple spec (m (Maybe a))
) =>
GenSymSimple spec (MaybeT m a)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => spec -> m (MaybeT m a)
simpleFresh spec
v = forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh spec
v
instance
{-# OVERLAPPING #-}
( GenSymSimple (m (Maybe a)) (m (Maybe a))
) =>
GenSymSimple (MaybeT m a) (MaybeT m a)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => MaybeT m a -> m (MaybeT m a)
simpleFresh (MaybeT m (Maybe a)
v) = forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh m (Maybe a)
v
instance
{-# OVERLAPPING #-}
( GenSymSimple (m (Maybe a)) (m (Maybe a)),
Mergeable1 m,
Mergeable a
) =>
GenSym (MaybeT m a) (MaybeT m a)
instance
{-# OVERLAPPABLE #-}
( GenSym spec (m (Either a b)),
Mergeable1 m,
Mergeable a,
Mergeable b
) =>
GenSym spec (ExceptT a m b)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
spec -> m (UnionM (ExceptT a m b))
fresh spec
v = do
UnionM (m (Either a b))
x <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
v
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> b
$ UnionM (m (Either a b))
x
instance
{-# OVERLAPPABLE #-}
( GenSymSimple spec (m (Either a b))
) =>
GenSymSimple spec (ExceptT a m b)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => spec -> m (ExceptT a m b)
simpleFresh spec
v = forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh spec
v
instance
{-# OVERLAPPING #-}
( GenSymSimple (m (Either e a)) (m (Either e a))
) =>
GenSymSimple (ExceptT e m a) (ExceptT e m a)
where
simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
ExceptT e m a -> m (ExceptT e m a)
simpleFresh (ExceptT m (Either e a)
v) = forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh m (Either e a)
v
instance
{-# OVERLAPPING #-}
( GenSymSimple (m (Either e a)) (m (Either e a)),
Mergeable1 m,
Mergeable e,
Mergeable a
) =>
GenSym (ExceptT e m a) (ExceptT e m a)
#define GENSYM_SIMPLE(symtype) \
instance GenSym symtype symtype
#define GENSYM_SIMPLE_SIMPLE(symtype) \
instance GenSymSimple symtype symtype where \
simpleFresh _ = simpleFresh ()
#define GENSYM_UNIT_SIMPLE(symtype) \
instance GenSym () symtype where \
fresh _ = mrgSingle <$> simpleFresh ()
#define GENSYM_UNIT_SIMPLE_SIMPLE(symtype) \
instance GenSymSimple () symtype where \
simpleFresh _ = do; \
ident <- getFreshIdent; \
FreshIndex i <- nextFreshIndex; \
case ident of; \
FreshIdent s -> return $ isym s i; \
FreshIdentWithInfo s info -> return $ iinfosym s i info
#define GENSYM_BV(symtype) \
instance (KnownNat n, 1 <= n) => GenSym (symtype n) (symtype n)
#define GENSYM_SIMPLE_BV(symtype) \
instance (KnownNat n, 1 <= n) => GenSymSimple (symtype n) (symtype n) where \
simpleFresh _ = simpleFresh ()
#define GENSYM_UNIT_BV(symtype) \
instance (KnownNat n, 1 <= n) => GenSym () (symtype n) where \
fresh _ = mrgSingle <$> simpleFresh ()
#define GENSYM_UNIT_SIMPLE_BV(symtype) \
instance (KnownNat n, 1 <= n) => GenSymSimple () (symtype n) where \
simpleFresh _ = do; \
ident <- getFreshIdent; \
FreshIndex i <- nextFreshIndex; \
case ident of; \
FreshIdent s -> return $ isym s i; \
FreshIdentWithInfo s info -> return $ iinfosym s i info
#define GENSYM_BV_SOME(symtype) \
instance GenSym symtype symtype
#define GENSYM_SIMPLE_BV_SOME(symtype) \
instance GenSymSimple symtype symtype where \
simpleFresh (symtype v) = simpleFresh v
#define GENSYM_N_BV_SOME(symtype) \
instance (KnownNat n, 1 <= n) => GenSym (p n) symtype where \
fresh p = mrgSingle <$> simpleFresh p
#define GENSYM_N_SIMPLE_BV_SOME(symtype, origtype) \
instance (KnownNat n, 1 <= n) => GenSymSimple (p n) symtype where \
simpleFresh _ = do; \
i :: origtype n <- simpleFresh (); \
return $ symtype i
#define GENSYM_N_INT_BV_SOME(symtype) \
instance GenSym Int symtype where \
fresh p = mrgSingle <$> simpleFresh p
#define GENSYM_N_INT_SIMPLE_BV_SOME(symtype, origtype) \
instance GenSymSimple Int symtype where \
simpleFresh i = if i > 0 then f (Proxy @0) else \
error "Can only generate bit vectors with positive bit size" \
where \
f :: forall p (n :: Nat) m. (MonadFresh m) => p n -> m symtype; \
f _ = case (unsafeKnownProof @n (fromIntegral i), unsafeLeqProof @1 @n) of \
(KnownProof, LeqProof) -> do \
v :: origtype n <- simpleFresh (); \
return $ symtype v; \
#define GENSYM_FUN(op) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GenSym (sa op sb) (sa op sb)
#define GENSYM_SIMPLE_FUN(op) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GenSymSimple (sa op sb) (sa op sb) where \
simpleFresh _ = simpleFresh ()
#define GENSYM_UNIT_FUN(op) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GenSym () (sa op sb) where \
fresh _ = mrgSingle <$> simpleFresh ()
#define GENSYM_UNIT_SIMPLE_FUN(op) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GenSymSimple () (sa op sb) where \
simpleFresh _ = do; \
ident <- getFreshIdent; \
FreshIndex i <- nextFreshIndex; \
case ident of; \
FreshIdent s -> return $ isym s i; \
FreshIdentWithInfo s info -> return $ iinfosym s i info
#if 1
GENSYM_SIMPLE(SymBool)
GENSYM_SIMPLE_SIMPLE(SymBool)
GENSYM_UNIT_SIMPLE(SymBool)
GENSYM_UNIT_SIMPLE_SIMPLE(SymBool)
GENSYM_SIMPLE(SymInteger)
GENSYM_SIMPLE_SIMPLE(SymInteger)
GENSYM_UNIT_SIMPLE(SymInteger)
GENSYM_UNIT_SIMPLE_SIMPLE(SymInteger)
GENSYM_BV(SymIntN)
GENSYM_SIMPLE_BV(SymIntN)
GENSYM_UNIT_BV(SymIntN)
GENSYM_UNIT_SIMPLE_BV(SymIntN)
GENSYM_BV(SymWordN)
GENSYM_SIMPLE_BV(SymWordN)
GENSYM_UNIT_BV(SymWordN)
GENSYM_UNIT_SIMPLE_BV(SymWordN)
GENSYM_BV_SOME(SomeSymIntN)
GENSYM_SIMPLE_BV_SOME(SomeSymIntN)
GENSYM_N_BV_SOME(SomeSymIntN)
GENSYM_N_SIMPLE_BV_SOME(SomeSymIntN, SymIntN)
GENSYM_N_INT_BV_SOME(SomeSymIntN)
GENSYM_N_INT_SIMPLE_BV_SOME(SomeSymIntN, SymIntN)
GENSYM_BV_SOME(SomeSymWordN)
GENSYM_SIMPLE_BV_SOME(SomeSymWordN)
GENSYM_N_BV_SOME(SomeSymWordN)
GENSYM_N_SIMPLE_BV_SOME(SomeSymWordN, SymWordN)
GENSYM_N_INT_BV_SOME(SomeSymWordN)
GENSYM_N_INT_SIMPLE_BV_SOME(SomeSymWordN, SymWordN)
GENSYM_FUN(=~>)
GENSYM_SIMPLE_FUN(=~>)
GENSYM_UNIT_FUN(=~>)
GENSYM_UNIT_SIMPLE_FUN(=~>)
GENSYM_FUN(-~>)
GENSYM_SIMPLE_FUN(-~>)
GENSYM_UNIT_FUN(-~>)
GENSYM_UNIT_SIMPLE_FUN(-~>)
#endif