module Data.Rewriting.Substitution.Ops (
apply,
gApply,
compose,
merge,
) where
import Data.Rewriting.Substitution.Type
import qualified Data.Rewriting.Term.Type as Term
import Data.Rewriting.Term.Type (Term (..))
import qualified Data.Map as M
import Control.Monad
import Control.Applicative
apply :: (Ord v) => Subst f v -> Term f v -> Term f v
apply subst = Term.fold var fun where
var v = M.findWithDefault (Var v) v (toMap subst)
fun = Fun
gApply :: (Ord v) => GSubst v f v' -> Term f v -> Maybe (Term f v')
gApply subst = Term.fold var fun where
var v = M.lookup v (toMap subst)
fun f ts = Fun f <$> sequence ts
compose :: (Ord v) => Subst f v -> Subst f v -> Subst f v
compose subst subst' =
fromMap (M.unionWith const (apply subst <$> toMap subst') (toMap subst))
merge :: (Ord v, Eq f, Eq v')
=> GSubst v f v' -> GSubst v f v' -> Maybe (GSubst v f v')
merge subst subst' = do
guard $ and (M.elems (M.intersectionWith (==) (toMap subst) (toMap subst')))
return $ fromMap $ M.union (toMap subst) (toMap subst')