{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.GenSym
-- 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.Internal.Core.Data.Class.GenSym
  ( -- * Indices and identifiers for fresh symbolic value generation
    FreshIndex (..),

    -- * Monad for fresh symbolic value generation
    MonadFresh (..),
    nextFreshIndex,
    liftFresh,
    FreshT (FreshT, runFreshTFromIndex),
    Fresh,
    runFreshT,
    runFresh,
    mrgRunFreshT,
    freshString,

    -- * Symbolic value generation
    GenSym (..),
    GenSymSimple (..),
    genSym,
    genSymSimple,
    derivedNoSpecFresh,
    derivedNoSpecSimpleFresh,
    derivedSameShapeSimpleFresh,

    -- * Symbolic choices
    chooseFresh,
    chooseSimpleFresh,
    chooseUnionFresh,
    choose,
    chooseSimple,
    chooseUnion,

    -- * Some common GenSym specifications
    ListSpec (..),
    SimpleListSpec (..),
    EnumGenBound (..),
    EnumGenUpperBound (..),
  )
where

import Control.Monad.Except
  ( ExceptT (ExceptT),
    MonadError (catchError, throwError),
  )
import Control.Monad.Identity (Identity (runIdentity))
import Control.Monad.RWS.Class
  ( MonadRWS,
    MonadReader (ask, local),
    MonadState (get, put),
    MonadWriter (listen, pass, writer),
    asks,
    gets,
  )
import qualified Control.Monad.RWS.Lazy as RWSLazy
import qualified Control.Monad.RWS.Strict as RWSStrict
import Control.Monad.Reader (ReaderT (ReaderT))
import Control.Monad.Signatures (Catch)
import qualified Control.Monad.State.Lazy as StateLazy
import qualified Control.Monad.State.Strict as StateStrict
import Control.Monad.Trans.Class
  ( MonadTrans (lift),
  )
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import Data.Bifunctor (Bifunctor (first))
import qualified Data.ByteString as B
import Data.Int (Int16, Int32, Int64, Int8)
import Data.String (IsString (fromString))
import qualified Data.Text as T
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeNats (KnownNat, type (<=))
import Generics.Deriving
  ( Generic (Rep, from, to),
    K1 (K1),
    M1 (M1),
    U1 (U1),
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import Grisette.Internal.Core.Control.Monad.UnionM (UnionM, isMerged, underlyingUnion)
import Grisette.Internal.Core.Data.Class.Mergeable
  ( Mergeable (rootStrategy),
    Mergeable1 (liftRootStrategy),
    Mergeable2 (liftRootStrategy2),
    MergingStrategy (SimpleStrategy),
    rootStrategy1,
    wrapStrategy,
  )
import Grisette.Internal.Core.Data.Class.SimpleMergeable
  ( SimpleMergeable (mrgIte),
    SimpleMergeable1 (liftMrgIte),
    UnionMergeable1 (mrgIfPropagatedStrategy, mrgIfWithStrategy),
    mrgIf,
  )
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (isym))
import Grisette.Internal.Core.Data.Class.TryMerge
  ( TryMerge (tryMergeWithStrategy),
    mrgSingle,
    tryMerge,
  )
import Grisette.Internal.Core.Data.Symbol (Identifier)
import Grisette.Internal.Core.Data.Union (Union (UnionIf, UnionSingle))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.GeneralFun (type (-->))
import Grisette.Internal.SymPrim.Prim.Term
  ( LinkedRep,
    SupportedPrim,
  )
import Grisette.Internal.SymPrim.SymBV
  ( SymIntN,
    SymWordN,
  )
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>))
import Grisette.Internal.SymPrim.SymInteger (SymInteger)
import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))
import Grisette.Internal.SymPrim.TabularFun (type (=->))

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> :set -XOverloadedStrings
-- >>> :set -XTypeApplications

-- | Index type used for 'GenSym'.
--
-- To generate fresh variables, a monadic stateful context will be maintained.
-- The index should be increased every time a new symbolic constant is
-- generated.
newtype FreshIndex = FreshIndex Int
  deriving (Int -> FreshIndex -> ShowS
[FreshIndex] -> ShowS
FreshIndex -> String
(Int -> FreshIndex -> ShowS)
-> (FreshIndex -> String)
-> ([FreshIndex] -> ShowS)
-> Show FreshIndex
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FreshIndex -> ShowS
showsPrec :: Int -> FreshIndex -> ShowS
$cshow :: FreshIndex -> String
show :: FreshIndex -> String
$cshowList :: [FreshIndex] -> ShowS
showList :: [FreshIndex] -> ShowS
Show)
  deriving (FreshIndex -> FreshIndex -> Bool
(FreshIndex -> FreshIndex -> Bool)
-> (FreshIndex -> FreshIndex -> Bool) -> Eq FreshIndex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FreshIndex -> FreshIndex -> Bool
== :: FreshIndex -> FreshIndex -> Bool
$c/= :: FreshIndex -> FreshIndex -> Bool
/= :: FreshIndex -> FreshIndex -> Bool
Eq, Eq FreshIndex
Eq FreshIndex =>
(FreshIndex -> FreshIndex -> Ordering)
-> (FreshIndex -> FreshIndex -> Bool)
-> (FreshIndex -> FreshIndex -> Bool)
-> (FreshIndex -> FreshIndex -> Bool)
-> (FreshIndex -> FreshIndex -> Bool)
-> (FreshIndex -> FreshIndex -> FreshIndex)
-> (FreshIndex -> FreshIndex -> FreshIndex)
-> Ord FreshIndex
FreshIndex -> FreshIndex -> Bool
FreshIndex -> FreshIndex -> Ordering
FreshIndex -> FreshIndex -> FreshIndex
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FreshIndex -> FreshIndex -> Ordering
compare :: FreshIndex -> FreshIndex -> Ordering
$c< :: FreshIndex -> FreshIndex -> Bool
< :: FreshIndex -> FreshIndex -> Bool
$c<= :: FreshIndex -> FreshIndex -> Bool
<= :: FreshIndex -> FreshIndex -> Bool
$c> :: FreshIndex -> FreshIndex -> Bool
> :: FreshIndex -> FreshIndex -> Bool
$c>= :: FreshIndex -> FreshIndex -> Bool
>= :: FreshIndex -> FreshIndex -> Bool
$cmax :: FreshIndex -> FreshIndex -> FreshIndex
max :: FreshIndex -> FreshIndex -> FreshIndex
$cmin :: FreshIndex -> FreshIndex -> FreshIndex
min :: FreshIndex -> FreshIndex -> FreshIndex
Ord, Integer -> FreshIndex
FreshIndex -> FreshIndex
FreshIndex -> FreshIndex -> FreshIndex
(FreshIndex -> FreshIndex -> FreshIndex)
-> (FreshIndex -> FreshIndex -> FreshIndex)
-> (FreshIndex -> FreshIndex -> FreshIndex)
-> (FreshIndex -> FreshIndex)
-> (FreshIndex -> FreshIndex)
-> (FreshIndex -> FreshIndex)
-> (Integer -> FreshIndex)
-> Num FreshIndex
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: FreshIndex -> FreshIndex -> FreshIndex
+ :: FreshIndex -> FreshIndex -> FreshIndex
$c- :: FreshIndex -> FreshIndex -> FreshIndex
- :: FreshIndex -> FreshIndex -> FreshIndex
$c* :: FreshIndex -> FreshIndex -> FreshIndex
* :: FreshIndex -> FreshIndex -> FreshIndex
$cnegate :: FreshIndex -> FreshIndex
negate :: FreshIndex -> FreshIndex
$cabs :: FreshIndex -> FreshIndex
abs :: FreshIndex -> FreshIndex
$csignum :: FreshIndex -> FreshIndex
signum :: FreshIndex -> FreshIndex
$cfromInteger :: Integer -> FreshIndex
fromInteger :: Integer -> FreshIndex
Num) via Int

instance Mergeable FreshIndex where
  rootStrategy :: MergingStrategy FreshIndex
rootStrategy = (SymBool -> FreshIndex -> FreshIndex -> FreshIndex)
-> MergingStrategy FreshIndex
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> FreshIndex -> FreshIndex -> FreshIndex)
 -> MergingStrategy FreshIndex)
-> (SymBool -> FreshIndex -> FreshIndex -> FreshIndex)
-> MergingStrategy FreshIndex
forall a b. (a -> b) -> a -> b
$ \SymBool
_ FreshIndex
t FreshIndex
f -> FreshIndex -> FreshIndex -> FreshIndex
forall a. Ord a => a -> a -> a
max FreshIndex
t FreshIndex
f

instance SimpleMergeable FreshIndex where
  mrgIte :: SymBool -> FreshIndex -> FreshIndex -> FreshIndex
mrgIte SymBool
_ = FreshIndex -> FreshIndex -> FreshIndex
forall a. Ord a => a -> a -> a
max

-- | Monad class for fresh symbolic value generation.
--
-- The monad should be a reader monad for the 'Identifier' and a state monad for
-- the 'FreshIndex'.
class (Monad m) => MonadFresh m where
  -- | Get the current index for fresh variable generation.
  getFreshIndex :: m FreshIndex

  -- | Set the current index for fresh variable generation.
  setFreshIndex :: FreshIndex -> m ()

  -- | Get the identifier.
  getIdentifier :: m Identifier

  -- | Change the identifier locally and use a new index from 0 locally.
  localIdentifier :: (Identifier -> Identifier) -> m a -> m a

-- | Get the next fresh index and increase the current index.
nextFreshIndex :: (MonadFresh m) => m FreshIndex
nextFreshIndex :: forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex = do
  FreshIndex
curr <- m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
  let new :: FreshIndex
new = FreshIndex
curr FreshIndex -> FreshIndex -> FreshIndex
forall a. Num a => a -> a -> a
+ FreshIndex
1
  FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
new
  FreshIndex -> m FreshIndex
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return FreshIndex
curr

-- | Lifts an @`Fresh` a@ into any `MonadFresh`.
liftFresh :: (MonadFresh m) => Fresh a -> m a
liftFresh :: forall (m :: * -> *) a. MonadFresh m => Fresh a -> m a
liftFresh (FreshT Identifier -> FreshIndex -> Identity (a, FreshIndex)
f) = do
  FreshIndex
index <- m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
  Identifier
ident <- m Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
  let (a
a, FreshIndex
newIdx) = Identity (a, FreshIndex) -> (a, FreshIndex)
forall a. Identity a -> a
runIdentity (Identity (a, FreshIndex) -> (a, FreshIndex))
-> Identity (a, FreshIndex) -> (a, FreshIndex)
forall a b. (a -> b) -> a -> b
$ Identifier -> FreshIndex -> Identity (a, FreshIndex)
f Identifier
ident FreshIndex
index
  FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
  a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

-- | Generate a fresh string with the given postfix.
--
-- >>> runFresh (freshString "b") "a" :: String
-- "a@0[b]"
freshString :: (MonadFresh m, IsString s) => String -> m s
freshString :: forall (m :: * -> *) s. (MonadFresh m, IsString s) => String -> m s
freshString String
postfix = do
  Identifier
ident <- m Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
  FreshIndex Int
index <- m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
nextFreshIndex
  s -> m s
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (s -> m s) -> s -> m s
forall a b. (a -> b) -> a -> b
$
    String -> s
forall a. IsString a => String -> a
fromString (String -> s) -> String -> s
forall a b. (a -> b) -> a -> b
$
      Identifier -> String
forall a. Show a => a -> String
show Identifier
ident String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"@" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
index String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"[" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
postfix String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"]"

-- | A symbolic generation monad transformer.
--
-- It is a reader monad transformer for an identifier and a state monad
-- transformer for indices.
--
-- Each time a fresh symbolic variable is generated, the index should be
-- increased.
newtype FreshT m a = FreshT
  { forall (m :: * -> *) a.
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex :: Identifier -> FreshIndex -> m (a, FreshIndex)
  }

instance
  (Mergeable a, Mergeable1 m) =>
  Mergeable (FreshT m a)
  where
  rootStrategy :: MergingStrategy (FreshT m a)
rootStrategy =
    MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex))
-> ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex))
-> MergingStrategy (FreshT m a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy
      (MergingStrategy (FreshIndex -> m (a, FreshIndex))
-> MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex))
forall a. MergingStrategy a -> MergingStrategy (Identifier -> a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (MergingStrategy (m (a, FreshIndex))
-> MergingStrategy (FreshIndex -> m (a, FreshIndex))
forall a. MergingStrategy a -> MergingStrategy (FreshIndex -> a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy MergingStrategy (m (a, FreshIndex))
forall a (u :: * -> *).
(Mergeable a, Mergeable1 u) =>
MergingStrategy (u a)
rootStrategy1))
      (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT
      FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex

instance (Mergeable1 m) => Mergeable1 (FreshT m) where
  liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (FreshT m a)
liftRootStrategy MergingStrategy a
m =
    MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex))
-> ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex))
-> MergingStrategy (FreshT m a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy
      ( MergingStrategy (FreshIndex -> m (a, FreshIndex))
-> MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex))
forall a. MergingStrategy a -> MergingStrategy (Identifier -> a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (MergingStrategy (FreshIndex -> m (a, FreshIndex))
 -> MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex)))
-> (MergingStrategy (a, FreshIndex)
    -> MergingStrategy (FreshIndex -> m (a, FreshIndex)))
-> MergingStrategy (a, FreshIndex)
-> MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MergingStrategy (m (a, FreshIndex))
-> MergingStrategy (FreshIndex -> m (a, FreshIndex))
forall a. MergingStrategy a -> MergingStrategy (FreshIndex -> a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (MergingStrategy (m (a, FreshIndex))
 -> MergingStrategy (FreshIndex -> m (a, FreshIndex)))
-> (MergingStrategy (a, FreshIndex)
    -> MergingStrategy (m (a, FreshIndex)))
-> MergingStrategy (a, FreshIndex)
-> MergingStrategy (FreshIndex -> m (a, FreshIndex))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MergingStrategy (a, FreshIndex)
-> MergingStrategy (m (a, FreshIndex))
forall a. MergingStrategy a -> MergingStrategy (m a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (MergingStrategy (a, FreshIndex)
 -> MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex)))
-> MergingStrategy (a, FreshIndex)
-> MergingStrategy (Identifier -> FreshIndex -> m (a, FreshIndex))
forall a b. (a -> b) -> a -> b
$
          MergingStrategy a
-> MergingStrategy FreshIndex -> MergingStrategy (a, FreshIndex)
forall a b.
MergingStrategy a -> MergingStrategy b -> MergingStrategy (a, b)
forall (u :: * -> * -> *) a b.
Mergeable2 u =>
MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
liftRootStrategy2 MergingStrategy a
m MergingStrategy FreshIndex
forall a. Mergeable a => MergingStrategy a
rootStrategy
      )
      (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT
      FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex

instance
  (UnionMergeable1 m, Mergeable a) =>
  SimpleMergeable (FreshT m a)
  where
  mrgIte :: SymBool -> FreshT m a -> FreshT m a -> FreshT m a
mrgIte = SymBool -> FreshT m a -> FreshT m a -> FreshT m a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf

instance
  (UnionMergeable1 m) =>
  SimpleMergeable1 (FreshT m)
  where
  liftMrgIte :: forall a.
(SymBool -> a -> a -> a)
-> SymBool -> FreshT m a -> FreshT m a -> FreshT m a
liftMrgIte SymBool -> a -> a -> a
m = MergingStrategy a
-> SymBool -> FreshT m a -> FreshT m a -> FreshT m a
forall a.
MergingStrategy a
-> SymBool -> FreshT m a -> FreshT m a -> FreshT m a
forall (u :: * -> *) a.
UnionMergeable1 u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy ((SymBool -> a -> a -> a) -> MergingStrategy a
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> a -> a -> a
m)

instance (TryMerge m) => TryMerge (FreshT m) where
  tryMergeWithStrategy :: forall a. MergingStrategy a -> FreshT m a -> FreshT m a
tryMergeWithStrategy MergingStrategy a
s (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
f) =
    (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
index ->
      MergingStrategy (a, FreshIndex)
-> m (a, FreshIndex) -> m (a, FreshIndex)
forall a. MergingStrategy a -> m a -> m a
forall (m :: * -> *) a.
TryMerge m =>
MergingStrategy a -> m a -> m a
tryMergeWithStrategy (MergingStrategy a
-> MergingStrategy FreshIndex -> MergingStrategy (a, FreshIndex)
forall a b.
MergingStrategy a -> MergingStrategy b -> MergingStrategy (a, b)
forall (u :: * -> * -> *) a b.
Mergeable2 u =>
MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
liftRootStrategy2 MergingStrategy a
s MergingStrategy FreshIndex
forall a. Mergeable a => MergingStrategy a
rootStrategy) (m (a, FreshIndex) -> m (a, FreshIndex))
-> m (a, FreshIndex) -> m (a, FreshIndex)
forall a b. (a -> b) -> a -> b
$ Identifier -> FreshIndex -> m (a, FreshIndex)
f Identifier
ident FreshIndex
index

instance
  (UnionMergeable1 m) =>
  UnionMergeable1 (FreshT m)
  where
  mrgIfWithStrategy :: forall a.
MergingStrategy a
-> SymBool -> FreshT m a -> FreshT m a -> FreshT m a
mrgIfWithStrategy MergingStrategy a
s SymBool
cond (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
t) (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
f) =
    (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
index ->
      MergingStrategy (a, FreshIndex)
-> SymBool
-> m (a, FreshIndex)
-> m (a, FreshIndex)
-> m (a, FreshIndex)
forall a. MergingStrategy a -> SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
UnionMergeable1 u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy
        (MergingStrategy a
-> MergingStrategy FreshIndex -> MergingStrategy (a, FreshIndex)
forall a b.
MergingStrategy a -> MergingStrategy b -> MergingStrategy (a, b)
forall (u :: * -> * -> *) a b.
Mergeable2 u =>
MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
liftRootStrategy2 MergingStrategy a
s MergingStrategy FreshIndex
forall a. Mergeable a => MergingStrategy a
rootStrategy)
        SymBool
cond
        (Identifier -> FreshIndex -> m (a, FreshIndex)
t Identifier
ident FreshIndex
index)
        (Identifier -> FreshIndex -> m (a, FreshIndex)
f Identifier
ident FreshIndex
index)
  mrgIfPropagatedStrategy :: forall a. SymBool -> FreshT m a -> FreshT m a -> FreshT m a
mrgIfPropagatedStrategy SymBool
cond (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
t) (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
f) =
    (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
index ->
      SymBool
-> m (a, FreshIndex) -> m (a, FreshIndex) -> m (a, FreshIndex)
forall a. SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
UnionMergeable1 u =>
SymBool -> u a -> u a -> u a
mrgIfPropagatedStrategy SymBool
cond (Identifier -> FreshIndex -> m (a, FreshIndex)
t Identifier
ident FreshIndex
index) (Identifier -> FreshIndex -> m (a, FreshIndex)
f Identifier
ident FreshIndex
index)

-- | Run the symbolic generation with the given identifier and 0 as the initial
-- index.
runFreshT :: (Monad m) => FreshT m a -> Identifier -> m a
runFreshT :: forall (m :: * -> *) a. Monad m => FreshT m a -> Identifier -> m a
runFreshT FreshT m a
m Identifier
ident = (a, FreshIndex) -> a
forall a b. (a, b) -> a
fst ((a, FreshIndex) -> a) -> m (a, FreshIndex) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex FreshT m a
m Identifier
ident (Int -> FreshIndex
FreshIndex Int
0)

mrgRunFreshT ::
  (Monad m, TryMerge m, Mergeable a) =>
  FreshT m a ->
  Identifier ->
  m a
mrgRunFreshT :: forall (m :: * -> *) a.
(Monad m, TryMerge m, Mergeable a) =>
FreshT m a -> Identifier -> m a
mrgRunFreshT FreshT m a
m Identifier
ident = m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ FreshT m a -> Identifier -> m a
forall (m :: * -> *) a. Monad m => FreshT m a -> Identifier -> m a
runFreshT FreshT m a
m Identifier
ident

instance (Functor f) => Functor (FreshT f) where
  fmap :: forall a b. (a -> b) -> FreshT f a -> FreshT f b
fmap a -> b
f (FreshT Identifier -> FreshIndex -> f (a, FreshIndex)
s) = (Identifier -> FreshIndex -> f (b, FreshIndex)) -> FreshT f b
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> f (b, FreshIndex)) -> FreshT f b)
-> (Identifier -> FreshIndex -> f (b, FreshIndex)) -> FreshT f b
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
idx -> (a -> b) -> (a, FreshIndex) -> (b, FreshIndex)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> b
f ((a, FreshIndex) -> (b, FreshIndex))
-> f (a, FreshIndex) -> f (b, FreshIndex)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Identifier -> FreshIndex -> f (a, FreshIndex)
s Identifier
ident FreshIndex
idx

instance (Applicative m, Monad m) => Applicative (FreshT m) where
  pure :: forall a. a -> FreshT m a
pure a
a = (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
_ FreshIndex
idx -> (a, FreshIndex) -> m (a, FreshIndex)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, FreshIndex
idx)
  FreshT Identifier -> FreshIndex -> m (a -> b, FreshIndex)
fs <*> :: forall a b. FreshT m (a -> b) -> FreshT m a -> FreshT m b
<*> FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
as = (Identifier -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b)
-> (Identifier -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
idx -> do
    (a -> b
f, FreshIndex
idx') <- Identifier -> FreshIndex -> m (a -> b, FreshIndex)
fs Identifier
ident FreshIndex
idx
    (a
a, FreshIndex
idx'') <- Identifier -> FreshIndex -> m (a, FreshIndex)
as Identifier
ident FreshIndex
idx'
    (b, FreshIndex) -> m (b, FreshIndex)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> b
f a
a, FreshIndex
idx'')

instance (Monad m) => Monad (FreshT m) where
  (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
s) >>= :: forall a b. FreshT m a -> (a -> FreshT m b) -> FreshT m b
>>= a -> FreshT m b
f = (Identifier -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b)
-> (Identifier -> FreshIndex -> m (b, FreshIndex)) -> FreshT m b
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
idx -> do
    (a
a, FreshIndex
idx') <- Identifier -> FreshIndex -> m (a, FreshIndex)
s Identifier
ident FreshIndex
idx
    FreshT m b -> Identifier -> FreshIndex -> m (b, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex (a -> FreshT m b
f a
a) Identifier
ident FreshIndex
idx'

instance MonadTrans FreshT where
  lift :: forall (m :: * -> *) a. Monad m => m a -> FreshT m a
lift m a
x = (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
_ FreshIndex
index -> (,FreshIndex
index) (a -> (a, FreshIndex)) -> m a -> m (a, FreshIndex)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
x

liftFreshTCache :: (Functor m) => Catch e m (a, FreshIndex) -> Catch e (FreshT m) a
liftFreshTCache :: forall (m :: * -> *) e a.
Functor m =>
Catch e m (a, FreshIndex) -> Catch e (FreshT m) a
liftFreshTCache Catch e m (a, FreshIndex)
catchE (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
m) e -> FreshT m a
h =
  (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
index -> Identifier -> FreshIndex -> m (a, FreshIndex)
m Identifier
ident FreshIndex
index Catch e m (a, FreshIndex)
`catchE` \e
e -> FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
forall (m :: * -> *) a.
FreshT m a -> Identifier -> FreshIndex -> m (a, FreshIndex)
runFreshTFromIndex (e -> FreshT m a
h e
e) Identifier
ident FreshIndex
index

instance (MonadError e m) => MonadError e (FreshT m) where
  throwError :: forall a. e -> FreshT m a
throwError = m a -> FreshT m a
forall (m :: * -> *) a. Monad m => m a -> FreshT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> FreshT m a) -> (e -> m a) -> e -> FreshT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> m a
forall a. e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
  catchError :: forall a. FreshT m a -> (e -> FreshT m a) -> FreshT m a
catchError = Catch e m (a, FreshIndex) -> Catch e (FreshT m) a
forall (m :: * -> *) e a.
Functor m =>
Catch e m (a, FreshIndex) -> Catch e (FreshT m) a
liftFreshTCache Catch e m (a, FreshIndex)
forall a. m a -> (e -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError

instance (MonadWriter w m) => MonadWriter w (FreshT m) where
  writer :: forall a. (a, w) -> FreshT m a
writer (a, w)
p = (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
_ FreshIndex
index -> (,FreshIndex
index) (a -> (a, FreshIndex)) -> m a -> m (a, FreshIndex)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a, w) -> m a
forall a. (a, w) -> m a
forall w (m :: * -> *) a. MonadWriter w m => (a, w) -> m a
writer (a, w)
p
  listen :: forall a. FreshT m a -> FreshT m (a, w)
listen (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
r) = (Identifier -> FreshIndex -> m ((a, w), FreshIndex))
-> FreshT m (a, w)
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m ((a, w), FreshIndex))
 -> FreshT m (a, w))
-> (Identifier -> FreshIndex -> m ((a, w), FreshIndex))
-> FreshT m (a, w)
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
index -> (\((a
a, FreshIndex
b), w
c) -> ((a
a, w
c), FreshIndex
b)) (((a, FreshIndex), w) -> ((a, w), FreshIndex))
-> m ((a, FreshIndex), w) -> m ((a, w), FreshIndex)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (a, FreshIndex) -> m ((a, FreshIndex), w)
forall a. m a -> m (a, w)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen (Identifier -> FreshIndex -> m (a, FreshIndex)
r Identifier
ident FreshIndex
index)
  pass :: forall a. FreshT m (a, w -> w) -> FreshT m a
pass (FreshT Identifier -> FreshIndex -> m ((a, w -> w), FreshIndex)
r) = (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
index -> m ((a, FreshIndex), w -> w) -> m (a, FreshIndex)
forall a. m (a, w -> w) -> m a
forall w (m :: * -> *) a. MonadWriter w m => m (a, w -> w) -> m a
pass (m ((a, FreshIndex), w -> w) -> m (a, FreshIndex))
-> m ((a, FreshIndex), w -> w) -> m (a, FreshIndex)
forall a b. (a -> b) -> a -> b
$ (\((a
a, w -> w
b), FreshIndex
c) -> ((a
a, FreshIndex
c), w -> w
b)) (((a, w -> w), FreshIndex) -> ((a, FreshIndex), w -> w))
-> m ((a, w -> w), FreshIndex) -> m ((a, FreshIndex), w -> w)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Identifier -> FreshIndex -> m ((a, w -> w), FreshIndex)
r Identifier
ident FreshIndex
index

instance (MonadState s m) => MonadState s (FreshT m) where
  get :: FreshT m s
get = (Identifier -> FreshIndex -> m (s, FreshIndex)) -> FreshT m s
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (s, FreshIndex)) -> FreshT m s)
-> (Identifier -> FreshIndex -> m (s, FreshIndex)) -> FreshT m s
forall a b. (a -> b) -> a -> b
$ \Identifier
_ FreshIndex
index -> (s -> (s, FreshIndex)) -> m (s, FreshIndex)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (,FreshIndex
index)
  put :: s -> FreshT m ()
put s
s = (Identifier -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ()
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ())
-> (Identifier -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ()
forall a b. (a -> b) -> a -> b
$ \Identifier
_ FreshIndex
index -> (,FreshIndex
index) (() -> ((), FreshIndex)) -> m () -> m ((), FreshIndex)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put s
s

instance (MonadReader r m) => MonadReader r (FreshT m) where
  local :: forall a. (r -> r) -> FreshT m a -> FreshT m a
local r -> r
t (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
r) = (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
index -> (r -> r) -> m (a, FreshIndex) -> m (a, FreshIndex)
forall a. (r -> r) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local r -> r
t (Identifier -> FreshIndex -> m (a, FreshIndex)
r Identifier
ident FreshIndex
index)
  ask :: FreshT m r
ask = (Identifier -> FreshIndex -> m (r, FreshIndex)) -> FreshT m r
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (r, FreshIndex)) -> FreshT m r)
-> (Identifier -> FreshIndex -> m (r, FreshIndex)) -> FreshT m r
forall a b. (a -> b) -> a -> b
$ \Identifier
_ FreshIndex
index -> (r -> (r, FreshIndex)) -> m (r, FreshIndex)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (,FreshIndex
index)

instance (MonadRWS r w s m) => MonadRWS r w s (FreshT m)

instance (MonadFresh m) => MonadFresh (ExceptT e m) where
  getFreshIndex :: ExceptT e m FreshIndex
getFreshIndex = m FreshIndex -> ExceptT e m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> ExceptT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
  setFreshIndex :: FreshIndex -> ExceptT e m ()
setFreshIndex FreshIndex
newIdx = m () -> ExceptT e m ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT e m ()) -> m () -> ExceptT e m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
  getIdentifier :: ExceptT e m Identifier
getIdentifier = m Identifier -> ExceptT e m Identifier
forall (m :: * -> *) a. Monad m => m a -> ExceptT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
  localIdentifier :: forall a.
(Identifier -> Identifier) -> ExceptT e m a -> ExceptT e m a
localIdentifier Identifier -> Identifier
f (ExceptT m (Either e a)
m) = m (Either e a) -> ExceptT e m a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (m (Either e a) -> ExceptT e m a)
-> m (Either e a) -> ExceptT e m a
forall a b. (a -> b) -> a -> b
$ (Identifier -> Identifier) -> m (Either e a) -> m (Either e a)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f m (Either e a)
m

instance (MonadFresh m, Monoid w) => MonadFresh (WriterLazy.WriterT w m) where
  getFreshIndex :: WriterT w m FreshIndex
getFreshIndex = m FreshIndex -> WriterT w m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
  setFreshIndex :: FreshIndex -> WriterT w m ()
setFreshIndex FreshIndex
newIdx = m () -> WriterT w m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT w m ()) -> m () -> WriterT w m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
  getIdentifier :: WriterT w m Identifier
getIdentifier = m Identifier -> WriterT w m Identifier
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
  localIdentifier :: forall a.
(Identifier -> Identifier) -> WriterT w m a -> WriterT w m a
localIdentifier Identifier -> Identifier
f (WriterLazy.WriterT m (a, w)
m) =
    m (a, w) -> WriterT w m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT (m (a, w) -> WriterT w m a) -> m (a, w) -> WriterT w m a
forall a b. (a -> b) -> a -> b
$ (Identifier -> Identifier) -> m (a, w) -> m (a, w)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f m (a, w)
m

instance (MonadFresh m, Monoid w) => MonadFresh (WriterStrict.WriterT w m) where
  getFreshIndex :: WriterT w m FreshIndex
getFreshIndex = m FreshIndex -> WriterT w m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
  setFreshIndex :: FreshIndex -> WriterT w m ()
setFreshIndex FreshIndex
newIdx = m () -> WriterT w m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT w m ()) -> m () -> WriterT w m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
  getIdentifier :: WriterT w m Identifier
getIdentifier = m Identifier -> WriterT w m Identifier
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
  localIdentifier :: forall a.
(Identifier -> Identifier) -> WriterT w m a -> WriterT w m a
localIdentifier Identifier -> Identifier
f (WriterStrict.WriterT m (a, w)
m) =
    m (a, w) -> WriterT w m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT (m (a, w) -> WriterT w m a) -> m (a, w) -> WriterT w m a
forall a b. (a -> b) -> a -> b
$ (Identifier -> Identifier) -> m (a, w) -> m (a, w)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f m (a, w)
m

instance (MonadFresh m) => MonadFresh (StateLazy.StateT s m) where
  getFreshIndex :: StateT s m FreshIndex
getFreshIndex = m FreshIndex -> StateT s m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
  setFreshIndex :: FreshIndex -> StateT s m ()
setFreshIndex FreshIndex
newIdx = m () -> StateT s m ()
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT s m ()) -> m () -> StateT s m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
  getIdentifier :: StateT s m Identifier
getIdentifier = m Identifier -> StateT s m Identifier
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
  localIdentifier :: forall a.
(Identifier -> Identifier) -> StateT s m a -> StateT s m a
localIdentifier Identifier -> Identifier
f (StateLazy.StateT s -> m (a, s)
m) =
    (s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateLazy.StateT ((s -> m (a, s)) -> StateT s m a)
-> (s -> m (a, s)) -> StateT s m a
forall a b. (a -> b) -> a -> b
$ \s
s -> (Identifier -> Identifier) -> m (a, s) -> m (a, s)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f (s -> m (a, s)
m s
s)

instance (MonadFresh m) => MonadFresh (StateStrict.StateT s m) where
  getFreshIndex :: StateT s m FreshIndex
getFreshIndex = m FreshIndex -> StateT s m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
  setFreshIndex :: FreshIndex -> StateT s m ()
setFreshIndex FreshIndex
newIdx = m () -> StateT s m ()
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT s m ()) -> m () -> StateT s m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
  getIdentifier :: StateT s m Identifier
getIdentifier = m Identifier -> StateT s m Identifier
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
  localIdentifier :: forall a.
(Identifier -> Identifier) -> StateT s m a -> StateT s m a
localIdentifier Identifier -> Identifier
f (StateStrict.StateT s -> m (a, s)
m) =
    (s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateStrict.StateT ((s -> m (a, s)) -> StateT s m a)
-> (s -> m (a, s)) -> StateT s m a
forall a b. (a -> b) -> a -> b
$ \s
s -> (Identifier -> Identifier) -> m (a, s) -> m (a, s)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f (s -> m (a, s)
m s
s)

instance (MonadFresh m) => MonadFresh (ReaderT r m) where
  getFreshIndex :: ReaderT r m FreshIndex
getFreshIndex = m FreshIndex -> ReaderT r m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
  setFreshIndex :: FreshIndex -> ReaderT r m ()
setFreshIndex FreshIndex
newIdx = m () -> ReaderT r m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
  getIdentifier :: ReaderT r m Identifier
getIdentifier = m Identifier -> ReaderT r m Identifier
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
  localIdentifier :: forall a.
(Identifier -> Identifier) -> ReaderT r m a -> ReaderT r m a
localIdentifier Identifier -> Identifier
f (ReaderT r -> m a
m) = (r -> m a) -> ReaderT r m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((r -> m a) -> ReaderT r m a) -> (r -> m a) -> ReaderT r m a
forall a b. (a -> b) -> a -> b
$ (Identifier -> Identifier) -> m a -> m a
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f (m a -> m a) -> (r -> m a) -> r -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> m a
m

instance (MonadFresh m, Monoid w) => MonadFresh (RWSLazy.RWST r w s m) where
  getFreshIndex :: RWST r w s m FreshIndex
getFreshIndex = m FreshIndex -> RWST r w s m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
  setFreshIndex :: FreshIndex -> RWST r w s m ()
setFreshIndex FreshIndex
newIdx = m () -> RWST r w s m ()
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> RWST r w s m ()) -> m () -> RWST r w s m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
  getIdentifier :: RWST r w s m Identifier
getIdentifier = m Identifier -> RWST r w s m Identifier
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
  localIdentifier :: forall a.
(Identifier -> Identifier) -> RWST r w s m a -> RWST r w s m a
localIdentifier Identifier -> Identifier
f (RWSLazy.RWST r -> s -> m (a, s, w)
m) =
    (r -> s -> m (a, s, w)) -> RWST r w s m a
forall r w s (m :: * -> *) a.
(r -> s -> m (a, s, w)) -> RWST r w s m a
RWSLazy.RWST ((r -> s -> m (a, s, w)) -> RWST r w s m a)
-> (r -> s -> m (a, s, w)) -> RWST r w s m a
forall a b. (a -> b) -> a -> b
$ \r
r s
s -> (Identifier -> Identifier) -> m (a, s, w) -> m (a, s, w)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f (r -> s -> m (a, s, w)
m r
r s
s)

instance (MonadFresh m, Monoid w) => MonadFresh (RWSStrict.RWST r w s m) where
  getFreshIndex :: RWST r w s m FreshIndex
getFreshIndex = m FreshIndex -> RWST r w s m FreshIndex
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m FreshIndex
forall (m :: * -> *). MonadFresh m => m FreshIndex
getFreshIndex
  setFreshIndex :: FreshIndex -> RWST r w s m ()
setFreshIndex FreshIndex
newIdx = m () -> RWST r w s m ()
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> RWST r w s m ()) -> m () -> RWST r w s m ()
forall a b. (a -> b) -> a -> b
$ FreshIndex -> m ()
forall (m :: * -> *). MonadFresh m => FreshIndex -> m ()
setFreshIndex FreshIndex
newIdx
  getIdentifier :: RWST r w s m Identifier
getIdentifier = m Identifier -> RWST r w s m Identifier
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Identifier
forall (m :: * -> *). MonadFresh m => m Identifier
getIdentifier
  localIdentifier :: forall a.
(Identifier -> Identifier) -> RWST r w s m a -> RWST r w s m a
localIdentifier Identifier -> Identifier
f (RWSStrict.RWST r -> s -> m (a, s, w)
m) =
    (r -> s -> m (a, s, w)) -> RWST r w s m a
forall r w s (m :: * -> *) a.
(r -> s -> m (a, s, w)) -> RWST r w s m a
RWSStrict.RWST ((r -> s -> m (a, s, w)) -> RWST r w s m a)
-> (r -> s -> m (a, s, w)) -> RWST r w s m a
forall a b. (a -> b) -> a -> b
$ \r
r s
s -> (Identifier -> Identifier) -> m (a, s, w) -> m (a, s, w)
forall a. (Identifier -> Identifier) -> m a -> m a
forall (m :: * -> *) a.
MonadFresh m =>
(Identifier -> Identifier) -> m a -> m a
localIdentifier Identifier -> Identifier
f (r -> s -> m (a, s, w)
m r
r s
s)

-- | 'FreshT' specialized with Identity.
type Fresh = FreshT Identity

-- | Run the symbolic generation with the given identifier and 0 as the initial
-- index.
runFresh :: Fresh a -> Identifier -> a
runFresh :: forall a. Fresh a -> Identifier -> a
runFresh Fresh a
m Identifier
ident = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> Identity a -> a
forall a b. (a -> b) -> a -> b
$ Fresh a -> Identifier -> Identity a
forall (m :: * -> *) a. Monad m => FreshT m a -> Identifier -> m a
runFreshT Fresh a
m Identifier
ident

instance (Monad m) => MonadFresh (FreshT m) where
  getFreshIndex :: FreshT m FreshIndex
getFreshIndex = (Identifier -> FreshIndex -> m (FreshIndex, FreshIndex))
-> FreshT m FreshIndex
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (FreshIndex, FreshIndex))
 -> FreshT m FreshIndex)
-> (Identifier -> FreshIndex -> m (FreshIndex, FreshIndex))
-> FreshT m FreshIndex
forall a b. (a -> b) -> a -> b
$ \Identifier
_ FreshIndex
idx -> (FreshIndex, FreshIndex) -> m (FreshIndex, FreshIndex)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FreshIndex
idx, FreshIndex
idx)
  setFreshIndex :: FreshIndex -> FreshT m ()
setFreshIndex FreshIndex
newIdx = (Identifier -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ()
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ())
-> (Identifier -> FreshIndex -> m ((), FreshIndex)) -> FreshT m ()
forall a b. (a -> b) -> a -> b
$ \Identifier
_ FreshIndex
_ -> ((), FreshIndex) -> m ((), FreshIndex)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((), FreshIndex
newIdx)
  getIdentifier :: FreshT m Identifier
getIdentifier = (Identifier -> FreshIndex -> m (Identifier, FreshIndex))
-> FreshT m Identifier
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (Identifier, FreshIndex))
 -> FreshT m Identifier)
-> (Identifier -> FreshIndex -> m (Identifier, FreshIndex))
-> FreshT m Identifier
forall a b. (a -> b) -> a -> b
$ ((Identifier, FreshIndex) -> m (Identifier, FreshIndex))
-> Identifier -> FreshIndex -> m (Identifier, FreshIndex)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Identifier, FreshIndex) -> m (Identifier, FreshIndex)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
  localIdentifier :: forall a. (Identifier -> Identifier) -> FreshT m a -> FreshT m a
localIdentifier Identifier -> Identifier
f (FreshT Identifier -> FreshIndex -> m (a, FreshIndex)
m) = (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall (m :: * -> *) a.
(Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
FreshT ((Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a)
-> (Identifier -> FreshIndex -> m (a, FreshIndex)) -> FreshT m a
forall a b. (a -> b) -> a -> b
$ \Identifier
ident FreshIndex
idx -> do
    let newIdent :: Identifier
newIdent = Identifier -> Identifier
f Identifier
ident
    (a
r, FreshIndex
_) <- Identifier -> FreshIndex -> m (a, FreshIndex)
m Identifier
newIdent FreshIndex
0
    (a, FreshIndex) -> m (a, FreshIndex)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
r, FreshIndex
idx)

-- | Class of types in which symbolic values can be generated with respect to
-- some specification.
--
-- The result will be wrapped in a union-like monad.
-- This ensures that we can generate those types with complex merging rules.
--
-- The uniqueness of symbolic constants is managed with the a monadic context.
-- 'Fresh' and 'FreshT' can be useful.
class (Mergeable a) => GenSym spec a where
  -- | Generate a symbolic value given some specification. Within a single
  -- `MonadFresh` context, calls to `fresh` would generate unique symbolic
  -- constants.
  --
  -- The following example generates a symbolic boolean. No specification is
  -- needed.
  --
  -- >>> runFresh (fresh ()) "a" :: UnionM SymBool
  -- {a@0}
  --
  -- The following example generates booleans, which cannot be merged into a
  -- single value with type 'Bool'. No specification is needed.
  --
  -- >>> runFresh (fresh ()) "a" :: UnionM Bool
  -- {If a@0 False True}
  --
  -- The following example generates @Maybe Bool@s.
  -- There are more than one symbolic constants introduced, and their uniqueness
  -- is ensured. No specification is needed.
  --
  -- >>> runFresh (fresh ()) "a" :: UnionM (Maybe Bool)
  -- {If a@0 Nothing (If a@1 (Just False) (Just True))}
  --
  -- The following example generates lists of symbolic booleans with length 1 to 2.
  --
  -- >>> runFresh (fresh (ListSpec 1 2 ())) "a" :: UnionM [SymBool]
  -- {If a@2 [a@1] [a@0,a@1]}
  --
  -- When multiple symbolic values are generated, there will not be any
  -- identifier collision
  --
  -- >>> runFresh (do; a <- fresh (); b <- fresh (); return (a, b)) "a" :: (UnionM SymBool, UnionM SymBool)
  -- ({a@0},{a@1})
  fresh ::
    (MonadFresh m) =>
    spec ->
    m (UnionM a)
  default fresh ::
    (GenSymSimple spec a) =>
    ( MonadFresh m
    ) =>
    spec ->
    m (UnionM a)
  fresh spec
spec = a -> UnionM a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a -> UnionM a) -> m a -> m (UnionM a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> spec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => spec -> m a
simpleFresh spec
spec

-- | Generate a symbolic variable wrapped in a Union without the monadic context.
-- A globally unique identifier should be supplied to ensure the uniqueness of
-- symbolic constants in the generated symbolic values.
--
-- >>> genSym (ListSpec 1 2 ()) "a" :: UnionM [SymBool]
-- {If a@2 [a@1] [a@0,a@1]}
genSym :: (GenSym spec a) => spec -> Identifier -> UnionM a
genSym :: forall spec a. GenSym spec a => spec -> Identifier -> UnionM a
genSym = Fresh (UnionM a) -> Identifier -> UnionM a
forall a. Fresh a -> Identifier -> a
runFresh (Fresh (UnionM a) -> Identifier -> UnionM a)
-> (spec -> Fresh (UnionM a)) -> spec -> Identifier -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. spec -> Fresh (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
fresh

-- | Class of types in which symbolic values can be generated with respect to some specification.
--
-- The result will __/not/__ be wrapped in a union-like monad.
--
-- The uniqueness of symbolic constants is managed with the a monadic context.
-- 'Fresh' and 'FreshT' can be useful.
class GenSymSimple spec a where
  -- | Generate a symbolic value given some specification. The uniqueness is ensured.
  --
  -- The following example generates a symbolic boolean. No specification is needed.
  --
  -- >>> runFresh (simpleFresh ()) "a" :: SymBool
  -- a@0
  --
  -- The following code generates list of symbolic boolean with length 2.
  -- As the length is fixed, we don't have to wrap the result in unions.
  --
  -- >>> runFresh (simpleFresh (SimpleListSpec 2 ())) "a" :: [SymBool]
  -- [a@0,a@1]
  simpleFresh ::
    ( MonadFresh m
    ) =>
    spec ->
    m a

-- | Generate a simple symbolic variable wrapped in a Union without the monadic context.
-- A globally unique identifier should be supplied to ensure the uniqueness of
-- symbolic constants in the generated symbolic values.
--
-- >>> genSymSimple (SimpleListSpec 2 ()) "a" :: [SymBool]
-- [a@0,a@1]
genSymSimple :: forall spec a. (GenSymSimple spec a) => spec -> Identifier -> a
genSymSimple :: forall spec a. GenSymSimple spec a => spec -> Identifier -> a
genSymSimple = Fresh a -> Identifier -> a
forall a. Fresh a -> Identifier -> a
runFresh (Fresh a -> Identifier -> a)
-> (spec -> Fresh a) -> spec -> Identifier -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. spec -> Fresh a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => spec -> m a
simpleFresh

class GenSymNoSpec a where
  freshNoSpec ::
    ( MonadFresh m
    ) =>
    m (UnionM (a c))

instance GenSymNoSpec U1 where
  freshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (UnionM (U1 c))
freshNoSpec = UnionM (U1 c) -> m (UnionM (U1 c))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (U1 c) -> m (UnionM (U1 c)))
-> UnionM (U1 c) -> m (UnionM (U1 c))
forall a b. (a -> b) -> a -> b
$ U1 c -> UnionM (U1 c)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle U1 c
forall k (p :: k). U1 p
U1

instance (GenSym () c) => GenSymNoSpec (K1 i c) where
  freshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (UnionM (K1 i c c))
freshNoSpec = (c -> K1 i c c) -> UnionM c -> UnionM (K1 i c c)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> K1 i c c
forall k i c (p :: k). c -> K1 i c p
K1 (UnionM c -> UnionM (K1 i c c))
-> m (UnionM c) -> m (UnionM (K1 i c c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => () -> m (UnionM c)
fresh ()

instance (GenSymNoSpec a) => GenSymNoSpec (M1 i c a) where
  freshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (UnionM (M1 i c a c))
freshNoSpec = (a c -> M1 i c a c) -> UnionM (a c) -> UnionM (M1 i c a c)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a c -> M1 i c a c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (UnionM (a c) -> UnionM (M1 i c a c))
-> m (UnionM (a c)) -> m (UnionM (M1 i c a c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (UnionM (a c))
forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
forall (m :: * -> *) c. MonadFresh m => m (UnionM (a c))
freshNoSpec

instance
  ( GenSymNoSpec a,
    GenSymNoSpec b,
    forall x. Mergeable (a x),
    forall x. Mergeable (b x)
  ) =>
  GenSymNoSpec (a :+: b)
  where
  freshNoSpec ::
    forall m c.
    ( MonadFresh m
    ) =>
    m (UnionM ((a :+: b) c))
  freshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (UnionM ((:+:) a b c))
freshNoSpec = do
    SymBool
cond :: bool <- () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m SymBool
simpleFresh ()
    UnionM (a c)
l :: UnionM (a c) <- m (UnionM (a c))
forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
forall (m :: * -> *) c. MonadFresh m => m (UnionM (a c))
freshNoSpec
    UnionM (b c)
r :: UnionM (b c) <- m (UnionM (b c))
forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
forall (m :: * -> *) c. MonadFresh m => m (UnionM (b c))
freshNoSpec
    UnionM ((:+:) a b c) -> m (UnionM ((:+:) a b c))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM ((:+:) a b c) -> m (UnionM ((:+:) a b c)))
-> UnionM ((:+:) a b c) -> m (UnionM ((:+:) a b c))
forall a b. (a -> b) -> a -> b
$ SymBool
-> UnionM ((:+:) a b c)
-> UnionM ((:+:) a b c)
-> UnionM ((:+:) a b c)
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond ((a c -> (:+:) a b c) -> UnionM (a c) -> UnionM ((:+:) a b c)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a c -> (:+:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 UnionM (a c)
l) ((b c -> (:+:) a b c) -> UnionM (b c) -> UnionM ((:+:) a b c)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b c -> (:+:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 UnionM (b c)
r)

instance
  (GenSymNoSpec a, GenSymNoSpec b) =>
  GenSymNoSpec (a :*: b)
  where
  freshNoSpec ::
    forall m c.
    ( MonadFresh m
    ) =>
    m (UnionM ((a :*: b) c))
  freshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (UnionM ((:*:) a b c))
freshNoSpec = do
    UnionM (a c)
l :: UnionM (a c) <- m (UnionM (a c))
forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
forall (m :: * -> *) c. MonadFresh m => m (UnionM (a c))
freshNoSpec
    UnionM (b c)
r :: UnionM (b c) <- m (UnionM (b c))
forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
forall (m :: * -> *) c. MonadFresh m => m (UnionM (b c))
freshNoSpec
    UnionM ((:*:) a b c) -> m (UnionM ((:*:) a b c))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM ((:*:) a b c) -> m (UnionM ((:*:) a b c)))
-> UnionM ((:*:) a b c) -> m (UnionM ((:*:) a b c))
forall a b. (a -> b) -> a -> b
$ do
      a c
l1 <- UnionM (a c)
l
      b c
r1 <- UnionM (b c)
r
      (:*:) a b c -> UnionM ((:*:) a b c)
forall a. a -> UnionM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:*:) a b c -> UnionM ((:*:) a b c))
-> (:*:) a b c -> UnionM ((:*:) a b c)
forall a b. (a -> b) -> a -> b
$ a c
l1 a c -> b c -> (:*:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b c
r1

-- | We cannot provide DerivingVia style derivation for 'GenSym', while you can
-- use this 'fresh' implementation to implement 'GenSym' for your own types.
--
-- This 'fresh' 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.
derivedNoSpecFresh ::
  forall a m.
  ( Generic a,
    GenSymNoSpec (Rep a),
    Mergeable a,
    MonadFresh m
  ) =>
  () ->
  m (UnionM a)
derivedNoSpecFresh :: forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh ()
_ = UnionM a -> UnionM a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (UnionM a -> UnionM a)
-> (UnionM (Rep a Any) -> UnionM a)
-> UnionM (Rep a Any)
-> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rep a Any -> a) -> UnionM (Rep a Any) -> UnionM a
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (UnionM (Rep a Any) -> UnionM a)
-> m (UnionM (Rep a Any)) -> m (UnionM a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (UnionM (Rep a Any))
forall (a :: * -> *) (m :: * -> *) c.
(GenSymNoSpec a, MonadFresh m) =>
m (UnionM (a c))
forall (m :: * -> *) c. MonadFresh m => m (UnionM (Rep a c))
freshNoSpec

class GenSymSimpleNoSpec a where
  simpleFreshNoSpec :: (MonadFresh m) => m (a c)

instance GenSymSimpleNoSpec U1 where
  simpleFreshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (U1 c)
simpleFreshNoSpec = U1 c -> m (U1 c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return U1 c
forall k (p :: k). U1 p
U1

instance (GenSymSimple () c) => GenSymSimpleNoSpec (K1 i c) where
  simpleFreshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (K1 i c c)
simpleFreshNoSpec = c -> K1 i c c
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c c) -> m c -> m (K1 i c c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m c
simpleFresh ()

instance (GenSymSimpleNoSpec a) => GenSymSimpleNoSpec (M1 i c a) where
  simpleFreshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m (M1 i c a c)
simpleFreshNoSpec = a c -> M1 i c a c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a c -> M1 i c a c) -> m (a c) -> m (M1 i c a c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (a c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSimpleNoSpec a, MonadFresh m) =>
m (a c)
forall (m :: * -> *) c. MonadFresh m => m (a c)
simpleFreshNoSpec

instance
  (GenSymSimpleNoSpec a, GenSymSimpleNoSpec b) =>
  GenSymSimpleNoSpec (a :*: b)
  where
  simpleFreshNoSpec :: forall (m :: * -> *) c. MonadFresh m => m ((:*:) a b c)
simpleFreshNoSpec = do
    a c
l :: a c <- m (a c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSimpleNoSpec a, MonadFresh m) =>
m (a c)
forall (m :: * -> *) c. MonadFresh m => m (a c)
simpleFreshNoSpec
    b c
r :: b c <- m (b c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSimpleNoSpec a, MonadFresh m) =>
m (a c)
forall (m :: * -> *) c. MonadFresh m => m (b c)
simpleFreshNoSpec
    (:*:) a b c -> m ((:*:) a b c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:*:) a b c -> m ((:*:) a b c)) -> (:*:) a b c -> m ((:*:) a b c)
forall a b. (a -> b) -> a -> b
$ a c
l a c -> b c -> (:*:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b c
r

-- | We cannot provide DerivingVia style derivation for 'GenSymSimple', while
-- you can use this 'simpleFresh' implementation to implement 'GenSymSimple' fo
-- your own types.
--
-- This 'simpleFresh' 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.
derivedNoSpecSimpleFresh ::
  forall a m.
  ( Generic a,
    GenSymSimpleNoSpec (Rep a),
    MonadFresh m
  ) =>
  () ->
  m a
derivedNoSpecSimpleFresh :: forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh ()
_ = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> m (Rep a Any) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Rep a Any)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSimpleNoSpec a, MonadFresh m) =>
m (a c)
forall (m :: * -> *) c. MonadFresh m => m (Rep a c)
simpleFreshNoSpec

class GenSymSameShape a where
  genSymSameShapeFresh ::
    ( MonadFresh m
    ) =>
    a c ->
    m (a c)

instance GenSymSameShape U1 where
  genSymSameShapeFresh :: forall (m :: * -> *) c. MonadFresh m => U1 c -> m (U1 c)
genSymSameShapeFresh U1 c
_ = U1 c -> m (U1 c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return U1 c
forall k (p :: k). U1 p
U1

instance (GenSymSimple c c) => GenSymSameShape (K1 i c) where
  genSymSameShapeFresh :: forall (m :: * -> *) c. MonadFresh m => K1 i c c -> m (K1 i c c)
genSymSameShapeFresh (K1 c
c) = c -> K1 i c c
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c c) -> m c -> m (K1 i c c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => c -> m c
simpleFresh c
c

instance (GenSymSameShape a) => GenSymSameShape (M1 i c a) where
  genSymSameShapeFresh :: forall (m :: * -> *) c.
MonadFresh m =>
M1 i c a c -> m (M1 i c a c)
genSymSameShapeFresh (M1 a c
a) = a c -> M1 i c a c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a c -> M1 i c a c) -> m (a c) -> m (M1 i c a c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a c -> m (a c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
forall (m :: * -> *) c. MonadFresh m => a c -> m (a c)
genSymSameShapeFresh a c
a

instance
  (GenSymSameShape a, GenSymSameShape b) =>
  GenSymSameShape (a :+: b)
  where
  genSymSameShapeFresh :: forall (m :: * -> *) c.
MonadFresh m =>
(:+:) a b c -> m ((:+:) a b c)
genSymSameShapeFresh (L1 a c
a) = a c -> (:+:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (a c -> (:+:) a b c) -> m (a c) -> m ((:+:) a b c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a c -> m (a c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
forall (m :: * -> *) c. MonadFresh m => a c -> m (a c)
genSymSameShapeFresh a c
a
  genSymSameShapeFresh (R1 b c
a) = b c -> (:+:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (b c -> (:+:) a b c) -> m (b c) -> m ((:+:) a b c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b c -> m (b c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
forall (m :: * -> *) c. MonadFresh m => b c -> m (b c)
genSymSameShapeFresh b c
a

instance
  (GenSymSameShape a, GenSymSameShape b) =>
  GenSymSameShape (a :*: b)
  where
  genSymSameShapeFresh :: forall (m :: * -> *) c.
MonadFresh m =>
(:*:) a b c -> m ((:*:) a b c)
genSymSameShapeFresh (a c
a :*: b c
b) = do
    a c
l :: a c <- a c -> m (a c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
forall (m :: * -> *) c. MonadFresh m => a c -> m (a c)
genSymSameShapeFresh a c
a
    b c
r :: b c <- b c -> m (b c)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
forall (m :: * -> *) c. MonadFresh m => b c -> m (b c)
genSymSameShapeFresh b c
b
    (:*:) a b c -> m ((:*:) a b c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:*:) a b c -> m ((:*:) a b c)) -> (:*:) a b c -> m ((:*:) a b c)
forall a b. (a -> b) -> a -> b
$ a c
l a c -> b c -> (:*:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b c
r

-- | We cannot provide DerivingVia style derivation for 'GenSymSimple', while
-- you can use this 'simpleFresh' implementation to implement 'GenSymSimple' fo
-- your own types.
--
-- This 'simpleFresh' 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.
derivedSameShapeSimpleFresh ::
  forall a m.
  ( Generic a,
    GenSymSameShape (Rep a),
    MonadFresh m
  ) =>
  a ->
  m a
derivedSameShapeSimpleFresh :: forall a (m :: * -> *).
(Generic a, GenSymSameShape (Rep a), MonadFresh m) =>
a -> m a
derivedSameShapeSimpleFresh a
a = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> m (Rep a Any) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rep a Any -> m (Rep a Any)
forall (a :: * -> *) (m :: * -> *) c.
(GenSymSameShape a, MonadFresh m) =>
a c -> m (a c)
forall (m :: * -> *) c. MonadFresh m => Rep a c -> m (Rep a c)
genSymSameShapeFresh (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
a)

-- | Symbolically chooses one of the provided values.
-- The procedure creates @n - 1@ fresh symbolic boolean variables every time it
-- is evaluated, and use these variables to conditionally select one of the @n@
-- provided expressions.
--
-- The result will be wrapped in a union-like monad, and also a monad
-- maintaining the 'MonadFresh' context.
--
-- >>> runFresh (chooseFresh [1,2,3]) "a" :: UnionM Integer
-- {If a@0 1 (If a@1 2 3)}
chooseFresh ::
  forall a m.
  ( Mergeable a,
    MonadFresh m
  ) =>
  [a] ->
  m (UnionM a)
chooseFresh :: forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh [a
x] = UnionM a -> m (UnionM a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM a -> m (UnionM a)) -> UnionM a -> m (UnionM a)
forall a b. (a -> b) -> a -> b
$ a -> UnionM a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
x
chooseFresh (a
r : [a]
rs) = do
  SymBool
b <- () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m SymBool
simpleFresh ()
  UnionM a
res <- [a] -> m (UnionM a)
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh [a]
rs
  UnionM a -> m (UnionM a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM a -> m (UnionM a)) -> UnionM a -> m (UnionM a)
forall a b. (a -> b) -> a -> b
$ SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
b (a -> UnionM a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
r) UnionM a
res
chooseFresh [] = String -> m (UnionM a)
forall a. HasCallStack => String -> a
error String
"chooseFresh expects at least one value"

-- | A wrapper for `chooseFresh` that executes the `MonadFresh` context.
-- A globally unique identifier should be supplied to ensure the uniqueness of
-- symbolic constants in the generated symbolic values.
choose ::
  forall a.
  ( Mergeable a
  ) =>
  [a] ->
  Identifier ->
  UnionM a
choose :: forall a. Mergeable a => [a] -> Identifier -> UnionM a
choose = Fresh (UnionM a) -> Identifier -> UnionM a
forall a. Fresh a -> Identifier -> a
runFresh (Fresh (UnionM a) -> Identifier -> UnionM a)
-> ([a] -> Fresh (UnionM a)) -> [a] -> Identifier -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Fresh (UnionM a)
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh

-- | Symbolically chooses one of the provided values.
-- The procedure creates @n - 1@ fresh symbolic boolean variables every time it is evaluated, and use
-- these variables to conditionally select one of the @n@ provided expressions.
--
-- The result will __/not/__ be wrapped in a union-like monad, but will be
-- wrapped in a monad maintaining the 'Fresh' context.
--
-- >>> import Data.Proxy
-- >>> runFresh (chooseSimpleFresh [ssym "b", ssym "c", ssym "d"]) "a" :: SymInteger
-- (ite a@0 b (ite a@1 c d))
chooseSimpleFresh ::
  forall a m.
  ( SimpleMergeable a,
    MonadFresh m
  ) =>
  [a] ->
  m a
chooseSimpleFresh :: forall a (m :: * -> *).
(SimpleMergeable a, MonadFresh m) =>
[a] -> m a
chooseSimpleFresh [a
x] = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
chooseSimpleFresh (a
r : [a]
rs) = do
  SymBool
b :: bool <- () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m SymBool
simpleFresh ()
  a
res <- [a] -> m a
forall a (m :: * -> *).
(SimpleMergeable a, MonadFresh m) =>
[a] -> m a
chooseSimpleFresh [a]
rs
  a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ SymBool -> a -> a -> a
forall a. SimpleMergeable a => SymBool -> a -> a -> a
mrgIte SymBool
b a
r a
res
chooseSimpleFresh [] = String -> m a
forall a. HasCallStack => String -> a
error String
"chooseSimpleFresh expects at least one value"

-- | A wrapper for `chooseSimpleFresh` that executes the `MonadFresh` context.
-- A globally unique identifier should be supplied to ensure the uniqueness of
-- symbolic constants in the generated symbolic values.
chooseSimple ::
  forall a.
  ( SimpleMergeable a
  ) =>
  [a] ->
  Identifier ->
  a
chooseSimple :: forall a. SimpleMergeable a => [a] -> Identifier -> a
chooseSimple = Fresh a -> Identifier -> a
forall a. Fresh a -> Identifier -> a
runFresh (Fresh a -> Identifier -> a)
-> ([a] -> Fresh a) -> [a] -> Identifier -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Fresh a
forall a (m :: * -> *).
(SimpleMergeable a, MonadFresh m) =>
[a] -> m a
chooseSimpleFresh

-- | Symbolically chooses one of the provided values wrapped in union-like
-- monads. The procedure creates @n - 1@ fresh symbolic boolean variables every
-- time it is evaluated, and use these variables to conditionally select one of
-- the @n@ provided expressions.
--
-- The result will be wrapped in a union-like monad, and also a monad
-- maintaining the 'Fresh' context.
--
-- >>> let a = runFresh (chooseFresh [1, 2]) "a" :: UnionM Integer
-- >>> let b = runFresh (chooseFresh [2, 3]) "b" :: UnionM Integer
-- >>> runFresh (chooseUnionFresh [a, b]) "c" :: UnionM Integer
-- {If (&& c@0 a@0) 1 (If (|| c@0 b@0) 2 3)}
chooseUnionFresh ::
  forall a m.
  ( Mergeable a,
    MonadFresh m
  ) =>
  [UnionM a] ->
  m (UnionM a)
chooseUnionFresh :: forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh [UnionM a
x] = UnionM a -> m (UnionM a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UnionM a
x
chooseUnionFresh (UnionM a
r : [UnionM a]
rs) = do
  SymBool
b <- () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m SymBool
simpleFresh ()
  UnionM a
res <- [UnionM a] -> m (UnionM a)
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh [UnionM a]
rs
  UnionM a -> m (UnionM a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM a -> m (UnionM a)) -> UnionM a -> m (UnionM a)
forall a b. (a -> b) -> a -> b
$ SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
b UnionM a
r UnionM a
res
chooseUnionFresh [] = String -> m (UnionM a)
forall a. HasCallStack => String -> a
error String
"chooseUnionFresh expects at least one value"

-- | A wrapper for `chooseUnionFresh` that executes the `MonadFresh` context.
-- A globally unique identifier should be supplied to ensure the uniqueness of
-- symbolic constants in the generated symbolic values.
chooseUnion ::
  forall a.
  ( Mergeable a
  ) =>
  [UnionM a] ->
  Identifier ->
  UnionM a
chooseUnion :: forall a. Mergeable a => [UnionM a] -> Identifier -> UnionM a
chooseUnion = Fresh (UnionM a) -> Identifier -> UnionM a
forall a. Fresh a -> Identifier -> a
runFresh (Fresh (UnionM a) -> Identifier -> UnionM a)
-> ([UnionM a] -> Fresh (UnionM a))
-> [UnionM a]
-> Identifier
-> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UnionM a] -> Fresh (UnionM a)
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh

#define CONCRETE_GENSYM_SAME_SHAPE(type) \
instance GenSym type type where fresh = return . mrgSingle

#define CONCRETE_GENSYMSIMPLE_SAME_SHAPE(type) \
instance GenSymSimple type type where simpleFresh = return

#define CONCRETE_GENSYM_SAME_SHAPE_BV(type) \
instance (KnownNat n, 1 <= n) => GenSym (type n) (type n) where fresh = return . mrgSingle

#define CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(type) \
instance (KnownNat n, 1 <= n) => GenSymSimple (type n) (type n) where simpleFresh = return

#if 1
CONCRETE_GENSYM_SAME_SHAPE(Bool)
CONCRETE_GENSYM_SAME_SHAPE(Integer)
CONCRETE_GENSYM_SAME_SHAPE(Char)
CONCRETE_GENSYM_SAME_SHAPE(Int)
CONCRETE_GENSYM_SAME_SHAPE(Int8)
CONCRETE_GENSYM_SAME_SHAPE(Int16)
CONCRETE_GENSYM_SAME_SHAPE(Int32)
CONCRETE_GENSYM_SAME_SHAPE(Int64)
CONCRETE_GENSYM_SAME_SHAPE(Word)
CONCRETE_GENSYM_SAME_SHAPE(Word8)
CONCRETE_GENSYM_SAME_SHAPE(Word16)
CONCRETE_GENSYM_SAME_SHAPE(Word32)
CONCRETE_GENSYM_SAME_SHAPE(Word64)
CONCRETE_GENSYM_SAME_SHAPE(B.ByteString)
CONCRETE_GENSYM_SAME_SHAPE(T.Text)
CONCRETE_GENSYM_SAME_SHAPE_BV(WordN)
CONCRETE_GENSYM_SAME_SHAPE_BV(IntN)

CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Bool)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Integer)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Char)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Int)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Int8)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Int16)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Int32)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Int64)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word8)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word16)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word32)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(Word64)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(B.ByteString)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE(T.Text)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(WordN)
CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(IntN)
#endif

-- Bool
instance GenSym () Bool where
  fresh :: forall (m :: * -> *). MonadFresh m => () -> m (UnionM Bool)
fresh = () -> m (UnionM Bool)
forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh

-- Enums

-- | Specification for enum values with upper bound (exclusive). The result would chosen from [0 .. upperbound].
--
-- >>> runFresh (fresh (EnumGenUpperBound @Integer 4)) "c" :: UnionM Integer
-- {If c@0 0 (If c@1 1 (If c@2 2 3))}
newtype EnumGenUpperBound a = EnumGenUpperBound a

instance (Enum v, Mergeable v) => GenSym (EnumGenUpperBound v) v where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
EnumGenUpperBound v -> m (UnionM v)
fresh (EnumGenUpperBound v
u) = [v] -> m (UnionM v)
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh (Int -> v
forall a. Enum a => Int -> a
toEnum (Int -> v) -> [Int] -> [v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0 .. v -> Int
forall a. Enum a => a -> Int
fromEnum v
u Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1])

-- | Specification for numbers with lower bound (inclusive) and upper bound (exclusive)
--
-- >>> runFresh (fresh (EnumGenBound @Integer 0 4)) "c" :: UnionM Integer
-- {If c@0 0 (If c@1 1 (If c@2 2 3))}
data EnumGenBound a = EnumGenBound a a

instance (Enum v, Mergeable v) => GenSym (EnumGenBound v) v where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
EnumGenBound v -> m (UnionM v)
fresh (EnumGenBound v
l v
u) = [v] -> m (UnionM v)
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh (Int -> v
forall a. Enum a => Int -> a
toEnum (Int -> v) -> [Int] -> [v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [v -> Int
forall a. Enum a => a -> Int
fromEnum v
l .. v -> Int
forall a. Enum a => a -> Int
fromEnum v
u Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1])

-- Either
instance
  ( GenSym aspec a,
    Mergeable a,
    GenSym bspec b,
    Mergeable b
  ) =>
  GenSym (Either aspec bspec) (Either a b)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
Either aspec bspec -> m (UnionM (Either a b))
fresh (Left aspec
aspec) = (UnionM (Either a b) -> UnionM (Either a b)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (UnionM (Either a b) -> UnionM (Either a b))
-> (UnionM a -> UnionM (Either a b))
-> UnionM a
-> UnionM (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Either a b) -> UnionM a -> UnionM (Either a b)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Either a b
forall a b. a -> Either a b
Left) (UnionM a -> UnionM (Either a b))
-> m (UnionM a) -> m (UnionM (Either a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
  fresh (Right bspec
bspec) = (UnionM (Either a b) -> UnionM (Either a b)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (UnionM (Either a b) -> UnionM (Either a b))
-> (UnionM b -> UnionM (Either a b))
-> UnionM b
-> UnionM (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Either a b) -> UnionM b -> UnionM (Either a b)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Either a b
forall a b. b -> Either a b
Right) (UnionM b -> UnionM (Either a b))
-> m (UnionM b) -> m (UnionM (Either a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec

instance
  ( GenSymSimple aspec a,
    GenSymSimple bspec b
  ) =>
  GenSymSimple (Either aspec bspec) (Either a b)
  where
  simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
Either aspec bspec -> m (Either a b)
simpleFresh (Left aspec
a) = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> m a -> m (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
a
  simpleFresh (Right bspec
b) = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> m b -> m (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
b

instance
  (GenSym () a, Mergeable a, GenSym () b, Mergeable b) =>
  GenSym () (Either a b)
  where
  fresh :: forall (m :: * -> *). MonadFresh m => () -> m (UnionM (Either a b))
fresh = () -> m (UnionM (Either a b))
forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh

instance
  ( GenSym aspec a,
    Mergeable a,
    GenSym bspec b,
    Mergeable b
  ) =>
  GenSym (aspec, bspec) (Either a b)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec) -> m (UnionM (Either a b))
fresh (aspec
aspec, bspec
bspec) = do
    UnionM a
l :: UnionM a <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
    UnionM b
r :: UnionM b <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
    [UnionM (Either a b)] -> m (UnionM (Either a b))
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh [a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> UnionM a -> UnionM (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnionM a
l, b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> UnionM b -> UnionM (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnionM b
r]

-- Maybe
instance
  {-# OVERLAPPING #-}
  (GenSym aspec a, Mergeable a) =>
  GenSym (Maybe aspec) (Maybe a)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
Maybe aspec -> m (UnionM (Maybe a))
fresh Maybe aspec
Nothing = UnionM (Maybe a) -> m (UnionM (Maybe a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (Maybe a) -> m (UnionM (Maybe a)))
-> UnionM (Maybe a) -> m (UnionM (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> UnionM (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Maybe a
forall a. Maybe a
Nothing
  fresh (Just aspec
aspec) = (UnionM (Maybe a) -> UnionM (Maybe a)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (UnionM (Maybe a) -> UnionM (Maybe a))
-> (UnionM a -> UnionM (Maybe a)) -> UnionM a -> UnionM (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe a) -> UnionM a -> UnionM (Maybe a)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Maybe a
forall a. a -> Maybe a
Just) (UnionM a -> UnionM (Maybe a))
-> m (UnionM a) -> m (UnionM (Maybe a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec

instance
  (GenSymSimple aspec a) =>
  GenSymSimple (Maybe aspec) (Maybe a)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => Maybe aspec -> m (Maybe a)
simpleFresh Maybe aspec
Nothing = Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
  simpleFresh (Just aspec
aspec) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> m a -> m (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec

instance
  {-# OVERLAPPABLE #-}
  (GenSym aspec a, Mergeable a) =>
  GenSym aspec (Maybe a)
  where
  fresh :: forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM (Maybe a))
fresh aspec
aspec = do
    SymBool
cond <- () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m SymBool
simpleFresh ()
    UnionM a
a :: UnionM a <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
    UnionM (Maybe a) -> m (UnionM (Maybe a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (Maybe a) -> m (UnionM (Maybe a)))
-> UnionM (Maybe a) -> m (UnionM (Maybe a))
forall a b. (a -> b) -> a -> b
$ SymBool -> UnionM (Maybe a) -> UnionM (Maybe a) -> UnionM (Maybe a)
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond (Maybe a -> UnionM (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Maybe a
forall a. Maybe a
Nothing) (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> UnionM a -> UnionM (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnionM a
a)

-- List
instance
  (GenSym () a, Mergeable a) =>
  GenSym Integer [a]
  where
  fresh :: forall (m :: * -> *). MonadFresh m => Integer -> m (UnionM [a])
fresh Integer
v = do
    [UnionM a]
l <- Integer -> m [UnionM a]
forall (m :: * -> *). MonadFresh m => Integer -> m [UnionM a]
gl Integer
v
    let xs :: [[UnionM a]]
xs = [[UnionM a]] -> [[UnionM a]]
forall a. [a] -> [a]
reverse ([[UnionM a]] -> [[UnionM a]]) -> [[UnionM a]] -> [[UnionM a]]
forall a b. (a -> b) -> a -> b
$ (UnionM a -> [UnionM a] -> [UnionM a])
-> [UnionM a] -> [UnionM a] -> [[UnionM a]]
forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr (:) [] [UnionM a]
l
    [UnionM [a]] -> m (UnionM [a])
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh ([UnionM [a]] -> m (UnionM [a])) -> [UnionM [a]] -> m (UnionM [a])
forall a b. (a -> b) -> a -> b
$ UnionM [a] -> UnionM [a]
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (UnionM [a] -> UnionM [a])
-> ([UnionM a] -> UnionM [a]) -> [UnionM a] -> UnionM [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UnionM a] -> UnionM [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([UnionM a] -> UnionM [a]) -> [[UnionM a]] -> [UnionM [a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[UnionM a]]
xs
    where
      gl :: (MonadFresh m) => Integer -> m [UnionM a]
      gl :: forall (m :: * -> *). MonadFresh m => Integer -> m [UnionM a]
gl Integer
v1
        | Integer
v1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 = [UnionM a] -> m [UnionM a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        | Bool
otherwise = do
            UnionM a
l <- () -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => () -> m (UnionM a)
fresh ()
            [UnionM a]
r <- Integer -> m [UnionM a]
forall (m :: * -> *). MonadFresh m => Integer -> m [UnionM a]
gl (Integer
v1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
            [UnionM a] -> m [UnionM a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UnionM a] -> m [UnionM a]) -> [UnionM a] -> m [UnionM a]
forall a b. (a -> b) -> a -> b
$ UnionM a
l UnionM a -> [UnionM a] -> [UnionM a]
forall a. a -> [a] -> [a]
: [UnionM a]
r

-- | Specification for list generation.
--
-- >>> runFresh (fresh (ListSpec 0 2 ())) "c" :: UnionM [SymBool]
-- {If c@2 [] (If c@3 [c@1] [c@0,c@1])}
--
-- >>> runFresh (fresh (ListSpec 0 2 (SimpleListSpec 1 ()))) "c" :: UnionM [[SymBool]]
-- {If c@2 [] (If c@3 [[c@1]] [[c@0],[c@1]])}
data ListSpec spec = ListSpec
  { -- | The minimum length of the generated lists
    forall spec. ListSpec spec -> Int
genListMinLength :: Int,
    -- | The maximum length of the generated lists
    forall spec. ListSpec spec -> Int
genListMaxLength :: Int,
    -- | Each element in the lists will be generated with the sub-specification
    forall spec. ListSpec spec -> spec
genListSubSpec :: spec
  }
  deriving (Int -> ListSpec spec -> ShowS
[ListSpec spec] -> ShowS
ListSpec spec -> String
(Int -> ListSpec spec -> ShowS)
-> (ListSpec spec -> String)
-> ([ListSpec spec] -> ShowS)
-> Show (ListSpec spec)
forall spec. Show spec => Int -> ListSpec spec -> ShowS
forall spec. Show spec => [ListSpec spec] -> ShowS
forall spec. Show spec => ListSpec spec -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall spec. Show spec => Int -> ListSpec spec -> ShowS
showsPrec :: Int -> ListSpec spec -> ShowS
$cshow :: forall spec. Show spec => ListSpec spec -> String
show :: ListSpec spec -> String
$cshowList :: forall spec. Show spec => [ListSpec spec] -> ShowS
showList :: [ListSpec spec] -> ShowS
Show)

instance
  (GenSym spec a, Mergeable a) =>
  GenSym (ListSpec spec) [a]
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
ListSpec spec -> m (UnionM [a])
fresh (ListSpec Int
minLen Int
maxLen spec
subSpec) =
    if Int
minLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
maxLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
minLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
maxLen
      then String -> m (UnionM [a])
forall a. HasCallStack => String -> a
error (String -> m (UnionM [a])) -> String -> m (UnionM [a])
forall a b. (a -> b) -> a -> b
$ String
"Bad lengths: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
minLen, Int
maxLen)
      else do
        [UnionM a]
l <- Int -> m [UnionM a]
forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl Int
maxLen
        let xs :: [[UnionM a]]
xs = Int -> [[UnionM a]] -> [[UnionM a]]
forall a. Int -> [a] -> [a]
drop Int
minLen ([[UnionM a]] -> [[UnionM a]]) -> [[UnionM a]] -> [[UnionM a]]
forall a b. (a -> b) -> a -> b
$ [[UnionM a]] -> [[UnionM a]]
forall a. [a] -> [a]
reverse ([[UnionM a]] -> [[UnionM a]]) -> [[UnionM a]] -> [[UnionM a]]
forall a b. (a -> b) -> a -> b
$ (UnionM a -> [UnionM a] -> [UnionM a])
-> [UnionM a] -> [UnionM a] -> [[UnionM a]]
forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr (:) [] [UnionM a]
l
        [UnionM [a]] -> m (UnionM [a])
forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh ([UnionM [a]] -> m (UnionM [a])) -> [UnionM [a]] -> m (UnionM [a])
forall a b. (a -> b) -> a -> b
$ UnionM [a] -> UnionM [a]
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (UnionM [a] -> UnionM [a])
-> ([UnionM a] -> UnionM [a]) -> [UnionM a] -> UnionM [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UnionM a] -> UnionM [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([UnionM a] -> UnionM [a]) -> [[UnionM a]] -> [UnionM [a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[UnionM a]]
xs
    where
      gl :: (MonadFresh m) => Int -> m [UnionM a]
      gl :: forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl Int
currLen
        | Int
currLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [UnionM a] -> m [UnionM a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        | Bool
otherwise = do
            UnionM a
l <- spec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
fresh spec
subSpec
            [UnionM a]
r <- Int -> m [UnionM a]
forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl (Int
currLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
            [UnionM a] -> m [UnionM a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UnionM a] -> m [UnionM a]) -> [UnionM a] -> m [UnionM a]
forall a b. (a -> b) -> a -> b
$ UnionM a
l UnionM a -> [UnionM a] -> [UnionM a]
forall a. a -> [a] -> [a]
: [UnionM a]
r

instance
  (GenSym a a, Mergeable a) =>
  GenSym [a] [a]
  where
  fresh :: forall (m :: * -> *). MonadFresh m => [a] -> m (UnionM [a])
fresh [a]
l = do
    [UnionM a]
r :: [UnionM a] <- (a -> m (UnionM a)) -> [a] -> m [UnionM a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => a -> m (UnionM a)
fresh [a]
l
    UnionM [a] -> m (UnionM [a])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM [a] -> m (UnionM [a])) -> UnionM [a] -> m (UnionM [a])
forall a b. (a -> b) -> a -> b
$ UnionM [a] -> UnionM [a]
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (UnionM [a] -> UnionM [a]) -> UnionM [a] -> UnionM [a]
forall a b. (a -> b) -> a -> b
$ [UnionM a] -> UnionM [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [UnionM a]
r

instance
  (GenSymSimple a a) =>
  GenSymSimple [a] [a]
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => [a] -> m [a]
simpleFresh = [a] -> m [a]
forall a (m :: * -> *).
(Generic a, GenSymSameShape (Rep a), MonadFresh m) =>
a -> m a
derivedSameShapeSimpleFresh

-- | Specification for list generation of a specific length.
--
-- >>> runFresh (simpleFresh (SimpleListSpec 2 ())) "c" :: [SymBool]
-- [c@0,c@1]
data SimpleListSpec spec = SimpleListSpec
  { -- | The length of the generated list
    forall spec. SimpleListSpec spec -> Int
genSimpleListLength :: Int,
    -- | Each element in the list will be generated with the sub-specification
    forall spec. SimpleListSpec spec -> spec
genSimpleListSubSpec :: spec
  }
  deriving (Int -> SimpleListSpec spec -> ShowS
[SimpleListSpec spec] -> ShowS
SimpleListSpec spec -> String
(Int -> SimpleListSpec spec -> ShowS)
-> (SimpleListSpec spec -> String)
-> ([SimpleListSpec spec] -> ShowS)
-> Show (SimpleListSpec spec)
forall spec. Show spec => Int -> SimpleListSpec spec -> ShowS
forall spec. Show spec => [SimpleListSpec spec] -> ShowS
forall spec. Show spec => SimpleListSpec spec -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall spec. Show spec => Int -> SimpleListSpec spec -> ShowS
showsPrec :: Int -> SimpleListSpec spec -> ShowS
$cshow :: forall spec. Show spec => SimpleListSpec spec -> String
show :: SimpleListSpec spec -> String
$cshowList :: forall spec. Show spec => [SimpleListSpec spec] -> ShowS
showList :: [SimpleListSpec spec] -> ShowS
Show)

instance
  (GenSym spec a, Mergeable a) =>
  GenSym (SimpleListSpec spec) [a]
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
SimpleListSpec spec -> m (UnionM [a])
fresh (SimpleListSpec Int
len spec
subSpec) =
    if Int
len Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
      then String -> m (UnionM [a])
forall a. HasCallStack => String -> a
error (String -> m (UnionM [a])) -> String -> m (UnionM [a])
forall a b. (a -> b) -> a -> b
$ String
"Bad lengths: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
len
      else do
        UnionM [a] -> UnionM [a]
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (UnionM [a] -> UnionM [a])
-> ([UnionM a] -> UnionM [a]) -> [UnionM a] -> UnionM [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UnionM a] -> UnionM [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([UnionM a] -> UnionM [a]) -> m [UnionM a] -> m (UnionM [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m [UnionM a]
forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl Int
len
    where
      gl :: (MonadFresh m) => Int -> m [UnionM a]
      gl :: forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl Int
currLen
        | Int
currLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [UnionM a] -> m [UnionM a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        | Bool
otherwise = do
            UnionM a
l <- spec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
fresh spec
subSpec
            [UnionM a]
r <- Int -> m [UnionM a]
forall (m :: * -> *). MonadFresh m => Int -> m [UnionM a]
gl (Int
currLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
            [UnionM a] -> m [UnionM a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UnionM a] -> m [UnionM a]) -> [UnionM a] -> m [UnionM a]
forall a b. (a -> b) -> a -> b
$ UnionM a
l UnionM a -> [UnionM a] -> [UnionM a]
forall a. a -> [a] -> [a]
: [UnionM a]
r

instance
  (GenSymSimple spec a) =>
  GenSymSimple (SimpleListSpec spec) [a]
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => SimpleListSpec spec -> m [a]
simpleFresh (SimpleListSpec Int
len spec
subSpec) =
    if Int
len Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
      then String -> m [a]
forall a. HasCallStack => String -> a
error (String -> m [a]) -> String -> m [a]
forall a b. (a -> b) -> a -> b
$ String
"Bad lengths: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
len
      else do
        Int -> m [a]
forall (m :: * -> *). MonadFresh m => Int -> m [a]
gl Int
len
    where
      gl :: (MonadFresh m) => Int -> m [a]
      gl :: forall (m :: * -> *). MonadFresh m => Int -> m [a]
gl Int
currLen
        | Int
currLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        | Bool
otherwise = do
            a
l <- spec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => spec -> m a
simpleFresh spec
subSpec
            [a]
r <- Int -> m [a]
forall (m :: * -> *). MonadFresh m => Int -> m [a]
gl (Int
currLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
            [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> m [a]) -> [a] -> m [a]
forall a b. (a -> b) -> a -> b
$ a
l a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
r

-- ()
instance GenSym () ()

instance GenSymSimple () () where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m ()
simpleFresh = () -> m ()
forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh

-- (,)
instance
  ( GenSym aspec a,
    Mergeable a,
    GenSym bspec b,
    Mergeable b
  ) =>
  GenSym (aspec, bspec) (a, b)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec) -> m (UnionM (a, b))
fresh (aspec
aspec, bspec
bspec) = do
    UnionM a
a1 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
    UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
    UnionM (a, b) -> m (UnionM (a, b))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b) -> m (UnionM (a, b)))
-> UnionM (a, b) -> m (UnionM (a, b))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      (a, b) -> UnionM (a, b)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a
ax, b
bx)

instance
  ( GenSymSimple aspec a,
    GenSymSimple bspec b
  ) =>
  GenSymSimple (aspec, bspec) (a, b)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => (aspec, bspec) -> m (a, b)
simpleFresh (aspec
aspec, bspec
bspec) = do
    (,)
      (a -> b -> (a, b)) -> m a -> m (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
      m (b -> (a, b)) -> m b -> m (a, b)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec

instance
  (GenSym () a, Mergeable a, GenSym () b, Mergeable b) =>
  GenSym () (a, b)
  where
  fresh :: forall (m :: * -> *). MonadFresh m => () -> m (UnionM (a, b))
fresh = () -> m (UnionM (a, b))
forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh

instance
  ( GenSymSimple () a,
    GenSymSimple () b
  ) =>
  GenSymSimple () (a, b)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m (a, b)
simpleFresh = () -> m (a, b)
forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh

-- (,,)
instance
  ( GenSym aspec a,
    Mergeable a,
    GenSym bspec b,
    Mergeable b,
    GenSym cspec c,
    Mergeable c
  ) =>
  GenSym (aspec, bspec, cspec) (a, b, c)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec) -> m (UnionM (a, b, c))
fresh (aspec
aspec, bspec
bspec, cspec
cspec) = do
    UnionM a
a1 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
    UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
    UnionM c
c1 <- cspec -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => cspec -> m (UnionM c)
fresh cspec
cspec
    UnionM (a, b, c) -> m (UnionM (a, b, c))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b, c) -> m (UnionM (a, b, c)))
-> UnionM (a, b, c) -> m (UnionM (a, b, c))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      c
cx <- UnionM c
c1
      (a, b, c) -> UnionM (a, b, c)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a
ax, b
bx, c
cx)

instance
  ( GenSymSimple aspec a,
    GenSymSimple bspec b,
    GenSymSimple cspec c
  ) =>
  GenSymSimple (aspec, bspec, cspec) (a, b, c)
  where
  simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec) -> m (a, b, c)
simpleFresh (aspec
aspec, bspec
bspec, cspec
cspec) = do
    (,,)
      (a -> b -> c -> (a, b, c)) -> m a -> m (b -> c -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
      m (b -> c -> (a, b, c)) -> m b -> m (c -> (a, b, c))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec
      m (c -> (a, b, c)) -> m c -> m (a, b, c)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> cspec -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => cspec -> m c
simpleFresh cspec
cspec

instance
  ( GenSym () a,
    Mergeable a,
    GenSym () b,
    Mergeable b,
    GenSym () c,
    Mergeable c
  ) =>
  GenSym () (a, b, c)
  where
  fresh :: forall (m :: * -> *). MonadFresh m => () -> m (UnionM (a, b, c))
fresh = () -> m (UnionM (a, b, c))
forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh

instance
  ( GenSymSimple () a,
    GenSymSimple () b,
    GenSymSimple () c
  ) =>
  GenSymSimple () (a, b, c)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m (a, b, c)
simpleFresh = () -> m (a, b, c)
forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh

-- (,,,)
instance
  ( GenSym aspec a,
    Mergeable a,
    GenSym bspec b,
    Mergeable b,
    GenSym cspec c,
    Mergeable c,
    GenSym dspec d,
    Mergeable d
  ) =>
  GenSym (aspec, bspec, cspec, dspec) (a, b, c, d)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec) -> m (UnionM (a, b, c, d))
fresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec) = do
    UnionM a
a1 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
    UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
    UnionM c
c1 <- cspec -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => cspec -> m (UnionM c)
fresh cspec
cspec
    UnionM d
d1 <- dspec -> m (UnionM d)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => dspec -> m (UnionM d)
fresh dspec
dspec
    UnionM (a, b, c, d) -> m (UnionM (a, b, c, d))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b, c, d) -> m (UnionM (a, b, c, d)))
-> UnionM (a, b, c, d) -> m (UnionM (a, b, c, d))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      c
cx <- UnionM c
c1
      d
dx <- UnionM d
d1
      (a, b, c, d) -> UnionM (a, b, c, d)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a
ax, b
bx, c
cx, d
dx)

instance
  ( GenSymSimple aspec a,
    GenSymSimple bspec b,
    GenSymSimple cspec c,
    GenSymSimple dspec d
  ) =>
  GenSymSimple (aspec, bspec, cspec, dspec) (a, b, c, d)
  where
  simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec) -> m (a, b, c, d)
simpleFresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec) = do
    (,,,)
      (a -> b -> c -> d -> (a, b, c, d))
-> m a -> m (b -> c -> d -> (a, b, c, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
      m (b -> c -> d -> (a, b, c, d))
-> m b -> m (c -> d -> (a, b, c, d))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec
      m (c -> d -> (a, b, c, d)) -> m c -> m (d -> (a, b, c, d))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> cspec -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => cspec -> m c
simpleFresh cspec
cspec
      m (d -> (a, b, c, d)) -> m d -> m (a, b, c, d)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> dspec -> m d
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => dspec -> m d
simpleFresh dspec
dspec

instance
  ( GenSym () a,
    Mergeable a,
    GenSym () b,
    Mergeable b,
    GenSym () c,
    Mergeable c,
    GenSym () d,
    Mergeable d
  ) =>
  GenSym () (a, b, c, d)
  where
  fresh :: forall (m :: * -> *). MonadFresh m => () -> m (UnionM (a, b, c, d))
fresh = () -> m (UnionM (a, b, c, d))
forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh

instance
  ( GenSymSimple () a,
    GenSymSimple () b,
    GenSymSimple () c,
    GenSymSimple () d
  ) =>
  GenSymSimple () (a, b, c, d)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m (a, b, c, d)
simpleFresh = () -> m (a, b, c, d)
forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh

-- (,,,,)
instance
  ( GenSym aspec a,
    Mergeable a,
    GenSym bspec b,
    Mergeable b,
    GenSym cspec c,
    Mergeable c,
    GenSym dspec d,
    Mergeable d,
    GenSym espec e,
    Mergeable e
  ) =>
  GenSym (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec) -> m (UnionM (a, b, c, d, e))
fresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec) = do
    UnionM a
a1 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
    UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
    UnionM c
c1 <- cspec -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => cspec -> m (UnionM c)
fresh cspec
cspec
    UnionM d
d1 <- dspec -> m (UnionM d)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => dspec -> m (UnionM d)
fresh dspec
dspec
    UnionM e
e1 <- espec -> m (UnionM e)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => espec -> m (UnionM e)
fresh espec
espec
    UnionM (a, b, c, d, e) -> m (UnionM (a, b, c, d, e))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b, c, d, e) -> m (UnionM (a, b, c, d, e)))
-> UnionM (a, b, c, d, e) -> m (UnionM (a, b, c, d, e))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      c
cx <- UnionM c
c1
      d
dx <- UnionM d
d1
      e
ex <- UnionM e
e1
      (a, b, c, d, e) -> UnionM (a, b, c, d, e)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex)

instance
  ( GenSymSimple aspec a,
    GenSymSimple bspec b,
    GenSymSimple cspec c,
    GenSymSimple dspec d,
    GenSymSimple espec e
  ) =>
  GenSymSimple (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)
  where
  simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec) -> m (a, b, c, d, e)
simpleFresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec) = do
    (,,,,)
      (a -> b -> c -> d -> e -> (a, b, c, d, e))
-> m a -> m (b -> c -> d -> e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
      m (b -> c -> d -> e -> (a, b, c, d, e))
-> m b -> m (c -> d -> e -> (a, b, c, d, e))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec
      m (c -> d -> e -> (a, b, c, d, e))
-> m c -> m (d -> e -> (a, b, c, d, e))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> cspec -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => cspec -> m c
simpleFresh cspec
cspec
      m (d -> e -> (a, b, c, d, e)) -> m d -> m (e -> (a, b, c, d, e))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> dspec -> m d
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => dspec -> m d
simpleFresh dspec
dspec
      m (e -> (a, b, c, d, e)) -> m e -> m (a, b, c, d, e)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> espec -> m e
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => espec -> m e
simpleFresh espec
espec

instance
  ( GenSym () a,
    Mergeable a,
    GenSym () b,
    Mergeable b,
    GenSym () c,
    Mergeable c,
    GenSym () d,
    Mergeable d,
    GenSym () e,
    Mergeable e
  ) =>
  GenSym () (a, b, c, d, e)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
() -> m (UnionM (a, b, c, d, e))
fresh = () -> m (UnionM (a, b, c, d, e))
forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh

instance
  ( GenSymSimple () a,
    GenSymSimple () b,
    GenSymSimple () c,
    GenSymSimple () d,
    GenSymSimple () e
  ) =>
  GenSymSimple () (a, b, c, d, e)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m (a, b, c, d, e)
simpleFresh = () -> m (a, b, c, d, e)
forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh

-- (,,,,,)
instance
  ( GenSym aspec a,
    Mergeable a,
    GenSym bspec b,
    Mergeable b,
    GenSym cspec c,
    Mergeable c,
    GenSym dspec d,
    Mergeable d,
    GenSym espec e,
    Mergeable e,
    GenSym fspec f,
    Mergeable f
  ) =>
  GenSym (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec, fspec)
-> m (UnionM (a, b, c, d, e, f))
fresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec) = do
    UnionM a
a1 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
    UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
    UnionM c
c1 <- cspec -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => cspec -> m (UnionM c)
fresh cspec
cspec
    UnionM d
d1 <- dspec -> m (UnionM d)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => dspec -> m (UnionM d)
fresh dspec
dspec
    UnionM e
e1 <- espec -> m (UnionM e)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => espec -> m (UnionM e)
fresh espec
espec
    UnionM f
f1 <- fspec -> m (UnionM f)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => fspec -> m (UnionM f)
fresh fspec
fspec
    UnionM (a, b, c, d, e, f) -> m (UnionM (a, b, c, d, e, f))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b, c, d, e, f) -> m (UnionM (a, b, c, d, e, f)))
-> UnionM (a, b, c, d, e, f) -> m (UnionM (a, b, c, d, e, f))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      c
cx <- UnionM c
c1
      d
dx <- UnionM d
d1
      e
ex <- UnionM e
e1
      f
fx <- UnionM f
f1
      (a, b, c, d, e, f) -> UnionM (a, b, c, d, e, f)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex, f
fx)

instance
  ( GenSymSimple aspec a,
    GenSymSimple bspec b,
    GenSymSimple cspec c,
    GenSymSimple dspec d,
    GenSymSimple espec e,
    GenSymSimple fspec f
  ) =>
  GenSymSimple (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)
  where
  simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec, fspec) -> m (a, b, c, d, e, f)
simpleFresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec) = do
    (,,,,,)
      (a -> b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> m a -> m (b -> c -> d -> e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
      m (b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> m b -> m (c -> d -> e -> f -> (a, b, c, d, e, f))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec
      m (c -> d -> e -> f -> (a, b, c, d, e, f))
-> m c -> m (d -> e -> f -> (a, b, c, d, e, f))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> cspec -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => cspec -> m c
simpleFresh cspec
cspec
      m (d -> e -> f -> (a, b, c, d, e, f))
-> m d -> m (e -> f -> (a, b, c, d, e, f))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> dspec -> m d
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => dspec -> m d
simpleFresh dspec
dspec
      m (e -> f -> (a, b, c, d, e, f))
-> m e -> m (f -> (a, b, c, d, e, f))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> espec -> m e
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => espec -> m e
simpleFresh espec
espec
      m (f -> (a, b, c, d, e, f)) -> m f -> m (a, b, c, d, e, f)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> fspec -> m f
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => fspec -> m f
simpleFresh fspec
fspec

instance
  ( GenSym () a,
    Mergeable a,
    GenSym () b,
    Mergeable b,
    GenSym () c,
    Mergeable c,
    GenSym () d,
    Mergeable d,
    GenSym () e,
    Mergeable e,
    GenSym () f,
    Mergeable f
  ) =>
  GenSym () (a, b, c, d, e, f)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
() -> m (UnionM (a, b, c, d, e, f))
fresh = () -> m (UnionM (a, b, c, d, e, f))
forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh

instance
  ( GenSymSimple () a,
    GenSymSimple () b,
    GenSymSimple () c,
    GenSymSimple () d,
    GenSymSimple () e,
    GenSymSimple () f
  ) =>
  GenSymSimple () (a, b, c, d, e, f)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m (a, b, c, d, e, f)
simpleFresh = () -> m (a, b, c, d, e, f)
forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh

-- (,,,,,,)
instance
  ( GenSym aspec a,
    Mergeable a,
    GenSym bspec b,
    Mergeable b,
    GenSym cspec c,
    Mergeable c,
    GenSym dspec d,
    Mergeable d,
    GenSym espec e,
    Mergeable e,
    GenSym fspec f,
    Mergeable f,
    GenSym gspec g,
    Mergeable g
  ) =>
  GenSym (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec, fspec, gspec)
-> m (UnionM (a, b, c, d, e, f, g))
fresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec) = do
    UnionM a
a1 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
    UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
    UnionM c
c1 <- cspec -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => cspec -> m (UnionM c)
fresh cspec
cspec
    UnionM d
d1 <- dspec -> m (UnionM d)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => dspec -> m (UnionM d)
fresh dspec
dspec
    UnionM e
e1 <- espec -> m (UnionM e)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => espec -> m (UnionM e)
fresh espec
espec
    UnionM f
f1 <- fspec -> m (UnionM f)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => fspec -> m (UnionM f)
fresh fspec
fspec
    UnionM g
g1 <- gspec -> m (UnionM g)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => gspec -> m (UnionM g)
fresh gspec
gspec
    UnionM (a, b, c, d, e, f, g) -> m (UnionM (a, b, c, d, e, f, g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b, c, d, e, f, g) -> m (UnionM (a, b, c, d, e, f, g)))
-> UnionM (a, b, c, d, e, f, g) -> m (UnionM (a, b, c, d, e, f, g))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      c
cx <- UnionM c
c1
      d
dx <- UnionM d
d1
      e
ex <- UnionM e
e1
      f
fx <- UnionM f
f1
      g
gx <- UnionM g
g1
      (a, b, c, d, e, f, g) -> UnionM (a, b, c, d, e, f, g)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex, f
fx, g
gx)

instance
  ( GenSymSimple aspec a,
    GenSymSimple bspec b,
    GenSymSimple cspec c,
    GenSymSimple dspec d,
    GenSymSimple espec e,
    GenSymSimple fspec f,
    GenSymSimple gspec g
  ) =>
  GenSymSimple (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)
  where
  simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec, fspec, gspec)
-> m (a, b, c, d, e, f, g)
simpleFresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec) = do
    (,,,,,,)
      (a -> b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> m a -> m (b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
      m (b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> m b -> m (c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec
      m (c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> m c -> m (d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> cspec -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => cspec -> m c
simpleFresh cspec
cspec
      m (d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> m d -> m (e -> f -> g -> (a, b, c, d, e, f, g))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> dspec -> m d
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => dspec -> m d
simpleFresh dspec
dspec
      m (e -> f -> g -> (a, b, c, d, e, f, g))
-> m e -> m (f -> g -> (a, b, c, d, e, f, g))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> espec -> m e
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => espec -> m e
simpleFresh espec
espec
      m (f -> g -> (a, b, c, d, e, f, g))
-> m f -> m (g -> (a, b, c, d, e, f, g))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> fspec -> m f
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => fspec -> m f
simpleFresh fspec
fspec
      m (g -> (a, b, c, d, e, f, g)) -> m g -> m (a, b, c, d, e, f, g)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> gspec -> m g
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => gspec -> m g
simpleFresh gspec
gspec

instance
  ( GenSym () a,
    Mergeable a,
    GenSym () b,
    Mergeable b,
    GenSym () c,
    Mergeable c,
    GenSym () d,
    Mergeable d,
    GenSym () e,
    Mergeable e,
    GenSym () f,
    Mergeable f,
    GenSym () g,
    Mergeable g
  ) =>
  GenSym () (a, b, c, d, e, f, g)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
() -> m (UnionM (a, b, c, d, e, f, g))
fresh = () -> m (UnionM (a, b, c, d, e, f, g))
forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh

instance
  ( GenSymSimple () a,
    GenSymSimple () b,
    GenSymSimple () c,
    GenSymSimple () d,
    GenSymSimple () e,
    GenSymSimple () f,
    GenSymSimple () g
  ) =>
  GenSymSimple () (a, b, c, d, e, f, g)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => () -> m (a, b, c, d, e, f, g)
simpleFresh = () -> m (a, b, c, d, e, f, g)
forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh

-- (,,,,,,,)
instance
  ( GenSym aspec a,
    Mergeable a,
    GenSym bspec b,
    Mergeable b,
    GenSym cspec c,
    Mergeable c,
    GenSym dspec d,
    Mergeable d,
    GenSym espec e,
    Mergeable e,
    GenSym fspec f,
    Mergeable f,
    GenSym gspec g,
    Mergeable g,
    GenSym hspec h,
    Mergeable h
  ) =>
  GenSym (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec)
-> m (UnionM (a, b, c, d, e, f, g, h))
fresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec, hspec
hspec) = do
    UnionM a
a1 <- aspec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => aspec -> m (UnionM a)
fresh aspec
aspec
    UnionM b
b1 <- bspec -> m (UnionM b)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => bspec -> m (UnionM b)
fresh bspec
bspec
    UnionM c
c1 <- cspec -> m (UnionM c)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => cspec -> m (UnionM c)
fresh cspec
cspec
    UnionM d
d1 <- dspec -> m (UnionM d)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => dspec -> m (UnionM d)
fresh dspec
dspec
    UnionM e
e1 <- espec -> m (UnionM e)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => espec -> m (UnionM e)
fresh espec
espec
    UnionM f
f1 <- fspec -> m (UnionM f)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => fspec -> m (UnionM f)
fresh fspec
fspec
    UnionM g
g1 <- gspec -> m (UnionM g)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => gspec -> m (UnionM g)
fresh gspec
gspec
    UnionM h
h1 <- hspec -> m (UnionM h)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => hspec -> m (UnionM h)
fresh hspec
hspec
    UnionM (a, b, c, d, e, f, g, h)
-> m (UnionM (a, b, c, d, e, f, g, h))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (a, b, c, d, e, f, g, h)
 -> m (UnionM (a, b, c, d, e, f, g, h)))
-> UnionM (a, b, c, d, e, f, g, h)
-> m (UnionM (a, b, c, d, e, f, g, h))
forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      c
cx <- UnionM c
c1
      d
dx <- UnionM d
d1
      e
ex <- UnionM e
e1
      f
fx <- UnionM f
f1
      g
gx <- UnionM g
g1
      h
hx <- UnionM h
h1
      (a, b, c, d, e, f, g, h) -> UnionM (a, b, c, d, e, f, g, h)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex, f
fx, g
gx, h
hx)

instance
  ( GenSymSimple aspec a,
    GenSymSimple bspec b,
    GenSymSimple cspec c,
    GenSymSimple dspec d,
    GenSymSimple espec e,
    GenSymSimple fspec f,
    GenSymSimple gspec g,
    GenSymSimple hspec h
  ) =>
  GenSymSimple (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)
  where
  simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
(aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec)
-> m (a, b, c, d, e, f, g, h)
simpleFresh (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec, hspec
hspec) = do
    (,,,,,,,)
      (a -> b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> m a
-> m (b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> aspec -> m a
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => aspec -> m a
simpleFresh aspec
aspec
      m (b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> m b
-> m (c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> bspec -> m b
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => bspec -> m b
simpleFresh bspec
bspec
      m (c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> m c -> m (d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> cspec -> m c
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => cspec -> m c
simpleFresh cspec
cspec
      m (d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> m d -> m (e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> dspec -> m d
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => dspec -> m d
simpleFresh dspec
dspec
      m (e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> m e -> m (f -> g -> h -> (a, b, c, d, e, f, g, h))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> espec -> m e
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => espec -> m e
simpleFresh espec
espec
      m (f -> g -> h -> (a, b, c, d, e, f, g, h))
-> m f -> m (g -> h -> (a, b, c, d, e, f, g, h))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> fspec -> m f
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => fspec -> m f
simpleFresh fspec
fspec
      m (g -> h -> (a, b, c, d, e, f, g, h))
-> m g -> m (h -> (a, b, c, d, e, f, g, h))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> gspec -> m g
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => gspec -> m g
simpleFresh gspec
gspec
      m (h -> (a, b, c, d, e, f, g, h))
-> m h -> m (a, b, c, d, e, f, g, h)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> hspec -> m h
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => hspec -> m h
simpleFresh hspec
hspec

instance
  ( GenSym () a,
    Mergeable a,
    GenSym () b,
    Mergeable b,
    GenSym () c,
    Mergeable c,
    GenSym () d,
    Mergeable d,
    GenSym () e,
    Mergeable e,
    GenSym () f,
    Mergeable f,
    GenSym () g,
    Mergeable g,
    GenSym () h,
    Mergeable h
  ) =>
  GenSym () (a, b, c, d, e, f, g, h)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
() -> m (UnionM (a, b, c, d, e, f, g, h))
fresh = () -> m (UnionM (a, b, c, d, e, f, g, h))
forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh

instance
  ( GenSymSimple () a,
    GenSymSimple () b,
    GenSymSimple () c,
    GenSymSimple () d,
    GenSymSimple () e,
    GenSymSimple () f,
    GenSymSimple () g,
    GenSymSimple () h
  ) =>
  GenSymSimple () (a, b, c, d, e, f, g, h)
  where
  simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
() -> m (a, b, c, d, e, f, g, h)
simpleFresh = () -> m (a, b, c, d, e, f, g, h)
forall a (m :: * -> *).
(Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) =>
() -> m a
derivedNoSpecSimpleFresh

-- MaybeT
instance
  {-# OVERLAPPABLE #-}
  ( GenSym spec (m (Maybe a)),
    Mergeable1 m,
    Mergeable a
  ) =>
  GenSym spec (MaybeT m a)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
spec -> m (UnionM (MaybeT m a))
fresh spec
v = do
    UnionM (m (Maybe a))
x <- spec -> m (UnionM (m (Maybe a)))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *).
MonadFresh m =>
spec -> m (UnionM (m (Maybe a)))
fresh spec
v
    UnionM (MaybeT m a) -> m (UnionM (MaybeT m a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (MaybeT m a) -> m (UnionM (MaybeT m a)))
-> UnionM (MaybeT m a) -> m (UnionM (MaybeT m a))
forall a b. (a -> b) -> a -> b
$ UnionM (MaybeT m a) -> UnionM (MaybeT m a)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (UnionM (MaybeT m a) -> UnionM (MaybeT m a))
-> (UnionM (m (Maybe a)) -> UnionM (MaybeT m a))
-> UnionM (m (Maybe a))
-> UnionM (MaybeT m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m (Maybe a) -> MaybeT m a)
-> UnionM (m (Maybe a)) -> UnionM (MaybeT m a)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (UnionM (m (Maybe a)) -> UnionM (MaybeT m a))
-> UnionM (m (Maybe a)) -> UnionM (MaybeT m a)
forall a b. (a -> b) -> a -> b
$ UnionM (m (Maybe a))
x

instance
  {-# OVERLAPPABLE #-}
  ( GenSymSimple spec (m (Maybe a))
  ) =>
  GenSymSimple spec (MaybeT m a)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => spec -> m (MaybeT m a)
simpleFresh spec
v = m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe a) -> MaybeT m a) -> m (m (Maybe a)) -> m (MaybeT m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> spec -> m (m (Maybe a))
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => spec -> m (m (Maybe a))
simpleFresh spec
v

instance
  {-# OVERLAPPING #-}
  ( GenSymSimple (m (Maybe a)) (m (Maybe a))
  ) =>
  GenSymSimple (MaybeT m a) (MaybeT m a)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => MaybeT m a -> m (MaybeT m a)
simpleFresh (MaybeT m (Maybe a)
v) = m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe a) -> MaybeT m a) -> m (m (Maybe a)) -> m (MaybeT m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe a) -> m (m (Maybe a))
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *).
MonadFresh m =>
m (Maybe a) -> m (m (Maybe a))
simpleFresh m (Maybe a)
v

instance
  {-# OVERLAPPING #-}
  ( GenSymSimple (m (Maybe a)) (m (Maybe a)),
    Mergeable1 m,
    Mergeable a
  ) =>
  GenSym (MaybeT m a) (MaybeT m a)

-- ExceptT
instance
  {-# OVERLAPPABLE #-}
  ( GenSym spec (m (Either a b)),
    Mergeable1 m,
    Mergeable a,
    Mergeable b
  ) =>
  GenSym spec (ExceptT a m b)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
spec -> m (UnionM (ExceptT a m b))
fresh spec
v = do
    UnionM (m (Either a b))
x <- spec -> m (UnionM (m (Either a b)))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *).
MonadFresh m =>
spec -> m (UnionM (m (Either a b)))
fresh spec
v
    UnionM (ExceptT a m b) -> m (UnionM (ExceptT a m b))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (ExceptT a m b) -> m (UnionM (ExceptT a m b)))
-> UnionM (ExceptT a m b) -> m (UnionM (ExceptT a m b))
forall a b. (a -> b) -> a -> b
$ UnionM (ExceptT a m b) -> UnionM (ExceptT a m b)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (UnionM (ExceptT a m b) -> UnionM (ExceptT a m b))
-> (UnionM (m (Either a b)) -> UnionM (ExceptT a m b))
-> UnionM (m (Either a b))
-> UnionM (ExceptT a m b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m (Either a b) -> ExceptT a m b)
-> UnionM (m (Either a b)) -> UnionM (ExceptT a m b)
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m (Either a b) -> ExceptT a m b
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (UnionM (m (Either a b)) -> UnionM (ExceptT a m b))
-> UnionM (m (Either a b)) -> UnionM (ExceptT a m b)
forall a b. (a -> b) -> a -> b
$ UnionM (m (Either a b))
x

instance
  {-# OVERLAPPABLE #-}
  ( GenSymSimple spec (m (Either a b))
  ) =>
  GenSymSimple spec (ExceptT a m b)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => spec -> m (ExceptT a m b)
simpleFresh spec
v = m (Either a b) -> ExceptT a m b
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (m (Either a b) -> ExceptT a m b)
-> m (m (Either a b)) -> m (ExceptT a m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> spec -> m (m (Either a b))
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => spec -> m (m (Either a b))
simpleFresh spec
v

instance
  {-# OVERLAPPING #-}
  ( GenSymSimple (m (Either e a)) (m (Either e a))
  ) =>
  GenSymSimple (ExceptT e m a) (ExceptT e m a)
  where
  simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
ExceptT e m a -> m (ExceptT e m a)
simpleFresh (ExceptT m (Either e a)
v) = m (Either e a) -> ExceptT e m a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (m (Either e a) -> ExceptT e m a)
-> m (m (Either e a)) -> m (ExceptT e m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Either e a) -> m (m (Either e a))
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *).
MonadFresh m =>
m (Either e a) -> m (m (Either e a))
simpleFresh m (Either e a)
v

instance
  {-# OVERLAPPING #-}
  ( GenSymSimple (m (Either e a)) (m (Either e a)),
    Mergeable1 m,
    Mergeable e,
    Mergeable a
  ) =>
  GenSym (ExceptT e m a) (ExceptT e m a)

#define GENSYM_SIMPLE(symtype) \
instance GenSym symtype symtype
#define GENSYM_SIMPLE_SIMPLE(symtype) \
instance GenSymSimple symtype symtype where \
  simpleFresh _ = simpleFresh ()
#define GENSYM_UNIT_SIMPLE(symtype) \
instance GenSym () symtype where \
  fresh _ = mrgSingle <$> simpleFresh ()
#define GENSYM_UNIT_SIMPLE_SIMPLE(symtype) \
instance GenSymSimple () symtype where \
  simpleFresh _ = do; \
    ident <- getIdentifier; \
    FreshIndex index <- nextFreshIndex; \
    return $ isym ident index

#define GENSYM_BV(symtype) \
instance (KnownNat n, 1 <= n) => GenSym (symtype n) (symtype n)
#define GENSYM_SIMPLE_BV(symtype) \
instance (KnownNat n, 1 <= n) => GenSymSimple (symtype n) (symtype n) where \
  simpleFresh _ = simpleFresh ()
#define GENSYM_UNIT_BV(symtype) \
instance (KnownNat n, 1 <= n) => GenSym () (symtype n) where \
  fresh _ = mrgSingle <$> simpleFresh ()
#define GENSYM_UNIT_SIMPLE_BV(symtype) \
instance (KnownNat n, 1 <= n) => GenSymSimple () (symtype n) where \
  simpleFresh _ = do; \
    ident <- getIdentifier; \
    FreshIndex index <- nextFreshIndex; \
    return $ isym ident index

#define GENSYM_FUN(cop, op) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
  GenSym (op sa sb) (op sa sb)
#define GENSYM_SIMPLE_FUN(cop, op) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
  GenSymSimple (op sa sb) (op sa sb) where \
  simpleFresh _ = simpleFresh ()
#define GENSYM_UNIT_FUN(cop, op) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
  GenSym () (op sa sb) where \
  fresh _ = mrgSingle <$> simpleFresh ()
#define GENSYM_UNIT_SIMPLE_FUN(cop, op) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
  GenSymSimple () (op sa sb) where \
  simpleFresh _ = do; \
    ident <- getIdentifier; \
    FreshIndex index <- nextFreshIndex; \
    return $ isym ident index

#if 1
GENSYM_SIMPLE(SymBool)
GENSYM_SIMPLE_SIMPLE(SymBool)
GENSYM_UNIT_SIMPLE(SymBool)
GENSYM_UNIT_SIMPLE_SIMPLE(SymBool)
GENSYM_SIMPLE(SymInteger)
GENSYM_SIMPLE_SIMPLE(SymInteger)
GENSYM_UNIT_SIMPLE(SymInteger)
GENSYM_UNIT_SIMPLE_SIMPLE(SymInteger)

GENSYM_BV(SymIntN)
GENSYM_SIMPLE_BV(SymIntN)
GENSYM_UNIT_BV(SymIntN)
GENSYM_UNIT_SIMPLE_BV(SymIntN)
GENSYM_BV(SymWordN)
GENSYM_SIMPLE_BV(SymWordN)
GENSYM_UNIT_BV(SymWordN)
GENSYM_UNIT_SIMPLE_BV(SymWordN)

GENSYM_FUN((=->), (=~>))
GENSYM_SIMPLE_FUN((=->), (=~>))
GENSYM_UNIT_FUN((=->), (=~>))
GENSYM_UNIT_SIMPLE_FUN((=->), (=~>))
GENSYM_FUN((-->), (-~>))
GENSYM_SIMPLE_FUN((-->), (-~>))
GENSYM_UNIT_FUN((-->), (-~>))
GENSYM_UNIT_SIMPLE_FUN((-->), (-~>))
#endif

instance (GenSym spec a, Mergeable a) => GenSym spec (UnionM a)

instance (GenSym spec a) => GenSymSimple spec (UnionM a) where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
simpleFresh spec
spec = do
    UnionM a
res <- spec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
fresh spec
spec
    if Bool -> Bool
not (UnionM a -> Bool
forall a. UnionM a -> Bool
isMerged UnionM a
res) then String -> m (UnionM a)
forall a. HasCallStack => String -> a
error String
"Not merged" else UnionM a -> m (UnionM a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UnionM a
res

instance
  (GenSym a a, Mergeable a) =>
  GenSym (UnionM a) a
  where
  fresh :: forall (m :: * -> *). MonadFresh m => UnionM a -> m (UnionM a)
fresh UnionM a
spec = Union a -> m (UnionM a)
forall {spec} {a} {m :: * -> *}.
(GenSym spec a, MonadFresh m) =>
Union spec -> m (UnionM a)
go (UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion (UnionM a -> Union a) -> UnionM a -> Union a
forall a b. (a -> b) -> a -> b
$ UnionM a -> UnionM a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge UnionM a
spec)
    where
      go :: Union spec -> m (UnionM a)
go (UnionSingle spec
x) = spec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
fresh spec
x
      go (UnionIf spec
_ Bool
_ SymBool
_ Union spec
t Union spec
f) = SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymBool -> UnionM a -> UnionM a -> UnionM a)
-> m SymBool -> m (UnionM a -> UnionM a -> UnionM a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m SymBool
simpleFresh () m (UnionM a -> UnionM a -> UnionM a)
-> m (UnionM a) -> m (UnionM a -> UnionM a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Union spec -> m (UnionM a)
go Union spec
t m (UnionM a -> UnionM a) -> m (UnionM a) -> m (UnionM a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Union spec -> m (UnionM a)
go Union spec
f