{-# LANGUAGE ConstraintKinds  #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs            #-}
{-# LANGUAGE LambdaCase       #-}
-- | 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, StrictnessMap, runTermDeps, runTypeDeps) where

import PlutusCore qualified as PLC
import PlutusCore.Builtin qualified as PLC
import PlutusCore.Name 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 Control.Monad.State

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

import Data.List.NonEmpty qualified as NE

import Data.Foldable

type DepCtx term = Node
type StrictnessMap = Map.Map PLC.Unique Strictness
type DepState = StrictnessMap

-- | 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
showList :: [Node] -> ShowS
$cshowList :: [Node] -> ShowS
show :: Node -> String
$cshow :: Node -> String
showsPrec :: Int -> Node -> ShowS
$cshowsPrec :: Int -> Node -> ShowS
Show, Node -> Node -> Bool
(Node -> Node -> Bool) -> (Node -> Node -> Bool) -> Eq Node
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Node -> Node -> Bool
$c/= :: Node -> Node -> Bool
== :: Node -> Node -> Bool
$c== :: 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
min :: Node -> Node -> Node
$cmin :: Node -> Node -> Node
max :: Node -> Node -> Node
$cmax :: Node -> Node -> Node
>= :: Node -> Node -> Bool
$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
compare :: Node -> Node -> Ordering
$ccompare :: Node -> Node -> Ordering
$cp1Ord :: Eq Node
Ord)

-- | 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)

varStrictnessFun ::
    (MonadState DepState m, PLC.HasUnique name u)
    => m (name -> Strictness)
varStrictnessFun :: m (name -> Strictness)
varStrictnessFun = do
    Map Unique Strictness
strictnessMap <- m (Map Unique Strictness)
forall s (m :: * -> *). MonadState s m => m s
get
    (name -> Strictness) -> m (name -> Strictness)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((name -> Strictness) -> m (name -> Strictness))
-> (name -> Strictness) -> m (name -> Strictness)
forall a b. (a -> b) -> a -> b
$ \name
n' -> Strictness -> Unique -> Map Unique Strictness -> Strictness
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Strictness
NonStrict (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
PLC.theUnique) Map Unique Strictness
strictnessMap

-- | 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)
    => Term tyname name uni fun a
    -> (g, StrictnessMap)
runTermDeps :: Term tyname name uni fun a -> (g, Map Unique Strictness)
runTermDeps Term tyname name uni fun a
t = (State (Map Unique Strictness) g
 -> Map Unique Strictness -> (g, Map Unique Strictness))
-> Map Unique Strictness
-> State (Map Unique Strictness) g
-> (g, Map Unique Strictness)
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (Map Unique Strictness) g
-> Map Unique Strictness -> (g, Map Unique Strictness)
forall s a. State s a -> s -> (a, s)
runState Map Unique Strictness
forall a. Monoid a => a
mempty (State (Map Unique Strictness) g -> (g, Map Unique Strictness))
-> State (Map Unique Strictness) g -> (g, Map Unique Strictness)
forall a b. (a -> b) -> a -> b
$ (ReaderT Node (StateT (Map Unique Strictness) Identity) g
 -> Node -> State (Map Unique Strictness) g)
-> Node
-> ReaderT Node (StateT (Map Unique Strictness) Identity) g
-> State (Map Unique Strictness) g
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT Node (StateT (Map Unique Strictness) Identity) g
-> Node -> State (Map Unique Strictness) g
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Node
Root (ReaderT Node (StateT (Map Unique Strictness) Identity) g
 -> State (Map Unique Strictness) g)
-> ReaderT Node (StateT (Map Unique Strictness) Identity) g
-> State (Map Unique Strictness) g
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun a
-> ReaderT Node (StateT (Map Unique Strictness) Identity) g
forall g term (m :: * -> *) tyname name (uni :: * -> *) fun a.
(DepGraph g, MonadReader Node m,
 MonadState (Map Unique Strictness) 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

-- | Compute the dependency graph of a 'Type'. The 'Root' node will correspond to the type itself.
--
-- This graph will always be simply a star from 'Root', since types have no internal let-bindings.
--
-- For example, the graph of @(all a (type) [f a])@ is:
-- @
--     ROOT -> f
--     ROOT -> a
-- @
--
runTypeDeps
    :: (DepGraph g, PLC.HasUnique tyname PLC.TypeUnique)
    => Type tyname uni a
    -> g
runTypeDeps :: Type tyname uni a -> g
runTypeDeps Type tyname uni a
t = (Reader Node g -> Node -> g) -> Node -> Reader Node g -> g
forall a b c. (a -> b -> c) -> b -> a -> c
flip Reader Node g -> Node -> g
forall r a. Reader r a -> r -> a
runReader Node
Root (Reader Node g -> g) -> Reader Node g -> g
forall a b. (a -> b) -> a -> b
$ Type tyname uni a -> Reader Node g
forall g term (m :: * -> *) tyname (uni :: * -> *) a.
(DepGraph g, MonadReader Node m, HasUnique tyname TypeUnique) =>
Type tyname uni a -> m g
typeDeps Type tyname uni a
t

-- | Record some dependencies on the current node.
currentDependsOn
    :: (DepGraph g, MonadReader (DepCtx term) m)
    => [PLC.Unique]
    -> m g
currentDependsOn :: [Unique] -> m g
currentDependsOn [Unique]
us = do
    Node
current <- m Node
forall r (m :: * -> *). MonadReader r m => m r
ask
    g -> m g
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 (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 term) m, PLC.HasUnique n u)
    => n
    -> m g
    -> m g
withCurrent :: n -> m g -> m g
withCurrent n
n = (Node -> Node) -> m g -> m g
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Node -> Node) -> m g -> m g) -> (Node -> Node) -> m g -> m g
forall a b. (a -> b) -> a -> b
$ \Node
_ -> 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
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 term) m, MonadState DepState m, PLC.HasUnique tyname PLC.TypeUnique, PLC.HasUnique name PLC.TermUnique,
       PLC.ToBuiltinMeaning uni fun)
    => Binding tyname name uni fun a
    -> m g
bindingDeps :: 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 fun a
d@(VarDecl a
_ name
n Type tyname uni a
_) Term tyname name uni fun a
rhs -> do
        g
vDeps <- VarDecl tyname name uni fun a -> m g
forall g term (m :: * -> *) tyname name (uni :: * -> *) fun a.
(DepGraph g, MonadReader Node m, HasUnique tyname TypeUnique,
 HasUnique name TermUnique) =>
VarDecl tyname name uni fun a -> m g
varDeclDeps VarDecl tyname name uni fun a
d
        g
tDeps <- name -> m g -> m g
forall term (m :: * -> *) n u g.
(MonadReader Node 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 term (m :: * -> *) tyname name (uni :: * -> *) fun a.
(DepGraph g, MonadReader Node m,
 MonadState (Map Unique Strictness) 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

        -- See Note [Strict term bindings and dependencies]
        name -> Strictness
strictnessFun <- m (name -> Strictness)
forall (m :: * -> *) name u.
(MonadState (Map Unique Strictness) m, HasUnique name u) =>
m (name -> Strictness)
varStrictnessFun
        g
evalDeps <- case Strictness
strictness of
            Strictness
Strict | Bool -> Bool
not ((name -> Strictness) -> Term tyname name uni fun a -> Bool
forall (uni :: * -> *) fun name tyname a.
ToBuiltinMeaning uni fun =>
(name -> Strictness) -> Term tyname name uni fun a -> Bool
isPure name -> Strictness
strictnessFun Term tyname name uni fun a
rhs) -> [Unique] -> m g
forall g term (m :: * -> *).
(DepGraph g, MonadReader Node 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
PLC.theUnique]
            Strictness
_                                       -> g -> m g
forall (f :: * -> *) a. Applicative f => a -> f a
pure g
forall g. Graph g => g
G.empty

        g -> m g
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 term (m :: * -> *) tyname a.
(Graph g, MonadReader Node m) =>
TyVarDecl tyname a -> m g
tyVarDeclDeps TyVarDecl tyname a
d
        g
tDeps <- tyname -> m g -> m g
forall term (m :: * -> *) n u g.
(MonadReader Node 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 term (m :: * -> *) tyname (uni :: * -> *) a.
(DepGraph g, MonadReader Node m, HasUnique tyname TypeUnique) =>
Type tyname uni a -> m g
typeDeps Type tyname uni a
rhs
        g -> m g
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 fun a]
constrs) -> do
        -- See Note [Dependencies for datatype bindings, and pruning them]
        g
vDeps <- TyVarDecl tyname a -> m g
forall g term (m :: * -> *) tyname a.
(Graph g, MonadReader Node 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)
traverse TyVarDecl tyname a -> m g
forall g term (m :: * -> *) tyname a.
(Graph g, MonadReader Node m) =>
TyVarDecl tyname a -> m g
tyVarDeclDeps [TyVarDecl tyname a]
tvs
        [g]
cstrDeps <- (VarDecl tyname name uni fun a -> m g)
-> [VarDecl tyname name uni fun a] -> m [g]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse VarDecl tyname name uni fun a -> m g
forall g term (m :: * -> *) tyname name (uni :: * -> *) fun a.
(DepGraph g, MonadReader Node m, HasUnique tyname TypeUnique,
 HasUnique name TermUnique) =>
VarDecl tyname name uni fun a -> m g
varDeclDeps [VarDecl tyname name uni fun 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 term (m :: * -> *) n u g.
(MonadReader Node 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 fun a -> m g)
-> [VarDecl tyname name uni fun a] -> m [g]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type tyname uni a -> m g
forall g term (m :: * -> *) tyname (uni :: * -> *) a.
(DepGraph g, MonadReader Node m, HasUnique tyname TypeUnique) =>
Type tyname uni a -> m g
typeDeps (Type tyname uni a -> m g)
-> (VarDecl tyname name uni fun a -> Type tyname uni a)
-> VarDecl tyname name uni fun a
-> m g
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDecl tyname name uni fun a -> Type tyname uni a
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> Type tyname uni ann
_varDeclType) [VarDecl tyname name uni fun a]
constrs)
        let tus :: [Unique]
tus = (name -> Unique) -> [name] -> [Unique]
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
PLC.theUnique) (name
destr name -> [name] -> [name]
forall a. a -> [a] -> [a]
: (VarDecl tyname name uni fun a -> name)
-> [VarDecl tyname name uni fun a] -> [name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VarDecl tyname name uni fun a -> name
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> name
_varDeclName [VarDecl tyname name uni fun 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Unique -> Node
Variable [Unique]
tus)
        g -> m g
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]

bindingStrictness
    :: (MonadState DepState m, PLC.HasUnique name PLC.TermUnique)
    => Binding tyname name uni fun a
    -> m ()
bindingStrictness :: Binding tyname name uni fun a -> m ()
bindingStrictness Binding tyname name uni fun a
b = case Binding tyname name uni fun a
b of
    TermBind a
_ Strictness
strictness (VarDecl a
_ name
n Type tyname uni a
_) Term tyname name uni fun a
_ -> (Map Unique Strictness -> Map Unique Strictness) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Unique
-> Strictness -> Map Unique Strictness -> Map Unique Strictness
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (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
PLC.theUnique) Strictness
strictness)
    TypeBind {} -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    DatatypeBind a
_ (Datatype a
_ TyVarDecl tyname a
_ [TyVarDecl tyname a]
_ name
destr [VarDecl tyname name uni fun a]
constrs) -> do
        -- Constructors and destructor are bound strictly
        [VarDecl tyname name uni fun a]
-> (VarDecl tyname name uni fun a -> m ()) -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [VarDecl tyname name uni fun a]
constrs ((VarDecl tyname name uni fun a -> m ()) -> m ())
-> (VarDecl tyname name uni fun a -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \(VarDecl a
_ name
n Type tyname uni a
_) -> (Map Unique Strictness -> Map Unique Strictness) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Unique
-> Strictness -> Map Unique Strictness -> Map Unique Strictness
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (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
PLC.theUnique) Strictness
Strict)
        (Map Unique Strictness -> Map Unique Strictness) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Unique
-> Strictness -> Map Unique Strictness -> Map Unique Strictness
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (name
destr 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
PLC.theUnique) Strictness
Strict)

varDeclDeps
    :: (DepGraph g, MonadReader (DepCtx term) m, PLC.HasUnique tyname PLC.TypeUnique, PLC.HasUnique name PLC.TermUnique)
    => VarDecl tyname name uni fun a
    -> m g
varDeclDeps :: VarDecl tyname name uni fun a -> m g
varDeclDeps (VarDecl a
_ name
n Type tyname uni a
ty) = name -> m g -> m g
forall term (m :: * -> *) n u g.
(MonadReader Node 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 term (m :: * -> *) tyname (uni :: * -> *) a.
(DepGraph g, MonadReader Node 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 term) m)
    => TyVarDecl tyname a
    -> m g
tyVarDeclDeps :: TyVarDecl tyname a -> m g
tyVarDeclDeps TyVarDecl tyname a
_ = g -> m g
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 term) m, MonadState DepState m, PLC.HasUnique tyname PLC.TypeUnique, PLC.HasUnique name PLC.TermUnique,
       PLC.ToBuiltinMeaning uni fun)
    => Term tyname name uni fun a
    -> m g
termDeps :: 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
        -- Need to do this before processing the RHSs of the bindings, as recursive bindings may need to know about
        -- the strictnesses of other variables.
        (Binding tyname name uni fun a -> m ())
-> NonEmpty (Binding tyname name uni fun a) -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Binding tyname name uni fun a -> m ()
forall (m :: * -> *) name tyname (uni :: * -> *) fun a.
(MonadState (Map Unique Strictness) m,
 HasUnique name TermUnique) =>
Binding tyname name uni fun a -> m ()
bindingStrictness NonEmpty (Binding tyname name uni fun a)
bs
        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)
traverse Binding tyname name uni fun a -> m g
forall g term (m :: * -> *) tyname name (uni :: * -> *) fun a.
(DepGraph g, MonadReader Node m,
 MonadState (Map Unique Strictness) 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 term (m :: * -> *) tyname name (uni :: * -> *) fun a.
(DepGraph g, MonadReader Node m,
 MonadState (Map Unique Strictness) 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 (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 term (m :: * -> *).
(DepGraph g, MonadReader Node 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
PLC.theUnique]
    LamAbs a
_ name
n Type tyname uni a
ty Term tyname name uni fun a
t -> do
        -- Record that lambda-bound variables are strict
        (Map Unique Strictness -> Map Unique Strictness) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Unique
-> Strictness -> Map Unique Strictness -> Map Unique Strictness
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (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
PLC.theUnique) Strictness
Strict)
        g
tds <- Term tyname name uni fun a -> m g
forall g term (m :: * -> *) tyname name (uni :: * -> *) fun a.
(DepGraph g, MonadReader Node m,
 MonadState (Map Unique Strictness) 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
tyds <- Type tyname uni a -> m g
forall g term (m :: * -> *) tyname (uni :: * -> *) a.
(DepGraph g, MonadReader Node m, HasUnique tyname TypeUnique) =>
Type tyname uni a -> m g
typeDeps Type tyname uni a
ty
        g -> m g
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
tds, g
tyds]
    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)
traverse Term tyname name uni fun a -> m g
forall g term (m :: * -> *) tyname name (uni :: * -> *) fun a.
(DepGraph g, MonadReader Node m,
 MonadState (Map Unique Strictness) 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.
Traversal'
  (Term tyname name uni fun a) (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)
traverse Type tyname uni a -> m g
forall g term (m :: * -> *) tyname (uni :: * -> *) a.
(DepGraph g, MonadReader Node 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.
Traversal' (Term tyname name uni fun a) (Type tyname uni a)
termSubtypes)
        g -> m g
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 term) m, PLC.HasUnique tyname PLC.TypeUnique)
    => Type tyname uni a
    -> m g
typeDeps :: 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.runTypeUsages Type tyname uni a
ty
    in [Unique] -> m g
forall g term (m :: * -> *).
(DepGraph g, MonadReader Node m) =>
[Unique] -> m g
currentDependsOn (Set Unique -> [Unique]
forall a. Set a -> [a]
Set.toList Set Unique
used)