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

module Data.Rewriting.Rule.Ops (
    -- * Operations on Rules
    funs,
    funsDL,
    vars,
    varsDL,
    left,
    right,
    rename,
    -- * Predicates on Rules
    both,
    isLinear, isLeftLinear, isRightLinear,
    isGround, isLeftGround, isRightGround,
    isErasing,
    isCreating,
    isDuplicating,
    isCollapsing,
    isExpanding,
    isValid,
    isInstanceOf,
    isVariantOf,
) where

import Data.Rewriting.Rule.Type
import Data.Rewriting.Substitution (match, merge)
import qualified Data.Rewriting.Term as Term

import qualified Data.Set as S
import qualified Data.MultiSet as MS
import Data.Maybe

-- | Test whether the given predicate is true for both sides of a rule.
both :: (Term f v -> Bool) -> Rule f v -> Bool
both :: forall f v. (Term f v -> Bool) -> Rule f v -> Bool
both Term f v -> Bool
p Rule f v
r = Term f v -> Bool
p (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
lhs Rule f v
r) Bool -> Bool -> Bool
&& Term f v -> Bool
p (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
rhs Rule f v
r)

-- | Apply a function to the lhs of a rule.
left :: (Term f v -> a) -> Rule f v -> a
left :: forall f v a. (Term f v -> a) -> Rule f v -> a
left Term f v -> a
f = Term f v -> a
f (Term f v -> a) -> (Rule f v -> Term f v) -> Rule f v -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule f v -> Term f v
forall f v. Rule f v -> Term f v
lhs

-- | Apply a function to the rhs of a rule.
right :: (Term f v -> a) -> Rule f v -> a
right :: forall f v a. (Term f v -> a) -> Rule f v -> a
right Term f v -> a
f = Term f v -> a
f (Term f v -> a) -> (Rule f v -> Term f v) -> Rule f v -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule f v -> Term f v
forall f v. Rule f v -> Term f v
rhs


-- | Lifting of 'Term.rename' to 'Rule': renames left- and right-hand sides.
-- 
-- >>> rename (+ 1) $ Rule {lhs = (Fun 'f' [Var 1, Fun 'g' [Var 2]]), rhs = Fun 'g' [Var 1]}
-- Rule {lhs = Fun 'f' [Var 2, Fun 'g' [Var 3]], rhs = Fun 'g' [Var 2]}
rename :: (v -> v') -> Rule f v -> Rule f v'
rename :: forall v v' f. (v -> v') -> Rule f v -> Rule f v'
rename v -> v'
f Rule f v
rl = Term f v' -> Term f v' -> Rule f v'
forall f v. Term f v -> Term f v -> Rule f v
Rule ((Term f v -> Term f v') -> Rule f v -> Term f v'
forall f v a. (Term f v -> a) -> Rule f v -> a
left ((v -> v') -> Term f v -> Term f v'
forall v v' f. (v -> v') -> Term f v -> Term f v'
Term.rename v -> v'
f) Rule f v
rl) ((Term f v -> Term f v') -> Rule f v -> Term f v'
forall f v a. (Term f v -> a) -> Rule f v -> a
right ((v -> v') -> Term f v -> Term f v'
forall v v' f. (v -> v') -> Term f v -> Term f v'
Term.rename v -> v'
f) Rule f v
rl)


-- | Lifting of 'Term.funs' to 'Rule': returns the list of function symbols
-- in left- and right-hand sides.
--
-- >>> funs $ Rule {lhs = Fun 'f' [Var 3, Fun 'g' [Fun 'f' []]], rhs = Fun 'h' [Fun 'f' []]}
-- "fgfhf"
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
r = Term f v -> [f] -> [f]
forall f v. Term f v -> [f] -> [f]
Term.funsDL (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
lhs Rule f v
r) ([f] -> [f]) -> ([f] -> [f]) -> [f] -> [f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f v -> [f] -> [f]
forall f v. Term f v -> [f] -> [f]
Term.funsDL (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
rhs Rule f v
r)

-- | Lifting of 'Term.vars' to 'Rule': returns the list of variables in
-- left- and right-hand sides.
--
-- >>> vars $ Rule {lhs = Fun 'g' [Var 3, Fun 'f' [Var 1, Var 2, Var 3]], rhs = Fun 'g' [Var 4, Var 3]}
-- [3,1,2,3,4,3]
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 []

-- | 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
r = Term f v -> [v] -> [v]
forall f v. Term f v -> [v] -> [v]
Term.varsDL (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
lhs Rule f v
r) ([v] -> [v]) -> ([v] -> [v]) -> [v] -> [v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f v -> [v] -> [v]
forall f v. Term f v -> [v] -> [v]
Term.varsDL (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
rhs Rule f v
r)

-- | Check whether both sides of the given rule are linear.
isLinear :: Ord v => Rule f v -> Bool
isLinear :: forall v f. Ord v => Rule f v -> Bool
isLinear = (Term f v -> Bool) -> Rule f v -> Bool
forall f v. (Term f v -> Bool) -> Rule f v -> Bool
both Term f v -> Bool
forall v f. Ord v => Term f v -> Bool
Term.isLinear

-- | Check whether the left hand side of the given rule is linear.
isLeftLinear :: Ord v => Rule f v -> Bool
isLeftLinear :: forall v f. Ord v => Rule f v -> Bool
isLeftLinear = (Term f v -> Bool) -> Rule f v -> Bool
forall f v a. (Term f v -> a) -> Rule f v -> a
left Term f v -> Bool
forall v f. Ord v => Term f v -> Bool
Term.isLinear

-- | Check whether the right hand side of the given rule is linear.
isRightLinear :: Ord v => Rule f v -> Bool
isRightLinear :: forall v f. Ord v => Rule f v -> Bool
isRightLinear = (Term f v -> Bool) -> Rule f v -> Bool
forall f v a. (Term f v -> a) -> Rule f v -> a
right Term f v -> Bool
forall v f. Ord v => Term f v -> Bool
Term.isLinear

-- | Check whether both sides of the given rule is are ground terms.
isGround :: Rule f v -> Bool
isGround :: forall f v. Rule f v -> Bool
isGround = (Term f v -> Bool) -> Rule f v -> Bool
forall f v. (Term f v -> Bool) -> Rule f v -> Bool
both Term f v -> Bool
forall f v. Term f v -> Bool
Term.isGround

-- | Check whether the left hand side of the given rule is a ground term.
isLeftGround :: Rule f v -> Bool
isLeftGround :: forall f v. Rule f v -> Bool
isLeftGround = (Term f v -> Bool) -> Rule f v -> Bool
forall f v a. (Term f v -> a) -> Rule f v -> a
left Term f v -> Bool
forall f v. Term f v -> Bool
Term.isGround

-- | Check whether the right hand side of the given rule is a ground term.
isRightGround :: Rule f v -> Bool
isRightGround :: forall f v. Rule f v -> Bool
isRightGround = (Term f v -> Bool) -> Rule f v -> Bool
forall f v a. (Term f v -> a) -> Rule f v -> a
right Term f v -> Bool
forall f v. Term f v -> Bool
Term.isGround

-- auxiliary: return variables of term as Set
varsS :: Ord v => Term f v -> S.Set v
varsS :: forall v f. Ord v => Term f v -> Set v
varsS = [v] -> Set v
forall a. Ord a => [a] -> Set a
S.fromList ([v] -> Set v) -> (Term f v -> [v]) -> Term f v -> Set v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f v -> [v]
forall f v. Term f v -> [v]
Term.vars

-- | Check whether the given rule is erasing, i.e., if some variable
-- occurs in the left hand side but not in the right hand side.
isErasing :: Ord v => Rule f v -> Bool
isErasing :: forall v f. Ord v => Rule f v -> Bool
isErasing Rule f v
r = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Term f v -> Set v
forall v f. Ord v => Term f v -> Set v
varsS (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
lhs Rule f v
r) Set v -> Set v -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Term f v -> Set v
forall v f. Ord v => Term f v -> Set v
varsS (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
rhs Rule f v
r)

-- | Check whether the given rule is creating, i.e., if some variable
-- occurs in its right hand side that does not occur in its left hand side.
--
-- This is the dual of 'isErasing'. The term /creating/ is non-standard.
-- Creating rules are usually forbidden. See also 'isValid'.
isCreating :: Ord v => Rule f v -> Bool
isCreating :: forall v f. Ord v => Rule f v -> Bool
isCreating Rule f v
r = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Term f v -> Set v
forall v f. Ord v => Term f v -> Set v
varsS (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
rhs Rule f v
r) Set v -> Set v -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Term f v -> Set v
forall v f. Ord v => Term f v -> Set v
varsS (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
lhs Rule f v
r)

-- auxiliary: return variables of term as MultiSet
varsMS :: Ord v => Term f v -> MS.MultiSet v
varsMS :: forall v f. Ord v => Term f v -> MultiSet v
varsMS = [v] -> MultiSet v
forall a. Ord a => [a] -> MultiSet a
MS.fromList ([v] -> MultiSet v) -> (Term f v -> [v]) -> Term f v -> MultiSet v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f v -> [v]
forall f v. Term f v -> [v]
Term.vars

-- | Check whether the given rule is duplicating, i.e., if some variable
-- occurs more often in its right hand side than in its left hand side.
isDuplicating :: Ord v => Rule f v -> Bool
isDuplicating :: forall v f. Ord v => Rule f v -> Bool
isDuplicating Rule f v
r = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Term f v -> MultiSet v
forall v f. Ord v => Term f v -> MultiSet v
varsMS (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
rhs Rule f v
r) MultiSet v -> MultiSet v -> Bool
forall a. Ord a => MultiSet a -> MultiSet a -> Bool
`MS.isSubsetOf` Term f v -> MultiSet v
forall v f. Ord v => Term f v -> MultiSet v
varsMS (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
lhs Rule f v
r)

-- | Check whether the given rule is collapsing, i.e., if its right
-- hand side is a variable.
isCollapsing :: Rule f v -> Bool
isCollapsing :: forall f v. Rule f v -> Bool
isCollapsing = Term f v -> Bool
forall f v. Term f v -> Bool
Term.isVar (Term f v -> Bool) -> (Rule f v -> Term f v) -> Rule f v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule f v -> Term f v
forall f v. Rule f v -> Term f v
rhs

-- | Check whether the given rule is expanding, i.e., if its left hand
-- sides is a variable.
--
-- This is the dual of 'isCollapsing'. The term /expanding/ is non-standard.
-- Expanding rules are usually forbidden. See also 'isValid'.
isExpanding :: Rule f v -> Bool
isExpanding :: forall f v. Rule f v -> Bool
isExpanding = Term f v -> Bool
forall f v. Term f v -> Bool
Term.isVar (Term f v -> Bool) -> (Rule f v -> Term f v) -> Rule f v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule f v -> Term f v
forall f v. Rule f v -> Term f v
lhs

-- | Check whether the given rule is non-creating and non-expanding.
-- See also 'isCreating' and 'isExpanding'
isValid :: Ord v => Rule f v -> Bool
isValid :: forall v f. Ord v => Rule f v -> Bool
isValid Rule f v
r = Bool -> Bool
not (Rule f v -> Bool
forall v f. Ord v => Rule f v -> Bool
isCreating Rule f v
r) Bool -> Bool -> Bool
&& Bool -> Bool
not (Rule f v -> Bool
forall f v. Rule f v -> Bool
isExpanding Rule f v
r)

-- | Check whether the first rule is an instance of the second rule.
isInstanceOf :: (Eq f, Ord v, Ord v') => Rule f v -> Rule f v' -> Bool
isInstanceOf :: forall f v v'.
(Eq f, Ord v, Ord v') =>
Rule f v -> Rule f v' -> Bool
isInstanceOf Rule f v
r Rule f v'
r' = case (Term f v' -> Term f v -> Maybe (GSubst v' f v)
forall f v v'.
(Eq f, Ord v, Eq v') =>
Term f v -> Term f v' -> Maybe (GSubst v f v')
match (Rule f v' -> Term f v'
forall f v. Rule f v -> Term f v
lhs Rule f v'
r') (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
lhs Rule f v
r), Term f v' -> Term f v -> Maybe (GSubst v' f v)
forall f v v'.
(Eq f, Ord v, Eq v') =>
Term f v -> Term f v' -> Maybe (GSubst v f v')
match (Rule f v' -> Term f v'
forall f v. Rule f v -> Term f v
rhs Rule f v'
r') (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
rhs Rule f v
r)) of
    (Just GSubst v' f v
s, Just GSubst v' f v
s') -> Maybe (GSubst v' f v) -> Bool
forall a. Maybe a -> Bool
isJust (GSubst v' f v -> GSubst v' f v -> Maybe (GSubst v' f v)
forall v f v'.
(Ord v, Eq f, Eq v') =>
GSubst v f v' -> GSubst v f v' -> Maybe (GSubst v f v')
merge GSubst v' f v
s GSubst v' f v
s')
    (Maybe (GSubst v' f v), Maybe (GSubst v' f v))
_ -> Bool
False

-- | Check whether two rules are variants of each other.
isVariantOf :: (Eq f, Ord v, Ord v') => Rule f v -> Rule f v' -> Bool
isVariantOf :: forall f v v'.
(Eq f, Ord v, Ord v') =>
Rule f v -> Rule f v' -> Bool
isVariantOf Rule f v
t Rule f v'
u = Rule f v -> Rule f v' -> Bool
forall f v v'.
(Eq f, Ord v, Ord v') =>
Rule f v -> Rule f v' -> Bool
isInstanceOf Rule f v
t Rule f v'
u Bool -> Bool -> Bool
&& Rule f v' -> Rule f v -> Bool
forall f v v'.
(Eq f, Ord v, Ord v') =>
Rule f v -> Rule f v' -> Bool
isInstanceOf Rule f v'
u Rule f v
t