{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Experimental.GenSymConstrained
(
GenSymConstrained (..),
GenSymSimpleConstrained (..),
genSymConstrained,
genSymSimpleConstrained,
derivedFreshConstrainedNoSpec,
derivedSimpleFreshConstrainedNoSpec,
derivedSimpleFreshConstrainedSameShape,
SOrdUpperBound (..),
SOrdLowerBound (..),
SOrdBound (..),
)
where
import Control.Monad.Except (ExceptT (ExceptT), MonadError (throwError))
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import GHC.Generics
( Generic (Rep, from, to),
K1 (K1),
M1 (M1),
U1 (U1),
type (:*:) ((:*:)),
type (:+:) (L1, R1),
)
import Grisette.Core.Control.Monad.UnionM
( UnionM,
liftToMonadUnion,
)
import Grisette.Core.Data.Class.Bool (LogicalOp ((||~)))
import Grisette.Core.Data.Class.GenSym
( FreshIdent,
GenSym (fresh),
GenSymSimple (simpleFresh),
ListSpec (ListSpec),
MonadFresh,
SimpleListSpec (SimpleListSpec),
chooseFresh,
chooseUnionFresh,
runFreshT,
)
import Grisette.Core.Data.Class.Mergeable (Mergeable, Mergeable1)
import Grisette.Core.Data.Class.SOrd (SOrd ((<~), (>=~)))
import Grisette.Core.Data.Class.SimpleMergeable
( UnionLike,
merge,
mrgIf,
mrgSingle,
)
class (Mergeable a) => GenSymConstrained spec a where
freshConstrained ::
(MonadFresh m, MonadError e m, UnionLike m) =>
e ->
spec ->
m (UnionM a)
default freshConstrained ::
(GenSymSimpleConstrained spec a) =>
( MonadFresh m,
MonadError e m,
UnionLike m
) =>
e ->
spec ->
m (UnionM a)
freshConstrained e
e spec
spec = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e spec
spec
genSymConstrained :: forall spec a e. (GenSymConstrained spec a, Mergeable e) => e -> spec -> FreshIdent -> ExceptT e UnionM (UnionM a)
genSymConstrained :: forall spec a e.
(GenSymConstrained spec a, Mergeable e) =>
e -> spec -> FreshIdent -> ExceptT e UnionM (UnionM a)
genSymConstrained e
e spec
spec = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => FreshT m a -> FreshIdent -> m a
runFreshT (forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e spec
spec)
class (Mergeable a) => GenSymSimpleConstrained spec a where
simpleFreshConstrained ::
(MonadFresh m, MonadError e m, UnionLike m) =>
e ->
spec ->
m a
genSymSimpleConstrained :: forall spec a e. (GenSymSimpleConstrained spec a, Mergeable e) => e -> spec -> FreshIdent -> ExceptT e UnionM a
genSymSimpleConstrained :: forall spec a e.
(GenSymSimpleConstrained spec a, Mergeable e) =>
e -> spec -> FreshIdent -> ExceptT e UnionM a
genSymSimpleConstrained e
e spec
spec = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => FreshT m a -> FreshIdent -> m a
runFreshT (forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e spec
spec)
instance {-# OVERLAPPABLE #-} (Mergeable a, GenSym spec a) => GenSymConstrained spec a where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
_ = forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh
instance {-# OVERLAPPABLE #-} (Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained spec a where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
_ = forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh
data SOrdUpperBound a spec = SOrdUpperBound a spec
instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdUpperBound a spec) a where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdUpperBound a spec -> m (UnionM a)
freshConstrained e
e (SOrdUpperBound a
u spec
spec) = do
UnionM a
s <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
spec
a
v <- forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
UnionM a -> u a
liftToMonadUnion UnionM a
s
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
v forall a. SOrd a => a -> a -> SymBool
>=~ a
u) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (forall (m :: * -> *) a. Monad m => a -> m a
return ())
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v
instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdUpperBound a spec) a where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdUpperBound a spec -> m a
simpleFreshConstrained e
e (SOrdUpperBound a
u spec
spec) = do
a
s <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh spec
spec
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
s forall a. SOrd a => a -> a -> SymBool
>=~ a
u) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (forall (m :: * -> *) a. Monad m => a -> m a
return ())
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
s
data SOrdLowerBound a spec = SOrdLowerBound a spec
instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdLowerBound a spec) a where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdLowerBound a spec -> m (UnionM a)
freshConstrained e
e (SOrdLowerBound a
l spec
spec) = do
UnionM a
s <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
spec
a
v <- forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
UnionM a -> u a
liftToMonadUnion UnionM a
s
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
v forall a. SOrd a => a -> a -> SymBool
<~ a
l) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (forall (m :: * -> *) a. Monad m => a -> m a
return ())
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v
instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdLowerBound a spec) a where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdLowerBound a spec -> m a
simpleFreshConstrained e
e (SOrdLowerBound a
l spec
spec) = do
a
s <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh spec
spec
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
s forall a. SOrd a => a -> a -> SymBool
<~ a
l) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (forall (m :: * -> *) a. Monad m => a -> m a
return ())
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
s
data SOrdBound a spec = SOrdBound a a spec
instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdBound a spec) a where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdBound a spec -> m (UnionM a)
freshConstrained e
e (SOrdBound a
l a
u spec
spec) = do
UnionM a
s <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
spec
a
v <- forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
UnionM a -> u a
liftToMonadUnion UnionM a
s
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
v forall a. SOrd a => a -> a -> SymBool
<~ a
l forall b. LogicalOp b => b -> b -> b
||~ a
v forall a. SOrd a => a -> a -> SymBool
>=~ a
u) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (forall (m :: * -> *) a. Monad m => a -> m a
return ())
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v
instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdBound a spec) a where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdBound a spec -> m a
simpleFreshConstrained e
e (SOrdBound a
l a
u spec
spec) = do
a
s <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh spec
spec
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
s forall a. SOrd a => a -> a -> SymBool
<~ a
l forall b. LogicalOp b => b -> b -> b
||~ a
s forall a. SOrd a => a -> a -> SymBool
>=~ a
u) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (forall (m :: * -> *) a. Monad m => a -> m a
return ())
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
s
instance GenSymConstrained (SOrdBound Integer ()) Integer where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdBound Integer () -> m (UnionM Integer)
freshConstrained e
_ (SOrdBound Integer
l Integer
r ()
_) = forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh [Integer
l .. Integer
r forall a. Num a => a -> a -> a
- Integer
1]
instance
( GenSymConstrained aspec a,
Mergeable a,
GenSymConstrained bspec b,
Mergeable b
) =>
GenSymConstrained (Either aspec bspec) (Either a b)
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Either aspec bspec -> m (UnionM (Either a b))
freshConstrained e
e (Left aspec
aspec) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e aspec
aspec
freshConstrained e
e (Right bspec
bspec) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e bspec
bspec
instance
( GenSymSimpleConstrained a a,
GenSymSimpleConstrained b b
) =>
GenSymSimpleConstrained (Either a b) (Either a b)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Either a b -> m (Either a b)
simpleFreshConstrained = forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedSameShape (Rep a), Mergeable a,
MonadFresh m, MonadError e m, UnionLike m) =>
e -> a -> m a
derivedSimpleFreshConstrainedSameShape
instance
(GenSymConstrained () a, Mergeable a, GenSymConstrained () b, Mergeable b) =>
GenSymConstrained () (Either a b)
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> () -> m (UnionM (Either a b))
freshConstrained = forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a,
MonadFresh m, MonadError e m, UnionLike m) =>
e -> () -> m (UnionM a)
derivedFreshConstrainedNoSpec
instance
(GenSymConstrained aspec a, Mergeable a) =>
GenSymConstrained (Maybe aspec) (Maybe a)
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Maybe aspec -> m (UnionM (Maybe a))
freshConstrained e
_ Maybe aspec
Nothing = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a. Maybe a
Nothing
freshConstrained e
e (Just aspec
aspec) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e aspec
aspec
instance
(GenSymSimpleConstrained aspec a) =>
GenSymSimpleConstrained (Maybe aspec) (Maybe a)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Maybe aspec -> m (Maybe a)
simpleFreshConstrained e
_ Maybe aspec
Nothing = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a. Maybe a
Nothing
simpleFreshConstrained e
e (Just aspec
aspec) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
instance (GenSymConstrained aspec a, Mergeable a) => GenSymConstrained aspec (Maybe a) where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> aspec -> m (UnionM (Maybe a))
freshConstrained e
e aspec
aspec = do
UnionM a
a :: UnionM a <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e aspec
aspec
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh [forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing, forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnionM a
a]
instance
(GenSymConstrained () a, Mergeable a) =>
GenSymConstrained Integer [a]
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Integer -> m (UnionM [a])
freshConstrained e
e Integer
v = do
[UnionM a]
l <- forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Integer -> m [UnionM a]
gl e
e Integer
v
let xs :: [[UnionM a]]
xs = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr (:) [] [UnionM a]
l
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[UnionM a]]
xs
where
gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Integer -> m [UnionM a]
gl :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Integer -> m [UnionM a]
gl e
e1 Integer
v1
| Integer
v1 forall a. Ord a => a -> a -> Bool
<= Integer
0 = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle []
| Bool
otherwise = do
UnionM a
l <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e1 ()
[UnionM a]
r <- forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Integer -> m [UnionM a]
gl e
e1 (Integer
v1 forall a. Num a => a -> a -> a
- Integer
1)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ UnionM a
l forall a. a -> [a] -> [a]
: [UnionM a]
r
instance
(GenSymConstrained spec a, Mergeable a) =>
GenSymConstrained (ListSpec spec) [a]
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> ListSpec spec -> m (UnionM [a])
freshConstrained e
e (ListSpec Int
minLen Int
maxLen spec
subSpec) =
if Int
minLen forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
maxLen forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
minLen forall a. Ord a => a -> a -> Bool
>= Int
maxLen
then forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Bad lengths: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Int
minLen, Int
maxLen)
else do
[UnionM a]
l <- forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [UnionM a]
gl e
e Int
maxLen
let xs :: [[UnionM a]]
xs = forall a. Int -> [a] -> [a]
drop Int
minLen forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr (:) [] [UnionM a]
l
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[UnionM a]]
xs
where
gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Int -> m [UnionM a]
gl :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [UnionM a]
gl e
e1 Int
currLen
| Int
currLen forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do
UnionM a
l <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e1 spec
subSpec
[UnionM a]
r <- forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [UnionM a]
gl e
e1 (Int
currLen forall a. Num a => a -> a -> a
- Int
1)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UnionM a
l forall a. a -> [a] -> [a]
: [UnionM a]
r
instance
(GenSymConstrained a a, Mergeable a) =>
GenSymConstrained [a] [a]
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> [a] -> m (UnionM [a])
freshConstrained e
e [a]
l = do
[UnionM a]
r :: [UnionM a] <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e) [a]
l
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [UnionM a]
r
instance
(GenSymSimpleConstrained a a) =>
GenSymSimpleConstrained [a] [a]
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> [a] -> m [a]
simpleFreshConstrained = forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedSameShape (Rep a), Mergeable a,
MonadFresh m, MonadError e m, UnionLike m) =>
e -> a -> m a
derivedSimpleFreshConstrainedSameShape
instance
(GenSymConstrained spec a, Mergeable a) =>
GenSymConstrained (SimpleListSpec spec) [a]
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SimpleListSpec spec -> m (UnionM [a])
freshConstrained e
e (SimpleListSpec Int
len spec
subSpec) =
if Int
len forall a. Ord a => a -> a -> Bool
< Int
0
then forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Bad lengths: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
len
else do
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [UnionM a]
gl e
e Int
len
where
gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Int -> m [UnionM a]
gl :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [UnionM a]
gl e
e1 Int
currLen
| Int
currLen forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle []
| Bool
otherwise = do
UnionM a
l <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e1 spec
subSpec
[UnionM a]
r <- forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [UnionM a]
gl e
e1 (Int
currLen forall a. Num a => a -> a -> a
- Int
1)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ UnionM a
l forall a. a -> [a] -> [a]
: [UnionM a]
r
instance
(GenSymSimpleConstrained spec a) =>
GenSymSimpleConstrained (SimpleListSpec spec) [a]
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SimpleListSpec spec -> m [a]
simpleFreshConstrained e
e (SimpleListSpec Int
len spec
subSpec) =
if Int
len forall a. Ord a => a -> a -> Bool
< Int
0
then forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Bad lengths: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
len
else do
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [a]
gl e
e Int
len
where
gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Int -> m [a]
gl :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [a]
gl e
e1 Int
currLen
| Int
currLen forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle []
| Bool
otherwise = do
a
l <- forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e1 spec
subSpec
[a]
r <- forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [a]
gl e
e1 (Int
currLen forall a. Num a => a -> a -> a
- Int
1)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
l forall a. a -> [a] -> [a]
: [a]
r
instance
( GenSymConstrained aspec a,
Mergeable a,
GenSymConstrained bspec b,
Mergeable b
) =>
GenSymConstrained (aspec, bspec) (a, b)
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec) -> m (UnionM (a, b))
freshConstrained e
err (aspec
aspec, bspec
bspec) = do
UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx)
instance
( GenSymSimpleConstrained aspec a,
GenSymSimpleConstrained bspec b
) =>
GenSymSimpleConstrained (aspec, bspec) (a, b)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec) -> m (a, b)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec) = do
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
(,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
instance
( GenSymConstrained aspec a,
Mergeable a,
GenSymConstrained bspec b,
Mergeable b,
GenSymConstrained cspec c,
Mergeable c
) =>
GenSymConstrained (aspec, bspec, cspec) (a, b, c)
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec, cspec) -> m (UnionM (a, b, c))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec) = do
UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
UnionM c
c1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err cspec
cspec
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx)
instance
( GenSymSimpleConstrained aspec a,
GenSymSimpleConstrained bspec b,
GenSymSimpleConstrained cspec c
) =>
GenSymSimpleConstrained (aspec, bspec, cspec) (a, b, c)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec, cspec) -> m (a, b, c)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec) = do
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
(,,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e cspec
cspec
instance
( GenSymConstrained aspec a,
Mergeable a,
GenSymConstrained bspec b,
Mergeable b,
GenSymConstrained cspec c,
Mergeable c,
GenSymConstrained dspec d,
Mergeable d
) =>
GenSymConstrained (aspec, bspec, cspec, dspec) (a, b, c, d)
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec, cspec, dspec) -> m (UnionM (a, b, c, d))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec) = do
UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
UnionM c
c1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err cspec
cspec
UnionM d
d1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err dspec
dspec
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
d
dx <- UnionM d
d1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx)
instance
( GenSymSimpleConstrained aspec a,
GenSymSimpleConstrained bspec b,
GenSymSimpleConstrained cspec c,
GenSymSimpleConstrained dspec d
) =>
GenSymSimpleConstrained (aspec, bspec, cspec, dspec) (a, b, c, d)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec, cspec, dspec) -> m (a, b, c, d)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec) = do
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
(,,,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e cspec
cspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e dspec
dspec
instance
( GenSymConstrained aspec a,
Mergeable a,
GenSymConstrained bspec b,
Mergeable b,
GenSymConstrained cspec c,
Mergeable c,
GenSymConstrained dspec d,
Mergeable d,
GenSymConstrained espec e,
Mergeable e
) =>
GenSymConstrained (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec)
-> m (UnionM (a, b, c, d, e))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec) = do
UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
UnionM c
c1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err cspec
cspec
UnionM d
d1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err dspec
dspec
UnionM e
e1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err espec
espec
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
d
dx <- UnionM d
d1
e
ex <- UnionM e
e1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex)
instance
( GenSymSimpleConstrained aspec a,
GenSymSimpleConstrained bspec b,
GenSymSimpleConstrained cspec c,
GenSymSimpleConstrained dspec d,
GenSymSimpleConstrained espec e
) =>
GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec, cspec, dspec, espec) -> m (a, b, c, d, e)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec) = do
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
(,,,,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e cspec
cspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e dspec
dspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e espec
espec
instance
( GenSymConstrained aspec a,
Mergeable a,
GenSymConstrained bspec b,
Mergeable b,
GenSymConstrained cspec c,
Mergeable c,
GenSymConstrained dspec d,
Mergeable d,
GenSymConstrained espec e,
Mergeable e,
GenSymConstrained fspec f,
Mergeable f
) =>
GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec)
-> m (UnionM (a, b, c, d, e, f))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec) = do
UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
UnionM c
c1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err cspec
cspec
UnionM d
d1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err dspec
dspec
UnionM e
e1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err espec
espec
UnionM f
f1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err fspec
fspec
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
d
dx <- UnionM d
d1
e
ex <- UnionM e
e1
f
fx <- UnionM f
f1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex, f
fx)
instance
( GenSymSimpleConstrained aspec a,
GenSymSimpleConstrained bspec b,
GenSymSimpleConstrained cspec c,
GenSymSimpleConstrained dspec d,
GenSymSimpleConstrained espec e,
GenSymSimpleConstrained fspec f
) =>
GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec)
-> m (a, b, c, d, e, f)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec) = do
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
(,,,,,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e cspec
cspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e dspec
dspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e espec
espec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e fspec
fspec
instance
( GenSymConstrained aspec a,
Mergeable a,
GenSymConstrained bspec b,
Mergeable b,
GenSymConstrained cspec c,
Mergeable c,
GenSymConstrained dspec d,
Mergeable d,
GenSymConstrained espec e,
Mergeable e,
GenSymConstrained fspec f,
Mergeable f,
GenSymConstrained gspec g,
Mergeable g
) =>
GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec, gspec)
-> m (UnionM (a, b, c, d, e, f, g))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec) = do
UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
UnionM c
c1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err cspec
cspec
UnionM d
d1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err dspec
dspec
UnionM e
e1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err espec
espec
UnionM f
f1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err fspec
fspec
UnionM g
g1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err gspec
gspec
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
d
dx <- UnionM d
d1
e
ex <- UnionM e
e1
f
fx <- UnionM f
f1
g
gx <- UnionM g
g1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex, f
fx, g
gx)
instance
( GenSymSimpleConstrained aspec a,
GenSymSimpleConstrained bspec b,
GenSymSimpleConstrained cspec c,
GenSymSimpleConstrained dspec d,
GenSymSimpleConstrained espec e,
GenSymSimpleConstrained fspec f,
GenSymSimpleConstrained gspec g
) =>
GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec, gspec)
-> m (a, b, c, d, e, f, g)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec) = do
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
(,,,,,,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e cspec
cspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e dspec
dspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e espec
espec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e fspec
fspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e gspec
gspec
instance
( GenSymConstrained aspec a,
Mergeable a,
GenSymConstrained bspec b,
Mergeable b,
GenSymConstrained cspec c,
Mergeable c,
GenSymConstrained dspec d,
Mergeable d,
GenSymConstrained espec e,
Mergeable e,
GenSymConstrained fspec f,
Mergeable f,
GenSymConstrained gspec g,
Mergeable g,
GenSymConstrained hspec h,
Mergeable h
) =>
GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec)
-> m (UnionM (a, b, c, d, e, f, g, h))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec, hspec
hspec) = do
UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
UnionM c
c1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err cspec
cspec
UnionM d
d1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err dspec
dspec
UnionM e
e1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err espec
espec
UnionM f
f1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err fspec
fspec
UnionM g
g1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err gspec
gspec
UnionM h
h1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err hspec
hspec
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
a
ax <- UnionM a
a1
b
bx <- UnionM b
b1
c
cx <- UnionM c
c1
d
dx <- UnionM d
d1
e
ex <- UnionM e
e1
f
fx <- UnionM f
f1
g
gx <- UnionM g
g1
h
hx <- UnionM h
h1
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex, f
fx, g
gx, h
hx)
instance
( GenSymSimpleConstrained aspec a,
GenSymSimpleConstrained bspec b,
GenSymSimpleConstrained cspec c,
GenSymSimpleConstrained dspec d,
GenSymSimpleConstrained espec e,
GenSymSimpleConstrained fspec f,
GenSymSimpleConstrained gspec g,
GenSymSimpleConstrained hspec h
) =>
GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec)
-> m (a, b, c, d, e, f, g, h)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec, hspec
hspec) = do
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
(,,,,,,,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e cspec
cspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e dspec
dspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e espec
espec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e fspec
fspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e gspec
gspec
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e hspec
hspec
instance
{-# OVERLAPPABLE #-}
( GenSymConstrained spec (m (Maybe a)),
Mergeable1 m,
Mergeable a
) =>
GenSymConstrained spec (MaybeT m a)
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> spec -> m (UnionM (MaybeT m a))
freshConstrained e
e spec
v = do
UnionM (m (Maybe a))
x <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e spec
v
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ UnionM (m (Maybe a))
x
instance
{-# OVERLAPPABLE #-}
( GenSymSimpleConstrained spec (m (Maybe a)),
Mergeable1 m,
Mergeable a
) =>
GenSymSimpleConstrained spec (MaybeT m a)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> spec -> m (MaybeT m a)
simpleFreshConstrained e
e spec
v = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e spec
v
instance
{-# OVERLAPPING #-}
( GenSymSimpleConstrained (m (Maybe a)) (m (Maybe a)),
Mergeable1 m,
Mergeable a
) =>
GenSymSimpleConstrained (MaybeT m a) (MaybeT m a)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> MaybeT m a -> m (MaybeT m a)
simpleFreshConstrained e
e (MaybeT m (Maybe a)
v) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e m (Maybe a)
v
instance
{-# OVERLAPPING #-}
( GenSymSimpleConstrained (m (Maybe a)) (m (Maybe a)),
Mergeable1 m,
Mergeable a
) =>
GenSymConstrained (MaybeT m a) (MaybeT m a)
instance
{-# OVERLAPPABLE #-}
( GenSymConstrained spec (m (Either a b)),
Mergeable1 m,
Mergeable a,
Mergeable b
) =>
GenSymConstrained spec (ExceptT a m b)
where
freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> spec -> m (UnionM (ExceptT a m b))
freshConstrained e
e spec
v = do
UnionM (m (Either a b))
x <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e spec
v
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> b
$ UnionM (m (Either a b))
x
instance
{-# OVERLAPPABLE #-}
( GenSymSimpleConstrained spec (m (Either a b)),
Mergeable1 m,
Mergeable a,
Mergeable b
) =>
GenSymSimpleConstrained spec (ExceptT a m b)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> spec -> m (ExceptT a m b)
simpleFreshConstrained e
e spec
v = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e spec
v
instance
{-# OVERLAPPING #-}
( GenSymSimpleConstrained (m (Either e a)) (m (Either e a)),
Mergeable1 m,
Mergeable e,
Mergeable a
) =>
GenSymSimpleConstrained (ExceptT e m a) (ExceptT e m a)
where
simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> ExceptT e m a -> m (ExceptT e m a)
simpleFreshConstrained e
e (ExceptT m (Either e a)
v) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e m (Either e a)
v
instance
{-# OVERLAPPING #-}
( GenSymSimpleConstrained (m (Either e a)) (m (Either e a)),
Mergeable1 m,
Mergeable e,
Mergeable a
) =>
GenSymConstrained (ExceptT e m a) (ExceptT e m a)
class GenSymConstrainedNoSpec a where
freshConstrainedNoSpec ::
( MonadFresh m,
MonadError e m,
UnionLike m
) =>
e ->
m (UnionM (a c))
instance GenSymConstrainedNoSpec U1 where
freshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (UnionM (U1 c))
freshConstrainedNoSpec e
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall k (p :: k). U1 p
U1
instance (GenSymConstrained () c) => GenSymConstrainedNoSpec (K1 i c) where
freshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (UnionM (K1 i c c))
freshConstrainedNoSpec e
e = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i c (p :: k). c -> K1 i c p
K1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e ()
instance (GenSymConstrainedNoSpec a) => GenSymConstrainedNoSpec (M1 i c a) where
freshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (UnionM (M1 i c a c))
freshConstrainedNoSpec e
e = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> m (UnionM (a c))
freshConstrainedNoSpec e
e
instance
( GenSymConstrainedNoSpec a,
GenSymConstrainedNoSpec b,
forall x. Mergeable (a x),
forall x. Mergeable (b x)
) =>
GenSymConstrainedNoSpec (a :+: b)
where
freshConstrainedNoSpec ::
forall m c e.
( MonadFresh m,
MonadError e m,
UnionLike m
) =>
e ->
m (UnionM ((a :+: b) c))
freshConstrainedNoSpec :: forall (m :: * -> *) c e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (UnionM ((:+:) a b c))
freshConstrainedNoSpec e
e = do
SymBool
cond :: bool <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh ()
UnionM (a c)
l :: UnionM (a c) <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> m (UnionM (a c))
freshConstrainedNoSpec e
e
UnionM (b c)
r :: UnionM (b c) <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> m (UnionM (a c))
freshConstrainedNoSpec e
e
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 UnionM (a c)
l) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 UnionM (b c)
r)
instance
(GenSymConstrainedNoSpec a, GenSymConstrainedNoSpec b) =>
GenSymConstrainedNoSpec (a :*: b)
where
freshConstrainedNoSpec ::
forall m c e.
( MonadFresh m,
MonadError e m,
UnionLike m
) =>
e ->
m (UnionM ((a :*: b) c))
freshConstrainedNoSpec :: forall (m :: * -> *) c e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (UnionM ((:*:) a b c))
freshConstrainedNoSpec e
e = do
UnionM (a c)
l :: UnionM (a c) <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> m (UnionM (a c))
freshConstrainedNoSpec e
e
UnionM (b c)
r :: UnionM (b c) <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> m (UnionM (a c))
freshConstrainedNoSpec e
e
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
a c
l1 <- UnionM (a c)
l
b c
r1 <- UnionM (b c)
r
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a c
l1 forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b c
r1
derivedFreshConstrainedNoSpec ::
forall a m e.
( Generic a,
GenSymConstrainedNoSpec (Rep a),
Mergeable a,
MonadFresh m,
MonadError e m,
UnionLike m
) =>
e ->
() ->
m (UnionM a)
derivedFreshConstrainedNoSpec :: forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a,
MonadFresh m, MonadError e m, UnionLike m) =>
e -> () -> m (UnionM a)
derivedFreshConstrainedNoSpec e
e ()
_ = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a x. Generic a => Rep a x -> a
to) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> m (UnionM (a c))
freshConstrainedNoSpec e
e
class GenSymSimpleConstrainedNoSpec a where
simpleFreshConstrainedNoSpec ::
( MonadFresh m,
MonadError e m,
UnionLike m
) =>
e ->
m (a c)
instance GenSymSimpleConstrainedNoSpec U1 where
simpleFreshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (U1 c)
simpleFreshConstrainedNoSpec e
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall k (p :: k). U1 p
U1
instance (GenSymSimpleConstrained () c) => GenSymSimpleConstrainedNoSpec (K1 i c) where
simpleFreshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (K1 i c c)
simpleFreshConstrainedNoSpec e
e = forall k i c (p :: k). c -> K1 i c p
K1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e ()
instance (GenSymSimpleConstrainedNoSpec a) => GenSymSimpleConstrainedNoSpec (M1 i c a) where
simpleFreshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (M1 i c a c)
simpleFreshConstrainedNoSpec e
e = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) e c.
(GenSymSimpleConstrainedNoSpec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> m (a c)
simpleFreshConstrainedNoSpec e
e
instance
(GenSymSimpleConstrainedNoSpec a, GenSymSimpleConstrainedNoSpec b) =>
GenSymSimpleConstrainedNoSpec (a :*: b)
where
simpleFreshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m ((:*:) a b c)
simpleFreshConstrainedNoSpec e
e = do
a c
l :: a c <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymSimpleConstrainedNoSpec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> m (a c)
simpleFreshConstrainedNoSpec e
e
b c
r :: b c <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymSimpleConstrainedNoSpec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> m (a c)
simpleFreshConstrainedNoSpec e
e
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a c
l forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b c
r
derivedSimpleFreshConstrainedNoSpec ::
forall a m e.
( Generic a,
GenSymSimpleConstrainedNoSpec (Rep a),
MonadFresh m,
MonadError e m,
UnionLike m,
Mergeable a
) =>
e ->
() ->
m a
derivedSimpleFreshConstrainedNoSpec :: forall a (m :: * -> *) e.
(Generic a, GenSymSimpleConstrainedNoSpec (Rep a), MonadFresh m,
MonadError e m, UnionLike m, Mergeable a) =>
e -> () -> m a
derivedSimpleFreshConstrainedNoSpec e
e ()
_ = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a x. Generic a => Rep a x -> a
to) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> *) (m :: * -> *) e c.
(GenSymSimpleConstrainedNoSpec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> m (a c)
simpleFreshConstrainedNoSpec e
e
class GenSymConstrainedSameShape a where
simpleFreshConstrainedSameShape ::
( MonadFresh m,
MonadError e m,
UnionLike m
) =>
e ->
a c ->
m (a c)
instance GenSymConstrainedSameShape U1 where
simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> U1 c -> m (U1 c)
simpleFreshConstrainedSameShape e
_ U1 c
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall k (p :: k). U1 p
U1
instance (GenSymSimpleConstrained c c) => GenSymConstrainedSameShape (K1 i c) where
simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> K1 i c c -> m (K1 i c c)
simpleFreshConstrainedSameShape e
e (K1 c
c) = forall k i c (p :: k). c -> K1 i c p
K1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e c
c
instance (GenSymConstrainedSameShape a) => GenSymConstrainedSameShape (M1 i c a) where
simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> M1 i c a c -> m (M1 i c a c)
simpleFreshConstrainedSameShape e
e (M1 a c
a) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e a c
a
instance
(GenSymConstrainedSameShape a, GenSymConstrainedSameShape b) =>
GenSymConstrainedSameShape (a :+: b)
where
simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (:+:) a b c -> m ((:+:) a b c)
simpleFreshConstrainedSameShape e
e (L1 a c
a) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e a c
a
simpleFreshConstrainedSameShape e
e (R1 b c
a) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e b c
a
instance
(GenSymConstrainedSameShape a, GenSymConstrainedSameShape b) =>
GenSymConstrainedSameShape (a :*: b)
where
simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (:*:) a b c -> m ((:*:) a b c)
simpleFreshConstrainedSameShape e
e (a c
a :*: b c
b) = do
a c
l :: a c <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e a c
a
b c
r :: b c <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e b c
b
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a c
l forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b c
r
derivedSimpleFreshConstrainedSameShape ::
( Generic a,
GenSymConstrainedSameShape (Rep a),
Mergeable a,
MonadFresh m,
MonadError e m,
UnionLike m
) =>
e ->
a ->
m a
derivedSimpleFreshConstrainedSameShape :: forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedSameShape (Rep a), Mergeable a,
MonadFresh m, MonadError e m, UnionLike m) =>
e -> a -> m a
derivedSimpleFreshConstrainedSameShape e
e a
a = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a x. Generic a => Rep a x -> a
to) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
UnionLike m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e (forall a x. Generic a => a -> Rep a x
from a
a)