{-# 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
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Experimental.GenSymConstrained
  ( -- * Symbolic value generation with errors
    GenSymConstrained (..),
    GenSymSimpleConstrained (..),
    genSymConstrained,
    genSymSimpleConstrained,
    derivedFreshConstrainedNoSpec,
    derivedSimpleFreshConstrainedNoSpec,
    derivedSimpleFreshConstrainedSameShape,

    -- * Some common GenSymConstrained specifications
    SymOrdUpperBound (..),
    SymOrdLowerBound (..),
    SymOrdBound (..),
  )
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.Internal.Core.Control.Monad.Class.Union (MonadUnion)
import Grisette.Internal.Core.Control.Monad.Union
  ( Union,
    liftToMonadUnion,
  )
import Grisette.Internal.Core.Data.Class.GenSym
  ( GenSym (fresh),
    GenSymSimple (simpleFresh),
    ListSpec (ListSpec),
    MonadFresh,
    SimpleListSpec (SimpleListSpec),
    chooseFresh,
    chooseUnionFresh,
    runFreshT,
  )
import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp ((.||)))
import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable, Mergeable1)
import Grisette.Internal.Core.Data.Class.SimpleMergeable
  ( mrgIf,
  )
import Grisette.Internal.Core.Data.Class.SymOrd (SymOrd ((.<), (.>=)))
import Grisette.Internal.Core.Data.Class.TryMerge
  ( mrgSingle,
    tryMerge,
  )
import Grisette.Internal.Core.Data.Symbol (Identifier)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.Experimental
-- >>> import Grisette.SymPrim

-- | Class of types in which symbolic values can be generated with some
-- specification.
--
-- See 'GenSym' for more details. The difference of this class is that it allows
-- constraints to be generated along with the generation of symbolic values.
class (Mergeable a) => GenSymConstrained spec a where
  -- | Generates a symbolic value with the given specification.
  --
  -- Constraint violations will throw an error in the monadic environment.
  --
  -- >>> runFreshT (freshConstrained () (SymOrdUpperBound (1 :: SymInteger) ())) "a" :: ExceptT () Union (Union SymInteger)
  -- ExceptT <If (<= 1 a@0) (Left ()) (Right {a@0})>
  freshConstrained ::
    (MonadFresh m, MonadError e m, MonadUnion m) =>
    e ->
    spec ->
    m (Union a)
  default freshConstrained ::
    (GenSymSimpleConstrained spec a) =>
    ( MonadFresh m,
      MonadError e m,
      MonadUnion m
    ) =>
    e ->
    spec ->
    m (Union a)
  freshConstrained e
e spec
spec = a -> Union a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a -> Union a) -> m a -> m (Union a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> spec -> m a
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> spec -> m a
simpleFreshConstrained e
e spec
spec

-- | Generates a symbolic value with the given specification, also place the
-- necessary constraints.
genSymConstrained :: forall spec a e. (GenSymConstrained spec a, Mergeable e) => e -> spec -> Identifier -> ExceptT e Union (Union a)
genSymConstrained :: forall spec a e.
(GenSymConstrained spec a, Mergeable e) =>
e -> spec -> Identifier -> ExceptT e Union (Union a)
genSymConstrained e
e spec
spec = ExceptT e Union (Union a) -> ExceptT e Union (Union a)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (ExceptT e Union (Union a) -> ExceptT e Union (Union a))
-> (Identifier -> ExceptT e Union (Union a))
-> Identifier
-> ExceptT e Union (Union a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreshT (ExceptT e Union) (Union a)
-> Identifier -> ExceptT e Union (Union a)
forall (m :: * -> *) a. Monad m => FreshT m a -> Identifier -> m a
runFreshT (e -> spec -> FreshT (ExceptT e Union) (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> spec -> m (Union a)
freshConstrained e
e spec
spec)

-- | Class of types in which symbolic values can be generated with some
-- specification.
--
-- See 'GenSymSimple' for more details. The difference of this class is that it allows
-- constraints to be generated along with the generation of symbolic values.
class (Mergeable a) => GenSymSimpleConstrained spec a where
  -- | Generates a symbolic value with the given specification.
  --
  -- Constraint violations will throw an error in the monadic environment.
  --
  -- >>> runFreshT (simpleFreshConstrained () (SymOrdUpperBound (1 :: SymInteger) ())) "a" :: ExceptT () Union SymInteger
  -- ExceptT <If (<= 1 a@0) (Left ()) (Right a@0)>
  simpleFreshConstrained ::
    (MonadFresh m, MonadError e m, MonadUnion m) =>
    e ->
    spec ->
    m a

-- | Generates a symbolic value with the given specification, also place the
-- necessary constraints.
genSymSimpleConstrained :: forall spec a e. (GenSymSimpleConstrained spec a, Mergeable e) => e -> spec -> Identifier -> ExceptT e Union a
genSymSimpleConstrained :: forall spec a e.
(GenSymSimpleConstrained spec a, Mergeable e) =>
e -> spec -> Identifier -> ExceptT e Union a
genSymSimpleConstrained e
e spec
spec = ExceptT e Union a -> ExceptT e Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (ExceptT e Union a -> ExceptT e Union a)
-> (Identifier -> ExceptT e Union a)
-> Identifier
-> ExceptT e Union a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreshT (ExceptT e Union) a -> Identifier -> ExceptT e Union a
forall (m :: * -> *) a. Monad m => FreshT m a -> Identifier -> m a
runFreshT (e -> spec -> FreshT (ExceptT e Union) a
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion 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, MonadUnion m) =>
e -> spec -> m (Union a)
freshConstrained e
_ = spec -> m (Union a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (Union a)
forall (m :: * -> *). MonadFresh m => spec -> m (Union a)
fresh

instance {-# OVERLAPPABLE #-} (Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained spec a where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> spec -> m a
simpleFreshConstrained e
_ = spec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => spec -> m a
simpleFresh

-- | Exclusive bound, generates the values with the specification, then filters
-- out the ones that are greater than or equal to the bound
data SymOrdUpperBound a spec = SymOrdUpperBound a spec

instance {-# OVERLAPPABLE #-} (SymOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SymOrdUpperBound a spec) a where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> SymOrdUpperBound a spec -> m (Union a)
freshConstrained e
e (SymOrdUpperBound a
u spec
spec) = do
    Union a
s <- spec -> m (Union a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (Union a)
forall (m :: * -> *). MonadFresh m => spec -> m (Union a)
fresh spec
spec
    a
v <- Union a -> m a
forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
Union a -> u a
liftToMonadUnion Union a
s
    SymBool -> m () -> m () -> m ()
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
v a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
u) (e -> m ()
forall a. e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (() -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
    Union a -> m (Union a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union a -> m (Union a)) -> Union a -> m (Union a)
forall a b. (a -> b) -> a -> b
$ a -> Union a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
v

instance {-# OVERLAPPABLE #-} (SymOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SymOrdUpperBound a spec) a where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> SymOrdUpperBound a spec -> m a
simpleFreshConstrained e
e (SymOrdUpperBound a
u spec
spec) = do
    a
s <- 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
    SymBool -> m () -> m () -> m ()
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
s a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
u) (e -> m ()
forall a. e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (() -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
    a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
s

-- | Inclusive bound, generates the values with the specification, then filters
-- out the ones that are less than the bound
data SymOrdLowerBound a spec = SymOrdLowerBound a spec

instance {-# OVERLAPPABLE #-} (SymOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SymOrdLowerBound a spec) a where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> SymOrdLowerBound a spec -> m (Union a)
freshConstrained e
e (SymOrdLowerBound a
l spec
spec) = do
    Union a
s <- spec -> m (Union a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (Union a)
forall (m :: * -> *). MonadFresh m => spec -> m (Union a)
fresh spec
spec
    a
v <- Union a -> m a
forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
Union a -> u a
liftToMonadUnion Union a
s
    SymBool -> m () -> m () -> m ()
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
v a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< a
l) (e -> m ()
forall a. e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (() -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
    Union a -> m (Union a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union a -> m (Union a)) -> Union a -> m (Union a)
forall a b. (a -> b) -> a -> b
$ a -> Union a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
v

instance {-# OVERLAPPABLE #-} (SymOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SymOrdLowerBound a spec) a where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> SymOrdLowerBound a spec -> m a
simpleFreshConstrained e
e (SymOrdLowerBound a
l spec
spec) = do
    a
s <- 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
    SymBool -> m () -> m () -> m ()
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
s a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< a
l) (e -> m ()
forall a. e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (() -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
    a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
s

-- | Left-inclusive, right-exclusive bound, generates the values with the
-- specification, then filters out the ones that are out-of-bound
data SymOrdBound a spec = SymOrdBound a a spec

instance {-# OVERLAPPABLE #-} (SymOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SymOrdBound a spec) a where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> SymOrdBound a spec -> m (Union a)
freshConstrained e
e (SymOrdBound a
l a
u spec
spec) = do
    Union a
s <- spec -> m (Union a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (Union a)
forall (m :: * -> *). MonadFresh m => spec -> m (Union a)
fresh spec
spec
    a
v <- Union a -> m a
forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
Union a -> u a
liftToMonadUnion Union a
s
    SymBool -> m () -> m () -> m ()
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
v a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< a
l SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| a
v a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
u) (e -> m ()
forall a. e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (() -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
    Union a -> m (Union a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union a -> m (Union a)) -> Union a -> m (Union a)
forall a b. (a -> b) -> a -> b
$ a -> Union a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
v

instance {-# OVERLAPPABLE #-} (SymOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SymOrdBound a spec) a where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> SymOrdBound a spec -> m a
simpleFreshConstrained e
e (SymOrdBound a
l a
u spec
spec) = do
    a
s <- 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
    SymBool -> m () -> m () -> m ()
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
s a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< a
l SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| a
s a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
u) (e -> m ()
forall a. e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (() -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
    a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
s

instance GenSymConstrained (SymOrdBound Integer ()) Integer where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> SymOrdBound Integer () -> m (Union Integer)
freshConstrained e
_ (SymOrdBound Integer
l Integer
r ()
_) = [Integer] -> m (Union Integer)
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (Union a)
chooseFresh [Integer
l .. Integer
r Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1]

-- Either
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, MonadUnion m) =>
e -> Either aspec bspec -> m (Union (Either a b))
freshConstrained e
e (Left aspec
aspec) = m (Union (Either a b)) -> m (Union (Either a b))
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (Union (Either a b)) -> m (Union (Either a b)))
-> m (Union (Either a b)) -> m (Union (Either a b))
forall a b. (a -> b) -> a -> b
$ (Union (Either a b) -> Union (Either a b)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union (Either a b) -> Union (Either a b))
-> (Union a -> Union (Either a b)) -> Union a -> Union (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Either a b) -> Union a -> Union (Either a b)
forall a b. (a -> b) -> Union a -> Union 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) (Union a -> Union (Either a b))
-> m (Union a) -> m (Union (Either a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> aspec -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m (Union a)
freshConstrained e
e aspec
aspec
  freshConstrained e
e (Right bspec
bspec) = m (Union (Either a b)) -> m (Union (Either a b))
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (Union (Either a b)) -> m (Union (Either a b)))
-> m (Union (Either a b)) -> m (Union (Either a b))
forall a b. (a -> b) -> a -> b
$ (Union (Either a b) -> Union (Either a b)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union (Either a b) -> Union (Either a b))
-> (Union b -> Union (Either a b)) -> Union b -> Union (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Either a b) -> Union b -> Union (Either a b)
forall a b. (a -> b) -> Union a -> Union 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) (Union b -> Union (Either a b))
-> m (Union b) -> m (Union (Either a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> bspec -> m (Union b)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m (Union b)
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, MonadUnion m) =>
e -> Either a b -> m (Either a b)
simpleFreshConstrained = e -> Either a b -> m (Either a b)
forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedSameShape (Rep a), Mergeable a,
 MonadFresh m, MonadError e m, MonadUnion 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, MonadUnion m) =>
e -> () -> m (Union (Either a b))
freshConstrained = e -> () -> m (Union (Either a b))
forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a,
 MonadFresh m, MonadError e m, MonadUnion m) =>
e -> () -> m (Union a)
derivedFreshConstrainedNoSpec

-- Maybe
instance
  (GenSymConstrained aspec a, Mergeable a) =>
  GenSymConstrained (Maybe aspec) (Maybe a)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Maybe aspec -> m (Union (Maybe a))
freshConstrained e
_ Maybe aspec
Nothing = Union (Maybe a) -> m (Union (Maybe a))
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union (Maybe a) -> m (Union (Maybe a)))
-> Union (Maybe a) -> m (Union (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> Union (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Maybe a
forall a. Maybe a
Nothing
  freshConstrained e
e (Just aspec
aspec) = m (Union (Maybe a)) -> m (Union (Maybe a))
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (Union (Maybe a)) -> m (Union (Maybe a)))
-> m (Union (Maybe a)) -> m (Union (Maybe a))
forall a b. (a -> b) -> a -> b
$ (Union (Maybe a) -> Union (Maybe a)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union (Maybe a) -> Union (Maybe a))
-> (Union a -> Union (Maybe a)) -> Union a -> Union (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe a) -> Union a -> Union (Maybe a)
forall a b. (a -> b) -> Union a -> Union b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Maybe a
forall a. a -> Maybe a
Just) (Union a -> Union (Maybe a)) -> m (Union a) -> m (Union (Maybe a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> aspec -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m (Union 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, MonadUnion m) =>
e -> Maybe aspec -> m (Maybe a)
simpleFreshConstrained e
_ Maybe aspec
Nothing = Maybe a -> m (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Maybe a
forall a. Maybe a
Nothing
  simpleFreshConstrained e
e (Just aspec
aspec) = m (Maybe a) -> m (Maybe a)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (Maybe a) -> m (Maybe a)) -> m (Maybe a) -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ 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
<$> e -> aspec -> m a
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> 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, MonadUnion m) =>
e -> aspec -> m (Union (Maybe a))
freshConstrained e
e aspec
aspec = do
    Union a
a :: Union a <- e -> aspec -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m (Union a)
freshConstrained e
e aspec
aspec
    m (Union (Maybe a)) -> m (Union (Maybe a))
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (Union (Maybe a)) -> m (Union (Maybe a)))
-> m (Union (Maybe a)) -> m (Union (Maybe a))
forall a b. (a -> b) -> a -> b
$ [Union (Maybe a)] -> m (Union (Maybe a))
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[Union a] -> m (Union a)
chooseUnionFresh [Maybe a -> Union (Maybe a)
forall a. a -> Union a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing, a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> Union a -> Union (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Union a
a]

-- List
instance
  (GenSymConstrained () a, Mergeable a) =>
  GenSymConstrained Integer [a]
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Integer -> m (Union [a])
freshConstrained e
e Integer
v = do
    [Union a]
l <- e -> Integer -> m [Union a]
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Integer -> m [Union a]
gl e
e Integer
v
    let xs :: [[Union a]]
xs = [[Union a]] -> [[Union a]]
forall a. [a] -> [a]
reverse ([[Union a]] -> [[Union a]]) -> [[Union a]] -> [[Union a]]
forall a b. (a -> b) -> a -> b
$ (Union a -> [Union a] -> [Union a])
-> [Union a] -> [Union a] -> [[Union a]]
forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr (:) [] [Union a]
l
    m (Union [a]) -> m (Union [a])
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (Union [a]) -> m (Union [a])) -> m (Union [a]) -> m (Union [a])
forall a b. (a -> b) -> a -> b
$ [Union [a]] -> m (Union [a])
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[Union a] -> m (Union a)
chooseUnionFresh ([Union [a]] -> m (Union [a])) -> [Union [a]] -> m (Union [a])
forall a b. (a -> b) -> a -> b
$ Union [a] -> Union [a]
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union [a] -> Union [a])
-> ([Union a] -> Union [a]) -> [Union a] -> Union [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Union a] -> Union [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 ([Union a] -> Union [a]) -> [[Union a]] -> [Union [a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Union a]]
xs
    where
      gl :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> Integer -> m [Union a]
      gl :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Integer -> m [Union a]
gl e
e1 Integer
v1
        | Integer
v1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 = [Union a] -> m [Union a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle []
        | Bool
otherwise = do
            Union a
l <- e -> () -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> () -> m (Union a)
freshConstrained e
e1 ()
            [Union a]
r <- e -> Integer -> m [Union a]
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Integer -> m [Union a]
gl e
e1 (Integer
v1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
            [Union a] -> m [Union a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle ([Union a] -> m [Union a]) -> [Union a] -> m [Union a]
forall a b. (a -> b) -> a -> b
$ Union a
l Union a -> [Union a] -> [Union a]
forall a. a -> [a] -> [a]
: [Union a]
r

instance
  (GenSymConstrained spec a, Mergeable a) =>
  GenSymConstrained (ListSpec spec) [a]
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> ListSpec spec -> m (Union [a])
freshConstrained e
e (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 [Char] -> m (Union [a])
forall a. HasCallStack => [Char] -> a
error ([Char] -> m (Union [a])) -> [Char] -> m (Union [a])
forall a b. (a -> b) -> a -> b
$ [Char]
"Bad lengths: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> [Char]
forall a. Show a => a -> [Char]
show (Int
minLen, Int
maxLen)
      else do
        [Union a]
l <- e -> Int -> m [Union a]
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Int -> m [Union a]
gl e
e Int
maxLen
        let xs :: [[Union a]]
xs = Int -> [[Union a]] -> [[Union a]]
forall a. Int -> [a] -> [a]
drop Int
minLen ([[Union a]] -> [[Union a]]) -> [[Union a]] -> [[Union a]]
forall a b. (a -> b) -> a -> b
$ [[Union a]] -> [[Union a]]
forall a. [a] -> [a]
reverse ([[Union a]] -> [[Union a]]) -> [[Union a]] -> [[Union a]]
forall a b. (a -> b) -> a -> b
$ (Union a -> [Union a] -> [Union a])
-> [Union a] -> [Union a] -> [[Union a]]
forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr (:) [] [Union a]
l
        m (Union [a]) -> m (Union [a])
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (Union [a]) -> m (Union [a])) -> m (Union [a]) -> m (Union [a])
forall a b. (a -> b) -> a -> b
$ [Union [a]] -> m (Union [a])
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[Union a] -> m (Union a)
chooseUnionFresh ([Union [a]] -> m (Union [a])) -> [Union [a]] -> m (Union [a])
forall a b. (a -> b) -> a -> b
$ Union [a] -> Union [a]
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union [a] -> Union [a])
-> ([Union a] -> Union [a]) -> [Union a] -> Union [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Union a] -> Union [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 ([Union a] -> Union [a]) -> [[Union a]] -> [Union [a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Union a]]
xs
    where
      gl :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> Int -> m [Union a]
      gl :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Int -> m [Union a]
gl e
e1 Int
currLen
        | Int
currLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [Union a] -> m [Union a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        | Bool
otherwise = do
            Union a
l <- e -> spec -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> spec -> m (Union a)
freshConstrained e
e1 spec
subSpec
            [Union a]
r <- e -> Int -> m [Union a]
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Int -> m [Union a]
gl e
e1 (Int
currLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
            [Union a] -> m [Union a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Union a] -> m [Union a]) -> [Union a] -> m [Union a]
forall a b. (a -> b) -> a -> b
$ Union a
l Union a -> [Union a] -> [Union a]
forall a. a -> [a] -> [a]
: [Union a]
r

instance
  (GenSymConstrained a a, Mergeable a) =>
  GenSymConstrained [a] [a]
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> [a] -> m (Union [a])
freshConstrained e
e [a]
l = do
    [Union a]
r :: [Union a] <- (a -> m (Union a)) -> [a] -> m [Union 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 (e -> a -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> a -> m (Union a)
freshConstrained e
e) [a]
l
    Union [a] -> m (Union [a])
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union [a] -> m (Union [a])) -> Union [a] -> m (Union [a])
forall a b. (a -> b) -> a -> b
$ Union [a] -> Union [a]
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union [a] -> Union [a]) -> Union [a] -> Union [a]
forall a b. (a -> b) -> a -> b
$ [Union a] -> Union [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 [Union a]
r

instance
  (GenSymSimpleConstrained a a) =>
  GenSymSimpleConstrained [a] [a]
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> [a] -> m [a]
simpleFreshConstrained = e -> [a] -> m [a]
forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedSameShape (Rep a), Mergeable a,
 MonadFresh m, MonadError e m, MonadUnion 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, MonadUnion m) =>
e -> SimpleListSpec spec -> m (Union [a])
freshConstrained e
e (SimpleListSpec Int
len spec
subSpec) =
    if Int
len Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
      then [Char] -> m (Union [a])
forall a. HasCallStack => [Char] -> a
error ([Char] -> m (Union [a])) -> [Char] -> m (Union [a])
forall a b. (a -> b) -> a -> b
$ [Char]
"Bad lengths: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
len
      else do
        m (Union [a]) -> m (Union [a])
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (Union [a]) -> m (Union [a])) -> m (Union [a]) -> m (Union [a])
forall a b. (a -> b) -> a -> b
$ Union [a] -> Union [a]
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union [a] -> Union [a])
-> ([Union a] -> Union [a]) -> [Union a] -> Union [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Union a] -> Union [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 ([Union a] -> Union [a]) -> m [Union a] -> m (Union [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> Int -> m [Union a]
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Int -> m [Union a]
gl e
e Int
len
    where
      gl :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> Int -> m [Union a]
      gl :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Int -> m [Union a]
gl e
e1 Int
currLen
        | Int
currLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [Union a] -> m [Union a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle []
        | Bool
otherwise = do
            Union a
l <- e -> spec -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> spec -> m (Union a)
freshConstrained e
e1 spec
subSpec
            [Union a]
r <- e -> Int -> m [Union a]
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Int -> m [Union a]
gl e
e1 (Int
currLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
            [Union a] -> m [Union a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle ([Union a] -> m [Union a]) -> [Union a] -> m [Union a]
forall a b. (a -> b) -> a -> b
$ Union a
l Union a -> [Union a] -> [Union a]
forall a. a -> [a] -> [a]
: [Union a]
r

instance
  (GenSymSimpleConstrained spec a) =>
  GenSymSimpleConstrained (SimpleListSpec spec) [a]
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> SimpleListSpec spec -> m [a]
simpleFreshConstrained e
e (SimpleListSpec Int
len spec
subSpec) =
    if Int
len Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
      then [Char] -> m [a]
forall a. HasCallStack => [Char] -> a
error ([Char] -> m [a]) -> [Char] -> m [a]
forall a b. (a -> b) -> a -> b
$ [Char]
"Bad lengths: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
len
      else do
        e -> Int -> m [a]
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Int -> m [a]
gl e
e Int
len
    where
      gl :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> Int -> m [a]
      gl :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Int -> m [a]
gl e
e1 Int
currLen
        | Int
currLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [a] -> m [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle []
        | Bool
otherwise = do
            a
l <- e -> spec -> m a
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> spec -> m a
simpleFreshConstrained e
e1 spec
subSpec
            [a]
r <- e -> Int -> m [a]
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Int -> m [a]
gl e
e1 (Int
currLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
            [a] -> m [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle ([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
  ( 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, MonadUnion m) =>
e -> (aspec, bspec) -> m (Union (a, b))
freshConstrained e
err (aspec
aspec, bspec
bspec) = do
    Union a
a1 <- e -> aspec -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m (Union a)
freshConstrained e
err aspec
aspec
    Union b
b1 <- e -> bspec -> m (Union b)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m (Union b)
freshConstrained e
err bspec
bspec
    Union (a, b) -> m (Union (a, b))
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union (a, b) -> m (Union (a, b)))
-> Union (a, b) -> m (Union (a, b))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- Union a
a1
      b
bx <- Union b
b1
      (a, b) -> Union (a, b)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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, MonadUnion m) =>
e -> (aspec, bspec) -> m (a, b)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec) = do
    m (a, b) -> m (a, b)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (a, b) -> m (a, b)) -> m (a, b) -> m (a, b)
forall a b. (a -> b) -> a -> b
$
      (,)
        (a -> b -> (a, b)) -> m a -> m (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> aspec -> m a
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m a
simpleFreshConstrained e
e 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
<*> e -> bspec -> m b
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m b
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, MonadUnion m) =>
e -> (aspec, bspec, cspec) -> m (Union (a, b, c))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec) = do
    Union a
a1 <- e -> aspec -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m (Union a)
freshConstrained e
err aspec
aspec
    Union b
b1 <- e -> bspec -> m (Union b)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m (Union b)
freshConstrained e
err bspec
bspec
    Union c
c1 <- e -> cspec -> m (Union c)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> cspec -> m (Union c)
freshConstrained e
err cspec
cspec
    Union (a, b, c) -> m (Union (a, b, c))
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union (a, b, c) -> m (Union (a, b, c)))
-> Union (a, b, c) -> m (Union (a, b, c))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- Union a
a1
      b
bx <- Union b
b1
      c
cx <- Union c
c1
      (a, b, c) -> Union (a, b, c)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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, MonadUnion m) =>
e -> (aspec, bspec, cspec) -> m (a, b, c)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec) = do
    m (a, b, c) -> m (a, b, c)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (a, b, c) -> m (a, b, c)) -> m (a, b, c) -> m (a, b, c)
forall a b. (a -> b) -> a -> b
$
      (,,)
        (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
<$> e -> aspec -> m a
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m a
simpleFreshConstrained e
e 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
<*> e -> bspec -> m b
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m b
simpleFreshConstrained e
e 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
<*> e -> cspec -> m c
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> cspec -> m c
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, MonadUnion m) =>
e -> (aspec, bspec, cspec, dspec) -> m (Union (a, b, c, d))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec) = do
    Union a
a1 <- e -> aspec -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m (Union a)
freshConstrained e
err aspec
aspec
    Union b
b1 <- e -> bspec -> m (Union b)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m (Union b)
freshConstrained e
err bspec
bspec
    Union c
c1 <- e -> cspec -> m (Union c)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> cspec -> m (Union c)
freshConstrained e
err cspec
cspec
    Union d
d1 <- e -> dspec -> m (Union d)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> dspec -> m (Union d)
freshConstrained e
err dspec
dspec
    Union (a, b, c, d) -> m (Union (a, b, c, d))
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union (a, b, c, d) -> m (Union (a, b, c, d)))
-> Union (a, b, c, d) -> m (Union (a, b, c, d))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- Union a
a1
      b
bx <- Union b
b1
      c
cx <- Union c
c1
      d
dx <- Union d
d1
      (a, b, c, d) -> Union (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
  ( 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, MonadUnion m) =>
e -> (aspec, bspec, cspec, dspec) -> m (a, b, c, d)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec) = do
    m (a, b, c, d) -> m (a, b, c, d)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (a, b, c, d) -> m (a, b, c, d))
-> m (a, b, c, d) -> m (a, b, c, d)
forall a b. (a -> b) -> a -> b
$
      (,,,)
        (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
<$> e -> aspec -> m a
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m a
simpleFreshConstrained e
e 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
<*> e -> bspec -> m b
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m b
simpleFreshConstrained e
e 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
<*> e -> cspec -> m c
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> cspec -> m c
simpleFreshConstrained e
e 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
<*> e -> dspec -> m d
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> dspec -> m d
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, MonadUnion m) =>
e
-> (aspec, bspec, cspec, dspec, espec) -> m (Union (a, b, c, d, e))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec) = do
    Union a
a1 <- e -> aspec -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m (Union a)
freshConstrained e
err aspec
aspec
    Union b
b1 <- e -> bspec -> m (Union b)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m (Union b)
freshConstrained e
err bspec
bspec
    Union c
c1 <- e -> cspec -> m (Union c)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> cspec -> m (Union c)
freshConstrained e
err cspec
cspec
    Union d
d1 <- e -> dspec -> m (Union d)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> dspec -> m (Union d)
freshConstrained e
err dspec
dspec
    Union e
e1 <- e -> espec -> m (Union e)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> espec -> m (Union e)
freshConstrained e
err espec
espec
    Union (a, b, c, d, e) -> m (Union (a, b, c, d, e))
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union (a, b, c, d, e) -> m (Union (a, b, c, d, e)))
-> Union (a, b, c, d, e) -> m (Union (a, b, c, d, e))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- Union a
a1
      b
bx <- Union b
b1
      c
cx <- Union c
c1
      d
dx <- Union d
d1
      e
ex <- Union e
e1
      (a, b, c, d, e) -> Union (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
  ( 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, MonadUnion 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
    m (a, b, c, d, e) -> m (a, b, c, d, e)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (a, b, c, d, e) -> m (a, b, c, d, e))
-> m (a, b, c, d, e) -> m (a, b, c, d, e)
forall a b. (a -> b) -> a -> b
$
      (,,,,)
        (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
<$> e -> aspec -> m a
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m a
simpleFreshConstrained e
e 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
<*> e -> bspec -> m b
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m b
simpleFreshConstrained e
e 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
<*> e -> cspec -> m c
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> cspec -> m c
simpleFreshConstrained e
e 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
<*> e -> dspec -> m d
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> dspec -> m d
simpleFreshConstrained e
e 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
<*> e -> espec -> m e
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> espec -> m e
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, MonadUnion m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec)
-> m (Union (a, b, c, d, e, f))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec) = do
    Union a
a1 <- e -> aspec -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m (Union a)
freshConstrained e
err aspec
aspec
    Union b
b1 <- e -> bspec -> m (Union b)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m (Union b)
freshConstrained e
err bspec
bspec
    Union c
c1 <- e -> cspec -> m (Union c)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> cspec -> m (Union c)
freshConstrained e
err cspec
cspec
    Union d
d1 <- e -> dspec -> m (Union d)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> dspec -> m (Union d)
freshConstrained e
err dspec
dspec
    Union e
e1 <- e -> espec -> m (Union e)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> espec -> m (Union e)
freshConstrained e
err espec
espec
    Union f
f1 <- e -> fspec -> m (Union f)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> fspec -> m (Union f)
freshConstrained e
err fspec
fspec
    Union (a, b, c, d, e, f) -> m (Union (a, b, c, d, e, f))
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union (a, b, c, d, e, f) -> m (Union (a, b, c, d, e, f)))
-> Union (a, b, c, d, e, f) -> m (Union (a, b, c, d, e, f))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- Union a
a1
      b
bx <- Union b
b1
      c
cx <- Union c
c1
      d
dx <- Union d
d1
      e
ex <- Union e
e1
      f
fx <- Union f
f1
      (a, b, c, d, e, f) -> Union (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
  ( 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, MonadUnion 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
    m (a, b, c, d, e, f) -> m (a, b, c, d, e, f)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (a, b, c, d, e, f) -> m (a, b, c, d, e, f))
-> m (a, b, c, d, e, f) -> m (a, b, c, d, e, f)
forall a b. (a -> b) -> a -> b
$
      (,,,,,)
        (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
<$> e -> aspec -> m a
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m a
simpleFreshConstrained e
e 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
<*> e -> bspec -> m b
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m b
simpleFreshConstrained e
e 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
<*> e -> cspec -> m c
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> cspec -> m c
simpleFreshConstrained e
e 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
<*> e -> dspec -> m d
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> dspec -> m d
simpleFreshConstrained e
e 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
<*> e -> espec -> m e
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> espec -> m e
simpleFreshConstrained e
e 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
<*> e -> fspec -> m f
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> fspec -> m f
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, MonadUnion m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec, gspec)
-> m (Union (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
    Union a
a1 <- e -> aspec -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m (Union a)
freshConstrained e
err aspec
aspec
    Union b
b1 <- e -> bspec -> m (Union b)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m (Union b)
freshConstrained e
err bspec
bspec
    Union c
c1 <- e -> cspec -> m (Union c)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> cspec -> m (Union c)
freshConstrained e
err cspec
cspec
    Union d
d1 <- e -> dspec -> m (Union d)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> dspec -> m (Union d)
freshConstrained e
err dspec
dspec
    Union e
e1 <- e -> espec -> m (Union e)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> espec -> m (Union e)
freshConstrained e
err espec
espec
    Union f
f1 <- e -> fspec -> m (Union f)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> fspec -> m (Union f)
freshConstrained e
err fspec
fspec
    Union g
g1 <- e -> gspec -> m (Union g)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> gspec -> m (Union g)
freshConstrained e
err gspec
gspec
    Union (a, b, c, d, e, f, g) -> m (Union (a, b, c, d, e, f, g))
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union (a, b, c, d, e, f, g) -> m (Union (a, b, c, d, e, f, g)))
-> Union (a, b, c, d, e, f, g) -> m (Union (a, b, c, d, e, f, g))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- Union a
a1
      b
bx <- Union b
b1
      c
cx <- Union c
c1
      d
dx <- Union d
d1
      e
ex <- Union e
e1
      f
fx <- Union f
f1
      g
gx <- Union g
g1
      (a, b, c, d, e, f, g) -> Union (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
  ( 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, MonadUnion 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
    m (a, b, c, d, e, f, g) -> m (a, b, c, d, e, f, g)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (a, b, c, d, e, f, g) -> m (a, b, c, d, e, f, g))
-> m (a, b, c, d, e, f, g) -> m (a, b, c, d, e, f, g)
forall a b. (a -> b) -> a -> b
$
      (,,,,,,)
        (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
<$> e -> aspec -> m a
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m a
simpleFreshConstrained e
e 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
<*> e -> bspec -> m b
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m b
simpleFreshConstrained e
e 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
<*> e -> cspec -> m c
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> cspec -> m c
simpleFreshConstrained e
e 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
<*> e -> dspec -> m d
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> dspec -> m d
simpleFreshConstrained e
e 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
<*> e -> espec -> m e
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> espec -> m e
simpleFreshConstrained e
e 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
<*> e -> fspec -> m f
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> fspec -> m f
simpleFreshConstrained e
e 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
<*> e -> gspec -> m g
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> gspec -> m g
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, MonadUnion m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec)
-> m (Union (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
    Union a
a1 <- e -> aspec -> m (Union a)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m (Union a)
freshConstrained e
err aspec
aspec
    Union b
b1 <- e -> bspec -> m (Union b)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m (Union b)
freshConstrained e
err bspec
bspec
    Union c
c1 <- e -> cspec -> m (Union c)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> cspec -> m (Union c)
freshConstrained e
err cspec
cspec
    Union d
d1 <- e -> dspec -> m (Union d)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> dspec -> m (Union d)
freshConstrained e
err dspec
dspec
    Union e
e1 <- e -> espec -> m (Union e)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> espec -> m (Union e)
freshConstrained e
err espec
espec
    Union f
f1 <- e -> fspec -> m (Union f)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> fspec -> m (Union f)
freshConstrained e
err fspec
fspec
    Union g
g1 <- e -> gspec -> m (Union g)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> gspec -> m (Union g)
freshConstrained e
err gspec
gspec
    Union h
h1 <- e -> hspec -> m (Union h)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> hspec -> m (Union h)
freshConstrained e
err hspec
hspec
    Union (a, b, c, d, e, f, g, h)
-> m (Union (a, b, c, d, e, f, g, h))
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union (a, b, c, d, e, f, g, h)
 -> m (Union (a, b, c, d, e, f, g, h)))
-> Union (a, b, c, d, e, f, g, h)
-> m (Union (a, b, c, d, e, f, g, h))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- Union a
a1
      b
bx <- Union b
b1
      c
cx <- Union c
c1
      d
dx <- Union d
d1
      e
ex <- Union e
e1
      f
fx <- Union f
f1
      g
gx <- Union g
g1
      h
hx <- Union h
h1
      (a, b, c, d, e, f, g, h) -> Union (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
  ( 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, MonadUnion 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
    m (a, b, c, d, e, f, g, h) -> m (a, b, c, d, e, f, g, h)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (a, b, c, d, e, f, g, h) -> m (a, b, c, d, e, f, g, h))
-> m (a, b, c, d, e, f, g, h) -> m (a, b, c, d, e, f, g, h)
forall a b. (a -> b) -> a -> b
$
      (,,,,,,,)
        (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
<$> e -> aspec -> m a
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> aspec -> m a
simpleFreshConstrained e
e 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
<*> e -> bspec -> m b
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> bspec -> m b
simpleFreshConstrained e
e 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
<*> e -> cspec -> m c
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> cspec -> m c
simpleFreshConstrained e
e 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
<*> e -> dspec -> m d
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> dspec -> m d
simpleFreshConstrained e
e 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
<*> e -> espec -> m e
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> espec -> m e
simpleFreshConstrained e
e 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
<*> e -> fspec -> m f
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> fspec -> m f
simpleFreshConstrained e
e 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
<*> e -> gspec -> m g
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> gspec -> m g
simpleFreshConstrained e
e 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
<*> e -> hspec -> m h
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> hspec -> m h
simpleFreshConstrained e
e hspec
hspec

-- MaybeT
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, MonadUnion m) =>
e -> spec -> m (Union (MaybeT m a))
freshConstrained e
e spec
v = do
    Union (m (Maybe a))
x <- e -> spec -> m (Union (m (Maybe a)))
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> spec -> m (Union (m (Maybe a)))
freshConstrained e
e spec
v
    Union (MaybeT m a) -> m (Union (MaybeT m a))
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union (MaybeT m a) -> m (Union (MaybeT m a)))
-> Union (MaybeT m a) -> m (Union (MaybeT m a))
forall a b. (a -> b) -> a -> b
$ Union (MaybeT m a) -> Union (MaybeT m a)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union (MaybeT m a) -> Union (MaybeT m a))
-> (Union (m (Maybe a)) -> Union (MaybeT m a))
-> Union (m (Maybe a))
-> Union (MaybeT m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m (Maybe a) -> MaybeT m a)
-> Union (m (Maybe a)) -> Union (MaybeT m a)
forall a b. (a -> b) -> Union a -> Union 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 (Union (m (Maybe a)) -> Union (MaybeT m a))
-> Union (m (Maybe a)) -> Union (MaybeT m a)
forall a b. (a -> b) -> a -> b
$ Union (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, MonadUnion m) =>
e -> spec -> m (MaybeT m a)
simpleFreshConstrained e
e spec
v = m (MaybeT m a) -> m (MaybeT m a)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (MaybeT m a) -> m (MaybeT m a))
-> m (MaybeT m a) -> m (MaybeT m a)
forall a b. (a -> b) -> a -> b
$ 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
<$> e -> spec -> m (m (Maybe a))
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> spec -> m (m (Maybe 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, MonadUnion m) =>
e -> MaybeT m a -> m (MaybeT m a)
simpleFreshConstrained e
e (MaybeT m (Maybe a)
v) = m (MaybeT m a) -> m (MaybeT m a)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (MaybeT m a) -> m (MaybeT m a))
-> m (MaybeT m a) -> m (MaybeT m a)
forall a b. (a -> b) -> a -> b
$ 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
<$> e -> m (Maybe a) -> m (m (Maybe a))
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Maybe a) -> m (m (Maybe 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)

-- ExceptT
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, MonadUnion m) =>
e -> spec -> m (Union (ExceptT a m b))
freshConstrained e
e spec
v = do
    Union (m (Either a b))
x <- e -> spec -> m (Union (m (Either a b)))
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> spec -> m (Union (m (Either a b)))
freshConstrained e
e spec
v
    Union (ExceptT a m b) -> m (Union (ExceptT a m b))
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Union (ExceptT a m b) -> m (Union (ExceptT a m b)))
-> Union (ExceptT a m b) -> m (Union (ExceptT a m b))
forall a b. (a -> b) -> a -> b
$ Union (ExceptT a m b) -> Union (ExceptT a m b)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union (ExceptT a m b) -> Union (ExceptT a m b))
-> (Union (m (Either a b)) -> Union (ExceptT a m b))
-> Union (m (Either a b))
-> Union (ExceptT a m b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m (Either a b) -> ExceptT a m b)
-> Union (m (Either a b)) -> Union (ExceptT a m b)
forall a b. (a -> b) -> Union a -> Union 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 (Union (m (Either a b)) -> Union (ExceptT a m b))
-> Union (m (Either a b)) -> Union (ExceptT a m b)
forall a b. (a -> b) -> a -> b
$ Union (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, MonadUnion m) =>
e -> spec -> m (ExceptT a m b)
simpleFreshConstrained e
e spec
v = m (ExceptT a m b) -> m (ExceptT a m b)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (ExceptT a m b) -> m (ExceptT a m b))
-> m (ExceptT a m b) -> m (ExceptT a m b)
forall a b. (a -> b) -> a -> b
$ 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
<$> e -> spec -> m (m (Either a b))
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> spec -> m (m (Either a b))
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, MonadUnion m) =>
e -> ExceptT e m a -> m (ExceptT e m a)
simpleFreshConstrained e
e (ExceptT m (Either e a)
v) = m (ExceptT e m a) -> m (ExceptT e m a)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (ExceptT e m a) -> m (ExceptT e m a))
-> m (ExceptT e m a) -> m (ExceptT e m a)
forall a b. (a -> b) -> a -> b
$ 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
<$> e -> m (Either e a) -> m (m (Either e a))
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Either e a) -> m (m (Either e 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)

-- Deriving

class GenSymConstrainedNoSpec a where
  freshConstrainedNoSpec ::
    ( MonadFresh m,
      MonadError e m,
      MonadUnion m
    ) =>
    e ->
    m (Union (a c))

instance GenSymConstrainedNoSpec U1 where
  freshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Union (U1 c))
freshConstrainedNoSpec e
_ = Union (U1 c) -> m (Union (U1 c))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Union (U1 c) -> m (Union (U1 c)))
-> Union (U1 c) -> m (Union (U1 c))
forall a b. (a -> b) -> a -> b
$ U1 c -> Union (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 (GenSymConstrained () c) => GenSymConstrainedNoSpec (K1 i c) where
  freshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Union (K1 i c c))
freshConstrainedNoSpec e
e = (c -> K1 i c c) -> Union c -> Union (K1 i c c)
forall a b. (a -> b) -> Union a -> Union 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 (Union c -> Union (K1 i c c))
-> m (Union c) -> m (Union (K1 i c c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> () -> m (Union c)
forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m (Union a)
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> () -> m (Union c)
freshConstrained e
e ()

instance (GenSymConstrainedNoSpec a) => GenSymConstrainedNoSpec (M1 i c a) where
  freshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Union (M1 i c a c))
freshConstrainedNoSpec e
e = (a c -> M1 i c a c) -> Union (a c) -> Union (M1 i c a c)
forall a b. (a -> b) -> Union a -> Union 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 (Union (a c) -> Union (M1 i c a c))
-> m (Union (a c)) -> m (Union (M1 i c a c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> m (Union (a c))
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> m (Union (a c))
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Union (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,
      MonadUnion m
    ) =>
    e ->
    m (Union ((a :+: b) c))
  freshConstrainedNoSpec :: forall (m :: * -> *) c e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Union ((:+:) a b c))
freshConstrainedNoSpec e
e = 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 ()
    Union (a c)
l :: Union (a c) <- e -> m (Union (a c))
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> m (Union (a c))
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Union (a c))
freshConstrainedNoSpec e
e
    Union (b c)
r :: Union (b c) <- e -> m (Union (b c))
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> m (Union (a c))
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Union (b c))
freshConstrainedNoSpec e
e
    Union ((:+:) a b c) -> m (Union ((:+:) a b c))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Union ((:+:) a b c) -> m (Union ((:+:) a b c)))
-> Union ((:+:) a b c) -> m (Union ((:+:) a b c))
forall a b. (a -> b) -> a -> b
$ SymBool
-> Union ((:+:) a b c)
-> Union ((:+:) a b c)
-> Union ((:+:) a b c)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond ((a c -> (:+:) a b c) -> Union (a c) -> Union ((:+:) a b c)
forall a b. (a -> b) -> Union a -> Union 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 Union (a c)
l) ((b c -> (:+:) a b c) -> Union (b c) -> Union ((:+:) a b c)
forall a b. (a -> b) -> Union a -> Union 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 Union (b c)
r)

instance
  (GenSymConstrainedNoSpec a, GenSymConstrainedNoSpec b) =>
  GenSymConstrainedNoSpec (a :*: b)
  where
  freshConstrainedNoSpec ::
    forall m c e.
    ( MonadFresh m,
      MonadError e m,
      MonadUnion m
    ) =>
    e ->
    m (Union ((a :*: b) c))
  freshConstrainedNoSpec :: forall (m :: * -> *) c e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Union ((:*:) a b c))
freshConstrainedNoSpec e
e = do
    Union (a c)
l :: Union (a c) <- e -> m (Union (a c))
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> m (Union (a c))
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Union (a c))
freshConstrainedNoSpec e
e
    Union (b c)
r :: Union (b c) <- e -> m (Union (b c))
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> m (Union (a c))
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Union (b c))
freshConstrainedNoSpec e
e
    Union ((:*:) a b c) -> m (Union ((:*:) a b c))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Union ((:*:) a b c) -> m (Union ((:*:) a b c)))
-> Union ((:*:) a b c) -> m (Union ((:*:) a b c))
forall a b. (a -> b) -> a -> b
$ do
      a c
l1 <- Union (a c)
l
      b c
r1 <- Union (b c)
r
      (:*:) a b c -> Union ((:*:) a b c)
forall a. a -> Union a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:*:) a b c -> Union ((:*:) a b c))
-> (:*:) a b c -> Union ((:*:) 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

-- | We cannot provide DerivingVia style derivation for 'GenSymConstrained', while you can
-- use this 'freshConstrained' implementation to implement 'GenSymConstrained' for your own types.
--
-- This 'freshConstrained' implementation is for the types that does not need any specification.
-- It will generate product types by generating each fields with @()@ as specification,
-- and generate all possible values for a sum type.
--
-- __Note:__ __Never__ use on recursive types.
derivedFreshConstrainedNoSpec ::
  forall a m e.
  ( Generic a,
    GenSymConstrainedNoSpec (Rep a),
    Mergeable a,
    MonadFresh m,
    MonadError e m,
    MonadUnion m
  ) =>
  e ->
  () ->
  m (Union a)
derivedFreshConstrainedNoSpec :: forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a,
 MonadFresh m, MonadError e m, MonadUnion m) =>
e -> () -> m (Union a)
derivedFreshConstrainedNoSpec e
e ()
_ = m (Union a) -> m (Union a)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (Union a) -> m (Union a)) -> m (Union a) -> m (Union a)
forall a b. (a -> b) -> a -> b
$ (Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union a -> Union a)
-> (Union (Rep a Any) -> Union a) -> Union (Rep a Any) -> Union a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rep a Any -> a) -> Union (Rep a Any) -> Union a
forall a b. (a -> b) -> Union a -> Union 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) (Union (Rep a Any) -> Union a)
-> m (Union (Rep a Any)) -> m (Union a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> m (Union (Rep a Any))
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> m (Union (a c))
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Union (Rep a c))
freshConstrainedNoSpec e
e

class GenSymSimpleConstrainedNoSpec a where
  simpleFreshConstrainedNoSpec ::
    ( MonadFresh m,
      MonadError e m,
      MonadUnion m
    ) =>
    e ->
    m (a c)

instance GenSymSimpleConstrainedNoSpec U1 where
  simpleFreshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (U1 c)
simpleFreshConstrainedNoSpec e
_ = 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 (GenSymSimpleConstrained () c) => GenSymSimpleConstrainedNoSpec (K1 i c) where
  simpleFreshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (K1 i c c)
simpleFreshConstrainedNoSpec e
e = 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
<$> e -> () -> m c
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> () -> m c
simpleFreshConstrained e
e ()

instance (GenSymSimpleConstrainedNoSpec a) => GenSymSimpleConstrainedNoSpec (M1 i c a) where
  simpleFreshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (M1 i c a c)
simpleFreshConstrainedNoSpec e
e = 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
<$> e -> m (a c)
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymSimpleConstrainedNoSpec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> m (a c)
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion 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, MonadUnion m) =>
e -> m ((:*:) a b c)
simpleFreshConstrainedNoSpec e
e = do
    a c
l :: a c <- e -> m (a c)
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymSimpleConstrainedNoSpec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> m (a c)
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (a c)
simpleFreshConstrainedNoSpec e
e
    b c
r :: b c <- e -> m (b c)
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymSimpleConstrainedNoSpec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> m (a c)
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (b c)
simpleFreshConstrainedNoSpec e
e
    (:*:) 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

-- | We cannot provide DerivingVia style derivation for 'GenSymSimpleConstrained', while
-- you can use this 'simpleFreshConstrained' implementation to implement 'GenSymSimpleConstrained' fo
-- your own types.
--
-- This 'simpleFreshConstrained' implementation is for the types that does not need any specification.
-- It will generate product types by generating each fields with () as specification.
-- It will not work on sum types.
--
-- __Note:__ __Never__ use on recursive types.
derivedSimpleFreshConstrainedNoSpec ::
  forall a m e.
  ( Generic a,
    GenSymSimpleConstrainedNoSpec (Rep a),
    MonadFresh m,
    MonadError e m,
    MonadUnion m,
    Mergeable a
  ) =>
  e ->
  () ->
  m a
derivedSimpleFreshConstrainedNoSpec :: forall a (m :: * -> *) e.
(Generic a, GenSymSimpleConstrainedNoSpec (Rep a), MonadFresh m,
 MonadError e m, MonadUnion m, Mergeable a) =>
e -> () -> m a
derivedSimpleFreshConstrainedNoSpec e
e ()
_ = 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
$ (m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> (m (Rep a Any) -> m a) -> m (Rep a Any) -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rep a Any -> a) -> m (Rep a Any) -> m a
forall a b. (a -> b) -> m a -> m 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) (m (Rep a Any) -> m a) -> m (Rep a Any) -> m a
forall a b. (a -> b) -> a -> b
$ e -> m (Rep a Any)
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymSimpleConstrainedNoSpec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> m (a c)
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> m (Rep a c)
simpleFreshConstrainedNoSpec e
e

class GenSymConstrainedSameShape a where
  simpleFreshConstrainedSameShape ::
    ( MonadFresh m,
      MonadError e m,
      MonadUnion m
    ) =>
    e ->
    a c ->
    m (a c)

instance GenSymConstrainedSameShape U1 where
  simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> U1 c -> m (U1 c)
simpleFreshConstrainedSameShape e
_ 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 (GenSymSimpleConstrained c c) => GenSymConstrainedSameShape (K1 i c) where
  simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> K1 i c c -> m (K1 i c c)
simpleFreshConstrainedSameShape e
e (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
<$> e -> c -> m c
forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> spec -> m a
forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> c -> m c
simpleFreshConstrained e
e c
c

instance (GenSymConstrainedSameShape a) => GenSymConstrainedSameShape (M1 i c a) where
  simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> M1 i c a c -> m (M1 i c a c)
simpleFreshConstrainedSameShape e
e (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
<$> e -> a c -> m (a c)
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> a c -> m (a c)
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion 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, MonadUnion m) =>
e -> (:+:) a b c -> m ((:+:) a b c)
simpleFreshConstrainedSameShape e
e (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
<$> e -> a c -> m (a c)
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> a c -> m (a c)
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e a c
a
  simpleFreshConstrainedSameShape e
e (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
<$> e -> b c -> m (b c)
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> a c -> m (a c)
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> b c -> m (b 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, MonadUnion m) =>
e -> (:*:) a b c -> m ((:*:) a b c)
simpleFreshConstrainedSameShape e
e (a c
a :*: b c
b) = do
    a c
l :: a c <- e -> a c -> m (a c)
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> a c -> m (a c)
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e a c
a
    b c
r :: b c <- e -> b c -> m (b c)
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> a c -> m (a c)
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> b c -> m (b c)
simpleFreshConstrainedSameShape e
e 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

-- | We cannot provide DerivingVia style derivation for 'GenSymSimpleConstrained', while
-- you can use this 'simpleFreshConstrained' implementation to implement 'GenSymSimpleConstrained' fo
-- your own types.
--
-- This 'simpleFreshConstrained' implementation is for the types that can be generated with
-- a reference value of the same type.
--
-- For sum types, it will generate the result with the same data constructor.
-- For product types, it will generate the result by generating each field with
-- the corresponding reference value.
--
-- __Note:__ __Can__ be used on recursive types.
derivedSimpleFreshConstrainedSameShape ::
  ( Generic a,
    GenSymConstrainedSameShape (Rep a),
    Mergeable a,
    MonadFresh m,
    MonadError e m,
    MonadUnion m
  ) =>
  e ->
  a ->
  m a
derivedSimpleFreshConstrainedSameShape :: forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedSameShape (Rep a), Mergeable a,
 MonadFresh m, MonadError e m, MonadUnion m) =>
e -> a -> m a
derivedSimpleFreshConstrainedSameShape e
e a
a = 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
$ (m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> (m (Rep a Any) -> m a) -> m (Rep a Any) -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rep a Any -> a) -> m (Rep a Any) -> m a
forall a b. (a -> b) -> m a -> m 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) (m (Rep a Any) -> m a) -> m (Rep a Any) -> m a
forall a b. (a -> b) -> a -> b
$ e -> Rep a Any -> m (Rep a Any)
forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
 MonadUnion m) =>
e -> a c -> m (a c)
forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, MonadUnion m) =>
e -> Rep a c -> m (Rep a c)
simpleFreshConstrainedSameShape e
e (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
a)