{-# language OverloadedStrings #-}

module TPDB.DP.Graph where

import TPDB.DP.TCap
import TPDB.DP.Unify
import TPDB.DP.Transform 

import TPDB.Data
import TPDB.Pretty

import TPDB.Plain.Read -- for testing
import TPDB.Plain.Write -- for testing

import qualified Data.IntSet as S
import qualified Data.IntMap.Strict as M
import Data.Graph ( stronglyConnComp, SCC(..) )
import Control.Monad ( guard, forM )
import Control.Applicative

import Control.Monad.State.Strict 


-- | DP problems for strongly connected components, 
-- topologically sorted, with CyclicComponents in Right,
-- others in Left.
components :: RS s (Term v s) -> [Either (Rule (Term v s)) (RS s (Term v s))]
components RS s (Term v s)
s = do 
    let su :: IntMap (Rule (Term v s))
su = RS s (Term v s) -> IntMap (Rule (Term v s))
forall v c. TRS v c -> IntMap (Rule (Term v c))
indexed RS s (Term v s)
s
        ns :: [Rule (Term v s)]
ns = (Rule (Term v s) -> Bool) -> [Rule (Term v s)] -> [Rule (Term v s)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (Rule (Term v s) -> Bool) -> Rule (Term v s) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule (Term v s) -> Bool
forall a. Rule a -> Bool
strict) (RS s (Term v s) -> [Rule (Term v s)]
forall s r. RS s r -> [Rule r]
rules RS s (Term v s)
s) 
        es :: IntMap IntSet
es = (IntSet -> IntSet -> IntSet) -> [(Key, IntSet)] -> IntMap IntSet
forall a. (a -> a -> a) -> [(Key, a)] -> IntMap a
M.fromListWith IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
(<>) 
           ([(Key, IntSet)] -> IntMap IntSet)
-> [(Key, IntSet)] -> IntMap IntSet
forall a b. (a -> b) -> a -> b
$ do (Key
i,Key
j) <- IntMap (Rule (Term v s)) -> [(Key, Key)]
forall {b} {c}.
(Ord b, Eq c) =>
IntMap (Rule (Term b c)) -> [(Key, Key)]
edges IntMap (Rule (Term v s))
su ; (Key, IntSet) -> [(Key, IntSet)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Key
i, Key -> IntSet
S.singleton Key
j)
    SCC (Rule (Term v s))
comp <- [SCC (Rule (Term v s))] -> [SCC (Rule (Term v s))]
forall a. [a] -> [a]
reverse ([SCC (Rule (Term v s))] -> [SCC (Rule (Term v s))])
-> [SCC (Rule (Term v s))] -> [SCC (Rule (Term v s))]
forall a b. (a -> b) -> a -> b
$ [(Rule (Term v s), Key, [Key])] -> [SCC (Rule (Term v s))]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp ([(Rule (Term v s), Key, [Key])] -> [SCC (Rule (Term v s))])
-> [(Rule (Term v s), Key, [Key])] -> [SCC (Rule (Term v s))]
forall a b. (a -> b) -> a -> b
$ do
        (Key
i,Rule (Term v s)
u) <- IntMap (Rule (Term v s)) -> [(Key, Rule (Term v s))]
forall a. IntMap a -> [(Key, a)]
M.toList IntMap (Rule (Term v s))
su
        let js :: IntSet
js = IntSet -> Key -> IntMap IntSet -> IntSet
forall a. a -> Key -> IntMap a -> a
M.findWithDefault IntSet
forall a. Monoid a => a
mempty Key
i IntMap IntSet
es
        (Rule (Term v s), Key, [Key]) -> [(Rule (Term v s), Key, [Key])]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule (Term v s)
u, Key
i, IntSet -> [Key]
S.toList IntSet
js)
    Either (Rule (Term v s)) (RS s (Term v s))
-> [Either (Rule (Term v s)) (RS s (Term v s))]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Rule (Term v s)) (RS s (Term v s))
 -> [Either (Rule (Term v s)) (RS s (Term v s))])
-> Either (Rule (Term v s)) (RS s (Term v s))
-> [Either (Rule (Term v s)) (RS s (Term v s))]
forall a b. (a -> b) -> a -> b
$ case SCC (Rule (Term v s))
comp of
        CyclicSCC [Rule (Term v s)]
vs -> RS s (Term v s) -> Either (Rule (Term v s)) (RS s (Term v s))
forall a b. b -> Either a b
Right (RS s (Term v s) -> Either (Rule (Term v s)) (RS s (Term v s)))
-> RS s (Term v s) -> Either (Rule (Term v s)) (RS s (Term v s))
forall a b. (a -> b) -> a -> b
$ RS s (Term v s)
s { rules = vs <> ns }
        AcyclicSCC Rule (Term v s)
v -> Rule (Term v s) -> Either (Rule (Term v s)) (RS s (Term v s))
forall a b. a -> Either a b
Left Rule (Term v s)
v

-- | edges of the estimated dependency graph
edges :: IntMap (Rule (Term b c)) -> [(Key, Key)]
edges IntMap (Rule (Term b c))
su = do
    (Key
i,Rule (Term b c)
u) <- IntMap (Rule (Term b c)) -> [(Key, Rule (Term b c))]
forall a. IntMap a -> [(Key, a)]
M.toList IntMap (Rule (Term b c))
su
    (Key
j,Rule (Term b c)
v) <- IntMap (Rule (Term b c)) -> [(Key, Rule (Term b c))]
forall a. IntMap a -> [(Key, a)]
M.toList IntMap (Rule (Term b c))
su
    Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Term (Either Key b) c -> Term (Either Key b) c -> Bool
forall {v} {c}. (Ord v, Eq c) => Term v c -> Term v c -> Bool
unifies ( (Key -> Either Key b) -> Term Key c -> Term (Either Key b) c
forall v s u.
(() :: Constraint, () :: Constraint) =>
(v -> u) -> Term v s -> Term u s
vmap Key -> Either Key b
forall a b. a -> Either a b
Left (Term Key c -> Term (Either Key b) c)
-> Term Key c -> Term (Either Key b) c
forall a b. (a -> b) -> a -> b
$ [Rule (Term b c)] -> Term b c -> Term Key c
forall v c.
(Ord v, Eq c, () :: Constraint) =>
[Rule (Term v c)] -> Term v c -> Term Key c
tcap (IntMap (Rule (Term b c)) -> [Rule (Term b c)]
forall a. IntMap a -> [a]
M.elems IntMap (Rule (Term b c))
su) (Term b c -> Term Key c) -> Term b c -> Term Key c
forall a b. (a -> b) -> a -> b
$ Rule (Term b c) -> Term b c
forall a. Rule a -> a
rhs Rule (Term b c)
u ) 
                    ( (b -> Either Key b) -> Term b c -> Term (Either Key b) c
forall v s u.
(() :: Constraint, () :: Constraint) =>
(v -> u) -> Term v s -> Term u s
vmap b -> Either Key b
forall a b. b -> Either a b
Right (Term b c -> Term (Either Key b) c)
-> Term b c -> Term (Either Key b) c
forall a b. (a -> b) -> a -> b
$ Rule (Term b c) -> Term b c
forall a. Rule a -> a
lhs Rule (Term b c)
v )
    (Key, Key) -> [(Key, Key)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Key
i,Key
j)

check :: [(Key, Key)]
check = IntMap (Rule (Term Identifier (Marked Identifier))) -> [(Key, Key)]
forall {b} {c}.
(Ord b, Eq c) =>
IntMap (Rule (Term b c)) -> [(Key, Key)]
edges (IntMap (Rule (Term Identifier (Marked Identifier)))
 -> [(Key, Key)])
-> IntMap (Rule (Term Identifier (Marked Identifier)))
-> [(Key, Key)]
forall a b. (a -> b) -> a -> b
$ TRS Identifier (Marked Identifier)
-> IntMap (Rule (Term Identifier (Marked Identifier)))
forall v c. TRS v c -> IntMap (Rule (Term v c))
indexed (TRS Identifier (Marked Identifier)
 -> IntMap (Rule (Term Identifier (Marked Identifier))))
-> TRS Identifier (Marked Identifier)
-> IntMap (Rule (Term Identifier (Marked Identifier)))
forall a b. (a -> b) -> a -> b
$ RS Identifier (Term Identifier Identifier)
-> TRS Identifier (Marked Identifier)
forall v s.
(Eq v, Ord s, () :: Constraint) =>
RS s (Term v s) -> RS (Marked s) (Term v (Marked s))
dp RS Identifier (Term Identifier Identifier)
sys

-- | numbering for non-strict rules
indexed :: TRS v c -> M.IntMap (Rule (Term v c))
indexed :: forall v c. TRS v c -> IntMap (Rule (Term v c))
indexed TRS v c
s = [(Key, Rule (Term v c))] -> IntMap (Rule (Term v c))
forall a. [(Key, a)] -> IntMap a
M.fromList ([(Key, Rule (Term v c))] -> IntMap (Rule (Term v c)))
-> [(Key, Rule (Term v c))] -> IntMap (Rule (Term v c))
forall a b. (a -> b) -> a -> b
$ [Key] -> [Rule (Term v c)] -> [(Key, Rule (Term v c))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Key
0::Int ..] ([Rule (Term v c)] -> [(Key, Rule (Term v c))])
-> [Rule (Term v c)] -> [(Key, Rule (Term v c))]
forall a b. (a -> b) -> a -> b
$ (Rule (Term v c) -> Bool) -> [Rule (Term v c)] -> [Rule (Term v c)]
forall a. (a -> Bool) -> [a] -> [a]
filter Rule (Term v c) -> Bool
forall a. Rule a -> Bool
strict ([Rule (Term v c)] -> [Rule (Term v c)])
-> [Rule (Term v c)] -> [Rule (Term v c)]
forall a b. (a -> b) -> a -> b
$ TRS v c -> [Rule (Term v c)]
forall s r. RS s r -> [Rule r]
rules TRS v c
s

-- example from "DP Revisited" http://colo6-c703.uibk.ac.at/ttt/rta04.pdf
Right RS Identifier (Term Identifier Identifier)
sys = 
    Text -> Either String (RS Identifier (Term Identifier Identifier))
TPDB.Plain.Read.trs Text
"(VAR x y) (RULES not(not(x)) -> x not(or(x,y)) -> and(not(x),not(y)) not(and(x,y)) -> or (not(x),not(y)) and(x,or(y,z)) -> or(and(x,z),and(y,z)) and(or(y,z),x) -> or(and(x,y),and(x,z)))"