{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Internal.Core.Data.Class.GenSym
(
FreshIndex (..),
MonadFresh (..),
nextFreshIndex,
liftFresh,
FreshT (FreshT, runFreshTFromIndex),
Fresh,
runFreshT,
runFresh,
mrgRunFreshT,
freshString,
GenSym (..),
GenSymSimple (..),
genSym,
genSymSimple,
derivedNoSpecFresh,
derivedNoSpecSimpleFresh,
derivedSameShapeSimpleFresh,
chooseFresh,
chooseSimpleFresh,
chooseUnionFresh,
choose,
chooseSimple,
chooseUnion,
ListSpec (..),
SimpleListSpec (..),
EnumGenBound (..),
EnumGenUpperBound (..),
)
where
import Control.Monad.Except
( ExceptT (ExceptT),
MonadError (catchError, throwError),
)
import Control.Monad.Identity (Identity (runIdentity))
import Control.Monad.RWS.Class
( MonadRWS,
MonadReader (ask, local),
MonadState (get, put),
MonadWriter (listen, pass, writer),
asks,
gets,
)
import qualified Control.Monad.RWS.Lazy as RWSLazy
import qualified Control.Monad.RWS.Strict as RWSStrict
import Control.Monad.Reader (ReaderT (ReaderT))
import Control.Monad.Signatures (Catch)
import qualified Control.Monad.State.Lazy as StateLazy
import qualified Control.Monad.State.Strict as StateStrict
import Control.Monad.Trans.Class
( MonadTrans (lift),
)
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import Data.Bifunctor (Bifunctor (first))
import qualified Data.ByteString as B
import Data.Int (Int16, Int32, Int64, Int8)
import Data.String (IsString (fromString))
import qualified Data.Text as T
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeNats (KnownNat, type (<=))
import Generics.Deriving
( Generic (Rep, from, to),
K1 (K1),
M1 (M1),
U1 (U1),
type (:*:) ((:*:)),
type (:+:) (L1, R1),
)
import Grisette.Internal.Core.Control.Monad.UnionM (UnionM, isMerged, underlyingUnion)
import Grisette.Internal.Core.Data.Class.Mergeable
( Mergeable (rootStrategy),
Mergeable1 (liftRootStrategy),
Mergeable2 (liftRootStrategy2),
MergingStrategy (SimpleStrategy),
rootStrategy1,
wrapStrategy,
)
import Grisette.Internal.Core.Data.Class.SimpleMergeable
( SimpleMergeable (mrgIte),
SimpleMergeable1 (liftMrgIte),
UnionMergeable1 (mrgIfPropagatedStrategy, mrgIfWithStrategy),
mrgIf,
)
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (isym))
import Grisette.Internal.Core.Data.Class.TryMerge
( TryMerge (tryMergeWithStrategy),
mrgSingle,
tryMerge,
)
import Grisette.Internal.Core.Data.Symbol (Identifier)
import Grisette.Internal.Core.Data.Union (Union (UnionIf, UnionSingle))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.GeneralFun (type (-->))
import Grisette.Internal.SymPrim.Prim.Term
( LinkedRep,
SupportedPrim,
)
import Grisette.Internal.SymPrim.SymBV
( SymIntN,
SymWordN,
)
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>))
import Grisette.Internal.SymPrim.SymInteger (SymInteger)
import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))
import Grisette.Internal.SymPrim.TabularFun (type (=->))
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
class (Monad m) => MonadFresh m where
getFreshIndex :: m FreshIndex
setFreshIndex :: FreshIndex -> m ()
getIdentifier :: m Identifier
localIdentifier :: (Identifier -> Identifier) -> m a -> m a
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 Identifier -> FreshIndex -> Identity (a, FreshIndex)
f) = do
FreshIndex
index <- m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
Identifier
ident <- m Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
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
$ Identifier -> FreshIndex -> Identity (a, FreshIndex)
f Identifier
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
freshString :: (MonadFresh m, IsString s) => String -> m s
freshString :: forall (m :: * -> *) s. (MonadFresh m, IsString s) => String -> m s
freshString String
postfix = do
Identifier
ident <- m Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
FreshIndex Int
index <- m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
s -> m s
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (s -> m s) -> s -> m s
forall a b. (a -> b) -> a -> b
$
String -> s
forall a. IsString a => String -> a
fromString (String -> s) -> String -> s
forall a b. (a -> b) -> a -> b
$
Identifier -> String
forall a. Show a => a -> String
show Identifier
ident String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"@" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
index String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"[" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
postfix String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"]"
newtype FreshT m a = FreshT
{ forall (m :: * -> *) a.
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex :: Identifier -> FreshIndex -> m (a, FreshIndex)
}
instance
(Mergeable a, Mergeable1 m) =>
Mergeable (FreshT m a)
where
rootStrategy :: MergingStrategy (FreshT m a)
rootStrategy =
MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex))
-> ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshT m a -> Identifier -> 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 (Identifier -> FreshIndex -> m (a, FreshIndex))
forall a. MergingStrategy a -> MergingStrategy (Identifier -> 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))
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> Identifier -> 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 (Identifier -> FreshIndex -> m (a, FreshIndex))
-> ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshT m a -> Identifier -> 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 (Identifier -> FreshIndex -> m (a, FreshIndex))
forall a. MergingStrategy a -> MergingStrategy (Identifier -> a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (MergingStrategy (FreshIndex -> m (a, FreshIndex))
-> MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex)))
-> (MergingStrategy (a, FreshIndex)
-> MergingStrategy (FreshIndex -> m (a, FreshIndex)))
-> MergingStrategy (a, FreshIndex)
-> MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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))
-> MergingStrategy (FreshIndex -> m (a, FreshIndex)))
-> (MergingStrategy (a, FreshIndex)
-> MergingStrategy (m (a, FreshIndex)))
-> MergingStrategy (a, FreshIndex)
-> MergingStrategy (FreshIndex -> m (a, FreshIndex))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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, FreshIndex)
-> MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex)))
-> MergingStrategy (a, FreshIndex)
-> MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex))
forall a b. (a -> b) -> a -> b
$
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
)
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex
instance
(UnionMergeable1 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.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
instance
(UnionMergeable1 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.
UnionMergeable1 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 (TryMerge m) => TryMerge (FreshT m) where
tryMergeWithStrategy :: forall a. MergingStrategy a -> FreshT m a -> FreshT m a
tryMergeWithStrategy MergingStrategy a
s (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
f) =
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
index ->
MergingStrategy (a, FreshIndex)
-> m (a, FreshIndex) -> m (a, FreshIndex)
forall a. MergingStrategy a -> m a -> m a
forall (m :: * -> *) a.
TryMerge m =>
MergingStrategy a -> m a -> m a
tryMergeWithStrategy (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
$ Identifier -> FreshIndex -> m (a, FreshIndex)
f Identifier
ident FreshIndex
index
instance
(UnionMergeable1 m) =>
UnionMergeable1 (FreshT m)
where
mrgIfWithStrategy :: forall a.
MergingStrategy a
-> SymBool -> FreshT m a -> FreshT m a -> FreshT m a
mrgIfWithStrategy MergingStrategy a
s SymBool
cond (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
t) (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
f) =
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
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.
UnionMergeable1 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
(Identifier -> FreshIndex -> m (a, FreshIndex)
t Identifier
ident FreshIndex
index)
(Identifier -> FreshIndex -> m (a, FreshIndex)
f Identifier
ident FreshIndex
index)
mrgIfPropagatedStrategy :: forall a. SymBool -> FreshT m a -> FreshT m a -> FreshT m a
mrgIfPropagatedStrategy SymBool
cond (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
t) (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
f) =
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
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.
UnionMergeable1 u =>
SymBool -> u a -> u a -> u a
mrgIfPropagatedStrategy SymBool
cond (Identifier -> FreshIndex -> m (a, FreshIndex)
t Identifier
ident FreshIndex
index) (Identifier -> FreshIndex -> m (a, FreshIndex)
f Identifier
ident FreshIndex
index)
runFreshT :: (Monad m) => FreshT m a -> Identifier -> m a
runFreshT :: forall (m :: * -> *) a. Monad m => FreshT m a -> Identifier -> m a
runFreshT FreshT m a
m Identifier
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 -> Identifier -> FreshIndex -> m (a, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex FreshT m a
m Identifier
ident (Int -> FreshIndex
FreshIndex Int
0)
mrgRunFreshT ::
(Monad m, TryMerge m, Mergeable a) =>
FreshT m a ->
Identifier ->
m a
mrgRunFreshT :: forall (m :: * -> *) a.
(Monad m, TryMerge m, Mergeable a) =>
FreshT m a -> Identifier -> m a
mrgRunFreshT FreshT m a
m Identifier
ident = m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ FreshT m a -> Identifier -> m a
forall (m :: * -> *) a. Monad m => FreshT m a -> Identifier -> m a
runFreshT FreshT m a
m Identifier
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 Identifier -> FreshIndex -> f (a, FreshIndex)
s) = (Identifier -> FreshIndex -> f (b, FreshIndex)) -> FreshT f b
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> f (b, FreshIndex)) -> FreshT f b)
-> (Identifier -> FreshIndex -> f (b, FreshIndex)) -> FreshT f b
forall a b. (a -> b) -> a -> b
$ \Identifier
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
<$> Identifier -> FreshIndex -> f (a, FreshIndex)
s Identifier
ident FreshIndex
idx
instance (Applicative m, Monad m) => Applicative (FreshT m) where
pure :: forall a. a -> FreshT m a
pure a
a = (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
_ 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 Identifier -> FreshIndex -> m (a -> b, FreshIndex)
fs <*> :: forall a b. FreshT m (a -> b) -> FreshT m a -> FreshT m b
<*> FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
as = (Identifier -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b)
-> (Identifier -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
idx -> do
(a -> b
f, FreshIndex
idx') <- Identifier -> FreshIndex -> m (a -> b, FreshIndex)
fs Identifier
ident FreshIndex
idx
(a
a, FreshIndex
idx'') <- Identifier -> FreshIndex -> m (a, FreshIndex)
as Identifier
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 Identifier -> FreshIndex -> m (a, FreshIndex)
s) >>= :: forall a b. FreshT m a -> (a -> FreshT m b) -> FreshT m b
>>= a -> FreshT m b
f = (Identifier -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b)
-> (Identifier -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
idx -> do
(a
a, FreshIndex
idx') <- Identifier -> FreshIndex -> m (a, FreshIndex)
s Identifier
ident FreshIndex
idx
FreshT m b -> Identifier -> FreshIndex -> m (b, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex (a -> FreshT m b
f a
a) Identifier
ident FreshIndex
idx'
instance MonadTrans FreshT where
lift :: forall (m :: * -> *) a. Monad m => m a -> FreshT m a
lift m a
x = (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
_ 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 Identifier -> FreshIndex -> m (a, FreshIndex)
m) e -> FreshT m a
h =
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
index -> Identifier -> FreshIndex -> m (a, FreshIndex)
m Identifier
ident FreshIndex
index Catch e m (a, FreshIndex)
`catchE` \e
e -> FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex (e -> FreshT m a
h e
e) Identifier
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 = (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
_ 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 Identifier -> FreshIndex -> m (a, FreshIndex)
r) = (Identifier -> FreshIndex -> m ((a, w), FreshIndex))
-> FreshT m (a, w)
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m ((a, w), FreshIndex))
-> FreshT m (a, w))
-> (Identifier -> FreshIndex -> m ((a, w), FreshIndex))
-> FreshT m (a, w)
forall a b. (a -> b) -> a -> b
$ \Identifier
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 (Identifier -> FreshIndex -> m (a, FreshIndex)
r Identifier
ident FreshIndex
index)
pass :: forall a. FreshT m (a, w -> w) -> FreshT m a
pass (FreshT Identifier -> FreshIndex -> m ((a, w -> w), FreshIndex)
r) = (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
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
<$> Identifier -> FreshIndex -> m ((a, w -> w), FreshIndex)
r Identifier
ident FreshIndex
index
instance (MonadState s m) => MonadState s (FreshT m) where
get :: FreshT m s
get = (Identifier -> FreshIndex -> m (s, FreshIndex)) -> FreshT m s
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (s, FreshIndex)) -> FreshT m s)
-> (Identifier -> FreshIndex -> m (s, FreshIndex)) -> FreshT m s
forall a b. (a -> b) -> a -> b
$ \Identifier
_ 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 = (Identifier -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ()
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ())
-> (Identifier -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ()
forall a b. (a -> b) -> a -> b
$ \Identifier
_ 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 Identifier -> FreshIndex -> m (a, FreshIndex)
r) = (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
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 (Identifier -> FreshIndex -> m (a, FreshIndex)
r Identifier
ident FreshIndex
index)
ask :: FreshT m r
ask = (Identifier -> FreshIndex -> m (r, FreshIndex)) -> FreshT m r
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (r, FreshIndex)) -> FreshT m r)
-> (Identifier -> FreshIndex -> m (r, FreshIndex)) -> FreshT m r
forall a b. (a -> b) -> a -> b
$ \Identifier
_ 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
getIdentifier :: ExceptT e m Identifier
getIdentifier = m Identifier -> ExceptT e m Identifier
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 Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
localIdentifier :: forall a.
(Identifier -> Identifier) -> ExceptT e m a -> ExceptT e m a
localIdentifier Identifier -> Identifier
f (ExceptT m (Either e a)
m) = 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 (Either e a) -> ExceptT e m a
forall a b. (a -> b) -> a -> b
$ (Identifier -> Identifier) -> m (Either e a) -> m (Either e a)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f m (Either e a)
m
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
getIdentifier :: WriterT w m Identifier
getIdentifier = m Identifier -> WriterT w m Identifier
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 Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
localIdentifier :: forall a.
(Identifier -> Identifier) -> WriterT w m a -> WriterT w m a
localIdentifier Identifier -> Identifier
f (WriterLazy.WriterT m (a, w)
m) =
m (a, w) -> WriterT w m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT (m (a, w) -> WriterT w m a) -> m (a, w) -> WriterT w m a
forall a b. (a -> b) -> a -> b
$ (Identifier -> Identifier) -> m (a, w) -> m (a, w)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f m (a, w)
m
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
getIdentifier :: WriterT w m Identifier
getIdentifier = m Identifier -> WriterT w m Identifier
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 Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
localIdentifier :: forall a.
(Identifier -> Identifier) -> WriterT w m a -> WriterT w m a
localIdentifier Identifier -> Identifier
f (WriterStrict.WriterT m (a, w)
m) =
m (a, w) -> WriterT w m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT (m (a, w) -> WriterT w m a) -> m (a, w) -> WriterT w m a
forall a b. (a -> b) -> a -> b
$ (Identifier -> Identifier) -> m (a, w) -> m (a, w)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f m (a, w)
m
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
getIdentifier :: StateT s m Identifier
getIdentifier = m Identifier -> StateT s m Identifier
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 Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
localIdentifier :: forall a.
(Identifier -> Identifier) -> StateT s m a -> StateT s m a
localIdentifier Identifier -> Identifier
f (StateLazy.StateT s -> m (a, s)
m) =
(s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateLazy.StateT ((s -> m (a, s)) -> StateT s m a)
-> (s -> m (a, s)) -> StateT s m a
forall a b. (a -> b) -> a -> b
$ \s
s -> (Identifier -> Identifier) -> m (a, s) -> m (a, s)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f (s -> m (a, s)
m s
s)
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
getIdentifier :: StateT s m Identifier
getIdentifier = m Identifier -> StateT s m Identifier
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 Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
localIdentifier :: forall a.
(Identifier -> Identifier) -> StateT s m a -> StateT s m a
localIdentifier Identifier -> Identifier
f (StateStrict.StateT s -> m (a, s)
m) =
(s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateStrict.StateT ((s -> m (a, s)) -> StateT s m a)
-> (s -> m (a, s)) -> StateT s m a
forall a b. (a -> b) -> a -> b
$ \s
s -> (Identifier -> Identifier) -> m (a, s) -> m (a, s)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f (s -> m (a, s)
m s
s)
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
getIdentifier :: ReaderT r m Identifier
getIdentifier = m Identifier -> ReaderT r m Identifier
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 Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
localIdentifier :: forall a.
(Identifier -> Identifier) -> ReaderT r m a -> ReaderT r m a
localIdentifier Identifier -> Identifier
f (ReaderT r -> m a
m) = (r -> m a) -> ReaderT r m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((r -> m a) -> ReaderT r m a) -> (r -> m a) -> ReaderT r m a
forall a b. (a -> b) -> a -> b
$ (Identifier -> Identifier) -> m a -> m a
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f (m a -> m a) -> (r -> m a) -> r -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> m a
m
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
getIdentifier :: RWST r w s m Identifier
getIdentifier = m Identifier -> RWST r w s m Identifier
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 Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
localIdentifier :: forall a.
(Identifier -> Identifier) -> RWST r w s m a -> RWST r w s m a
localIdentifier Identifier -> Identifier
f (RWSLazy.RWST r -> s -> m (a, s, w)
m) =
(r -> s -> m (a, s, w)) -> RWST r w s m a
forall r w s (m :: * -> *) a.
(r -> s -> m (a, s, w)) -> RWST r w s m a
RWSLazy.RWST ((r -> s -> m (a, s, w)) -> RWST r w s m a)
-> (r -> s -> m (a, s, w)) -> RWST r w s m a
forall a b. (a -> b) -> a -> b
$ \r
r s
s -> (Identifier -> Identifier) -> m (a, s, w) -> m (a, s, w)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f (r -> s -> m (a, s, w)
m r
r s
s)
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
getIdentifier :: RWST r w s m Identifier
getIdentifier = m Identifier -> RWST r w s m Identifier
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 Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
localIdentifier :: forall a.
(Identifier -> Identifier) -> RWST r w s m a -> RWST r w s m a
localIdentifier Identifier -> Identifier
f (RWSStrict.RWST r -> s -> m (a, s, w)
m) =
(r -> s -> m (a, s, w)) -> RWST r w s m a
forall r w s (m :: * -> *) a.
(r -> s -> m (a, s, w)) -> RWST r w s m a
RWSStrict.RWST ((r -> s -> m (a, s, w)) -> RWST r w s m a)
-> (r -> s -> m (a, s, w)) -> RWST r w s m a
forall a b. (a -> b) -> a -> b
$ \r
r s
s -> (Identifier -> Identifier) -> m (a, s, w) -> m (a, s, w)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f (r -> s -> m (a, s, w)
m r
r s
s)
type Fresh = FreshT Identity
runFresh :: Fresh a -> Identifier -> a
runFresh :: forall a. Fresh a -> Identifier -> a
runFresh Fresh a
m Identifier
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 -> Identifier -> Identity a
forall (m :: * -> *) a. Monad m => FreshT m a -> Identifier -> m a
runFreshT Fresh a
m Identifier
ident
instance (Monad m) => MonadFresh (FreshT m) where
getFreshIndex :: FreshT m FreshIndex
getFreshIndex = (Identifier -> FreshIndex -> m (FreshIndex, FreshIndex))
-> FreshT m FreshIndex
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (FreshIndex, FreshIndex))
-> FreshT m FreshIndex)
-> (Identifier -> FreshIndex -> m (FreshIndex, FreshIndex))
-> FreshT m FreshIndex
forall a b. (a -> b) -> a -> b
$ \Identifier
_ 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 = (Identifier -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ()
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ())
-> (Identifier -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ()
forall a b. (a -> b) -> a -> b
$ \Identifier
_ FreshIndex
_ -> ((), FreshIndex) -> m ((), FreshIndex)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((), FreshIndex
newIdx)
getIdentifier :: FreshT m Identifier
getIdentifier = (Identifier -> FreshIndex -> m (Identifier, FreshIndex))
-> FreshT m Identifier
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (Identifier, FreshIndex))
-> FreshT m Identifier)
-> (Identifier -> FreshIndex -> m (Identifier, FreshIndex))
-> FreshT m Identifier
forall a b. (a -> b) -> a -> b
$ ((Identifier, FreshIndex) -> m (Identifier, FreshIndex))
-> Identifier -> FreshIndex -> m (Identifier, FreshIndex)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Identifier, FreshIndex) -> m (Identifier, FreshIndex)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
localIdentifier :: forall a. (Identifier -> Identifier) -> FreshT m a -> FreshT m a
localIdentifier Identifier -> Identifier
f (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
m) = (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
idx -> do
let newIdent :: Identifier
newIdent = Identifier -> Identifier
f Identifier
ident
(a
r, FreshIndex
_) <- Identifier -> FreshIndex -> m (a, FreshIndex)
m Identifier
newIdent FreshIndex
0
(a, FreshIndex) -> m (a, FreshIndex)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
r, FreshIndex
idx)
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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 -> Identifier -> UnionM a
genSym :: forall spec a. GenSym spec a => spec -> Identifier -> UnionM a
genSym = Fresh (UnionM a) -> Identifier -> UnionM a
forall a. Fresh a -> Identifier -> a
runFresh (Fresh (UnionM a) -> Identifier -> UnionM a)
-> (spec -> Fresh (UnionM a)) -> spec -> Identifier -> 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 -> Identifier -> a
genSymSimple :: forall spec a. GenSymSimple spec a => spec -> Identifier -> a
genSymSimple = Fresh a -> Identifier -> a
forall a. Fresh a -> Identifier -> a
runFresh (Fresh a -> Identifier -> a)
-> (spec -> Fresh a) -> spec -> Identifier -> 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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.
(UnionMergeable1 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 (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
b (a -> UnionM a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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] ->
Identifier ->
UnionM a
choose :: forall a. Mergeable a => [a] -> Identifier -> UnionM a
choose = Fresh (UnionM a) -> Identifier -> UnionM a
forall a. Fresh a -> Identifier -> a
runFresh (Fresh (UnionM a) -> Identifier -> UnionM a)
-> ([a] -> Fresh (UnionM a)) -> [a] -> Identifier -> 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] ->
Identifier ->
a
chooseSimple :: forall a. SimpleMergeable a => [a] -> Identifier -> a
chooseSimple = Fresh a -> Identifier -> a
forall a. Fresh a -> Identifier -> a
runFresh (Fresh a -> Identifier -> a)
-> ([a] -> Fresh a) -> [a] -> Identifier -> 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.
(UnionMergeable1 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] ->
Identifier ->
UnionM a
chooseUnion :: forall a. Mergeable a => [UnionM a] -> Identifier -> UnionM a
chooseUnion = Fresh (UnionM a) -> Identifier -> UnionM a
forall a. Fresh a -> Identifier -> a
runFresh (Fresh (UnionM a) -> Identifier -> UnionM a)
-> ([UnionM a] -> Fresh (UnionM a))
-> [UnionM a]
-> Identifier
-> 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(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(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 (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (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 (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Maybe a
forall a. Maybe a
Nothing
fresh (Just aspec
aspec) = (UnionM (Maybe a) -> UnionM (Maybe a)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (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.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond (Maybe a -> UnionM (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (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 (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (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 (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (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 (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (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 (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (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 <- getIdentifier; \
FreshIndex index <- nextFreshIndex; \
return $ isym ident index
#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 <- getIdentifier; \
FreshIndex index <- nextFreshIndex; \
return $ isym ident index
#define GENSYM_FUN(cop, op) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
GenSym (op sa sb) (op sa sb)
#define GENSYM_SIMPLE_FUN(cop, op) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
GenSymSimple (op sa sb) (op sa sb) where \
simpleFresh _ = simpleFresh ()
#define GENSYM_UNIT_FUN(cop, op) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
GenSym () (op sa sb) where \
fresh _ = mrgSingle <$> simpleFresh ()
#define GENSYM_UNIT_SIMPLE_FUN(cop, op) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
GenSymSimple () (op sa sb) where \
simpleFresh _ = do; \
ident <- getIdentifier; \
FreshIndex index <- nextFreshIndex; \
return $ isym ident index
#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_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 (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge 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.
(UnionMergeable1 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