-- | This module contains functions to construct dependency graphs of
--   declarations and modules of the intermediate language. A dependency graph
--   is a directed graph whose nodes are labeled with declarations. There is an
--   edge from node @A@ to @B@ if the declaration of @A@ depends on the
--   declaration of @B@ (i.e. in Coq @B@ has to be defined before @A@ or both
--   have to be declared in the same sentence). The module dependency graph
--   contains an edge from node @A@ to @B@ if the module of @A@ contains an
--   @import@ declaration for the module of @B@.
--
--   The dependency graph does only contain defined top-level declarations
--   (i.e. there are no nodes for imported or built-in data types or operations
--   and there are no nodes for local variables such as function parameters or
--   variable patterns). However, the entries of the dependency graph contain
--   keys for predefined functions (but not local variables) as well as the
--   special functions @error@ and @undefined@ that are used in error terms.
--
--   We distinguish between the type and value dependency graph.
--   This is because function declarations and type declarations
--   live in separate scopes but we want to avoid name conflicts.
--   Since we assume all type declarations to precede function declarations
--   in the generated Coq code, this separation of the dependency graphs
--   should not be a problem. For the same reason, the value dependency
--   graph does not include nodes for constructors (as always, the keys of
--   used constructors are still present).
--
--   The construction of a dependency graph does not fail even if there are
--   are undefined identifiers. The dependency graph does not know about the
--   environment, it only knows which (type) constructors and (type) variables
--   occur freely in the declarations. Most importantly, that means that it
--   does not know about the module system. Thus, dependency analysis should
--   not be performed before all references have been resolved to their
--   original (qualified) identifiers.
--
--   For debugging purposes, dependency graphs can be converted to the DOT
--   format such that they can be visualized using Graphviz
--   (See <https://www.graphviz.org/>).
module FreeC.IR.DependencyGraph
  ( -- * Dependency Graph
    DGKey
  , DGEntry
  , DependencyGraph(..)
    -- ** Getters
  , dgEntries
    -- ** Predicates
  , dependsDirectlyOn
    -- ** Constructors
  , typeDependencyGraph
  , valueDependencyGraph
  , moduleDependencyGraph
    -- * Strongly Connected Components
  , DependencyComponent(..)
  , unwrapComponent
    -- ** Constructors
  , dependencyComponents
  , typeDependencyComponents
  , valueDependencyComponents
  , groupModules
    -- ** Manipulating
  , mapComponent
  , mapComponentM
  , mapComponentM_
  ) where

import           Control.Monad      ( liftM2, void )
import           Control.Monad.Fail ( MonadFail )
import           Data.Graph
import           Data.Maybe         ( mapMaybe )
import           Data.Tuple.Extra

import           FreeC.IR.Reference ( HasRefs, typeRefs, valueRefs )
import qualified FreeC.IR.Syntax    as IR
import           FreeC.Pretty

-------------------------------------------------------------------------------
-- Dependency Graph                                                          --
-------------------------------------------------------------------------------
-- | Every node of the dependency graph is uniquely identified by a key.
--   We use their qualified original name to identify declarations.
type DGKey = IR.QName

-- | Every node (i.e., declaration) in a dependency graph is associated with a
--   unique key (its qualified original name) and a list of keys that identify
--   the nodes this node depends on (adjacency list).
type DGEntry node = (node, DGKey, [DGKey])

-- | A dependency graph is a directed graph whose nodes are declarations
--   (Usually 'IR.TypeDecl' or 'IR.FuncDecl'). There is an edge from node
--   @A@ to node @B@ if the declaration of @A@ depends on @B@.
--
--   Nodes are identified by their qualified original name (See 'DGKey').
--   Internally, nodes are identified by a number (See 'Vertex').
--
--   In addition to the actual 'Graph' that stores the adjacency matrix
--   of the internal identifiers, this data type contains functions to convert
--   between the internal and high level representation.
data DependencyGraph node = DependencyGraph
  { dgGraph     :: Graph
    -- ^ The actual graph.
  , dgGetEntry  :: Vertex -> DGEntry node
    -- ^ Gets an entry for a vertex of the graph.
  , dgGetVertex :: DGKey -> Maybe Vertex
    -- ^ Gets the vertex of a node with the given key.
  }

-------------------------------------------------------------------------------
-- Getters                                                                   --
-------------------------------------------------------------------------------
-- | Gets the entries of the given dependency graph.
dgEntries :: DependencyGraph node -> [DGEntry node]
dgEntries = liftM2 map dgGetEntry dgVertices

-- | Gets the vertices of the given dependency graph.
dgVertices :: DependencyGraph node -> [Vertex]
dgVertices = vertices . dgGraph

-- | Gets the edges of the given dependency graph.
dgEdges :: DependencyGraph node -> [(Vertex, Vertex)]
dgEdges = edges . dgGraph

-------------------------------------------------------------------------------
-- Predicates                                                                --
-------------------------------------------------------------------------------
-- | Tests whether two nodes (identified by the given keys) of the dependency
--   graph depend on each other directly (i.e., there is an edge from the
--   first node to the second node).
--
--   Returns @False@ if one of the nodes does not exist.
dependsDirectlyOn :: DependencyGraph node -- ^ The dependency graph.
                  -> DGKey                -- ^ The key of the first node.
                  -> DGKey                -- ^ The key of the second node.
                  -> Bool
dependsDirectlyOn graph k1 k2 = containsEdge == Just True
 where
  containsEdge :: Maybe Bool
  containsEdge = do
    v1 <- dgGetVertex graph k1
    v2 <- dgGetVertex graph k2
    return ((v1, v2) `elem` dgEdges graph)

-------------------------------------------------------------------------------
-- Type Dependencies                                                         --
-------------------------------------------------------------------------------
-- | Creates the type dependency graph for a list of nodes.
typeDependencyGraph
  :: (HasRefs node, IR.HasDeclIdent node) => [node] -> DependencyGraph node
typeDependencyGraph = uncurry3 DependencyGraph . graphFromEdges . map typeEntry

-- | Creates an entry of the type dependency graph.
typeEntry :: (HasRefs node, IR.HasDeclIdent node) => node -> DGEntry node
typeEntry node = (node, IR.declQName node, typeRefs node)

-------------------------------------------------------------------------------
-- Function Dependencies                                                     --
-------------------------------------------------------------------------------
-- | Creates the dependency graph for a list of function declarations.
valueDependencyGraph
  :: (HasRefs node, IR.HasDeclIdent node) => [node] -> DependencyGraph node
valueDependencyGraph
  = uncurry3 DependencyGraph . graphFromEdges . map valueEntry

-- | Creates an entry of the dependency graph for the given function
--   declaration or pattern binding.
valueEntry :: (HasRefs node, IR.HasDeclIdent node) => node -> DGEntry node
valueEntry node = (node, IR.declQName node, valueRefs node)

-------------------------------------------------------------------------------
-- Module Dependencies                                                       --
-------------------------------------------------------------------------------
-- | Creates the dependency graph for the given modules.
moduleDependencyGraph
  :: [IR.ModuleOf decls] -> DependencyGraph (IR.ModuleOf decls)
moduleDependencyGraph
  = uncurry3 DependencyGraph . graphFromEdges . map moduleEntries

-- | Creates an entry of the dependency graph for the given module.
moduleEntries :: IR.ModuleOf decls -> DGEntry (IR.ModuleOf decls)
moduleEntries decl
  = ( decl
    , IR.UnQual (IR.Ident (IR.modName decl))
    , map (IR.UnQual . IR.Ident . IR.importName) (IR.modImports decl)
    )

-------------------------------------------------------------------------------
-- Pretty Print Dependency Graph                                             --
-------------------------------------------------------------------------------
-- | Pretty instance that converts a dependency graph to the DOT format.
instance Pretty (DependencyGraph node) where
  pretty (DependencyGraph graph getEntry getVertex) = digraph
    <+> braces (line <> indent 2 (vcat (nodeDocs ++ edgesDocs)) <> line)
    <> line
   where
    -- | A document for the DOT digraph keyword.
    digraph :: Doc
    digraph = prettyString "digraph"

    -- | A document for the DOT label attribute.
    label :: Doc
    label = prettyString "label"

    -- | A document for the DOT arrow symbol.
    arrow :: Doc
    arrow = prettyString "->"

    -- | Pretty printed DOT nodes for the dependency graph.
    nodeDocs :: [Doc]
    nodeDocs = map prettyNode (vertices graph)

    -- | Pretty prints the given vertex as a DOT command. The key of the node
    --   is used a the label.
    prettyNode :: Vertex -> Doc
    prettyNode v
      = let (_, key, _) = getEntry v
        in int v <+> brackets (label <> equals <> dquotes (pretty key)) <> semi

    -- | Pretty printed DOT edges for the dependency graph.
    edgesDocs :: [Doc]
    edgesDocs = mapMaybe prettyEdges (vertices graph)

    -- | Pretty prints all outgoing edges of the given vertex as a single
    --   DOT command. Returns 'Nothing' if the vertex is not incident to
    --   any edge.
    prettyEdges :: Vertex -> Maybe Doc
    prettyEdges v
      = let (_, _, neighbors) = getEntry v
        in case mapMaybe getVertex neighbors of
             [] -> Nothing
             vs -> Just
               $ int v
               <+> arrow
               <+> braces (cat (punctuate comma (map int vs))) <> semi

-------------------------------------------------------------------------------
-- Strongly Connected Components                                             --
-------------------------------------------------------------------------------
-- | A strongly connected component of the dependency graph.
--
--   All declarations that mutually depend on each other are in the same
--   strongly connected component.
--
--   The only difference to @'SCC' decl@ is that the constructors have been
--   renamed to be more explanatory in the context of dependency analysis.
data DependencyComponent decl
  = NonRecursive decl -- ^ A single non-recursive declaration.
  | Recursive [decl]  -- ^ A list of mutually recursive declarations.
 deriving Show

-- | Gets the declarations wrapped by the given strongly connected component.
unwrapComponent :: DependencyComponent decl -> [decl]
unwrapComponent (NonRecursive decl) = [decl]
unwrapComponent (Recursive decls)   = decls

-------------------------------------------------------------------------------
-- Constructing SCCs                                                         --
-------------------------------------------------------------------------------
-- | Computes the strongly connected components of the given dependency graph.
--
--   Each strongly connected component corresponds either to a set of mutually
--   recursive declarations or a single non-recursive declaration.
--
--   The returned list of strongly connected components is in reverse
--   topological order, i.e. if any declaration in a strongly connected
--   component @B@ depends on a declaration in a strongly connected component
--   @A@, then @A@ precedes @B@ in the returned list.
--
--   If two components do not depend on each other, they are in reverse
--   alphabetical order.
dependencyComponents :: DependencyGraph a -> [DependencyComponent a]
dependencyComponents = map convertSCC . stronglyConnComp . dgEntries
 where
  -- | Converts a strongly connected component from @Data.Graph@ to a
  --   'DependencyComponent'.
  convertSCC :: SCC decl -> DependencyComponent decl
  convertSCC (AcyclicSCC decl) = NonRecursive decl
  convertSCC (CyclicSCC decls) = Recursive decls

-- | Combines the construction of the type dependency graph with the
--   computation of strongly connected components.
typeDependencyComponents :: (HasRefs node, IR.HasDeclIdent node)
                         => [node]
                         -> [DependencyComponent node]
typeDependencyComponents = dependencyComponents . typeDependencyGraph

-- | Combines the construction of the value dependency graph with the
--   computation of strongly connected components.
valueDependencyComponents :: (HasRefs node, IR.HasDeclIdent node)
                          => [node]
                          -> [DependencyComponent node]
valueDependencyComponents = dependencyComponents . valueDependencyGraph

-- | Combines the construction of the dependency graph for the given
--   modules (See 'moduleDependencyGraph') with the computation of strongly
--   connected components.
--
--   Since cyclic module dependencies are not allowed, all
--   'DependencyComponent's in the returned list should be 'NonRecursive'.
--   Otherwise, there is a module dependency error.
groupModules :: [IR.ModuleOf decls]
             -> [DependencyComponent (IR.ModuleOf decls)]
groupModules = dependencyComponents . moduleDependencyGraph

-------------------------------------------------------------------------------
-- Manipulating SCCs                                                         --
-------------------------------------------------------------------------------
-- | Applies the given function to the declarations in the given strongly
--   connected component of the dependency graph.
--
--   In case of a 'NonRecursive' component, the function is given a singleton
--   list. The given function must not change the number of declarations in the
--   component.
mapComponent :: ([decl] -> [decl'])
             -> DependencyComponent decl
             -> DependencyComponent decl'
mapComponent f (NonRecursive decl) = let [decl'] = f [decl]
                                     in NonRecursive decl'
mapComponent f (Recursive decls)   = Recursive (f decls)

-- | Monadic version of 'mapComponent'.
--
--   There must be a 'MonadFail' instance since this function fails if the
--   given function changes the number of declarations in a non-recursive
--   strongly connected component.
mapComponentM :: MonadFail m
              => ([decl] -> m [decl'])
              -> DependencyComponent decl
              -> m (DependencyComponent decl')
mapComponentM f (NonRecursive decl) = do
  [decl'] <- f [decl]
  return (NonRecursive decl')
mapComponentM f (Recursive decls)   = Recursive <$> f decls

-- | Like 'mapComponentM' but discards the result.
mapComponentM_
  :: MonadFail m => ([decl] -> m a) -> DependencyComponent decl -> m ()
mapComponentM_ f (NonRecursive decl) = void (f [decl])
mapComponentM_ f (Recursive decls)   = void (f decls)

-------------------------------------------------------------------------------
-- Pretty Print SCCs                                                         --
-------------------------------------------------------------------------------
-- | Pretty instance that pretty prints the declarations of a strongly
--   connected component.
--
--   Each declaration is on its own line and indented by two spaces.
--   The first line of the document indicates whether the component
--   was recursive or not.
instance Pretty decl => Pretty (DependencyComponent decl) where
  pretty (NonRecursive decl) = prettyString "non-recursive"
    <$$> indent 2 (pretty decl)
  pretty (Recursive decls)   = prettyString "recursive"
    <$$> indent 2 (vcat (map pretty decls))