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
restrict :: (Ord c, Ord v) => RS c (Term v c) -> RS c (Term v c)
restrict dp =
dp { rules = filter strict (rules dp)
++ S.toList ( usable dp)
}
usable :: (Ord v, Ord c)
=> TRS v c -> S.Set (Rule (Term v c))
usable dp = fixpoint ( \ s -> S.union s $ required dp s)
(required dp $ S.filter strict
$ S.fromList $ rules dp)
fixpoint f x =
let y = f x in if x == y then x else fixpoint f y
required :: (Ord v, Ord c)
=> TRS v c -> S.Set ( Rule (Term v c) ) -> S.Set ( Rule (Term v c) )
required dp rs =
S.fromList $ do { r <- S.toList rs ; needed dp $ rhs r }
needed :: (Ord v, Ord c)
=> TRS v c -> Term v c -> [ Rule (Term v c) ]
needed dp t = case t of
Node f args ->
filter ( \ u -> unifies ( vmap Left $ lhs u ) ( vmap Right $ tcap dp t ) )
( filter (not . strict) $ rules dp )
++ ( args >>= needed dp )
Var v -> []