module TPDB.DP.Usable where

import TPDB.Data
import TPDB.Pretty

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

import qualified Data.IntSet as S
import qualified Data.IntMap.Strict as M

-- | restrict one SCC to its usable rules.
-- DANGER: this ignores the CE condition
restrict :: (Eq c, Ord v, TermC v c) => RS c (Term v c) -> RS c (Term v c)
restrict :: forall c v.
(Eq c, Ord v, TermC v c) =>
RS c (Term v c) -> RS c (Term v c)
restrict RS c (Term v c)
dp = 
    RS c (Term v c)
dp { rules = filter strict (rules dp)
               ++ usable dp
       }

-- | computes the least closed set of usable rules, cf. Def 4.5
-- http://cl-informatik.uibk.ac.at/users/griff/publications/Sternagel-Thiemann-RTA10.pdf

usable :: (Eq c, Ord v, TermC v c)
       => TRS v c -> [Rule (Term v c)]
usable :: forall c v.
(Eq c, Ord v, TermC v c) =>
TRS v c -> [Rule (Term v c)]
usable TRS v c
dp =
  let dpi :: IntMap (Rule (Term v c))
dpi = [(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..] ([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
$ TRS v c -> [Rule (Term v c)]
forall s r. RS s r -> [Rule r]
rules TRS v c
dp
      fp :: IntSet
fp = (IntSet -> IntSet) -> IntSet -> IntSet
forall {t}. Eq t => (t -> t) -> t -> t
fixpoint
        ( \ IntSet
s -> IntSet -> IntSet -> IntSet
S.union IntSet
s (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ IntMap (Rule (Term v c)) -> [Key] -> IntSet
forall c v.
(Eq c, Ord v, TermC v c) =>
IntMap (Rule (Term v c)) -> [Key] -> IntSet
required IntMap (Rule (Term v c))
dpi ([Key] -> IntSet) -> [Key] -> IntSet
forall a b. (a -> b) -> a -> b
$ IntSet -> [Key]
S.toList IntSet
s)
        (IntMap (Rule (Term v c)) -> [Key] -> IntSet
forall c v.
(Eq c, Ord v, TermC v c) =>
IntMap (Rule (Term v c)) -> [Key] -> IntSet
required IntMap (Rule (Term v c))
dpi ([Key] -> IntSet) -> [Key] -> IntSet
forall a b. (a -> b) -> a -> b
$ ((Key, Rule (Term v c)) -> Key)
-> [(Key, Rule (Term v c))] -> [Key]
forall a b. (a -> b) -> [a] -> [b]
map (Key, Rule (Term v c)) -> Key
forall a b. (a, b) -> a
fst ([(Key, Rule (Term v c))] -> [Key])
-> [(Key, Rule (Term v c))] -> [Key]
forall a b. (a -> b) -> a -> b
$ ((Key, Rule (Term v c)) -> Bool)
-> [(Key, Rule (Term v c))] -> [(Key, 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) -> Bool)
-> ((Key, Rule (Term v c)) -> Rule (Term v c))
-> (Key, Rule (Term v c))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Key, Rule (Term v c)) -> Rule (Term v c)
forall a b. (a, b) -> b
snd) ([(Key, Rule (Term v c))] -> [(Key, Rule (Term v c))])
-> [(Key, Rule (Term v c))] -> [(Key, Rule (Term v c))]
forall a b. (a -> b) -> a -> b
$ IntMap (Rule (Term v c)) -> [(Key, Rule (Term v c))]
forall a. IntMap a -> [(Key, a)]
M.toList IntMap (Rule (Term v c))
dpi)
  in  (Key -> Rule (Term v c)) -> [Key] -> [Rule (Term v c)]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap (Rule (Term v c))
dpi IntMap (Rule (Term v c)) -> Key -> Rule (Term v c)
forall a. IntMap a -> Key -> a
M.!) ([Key] -> [Rule (Term v c)]) -> [Key] -> [Rule (Term v c)]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Key]
S.toList IntSet
fp

fixpoint :: (t -> t) -> t -> t
fixpoint t -> t
f t
x = 
    let y :: t
y = t -> t
f t
x in if t
x t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
y then t
x else (t -> t) -> t -> t
fixpoint t -> t
f t
y

-- | indices of rules that can be used
-- to rewrite rhs of rules with indices @is@
required :: (Eq c, Ord v, TermC v c)
       => M.IntMap ( Rule (Term v c) )
         -> [ Int ]
         -> S.IntSet
required :: forall c v.
(Eq c, Ord v, TermC v c) =>
IntMap (Rule (Term v c)) -> [Key] -> IntSet
required IntMap (Rule (Term v c))
dpi [Key]
is =  [Key] -> IntSet
S.fromList
  ([Key] -> IntSet) -> [Key] -> IntSet
forall a b. (a -> b) -> a -> b
$ (Term v c -> [Key]) -> [Term v c] -> [Key]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (IntMap (Rule (Term v c)) -> Term v c -> [Key]
forall c v.
(Eq c, Ord v, TermC v c) =>
IntMap (Rule (Term v c)) -> Term v c -> [Key]
needed IntMap (Rule (Term v c))
dpi)
  ([Term v c] -> [Key]) -> [Term v c] -> [Key]
forall a b. (a -> b) -> a -> b
$ (Key -> Term v c) -> [Key] -> [Term v c]
forall a b. (a -> b) -> [a] -> [b]
map (Rule (Term v c) -> Term v c
forall a. Rule a -> a
rhs (Rule (Term v c) -> Term v c)
-> (Key -> Rule (Term v c)) -> Key -> Term v c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntMap (Rule (Term v c))
dpi IntMap (Rule (Term v c)) -> Key -> Rule (Term v c)
forall a. IntMap a -> Key -> a
M.!)) [Key]
is

-- | indices of rules that can be used
-- to rewrite the given term @t@ (including subterms)
needed :: (Eq c, Ord v, TermC v c)
       => M.IntMap (Rule (Term v c))
       -> Term v c
       -> [ Int ]
needed :: forall c v.
(Eq c, Ord v, TermC v c) =>
IntMap (Rule (Term v c)) -> Term v c -> [Key]
needed IntMap (Rule (Term v c))
dpi Term v c
t = case Term v c
t of
    Node c
f [Term v c]
args -> (((Key, Rule (Term v c)) -> Key)
-> [(Key, Rule (Term v c))] -> [Key]
forall a b. (a -> b) -> [a] -> [b]
map (Key, Rule (Term v c)) -> Key
forall a b. (a, b) -> a
fst
         ([(Key, Rule (Term v c))] -> [Key])
-> [(Key, Rule (Term v c))] -> [Key]
forall a b. (a -> b) -> a -> b
$ ((Key, Rule (Term v c)) -> Bool)
-> [(Key, Rule (Term v c))] -> [(Key, Rule (Term v c))]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ (Key
j,Rule (Term v c)
u) -> Term (Either v Key) c -> Term (Either v Key) c -> Bool
forall {v} {c}. (Ord v, Eq c) => Term v c -> Term v c -> Bool
unifies ( (v -> Either v Key) -> Term v c -> Term (Either v Key) c
forall v s u.
(TermC v c, TermC v c) =>
(v -> u) -> Term v s -> Term u s
vmap v -> Either v Key
forall a b. a -> Either a b
Left (Term v c -> Term (Either v Key) c)
-> Term v c -> Term (Either v Key) c
forall a b. (a -> b) -> a -> b
$ Rule (Term v c) -> Term v c
forall a. Rule a -> a
lhs Rule (Term v c)
u ) ( (Key -> Either v Key) -> Term Key c -> Term (Either v Key) c
forall v s u.
(TermC v c, TermC v c) =>
(v -> u) -> Term v s -> Term u s
vmap Key -> Either v Key
forall a b. b -> Either a b
Right (Term Key c -> Term (Either v Key) c)
-> Term Key c -> Term (Either v Key) c
forall a b. (a -> b) -> a -> b
$ [Rule (Term v c)] -> Term v c -> Term Key c
forall v c.
(Ord v, Eq c, TermC v c) =>
[Rule (Term v c)] -> Term v c -> Term Key c
tcap (IntMap (Rule (Term v c)) -> [Rule (Term v c)]
forall a. IntMap a -> [a]
M.elems IntMap (Rule (Term v c))
dpi) Term v c
t ) )
         ([(Key, Rule (Term v c))] -> [(Key, Rule (Term v c))])
-> [(Key, Rule (Term v c))] -> [(Key, Rule (Term v c))]
forall a b. (a -> b) -> a -> b
$ ((Key, Rule (Term v c)) -> Bool)
-> [(Key, Rule (Term v c))] -> [(Key, Rule (Term v c))]
forall a. (a -> Bool) -> [a] -> [a]
filter ( Bool -> Bool
not (Bool -> Bool)
-> ((Key, Rule (Term v c)) -> Bool)
-> (Key, Rule (Term v c))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule (Term v c) -> Bool
forall a. Rule a -> Bool
strict (Rule (Term v c) -> Bool)
-> ((Key, Rule (Term v c)) -> Rule (Term v c))
-> (Key, Rule (Term v c))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Key, Rule (Term v c)) -> Rule (Term v c)
forall a b. (a, b) -> b
snd)
         ([(Key, Rule (Term v c))] -> [(Key, Rule (Term v c))])
-> [(Key, Rule (Term v c))] -> [(Key, Rule (Term v c))]
forall a b. (a -> b) -> a -> b
$ IntMap (Rule (Term v c)) -> [(Key, Rule (Term v c))]
forall a. IntMap a -> [(Key, a)]
M.toList IntMap (Rule (Term v c))
dpi)
        [Key] -> [Key] -> [Key]
forall a. [a] -> [a] -> [a]
++ ( [Term v c]
args [Term v c] -> (Term v c -> [Key]) -> [Key]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IntMap (Rule (Term v c)) -> Term v c -> [Key]
forall c v.
(Eq c, Ord v, TermC v c) =>
IntMap (Rule (Term v c)) -> Term v c -> [Key]
needed IntMap (Rule (Term v c))
dpi )
    Var v
v -> []