{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Matching
-- Copyright   :  (c) 2010-2011 Patrick Bahr
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module implements matching of contexts or terms with variables againts terms
--
--------------------------------------------------------------------------------

module Data.Comp.Matching
    (
     matchCxt,
     matchTerm,
     module Data.Comp.Variables
    ) where

import Data.Comp.Equality
import Data.Comp.Term
import Data.Comp.Variables
import Data.Foldable
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Traversable

import Prelude hiding (all, mapM, mapM_)

{-| This is an auxiliary function for implementing 'matchCxt'. It behaves
similarly as 'match' but is oblivious to non-linearity. Therefore, the
substitution that is returned maps holes to non-empty lists of terms
(resp. contexts in general). This substitution is only a matching
substitution if all elements in each list of the substitution's range
are equal. -}

matchCxt' :: (Ord v, EqF f, Functor f, Foldable f)
       => Context f v -> Cxt h f a -> Maybe (Map v [Cxt h f a])
matchCxt' :: Context f v -> Cxt h f a -> Maybe (Map v [Cxt h f a])
matchCxt' (Hole v
v) Cxt h f a
t = Map v [Cxt h f a] -> Maybe (Map v [Cxt h f a])
forall a. a -> Maybe a
Just (Map v [Cxt h f a] -> Maybe (Map v [Cxt h f a]))
-> Map v [Cxt h f a] -> Maybe (Map v [Cxt h f a])
forall a b. (a -> b) -> a -> b
$  v -> [Cxt h f a] -> Map v [Cxt h f a]
forall k a. k -> a -> Map k a
Map.singleton v
v [Cxt h f a
t]
matchCxt' (Term f (Context f v)
s) (Term f (Cxt h f a)
t) = do
  [(Context f v, Cxt h f a)]
eqs <- f (Context f v)
-> f (Cxt h f a) -> Maybe [(Context f v, Cxt h f a)]
forall (f :: * -> *) a b.
(EqF f, Functor f, Foldable f) =>
f a -> f b -> Maybe [(a, b)]
eqMod f (Context f v)
s f (Cxt h f a)
t
  [Map v [Cxt h f a]]
substs <- ((Context f v, Cxt h f a) -> Maybe (Map v [Cxt h f a]))
-> [(Context f v, Cxt h f a)] -> Maybe [Map v [Cxt h f a]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Context f v -> Cxt h f a -> Maybe (Map v [Cxt h f a]))
-> (Context f v, Cxt h f a) -> Maybe (Map v [Cxt h f a])
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Context f v -> Cxt h f a -> Maybe (Map v [Cxt h f a])
forall v (f :: * -> *) h a.
(Ord v, EqF f, Functor f, Foldable f) =>
Context f v -> Cxt h f a -> Maybe (Map v [Cxt h f a])
matchCxt') [(Context f v, Cxt h f a)]
eqs
  Map v [Cxt h f a] -> Maybe (Map v [Cxt h f a])
forall (m :: * -> *) a. Monad m => a -> m a
return (Map v [Cxt h f a] -> Maybe (Map v [Cxt h f a]))
-> Map v [Cxt h f a] -> Maybe (Map v [Cxt h f a])
forall a b. (a -> b) -> a -> b
$ ([Cxt h f a] -> [Cxt h f a] -> [Cxt h f a])
-> [Map v [Cxt h f a]] -> Map v [Cxt h f a]
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith [Cxt h f a] -> [Cxt h f a] -> [Cxt h f a]
forall a. [a] -> [a] -> [a]
(++) [Map v [Cxt h f a]]
substs
matchCxt' Term {} Hole {} = Maybe (Map v [Cxt h f a])
forall a. Maybe a
Nothing


{-| This function takes a context @c@ as the first argument and tries
to match it against the term @t@ (or in general a context with holes
in @a@). The context @c@ matches the term @t@ if there is a
/matching substitution/ @s@ that maps holes to terms (resp. contexts in general)
such that if the holes in the context @c@ are replaced according to
the substitution @s@, the term @t@ is obtained. Note that the context
@c@ might be non-linear, i.e. has multiple holes that are
equal. According to the above definition this means that holes with
equal holes have to be instantiated by equal terms! -}

matchCxt :: (Ord v,EqF f, Eq (Cxt h f a), Functor f, Foldable f)
         => Context f v -> Cxt h f a -> Maybe (CxtSubst h a f v)
matchCxt :: Context f v -> Cxt h f a -> Maybe (CxtSubst h a f v)
matchCxt Context f v
c1 Cxt h f a
c2 = do
  Map v [Cxt h f a]
res <- Context f v -> Cxt h f a -> Maybe (Map v [Cxt h f a])
forall v (f :: * -> *) h a.
(Ord v, EqF f, Functor f, Foldable f) =>
Context f v -> Cxt h f a -> Maybe (Map v [Cxt h f a])
matchCxt' Context f v
c1 Cxt h f a
c2
  let insts :: [[Cxt h f a]]
insts = Map v [Cxt h f a] -> [[Cxt h f a]]
forall k a. Map k a -> [a]
Map.elems Map v [Cxt h f a]
res
  ([Cxt h f a] -> Maybe ()) -> [[Cxt h f a]] -> Maybe ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Cxt h f a] -> Maybe ()
forall a. Eq a => [a] -> Maybe ()
checkEq [[Cxt h f a]]
insts
  CxtSubst h a f v -> Maybe (CxtSubst h a f v)
forall (m :: * -> *) a. Monad m => a -> m a
return (CxtSubst h a f v -> Maybe (CxtSubst h a f v))
-> CxtSubst h a f v -> Maybe (CxtSubst h a f v)
forall a b. (a -> b) -> a -> b
$ ([Cxt h f a] -> Cxt h f a) -> Map v [Cxt h f a] -> CxtSubst h a f v
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map [Cxt h f a] -> Cxt h f a
forall a. [a] -> a
head Map v [Cxt h f a]
res
    where checkEq :: [a] -> Maybe ()
checkEq [] = Maybe ()
forall a. Maybe a
Nothing
          checkEq (a
c : [a]
cs)
              | (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c) [a]
cs = () -> Maybe ()
forall a. a -> Maybe a
Just ()
              | Bool
otherwise = Maybe ()
forall a. Maybe a
Nothing

{-| This function is similar to 'matchCxt' but instead of a context it
matches a term with variables against a context.  -}

matchTerm :: (Ord v, EqF f, Eq (Cxt h f a) , Traversable f, HasVars f v)
          => Term f -> Cxt h f a -> Maybe (CxtSubst h a f v)
matchTerm :: Term f -> Cxt h f a -> Maybe (CxtSubst h a f v)
matchTerm Term f
t = Context f v -> Cxt h f a -> Maybe (CxtSubst h a f v)
forall v (f :: * -> *) h a.
(Ord v, EqF f, Eq (Cxt h f a), Functor f, Foldable f) =>
Context f v -> Cxt h f a -> Maybe (CxtSubst h a f v)
matchCxt (Term f -> Context f v
forall (f :: * -> *) v.
(Traversable f, HasVars f v, Ord v) =>
Term f -> Context f v
varsToHoles Term f
t)