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

instance PPrint CVertex where
  pprintTidy :: Tidy -> CVertex -> Doc
pprintTidy Tidy
_ (KVar KVar
k)  = Doc -> Doc
doubleQuotes forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ KVar -> Symbol
kv KVar
k
  pprintTidy Tidy
_ (EBind Symbol
s)  = Doc -> Doc
doubleQuotes forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> Doc
pprint Symbol
s
  pprintTidy Tidy
_ (Cstr Integer
i)  = String -> Doc
text String
"id_" Doc -> Doc -> Doc
<-> forall a. PPrint a => a -> Doc
pprint Integer
i
  pprintTidy Tidy
_ (DKVar KVar
k) = forall a. PPrint a => a -> Doc
pprint KVar
k   Doc -> Doc -> Doc
<-> String -> Doc
text String
"*"


instance Hashable CVertex

newtype KVGraph = KVGraph { KVGraph -> [(CVertex, CVertex, [CVertex])]
kvgEdges :: [(CVertex, CVertex, [CVertex])] }
type CEdge      = (CVertex, CVertex)
type Comps a    = [[a]]
type KVComps    = Comps CVertex

instance PPrint KVGraph where
  pprintTidy :: Tidy -> KVGraph -> Doc
pprintTidy Tidy
_ = forall a. PPrint a => a -> Doc
pprint forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVGraph -> [(CVertex, CVertex, [CVertex])]
kvgEdges

--------------------------------------------------------------------------------
writeGraph :: FilePath -> KVGraph -> IO ()
--------------------------------------------------------------------------------
writeGraph :: String -> KVGraph -> IO ()
writeGraph String
f = String -> [CEdge] -> IO ()
writeEdges String
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVGraph -> [CEdge]
graphEdges
  where
    graphEdges :: KVGraph -> [CEdge]
    graphEdges :: KVGraph -> [CEdge]
graphEdges (KVGraph [(CVertex, CVertex, [CVertex])]
g) = [ (CVertex
v, CVertex
v') | (CVertex
v,CVertex
_,[CVertex]
vs) <- [(CVertex, CVertex, [CVertex])]
g, CVertex
v' <- [CVertex]
vs]

--------------------------------------------------------------------------------
writeEdges :: FilePath -> [CEdge] -> IO ()
--------------------------------------------------------------------------------
writeEdges :: String -> [CEdge] -> IO ()
writeEdges String
f = String -> String -> IO ()
writeFile String
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. [CEdge] -> Doc
ppEdges

ppEdges :: [CEdge] -> Doc
ppEdges :: [CEdge] -> Doc
ppEdges             = [Doc] -> Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a] -> [a] -> [a]
wrap [Doc
"digraph Deps {"] [Doc
"}"]
                           forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. (PPrint a, PPrint a) => (a, a) -> Doc
ppE
                           forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Bool
True then forall a. (a -> Bool) -> [a] -> [a]
filter CEdge -> Bool
isRealEdge else [CEdge] -> [CEdge]
txEdges)  -- RJ: use this to collapse "constraint" vertices
  where
    ppE :: (a, a) -> Doc
ppE (a
v, a
v')     = forall a. PPrint a => a -> Doc
pprint a
v Doc -> Doc -> Doc
<+> Doc
"->" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a
v'

isRealEdge :: CEdge -> Bool
isRealEdge :: CEdge -> Bool
isRealEdge (DKVar KVar
_, CVertex
_)     = Bool
False
isRealEdge (CVertex
_, DKVar KVar
_)     = Bool
False
isRealEdge (Cstr Integer
_, Cstr Integer
_) = Bool
False
isRealEdge CEdge
_                = Bool
True

txEdges    :: [CEdge] -> [CEdge]
txEdges :: [CEdge] -> [CEdge]
txEdges [CEdge]
es = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Integer -> [CEdge]
iEs [Integer]
is
  where
    is :: [Integer]
is     = [Integer
i | (Cstr Integer
i, Cstr Integer
_) <- [CEdge]
es]
    kvInM :: HashMap Integer [KVar]
kvInM  = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [ (Integer
i, KVar
k) | (KVar KVar
k, Cstr Integer
i) <- [CEdge]
es]
    kvOutM :: HashMap Integer [KVar]
kvOutM = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [ (Integer
i, KVar
k') | (Cstr Integer
i, KVar KVar
k') <- [CEdge]
es]
    ins :: Integer -> [KVar]
ins Integer
i  = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] Integer
i HashMap Integer [KVar]
kvInM
    outs :: Integer -> [KVar]
outs Integer
i = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] Integer
i HashMap Integer [KVar]
kvOutM
    iEs :: Integer -> [CEdge]
iEs Integer
i  = case (Integer -> [KVar]
ins Integer
i, Integer -> [KVar]
outs Integer
i) of
                 ([KVar]
ks, [] ) -> [(KVar -> CVertex
KVar KVar
k, Integer -> CVertex
Cstr Integer
i ) | KVar
k  <- [KVar]
ks ]
                 ([], [KVar]
ks') -> [(Integer -> CVertex
Cstr Integer
i, KVar -> CVertex
KVar KVar
k') | KVar
k' <- [KVar]
ks']
                 ([KVar]
ks, [KVar]
ks') -> [(KVar -> CVertex
KVar KVar
k, KVar -> CVertex
KVar KVar
k') | KVar
k  <- [KVar]
ks, KVar
k' <- [KVar]
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 { Slice -> [Integer]
slKVarCs :: [F.SubcId]     -- ^ F.SubcIds that transitively "reach" below
                   , Slice -> [Integer]
slConcCs :: [F.SubcId]     -- ^ F.SubcIds with Concrete RHS
                   , Slice -> [DepEdge]
slEdges  :: [DepEdge] -- ^ Dependencies between slKVarCs
                   } deriving (Slice -> Slice -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Slice -> Slice -> Bool
$c/= :: Slice -> Slice -> Bool
== :: Slice -> Slice -> Bool
$c== :: Slice -> Slice -> Bool
Eq, Int -> Slice -> ShowS
[Slice] -> ShowS
Slice -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Slice] -> ShowS
$cshowList :: [Slice] -> ShowS
show :: Slice -> String
$cshow :: Slice -> String
showsPrec :: Int -> Slice -> ShowS
$cshowsPrec :: Int -> Slice -> ShowS
Show)

data CGraph = CGraph
  { CGraph -> [DepEdge]
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.
  , CGraph -> CMap Int
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.
  , CGraph -> CMap [Integer]
gSucc  :: !(F.CMap [F.SubcId])
    -- | Amount of strongly connected components
  , CGraph -> Int
gSccs  :: !Int
  }

---------------------------------------------------------------------------
-- | CMap API -------------------------------------------------------------
---------------------------------------------------------------------------
lookupCMap :: (?callStack :: CallStack) => F.CMap a -> F.SubcId -> a
lookupCMap :: forall a. (?callStack::CallStack) => CMap a -> Integer -> a
lookupCMap CMap a
rm Integer
i = forall k v.
(?callStack::CallStack, Eq k, Hashable k) =>
String -> k -> HashMap k v -> v
safeLookup String
err Integer
i CMap a
rm
  where
    err :: String
err      = String
"lookupCMap: cannot find info for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
i

--------------------------------------------------------------------------------
-- | Constraint Dependencies ---------------------------------------------------
--------------------------------------------------------------------------------

data CDeps = CDs { CDeps -> CMap [Integer]
cSucc   :: !(F.CMap [F.SubcId]) -- ^ Constraints *written by* a SubcId
                 , CDeps -> HashMap Integer [KVar]
cPrev   :: !(F.CMap [F.KVar])   -- ^ (Cut) KVars *read by*    a SubcId
                 , CDeps -> CMap Rank
cRank   :: !(F.CMap Rank)       -- ^ SCC rank of a SubcId
                 , CDeps -> Int
cNumScc :: !Int                 -- ^ Total number of Sccs
                 }


-- | Ranks ---------------------------------------------------------------------

data Rank = Rank { Rank -> Int
rScc  :: !Int    -- ^ SCC number with ALL dependencies
                 , Rank -> Int
rIcc  :: !Int    -- ^ SCC number without CUT dependencies
                 , Rank -> Tag
rTag  :: !F.Tag  -- ^ The constraint's Tag
                 } deriving (Rank -> Rank -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rank -> Rank -> Bool
$c/= :: Rank -> Rank -> Bool
== :: Rank -> Rank -> Bool
$c== :: Rank -> Rank -> Bool
Eq, Int -> Rank -> ShowS
[Rank] -> ShowS
Rank -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rank] -> ShowS
$cshowList :: [Rank] -> ShowS
show :: Rank -> String
$cshow :: Rank -> String
showsPrec :: Int -> Rank -> ShowS
$cshowsPrec :: Int -> Rank -> ShowS
Show)

instance PPrint Rank where
  pprintTidy :: Tidy -> Rank -> Doc
pprintTidy Tidy
_ = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
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
  { forall a b. SolverInfo a b -> Sol b QBind
siSol     :: !(F.Sol b F.QBind)             -- ^ the initial solution
  , forall a b. SolverInfo a b -> SInfo a
siQuery   :: !(F.SInfo a)                   -- ^ the whole input query
  , forall a b. SolverInfo a b -> CDeps
siDeps    :: !CDeps                         -- ^ dependencies between constraints/ranks etc.
  , forall a b. SolverInfo a b -> HashSet KVar
siVars    :: !(S.HashSet F.KVar)            -- ^ set of KVars to actually solve for
  }