{-# 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 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.
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 = (a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis a -> m ()
f m ()
r (m b -> a -> m b
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 m () -> m () -> m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m ()
r m () -> m b -> m b
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) =
    (a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis a -> m ()
f m ()
r ((a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
func (m a -> m b) -> (a -> m a) -> a -> m b
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) =
    (a -> m ()) -> m () -> (a -> m c) -> Analysis m a c
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis ((a -> b) -> (b -> m ()) -> a -> m ()
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
fn b -> m ()
f) m ()
r ((a -> b) -> (b -> m c) -> a -> m c
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 = (b -> c) -> Analysis m a b -> Analysis m a c
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 = (a -> m ()) -> m () -> (a -> m a) -> Analysis m a a
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis a -> m ()
forall a. Monoid a => a
mempty m ()
forall a. Monoid a => a
mempty (m a -> a -> m a
forall a b. a -> b -> a
const (m a -> a -> m a) -> m a -> a -> m a
forall a b. (a -> b) -> a -> b
$ a -> m a
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 =
    (a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (a -> m ()
f1 (a -> m ()) -> (a -> m ()) -> a -> m ()
forall a. Semigroup a => a -> a -> a
<> a -> m ()
f2) (m ()
r1 m () -> m () -> m ()
forall a. Semigroup a => a -> a -> a
<> m ()
r2) (\a
a -> a -> m (a -> b)
g1 a
a m (a -> b) -> m a -> m b
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 =
    (a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (a -> m ()
f1 (a -> m ()) -> (a -> m ()) -> a -> m ()
forall a. Semigroup a => a -> a -> a
<> a -> m ()
f2) (m ()
r1 m () -> m () -> m ()
forall a. Semigroup a => a -> a -> a
<> m ()
r2) (a -> m b
g1 (a -> m b) -> (a -> m b) -> a -> m b
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 = (a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis a -> m ()
forall a. Monoid a => a
mempty m ()
forall a. Monoid a => a
mempty a -> m b
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 = (a -> m ()) -> m () -> (a -> m a) -> Analysis m a a
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis a -> m ()
forall a. Monoid a => a
mempty m ()
forall a. Monoid a => a
mempty a -> m a
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 = (a -> m ()) -> m () -> (a -> m c) -> Analysis m a c
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 = Analysis m a b -> a -> m b
forall (m :: * -> *) a b.
Applicative m =>
Analysis m a b -> a -> m b
execAnalysis ((a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis a -> m ()
f2 m ()
r2 a -> m b
g2) (a -> m b) -> (b -> m ()) -> a -> m ()
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 (a -> m b) -> (b -> m c) -> a -> m c
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) =
    ((a, c) -> m ())
-> m () -> ((a, c) -> m (b, c)) -> Analysis m (a, c) (b, c)
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (a -> m ()
f (a -> m ()) -> ((a, c) -> a) -> (a, c) -> m ()
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a, c) -> a
forall a b. (a, b) -> a
fst) m ()
r (((a, c) -> m (b, c)) -> Analysis m (a, c) (b, c))
-> ((a, c) -> m (b, c)) -> Analysis m (a, c) (b, c)
forall a b. (a -> b) -> a -> b
$ \(a
b, c
d) -> (,c
d) (b -> (b, c)) -> m b -> m (b, c)
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) =
    ((c, a) -> m ())
-> m () -> ((c, a) -> m (c, b)) -> Analysis m (c, a) (c, b)
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (a -> m ()
f (a -> m ()) -> ((c, a) -> a) -> (c, a) -> m ()
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (c, a) -> a
forall a b. (a, b) -> b
snd) m ()
r (((c, a) -> m (c, b)) -> Analysis m (c, a) (c, b))
-> ((c, a) -> m (c, b)) -> Analysis m (c, a) (c, b)
forall a b. (a -> b) -> a -> b
$ \(c
d, a
b) -> (c
d,) (b -> (c, b)) -> m b -> m (c, b)
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) = (Either a c -> m ())
-> m ()
-> (Either a c -> m (Either b c))
-> Analysis m (Either a c) (Either b c)
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis Either a c -> m ()
forall {b}. Either a b -> m ()
f' m ()
r Either a c -> m (Either b c)
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
_ -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      g' :: Either a b -> m (Either b b)
g' = \case
        Left a
b -> b -> Either b b
forall a b. a -> Either a b
Left (b -> Either b b) -> m b -> m (Either b b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
g a
b
        Right b
d -> Either b b -> m (Either b b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either b b -> m (Either b b)) -> Either b b -> m (Either b b)
forall a b. (a -> b) -> a -> b
$ b -> Either b 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) = (Either c a -> m ())
-> m ()
-> (Either c a -> m (Either c b))
-> Analysis m (Either c a) (Either c b)
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis Either c a -> m ()
forall {a}. Either a a -> m ()
f' m ()
r Either c a -> m (Either c b)
forall {a}. Either a a -> m (Either a b)
g'
    where
      f' :: Either a a -> m ()
f' = \case
        Left a
_ -> () -> m ()
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 -> Either a b -> m (Either a b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either a b -> m (Either a b)) -> Either a b -> m (Either a b)
forall a b. (a -> b) -> a -> b
$ a -> Either a b
forall a b. a -> Either a b
Left a
d
        Right a
b -> 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
<$> 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 = (b -> m ()) -> m () -> (b -> m c) -> Analysis m b c
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis b -> m ()
forall a. Monoid a => a
mempty m ()
forall a. Monoid a => a
mempty (c -> m c
forall (f :: * -> *) a. Applicative f => a -> f a
pure (c -> m c) -> (b -> c) -> b -> m c
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 = Analysis m b c -> Analysis m (b, d) (c, d)
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 = Analysis m b c -> Analysis m (d, b) (d, c)
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 =
    ((b, b') -> m ())
-> m () -> ((b, b') -> m (c, c')) -> Analysis m (b, b') (c, c')
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (\(b
b, b'
b') -> b -> m ()
f1 b
b m () -> m () -> m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> b' -> m ()
f2 b'
b') (m ()
r1 m () -> m () -> m ()
forall a. Semigroup a => a -> a -> a
<> m ()
r2) (((b, b') -> m (c, c')) -> Analysis m (b, b') (c, c'))
-> ((b, b') -> m (c, c')) -> Analysis m (b, b') (c, c')
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'
      (c, c') -> m (c, c')
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 =
    (b -> m ()) -> m () -> (b -> m (c, c')) -> Analysis m b (c, c')
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis (b -> m ()
f1 (b -> m ()) -> (b -> m ()) -> b -> m ()
forall a. Semigroup a => a -> a -> a
<> b -> m ()
f2) (m ()
r1 m () -> m () -> m ()
forall a. Semigroup a => a -> a -> a
<> m ()
r2) ((b -> m (c, c')) -> Analysis m b (c, c'))
-> (b -> m (c, c')) -> Analysis m b (c, c')
forall a b. (a -> b) -> a -> b
$ \b
b -> (,) (c -> c' -> (c, c')) -> m c -> m (c' -> (c, c'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m c
g1 b
b m (c' -> (c, c')) -> m c' -> m (c, c')
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 = Analysis m b c -> Analysis m (Either b d) (Either c d)
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 = Analysis m b c -> Analysis m (Either d b) (Either d c)
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 = (Either b b' -> m ())
-> m ()
-> (Either b b' -> m (Either c c'))
-> Analysis m (Either b b') (Either c c')
forall (m :: * -> *) a b.
(a -> m ()) -> m () -> (a -> m b) -> Analysis m a b
Analysis Either b b' -> m ()
f' (m ()
r1 m () -> m () -> m ()
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 -> c -> Either c c'
forall a b. a -> Either a b
Left (c -> Either c c') -> m c -> m (Either c c')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m c
g1 b
b
        Right b'
b' -> c' -> Either c c'
forall a b. b -> Either a b
Right (c' -> Either c c') -> m c' -> m (Either c c')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b' -> m c'
g2 b'
b'
  {-# INLINABLE (+++) #-}