{-# LANGUAGE ConstraintKinds  #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs            #-}
{-# LANGUAGE LambdaCase       #-}
{-# LANGUAGE TemplateHaskell  #-}
{-# LANGUAGE TypeOperators    #-}

{- | Functions for computing the dependency graph of variables within a term or type.
A "dependency" between two nodes "A depends on B" means that B cannot be removed
from the program without also removing A.
-}
module PlutusIR.Analysis.Dependencies (
  Node (..),
  DepGraph,
  runTermDeps,
) where

import PlutusCore qualified as PLC
import PlutusCore.Builtin qualified as PLC
import PlutusCore.Name.Unique qualified as PLC

import PlutusIR
import PlutusIR.Analysis.Usages qualified as Usages
import PlutusIR.Purity

import Control.Lens hiding (Strict)
import Control.Monad.Reader

import Algebra.Graph.Class qualified as G
import Data.Set qualified as Set

import Data.List.NonEmpty qualified as NE

import PlutusIR.Analysis.Builtins
import PlutusIR.Analysis.VarInfo

{- | A node in a dependency graph. Either a specific 'PLC.Unique', or a specific
node indicating the root of the graph. We need the root node because when computing the
dependency graph of, say, a term, there will not be a binding for the term itself which
we can use to represent it in the graph.
-}
data Node = Variable PLC.Unique | Root deriving stock (Int -> Node -> ShowS
[Node] -> ShowS
Node -> String
(Int -> Node -> ShowS)
-> (Node -> String) -> ([Node] -> ShowS) -> Show Node
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Node -> ShowS
showsPrec :: Int -> Node -> ShowS
$cshow :: Node -> String
show :: Node -> String
$cshowList :: [Node] -> ShowS
showList :: [Node] -> ShowS
Show, Node -> Node -> Bool
(Node -> Node -> Bool) -> (Node -> Node -> Bool) -> Eq Node
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Node -> Node -> Bool
== :: Node -> Node -> Bool
$c/= :: Node -> Node -> Bool
/= :: Node -> Node -> Bool
Eq, Eq Node
Eq Node =>
(Node -> Node -> Ordering)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Node)
-> (Node -> Node -> Node)
-> Ord Node
Node -> Node -> Bool
Node -> Node -> Ordering
Node -> Node -> Node
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Node -> Node -> Ordering
compare :: Node -> Node -> Ordering
$c< :: Node -> Node -> Bool
< :: Node -> Node -> Bool
$c<= :: Node -> Node -> Bool
<= :: Node -> Node -> Bool
$c> :: Node -> Node -> Bool
> :: Node -> Node -> Bool
$c>= :: Node -> Node -> Bool
>= :: Node -> Node -> Bool
$cmax :: Node -> Node -> Node
max :: Node -> Node -> Node
$cmin :: Node -> Node -> Node
min :: Node -> Node -> Node
Ord)

data DepCtx tyname name uni fun a = DepCtx
  { forall tyname name (uni :: * -> *) fun a.
DepCtx tyname name uni fun a -> Node
_depNode         :: Node
  , forall tyname name (uni :: * -> *) fun a.
DepCtx tyname name uni fun a -> BuiltinsInfo uni fun
_depBuiltinsInfo :: BuiltinsInfo uni fun
  , forall tyname name (uni :: * -> *) fun a.
DepCtx tyname name uni fun a -> VarsInfo tyname name uni a
_depVarInfo      :: VarsInfo tyname name uni a
  }
makeLenses ''DepCtx

{- | A constraint requiring @g@ to be a 'G.Graph' (so we can compute e.g. a @Relation@ from
it), whose vertices are 'Node's.
-}
type DepGraph g = (G.Graph g, G.Vertex g ~ Node)

{- | Compute the dependency graph of a 'Term'. The 'Root' node will correspond to the term itself.

For example, the graph of @[(let (nonrec) (vardecl x t) y) [x z]]@ is
@
    ROOT -> x
    ROOT -> z
    x -> y
    x -> t
@
-}
runTermDeps ::
  ( DepGraph g
  , PLC.HasUnique tyname PLC.TypeUnique
  , PLC.HasUnique name PLC.TermUnique
  , PLC.ToBuiltinMeaning uni fun
  ) =>
  BuiltinsInfo uni fun ->
  VarsInfo tyname name uni a ->
  Term tyname name uni fun a ->
  g
runTermDeps :: forall g tyname name (uni :: * -> *) fun a.
(DepGraph g, HasUnique tyname TypeUnique,
 HasUnique name TermUnique, ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a -> Term tyname name uni fun a -> g
runTermDeps BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo Term tyname name uni fun a
t = (Reader (DepCtx tyname name uni fun a) g
 -> DepCtx tyname name uni fun a -> g)
-> DepCtx tyname name uni fun a
-> Reader (DepCtx tyname name uni fun a) g
-> g
forall a b c. (a -> b -> c) -> b -> a -> c
flip Reader (DepCtx tyname name uni fun a) g
-> DepCtx tyname name uni fun a -> g
forall r a. Reader r a -> r -> a
runReader (Node
-> BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> DepCtx tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Node
-> BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> DepCtx tyname name uni fun a
DepCtx Node
Root BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo) (Reader (DepCtx tyname name uni fun a) g -> g)
-> Reader (DepCtx tyname name uni fun a) g -> g
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun a
-> Reader (DepCtx tyname name uni fun a) g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique, HasUnique name TermUnique,
 ToBuiltinMeaning uni fun) =>
Term tyname name uni fun a -> m g
termDeps Term tyname name uni fun a
t

-- | Record some dependencies on the current node.
currentDependsOn ::
  (DepGraph g, MonadReader (DepCtx tyname name uni fun a) m) =>
  [PLC.Unique] ->
  m g
currentDependsOn :: forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m) =>
[Unique] -> m g
currentDependsOn [Unique]
us = do
  Node
current <- Getting Node (DepCtx tyname name uni fun a) Node -> m Node
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Node (DepCtx tyname name uni fun a) Node
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Functor f =>
(Node -> f Node)
-> DepCtx tyname name uni fun a -> f (DepCtx tyname name uni fun a)
depNode
  g -> m g
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (g -> m g) -> g -> m g
forall a b. (a -> b) -> a -> b
$ g -> g -> g
forall g. Graph g => g -> g -> g
G.connect ([Vertex g] -> g
forall g. Graph g => [Vertex g] -> g
G.vertices [Vertex g
Node
current]) ([Vertex g] -> g
forall g. Graph g => [Vertex g] -> g
G.vertices ((Unique -> Node) -> [Unique] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Unique -> Node
Variable [Unique]
us))

-- | Process the given action with the given name as the current node.
withCurrent ::
  (MonadReader (DepCtx tyname name uni fun a) m, PLC.HasUnique n u) =>
  n ->
  m g ->
  m g
withCurrent :: forall tyname name (uni :: * -> *) fun a (m :: * -> *) n u g.
(MonadReader (DepCtx tyname name uni fun a) m, HasUnique n u) =>
n -> m g -> m g
withCurrent n
n = (DepCtx tyname name uni fun a -> DepCtx tyname name uni fun a)
-> m g -> m g
forall a.
(DepCtx tyname name uni fun a -> DepCtx tyname name uni fun a)
-> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((DepCtx tyname name uni fun a -> DepCtx tyname name uni fun a)
 -> m g -> m g)
-> (DepCtx tyname name uni fun a -> DepCtx tyname name uni fun a)
-> m g
-> m g
forall a b. (a -> b) -> a -> b
$ ASetter
  (DepCtx tyname name uni fun a)
  (DepCtx tyname name uni fun a)
  Node
  Node
-> Node
-> DepCtx tyname name uni fun a
-> DepCtx tyname name uni fun a
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter
  (DepCtx tyname name uni fun a)
  (DepCtx tyname name uni fun a)
  Node
  Node
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Functor f =>
(Node -> f Node)
-> DepCtx tyname name uni fun a -> f (DepCtx tyname name uni fun a)
depNode (Node
 -> DepCtx tyname name uni fun a -> DepCtx tyname name uni fun a)
-> Node
-> DepCtx tyname name uni fun a
-> DepCtx tyname name uni fun a
forall a b. (a -> b) -> a -> b
$ Unique -> Node
Variable (Unique -> Node) -> Unique -> Node
forall a b. (a -> b) -> a -> b
$ n
n n -> Getting Unique n Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique n Unique
forall name unique. HasUnique name unique => Lens' name Unique
Lens' n Unique
PLC.theUnique

{- Note [Strict term bindings and dependencies]
A node inside a strict let binding can incur a dependency on it even if the defined variable
is unused.

Consider:

let strict x = error in y

This evaluates to error, because the RHS of a strict binding is evaluated when we evaluate
the let-term.

We only care about this for its *effects*: the variable itself is still unused. So we only need to
worry in the case where the RHS is not a value. If it *is* a value, then evaluating it is a noop,
so there can be no effects that we're missing. Essentially we are using "is a value" as an
under-approximation of "is pure".

From the point of view of our algorithm, we handle the dependency by treating it as though
there was an reference to the newly bound variable alongside the binding, but only in the
cases where it matters.
-}

{- Note [Dependencies for datatype bindings, and pruning them]
At face value, all the names introduced by datatype bindings should depend on each other.
Given our meaning of "A depends on B", since we cannot remove any part of the datatype
binding without removing the whole thing, they all depend on each other

However, there are some circumstances in which we *can* prune datatype bindings.

In particular, if the datatype is only used at the type-level (i.e. all the term-level parts
(constructors and destructor) are dead), then we are free to completely replace the binding
with one for a trivial type with the same kind.

This is because there are *no* term-level effects, and types are erased in the end, so
in this case rest of the datatype binding really is superfluous.

But how do we represent this in the dependency graph? We still need to have proper dependencies
so that we don't make the wrong decisions wrt transitively used values, e.g.

let U :: * = ...
let datatype T = T1 | T2 U
in T1

Here we need to not delete U, even though T2 is "dead"!

The solution is to focus on the meaning of "dependency": with the pruning that we can do, we *can*
remove all the term level bits en masse, but only en-mass. So we need to make *them* into a clique,
so that this is visible to the dependency analysis.
-}

bindingDeps ::
  ( DepGraph g
  , MonadReader (DepCtx tyname name uni fun a) m
  , PLC.HasUnique tyname PLC.TypeUnique
  , PLC.HasUnique name PLC.TermUnique
  , PLC.ToBuiltinMeaning uni fun
  ) =>
  Binding tyname name uni fun a ->
  m g
bindingDeps :: forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique, HasUnique name TermUnique,
 ToBuiltinMeaning uni fun) =>
Binding tyname name uni fun a -> m g
bindingDeps Binding tyname name uni fun a
b = case Binding tyname name uni fun a
b of
  TermBind a
_ Strictness
strictness d :: VarDecl tyname name uni a
d@(VarDecl a
_ name
n Type tyname uni a
_) Term tyname name uni fun a
rhs -> do
    g
vDeps <- VarDecl tyname name uni a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique, HasUnique name TermUnique) =>
VarDecl tyname name uni a -> m g
varDeclDeps VarDecl tyname name uni a
d
    g
tDeps <- name -> m g -> m g
forall tyname name (uni :: * -> *) fun a (m :: * -> *) n u g.
(MonadReader (DepCtx tyname name uni fun a) m, HasUnique n u) =>
n -> m g -> m g
withCurrent name
n (m g -> m g) -> m g -> m g
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique, HasUnique name TermUnique,
 ToBuiltinMeaning uni fun) =>
Term tyname name uni fun a -> m g
termDeps Term tyname name uni fun a
rhs

    BuiltinsInfo uni fun
binfo <- Getting
  (BuiltinsInfo uni fun)
  (DepCtx tyname name uni fun a)
  (BuiltinsInfo uni fun)
-> m (BuiltinsInfo uni fun)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (BuiltinsInfo uni fun)
  (DepCtx tyname name uni fun a)
  (BuiltinsInfo uni fun)
forall tyname name (uni :: * -> *) fun a fun (f :: * -> *).
Functor f =>
(BuiltinsInfo uni fun -> f (BuiltinsInfo uni fun))
-> DepCtx tyname name uni fun a -> f (DepCtx tyname name uni fun a)
depBuiltinsInfo
    -- See Note [Strict term bindings and dependencies]
    VarsInfo tyname name uni a
vinfo <- Getting
  (VarsInfo tyname name uni a)
  (DepCtx tyname name uni fun a)
  (VarsInfo tyname name uni a)
-> m (VarsInfo tyname name uni a)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (VarsInfo tyname name uni a)
  (DepCtx tyname name uni fun a)
  (VarsInfo tyname name uni a)
forall tyname name (uni :: * -> *) fun a tyname name a
       (f :: * -> *).
Functor f =>
(VarsInfo tyname name uni a -> f (VarsInfo tyname name uni a))
-> DepCtx tyname name uni fun a -> f (DepCtx tyname name uni fun a)
depVarInfo
    g
evalDeps <- case Strictness
strictness of
      Strictness
Strict | Bool -> Bool
not (BuiltinsInfo uni fun
-> VarsInfo tyname name uni a -> Term tyname name uni fun a -> Bool
forall (uni :: * -> *) fun name tyname a.
(ToBuiltinMeaning uni fun, HasUnique name TermUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a -> Term tyname name uni fun a -> Bool
isPure BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo Term tyname name uni fun a
rhs) -> [Unique] -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m) =>
[Unique] -> m g
currentDependsOn [name
n name -> Getting Unique name Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique name Unique
forall name unique. HasUnique name unique => Lens' name Unique
Lens' name Unique
PLC.theUnique]
      Strictness
_                                     -> g -> m g
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure g
forall g. Graph g => g
G.empty

    g -> m g
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (g -> m g) -> g -> m g
forall a b. (a -> b) -> a -> b
$ [g] -> g
forall g. Graph g => [g] -> g
G.overlays [g
vDeps, g
tDeps, g
evalDeps]
  TypeBind a
_ d :: TyVarDecl tyname a
d@(TyVarDecl a
_ tyname
n Kind a
_) Type tyname uni a
rhs -> do
    g
vDeps <- TyVarDecl tyname a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(Graph g, MonadReader (DepCtx tyname name uni fun a) m) =>
TyVarDecl tyname a -> m g
tyVarDeclDeps TyVarDecl tyname a
d
    g
tDeps <- tyname -> m g -> m g
forall tyname name (uni :: * -> *) fun a (m :: * -> *) n u g.
(MonadReader (DepCtx tyname name uni fun a) m, HasUnique n u) =>
n -> m g -> m g
withCurrent tyname
n (m g -> m g) -> m g -> m g
forall a b. (a -> b) -> a -> b
$ Type tyname uni a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique) =>
Type tyname uni a -> m g
typeDeps Type tyname uni a
rhs
    g -> m g
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (g -> m g) -> g -> m g
forall a b. (a -> b) -> a -> b
$ g -> g -> g
forall g. Graph g => g -> g -> g
G.overlay g
vDeps g
tDeps
  DatatypeBind a
_ (Datatype a
_ TyVarDecl tyname a
d [TyVarDecl tyname a]
tvs name
destr [VarDecl tyname name uni a]
constrs) -> do
    -- See Note [Dependencies for datatype bindings, and pruning them]
    g
vDeps <- TyVarDecl tyname a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(Graph g, MonadReader (DepCtx tyname name uni fun a) m) =>
TyVarDecl tyname a -> m g
tyVarDeclDeps TyVarDecl tyname a
d
    [g]
tvDeps <- (TyVarDecl tyname a -> m g) -> [TyVarDecl tyname a] -> m [g]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse TyVarDecl tyname a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(Graph g, MonadReader (DepCtx tyname name uni fun a) m) =>
TyVarDecl tyname a -> m g
tyVarDeclDeps [TyVarDecl tyname a]
tvs
    [g]
cstrDeps <- (VarDecl tyname name uni a -> m g)
-> [VarDecl tyname name uni a] -> m [g]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse VarDecl tyname name uni a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique, HasUnique name TermUnique) =>
VarDecl tyname name uni a -> m g
varDeclDeps [VarDecl tyname name uni a]
constrs
    -- Destructors depend on the datatype and the argument types of all the constructors,
    -- because e.g. a destructor for Maybe looks like:
    -- forall a . Maybe a -> (a -> r) -> r -> r
    -- i.e. the argument type of the Just constructor appears as the argument to the branch.
    --
    -- We can get the effect of that by having it depend on all the constructor types
    -- (which also include the datatype).
    -- This is more diligent than currently necessary since we're going to make all the
    -- term-level parts depend on each other later, but it's good practice and will be
    -- useful if we ever stop doing that.
    g
destrDeps <-
      [g] -> g
forall g. Graph g => [g] -> g
G.overlays
        ([g] -> g) -> m [g] -> m g
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (name -> m [g] -> m [g]
forall tyname name (uni :: * -> *) fun a (m :: * -> *) n u g.
(MonadReader (DepCtx tyname name uni fun a) m, HasUnique n u) =>
n -> m g -> m g
withCurrent name
destr (m [g] -> m [g]) -> m [g] -> m [g]
forall a b. (a -> b) -> a -> b
$ (VarDecl tyname name uni a -> m g)
-> [VarDecl tyname name uni a] -> m [g]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Type tyname uni a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique) =>
Type tyname uni a -> m g
typeDeps (Type tyname uni a -> m g)
-> (VarDecl tyname name uni a -> Type tyname uni a)
-> VarDecl tyname name uni a
-> m g
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDecl tyname name uni a -> Type tyname uni a
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> Type tyname uni ann
_varDeclType) [VarDecl tyname name uni a]
constrs)
    let tus :: [Unique]
tus = (name -> Unique) -> [name] -> [Unique]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Getting Unique name Unique -> name -> Unique
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Unique name Unique
forall name unique. HasUnique name unique => Lens' name Unique
Lens' name Unique
PLC.theUnique) (name
destr name -> [name] -> [name]
forall a. a -> [a] -> [a]
: (VarDecl tyname name uni a -> name)
-> [VarDecl tyname name uni a] -> [name]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VarDecl tyname name uni a -> name
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> name
_varDeclName [VarDecl tyname name uni a]
constrs)
    -- See Note [Dependencies for datatype bindings, and pruning them]
    let nonDatatypeClique :: g
nonDatatypeClique = [Vertex g] -> g
forall g. Graph g => [Vertex g] -> g
G.clique ((Unique -> Node) -> [Unique] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Unique -> Node
Variable [Unique]
tus)
    g -> m g
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (g -> m g) -> g -> m g
forall a b. (a -> b) -> a -> b
$ [g] -> g
forall g. Graph g => [g] -> g
G.overlays ([g] -> g) -> [g] -> g
forall a b. (a -> b) -> a -> b
$ [g
vDeps] [g] -> [g] -> [g]
forall a. [a] -> [a] -> [a]
++ [g]
tvDeps [g] -> [g] -> [g]
forall a. [a] -> [a] -> [a]
++ [g]
cstrDeps [g] -> [g] -> [g]
forall a. [a] -> [a] -> [a]
++ [g
destrDeps] [g] -> [g] -> [g]
forall a. [a] -> [a] -> [a]
++ [g
nonDatatypeClique]

varDeclDeps ::
  ( DepGraph g
  , MonadReader (DepCtx tyname name uni fun a) m
  , PLC.HasUnique tyname PLC.TypeUnique
  , PLC.HasUnique name PLC.TermUnique
  ) =>
  VarDecl tyname name uni a ->
  m g
varDeclDeps :: forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique, HasUnique name TermUnique) =>
VarDecl tyname name uni a -> m g
varDeclDeps (VarDecl a
_ name
n Type tyname uni a
ty) = name -> m g -> m g
forall tyname name (uni :: * -> *) fun a (m :: * -> *) n u g.
(MonadReader (DepCtx tyname name uni fun a) m, HasUnique n u) =>
n -> m g -> m g
withCurrent name
n (m g -> m g) -> m g -> m g
forall a b. (a -> b) -> a -> b
$ Type tyname uni a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique) =>
Type tyname uni a -> m g
typeDeps Type tyname uni a
ty

-- Here for completeness, but doesn't do much
tyVarDeclDeps ::
  (G.Graph g, MonadReader (DepCtx tyname name uni fun a) m) =>
  TyVarDecl tyname a ->
  m g
tyVarDeclDeps :: forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(Graph g, MonadReader (DepCtx tyname name uni fun a) m) =>
TyVarDecl tyname a -> m g
tyVarDeclDeps TyVarDecl tyname a
_ = g -> m g
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure g
forall g. Graph g => g
G.empty

{- | Compute the dependency graph of a term. Takes an initial 'Node' indicating what the
term itself depends on (usually 'Root' if it is the real term you are interested in).
-}
termDeps ::
  ( DepGraph g
  , MonadReader (DepCtx tyname name uni fun a) m
  , PLC.HasUnique tyname PLC.TypeUnique
  , PLC.HasUnique name PLC.TermUnique
  , PLC.ToBuiltinMeaning uni fun
  ) =>
  Term tyname name uni fun a ->
  m g
termDeps :: forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique, HasUnique name TermUnique,
 ToBuiltinMeaning uni fun) =>
Term tyname name uni fun a -> m g
termDeps = \case
  Let a
_ Recursivity
_ NonEmpty (Binding tyname name uni fun a)
bs Term tyname name uni fun a
t -> do
    NonEmpty g
bGraphs <- (Binding tyname name uni fun a -> m g)
-> NonEmpty (Binding tyname name uni fun a) -> m (NonEmpty g)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse Binding tyname name uni fun a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique, HasUnique name TermUnique,
 ToBuiltinMeaning uni fun) =>
Binding tyname name uni fun a -> m g
bindingDeps NonEmpty (Binding tyname name uni fun a)
bs
    g
bodyGraph <- Term tyname name uni fun a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique, HasUnique name TermUnique,
 ToBuiltinMeaning uni fun) =>
Term tyname name uni fun a -> m g
termDeps Term tyname name uni fun a
t
    g -> m g
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (g -> m g) -> (NonEmpty g -> g) -> NonEmpty g -> m g
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [g] -> g
forall g. Graph g => [g] -> g
G.overlays ([g] -> g) -> (NonEmpty g -> [g]) -> NonEmpty g -> g
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty g -> [g]
forall a. NonEmpty a -> [a]
NE.toList (NonEmpty g -> m g) -> NonEmpty g -> m g
forall a b. (a -> b) -> a -> b
$ g
bodyGraph g -> NonEmpty g -> NonEmpty g
forall a. a -> NonEmpty a -> NonEmpty a
NE.<| NonEmpty g
bGraphs
  Var a
_ name
n -> [Unique] -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m) =>
[Unique] -> m g
currentDependsOn [name
n name -> Getting Unique name Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique name Unique
forall name unique. HasUnique name unique => Lens' name Unique
Lens' name Unique
PLC.theUnique]
  Term tyname name uni fun a
x -> do
    [g]
tds <- (Term tyname name uni fun a -> m g)
-> [Term tyname name uni fun a] -> m [g]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term tyname name uni fun a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique, HasUnique name TermUnique,
 ToBuiltinMeaning uni fun) =>
Term tyname name uni fun a -> m g
termDeps (Term tyname name uni fun a
x Term tyname name uni fun a
-> Getting
     (Endo [Term tyname name uni fun a])
     (Term tyname name uni fun a)
     (Term tyname name uni fun a)
-> [Term tyname name uni fun a]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. Getting
  (Endo [Term tyname name uni fun a])
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms)
    [g]
tyds <- (Type tyname uni a -> m g) -> [Type tyname uni a] -> m [g]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Type tyname uni a -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique) =>
Type tyname uni a -> m g
typeDeps (Term tyname name uni fun a
x Term tyname name uni fun a
-> Getting
     (Endo [Type tyname uni a])
     (Term tyname name uni fun a)
     (Type tyname uni a)
-> [Type tyname uni a]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. Getting
  (Endo [Type tyname uni a])
  (Term tyname name uni fun a)
  (Type tyname uni a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubtypes)
    g -> m g
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (g -> m g) -> g -> m g
forall a b. (a -> b) -> a -> b
$ [g] -> g
forall g. Graph g => [g] -> g
G.overlays ([g] -> g) -> [g] -> g
forall a b. (a -> b) -> a -> b
$ [g]
tds [g] -> [g] -> [g]
forall a. [a] -> [a] -> [a]
++ [g]
tyds

{- | Compute the dependency graph of a type. Takes an initial 'Node' indicating what
the type itself depends on (usually 'Root' if it is the real type you are interested in).
-}
typeDeps ::
  (DepGraph g, MonadReader (DepCtx tyname name uni fun a) m, PLC.HasUnique tyname PLC.TypeUnique) =>
  Type tyname uni a ->
  m g
typeDeps :: forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m,
 HasUnique tyname TypeUnique) =>
Type tyname uni a -> m g
typeDeps Type tyname uni a
ty =
  -- The dependency graph of a type is very simple since it doesn't have any internal
  -- let-bindings. So we just need to find all the used variables and mark them as
  -- dependencies of the current node.
  let used :: Set Unique
used = Usages -> Set Unique
Usages.allUsed (Usages -> Set Unique) -> Usages -> Set Unique
forall a b. (a -> b) -> a -> b
$ Type tyname uni a -> Usages
forall tyname (uni :: * -> *) a.
HasUnique tyname TypeUnique =>
Type tyname uni a -> Usages
Usages.typeUsages Type tyname uni a
ty
   in [Unique] -> m g
forall g tyname name (uni :: * -> *) fun a (m :: * -> *).
(DepGraph g, MonadReader (DepCtx tyname name uni fun a) m) =>
[Unique] -> m g
currentDependsOn (Set Unique -> [Unique]
forall a. Set a -> [a]
Set.toList Set Unique
used)