module TPDB.DP.Usable where

import TPDB.Data
import TPDB.Pretty

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

import qualified Data.Set as S

-- | DANGER: this ignores the CE condition
restrict :: (Ord c, Ord v) => RS c (Term v c) -> RS c (Term v c)
restrict :: RS c (Term v c) -> RS c (Term v c)
restrict RS c (Term v c)
dp = 
    RS c (Term v c)
dp { rules :: [Rule (Term v c)]
rules = (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 (RS c (Term v c) -> [Rule (Term v c)]
forall s r. RS s r -> [Rule r]
rules RS c (Term v c)
dp)
               [Rule (Term v c)] -> [Rule (Term v c)] -> [Rule (Term v c)]
forall a. [a] -> [a] -> [a]
++ Set (Rule (Term v c)) -> [Rule (Term v c)]
forall a. Set a -> [a]
S.toList ( RS c (Term v c) -> Set (Rule (Term v c))
forall v c. (Ord v, Ord c) => TRS v c -> Set (Rule (Term v c))
usable RS c (Term v c)
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 ::   (Ord v, Ord c)
       => TRS v c -> S.Set (Rule (Term v c))
usable :: TRS v c -> Set (Rule (Term v c))
usable TRS v c
dp = (Set (Rule (Term v c)) -> Set (Rule (Term v c)))
-> Set (Rule (Term v c)) -> Set (Rule (Term v c))
forall t. Eq t => (t -> t) -> t -> t
fixpoint ( \ Set (Rule (Term v c))
s -> Set (Rule (Term v c))
-> Set (Rule (Term v c)) -> Set (Rule (Term v c))
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (Rule (Term v c))
s (Set (Rule (Term v c)) -> Set (Rule (Term v c)))
-> Set (Rule (Term v c)) -> Set (Rule (Term v c))
forall a b. (a -> b) -> a -> b
$ TRS v c -> Set (Rule (Term v c)) -> Set (Rule (Term v c))
forall v c.
(Ord v, Ord c) =>
TRS v c -> Set (Rule (Term v c)) -> Set (Rule (Term v c))
required TRS v c
dp Set (Rule (Term v c))
s)
    (TRS v c -> Set (Rule (Term v c)) -> Set (Rule (Term v c))
forall v c.
(Ord v, Ord c) =>
TRS v c -> Set (Rule (Term v c)) -> Set (Rule (Term v c))
required TRS v c
dp (Set (Rule (Term v c)) -> Set (Rule (Term v c)))
-> Set (Rule (Term v c)) -> Set (Rule (Term v c))
forall a b. (a -> b) -> a -> b
$ (Rule (Term v c) -> Bool)
-> Set (Rule (Term v c)) -> Set (Rule (Term v c))
forall a. (a -> Bool) -> Set a -> Set a
S.filter Rule (Term v c) -> Bool
forall a. Rule a -> Bool
strict
                 (Set (Rule (Term v c)) -> Set (Rule (Term v c)))
-> Set (Rule (Term v c)) -> Set (Rule (Term v c))
forall a b. (a -> b) -> a -> b
$ [Rule (Term v c)] -> Set (Rule (Term v c))
forall a. Ord a => [a] -> Set a
S.fromList ([Rule (Term v c)] -> Set (Rule (Term v c)))
-> [Rule (Term v c)] -> Set (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) 

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

required ::  (Ord v, Ord c)
       => TRS v c -> S.Set ( Rule (Term v c) ) ->  S.Set ( Rule (Term v c) ) 
required :: TRS v c -> Set (Rule (Term v c)) -> Set (Rule (Term v c))
required TRS v c
dp Set (Rule (Term v c))
rs = 
    [Rule (Term v c)] -> Set (Rule (Term v c))
forall a. Ord a => [a] -> Set a
S.fromList ([Rule (Term v c)] -> Set (Rule (Term v c)))
-> [Rule (Term v c)] -> Set (Rule (Term v c))
forall a b. (a -> b) -> a -> b
$ do { Rule (Term v c)
r <- Set (Rule (Term v c)) -> [Rule (Term v c)]
forall a. Set a -> [a]
S.toList Set (Rule (Term v c))
rs ;  TRS v c -> Term v c -> [Rule (Term v c)]
forall v c.
(Ord v, Ord c) =>
TRS v c -> Term v c -> [Rule (Term v c)]
needed TRS v c
dp (Term v c -> [Rule (Term v c)]) -> Term v c -> [Rule (Term v c)]
forall a b. (a -> b) -> a -> b
$ Rule (Term v c) -> Term v c
forall a. Rule a -> a
rhs Rule (Term v c)
r }

needed :: (Ord v, Ord c)
       => TRS v c -> Term v c -> [ Rule (Term v c) ]
needed :: TRS v c -> Term v c -> [Rule (Term v c)]
needed TRS v c
dp Term v c
t = case Term v c
t of
    Node c
f [Term v c]
args -> 
          (Rule (Term v c) -> Bool) -> [Rule (Term v c)] -> [Rule (Term v c)]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ Rule (Term v c)
u -> Term (Either v Int) c -> Term (Either v Int) c -> Bool
forall v c. (Ord v, Eq c) => Term v c -> Term v c -> Bool
unifies ( (v -> Either v Int) -> Term v c -> Term (Either v Int) c
forall v u s. (v -> u) -> Term v s -> Term u s
vmap v -> Either v Int
forall a b. a -> Either a b
Left (Term v c -> Term (Either v Int) c)
-> Term v c -> Term (Either v Int) 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 ) ( (Int -> Either v Int) -> Term Int c -> Term (Either v Int) c
forall v u s. (v -> u) -> Term v s -> Term u s
vmap Int -> Either v Int
forall a b. b -> Either a b
Right (Term Int c -> Term (Either v Int) c)
-> Term Int c -> Term (Either v Int) c
forall a b. (a -> b) -> a -> b
$ TRS v c -> Term v c -> Term Int c
forall v c. (Ord v, Ord c) => TRS v c -> Term v c -> Term Int c
tcap TRS v c
dp Term v c
t ) )
                ( (Rule (Term v c) -> Bool) -> [Rule (Term v c)] -> [Rule (Term v c)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (Rule (Term v c) -> Bool) -> 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)] -> [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
dp )
        [Rule (Term v c)] -> [Rule (Term v c)] -> [Rule (Term v c)]
forall a. [a] -> [a] -> [a]
++ ( [Term v c]
args [Term v c] -> (Term v c -> [Rule (Term v c)]) -> [Rule (Term v c)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TRS v c -> Term v c -> [Rule (Term v c)]
forall v c.
(Ord v, Ord c) =>
TRS v c -> Term v c -> [Rule (Term v c)]
needed TRS v c
dp )
    Var v
v -> []