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

{-# LANGUAGE BangPatterns #-}
-- |
-- Simple rewriting.
--
-- Note: The rules are assumed to be non-creating, i.e., variables on the
-- rhs should also occur on the lhs. Rules violating this constraint
-- will have no effect.
module Data.Rewriting.Rules.Rewrite (
    Reduct (..),
    Strategy,
    fullRewrite,
    outerRewrite,
    innerRewrite,
    rootRewrite,
    -- * utilities not reexported from "Data.Rewriting.Rules"
    nested,
    listContexts,
) where

import Data.Rewriting.Substitution
import Data.Rewriting.Pos
import Data.Rewriting.Rule

import Data.Maybe

-- | A reduct. It contains the resulting term, the position that the term
-- was rewritten at, and the applied rule.
data Reduct f v v' = Reduct {
     forall f v v'. Reduct f v v' -> Term f v
result :: Term f v,
     forall f v v'. Reduct f v v' -> Pos
pos :: Pos,
     forall f v v'. Reduct f v v' -> Rule f v'
rule :: Rule f v',
     forall f v v'. Reduct f v v' -> GSubst v' f v
subst :: GSubst v' f v
}

-- | A rewrite strategy.
type Strategy f v v' = Term f v -> [Reduct f v v']

-- | Full rewriting: Apply rules anywhere in the term.
--
-- Reducts are returned in pre-order: the first is a leftmost, outermost redex.
fullRewrite :: (Ord v', Eq v, Eq f)
    => [Rule f v'] -> Strategy f v v'
fullRewrite :: forall v' v f.
(Ord v', Eq v, Eq f) =>
[Rule f v'] -> Strategy f v v'
fullRewrite [Rule f v']
trs Term f v
t = [Rule f v'] -> Strategy f v v'
forall v' v f.
(Ord v', Eq v, Eq f) =>
[Rule f v'] -> Strategy f v v'
rootRewrite [Rule f v']
trs Term f v
t [Reduct f v v'] -> [Reduct f v v'] -> [Reduct f v v']
forall a. [a] -> [a] -> [a]
++ Strategy f v v' -> Strategy f v v'
forall f v v'. Strategy f v v' -> Strategy f v v'
nested ([Rule f v'] -> Strategy f v v'
forall v' v f.
(Ord v', Eq v, Eq f) =>
[Rule f v'] -> Strategy f v v'
fullRewrite [Rule f v']
trs) Term f v
t

-- | Outer rewriting: Apply rules at outermost redexes.
--
-- Reducts are returned in left to right order.
outerRewrite :: (Ord v', Eq v, Eq f)
    => [Rule f v'] -> Strategy f v v'
outerRewrite :: forall v' v f.
(Ord v', Eq v, Eq f) =>
[Rule f v'] -> Strategy f v v'
outerRewrite [Rule f v']
trs Term f v
t = case [Rule f v'] -> Strategy f v v'
forall v' v f.
(Ord v', Eq v, Eq f) =>
[Rule f v'] -> Strategy f v v'
rootRewrite [Rule f v']
trs Term f v
t of
    [] -> Strategy f v v' -> Strategy f v v'
forall f v v'. Strategy f v v' -> Strategy f v v'
nested ([Rule f v'] -> Strategy f v v'
forall v' v f.
(Ord v', Eq v, Eq f) =>
[Rule f v'] -> Strategy f v v'
outerRewrite [Rule f v']
trs) Term f v
t
    [Reduct f v v']
rs -> [Reduct f v v']
rs

-- | Inner rewriting: Apply rules at innermost redexes.
--
-- Reducts are returned in left to right order.
innerRewrite :: (Ord v', Eq v, Eq f)
    => [Rule f v'] -> Strategy f v v'
innerRewrite :: forall v' v f.
(Ord v', Eq v, Eq f) =>
[Rule f v'] -> Strategy f v v'
innerRewrite [Rule f v']
trs Term f v
t = case Strategy f v v' -> Strategy f v v'
forall f v v'. Strategy f v v' -> Strategy f v v'
nested ([Rule f v'] -> Strategy f v v'
forall v' v f.
(Ord v', Eq v, Eq f) =>
[Rule f v'] -> Strategy f v v'
innerRewrite [Rule f v']
trs) Term f v
t of
    [] -> [Rule f v'] -> Strategy f v v'
forall v' v f.
(Ord v', Eq v, Eq f) =>
[Rule f v'] -> Strategy f v v'
rootRewrite [Rule f v']
trs Term f v
t
    [Reduct f v v']
rs -> [Reduct f v v']
rs

-- | Root rewriting: Apply rules only at the root of the term.
--
-- This is mainly useful as a building block for various rewriting strategies.
rootRewrite :: (Ord v', Eq v, Eq f)
    => [Rule f v'] -> Strategy f v v'
rootRewrite :: forall v' v f.
(Ord v', Eq v, Eq f) =>
[Rule f v'] -> Strategy f v v'
rootRewrite [Rule f v']
trs Term f v
t = do
    Rule f v'
r <- [Rule f v']
trs
    GSubst v' f v
s <- Maybe (GSubst v' f v) -> [GSubst v' f v]
forall a. Maybe a -> [a]
maybeToList (Maybe (GSubst v' f v) -> [GSubst v' f v])
-> Maybe (GSubst v' f v) -> [GSubst v' f v]
forall a b. (a -> b) -> a -> b
$ 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) Term f v
t
    Term f v
t' <- Maybe (Term f v) -> [Term f v]
forall a. Maybe a -> [a]
maybeToList (Maybe (Term f v) -> [Term f v]) -> Maybe (Term f v) -> [Term f v]
forall a b. (a -> b) -> a -> b
$ GSubst v' f v -> Term f v' -> Maybe (Term f v)
forall v f v'.
Ord v =>
GSubst v f v' -> Term f v -> Maybe (Term f v')
gApply GSubst v' f v
s (Rule f v' -> Term f v'
forall f v. Rule f v -> Term f v
rhs Rule f v'
r)
    Reduct f v v' -> [Reduct f v v']
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Reduct{ result :: Term f v
result = Term f v
t', pos :: Pos
pos = [], rule :: Rule f v'
rule = Rule f v'
r, subst :: GSubst v' f v
subst = GSubst v' f v
s }

-- | Nested rewriting: Apply a rewriting strategy to all arguments of a
-- function symbol, left to right. For variables, the result will be empty.
--
-- This is another building block for rewriting strategies.
nested :: Strategy f v v' -> Strategy f v v'
nested :: forall f v v'. Strategy f v v' -> Strategy f v v'
nested Strategy f v v'
_ (Var v
_) = []
nested Strategy f v v'
s (Fun f
f [Term f v]
ts) = do
    (Int
n, Term f v -> [Term f v]
cl, 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
    (\Reduct f v v'
r -> Reduct f v v'
r{ result = Fun f (cl (result r)), pos = n : pos r }) (Reduct f v v' -> Reduct f v v')
-> [Reduct f v v'] -> [Reduct f v v']
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Strategy f v v'
s Term f v
t

-- | Return a list of contexts of a list. Each returned element is an element
-- index (starting from 0), a function that replaces the list element by a
-- new one, and the original element.
listContexts :: [a] -> [(Int, a -> [a], a)]
listContexts :: forall a. [a] -> [(Int, a -> [a], a)]
listContexts = Int -> ([a] -> [a]) -> [a] -> [(Int, a -> [a], a)]
forall {t} {c} {c}.
Num t =>
t -> ([c] -> c) -> [c] -> [(t, c -> c, c)]
go Int
0 [a] -> [a]
forall a. a -> a
id where
    go :: t -> ([c] -> c) -> [c] -> [(t, c -> c, c)]
go !t
n [c] -> c
f [] = []
    go !t
n [c] -> c
f (c
x:[c]
xs) = (t
n, [c] -> c
f ([c] -> c) -> (c -> [c]) -> c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c -> [c] -> [c]
forall a. a -> [a] -> [a]
: [c]
xs), c
x) (t, c -> c, c) -> [(t, c -> c, c)] -> [(t, c -> c, c)]
forall a. a -> [a] -> [a]
: t -> ([c] -> c) -> [c] -> [(t, c -> c, c)]
go (t
nt -> t -> t
forall a. Num a => a -> a -> a
+t
1) ([c] -> c
f ([c] -> c) -> ([c] -> [c]) -> [c] -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c
xc -> [c] -> [c]
forall a. a -> [a] -> [a]
:)) [c]
xs