{-# LANGUAGE UndecidableInstances, TupleSections #-}

{- | This module provides an 'Analysis' type for combining multiple Datalog
     analyses together. Composition of analyses is done via the various
     type-classes that are implemented for this type. For a longer explanation
     of how the 'Analysis' type works, see this
     <https://luctielen.com/posts/analyses_are_arrows/ blogpost>.

     If you are just starting out using this library, you are probably better
     of taking a look at the "Language.Souffle.Interpreted" module instead to
     start interacting with a single Datalog program.
-}
module Language.Souffle.Analysis
  ( Analysis
  , mkAnalysis
  , execAnalysis
  ) where

import Prelude hiding (id, (.))
import Data.Kind (Type)
import Control.Category
import Control.Monad
import Control.Arrow
import Data.Profunctor

-- | Data type used to compose multiple Datalog programs. Composition is mainly
--   done via the various type-classes implemented for this type.
--   Values of this type can be created using 'mkAnalysis'.
--
--   The @m@ type-variable represents the monad the analysis will run in. In
--   most cases, this will be the @SouffleM@ monad from either
--   "Language.Souffle.Compiled" or "Language.Souffle.Interpreted".
--   The @a@ and @b@ type-variables represent respectively the input and output
--   types of the analysis.
type Analysis :: (Type -> Type) -> Type -> Type -> Type
data Analysis m a b
  = Analysis (a -> m ()) (m ()) (a -> m b)

-- | Creates an 'Analysis' value.
mkAnalysis :: (a -> m ()) -- ^ Function for finding facts used by the 'Analysis'.
           -> m ()        -- ^ Function for actually running the 'Analysis'.
           -> m b         -- ^ Function for retrieving the 'Analysis' results from Souffle.
           -> Analysis m a b
mkAnalysis :: forall a (m :: * -> *) b.
(a -> m ()) -> m () -> m b -> Analysis m a b
mkAnalysis a -> m ()
f m ()
r m b
g = forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis a -> m ()
f m ()
r (forall a b. a -> b -> a
const m b
g)
{-# INLINABLE mkAnalysis #-}

-- | Converts an 'Analysis' into an effectful function, so it can be executed.
execAnalysis :: Applicative m => Analysis m a b -> (a -> m b)
execAnalysis :: forall (m :: * -> *) a b.
Applicative m =>
Analysis m a b -> a -> m b
execAnalysis (Analysis a -> m ()
f m ()
r a -> m b
g) a
a = a -> m ()
f a
a forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m ()
r forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> a -> m b
g a
a
{-# INLINABLE execAnalysis #-}

instance Functor m => Functor (Analysis m a) where
  fmap :: forall a b. (a -> b) -> Analysis m a a -> Analysis m a b
fmap a -> b
func (Analysis a -> m ()
f m ()
r a -> m a
g) =
    forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis a -> m ()
f m ()
r (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
func forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
g)
  {-# INLINABLE fmap #-}

instance Functor m => Profunctor (Analysis m) where
  lmap :: forall a b c. (a -> b) -> Analysis m b c -> Analysis m a c
lmap a -> b
fn (Analysis b -> m ()
f m ()
r b -> m c
g) =
    forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
fn b -> m ()
f) m ()
r (forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
fn b -> m c
g)
  {-# INLINABLE lmap #-}

  rmap :: forall b c a. (b -> c) -> Analysis m a b -> Analysis m a c
rmap = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
  {-# INLINABLE rmap #-}

instance (Monoid (m ()), Applicative m) => Applicative (Analysis m a) where
  pure :: forall a. a -> Analysis m a a
pure a
a = forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a)
  {-# INLINABLE pure #-}

  Analysis a -> m ()
f1 m ()
r1 a -> m (a -> b)
g1 <*> :: forall a b.
Analysis m a (a -> b) -> Analysis m a a -> Analysis m a b
<*> Analysis a -> m ()
f2 m ()
r2 a -> m a
g2 =
    forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (a -> m ()
f1 forall a. Semigroup a => a -> a -> a
<> a -> m ()
f2) (m ()
r1 forall a. Semigroup a => a -> a -> a
<> m ()
r2) (\a
a -> a -> m (a -> b)
g1 a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> m a
g2 a
a)
  {-# INLINABLE (<*>) #-}

instance (Semigroup (m ()), Semigroup (m b)) => Semigroup (Analysis m a b) where
  Analysis a -> m ()
f1 m ()
r1 a -> m b
g1 <> :: Analysis m a b -> Analysis m a b -> Analysis m a b
<> Analysis a -> m ()
f2 m ()
r2 a -> m b
g2 =
    forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (a -> m ()
f1 forall a. Semigroup a => a -> a -> a
<> a -> m ()
f2) (m ()
r1 forall a. Semigroup a => a -> a -> a
<> m ()
r2) (a -> m b
g1 forall a. Semigroup a => a -> a -> a
<> a -> m b
g2)
  {-# INLINABLE (<>) #-}

instance (Monoid (m ()), Monoid (m b)) => Monoid (Analysis m a b) where
  mempty :: Analysis m a b
mempty = forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
  {-# INLINABLE mempty #-}

instance (Monoid (m ()), Monad m) => Category (Analysis m) where
  id :: forall a. Analysis m a a
id = forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall (f :: * -> *) a. Applicative f => a -> f a
pure
  {-# INLINABLE id #-}

  Analysis b -> m ()
f1 m ()
r1 b -> m c
g1 . :: forall b c a. Analysis m b c -> Analysis m a b -> Analysis m a c
. Analysis a -> m ()
f2 m ()
r2 a -> m b
g2 = forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis a -> m ()
f m ()
r1 a -> m c
g
    where
      f :: a -> m ()
f = forall (m :: * -> *) a b.
Applicative m =>
Analysis m a b -> a -> m b
execAnalysis (forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis a -> m ()
f2 m ()
r2 a -> m b
g2) forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> b -> m ()
f1
      -- NOTE: lazyness avoids work here in g2 in cases where "const" is used
      g :: a -> m c
g = a -> m b
g2 forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> b -> m c
g1
  {-# INLINABLE (.) #-}

instance Functor m => Strong (Analysis m) where
  first' :: forall a b c. Analysis m a b -> Analysis m (a, c) (b, c)
first' (Analysis a -> m ()
f m ()
r a -> m b
g) =
    forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (a -> m ()
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a, b) -> a
fst) m ()
r forall a b. (a -> b) -> a -> b
$ \(a
b, c
d) -> (,c
d) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
g a
b
  {-# INLINABLE first' #-}

  second' :: forall a b c. Analysis m a b -> Analysis m (c, a) (c, b)
second' (Analysis a -> m ()
f m ()
r a -> m b
g) =
    forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (a -> m ()
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a, b) -> b
snd) m ()
r forall a b. (a -> b) -> a -> b
$ \(c
d, a
b) -> (c
d,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
g a
b
  {-# INLINABLE second' #-}

instance Applicative m => Choice (Analysis m) where
  left' :: forall a b c.
Analysis m a b -> Analysis m (Either a c) (Either b c)
left' (Analysis a -> m ()
f m ()
r a -> m b
g) = forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis forall {b}. Either a b -> m ()
f' m ()
r forall {b}. Either a b -> m (Either b b)
g'
    where
      f' :: Either a b -> m ()
f' = \case
        Left a
b -> a -> m ()
f a
b
        Right b
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      g' :: Either a b -> m (Either b b)
g' = \case
        Left a
b -> forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
g a
b
        Right b
d -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right b
d
  {-# INLINABLE left' #-}

  right' :: forall a b c.
Analysis m a b -> Analysis m (Either c a) (Either c b)
right' (Analysis a -> m ()
f m ()
r a -> m b
g) = forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis forall {a}. Either a a -> m ()
f' m ()
r forall {a}. Either a a -> m (Either a b)
g'
    where
      f' :: Either a a -> m ()
f' = \case
        Left a
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Right a
b -> a -> m ()
f a
b
      g' :: Either a a -> m (Either a b)
g' = \case
        Left a
d -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left a
d
        Right a
b -> forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
g a
b
  {-# INLINABLE right' #-}

instance (Monad m, Monoid (m ()), Category (Analysis m)) => Arrow (Analysis m) where
  arr :: forall b c. (b -> c) -> Analysis m b c
arr b -> c
f = forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. b -> c
f)
  {-# INLINABLE arr #-}

  first :: forall b c d. Analysis m b c -> Analysis m (b, d) (c, d)
first = forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first'
  {-# INLINABLE first #-}

  second :: forall b c d. Analysis m b c -> Analysis m (d, b) (d, c)
second = forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (c, a) (c, b)
second'
  {-# INLINABLE second #-}

  Analysis b -> m ()
f1 m ()
r1 b -> m c
g1 *** :: forall b c b' c'.
Analysis m b c -> Analysis m b' c' -> Analysis m (b, b') (c, c')
*** Analysis b' -> m ()
f2 m ()
r2 b' -> m c'
g2 =
    forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (\(b
b, b'
b') -> b -> m ()
f1 b
b forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> b' -> m ()
f2 b'
b') (m ()
r1 forall a. Semigroup a => a -> a -> a
<> m ()
r2) forall a b. (a -> b) -> a -> b
$ \(b
b, b'
b') -> do
      c
c <- b -> m c
g1 b
b
      c'
c' <- b' -> m c'
g2 b'
b'
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (c
c, c'
c')
  {-# INLINABLE (***) #-}

  Analysis b -> m ()
f1 m ()
r1 b -> m c
g1 &&& :: forall b c c'.
Analysis m b c -> Analysis m b c' -> Analysis m b (c, c')
&&& Analysis b -> m ()
f2 m ()
r2 b -> m c'
g2 =
    forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (b -> m ()
f1 forall a. Semigroup a => a -> a -> a
<> b -> m ()
f2) (m ()
r1 forall a. Semigroup a => a -> a -> a
<> m ()
r2) forall a b. (a -> b) -> a -> b
$ \b
b -> (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m c
g1 b
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> m c'
g2 b
b
  {-# INLINABLE (&&&) #-}

instance (Monad m, Monoid (m ())) => ArrowChoice (Analysis m) where
  left :: forall b c d.
Analysis m b c -> Analysis m (Either b d) (Either c d)
left = forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left'
  {-# INLINABLE left #-}

  right :: forall b c d.
Analysis m b c -> Analysis m (Either d b) (Either d c)
right = forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right'
  {-# INLINABLE right #-}

  Analysis b -> m ()
f1 m ()
r1 b -> m c
g1 +++ :: forall b c b' c'.
Analysis m b c
-> Analysis m b' c' -> Analysis m (Either b b') (Either c c')
+++ Analysis b' -> m ()
f2 m ()
r2 b' -> m c'
g2 = forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis Either b b' -> m ()
f' (m ()
r1 forall a. Semigroup a => a -> a -> a
<> m ()
r2) Either b b' -> m (Either c c')
g'
    where
      f' :: Either b b' -> m ()
f' = \case
        Left b
b -> b -> m ()
f1 b
b
        Right b'
b' -> b' -> m ()
f2 b'
b'
      g' :: Either b b' -> m (Either c c')
g' = \case
        Left b
b -> forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m c
g1 b
b
        Right b'
b' -> forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b' -> m c'
g2 b'
b'
  {-# INLINABLE (+++) #-}