{-# 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
import TPDB.Plain.Write
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
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 :: 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
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)))"