-- 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, Christian Sternagel

module Data.Rewriting.Substitution.Ops (
    apply,
    applyRule,
    applyCtxt,
    gApply,
    compose,
    merge,
) where

import Data.Rewriting.Substitution.Type
import qualified Data.Rewriting.Term.Type as Term
import Data.Rewriting.Term.Type (Term (..))
import Data.Rewriting.Rule.Type (Rule (..))
import Data.Rewriting.Context.Type (Ctxt (..))
import qualified Data.Map as M
import Control.Monad
import Control.Applicative

-- | Apply a substitution, assuming that it's the identity on variables not
-- mentionend in the substitution.
apply :: (Ord v) => Subst f v -> Term f v -> Term f v
apply :: forall v f. Ord v => Subst f v -> Term f v -> Term f v
apply Subst f v
subst = (v -> Term f v)
-> (f -> [Term f v] -> Term f v) -> Term f v -> Term f v
forall v a f. (v -> a) -> (f -> [a] -> a) -> Term f v -> a
Term.fold v -> Term f v
var f -> [Term f v] -> Term f v
forall {f} {v}. f -> [Term f v] -> Term f v
fun where
    var :: v -> Term f v
var v
v = Term f v -> v -> Map v (Term f v) -> Term f v
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault (v -> Term f v
forall f v. v -> Term f v
Var v
v) v
v (Subst f v -> Map v (Term f v)
forall v f v'. GSubst v f v' -> Map v (Term f v')
toMap Subst f v
subst)
    fun :: f -> [Term f v] -> Term f v
fun = f -> [Term f v] -> Term f v
forall {f} {v}. f -> [Term f v] -> Term f v
Fun

-- | Liftting of 'apply' to rules: applies the given substitution to left- and right-hand side.
applyRule :: (Ord v) => Subst f v -> Rule f v -> Rule f v
applyRule :: forall v f. Ord v => Subst f v -> Rule f v -> Rule f v
applyRule Subst f v
subst 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 (Subst f v -> Term f v -> Term f v
forall v f. Ord v => Subst f v -> Term f v -> Term f v
apply Subst f v
subst (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
lhs Rule f v
rl)) (Subst f v -> Term f v -> Term f v
forall v f. Ord v => Subst f v -> Term f v -> Term f v
apply Subst f v
subst (Rule f v -> Term f v
forall f v. Rule f v -> Term f v
rhs Rule f v
rl))

-- | Liftting of 'apply' to contexts.
applyCtxt :: Ord v => Subst f v -> Ctxt f v -> Ctxt f v
applyCtxt :: forall v f. Ord v => Subst f v -> Ctxt f v -> Ctxt f v
applyCtxt Subst f v
_ Ctxt f v
Hole = Ctxt f v
forall f v. Ctxt f v
Hole
applyCtxt Subst f v
subst (Ctxt f
f [Term f v]
ts1 Ctxt f v
ctxt [Term f v]
ts2) =
  f -> [Term f v] -> Ctxt f v -> [Term f v] -> Ctxt f v
forall f v. f -> [Term f v] -> Ctxt f v -> [Term f v] -> Ctxt f v
Ctxt f
f ((Term f v -> Term f v) -> [Term f v] -> [Term f v]
forall a b. (a -> b) -> [a] -> [b]
map (Subst f v -> Term f v -> Term f v
forall v f. Ord v => Subst f v -> Term f v -> Term f v
apply Subst f v
subst) [Term f v]
ts1) (Subst f v -> Ctxt f v -> Ctxt f v
forall v f. Ord v => Subst f v -> Ctxt f v -> Ctxt f v
applyCtxt Subst f v
subst Ctxt f v
ctxt) ((Term f v -> Term f v) -> [Term f v] -> [Term f v]
forall a b. (a -> b) -> [a] -> [b]
map (Subst f v -> Term f v -> Term f v
forall v f. Ord v => Subst f v -> Term f v -> Term f v
apply Subst f v
subst) [Term f v]
ts2)


-- | Apply a substitution, assuming that it's total. If the term contains
-- a variable not defined by the substitution, return 'Nothing'.
gApply :: (Ord v) => GSubst v f v' -> Term f v -> Maybe (Term f v')
gApply :: forall v f v'.
Ord v =>
GSubst v f v' -> Term f v -> Maybe (Term f v')
gApply GSubst v f v'
subst = (v -> Maybe (Term f v'))
-> (f -> [Maybe (Term f v')] -> Maybe (Term f v'))
-> Term f v
-> Maybe (Term f v')
forall v a f. (v -> a) -> (f -> [a] -> a) -> Term f v -> a
Term.fold v -> Maybe (Term f v')
var f -> [Maybe (Term f v')] -> Maybe (Term f v')
forall {f :: * -> *} {f} {v}.
Monad f =>
f -> [f (Term f v)] -> f (Term f v)
fun where
    var :: v -> Maybe (Term f v')
var v
v = v -> Map v (Term f v') -> Maybe (Term f v')
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup v
v (GSubst v f v' -> Map v (Term f v')
forall v f v'. GSubst v f v' -> Map v (Term f v')
toMap GSubst v f v'
subst)
    fun :: f -> [f (Term f v)] -> f (Term f v)
fun f
f [f (Term f v)]
ts = 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) -> f [Term f v] -> f (Term f v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [f (Term f v)] -> f [Term f v]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [f (Term f v)]
ts

-- | Compose substitutions. We have
--
-- > (s1 `compose` s2) `apply` t = s1 `apply` (s2 `apply` t).
compose :: (Ord v) => Subst f v -> Subst f v -> Subst f v
compose :: forall v f. Ord v => Subst f v -> Subst f v -> Subst f v
compose Subst f v
subst Subst f v
subst' =
    Map v (Term f v) -> Subst f v
forall v f v'. Map v (Term f v') -> GSubst v f v'
fromMap ((Term f v -> Term f v -> Term f v)
-> Map v (Term f v) -> Map v (Term f v) -> Map v (Term f v)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Term f v -> Term f v -> Term f v
forall a b. a -> b -> a
const (Subst f v -> Term f v -> Term f v
forall v f. Ord v => Subst f v -> Term f v -> Term f v
apply Subst f v
subst (Term f v -> Term f v) -> Map v (Term f v) -> Map v (Term f v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subst f v -> Map v (Term f v)
forall v f v'. GSubst v f v' -> Map v (Term f v')
toMap Subst f v
subst') (Subst f v -> Map v (Term f v)
forall v f v'. GSubst v f v' -> Map v (Term f v')
toMap Subst f v
subst))

-- | Merge two substitutions. The operation fails if some variable is
-- different terms by the substitutions.
merge :: (Ord v, Eq f, Eq v')
    => GSubst v f v' -> GSubst v f v' -> Maybe (GSubst v f v')
merge :: 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'
subst GSubst v f v'
subst' = do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (Map v Bool -> [Bool]
forall k a. Map k a -> [a]
M.elems ((Term f v' -> Term f v' -> Bool)
-> Map v (Term f v') -> Map v (Term f v') -> Map v Bool
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith Term f v' -> Term f v' -> Bool
forall a. Eq a => a -> a -> Bool
(==) (GSubst v f v' -> Map v (Term f v')
forall v f v'. GSubst v f v' -> Map v (Term f v')
toMap GSubst v f v'
subst) (GSubst v f v' -> Map v (Term f v')
forall v f v'. GSubst v f v' -> Map v (Term f v')
toMap GSubst v f v'
subst')))
    GSubst v f v' -> Maybe (GSubst v f v')
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (GSubst v f v' -> Maybe (GSubst v f v'))
-> GSubst v f v' -> Maybe (GSubst v f v')
forall a b. (a -> b) -> a -> b
$ Map v (Term f v') -> GSubst v f v'
forall v f v'. Map v (Term f v') -> GSubst v f v'
fromMap (Map v (Term f v') -> GSubst v f v')
-> Map v (Term f v') -> GSubst v f v'
forall a b. (a -> b) -> a -> b
$ Map v (Term f v') -> Map v (Term f v') -> Map v (Term f v')
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union (GSubst v f v' -> Map v (Term f v')
forall v f v'. GSubst v f v' -> Map v (Term f v')
toMap GSubst v f v'
subst) (GSubst v f v' -> Map v (Term f v')
forall v f v'. GSubst v f v' -> Map v (Term f v')
toMap GSubst v f v'
subst')