-- This file is part of the 'term-rewriting' library. It is licensed
-- under an MIT license. See the accompanying 'LICENSE' file for details.
--
-- Authors: Martin Avanzini, Bertram Felgenhauer

module Data.Rewriting.Rules.Ops (
    -- * Operations on Rules
    funs,
    funsDL,
    vars,
    varsDL,
    lhss,
    rhss,
    map,
    restrictFuns,
    -- * Predicates on Rules
    isLinear, isLeftLinear, isRightLinear,
    isGround, isLeftGround, isRightGround,
    isErasing,
    isCreating,
    isExpanding,
    isDuplicating,
    isCollapsing,
    isValid,
) where

import Prelude hiding (map)
import qualified Prelude as P
import Data.Rewriting.Rule (Rule)
import Data.Rewriting.Term (Term)
import qualified Data.Rewriting.Term as Term
import qualified Data.Rewriting.Rule as Rule


-- | @lhss rs@ returns the list of left-hand sides of @rs@
lhss :: [Rule f v] -> [Term f v]
lhss :: forall f v. [Rule f v] -> [Term f v]
lhss = (Rule f v -> Term f v) -> [Rule f v] -> [Term f v]
forall a b. (a -> b) -> [a] -> [b]
P.map Rule f v -> Term f v
forall f v. Rule f v -> Term f v
Rule.lhs

-- | @lhss rs@ returns the list of right-hand sides of @rs@
rhss :: [Rule f v] -> [Term f v]
rhss :: forall f v. [Rule f v] -> [Term f v]
rhss = (Rule f v -> Term f v) -> [Rule f v] -> [Term f v]
forall a b. (a -> b) -> [a] -> [b]
P.map Rule f v -> Term f v
forall f v. Rule f v -> Term f v
Rule.rhs

-- | Lifting of Term.'Term.funs' to list of rules.
funs :: [Rule f v] -> [f]
funs :: forall f v. [Rule f v] -> [f]
funs = ([Rule f v] -> [f] -> [f]) -> [f] -> [Rule f v] -> [f]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Rule f v] -> [f] -> [f]
forall f v. [Rule f v] -> [f] -> [f]
funsDL []

-- | Difference List version of 'funs'.
-- We have @funsDL r vs = funs r ++ vs@.
funsDL :: [Rule f v] -> [f] -> [f]
funsDL :: forall f v. [Rule f v] -> [f] -> [f]
funsDL [Rule f v]
rs [f]
fs = (Rule f v -> [f] -> [f]) -> [f] -> [Rule f v] -> [f]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Rule f v -> [f] -> [f]
forall f v. Rule f v -> [f] -> [f]
Rule.funsDL [f]
fs [Rule f v]
rs

-- | Lifting of Term.'Term.vars' to list of rules.
vars :: [Rule f v] -> [v]
vars :: forall f v. [Rule f v] -> [v]
vars = ([Rule f v] -> [v] -> [v]) -> [v] -> [Rule f v] -> [v]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Rule f v] -> [v] -> [v]
forall f v. [Rule f v] -> [v] -> [v]
varsDL []

-- | Lifting of Rule.'Rule.map' to list of rules.
map :: (f -> f') -> (v -> v') -> [Rule f v] -> [Rule f' v']
map :: forall f f' v v'.
(f -> f') -> (v -> v') -> [Rule f v] -> [Rule f' v']
map f -> f'
f v -> v'
v = (Rule f v -> Rule f' v') -> [Rule f v] -> [Rule f' v']
forall a b. (a -> b) -> [a] -> [b]
P.map ((f -> f') -> (v -> v') -> Rule f v -> Rule f' v'
forall f f' v v'. (f -> f') -> (v -> v') -> Rule f v -> Rule f' v'
Rule.map f -> f'
f v -> v'
v)

-- | Difference List version of 'vars'.
-- We have @varsDL r vs = vars r ++ vs@.
varsDL :: [Rule f v] -> [v] -> [v]
varsDL :: forall f v. [Rule f v] -> [v] -> [v]
varsDL [Rule f v]
rs [v]
fs = (Rule f v -> [v] -> [v]) -> [v] -> [Rule f v] -> [v]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Rule f v -> [v] -> [v]
forall f v. Rule f v -> [v] -> [v]
Rule.varsDL [v]
fs [Rule f v]
rs

-- | Returns 'True' iff all given rules satisfy 'Rule.isLinear'
isLinear :: Ord v => [Rule f v] -> Bool
isLinear :: forall v f. Ord v => [Rule f v] -> Bool
isLinear = (Rule f v -> Bool) -> [Rule f v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Rule f v -> Bool
forall v f. Ord v => Rule f v -> Bool
Rule.isLinear

-- | Returns 'True' iff all given rules satisfy 'Rule.isLeftLinear'
isLeftLinear :: Ord v => [Rule f v] -> Bool
isLeftLinear :: forall v f. Ord v => [Rule f v] -> Bool
isLeftLinear = (Rule f v -> Bool) -> [Rule f v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Rule f v -> Bool
forall v f. Ord v => Rule f v -> Bool
Rule.isLeftLinear

-- | Returns 'True' iff all given rules satisfy 'Rule.isRightLinear'
isRightLinear :: Ord v => [Rule f v] -> Bool
isRightLinear :: forall v f. Ord v => [Rule f v] -> Bool
isRightLinear = (Rule f v -> Bool) -> [Rule f v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Rule f v -> Bool
forall v f. Ord v => Rule f v -> Bool
Rule.isRightLinear

-- | Returns 'True' iff all given rules satisfy 'Rule.isGroundLinear'
isGround :: [Rule f v] -> Bool
isGround :: forall f v. [Rule f v] -> Bool
isGround = (Rule f v -> Bool) -> [Rule f v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Rule f v -> Bool
forall f v. Rule f v -> Bool
Rule.isGround

-- | Returns 'True' iff all given rules satisfy 'Rule.isLeftGround'
isLeftGround :: [Rule f v] -> Bool
isLeftGround :: forall f v. [Rule f v] -> Bool
isLeftGround = (Rule f v -> Bool) -> [Rule f v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Rule f v -> Bool
forall f v. Rule f v -> Bool
Rule.isLeftGround

-- | Returns 'True' iff all given rules satisfy 'Rule.isRightGround'
isRightGround :: [Rule f v] -> Bool
isRightGround :: forall f v. [Rule f v] -> Bool
isRightGround = (Rule f v -> Bool) -> [Rule f v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Rule f v -> Bool
forall f v. Rule f v -> Bool
Rule.isRightGround

-- | Returns 'True' iff any of the given rules satisfy 'Rule.isErasing'
isErasing :: Ord v => [Rule f v] -> Bool
isErasing :: forall v f. Ord v => [Rule f v] -> Bool
isErasing = (Rule f v -> Bool) -> [Rule f v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Rule f v -> Bool
forall v f. Ord v => Rule f v -> Bool
Rule.isErasing

-- | Returns 'True' iff any of the given rules satisfy 'Rule.isCreating'
isCreating :: Ord v => [Rule f v] -> Bool
isCreating :: forall v f. Ord v => [Rule f v] -> Bool
isCreating = (Rule f v -> Bool) -> [Rule f v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Rule f v -> Bool
forall v f. Ord v => Rule f v -> Bool
Rule.isCreating

-- | Returns 'True' iff any of the given rules satisfy 'Rule.isDuplicating'
isDuplicating :: Ord v => [Rule f v] -> Bool
isDuplicating :: forall v f. Ord v => [Rule f v] -> Bool
isDuplicating = (Rule f v -> Bool) -> [Rule f v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Rule f v -> Bool
forall v f. Ord v => Rule f v -> Bool
Rule.isDuplicating

-- | Returns 'True' iff any of the given rules satisfy 'Rule.isCollapsing'
isCollapsing :: [Rule f v] -> Bool
isCollapsing :: forall f v. [Rule f v] -> Bool
isCollapsing = (Rule f v -> Bool) -> [Rule f v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Rule f v -> Bool
forall f v. Rule f v -> Bool
Rule.isCollapsing

-- | Returns 'True' iff any of the given rules satisfy 'Rule.isExpanding'
isExpanding :: [Rule f v] -> Bool
isExpanding :: forall f v. [Rule f v] -> Bool
isExpanding = (Rule f v -> Bool) -> [Rule f v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Rule f v -> Bool
forall f v. Rule f v -> Bool
Rule.isExpanding

-- | Returns 'True' iff all rules satisfy 'Rule.isValid'
isValid :: Ord v => [Rule f v] -> Bool
isValid :: forall v f. Ord v => [Rule f v] -> Bool
isValid = (Rule f v -> Bool) -> [Rule f v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Rule f v -> Bool
forall v f. Ord v => Rule f v -> Bool
Rule.isValid

-- | Restrict the rules to those only using function symbols satisfying
-- the given predicate.
restrictFuns :: (f -> Bool) -> [Rule f v] -> [Rule f v]
restrictFuns :: forall f v. (f -> Bool) -> [Rule f v] -> [Rule f v]
restrictFuns f -> Bool
funp = (Rule f v -> Bool) -> [Rule f v] -> [Rule f v]
forall a. (a -> Bool) -> [a] -> [a]
filter ((f -> Bool) -> [f] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all f -> Bool
funp ([f] -> Bool) -> (Rule f v -> [f]) -> Rule f v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule f v -> [f]
forall f v. Rule f v -> [f]
Rule.funs)