{-# LANGUAGE DefaultSignatures #-}

module Language.Hasmtlib.Variable where

import Language.Hasmtlib.Internal.Expr
import Language.Hasmtlib.Type.MonadSMT
import Language.Hasmtlib.Type.SMTSort
import Data.Proxy
import Data.Monoid (Sum, Product, First, Last, Alt, Dual)
import Data.Functor.Const (Const)
import Data.Functor.Identity (Identity)
import Data.Functor.Compose (Compose)
import GHC.Generics

-- | Construct a variable datum of a data-type by creating variables for all its fields.
--
--   You can derive an instance of this class if your type is 'Generic' and has exactly one constructor.
--
-- @
--    data V3 a = V3 a a a deriving Generic
--    instance Variable a => V3 a
-- @
--
--    >>> varV3 :: V3 (Expr RealType) <- variable ; varV3
--        V3 (Expr RealType) (Expr RealType) (Expr RealType)
class Variable a where
  variable :: MonadSMT s m => m a
  default variable :: (MonadSMT s m, Generic a, GVariable (Rep a)) => m a
  variable = 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 {k} (f :: k -> *) s (m :: * -> *) (a :: k).
(GVariable f, MonadSMT s m) =>
m (f a)
forall s (m :: * -> *) a. MonadSMT s m => m (Rep a a)
gvariable

-- | Wrapper for 'variable' which takes a 'Proxy'
variable' :: forall s m a. (MonadSMT s m, Variable a) => Proxy a -> m a
variable' :: forall s (m :: * -> *) a.
(MonadSMT s m, Variable a) =>
Proxy a -> m a
variable' Proxy a
_ = forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
variable @a
{-# INLINE variable' #-}

instance KnownSMTSort t => Variable (Expr t) where
  variable :: forall s (m :: * -> *). MonadSMT s m => m (Expr t)
variable = m (Expr t)
forall (t :: SMTSort) s (m :: * -> *).
(KnownSMTSort t, MonadSMT s m) =>
m (Expr t)
var
  {-# INLINE variable #-}

instance Variable ()
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)
instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f, Variable g, Variable h) => Variable (a,b,c,d,e,f,g,h)
instance Variable a => Variable (Sum a)
instance Variable a => Variable (Product a)
instance Variable a => Variable (First a)
instance Variable a => Variable (Last a)
instance Variable a => Variable (Dual a)
instance Variable a => Variable (Identity a)
instance Variable m => Variable (Const m a)
instance Variable (f a) => Variable (Alt f a)
instance Variable (f (g a)) => Variable (Compose f g a)

instance Variable a => Variable (Maybe a) where
  variable :: forall s (m :: * -> *). MonadSMT s m => m (Maybe a)
variable = 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
<$> m a
forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
forall s (m :: * -> *). MonadSMT s m => m a
variable

instance Variable b => Variable (Either a b) where
  variable :: forall s (m :: * -> *). MonadSMT s m => m (Either a b)
variable = 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
<$> m b
forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
forall s (m :: * -> *). MonadSMT s m => m b
variable

class GVariable f where
  gvariable :: MonadSMT s m => m (f a)

instance GVariable U1 where
  gvariable :: forall s (m :: * -> *) (a :: k). MonadSMT s m => m (U1 a)
gvariable = U1 a -> m (U1 a)
forall a. a -> m 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
  gvariable :: forall s (m :: * -> *) (a :: k). MonadSMT s m => m ((:*:) f g a)
gvariable = (f a -> g a -> (:*:) f g a)
-> m (f a) -> m (g a) -> m ((:*:) f g a)
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) m (f a)
forall {k} (f :: k -> *) s (m :: * -> *) (a :: k).
(GVariable f, MonadSMT s m) =>
m (f a)
forall s (m :: * -> *) (a :: k). MonadSMT s m => m (f a)
gvariable m (g a)
forall {k} (f :: k -> *) s (m :: * -> *) (a :: k).
(GVariable f, MonadSMT s m) =>
m (f a)
forall s (m :: * -> *) (a :: k). MonadSMT s m => m (g a)
gvariable

instance GVariable f => GVariable (M1 i c f) where
  gvariable :: forall s (m :: * -> *) (a :: k). MonadSMT s m => m (M1 i c f a)
gvariable = f a -> M1 i c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (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
<$> m (f a)
forall {k} (f :: k -> *) s (m :: * -> *) (a :: k).
(GVariable f, MonadSMT s m) =>
m (f a)
forall s (m :: * -> *) (a :: k). MonadSMT s m => m (f a)
gvariable

instance Variable a => GVariable (K1 i a) where
  gvariable :: forall s (m :: * -> *) (a :: k). MonadSMT s m => m (K1 i a a)
gvariable = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> m a -> m (K1 i a a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
forall s (m :: * -> *). MonadSMT s m => m a
variable