{-# LANGUAGE DefaultSignatures #-}

module Language.Hasmtlib.Variable where

import Language.Hasmtlib.Internal.Expr
import Language.Hasmtlib.Type.MonadSMT
import Data.Proxy

-- | Construct a variable datum of a data-type by creating variables for all its fields.
-- 
-- @
--    data V3 a = V3 a a a
--    instance Variable a => V3 a 
-- @
--
--    >>> varV3 <- variable @(V3 (Expr RealType)) ; varV3
--        V3 (Var RealType) (Var RealType) (Var RealType)
class Variable a where
  variable :: MonadSMT s m => m a
  default variable :: (MonadSMT s m, Applicative f, Traversable f, Variable b, a ~ f b) => m a
  variable = f (m b) -> m (f b)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => f (f a) -> f (f a)
sequenceA (f (m b) -> m (f b)) -> f (m b) -> m (f b)
forall a b. (a -> b) -> a -> b
$ m b -> f (m b)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure m b
forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
forall s (m :: * -> *). MonadSMT s m => m b
variable
  {-# INLINEABLE variable #-}

-- | 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 () where
  variable :: forall s (m :: * -> *). MonadSMT s m => m ()
variable = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

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

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

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

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

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

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) where
  variable :: forall s (m :: * -> *). MonadSMT s m => m (a, b, c, d, e, f, g, h)
variable = (,,,,,,,) (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
<$> m a
forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
forall s (m :: * -> *). MonadSMT s m => m a
variable 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
<*> m b
forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
forall s (m :: * -> *). MonadSMT s m => m b
variable 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
<*> m c
forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
forall s (m :: * -> *). MonadSMT s m => m c
variable 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
<*> m d
forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
forall s (m :: * -> *). MonadSMT s m => m d
variable 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
<*> m e
forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
forall s (m :: * -> *). MonadSMT s m => m e
variable 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
<*> m f
forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
forall s (m :: * -> *). MonadSMT s m => m f
variable 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
<*> m g
forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
forall s (m :: * -> *). MonadSMT s m => m g
variable 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
<*> m h
forall a s (m :: * -> *). (Variable a, MonadSMT s m) => m a
forall s (m :: * -> *). MonadSMT s m => m h
variable

instance Variable a => Variable (Maybe a)
instance Variable b => Variable (Either a b)