-- 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.Substitution.Match (
    match,
) 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

-- | Match two terms. If matching succeeds, return the resulting subtitution.
-- We have the following property:
--
-- > match t u == Just s   ==>   apply s t == gapply s t == u
match :: (Eq f, Ord v, Eq v') => Term f v -> Term f v' -> Maybe (GSubst v f v')
match :: forall f v v'.
(Eq f, Ord v, Eq v') =>
Term f v -> Term f v' -> Maybe (GSubst v f v')
match Term f v
t Term f v'
u = 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')
-> Maybe (Map v (Term f v')) -> Maybe (GSubst v f v')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term f v
-> Term f v' -> Map v (Term f v') -> Maybe (Map v (Term f v'))
forall {k} {v} {a}.
(Ord k, Eq v, Eq a) =>
Term a k
-> Term a v -> Map k (Term a v) -> Maybe (Map k (Term a v))
go Term f v
t Term f v'
u (Map v (Term f v')
forall k a. Map k a
M.empty) where
   go :: Term a k
-> Term a v -> Map k (Term a v) -> Maybe (Map k (Term a v))
go (Var k
v) Term a v
t Map k (Term a v)
subst = case k -> Map k (Term a v) -> Maybe (Term a v)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
v Map k (Term a v)
subst of
       Maybe (Term a v)
Nothing -> Map k (Term a v) -> Maybe (Map k (Term a v))
forall a. a -> Maybe a
Just (k -> Term a v -> Map k (Term a v) -> Map k (Term a v)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert k
v Term a v
t Map k (Term a v)
subst)
       Just Term a v
t' | Term a v
t Term a v -> Term a v -> Bool
forall a. Eq a => a -> a -> Bool
== Term a v
t' -> Map k (Term a v) -> Maybe (Map k (Term a v))
forall a. a -> Maybe a
Just Map k (Term a v)
subst
       Maybe (Term a v)
_ -> Maybe (Map k (Term a v))
forall a. Maybe a
Nothing
   go (Fun a
f [Term a k]
ts) (Fun a
f' [Term a v]
ts') Map k (Term a v)
subst
       | a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
f' Bool -> Bool -> Bool
|| [Term a k] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term a k]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Term a v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term a v]
ts' = Maybe (Map k (Term a v))
forall a. Maybe a
Nothing
       | Bool
otherwise = [Map k (Term a v) -> Maybe (Map k (Term a v))]
-> Map k (Term a v) -> Maybe (Map k (Term a v))
forall (m :: * -> *) a. Monad m => [a -> m a] -> a -> m a
composeM ((Term a k
 -> Term a v -> Map k (Term a v) -> Maybe (Map k (Term a v)))
-> [Term a k]
-> [Term a v]
-> [Map k (Term a v) -> Maybe (Map k (Term a v))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Term a k
-> Term a v -> Map k (Term a v) -> Maybe (Map k (Term a v))
go [Term a k]
ts [Term a v]
ts') Map k (Term a v)
subst
   go Term a k
_ Term a v
_ Map k (Term a v)
_ = Maybe (Map k (Term a v))
forall a. Maybe a
Nothing

-- TODO: move to Utils module
composeM :: Monad m => [a -> m a] -> a -> m a
composeM :: forall (m :: * -> *) a. Monad m => [a -> m a] -> a -> m a
composeM = ((a -> m a) -> (a -> m a) -> a -> m a)
-> (a -> m a) -> [a -> m a] -> a -> m a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a -> m a) -> (a -> m a) -> a -> m a
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
(>=>) a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return