module TPDB.DP.Unify ( mgu, match, unifies, apply, times ) where

import TPDB.Data
import qualified Data.Map as M
import Control.Monad ( guard, foldM )
import Data.Maybe (isJust)

type Substitution v c = M.Map v (Term v c)

unifies :: Term v c -> Term v c -> Bool
unifies Term v c
t1 Term v c
t2 = Maybe (Map v (Term v c)) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Map v (Term v c)) -> Bool)
-> Maybe (Map v (Term v c)) -> Bool
forall a b. (a -> b) -> a -> b
$ Term v c -> Term v c -> Maybe (Map v (Term v c))
forall v c.
(Ord v, Eq c) =>
Term v c -> Term v c -> Maybe (Map v (Term v c))
mgu Term v c
t1 Term v c
t2

-- | view variables as symbols
pack :: Term v c -> Term any (Either v c)
pack :: Term v c -> Term any (Either v c)
pack ( Var v
v ) = Either v c -> [Term any (Either v c)] -> Term any (Either v c)
forall v s. s -> [Term v s] -> Term v s
Node ( v -> Either v c
forall a b. a -> Either a b
Left v
v ) []
pack ( Node c
f [Term v c]
args ) = Either v c -> [Term any (Either v c)] -> Term any (Either v c)
forall v s. s -> [Term v s] -> Term v s
Node ( c -> Either v c
forall a b. b -> Either a b
Right c
f ) ( (Term v c -> Term any (Either v c))
-> [Term v c] -> [Term any (Either v c)]
forall a b. (a -> b) -> [a] -> [b]
map Term v c -> Term any (Either v c)
forall v c any. Term v c -> Term any (Either v c)
pack [Term v c]
args )

unpack :: Term any (Either v c) -> Term v c
unpack :: Term any (Either v c) -> Term v c
unpack ( Node ( Left v
v ) [] ) = v -> Term v c
forall v s. v -> Term v s
Var v
v
unpack ( Node ( Right c
f ) [Term any (Either v c)]
args ) = c -> [Term v c] -> Term v c
forall v s. s -> [Term v s] -> Term v s
Node c
f ( (Term any (Either v c) -> Term v c)
-> [Term any (Either v c)] -> [Term v c]
forall a b. (a -> b) -> [a] -> [b]
map Term any (Either v c) -> Term v c
forall any v c. Term any (Either v c) -> Term v c
unpack [Term any (Either v c)]
args )

-- | will only bind variables in the left side
match :: ( Ord v, Ord w, Eq c )
      => Term v c
      -> Term w c
      -> Maybe ( M.Map v ( Term w c ) )
match :: Term v c -> Term w c -> Maybe (Map v (Term w c))
match Term v c
l Term w c
r = do
    Map v (Term v (Either w c))
u <- Term v (Either w c)
-> Term v (Either w c) -> Maybe (Map v (Term v (Either w c)))
forall v c.
(Ord v, Eq c) =>
Term v c -> Term v c -> Maybe (Map v (Term v c))
mgu ( (c -> Either w c) -> Term v c -> Term v (Either w c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> Either w c
forall a b. b -> Either a b
Right Term v c
l ) ( Term w c -> Term v (Either w c)
forall v c any. Term v c -> Term any (Either v c)
pack Term w c
r )
    Map v (Term w c) -> Maybe (Map v (Term w c))
forall (m :: * -> *) a. Monad m => a -> m a
return (Map v (Term w c) -> Maybe (Map v (Term w c)))
-> Map v (Term w c) -> Maybe (Map v (Term w c))
forall a b. (a -> b) -> a -> b
$ (Term v (Either w c) -> Term w c)
-> Map v (Term v (Either w c)) -> Map v (Term w c)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map Term v (Either w c) -> Term w c
forall any v c. Term any (Either v c) -> Term v c
unpack  Map v (Term v (Either w c))
u


-- | naive implementation (worst case exponential)
mgu
  :: (Ord v, Eq c) =>
     Term v c -> Term v c -> Maybe (M.Map v (Term v c))
mgu :: Term v c -> Term v c -> Maybe (Map v (Term v c))
mgu Term v c
t1 Term v c
t2 | Term v c
t1 Term v c -> Term v c -> Bool
forall a. Eq a => a -> a -> Bool
== Term v c
t2 = Map v (Term v c) -> Maybe (Map v (Term v c))
forall (m :: * -> *) a. Monad m => a -> m a
return Map v (Term v c)
forall k a. Map k a
M.empty
mgu ( Var v
v ) Term v c
t2 = do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Term v c -> [Term v c] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (v -> Term v c
forall v s. v -> Term v s
Var v
v) ([Term v c] -> Bool) -> [Term v c] -> Bool
forall a b. (a -> b) -> a -> b
$ Term v c -> [Term v c]
forall v c. Term v c -> [Term v c]
subterms Term v c
t2
    Map v (Term v c) -> Maybe (Map v (Term v c))
forall (m :: * -> *) a. Monad m => a -> m a
return (Map v (Term v c) -> Maybe (Map v (Term v c)))
-> Map v (Term v c) -> Maybe (Map v (Term v c))
forall a b. (a -> b) -> a -> b
$ v -> Term v c -> Map v (Term v c)
forall k a. k -> a -> Map k a
M.singleton v
v Term v c
t2
mgu Term v c
t1 ( Var v
v ) = Term v c -> Term v c -> Maybe (Map v (Term v c))
forall v c.
(Ord v, Eq c) =>
Term v c -> Term v c -> Maybe (Map v (Term v c))
mgu ( v -> Term v c
forall v s. v -> Term v s
Var v
v ) Term v c
t1  
mgu (Node c
f1 [Term v c]
args1) (Node c
f2 [Term v c]
args2) 
    | c
f1 c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
f2 Bool -> Bool -> Bool
&& [Term v c] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term v c]
args1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Term v c] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term v c]
args2 = do
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ c
f1 c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
f2
        (Map v (Term v c)
 -> (Term v c, Term v c) -> Maybe (Map v (Term v c)))
-> Map v (Term v c)
-> [(Term v c, Term v c)]
-> Maybe (Map v (Term v c))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ( \ Map v (Term v c)
s (Term v c
l,Term v c
r) -> do
            Map v (Term v c)
t <- Term v c -> Term v c -> Maybe (Map v (Term v c))
forall v c.
(Ord v, Eq c) =>
Term v c -> Term v c -> Maybe (Map v (Term v c))
mgu (Term v c -> Map v (Term v c) -> Term v c
forall k s. Ord k => Term k s -> Map k (Term k s) -> Term k s
apply Term v c
l Map v (Term v c)
s) (Term v c -> Map v (Term v c) -> Term v c
forall k s. Ord k => Term k s -> Map k (Term k s) -> Term k s
apply Term v c
r Map v (Term v c)
s) 
            Map v (Term v c) -> Maybe (Map v (Term v c))
forall (m :: * -> *) a. Monad m => a -> m a
return (Map v (Term v c) -> Maybe (Map v (Term v c)))
-> Map v (Term v c) -> Maybe (Map v (Term v c))
forall a b. (a -> b) -> a -> b
$ Map v (Term v c) -> Map v (Term v c) -> Map v (Term v c)
forall v c.
Ord v =>
Substitution v c -> Substitution v c -> Substitution v c
times Map v (Term v c)
s Map v (Term v c)
t ) Map v (Term v c)
forall k a. Map k a
M.empty ([(Term v c, Term v c)] -> Maybe (Map v (Term v c)))
-> [(Term v c, Term v c)] -> Maybe (Map v (Term v c))
forall a b. (a -> b) -> a -> b
$ [Term v c] -> [Term v c] -> [(Term v c, Term v c)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term v c]
args1 [Term v c]
args2 
mgu Term v c
_ Term v c
_ = Maybe (Map v (Term v c))
forall a. Maybe a
Nothing
   
times :: Ord v 
      => Substitution v c -> Substitution v c -> Substitution v c
times :: Substitution v c -> Substitution v c -> Substitution v c
times Substitution v c
s Substitution v c
t = 
    Substitution v c -> Substitution v c -> Substitution v c
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union ( Substitution v c -> Substitution v c -> Substitution v c
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.difference Substitution v c
t Substitution v c
s )
            ( (Term v c -> Term v c) -> Substitution v c -> Substitution v c
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ( \ Term v c
v -> Term v c -> Substitution v c -> Term v c
forall k s. Ord k => Term k s -> Map k (Term k s) -> Term k s
apply Term v c
v Substitution v c
t ) Substitution v c
s )

apply :: Term k s -> Map k (Term k s) -> Term k s
apply Term k s
t Map k (Term k s)
s = case Term k s
t of
    Var k
v -> case  k -> Map k (Term k s) -> Maybe (Term k s)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
v Map k (Term k s)
s of Maybe (Term k s)
Nothing -> Term k s
t ; Just Term k s
w -> Term k s
w
    Node s
f [Term k s]
args -> s -> [Term k s] -> Term k s
forall v s. s -> [Term v s] -> Term v s
Node s
f ([Term k s] -> Term k s) -> [Term k s] -> Term k s
forall a b. (a -> b) -> a -> b
$ (Term k s -> Term k s) -> [Term k s] -> [Term k s]
forall a b. (a -> b) -> [a] -> [b]
map (\ Term k s
a -> Term k s -> Map k (Term k s) -> Term k s
apply Term k s
a Map k (Term k s)
s) [Term k s]
args