{-# LANGUAGE DefaultSignatures #-}

{- |
This module provides the class 'Variable' which lets you create symbolical values of a data-type.

A generic default implementation with 'GVariable' is possible.

==== __Example__

@
data V3 a = V3 a a a deriving Generic
instance Codec a => Codec (V3 a)
instance Equatable a => Codec (V3 a)

problem :: MonadSMT s m => StateT s m (V3 (Expr RealSort))
problem = do
  let constantV3 = encode $ V3 7 69 42
  symbolicV3 <- variable \@(V3 (Expr RealSort))
  assert $ symbolicV3 /== constantV3
  return symbolicV3
@
-}
module Language.Hasmtlib.Variable
(
  -- * Class
  Variable(..)

  -- * Other functions
, variable'

  -- * Generics
, GVariable(..)
)
where

import Language.Hasmtlib.Type.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.
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
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (f a -> g a -> (:*:) f g a) -> m (f a) -> m (g a -> (:*:) f g 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 m (g a -> (:*:) f g a) -> m (g a) -> m ((:*:) f g a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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