content: 
  -- | This module contains the types for representing dependency
  --   graphs between kvars and constraints.
  
  {-# LANGUAGE ImplicitParams        #-}
  {-# LANGUAGE DeriveGeneric     #-}
  {-# LANGUAGE OverloadedStrings #-}
  
  module Language.Fixpoint.Graph.Types (
  
    -- * Graphs
      CVertex (..)
    , CEdge
    , isRealEdge
    , KVGraph (..)
  
    -- * Components
    , Comps
    , KVComps
  
    -- * Printing
    , writeGraph
    , writeEdges
  
    -- * Constraints
    , F.SubcId
    , KVRead
    , DepEdge
  
    -- * Slice of relevant constraints
    , Slice (..)
  
    -- * Constraint Dependency Graphs
    , CGraph (..)
  
    -- * Alias for Constraint Maps
    , F.CMap
    , lookupCMap
  
    -- * Ranks
    , Rank (..)
  
    -- * Constraint Dependencies
    , CDeps (..)
  
    -- * Solver Info
    , SolverInfo (..)
    )
    where
  
  import           GHC.Generics              (Generic)
  import           Data.Hashable
  import           Text.PrettyPrint.HughesPJ.Compat
  
  import           Language.Fixpoint.Misc         -- hiding (group)
  import           Language.Fixpoint.Types.PrettyPrint
  import           Language.Fixpoint.Types.Refinements -- Constraints
  import qualified Language.Fixpoint.Types.Solutions as F
  -- import           Language.Fixpoint.Misc (safeLookup)
  import qualified Language.Fixpoint.Types   as F
  import qualified Data.HashMap.Strict       as M
  import qualified Data.HashSet              as S
  
  import GHC.Stack
  --------------------------------------------------------------------------------
  
  data CVertex = KVar  !KVar    -- ^ real kvar vertex
               | DKVar !KVar    -- ^ dummy to ensure each kvar has a successor
               | EBind !F.Symbol  -- ^ existentially bound "ghost paramter" to solve for
               | Cstr  !Integer -- ^ constraint-id which creates a dependency
                 deriving (Eq, Ord, Show, Generic)
  
  instance PPrint CVertex where
    pprintTidy _ (KVar k)  = doubleQuotes $ pprint $ kv k
    pprintTidy _ (EBind s)  = doubleQuotes $ pprint s
    pprintTidy _ (Cstr i)  = text "id_" <-> pprint i
    pprintTidy _ (DKVar k) = pprint k   <-> text "*"
  
  
  instance Hashable CVertex
  
  newtype KVGraph = KVGraph { kvgEdges :: [(CVertex, CVertex, [CVertex])] }
  type CEdge      = (CVertex, CVertex)
  type Comps a    = [[a]]
  type KVComps    = Comps CVertex
  
  instance PPrint KVGraph where
    pprintTidy _ = pprint . kvgEdges
  
  --------------------------------------------------------------------------------
  writeGraph :: FilePath -> KVGraph -> IO ()
  --------------------------------------------------------------------------------
  writeGraph f = writeEdges f . graphEdges
    where
      graphEdges :: KVGraph -> [CEdge]
      graphEdges (KVGraph g) = [ (v, v') | (v,_,vs) <- g, v' <- vs]
  
  --------------------------------------------------------------------------------
  writeEdges :: FilePath -> [CEdge] -> IO ()
  --------------------------------------------------------------------------------
  writeEdges f = writeFile f . render . ppEdges
  
  ppEdges :: [CEdge] -> Doc
  ppEdges             = vcat . wrap ["digraph Deps {"] ["}"]
                             . map ppE
                             . (if True then filter isRealEdge else txEdges)  -- RJ: use this to collapse "constraint" vertices
    where
      ppE (v, v')     = pprint v <+> "->" <+> pprint v'
  
  isRealEdge :: CEdge -> Bool
  isRealEdge (DKVar _, _)     = False
  isRealEdge (_, DKVar _)     = False
  isRealEdge (Cstr _, Cstr _) = False
  isRealEdge _                = True
  
  txEdges    :: [CEdge] -> [CEdge]
  txEdges es = concatMap iEs is
    where
      is     = [i | (Cstr i, Cstr _) <- es]
      kvInM  = group [ (i, k) | (KVar k, Cstr i) <- es]
      kvOutM = group [ (i, k') | (Cstr i, KVar k') <- es]
      ins i  = M.lookupDefault [] i kvInM
      outs i = M.lookupDefault [] i kvOutM
      iEs i  = case (ins i, outs i) of
                   (ks, [] ) -> [(KVar k, Cstr i ) | k  <- ks ]
                   ([], ks') -> [(Cstr i, KVar k') | k' <- ks']
                   (ks, ks') -> [(KVar k, KVar k') | k  <- ks, k' <- ks']
  
  
  
  ---------------------------------------------------------------------------
  -- | Dramatis Personae
  ---------------------------------------------------------------------------
  type KVRead  = M.HashMap F.KVar [F.SubcId]
  -- | (Constraint id, vertex key, edges to other constraints)
  --
  -- The vertex key is always equal to the constraint id. The redundancy
  -- is imposed by how @containers:Data.Graph@ requires graphs to be created.
  type DepEdge = (F.SubcId, F.SubcId, [F.SubcId])
  
  data Slice = Slice { slKVarCs :: [F.SubcId]     -- ^ F.SubcIds that transitively "reach" below
                     , slConcCs :: [F.SubcId]     -- ^ F.SubcIds with Concrete RHS
                     , slEdges  :: [DepEdge] -- ^ Dependencies between slKVarCs
                     } deriving (Eq, Show)
  
  data CGraph = CGraph
    { gEdges :: [DepEdge]
      -- | Maps a constraint id to an index identifying the strongly connected
      -- component to which it belongs.
      -- The scc indices correspond with a topological ordering of the sccs.
    , gRanks :: !(F.CMap Int)
      -- | Tells for each constraint C, which constraints read any kvars that
      -- C writes.
      --
      -- This is redundant with 'gEdges', so both fields need to express the
      -- exact same dependencies.
    , gSucc  :: !(F.CMap [F.SubcId])
      -- | Amount of strongly connected components
    , gSccs  :: !Int
    }
  
  ---------------------------------------------------------------------------
  -- | CMap API -------------------------------------------------------------
  ---------------------------------------------------------------------------
  lookupCMap :: (?callStack :: CallStack) => F.CMap a -> F.SubcId -> a
  lookupCMap rm i = safeLookup err i rm
    where
      err      = "lookupCMap: cannot find info for " ++ show i
  
  --------------------------------------------------------------------------------
  -- | Constraint Dependencies ---------------------------------------------------
  --------------------------------------------------------------------------------
  
  data CDeps = CDs { cSucc   :: !(F.CMap [F.SubcId]) -- ^ Constraints *written by* a SubcId
                   , cPrev   :: !(F.CMap [F.KVar])   -- ^ (Cut) KVars *read by*    a SubcId
                   , cRank   :: !(F.CMap Rank)       -- ^ SCC rank of a SubcId
                   , cNumScc :: !Int                 -- ^ Total number of Sccs
                   }
  
  
  -- | Ranks ---------------------------------------------------------------------
  
  data Rank = Rank { rScc  :: !Int    -- ^ SCC number with ALL dependencies
                   , rIcc  :: !Int    -- ^ SCC number without CUT dependencies
                   , rTag  :: !F.Tag  -- ^ The constraint's Tag
                   } deriving (Eq, Show)
  
  instance PPrint Rank where
    pprintTidy _ = text . show
  
  --------------------------------------------------------------------------------
  -- | `SolverInfo` contains all the stuff needed to produce a result, and is the
  --   the essential ingredient of the state needed by solve_
  --------------------------------------------------------------------------------
  data SolverInfo a b = SI
    { siSol     :: !(F.Sol b F.QBind)             -- ^ the initial solution
    , siQuery   :: !(F.SInfo a)                   -- ^ the whole input query
    , siDeps    :: !CDeps                         -- ^ dependencies between constraints/ranks etc.
    , siVars    :: !(S.HashSet F.KVar)            -- ^ set of KVars to actually solve for
    }
  