-- 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

module Data.Rewriting.CriticalPair.Ops (
    -- * pairs of rewrite systems
    cps,
    cpsIn,
    cpsOut,
    -- * single rewrite systems
    cps',
    cpsIn',
    cpsOut',
) where

import Data.Rewriting.CriticalPair.Type
import Data.Rewriting.Substitution
import Data.Rewriting.Rule.Type
import qualified Data.Rewriting.Term as Term
import Data.Rewriting.Pos
import Data.Rewriting.Rules.Rewrite (listContexts)

import Data.Maybe
import Control.Monad
import Data.List

-- cpW does all the hard work:
-- Given a function that returns contexts to consider for rewriting,
-- unify the contexts of the right rule's lhs with the left rule's lhs,
-- and return the resulting critical pairs.
cpW :: (Ord v, Ord v', Eq f)
    => (Term f (Either v v')
        -> [(Pos, Context f (Either v v'), Term f (Either v v'))])
    -> Rule f v -> Rule f v' -> [(CP f v v')]
cpW :: forall v v' f.
(Ord v, Ord v', Eq f) =>
(Term f (Either v v')
 -> [(Pos, Context f (Either v v'), Term f (Either v v'))])
-> Rule f v -> Rule f v' -> [CP f v v']
cpW Term f (Either v v')
-> [(Pos, Context f (Either v v'), Term f (Either v v'))]
f Rule f v
rl Rule f v'
rr = do
    let rl' :: Term f (Either v b)
rl' = (f -> f) -> (v -> Either v b) -> Term f v -> Term f (Either v b)
forall f f' v v'. (f -> f') -> (v -> v') -> Term f v -> Term f' v'
Term.map f -> f
forall a. a -> a
id v -> Either v b
forall a b. a -> Either a b
Left (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
lhs Rule f v
rl)
        rr' :: Term f (Either a v')
rr' = (f -> f)
-> (v' -> Either a v') -> Term f v' -> Term f (Either a v')
forall f f' v v'. (f -> f') -> (v -> v') -> Term f v -> Term f' v'
Term.map f -> f
forall a. a -> a
id v' -> Either a v'
forall a b. b -> Either a b
Right (Rule f v' -> Term f v'
forall f v. Rule f v -> Term f v
lhs Rule f v'
rr)
    (Pos
pos, Context f (Either v v')
ctx, Term f (Either v v')
rr'') <- Term f (Either v v')
-> [(Pos, Context f (Either v v'), Term f (Either v v'))]
f Term f (Either v v')
forall {a}. Term f (Either a v')
rr'
    Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Term f (Either v v') -> Bool
forall f v. Term f v -> Bool
Term.isVar Term f (Either v v')
rr'')
    Subst f (Either v v')
subst <- Maybe (Subst f (Either v v')) -> [Subst f (Either v v')]
forall a. Maybe a -> [a]
maybeToList (Maybe (Subst f (Either v v')) -> [Subst f (Either v v')])
-> Maybe (Subst f (Either v v')) -> [Subst f (Either v v')]
forall a b. (a -> b) -> a -> b
$ Term f (Either v v')
-> Term f (Either v v') -> Maybe (Subst f (Either v v'))
forall f v.
(Eq f, Ord v) =>
Term f v -> Term f v -> Maybe (Subst f v)
unify Term f (Either v v')
forall {b}. Term f (Either v b)
rl' Term f (Either v v')
rr''
    CP f v v' -> [CP f v v']
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return CP{
        left :: Term f (Either v v')
left = Subst f (Either v v') -> Context f (Either v v')
forall v f. Ord v => Subst f v -> Term f v -> Term f v
apply Subst f (Either v v')
subst (Context f (Either v v')
ctx ((f -> f) -> (v -> Either v v') -> Term f v -> Term f (Either v v')
forall f f' v v'. (f -> f') -> (v -> v') -> Term f v -> Term f' v'
Term.map f -> f
forall a. a -> a
id v -> Either v v'
forall a b. a -> Either a b
Left (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
rhs Rule f v
rl))),
        top :: Term f (Either v v')
top = Subst f (Either v v') -> Context f (Either v v')
forall v f. Ord v => Subst f v -> Term f v -> Term f v
apply Subst f (Either v v')
subst Term f (Either v v')
forall {a}. Term f (Either a v')
rr',
        right :: Term f (Either v v')
right = Subst f (Either v v') -> Context f (Either v v')
forall v f. Ord v => Subst f v -> Term f v -> Term f v
apply Subst f (Either v v')
subst ((f -> f)
-> (v' -> Either v v') -> Term f v' -> Term f (Either v v')
forall f f' v v'. (f -> f') -> (v -> v') -> Term f v -> Term f' v'
Term.map f -> f
forall a. a -> a
id v' -> Either v v'
forall a b. b -> Either a b
Right (Rule f v' -> Term f v'
forall f v. Rule f v -> Term f v
rhs Rule f v'
rr)),
        leftRule :: Rule f v
leftRule = Rule f v
rl,
        leftPos :: Pos
leftPos = Pos
pos,
        rightRule :: Rule f v'
rightRule = Rule f v'
rr,
        subst :: Subst f (Either v v')
subst = Subst f (Either v v')
subst
    }


-- TODO: find a better place for this kind of contexts.
type Context f v = Term f v -> Term f v

-- Calculate contexts of a term, in pre-order.
-- In particular, the root context is returned first.
contexts :: Term f v -> [(Pos, Context f v, Term f v)]
contexts :: forall f v. Term f v -> [(Pos, Context f v, Term f v)]
contexts t :: Term f v
t@(Var v
_)    = [([], Context f v
forall a. a -> a
id, Term f v
t)]
contexts t :: Term f v
t@(Fun f
f [Term f v]
ts) = ([], Context f v
forall a. a -> a
id, Term f v
t) (Pos, Context f v, Term f v)
-> [(Pos, Context f v, Term f v)] -> [(Pos, Context f v, Term f v)]
forall a. a -> [a] -> [a]
: do
    (Int
i, Term f v -> [Term f v]
ctxL, Term f v
t) <- [Term f v] -> [(Int, Term f v -> [Term f v], Term f v)]
forall a. [a] -> [(Int, a -> [a], a)]
listContexts [Term f v]
ts
    (Pos
pos, Context f v
ctxT, Term f v
t') <- Term f v -> [(Pos, Context f v, Term f v)]
forall f v. Term f v -> [(Pos, Context f v, Term f v)]
contexts Term f v
t
    (Pos, Context f v, Term f v) -> [(Pos, Context f v, Term f v)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i Int -> Pos -> Pos
forall a. a -> [a] -> [a]
: Pos
pos, f -> [Term f v] -> Term f v
forall f v. f -> [Term f v] -> Term f v
Fun f
f ([Term f v] -> Term f v) -> (Term f v -> [Term f v]) -> Context f v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f v -> [Term f v]
ctxL (Term f v -> [Term f v]) -> Context f v -> Term f v -> [Term f v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context f v
ctxT, Term f v
t')

-- Determine critical pairs for a pair of rules.
cp :: (Ord v, Ord v', Eq f)
    => Rule f v -> Rule f v' -> [(CP f v v')]
cp :: forall v v' f.
(Ord v, Ord v', Eq f) =>
Rule f v -> Rule f v' -> [CP f v v']
cp  = (Term f (Either v v')
 -> [(Pos, Context f (Either v v'), Term f (Either v v'))])
-> Rule f v -> Rule f v' -> [CP f v v']
forall v v' f.
(Ord v, Ord v', Eq f) =>
(Term f (Either v v')
 -> [(Pos, Context f (Either v v'), Term f (Either v v'))])
-> Rule f v -> Rule f v' -> [CP f v v']
cpW Term f (Either v v')
-> [(Pos, Context f (Either v v'), Term f (Either v v'))]
forall f v. Term f v -> [(Pos, Context f v, Term f v)]
contexts

-- Determine outer critical pairs for a pair of rules.
cpOut :: (Ord v, Ord v', Eq f)
    => Rule f v -> Rule f v' -> [(CP f v v')]
cpOut :: forall v v' f.
(Ord v, Ord v', Eq f) =>
Rule f v -> Rule f v' -> [CP f v v']
cpOut = (Term f (Either v v')
 -> [(Pos, Context f (Either v v'), Term f (Either v v'))])
-> Rule f v -> Rule f v' -> [CP f v v']
forall v v' f.
(Ord v, Ord v', Eq f) =>
(Term f (Either v v')
 -> [(Pos, Context f (Either v v'), Term f (Either v v'))])
-> Rule f v -> Rule f v' -> [CP f v v']
cpW (Int
-> [(Pos, Context f (Either v v'), Term f (Either v v'))]
-> [(Pos, Context f (Either v v'), Term f (Either v v'))]
forall a. Int -> [a] -> [a]
take Int
1 ([(Pos, Context f (Either v v'), Term f (Either v v'))]
 -> [(Pos, Context f (Either v v'), Term f (Either v v'))])
-> (Term f (Either v v')
    -> [(Pos, Context f (Either v v'), Term f (Either v v'))])
-> Term f (Either v v')
-> [(Pos, Context f (Either v v'), Term f (Either v v'))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f (Either v v')
-> [(Pos, Context f (Either v v'), Term f (Either v v'))]
forall f v. Term f v -> [(Pos, Context f v, Term f v)]
contexts)

-- Determine inner critical pairs for a pair of rules.
cpIn :: (Ord v, Ord v', Eq f)
    => Rule f v -> Rule f v' -> [(CP f v v')]
cpIn :: forall v v' f.
(Ord v, Ord v', Eq f) =>
Rule f v -> Rule f v' -> [CP f v v']
cpIn = (Term f (Either v v')
 -> [(Pos, Context f (Either v v'), Term f (Either v v'))])
-> Rule f v -> Rule f v' -> [CP f v v']
forall v v' f.
(Ord v, Ord v', Eq f) =>
(Term f (Either v v')
 -> [(Pos, Context f (Either v v'), Term f (Either v v'))])
-> Rule f v -> Rule f v' -> [CP f v v']
cpW ([(Pos, Context f (Either v v'), Term f (Either v v'))]
-> [(Pos, Context f (Either v v'), Term f (Either v v'))]
forall a. HasCallStack => [a] -> [a]
tail ([(Pos, Context f (Either v v'), Term f (Either v v'))]
 -> [(Pos, Context f (Either v v'), Term f (Either v v'))])
-> (Term f (Either v v')
    -> [(Pos, Context f (Either v v'), Term f (Either v v'))])
-> Term f (Either v v')
-> [(Pos, Context f (Either v v'), Term f (Either v v'))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f (Either v v')
-> [(Pos, Context f (Either v v'), Term f (Either v v'))]
forall f v. Term f v -> [(Pos, Context f v, Term f v)]
contexts)


-- | Determine all critical pairs for a pair of TRSs.
cps :: (Ord v, Ord v', Eq f) => [Rule f v] -> [Rule f v']
    -> [(CP f v v')]
cps :: forall v v' f.
(Ord v, Ord v', Eq f) =>
[Rule f v] -> [Rule f v'] -> [CP f v v']
cps  [Rule f v]
trs1 [Rule f v']
trs2 = do
    Rule f v
rl <- [Rule f v]
trs1
    Rule f v'
rr <- [Rule f v']
trs2
    Rule f v -> Rule f v' -> [CP f v v']
forall v v' f.
(Ord v, Ord v', Eq f) =>
Rule f v -> Rule f v' -> [CP f v v']
cp Rule f v
rl Rule f v'
rr

-- | Determine all inner critical pairs for a pair of TRSs.
--
-- A critical pair is /inner/ if the left rewrite step is not a root step.
cpsIn :: (Ord v, Ord v', Eq f) => [Rule f v] -> [Rule f v']
    -> [(CP f v v')]
cpsIn :: forall v v' f.
(Ord v, Ord v', Eq f) =>
[Rule f v] -> [Rule f v'] -> [CP f v v']
cpsIn [Rule f v]
trs1 [Rule f v']
trs2 = do
    Rule f v
rl <- [Rule f v]
trs1
    Rule f v'
rr <- [Rule f v']
trs2
    Rule f v -> Rule f v' -> [CP f v v']
forall v v' f.
(Ord v, Ord v', Eq f) =>
Rule f v -> Rule f v' -> [CP f v v']
cpIn Rule f v
rl Rule f v'
rr

-- | Determine outer critical pairs for a pair of TRSs.
--
-- A critical pair is /outer/ if the left rewrite step is a root step.
cpsOut :: (Ord v, Ord v', Eq f) => [Rule f v] -> [Rule f v']
    -> [(CP f v v')]
cpsOut :: forall v v' f.
(Ord v, Ord v', Eq f) =>
[Rule f v] -> [Rule f v'] -> [CP f v v']
cpsOut [Rule f v]
trs1 [Rule f v']
trs2 = do
    Rule f v
rl <- [Rule f v]
trs1
    Rule f v'
rr <- [Rule f v']
trs2
    Rule f v -> Rule f v' -> [CP f v v']
forall v v' f.
(Ord v, Ord v', Eq f) =>
Rule f v -> Rule f v' -> [CP f v v']
cpOut Rule f v
rl Rule f v'
rr


-- | Determine all critical pairs of a single TRS with itself.
--
-- Unlike @cps@, @cps'@ takes symmetries into account. See 'cpsIn'' and
-- 'cpsOut'' for details.
cps' :: (Ord v, Eq f) => [Rule f v] -> [(CP f v v)]
cps' :: forall v f. (Ord v, Eq f) => [Rule f v] -> [CP f v v]
cps'  [Rule f v]
trs = [Rule f v] -> [CP f v v]
forall v f. (Ord v, Eq f) => [Rule f v] -> [CP f v v]
cpsIn' [Rule f v]
trs [CP f v v] -> [CP f v v] -> [CP f v v]
forall a. [a] -> [a] -> [a]
++ [Rule f v] -> [CP f v v]
forall v f. (Ord v, Eq f) => [Rule f v] -> [CP f v v]
cpsOut' [Rule f v]
trs

-- | Determine all inner critical pairs of a single TRS with itself.
--
-- The result of @cpsIn' trs@ differs from @cpsIn trs trs@ in that overlaps
-- of a rule with itself are returned once, not twice.
cpsIn' :: (Ord v, Eq f) => [Rule f v] -> [(CP f v v)]
cpsIn' :: forall v f. (Ord v, Eq f) => [Rule f v] -> [CP f v v]
cpsIn' [Rule f v]
trs = do
    Rule f v
r1 : [Rule f v]
trs' <- [Rule f v] -> [[Rule f v]]
forall a. [a] -> [[a]]
tails [Rule f v]
trs
    Rule f v -> Rule f v -> [CP f v v]
forall v v' f.
(Ord v, Ord v', Eq f) =>
Rule f v -> Rule f v' -> [CP f v v']
cpIn Rule f v
r1 Rule f v
r1 [CP f v v] -> [CP f v v] -> [CP f v v]
forall a. [a] -> [a] -> [a]
++ do
        Rule f v
r2 <- [Rule f v]
trs'
        Rule f v -> Rule f v -> [CP f v v]
forall v v' f.
(Ord v, Ord v', Eq f) =>
Rule f v -> Rule f v' -> [CP f v v']
cpIn Rule f v
r1 Rule f v
r2 [CP f v v] -> [CP f v v] -> [CP f v v]
forall a. [a] -> [a] -> [a]
++ Rule f v -> Rule f v -> [CP f v v]
forall v v' f.
(Ord v, Ord v', Eq f) =>
Rule f v -> Rule f v' -> [CP f v v']
cpIn Rule f v
r2 Rule f v
r1

-- | Determine all outer critical pairs of a single TRS with itself.
--
-- The result of @cpsOut' trs@ differs from @cpsOut trs trs@ in two aspects:
--
--  * The trivial overlaps of rules with themselves are omitted.
--
--  * Symmetry is taken into account: Overlaps between distinct rules are
--    returned once instead of twice.
cpsOut' :: (Ord v, Eq f) => [Rule f v] -> [(CP f v v)]
cpsOut' :: forall v f. (Ord v, Eq f) => [Rule f v] -> [CP f v v]
cpsOut' [Rule f v]
trs = do
    Rule f v
rl : [Rule f v]
trs' <- [Rule f v] -> [[Rule f v]]
forall a. [a] -> [[a]]
tails [Rule f v]
trs
    Rule f v
rr <- [Rule f v]
trs'
    Rule f v -> Rule f v -> [CP f v v]
forall v v' f.
(Ord v, Ord v', Eq f) =>
Rule f v -> Rule f v' -> [CP f v v']
cpOut Rule f v
rl Rule f v
rr