content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE DefaultSignatures #-}
  {-# LANGUAGE UndecidableInstances #-}
  --------------------------------------------------------------------
  -- |
  -- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
  -- License   :  BSD3
  -- Maintainer:  Edward Kmett <ekmett@gmail.com>
  -- Stability :  experimental
  -- Portability: non-portable
  --
  --------------------------------------------------------------------
  module Ersatz.Variable
    ( Variable(..)
  #ifndef HLINT
    , forall_
  #endif
    , exists
  
    , GVariable(..)
    , genericLiterally
    ) where
  
  import Control.Monad
  import Ersatz.Internal.Literal
  import Ersatz.Problem
  import GHC.Generics
  
  exists :: (Variable a, MonadSAT s m)  => m a
  exists = literally literalExists
  
  #ifndef HLINT
  forall_ :: (Variable a, MonadQSAT s m) => m a
  forall_ = literally literalForall
  #endif
  
  class GVariable f where
    gliterally :: MonadSAT s m => m Literal -> m (f a)
  
  instance GVariable U1 where
    gliterally _ = return U1
  
  instance (GVariable f, GVariable g) => GVariable (f :*: g) where
    gliterally m = liftM2 (:*:) (gliterally m) (gliterally m)
  
  instance Variable a => GVariable (K1 i a) where
    gliterally = fmap K1 . literally
  
  instance GVariable f => GVariable (M1 i c f) where
    gliterally = fmap M1 . gliterally
  
  -- | This class describes all types that can be represented
  -- by a collection of literals. The class method 'literally'
  -- is usually applied to 'literalExists' or 'literalForall',
  -- see implementations of 'exists' and 'forall'.
  --
  -- Instances for this class for product-like types can be automatically derived
  -- for any type that is an instance of 'Generic'.
  --
  -- === __Example usage__
  --
  -- @
  -- {-# language DeriveGeneric, TypeApplications #-}
  -- import GHC.Generics
  --
  -- data T = C Bit Bit deriving Generic
  -- instance Variable T
  --
  -- constraint = do t <- exists @T ; ...
  -- @
  
  class Variable t where
    literally :: MonadSAT s m => m Literal -> m t
    default literally ::
      (MonadSAT s m, Generic t, GVariable (Rep t)) =>
      m Literal -> m t
    literally = genericLiterally
  
  genericLiterally ::
    (MonadSAT s m, Generic t, GVariable (Rep t)) =>
    m Literal -> m t
  genericLiterally = fmap to . gliterally
  
  instance Variable Literal where
    literally = id
  
  instance (Variable a, Variable b) => Variable (a,b)
  instance (Variable a, Variable b, Variable c) => Variable (a,b,c)
  instance (Variable a, Variable b, Variable c, Variable d) => Variable (a,b,c,d)
  instance (Variable a, Variable b, Variable c, Variable d, Variable e) => Variable (a,b,c,d,e)
  instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f) => Variable (a,b,c,d,e,f)
  instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f, Variable g) => Variable (a,b,c,d,e,f,g)
  