{-# 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.Set as S
import qualified Data.Map 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 (Marked a) (Term v (Marked a))
-> [Either
      (Rule (Term v (Marked a))) (RS (Marked a) (Term v (Marked a)))]
components RS (Marked a) (Term v (Marked a))
s = do 
    let es :: Map (Rule (Term v (Marked a))) [Rule (Term v (Marked a))]
es = ([Rule (Term v (Marked a))]
 -> [Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))])
-> [(Rule (Term v (Marked a)), [Rule (Term v (Marked a))])]
-> Map (Rule (Term v (Marked a))) [Rule (Term v (Marked a))]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith [Rule (Term v (Marked a))]
-> [Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))]
forall a. [a] -> [a] -> [a]
(++) 
           ([(Rule (Term v (Marked a)), [Rule (Term v (Marked a))])]
 -> Map (Rule (Term v (Marked a))) [Rule (Term v (Marked a))])
-> [(Rule (Term v (Marked a)), [Rule (Term v (Marked a))])]
-> Map (Rule (Term v (Marked a))) [Rule (Term v (Marked a))]
forall a b. (a -> b) -> a -> b
$ do (Rule (Term v (Marked a))
p,Rule (Term v (Marked a))
q) <- RS (Marked a) (Term v (Marked a))
-> [(Rule (Term v (Marked a)), Rule (Term v (Marked a)))]
forall v a.
(Ord v, Ord a) =>
RS (Marked a) (Term v (Marked a))
-> [(Rule (Term v (Marked a)), Rule (Term v (Marked a)))]
edges RS (Marked a) (Term v (Marked a))
s ; (Rule (Term v (Marked a)), [Rule (Term v (Marked a))])
-> [(Rule (Term v (Marked a)), [Rule (Term v (Marked a))])]
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule (Term v (Marked a))
p, [Rule (Term v (Marked a))
q])
        key :: Map (Rule (Term v (Marked a))) Integer
key = [(Rule (Term v (Marked a)), Integer)]
-> Map (Rule (Term v (Marked a))) Integer
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList 
            ([(Rule (Term v (Marked a)), Integer)]
 -> Map (Rule (Term v (Marked a))) Integer)
-> [(Rule (Term v (Marked a)), Integer)]
-> Map (Rule (Term v (Marked a))) Integer
forall a b. (a -> b) -> a -> b
$ [Rule (Term v (Marked a))]
-> [Integer] -> [(Rule (Term v (Marked a)), Integer)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Rule (Term v (Marked a)) -> Bool)
-> [Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))]
forall a. (a -> Bool) -> [a] -> [a]
filter Rule (Term v (Marked a)) -> Bool
forall a. Rule a -> Bool
strict ([Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))])
-> [Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))]
forall a b. (a -> b) -> a -> b
$ RS (Marked a) (Term v (Marked a)) -> [Rule (Term v (Marked a))]
forall s r. RS s r -> [Rule r]
rules RS (Marked a) (Term v (Marked a))
s) [Integer
0.. ]
    SCC (Rule (Term v (Marked a)))
comp <- [SCC (Rule (Term v (Marked a)))]
-> [SCC (Rule (Term v (Marked a)))]
forall a. [a] -> [a]
reverse ([SCC (Rule (Term v (Marked a)))]
 -> [SCC (Rule (Term v (Marked a)))])
-> [SCC (Rule (Term v (Marked a)))]
-> [SCC (Rule (Term v (Marked a)))]
forall a b. (a -> b) -> a -> b
$ [(Rule (Term v (Marked a)), Integer, [Integer])]
-> [SCC (Rule (Term v (Marked a)))]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp ([(Rule (Term v (Marked a)), Integer, [Integer])]
 -> [SCC (Rule (Term v (Marked a)))])
-> [(Rule (Term v (Marked a)), Integer, [Integer])]
-> [SCC (Rule (Term v (Marked a)))]
forall a b. (a -> b) -> a -> b
$ do
        Rule (Term v (Marked a))
p <- Map (Rule (Term v (Marked a))) Integer
-> [Rule (Term v (Marked a))]
forall k a. Map k a -> [k]
M.keys Map (Rule (Term v (Marked a))) Integer
key
        let qs :: [Rule (Term v (Marked a))]
qs = [Rule (Term v (Marked a))]
-> Rule (Term v (Marked a))
-> Map (Rule (Term v (Marked a))) [Rule (Term v (Marked a))]
-> [Rule (Term v (Marked a))]
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault [] Rule (Term v (Marked a))
p Map (Rule (Term v (Marked a))) [Rule (Term v (Marked a))]
es
        (Rule (Term v (Marked a)), Integer, [Integer])
-> [(Rule (Term v (Marked a)), Integer, [Integer])]
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule (Term v (Marked a))
p, Map (Rule (Term v (Marked a))) Integer
key Map (Rule (Term v (Marked a))) Integer
-> Rule (Term v (Marked a)) -> Integer
forall k a. Ord k => Map k a -> k -> a
M.! Rule (Term v (Marked a))
p, (Rule (Term v (Marked a)) -> Integer)
-> [Rule (Term v (Marked a))] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Map (Rule (Term v (Marked a))) Integer
key Map (Rule (Term v (Marked a))) Integer
-> Rule (Term v (Marked a)) -> Integer
forall k a. Ord k => Map k a -> k -> a
M.!) [Rule (Term v (Marked a))]
qs )
    Either
  (Rule (Term v (Marked a))) (RS (Marked a) (Term v (Marked a)))
-> [Either
      (Rule (Term v (Marked a))) (RS (Marked a) (Term v (Marked a)))]
forall (m :: * -> *) a. Monad m => a -> m a
return (Either
   (Rule (Term v (Marked a))) (RS (Marked a) (Term v (Marked a)))
 -> [Either
       (Rule (Term v (Marked a))) (RS (Marked a) (Term v (Marked a)))])
-> Either
     (Rule (Term v (Marked a))) (RS (Marked a) (Term v (Marked a)))
-> [Either
      (Rule (Term v (Marked a))) (RS (Marked a) (Term v (Marked a)))]
forall a b. (a -> b) -> a -> b
$ case SCC (Rule (Term v (Marked a)))
comp of
        CyclicSCC [Rule (Term v (Marked a))]
vs -> RS (Marked a) (Term v (Marked a))
-> Either
     (Rule (Term v (Marked a))) (RS (Marked a) (Term v (Marked a)))
forall a b. b -> Either a b
Right (RS (Marked a) (Term v (Marked a))
 -> Either
      (Rule (Term v (Marked a))) (RS (Marked a) (Term v (Marked a))))
-> RS (Marked a) (Term v (Marked a))
-> Either
     (Rule (Term v (Marked a))) (RS (Marked a) (Term v (Marked a)))
forall a b. (a -> b) -> a -> b
$ RS (Marked a) (Term v (Marked a))
s { rules :: [Rule (Term v (Marked a))]
rules = [Rule (Term v (Marked a))]
vs 
                 [Rule (Term v (Marked a))]
-> [Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))]
forall a. [a] -> [a] -> [a]
++ (Rule (Term v (Marked a)) -> Bool)
-> [Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (Rule (Term v (Marked a)) -> Bool)
-> Rule (Term v (Marked a))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule (Term v (Marked a)) -> Bool
forall a. Rule a -> Bool
strict) (RS (Marked a) (Term v (Marked a)) -> [Rule (Term v (Marked a))]
forall s r. RS s r -> [Rule r]
rules RS (Marked a) (Term v (Marked a))
s) } 
        AcyclicSCC Rule (Term v (Marked a))
v -> Rule (Term v (Marked a))
-> Either
     (Rule (Term v (Marked a))) (RS (Marked a) (Term v (Marked a)))
forall a b. a -> Either a b
Left Rule (Term v (Marked a))
v

-- | edges of the estimated dependency graph
edges :: RS (Marked a) (Term v (Marked a))
-> [(Rule (Term v (Marked a)), Rule (Term v (Marked a)))]
edges RS (Marked a) (Term v (Marked a))
s = do
    let def :: Set (Marked a)
def = (Marked a -> Bool) -> Set (Marked a) -> Set (Marked a)
forall a. (a -> Bool) -> Set a -> Set a
S.filter Marked a -> Bool
forall a. Marked a -> Bool
isOriginal (Set (Marked a) -> Set (Marked a))
-> Set (Marked a) -> Set (Marked a)
forall a b. (a -> b) -> a -> b
$ RS (Marked a) (Term v (Marked a)) -> Set (Marked a)
forall a s v. Ord a => RS s (Term v a) -> Set a
defined RS (Marked a) (Term v (Marked a))
s
    Rule (Term v (Marked a))
u <- (Rule (Term v (Marked a)) -> Bool)
-> [Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))]
forall a. (a -> Bool) -> [a] -> [a]
filter Rule (Term v (Marked a)) -> Bool
forall a. Rule a -> Bool
strict ([Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))])
-> [Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))]
forall a b. (a -> b) -> a -> b
$ RS (Marked a) (Term v (Marked a)) -> [Rule (Term v (Marked a))]
forall s r. RS s r -> [Rule r]
rules RS (Marked a) (Term v (Marked a))
s
    Rule (Term v (Marked a))
v <- (Rule (Term v (Marked a)) -> Bool)
-> [Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))]
forall a. (a -> Bool) -> [a] -> [a]
filter Rule (Term v (Marked a)) -> Bool
forall a. Rule a -> Bool
strict ([Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))])
-> [Rule (Term v (Marked a))] -> [Rule (Term v (Marked a))]
forall a b. (a -> b) -> a -> b
$ RS (Marked a) (Term v (Marked a)) -> [Rule (Term v (Marked a))]
forall s r. RS s r -> [Rule r]
rules RS (Marked a) (Term v (Marked a))
s
    Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Term (Either Int v) (Marked a)
-> Term (Either Int v) (Marked a) -> Bool
forall v c. (Ord v, Eq c) => Term v c -> Term v c -> Bool
unifies ( (Int -> Either Int v)
-> Term Int (Marked a) -> Term (Either Int v) (Marked a)
forall v u s. (v -> u) -> Term v s -> Term u s
vmap Int -> Either Int v
forall a b. a -> Either a b
Left (Term Int (Marked a) -> Term (Either Int v) (Marked a))
-> Term Int (Marked a) -> Term (Either Int v) (Marked a)
forall a b. (a -> b) -> a -> b
$ RS (Marked a) (Term v (Marked a))
-> Term v (Marked a) -> Term Int (Marked a)
forall v c. (Ord v, Ord c) => TRS v c -> Term v c -> Term Int c
tcap RS (Marked a) (Term v (Marked a))
s (Term v (Marked a) -> Term Int (Marked a))
-> Term v (Marked a) -> Term Int (Marked a)
forall a b. (a -> b) -> a -> b
$ Rule (Term v (Marked a)) -> Term v (Marked a)
forall a. Rule a -> a
rhs Rule (Term v (Marked a))
u ) 
                    ( (v -> Either Int v)
-> Term v (Marked a) -> Term (Either Int v) (Marked a)
forall v u s. (v -> u) -> Term v s -> Term u s
vmap v -> Either Int v
forall a b. b -> Either a b
Right (Term v (Marked a) -> Term (Either Int v) (Marked a))
-> Term v (Marked a) -> Term (Either Int v) (Marked a)
forall a b. (a -> b) -> a -> b
$ Rule (Term v (Marked a)) -> Term v (Marked a)
forall a. Rule a -> a
lhs Rule (Term v (Marked a))
v )
    (Rule (Term v (Marked a)), Rule (Term v (Marked a)))
-> [(Rule (Term v (Marked a)), Rule (Term v (Marked a)))]
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule (Term v (Marked a))
u,Rule (Term v (Marked a))
v)

check :: [(Rule (Term Identifier (Marked Identifier)),
  Rule (Term Identifier (Marked Identifier)))]
check = RS (Marked Identifier) (Term Identifier (Marked Identifier))
-> [(Rule (Term Identifier (Marked Identifier)),
     Rule (Term Identifier (Marked Identifier)))]
forall v a.
(Ord v, Ord a) =>
RS (Marked a) (Term v (Marked a))
-> [(Rule (Term v (Marked a)), Rule (Term v (Marked a)))]
edges (RS (Marked Identifier) (Term Identifier (Marked Identifier))
 -> [(Rule (Term Identifier (Marked Identifier)),
      Rule (Term Identifier (Marked Identifier)))])
-> RS (Marked Identifier) (Term Identifier (Marked Identifier))
-> [(Rule (Term Identifier (Marked Identifier)),
     Rule (Term Identifier (Marked Identifier)))]
forall a b. (a -> b) -> a -> b
$ RS Identifier (Term Identifier Identifier)
-> RS (Marked Identifier) (Term Identifier (Marked Identifier))
forall v s.
(Ord v, Ord s) =>
RS s (Term v s) -> RS (Marked s) (Term v (Marked s))
dp RS Identifier (Term Identifier Identifier)
sys

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