{-# 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 (..),
nextFreshIndex,
liftFresh,
FreshT (FreshT, runFreshTFromIndex),
Fresh,
runFreshT,
runFresh,
mrgRunFreshT,
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)
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 Grisette.Core.Control.Monad.UnionM (UnionM, isMerged, underlyingUnion)
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.Core.Data.Union (Union (UnionIf, UnionSingle))
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
( LinkedRep,
SupportedPrim,
)
import 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
(Int -> FreshIndex -> ShowS)
-> (FreshIndex -> String)
-> ([FreshIndex] -> ShowS)
-> Show FreshIndex
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FreshIndex -> ShowS
showsPrec :: Int -> FreshIndex -> ShowS
$cshow :: FreshIndex -> String
show :: FreshIndex -> String
$cshowList :: [FreshIndex] -> ShowS
showList :: [FreshIndex] -> ShowS
Show)
deriving (FreshIndex -> FreshIndex -> Bool
(FreshIndex -> FreshIndex -> Bool)
-> (FreshIndex -> FreshIndex -> Bool) -> Eq FreshIndex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FreshIndex -> FreshIndex -> Bool
== :: FreshIndex -> FreshIndex -> Bool
$c/= :: FreshIndex -> FreshIndex -> Bool
/= :: FreshIndex -> FreshIndex -> Bool
Eq, Eq FreshIndex
Eq FreshIndex =>
(FreshIndex -> FreshIndex -> Ordering)
-> (FreshIndex -> FreshIndex -> Bool)
-> (FreshIndex -> FreshIndex -> Bool)
-> (FreshIndex -> FreshIndex -> Bool)
-> (FreshIndex -> FreshIndex -> Bool)
-> (FreshIndex -> FreshIndex -> FreshIndex)
-> (FreshIndex -> FreshIndex -> FreshIndex)
-> Ord 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
$ccompare :: FreshIndex -> FreshIndex -> Ordering
compare :: FreshIndex -> FreshIndex -> Ordering
$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
>= :: FreshIndex -> FreshIndex -> Bool
$cmax :: FreshIndex -> FreshIndex -> FreshIndex
max :: FreshIndex -> FreshIndex -> FreshIndex
$cmin :: FreshIndex -> FreshIndex -> FreshIndex
min :: FreshIndex -> FreshIndex -> FreshIndex
Ord, Integer -> FreshIndex
FreshIndex -> FreshIndex
FreshIndex -> FreshIndex -> FreshIndex
(FreshIndex -> FreshIndex -> FreshIndex)
-> (FreshIndex -> FreshIndex -> FreshIndex)
-> (FreshIndex -> FreshIndex -> FreshIndex)
-> (FreshIndex -> FreshIndex)
-> (FreshIndex -> FreshIndex)
-> (FreshIndex -> FreshIndex)
-> (Integer -> FreshIndex)
-> Num FreshIndex
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: FreshIndex -> FreshIndex -> FreshIndex
+ :: FreshIndex -> FreshIndex -> FreshIndex
$c- :: FreshIndex -> FreshIndex -> FreshIndex
- :: FreshIndex -> FreshIndex -> FreshIndex
$c* :: FreshIndex -> FreshIndex -> FreshIndex
* :: FreshIndex -> FreshIndex -> FreshIndex
$cnegate :: FreshIndex -> FreshIndex
negate :: FreshIndex -> FreshIndex
$cabs :: FreshIndex -> FreshIndex
abs :: FreshIndex -> FreshIndex
$csignum :: FreshIndex -> FreshIndex
signum :: FreshIndex -> FreshIndex
$cfromInteger :: Integer -> FreshIndex
fromInteger :: Integer -> FreshIndex
Num) via Int
instance Mergeable FreshIndex where
rootStrategy :: MergingStrategy FreshIndex
rootStrategy = (SymBool -> FreshIndex -> FreshIndex -> FreshIndex)
-> MergingStrategy FreshIndex
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> FreshIndex -> FreshIndex -> FreshIndex)
-> MergingStrategy FreshIndex)
-> (SymBool -> FreshIndex -> FreshIndex -> FreshIndex)
-> MergingStrategy FreshIndex
forall a b. (a -> b) -> a -> b
$ \SymBool
_ FreshIndex
t FreshIndex
f -> FreshIndex -> FreshIndex -> FreshIndex
forall a. Ord a => a -> a -> a
max FreshIndex
t FreshIndex
f
instance SimpleMergeable FreshIndex where
mrgIte :: SymBool -> FreshIndex -> FreshIndex -> FreshIndex
mrgIte SymBool
_ = FreshIndex -> FreshIndex -> FreshIndex
forall a. Ord a => a -> a -> a
max
data FreshIdent where
FreshIdent :: T.Text -> FreshIdent
FreshIdentWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => T.Text -> a -> FreshIdent
instance Show FreshIdent where
show :: FreshIdent -> String
show (FreshIdent Text
i) = Text -> String
T.unpack Text
i
show (FreshIdentWithInfo Text
s a
i) = Text -> String
T.unpack Text
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i
instance IsString FreshIdent where
fromString :: String -> FreshIdent
fromString = Text -> FreshIdent
name (Text -> FreshIdent) -> (String -> Text) -> String -> FreshIdent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack
instance Eq FreshIdent where
FreshIdent Text
l == :: FreshIdent -> FreshIdent -> Bool
== FreshIdent Text
r = Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
r
FreshIdentWithInfo Text
l (a
linfo :: linfo) == FreshIdentWithInfo Text
r (a
rinfo :: rinfo) = case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @linfo @rinfo of
Just a :~: a
Refl -> Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
r Bool -> Bool -> Bool
&& a
linfo a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a
rinfo
Maybe (a :~: a)
_ -> Bool
False
FreshIdent
_ == FreshIdent
_ = Bool
False
instance Ord FreshIdent where
FreshIdent Text
l <= :: FreshIdent -> FreshIdent -> Bool
<= FreshIdent Text
r = Text
l Text -> Text -> Bool
forall a. Ord a => a -> a -> Bool
<= Text
r
FreshIdent Text
_ <= FreshIdent
_ = Bool
True
FreshIdent
_ <= FreshIdent Text
_ = Bool
False
FreshIdentWithInfo Text
l (a
linfo :: linfo) <= FreshIdentWithInfo Text
r (a
rinfo :: rinfo) =
Text
l Text -> Text -> Bool
forall a. Ord a => a -> a -> Bool
< Text
r
Bool -> Bool -> Bool
|| ( Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
r
Bool -> Bool -> Bool
&& ( case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @linfo @rinfo of
Just a :~: a
Refl -> a
linfo a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
a
rinfo
Maybe (a :~: a)
_ -> Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @linfo) TypeRep -> TypeRep -> Bool
forall a. Ord a => a -> a -> Bool
<= Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @rinfo)
)
)
instance Hashable FreshIdent where
hashWithSalt :: Int -> FreshIdent -> Int
hashWithSalt Int
s (FreshIdent Text
n) = Int
s Int -> Text -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Text
n
hashWithSalt Int
s (FreshIdentWithInfo Text
n a
i) = Int
s Int -> Text -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Text
n Int -> a -> Int
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 Text
n) = [||Text -> FreshIdent
FreshIdent Text
n||]
liftTyped (FreshIdentWithInfo Text
n a
i) = [||Text -> a -> FreshIdent
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> a -> FreshIdent
FreshIdentWithInfo Text
n a
i||]
instance NFData FreshIdent where
rnf :: FreshIdent -> ()
rnf (FreshIdent Text
n) = Text -> ()
forall a. NFData a => a -> ()
rnf Text
n
rnf (FreshIdentWithInfo Text
n a
i) = Text -> ()
forall a. NFData a => a -> ()
rnf Text
n () -> () -> ()
forall a b. a -> b -> b
`seq` a -> ()
forall a. NFData a => a -> ()
rnf a
i
name :: T.Text -> FreshIdent
name :: Text -> FreshIdent
name = Text -> FreshIdent
FreshIdent
nameWithInfo :: forall a. (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => T.Text -> a -> FreshIdent
nameWithInfo :: forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> a -> FreshIdent
nameWithInfo = Text -> a -> FreshIdent
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> a -> FreshIdent
FreshIdentWithInfo
class (Monad m) => MonadFresh m where
getFreshIndex :: m FreshIndex
setFreshIndex :: FreshIndex -> m ()
getFreshIdent :: m FreshIdent
nextFreshIndex :: (MonadFresh m) => m FreshIndex
nextFreshIndex :: forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex = do
FreshIndex
curr <- m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
let new :: FreshIndex
new = FreshIndex
curr FreshIndex -> FreshIndex -> FreshIndex
forall a. Num a => a -> a -> a
+ FreshIndex
1
FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
new
FreshIndex -> m FreshIndex
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return FreshIndex
curr
liftFresh :: (MonadFresh m) => Fresh a -> m a
liftFresh :: forall (m :: * -> *) a. MonadFresh m => Fresh a -> m a
liftFresh (FreshT FreshIdent -> FreshIndex -> Identity (a, FreshIndex)
f) = do
FreshIndex
index <- m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
FreshIdent
ident <- m FreshIdent
forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
let (a
a, FreshIndex
newIdx) = Identity (a, FreshIndex) -> (a, FreshIndex)
forall a. Identity a -> a
runIdentity (Identity (a, FreshIndex) -> (a, FreshIndex))
-> Identity (a, FreshIndex) -> (a, FreshIndex)
forall a b. (a -> b) -> a -> b
$ FreshIdent -> FreshIndex -> Identity (a, FreshIndex)
f FreshIdent
ident FreshIndex
index
FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
newtype FreshT m a = FreshT
{ forall (m :: * -> *) a.
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex :: FreshIdent -> FreshIndex -> m (a, FreshIndex)
}
instance
(Mergeable a, Mergeable1 m) =>
Mergeable (FreshT m a)
where
rootStrategy :: MergingStrategy (FreshT m a)
rootStrategy =
MergingStrategy (FreshIdent -> FreshIndex -> m (a, FreshIndex))
-> ((FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex))
-> MergingStrategy (FreshT m a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (MergingStrategy (FreshIndex -> m (a, FreshIndex))
-> MergingStrategy (FreshIdent -> FreshIndex -> m (a, FreshIndex))
forall a. MergingStrategy a -> MergingStrategy (FreshIdent -> a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (MergingStrategy (m (a, FreshIndex))
-> MergingStrategy (FreshIndex -> m (a, FreshIndex))
forall a. MergingStrategy a -> MergingStrategy (FreshIndex -> a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy MergingStrategy (m (a, FreshIndex))
forall a (u :: * -> *).
(Mergeable a, Mergeable1 u) =>
MergingStrategy (u a)
rootStrategy1)) (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex
instance (Mergeable1 m) => Mergeable1 (FreshT m) where
liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (FreshT m a)
liftRootStrategy MergingStrategy a
m =
MergingStrategy (FreshIdent -> FreshIndex -> m (a, FreshIndex))
-> ((FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex))
-> MergingStrategy (FreshT m a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy
(MergingStrategy (FreshIndex -> m (a, FreshIndex))
-> MergingStrategy (FreshIdent -> FreshIndex -> m (a, FreshIndex))
forall a. MergingStrategy a -> MergingStrategy (FreshIdent -> a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (MergingStrategy (m (a, FreshIndex))
-> MergingStrategy (FreshIndex -> m (a, FreshIndex))
forall a. MergingStrategy a -> MergingStrategy (FreshIndex -> a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (MergingStrategy (a, FreshIndex)
-> MergingStrategy (m (a, FreshIndex))
forall a. MergingStrategy a -> MergingStrategy (m a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (MergingStrategy a
-> MergingStrategy FreshIndex -> MergingStrategy (a, FreshIndex)
forall a b.
MergingStrategy a -> MergingStrategy b -> MergingStrategy (a, b)
forall (u :: * -> * -> *) a b.
Mergeable2 u =>
MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
liftRootStrategy2 MergingStrategy a
m MergingStrategy FreshIndex
forall a. Mergeable a => MergingStrategy a
rootStrategy))))
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex
instance
(UnionLike m, Mergeable a) =>
SimpleMergeable (FreshT m a)
where
mrgIte :: SymBool -> FreshT m a -> FreshT m a -> FreshT m a
mrgIte = SymBool -> FreshT m a -> FreshT m a -> FreshT m a
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 = MergingStrategy a
-> SymBool -> FreshT m a -> FreshT m a -> FreshT m a
forall a.
MergingStrategy a
-> SymBool -> FreshT m a -> FreshT m a -> FreshT m a
forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy ((SymBool -> a -> a -> a) -> MergingStrategy a
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) =
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> MergingStrategy (a, FreshIndex)
-> m (a, FreshIndex) -> m (a, FreshIndex)
forall a. MergingStrategy a -> m a -> m a
forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy (MergingStrategy a
-> MergingStrategy FreshIndex -> MergingStrategy (a, FreshIndex)
forall a b.
MergingStrategy a -> MergingStrategy b -> MergingStrategy (a, b)
forall (u :: * -> * -> *) a b.
Mergeable2 u =>
MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
liftRootStrategy2 MergingStrategy a
s MergingStrategy FreshIndex
forall a. Mergeable a => MergingStrategy a
rootStrategy) (m (a, FreshIndex) -> m (a, FreshIndex))
-> m (a, FreshIndex) -> m (a, FreshIndex)
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) =
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> MergingStrategy (a, FreshIndex)
-> SymBool
-> m (a, FreshIndex)
-> m (a, FreshIndex)
-> m (a, FreshIndex)
forall a. MergingStrategy a -> SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy (MergingStrategy a
-> MergingStrategy FreshIndex -> MergingStrategy (a, FreshIndex)
forall a b.
MergingStrategy a -> MergingStrategy b -> MergingStrategy (a, b)
forall (u :: * -> * -> *) a b.
Mergeable2 u =>
MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
liftRootStrategy2 MergingStrategy a
s MergingStrategy FreshIndex
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 = (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
i -> (a, FreshIndex) -> m (a, FreshIndex)
forall a. a -> m a
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) =
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> SymBool
-> m (a, FreshIndex) -> m (a, FreshIndex) -> m (a, FreshIndex)
forall a. SymBool -> m a -> m a -> m a
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 = (a, FreshIndex) -> a
forall a b. (a, b) -> a
fst ((a, FreshIndex) -> a) -> m (a, FreshIndex) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex FreshT m a
m FreshIdent
ident (Int -> FreshIndex
FreshIndex Int
0)
mrgRunFreshT ::
(Monad m, UnionLike m, Mergeable a) =>
FreshT m a ->
FreshIdent ->
m a
mrgRunFreshT :: forall (m :: * -> *) a.
(Monad m, UnionLike m, Mergeable a) =>
FreshT m a -> FreshIdent -> m a
mrgRunFreshT FreshT m a
m FreshIdent
ident = m a -> m a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ FreshT m a -> FreshIdent -> m a
forall (m :: * -> *) a. Monad m => FreshT m a -> FreshIdent -> m a
runFreshT FreshT m a
m FreshIdent
ident
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) = (FreshIdent -> FreshIndex -> f (b, FreshIndex)) -> FreshT f b
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> f (b, FreshIndex)) -> FreshT f b)
-> (FreshIdent -> FreshIndex -> f (b, FreshIndex)) -> FreshT f b
forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
idx -> (a -> b) -> (a, FreshIndex) -> (b, FreshIndex)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> b
f ((a, FreshIndex) -> (b, FreshIndex))
-> f (a, FreshIndex) -> f (b, FreshIndex)
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 = (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
idx -> (a, FreshIndex) -> m (a, FreshIndex)
forall a. a -> m a
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 = (FreshIdent -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b)
-> (FreshIdent -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b
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'
(b, FreshIndex) -> m (b, FreshIndex)
forall a. a -> m a
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 = (FreshIdent -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b)
-> (FreshIdent -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b
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
FreshT m b -> FreshIdent -> FreshIndex -> m (b, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex (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 = (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
index -> (,FreshIndex
index) (a -> (a, FreshIndex)) -> m a -> m (a, FreshIndex)
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 =
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
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 -> FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> FreshIdent -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex (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 = m a -> FreshT m a
forall (m :: * -> *) a. Monad m => m a -> FreshT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> FreshT m a) -> (e -> m a) -> e -> FreshT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> m a
forall a. e -> m a
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 = Catch e m (a, FreshIndex) -> Catch e (FreshT m) a
forall (m :: * -> *) e a.
Functor m =>
Catch e m (a, FreshIndex) -> Catch e (FreshT m) a
liftFreshTCache Catch e m (a, FreshIndex)
forall a. m a -> (e -> m a) -> m a
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 = (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
index -> (,FreshIndex
index) (a -> (a, FreshIndex)) -> m a -> m (a, FreshIndex)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a, w) -> m a
forall a. (a, w) -> m a
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) = (FreshIdent -> FreshIndex -> m ((a, w), FreshIndex))
-> FreshT m (a, w)
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m ((a, w), FreshIndex))
-> FreshT m (a, w))
-> (FreshIdent -> FreshIndex -> m ((a, w), FreshIndex))
-> FreshT m (a, w)
forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> (\((a
a, FreshIndex
b), w
c) -> ((a
a, w
c), FreshIndex
b)) (((a, FreshIndex), w) -> ((a, w), FreshIndex))
-> m ((a, FreshIndex), w) -> m ((a, w), FreshIndex)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (a, FreshIndex) -> m ((a, FreshIndex), w)
forall a. m a -> m (a, w)
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) = (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> m ((a, FreshIndex), w -> w) -> m (a, FreshIndex)
forall a. m (a, w -> w) -> m a
forall w (m :: * -> *) a. MonadWriter w m => m (a, w -> w) -> m a
pass (m ((a, FreshIndex), w -> w) -> m (a, FreshIndex))
-> m ((a, FreshIndex), w -> w) -> m (a, FreshIndex)
forall a b. (a -> b) -> a -> b
$ (\((a
a, w -> w
b), FreshIndex
c) -> ((a
a, FreshIndex
c), w -> w
b)) (((a, w -> w), FreshIndex) -> ((a, FreshIndex), w -> w))
-> m ((a, w -> w), FreshIndex) -> m ((a, FreshIndex), w -> w)
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 = (FreshIdent -> FreshIndex -> m (s, FreshIndex)) -> FreshT m s
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (s, FreshIndex)) -> FreshT m s)
-> (FreshIdent -> FreshIndex -> m (s, FreshIndex)) -> FreshT m s
forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
index -> (s -> (s, FreshIndex)) -> m (s, FreshIndex)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (,FreshIndex
index)
put :: s -> FreshT m ()
put s
s = (FreshIdent -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ()
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ())
-> (FreshIdent -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ()
forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
index -> (,FreshIndex
index) (() -> ((), FreshIndex)) -> m () -> m ((), FreshIndex)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s -> m ()
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) = (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \FreshIdent
ident FreshIndex
index -> (r -> r) -> m (a, FreshIndex) -> m (a, FreshIndex)
forall a. (r -> r) -> m a -> m a
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 = (FreshIdent -> FreshIndex -> m (r, FreshIndex)) -> FreshT m r
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (r, FreshIndex)) -> FreshT m r)
-> (FreshIdent -> FreshIndex -> m (r, FreshIndex)) -> FreshT m r
forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
index -> (r -> (r, FreshIndex)) -> m (r, FreshIndex)
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
getFreshIndex :: ExceptT e m FreshIndex
getFreshIndex = m FreshIndex -> ExceptT e m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> ExceptT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
setFreshIndex :: FreshIndex -> ExceptT e m ()
setFreshIndex FreshIndex
newIdx = m () -> ExceptT e m ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT e m ()) -> m () -> ExceptT e m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
getFreshIdent :: ExceptT e m FreshIdent
getFreshIdent = m FreshIdent -> ExceptT e m FreshIdent
forall (m :: * -> *) a. Monad m => m a -> ExceptT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIdent
forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m, Monoid w) => MonadFresh (WriterLazy.WriterT w m) where
getFreshIndex :: WriterT w m FreshIndex
getFreshIndex = m FreshIndex -> WriterT w m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
setFreshIndex :: FreshIndex -> WriterT w m ()
setFreshIndex FreshIndex
newIdx = m () -> WriterT w m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT w m ()) -> m () -> WriterT w m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
getFreshIdent :: WriterT w m FreshIdent
getFreshIdent = m FreshIdent -> WriterT w m FreshIdent
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIdent
forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m, Monoid w) => MonadFresh (WriterStrict.WriterT w m) where
getFreshIndex :: WriterT w m FreshIndex
getFreshIndex = m FreshIndex -> WriterT w m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
setFreshIndex :: FreshIndex -> WriterT w m ()
setFreshIndex FreshIndex
newIdx = m () -> WriterT w m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT w m ()) -> m () -> WriterT w m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
getFreshIdent :: WriterT w m FreshIdent
getFreshIdent = m FreshIdent -> WriterT w m FreshIdent
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIdent
forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m) => MonadFresh (StateLazy.StateT s m) where
getFreshIndex :: StateT s m FreshIndex
getFreshIndex = m FreshIndex -> StateT s m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
setFreshIndex :: FreshIndex -> StateT s m ()
setFreshIndex FreshIndex
newIdx = m () -> StateT s m ()
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT s m ()) -> m () -> StateT s m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
getFreshIdent :: StateT s m FreshIdent
getFreshIdent = m FreshIdent -> StateT s m FreshIdent
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIdent
forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m) => MonadFresh (StateStrict.StateT s m) where
getFreshIndex :: StateT s m FreshIndex
getFreshIndex = m FreshIndex -> StateT s m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
setFreshIndex :: FreshIndex -> StateT s m ()
setFreshIndex FreshIndex
newIdx = m () -> StateT s m ()
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT s m ()) -> m () -> StateT s m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
getFreshIdent :: StateT s m FreshIdent
getFreshIdent = m FreshIdent -> StateT s m FreshIdent
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIdent
forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m) => MonadFresh (ReaderT r m) where
getFreshIndex :: ReaderT r m FreshIndex
getFreshIndex = m FreshIndex -> ReaderT r m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
setFreshIndex :: FreshIndex -> ReaderT r m ()
setFreshIndex FreshIndex
newIdx = m () -> ReaderT r m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
getFreshIdent :: ReaderT r m FreshIdent
getFreshIdent = m FreshIdent -> ReaderT r m FreshIdent
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIdent
forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m, Monoid w) => MonadFresh (RWSLazy.RWST r w s m) where
getFreshIndex :: RWST r w s m FreshIndex
getFreshIndex = m FreshIndex -> RWST r w s m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
setFreshIndex :: FreshIndex -> RWST r w s m ()
setFreshIndex FreshIndex
newIdx = m () -> RWST r w s m ()
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> RWST r w s m ()) -> m () -> RWST r w s m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
getFreshIdent :: RWST r w s m FreshIdent
getFreshIdent = m FreshIdent -> RWST r w s m FreshIdent
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIdent
forall (m :: * -> *). MonadFresh m => m FreshIdent
getFreshIdent
instance (MonadFresh m, Monoid w) => MonadFresh (RWSStrict.RWST r w s m) where
getFreshIndex :: RWST r w s m FreshIndex
getFreshIndex = m FreshIndex -> RWST r w s m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
setFreshIndex :: FreshIndex -> RWST r w s m ()
setFreshIndex FreshIndex
newIdx = m () -> RWST r w s m ()
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> RWST r w s m ()) -> m () -> RWST r w s m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
getFreshIdent :: RWST r w s m FreshIdent
getFreshIdent = m FreshIdent -> RWST r w s m FreshIdent
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIdent
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 = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> Identity a -> a
forall a b. (a -> b) -> a -> b
$ Fresh a -> FreshIdent -> Identity a
forall (m :: * -> *) a. Monad m => FreshT m a -> FreshIdent -> m a
runFreshT Fresh a
m FreshIdent
ident
instance (Monad m) => MonadFresh (FreshT m) where
getFreshIndex :: FreshT m FreshIndex
getFreshIndex = (FreshIdent -> FreshIndex -> m (FreshIndex, FreshIndex))
-> FreshT m FreshIndex
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (FreshIndex, FreshIndex))
-> FreshT m FreshIndex)
-> (FreshIdent -> FreshIndex -> m (FreshIndex, FreshIndex))
-> FreshT m FreshIndex
forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
idx -> (FreshIndex, FreshIndex) -> m (FreshIndex, FreshIndex)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FreshIndex
idx, FreshIndex
idx)
setFreshIndex :: FreshIndex -> FreshT m ()
setFreshIndex FreshIndex
newIdx = (FreshIdent -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ()
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ())
-> (FreshIdent -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ()
forall a b. (a -> b) -> a -> b
$ \FreshIdent
_ FreshIndex
_ -> ((), FreshIndex) -> m ((), FreshIndex)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((), FreshIndex
newIdx)
getFreshIdent :: FreshT m FreshIdent
getFreshIdent = (FreshIdent -> FreshIndex -> m (FreshIdent, FreshIndex))
-> FreshT m FreshIdent
forall (m :: * -> *) a.
(FreshIdent -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((FreshIdent -> FreshIndex -> m (FreshIdent, FreshIndex))
-> FreshT m FreshIdent)
-> (FreshIdent -> FreshIndex -> m (FreshIdent, FreshIndex))
-> FreshT m FreshIdent
forall a b. (a -> b) -> a -> b
$ ((FreshIdent, FreshIndex) -> m (FreshIdent, FreshIndex))
-> FreshIdent -> FreshIndex -> m (FreshIdent, FreshIndex)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (FreshIdent, FreshIndex) -> m (FreshIdent, FreshIndex)
forall a. a -> m a
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 = a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> m a -> m (UnionM a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> spec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). 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 = Fresh (UnionM a) -> FreshIdent -> UnionM a
forall a. Fresh a -> FreshIdent -> a
runFresh (Fresh (UnionM a) -> FreshIdent -> UnionM a)
-> (spec -> Fresh (UnionM a)) -> spec -> FreshIdent -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. spec -> Fresh (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). 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 = Fresh a -> FreshIdent -> a
forall a. Fresh a -> FreshIdent -> a
runFresh (Fresh a -> FreshIdent -> a)
-> (spec -> Fresh a) -> spec -> FreshIdent -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. spec -> Fresh a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). 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 = UnionM (U1 c) -> m (UnionM (U1 c))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (U1 c) -> m (UnionM (U1 c)))
-> UnionM (U1 c) -> m (UnionM (U1 c))
forall a b. (a -> b) -> a -> b
$ U1 c -> UnionM (U1 c)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle U1 c
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 = (c -> K1 i c c) -> UnionM c -> UnionM (K1 i c c)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> K1 i c c
forall k i c (p :: k). c -> K1 i c p
K1 (UnionM c -> UnionM (K1 i c c))
-> m (UnionM c) -> m (UnionM (K1 i c c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => () -> m (UnionM c)
fresh ()
instance (GenSymNoSpec a) => GenSymNoSpec (M1 i c a) where
freshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (UnionM (M1 i c a c))
freshNoSpec = (a c -> M1 i c a c) -> UnionM (a c) -> UnionM (M1 i c a c)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a c -> M1 i c a c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (UnionM (a c) -> UnionM (M1 i c a c))
-> m (UnionM (a c)) -> m (UnionM (M1 i c a c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (UnionM (a c))
forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
forall (m :: * -> *) c. 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 <- () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m SymBool
simpleFresh ()
UnionM (a c)
l :: UnionM (a c) <- m (UnionM (a c))
forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
forall (m :: * -> *) c. MonadFresh m => m (UnionM (a c))
freshNoSpec
UnionM (b c)
r :: UnionM (b c) <- m (UnionM (b c))
forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
forall (m :: * -> *) c. MonadFresh m => m (UnionM (b c))
freshNoSpec
UnionM ((:+:) a b c) -> m (UnionM ((:+:) a b c))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM ((:+:) a b c) -> m (UnionM ((:+:) a b c)))
-> UnionM ((:+:) a b c) -> m (UnionM ((:+:) a b c))
forall a b. (a -> b) -> a -> b
$ SymBool
-> UnionM ((:+:) a b c)
-> UnionM ((:+:) a b c)
-> UnionM ((:+:) a b c)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond ((a c -> (:+:) a b c) -> UnionM (a c) -> UnionM ((:+:) a b c)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a c -> (:+:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 UnionM (a c)
l) ((b c -> (:+:) a b c) -> UnionM (b c) -> UnionM ((:+:) a b c)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b c -> (:+:) a b c
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) <- m (UnionM (a c))
forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
forall (m :: * -> *) c. MonadFresh m => m (UnionM (a c))
freshNoSpec
UnionM (b c)
r :: UnionM (b c) <- m (UnionM (b c))
forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
forall (m :: * -> *) c. MonadFresh m => m (UnionM (b c))
freshNoSpec
UnionM ((:*:) a b c) -> m (UnionM ((:*:) a b c))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM ((:*:) a b c) -> m (UnionM ((:*:) a b c)))
-> UnionM ((:*:) a b c) -> m (UnionM ((:*:) a b c))
forall a b. (a -> b) -> a -> b
$ do
a c
l1 <- UnionM (a c)
l
b c
r1 <- UnionM (b c)
r
(:*:) a b c -> UnionM ((:*:) a b c)
forall a. a -> UnionM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:*:) a b c -> UnionM ((:*:) a b c))
-> (:*:) a b c -> UnionM ((:*:) a b c)
forall a b. (a -> b) -> a -> b
$ a c
l1 a c -> b c -> (:*:) a b c
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 ()
_ = UnionM a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM a -> UnionM a)
-> (UnionM (Rep a Any) -> UnionM a)
-> UnionM (Rep a Any)
-> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rep a Any -> a) -> UnionM (Rep a Any) -> UnionM a
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (UnionM (Rep a Any) -> UnionM a)
-> m (UnionM (Rep a Any)) -> m (UnionM a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (UnionM (Rep a Any))
forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
forall (m :: * -> *) c. MonadFresh m => m (UnionM (Rep 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 = U1 c -> m (U1 c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return U1 c
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 = c -> K1 i c c
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c c) -> m c -> m (K1 i c c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m c
simpleFresh ()
instance (GenSymSimpleNoSpec a) => GenSymSimpleNoSpec (M1 i c a) where
simpleFreshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (M1 i c a c)
simpleFreshNoSpec = a c -> M1 i c a c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a c -> M1 i c a c) -> m (a c) -> m (M1 i c a c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (a c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSimpleNoSpec a, MonadFresh m) =>
m (a c)
forall (m :: * -> *) c. 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 <- m (a c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSimpleNoSpec a, MonadFresh m) =>
m (a c)
forall (m :: * -> *) c. MonadFresh m => m (a c)
simpleFreshNoSpec
b c
r :: b c <- m (b c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSimpleNoSpec a, MonadFresh m) =>
m (a c)
forall (m :: * -> *) c. MonadFresh m => m (b c)
simpleFreshNoSpec
(:*:) a b c -> m ((:*:) a b c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:*:) a b c -> m ((:*:) a b c)) -> (:*:) a b c -> m ((:*:) a b c)
forall a b. (a -> b) -> a -> b
$ a c
l a c -> b c -> (:*:) a b c
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 ()
_ = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> m (Rep a Any) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Rep a Any)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSimpleNoSpec a, MonadFresh m) =>
m (a c)
forall (m :: * -> *) c. MonadFresh m => m (Rep 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
_ = U1 c -> m (U1 c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return U1 c
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) = c -> K1 i c c
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c c) -> m c -> m (K1 i c c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => c -> m c
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) = a c -> M1 i c a c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a c -> M1 i c a c) -> m (a c) -> m (M1 i c a c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a c -> m (a c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
forall (m :: * -> *) c. 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) = a c -> (:+:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (a c -> (:+:) a b c) -> m (a c) -> m ((:+:) a b c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a c -> m (a c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
forall (m :: * -> *) c. MonadFresh m => a c -> m (a c)
genSymSameShapeFresh a c
a
genSymSameShapeFresh (R1 b c
a) = b c -> (:+:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (b c -> (:+:) a b c) -> m (b c) -> m ((:+:) a b c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b c -> m (b c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
forall (m :: * -> *) c. MonadFresh m => b c -> m (b 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 <- a c -> m (a c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
forall (m :: * -> *) c. MonadFresh m => a c -> m (a c)
genSymSameShapeFresh a c
a
b c
r :: b c <- b c -> m (b c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
forall (m :: * -> *) c. MonadFresh m => b c -> m (b c)
genSymSameShapeFresh b c
b
(:*:) a b c -> m ((:*:) a b c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:*:) a b c -> m ((:*:) a b c)) -> (:*:) a b c -> m ((:*:) a b c)
forall a b. (a -> b) -> a -> b
$ a c
l a c -> b c -> (:*:) a b c
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 = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> m (Rep a Any) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rep a Any -> m (Rep a Any)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
forall (m :: * -> *) c. MonadFresh m => Rep a c -> m (Rep a c)
genSymSameShapeFresh (a -> Rep a Any
forall x. a -> Rep a x
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] = UnionM a -> m (UnionM a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM a -> m (UnionM a)) -> UnionM a -> m (UnionM a)
forall a b. (a -> b) -> a -> b
$ a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
x
chooseFresh (a
r : [a]
rs) = do
SymBool
b <- () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m SymBool
simpleFresh ()
UnionM a
res <- [a] -> m (UnionM a)
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh [a]
rs
UnionM a -> m (UnionM a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM a -> m (UnionM a)) -> UnionM a -> m (UnionM a)
forall a b. (a -> b) -> a -> b
$ SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
b (a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
r) UnionM a
res
chooseFresh [] = String -> m (UnionM a)
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 = Fresh (UnionM a) -> FreshIdent -> UnionM a
forall a. Fresh a -> FreshIdent -> a
runFresh (Fresh (UnionM a) -> FreshIdent -> UnionM a)
-> ([a] -> Fresh (UnionM a)) -> [a] -> FreshIdent -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Fresh (UnionM a)
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] = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
chooseSimpleFresh (a
r : [a]
rs) = do
SymBool
b :: bool <- () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m SymBool
simpleFresh ()
a
res <- [a] -> m a
forall a (m :: * -> *).
(SimpleMergeable a, MonadFresh m) =>
[a] -> m a
chooseSimpleFresh [a]
rs
a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ SymBool -> a -> a -> a
forall a. SimpleMergeable a => SymBool -> a -> a -> a
mrgIte SymBool
b a
r a
res
chooseSimpleFresh [] = String -> m a
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 = Fresh a -> FreshIdent -> a
forall a. Fresh a -> FreshIdent -> a
runFresh (Fresh a -> FreshIdent -> a)
-> ([a] -> Fresh a) -> [a] -> FreshIdent -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Fresh a
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] = UnionM a -> m (UnionM a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UnionM a
x
chooseUnionFresh (UnionM a
r : [UnionM a]
rs) = do
SymBool
b <- () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m SymBool
simpleFresh ()
UnionM a
res <- [UnionM a] -> m (UnionM a)
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh [UnionM a]
rs
UnionM a -> m (UnionM a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM a -> m (UnionM a)) -> UnionM a -> m (UnionM a)
forall a b. (a -> b) -> a -> b
$ SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
b UnionM a
r UnionM a
res
chooseUnionFresh [] = String -> m (UnionM a)
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 = Fresh (UnionM a) -> FreshIdent -> UnionM a
forall a. Fresh a -> FreshIdent -> a
runFresh (Fresh (UnionM a) -> FreshIdent -> UnionM a)
-> ([UnionM a] -> Fresh (UnionM a))
-> [UnionM a]
-> FreshIdent
-> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UnionM a] -> Fresh (UnionM a)
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 = () -> m (UnionM Bool)
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) = [v] -> m (UnionM v)
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh (Int -> v
forall a. Enum a => Int -> a
toEnum (Int -> v) -> [Int] -> [v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0 .. v -> Int
forall a. Enum a => a -> Int
fromEnum v
u Int -> Int -> Int
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) = [v] -> m (UnionM v)
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh (Int -> v
forall a. Enum a => Int -> a
toEnum (Int -> v) -> [Int] -> [v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [v -> Int
forall a. Enum a => a -> Int
fromEnum v
l .. v -> Int
forall a. Enum a => a -> Int
fromEnum v
u Int -> Int -> Int
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) = (UnionM (Either a b) -> UnionM (Either a b)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM (Either a b) -> UnionM (Either a b))
-> (UnionM a -> UnionM (Either a b))
-> UnionM a
-> UnionM (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Either a b) -> UnionM a -> UnionM (Either a b)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Either a b
forall a b. a -> Either a b
Left) (UnionM a -> UnionM (Either a b))
-> m (UnionM a) -> m (UnionM (Either a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
fresh (Right bspec
bspec) = (UnionM (Either a b) -> UnionM (Either a b)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM (Either a b) -> UnionM (Either a b))
-> (UnionM b -> UnionM (Either a b))
-> UnionM b
-> UnionM (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Either a b) -> UnionM b -> UnionM (Either a b)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Either a b
forall a b. b -> Either a b
Right) (UnionM b -> UnionM (Either a b))
-> m (UnionM b) -> m (UnionM (Either a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
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) = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> m a -> m (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
a
simpleFresh (Right bspec
b) = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> m b -> m (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
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 = () -> m (UnionM (Either a b))
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 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
UnionM b
r :: UnionM b <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
[UnionM (Either a b)] -> m (UnionM (Either a b))
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh [a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> UnionM a -> UnionM (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnionM a
l, b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> UnionM b -> UnionM (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnionM b
r]
instance
{-# OVERLAPPING #-}
(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 = UnionM (Maybe a) -> m (UnionM (Maybe a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (Maybe a) -> m (UnionM (Maybe a)))
-> UnionM (Maybe a) -> m (UnionM (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> UnionM (Maybe a)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Maybe a
forall a. Maybe a
Nothing
fresh (Just aspec
aspec) = (UnionM (Maybe a) -> UnionM (Maybe a)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM (Maybe a) -> UnionM (Maybe a))
-> (UnionM a -> UnionM (Maybe a)) -> UnionM a -> UnionM (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe a) -> UnionM a -> UnionM (Maybe a)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Maybe a
forall a. a -> Maybe a
Just) (UnionM a -> UnionM (Maybe a))
-> m (UnionM a) -> m (UnionM (Maybe a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> 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 = Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
simpleFresh (Just aspec
aspec) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> m a -> m (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
instance
{-# OVERLAPPABLE #-}
(GenSym aspec a, Mergeable a) =>
GenSym aspec (Maybe a)
where
fresh :: forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM (Maybe a))
fresh aspec
aspec = do
SymBool
cond <- () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m SymBool
simpleFresh ()
UnionM a
a :: UnionM a <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
UnionM (Maybe a) -> m (UnionM (Maybe a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (Maybe a) -> m (UnionM (Maybe a)))
-> UnionM (Maybe a) -> m (UnionM (Maybe a))
forall a b. (a -> b) -> a -> b
$ SymBool -> UnionM (Maybe a) -> UnionM (Maybe a) -> UnionM (Maybe a)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond (Maybe a -> UnionM (Maybe a)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Maybe a
forall a. Maybe a
Nothing) (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> UnionM a -> UnionM (Maybe a)
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 <- Integer -> m [UnionM a]
forall (m :: * -> *). MonadFresh m => Integer -> m [UnionM a]
gl Integer
v
let xs :: [[UnionM a]]
xs = [[UnionM a]] -> [[UnionM a]]
forall a. [a] -> [a]
reverse ([[UnionM a]] -> [[UnionM a]]) -> [[UnionM a]] -> [[UnionM a]]
forall a b. (a -> b) -> a -> b
$ (UnionM a -> [UnionM a] -> [UnionM a])
-> [UnionM a] -> [UnionM a] -> [[UnionM a]]
forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr (:) [] [UnionM a]
l
[UnionM [a]] -> m (UnionM [a])
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh ([UnionM [a]] -> m (UnionM [a])) -> [UnionM [a]] -> m (UnionM [a])
forall a b. (a -> b) -> a -> b
$ UnionM [a] -> UnionM [a]
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM [a] -> UnionM [a])
-> ([UnionM a] -> UnionM [a]) -> [UnionM a] -> UnionM [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UnionM a] -> UnionM [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([UnionM a] -> UnionM [a]) -> [[UnionM a]] -> [UnionM [a]]
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 = [UnionM a] -> m [UnionM a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do
UnionM a
l <- () -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => () -> m (UnionM a)
fresh ()
[UnionM a]
r <- Integer -> m [UnionM a]
forall (m :: * -> *). MonadFresh m => Integer -> m [UnionM a]
gl (Integer
v1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
[UnionM a] -> m [UnionM a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UnionM a] -> m [UnionM a]) -> [UnionM a] -> m [UnionM a]
forall a b. (a -> b) -> a -> b
$ UnionM a
l UnionM a -> [UnionM a] -> [UnionM a]
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
[ListSpec spec] -> ShowS
ListSpec spec -> String
(Int -> ListSpec spec -> ShowS)
-> (ListSpec spec -> String)
-> ([ListSpec spec] -> ShowS)
-> Show (ListSpec spec)
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
$cshowsPrec :: forall spec. Show spec => Int -> ListSpec spec -> ShowS
showsPrec :: Int -> ListSpec spec -> ShowS
$cshow :: forall spec. Show spec => ListSpec spec -> String
show :: ListSpec spec -> String
$cshowList :: forall spec. Show spec => [ListSpec spec] -> ShowS
showList :: [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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
maxLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
minLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
maxLen
then String -> m (UnionM [a])
forall a. HasCallStack => String -> a
error (String -> m (UnionM [a])) -> String -> m (UnionM [a])
forall a b. (a -> b) -> a -> b
$ String
"Bad lengths: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
minLen, Int
maxLen)
else do
[UnionM a]
l <- Int -> m [UnionM a]
forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl Int
maxLen
let xs :: [[UnionM a]]
xs = Int -> [[UnionM a]] -> [[UnionM a]]
forall a. Int -> [a] -> [a]
drop Int
minLen ([[UnionM a]] -> [[UnionM a]]) -> [[UnionM a]] -> [[UnionM a]]
forall a b. (a -> b) -> a -> b
$ [[UnionM a]] -> [[UnionM a]]
forall a. [a] -> [a]
reverse ([[UnionM a]] -> [[UnionM a]]) -> [[UnionM a]] -> [[UnionM a]]
forall a b. (a -> b) -> a -> b
$ (UnionM a -> [UnionM a] -> [UnionM a])
-> [UnionM a] -> [UnionM a] -> [[UnionM a]]
forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr (:) [] [UnionM a]
l
[UnionM [a]] -> m (UnionM [a])
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh ([UnionM [a]] -> m (UnionM [a])) -> [UnionM [a]] -> m (UnionM [a])
forall a b. (a -> b) -> a -> b
$ UnionM [a] -> UnionM [a]
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM [a] -> UnionM [a])
-> ([UnionM a] -> UnionM [a]) -> [UnionM a] -> UnionM [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UnionM a] -> UnionM [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([UnionM a] -> UnionM [a]) -> [[UnionM a]] -> [UnionM [a]]
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [UnionM a] -> m [UnionM a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do
UnionM a
l <- spec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
fresh spec
subSpec
[UnionM a]
r <- Int -> m [UnionM a]
forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl (Int
currLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
[UnionM a] -> m [UnionM a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UnionM a] -> m [UnionM a]) -> [UnionM a] -> m [UnionM a]
forall a b. (a -> b) -> a -> b
$ UnionM a
l UnionM a -> [UnionM a] -> [UnionM a]
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] <- (a -> m (UnionM a)) -> [a] -> m [UnionM a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => a -> m (UnionM a)
fresh [a]
l
UnionM [a] -> m (UnionM [a])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM [a] -> m (UnionM [a])) -> UnionM [a] -> m (UnionM [a])
forall a b. (a -> b) -> a -> b
$ UnionM [a] -> UnionM [a]
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM [a] -> UnionM [a]) -> UnionM [a] -> UnionM [a]
forall a b. (a -> b) -> a -> b
$ [UnionM a] -> UnionM [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [UnionM a]
r
instance
(GenSymSimple a a) =>
GenSymSimple [a] [a]
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => [a] -> m [a]
simpleFresh = [a] -> m [a]
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
[SimpleListSpec spec] -> ShowS
SimpleListSpec spec -> String
(Int -> SimpleListSpec spec -> ShowS)
-> (SimpleListSpec spec -> String)
-> ([SimpleListSpec spec] -> ShowS)
-> Show (SimpleListSpec spec)
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
$cshowsPrec :: forall spec. Show spec => Int -> SimpleListSpec spec -> ShowS
showsPrec :: Int -> SimpleListSpec spec -> ShowS
$cshow :: forall spec. Show spec => SimpleListSpec spec -> String
show :: SimpleListSpec spec -> String
$cshowList :: forall spec. Show spec => [SimpleListSpec spec] -> ShowS
showList :: [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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
then String -> m (UnionM [a])
forall a. HasCallStack => String -> a
error (String -> m (UnionM [a])) -> String -> m (UnionM [a])
forall a b. (a -> b) -> a -> b
$ String
"Bad lengths: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
len
else do
UnionM [a] -> UnionM [a]
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM [a] -> UnionM [a])
-> ([UnionM a] -> UnionM [a]) -> [UnionM a] -> UnionM [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UnionM a] -> UnionM [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([UnionM a] -> UnionM [a]) -> m [UnionM a] -> m (UnionM [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m [UnionM a]
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [UnionM a] -> m [UnionM a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do
UnionM a
l <- spec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
fresh spec
subSpec
[UnionM a]
r <- Int -> m [UnionM a]
forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl (Int
currLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
[UnionM a] -> m [UnionM a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UnionM a] -> m [UnionM a]) -> [UnionM a] -> m [UnionM a]
forall a b. (a -> b) -> a -> b
$ UnionM a
l UnionM a -> [UnionM a] -> [UnionM a]
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
then String -> m [a]
forall a. HasCallStack => String -> a
error (String -> m [a]) -> String -> m [a]
forall a b. (a -> b) -> a -> b
$ String
"Bad lengths: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
len
else do
Int -> m [a]
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do
a
l <- spec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => spec -> m a
simpleFresh spec
subSpec
[a]
r <- Int -> m [a]
forall (m :: * -> *). MonadFresh m => Int -> m [a]
gl (Int
currLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
[a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> m [a]) -> [a] -> m [a]
forall a b. (a -> b) -> a -> b
$ a
l a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
r
instance GenSym () ()
instance GenSymSimple () () where
simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m ()
simpleFresh = () -> m ()
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 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
UnionM (a, b) -> m (UnionM (a, b))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b) -> m (UnionM (a, b)))
-> UnionM (a, b) -> m (UnionM (a, b))
forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
(a, b) -> UnionM (a, b)
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
(,)
(a -> b -> (a, b)) -> m a -> m (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
m (b -> (a, b)) -> m b -> m (a, b)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
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 = () -> m (UnionM (a, b))
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 = () -> m (a, b)
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 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
UnionM c
c1 <- cspec -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => cspec -> m (UnionM c)
fresh cspec
cspec
UnionM (a, b, c) -> m (UnionM (a, b, c))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b, c) -> m (UnionM (a, b, c)))
-> UnionM (a, b, c) -> m (UnionM (a, b, c))
forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
(a, b, c) -> UnionM (a, b, c)
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
(,,)
(a -> b -> c -> (a, b, c)) -> m a -> m (b -> c -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
m (b -> c -> (a, b, c)) -> m b -> m (c -> (a, b, c))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec
m (c -> (a, b, c)) -> m c -> m (a, b, c)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> cspec -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => cspec -> m c
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 = () -> m (UnionM (a, b, c))
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 = () -> m (a, b, c)
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 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
UnionM c
c1 <- cspec -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => cspec -> m (UnionM c)
fresh cspec
cspec
UnionM d
d1 <- dspec -> m (UnionM d)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => dspec -> m (UnionM d)
fresh dspec
dspec
UnionM (a, b, c, d) -> m (UnionM (a, b, c, d))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b, c, d) -> m (UnionM (a, b, c, d)))
-> UnionM (a, b, c, d) -> m (UnionM (a, b, c, d))
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
(a, b, c, d) -> UnionM (a, b, c, d)
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
(,,,)
(a -> b -> c -> d -> (a, b, c, d))
-> m a -> m (b -> c -> d -> (a, b, c, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
m (b -> c -> d -> (a, b, c, d))
-> m b -> m (c -> d -> (a, b, c, d))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec
m (c -> d -> (a, b, c, d)) -> m c -> m (d -> (a, b, c, d))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> cspec -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => cspec -> m c
simpleFresh cspec
cspec
m (d -> (a, b, c, d)) -> m d -> m (a, b, c, d)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> dspec -> m d
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => dspec -> m d
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 = () -> m (UnionM (a, b, c, d))
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 = () -> m (a, b, c, d)
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 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
UnionM c
c1 <- cspec -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => cspec -> m (UnionM c)
fresh cspec
cspec
UnionM d
d1 <- dspec -> m (UnionM d)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => dspec -> m (UnionM d)
fresh dspec
dspec
UnionM e
e1 <- espec -> m (UnionM e)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => espec -> m (UnionM e)
fresh espec
espec
UnionM (a, b, c, d, e) -> m (UnionM (a, b, c, d, e))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b, c, d, e) -> m (UnionM (a, b, c, d, e)))
-> UnionM (a, b, c, d, e) -> m (UnionM (a, b, c, d, e))
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
(a, b, c, d, e) -> UnionM (a, b, c, d, e)
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
(,,,,)
(a -> b -> c -> d -> e -> (a, b, c, d, e))
-> m a -> m (b -> c -> d -> e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
m (b -> c -> d -> e -> (a, b, c, d, e))
-> m b -> m (c -> d -> e -> (a, b, c, d, e))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec
m (c -> d -> e -> (a, b, c, d, e))
-> m c -> m (d -> e -> (a, b, c, d, e))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> cspec -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => cspec -> m c
simpleFresh cspec
cspec
m (d -> e -> (a, b, c, d, e)) -> m d -> m (e -> (a, b, c, d, e))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> dspec -> m d
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => dspec -> m d
simpleFresh dspec
dspec
m (e -> (a, b, c, d, e)) -> m e -> m (a, b, c, d, e)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> espec -> m e
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => espec -> m e
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 = () -> m (UnionM (a, b, c, d, e))
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 = () -> m (a, b, c, d, e)
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 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
UnionM c
c1 <- cspec -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => cspec -> m (UnionM c)
fresh cspec
cspec
UnionM d
d1 <- dspec -> m (UnionM d)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => dspec -> m (UnionM d)
fresh dspec
dspec
UnionM e
e1 <- espec -> m (UnionM e)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => espec -> m (UnionM e)
fresh espec
espec
UnionM f
f1 <- fspec -> m (UnionM f)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => fspec -> m (UnionM f)
fresh fspec
fspec
UnionM (a, b, c, d, e, f) -> m (UnionM (a, b, c, d, e, f))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b, c, d, e, f) -> m (UnionM (a, b, c, d, e, f)))
-> UnionM (a, b, c, d, e, f) -> m (UnionM (a, b, c, d, e, f))
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
(a, b, c, d, e, f) -> UnionM (a, b, c, d, e, f)
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
(,,,,,)
(a -> b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> m a -> m (b -> c -> d -> e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
m (b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> m b -> m (c -> d -> e -> f -> (a, b, c, d, e, f))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec
m (c -> d -> e -> f -> (a, b, c, d, e, f))
-> m c -> m (d -> e -> f -> (a, b, c, d, e, f))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> cspec -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => cspec -> m c
simpleFresh cspec
cspec
m (d -> e -> f -> (a, b, c, d, e, f))
-> m d -> m (e -> f -> (a, b, c, d, e, f))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> dspec -> m d
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => dspec -> m d
simpleFresh dspec
dspec
m (e -> f -> (a, b, c, d, e, f))
-> m e -> m (f -> (a, b, c, d, e, f))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> espec -> m e
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => espec -> m e
simpleFresh espec
espec
m (f -> (a, b, c, d, e, f)) -> m f -> m (a, b, c, d, e, f)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> fspec -> m f
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => fspec -> m f
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 = () -> m (UnionM (a, b, c, d, e, f))
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 = () -> m (a, b, c, d, e, f)
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 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
UnionM c
c1 <- cspec -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => cspec -> m (UnionM c)
fresh cspec
cspec
UnionM d
d1 <- dspec -> m (UnionM d)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => dspec -> m (UnionM d)
fresh dspec
dspec
UnionM e
e1 <- espec -> m (UnionM e)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => espec -> m (UnionM e)
fresh espec
espec
UnionM f
f1 <- fspec -> m (UnionM f)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => fspec -> m (UnionM f)
fresh fspec
fspec
UnionM g
g1 <- gspec -> m (UnionM g)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => gspec -> m (UnionM g)
fresh gspec
gspec
UnionM (a, b, c, d, e, f, g) -> m (UnionM (a, b, c, d, e, f, g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b, c, d, e, f, g) -> m (UnionM (a, b, c, d, e, f, g)))
-> UnionM (a, b, c, d, e, f, g) -> m (UnionM (a, b, c, d, e, f, g))
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
(a, b, c, d, e, f, g) -> UnionM (a, b, c, d, e, f, g)
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
(,,,,,,)
(a -> b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> m a -> m (b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
m (b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> m b -> m (c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec
m (c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> m c -> m (d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> cspec -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => cspec -> m c
simpleFresh cspec
cspec
m (d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> m d -> m (e -> f -> g -> (a, b, c, d, e, f, g))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> dspec -> m d
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => dspec -> m d
simpleFresh dspec
dspec
m (e -> f -> g -> (a, b, c, d, e, f, g))
-> m e -> m (f -> g -> (a, b, c, d, e, f, g))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> espec -> m e
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => espec -> m e
simpleFresh espec
espec
m (f -> g -> (a, b, c, d, e, f, g))
-> m f -> m (g -> (a, b, c, d, e, f, g))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> fspec -> m f
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => fspec -> m f
simpleFresh fspec
fspec
m (g -> (a, b, c, d, e, f, g)) -> m g -> m (a, b, c, d, e, f, g)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> gspec -> m g
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => gspec -> m g
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 = () -> m (UnionM (a, b, c, d, e, f, g))
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 = () -> m (a, b, c, d, e, f, g)
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 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
UnionM c
c1 <- cspec -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => cspec -> m (UnionM c)
fresh cspec
cspec
UnionM d
d1 <- dspec -> m (UnionM d)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => dspec -> m (UnionM d)
fresh dspec
dspec
UnionM e
e1 <- espec -> m (UnionM e)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => espec -> m (UnionM e)
fresh espec
espec
UnionM f
f1 <- fspec -> m (UnionM f)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => fspec -> m (UnionM f)
fresh fspec
fspec
UnionM g
g1 <- gspec -> m (UnionM g)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => gspec -> m (UnionM g)
fresh gspec
gspec
UnionM h
h1 <- hspec -> m (UnionM h)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => hspec -> m (UnionM h)
fresh hspec
hspec
UnionM (a, b, c, d, e, f, g, h)
-> m (UnionM (a, b, c, d, e, f, g, h))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b, c, d, e, f, g, h)
-> m (UnionM (a, b, c, d, e, f, g, h)))
-> UnionM (a, b, c, d, e, f, g, h)
-> m (UnionM (a, b, c, d, e, f, g, h))
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
(a, b, c, d, e, f, g, h) -> UnionM (a, b, c, d, e, f, g, h)
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
(,,,,,,,)
(a -> b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> m a
-> m (b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
m (b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> m b
-> m (c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec
m (c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> m c -> m (d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> cspec -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => cspec -> m c
simpleFresh cspec
cspec
m (d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> m d -> m (e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> dspec -> m d
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => dspec -> m d
simpleFresh dspec
dspec
m (e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> m e -> m (f -> g -> h -> (a, b, c, d, e, f, g, h))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> espec -> m e
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => espec -> m e
simpleFresh espec
espec
m (f -> g -> h -> (a, b, c, d, e, f, g, h))
-> m f -> m (g -> h -> (a, b, c, d, e, f, g, h))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> fspec -> m f
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => fspec -> m f
simpleFresh fspec
fspec
m (g -> h -> (a, b, c, d, e, f, g, h))
-> m g -> m (h -> (a, b, c, d, e, f, g, h))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> gspec -> m g
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => gspec -> m g
simpleFresh gspec
gspec
m (h -> (a, b, c, d, e, f, g, h))
-> m h -> m (a, b, c, d, e, f, g, h)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> hspec -> m h
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => hspec -> m h
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 = () -> m (UnionM (a, b, c, d, e, f, g, h))
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 = () -> m (a, b, c, d, e, f, g, h)
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 <- spec -> m (UnionM (m (Maybe a)))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *).
MonadFresh m =>
spec -> m (UnionM (m (Maybe a)))
fresh spec
v
UnionM (MaybeT m a) -> m (UnionM (MaybeT m a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (MaybeT m a) -> m (UnionM (MaybeT m a)))
-> UnionM (MaybeT m a) -> m (UnionM (MaybeT m a))
forall a b. (a -> b) -> a -> b
$ UnionM (MaybeT m a) -> UnionM (MaybeT m a)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM (MaybeT m a) -> UnionM (MaybeT m a))
-> (UnionM (m (Maybe a)) -> UnionM (MaybeT m a))
-> UnionM (m (Maybe a))
-> UnionM (MaybeT m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m (Maybe a) -> MaybeT m a)
-> UnionM (m (Maybe a)) -> UnionM (MaybeT m a)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (UnionM (m (Maybe a)) -> UnionM (MaybeT m a))
-> UnionM (m (Maybe a)) -> UnionM (MaybeT m a)
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 = m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe a) -> MaybeT m a) -> m (m (Maybe a)) -> m (MaybeT m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> spec -> m (m (Maybe a))
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => spec -> m (m (Maybe 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) = m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe a) -> MaybeT m a) -> m (m (Maybe a)) -> m (MaybeT m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe a) -> m (m (Maybe a))
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *).
MonadFresh m =>
m (Maybe a) -> m (m (Maybe 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 <- spec -> m (UnionM (m (Either a b)))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *).
MonadFresh m =>
spec -> m (UnionM (m (Either a b)))
fresh spec
v
UnionM (ExceptT a m b) -> m (UnionM (ExceptT a m b))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (ExceptT a m b) -> m (UnionM (ExceptT a m b)))
-> UnionM (ExceptT a m b) -> m (UnionM (ExceptT a m b))
forall a b. (a -> b) -> a -> b
$ UnionM (ExceptT a m b) -> UnionM (ExceptT a m b)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM (ExceptT a m b) -> UnionM (ExceptT a m b))
-> (UnionM (m (Either a b)) -> UnionM (ExceptT a m b))
-> UnionM (m (Either a b))
-> UnionM (ExceptT a m b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m (Either a b) -> ExceptT a m b)
-> UnionM (m (Either a b)) -> UnionM (ExceptT a m b)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m (Either a b) -> ExceptT a m b
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (UnionM (m (Either a b)) -> UnionM (ExceptT a m b))
-> UnionM (m (Either a b)) -> UnionM (ExceptT a m b)
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 = m (Either a b) -> ExceptT a m b
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (m (Either a b) -> ExceptT a m b)
-> m (m (Either a b)) -> m (ExceptT a m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> spec -> m (m (Either a b))
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => spec -> m (m (Either a b))
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) = m (Either e a) -> ExceptT e m a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (m (Either e a) -> ExceptT e m a)
-> m (m (Either e a)) -> m (ExceptT e m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Either e a) -> m (m (Either e a))
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *).
MonadFresh m =>
m (Either e a) -> m (m (Either e 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
instance (GenSym spec a, Mergeable a) => GenSym spec (UnionM a)
instance (GenSym spec a) => GenSymSimple spec (UnionM a) where
simpleFresh :: forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
simpleFresh spec
spec = do
UnionM a
res <- spec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
fresh spec
spec
if Bool -> Bool
not (UnionM a -> Bool
forall a. UnionM a -> Bool
isMerged UnionM a
res) then String -> m (UnionM a)
forall a. HasCallStack => String -> a
error String
"Not merged" else UnionM a -> m (UnionM a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UnionM a
res
instance
(GenSym a a, Mergeable a) =>
GenSym (UnionM a) a
where
fresh :: forall (m :: * -> *). MonadFresh m => UnionM a -> m (UnionM a)
fresh UnionM a
spec = Union a -> m (UnionM a)
forall {spec} {a} {m :: * -> *}.
(GenSym spec a, MonadFresh m) =>
Union spec -> m (UnionM a)
go (UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion (UnionM a -> Union a) -> UnionM a -> Union a
forall a b. (a -> b) -> a -> b
$ UnionM a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge UnionM a
spec)
where
go :: Union spec -> m (UnionM a)
go (UnionSingle spec
x) = spec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
fresh spec
x
go (UnionIf spec
_ Bool
_ SymBool
_ Union spec
t Union spec
f) = SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymBool -> UnionM a -> UnionM a -> UnionM a)
-> m SymBool -> m (UnionM a -> UnionM a -> UnionM a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m SymBool
simpleFresh () m (UnionM a -> UnionM a -> UnionM a)
-> m (UnionM a) -> m (UnionM a -> UnionM a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Union spec -> m (UnionM a)
go Union spec
t m (UnionM a -> UnionM a) -> m (UnionM a) -> m (UnionM a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Union spec -> m (UnionM a)
go Union spec
f