{-# 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 :: m a
exists = m Literal -> m a
forall t s (m :: * -> *).
(Variable t, MonadSAT s m) =>
m Literal -> m t
literally m Literal
forall s (m :: * -> *). MonadSAT s m => m Literal
literalExists

#ifndef HLINT
forall :: (Variable a, MonadQSAT s m)  => m a
forall :: m a
forall = m Literal -> m a
forall t s (m :: * -> *).
(Variable t, MonadSAT s m) =>
m Literal -> m t
literally m Literal
forall s (m :: * -> *). MonadQSAT s m => m Literal
literalForall
#endif

class GVariable f where
  gliterally :: MonadSAT s m => m Literal -> m (f a)

instance GVariable U1 where
  gliterally :: m Literal -> m (U1 a)
gliterally m Literal
_ = U1 a -> m (U1 a)
forall (m :: * -> *) a. Monad m => a -> m a
return U1 a
forall k (p :: k). U1 p
U1

instance (GVariable f, GVariable g) => GVariable (f :*: g) where
  gliterally :: m Literal -> m ((:*:) f g a)
gliterally m Literal
m = (f a -> g a -> (:*:) f g a)
-> m (f a) -> m (g a) -> m ((:*:) f g a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (m Literal -> m (f a)
forall (f :: * -> *) s (m :: * -> *) a.
(GVariable f, MonadSAT s m) =>
m Literal -> m (f a)
gliterally m Literal
m) (m Literal -> m (g a)
forall (f :: * -> *) s (m :: * -> *) a.
(GVariable f, MonadSAT s m) =>
m Literal -> m (f a)
gliterally m Literal
m)

instance Variable a => GVariable (K1 i a) where
  gliterally :: m Literal -> m (K1 i a a)
gliterally = (a -> K1 i a a) -> m a -> m (K1 i a a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (m a -> m (K1 i a a))
-> (m Literal -> m a) -> m Literal -> m (K1 i a a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Literal -> m a
forall t s (m :: * -> *).
(Variable t, MonadSAT s m) =>
m Literal -> m t
literally

instance GVariable f => GVariable (M1 i c f) where
  gliterally :: m Literal -> m (M1 i c f a)
gliterally = (f a -> M1 i c f a) -> m (f a) -> m (M1 i c f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> M1 i c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (m (f a) -> m (M1 i c f a))
-> (m Literal -> m (f a)) -> m Literal -> m (M1 i c f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Literal -> m (f a)
forall (f :: * -> *) s (m :: * -> *) a.
(GVariable f, MonadSAT s m) =>
m Literal -> m (f a)
gliterally

-- | Instances for this class for product-like types can be automatically derived
-- for any type that is an instance of 'Generic'.
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 = m Literal -> m t
forall s (m :: * -> *) t.
(MonadSAT s m, Generic t, GVariable (Rep t)) =>
m Literal -> m t
genericLiterally

genericLiterally ::
  (MonadSAT s m, Generic t, GVariable (Rep t)) =>
  m Literal -> m t
genericLiterally :: m Literal -> m t
genericLiterally = (Rep t Any -> t) -> m (Rep t Any) -> m t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep t Any -> t
forall a x. Generic a => Rep a x -> a
to (m (Rep t Any) -> m t)
-> (m Literal -> m (Rep t Any)) -> m Literal -> m t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Literal -> m (Rep t Any)
forall (f :: * -> *) s (m :: * -> *) a.
(GVariable f, MonadSAT s m) =>
m Literal -> m (f a)
gliterally

instance Variable Literal where
  literally :: m Literal -> m Literal
literally = m Literal -> m Literal
forall a. a -> a
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)