{-# 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' :: 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' (Hole v
v) Cxt h f a
t = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$  forall k a. k -> a -> Map k a
Map.singleton v
v [Cxt h f a
t]
matchCxt' (Term f (Cxt Hole f v)
s) (Term f (Cxt h f a)
t) = do
  [(Cxt Hole f v, Cxt h f a)]
eqs <- forall (f :: * -> *) a b.
(EqF f, Functor f, Foldable f) =>
f a -> f b -> Maybe [(a, b)]
eqMod f (Cxt Hole f v)
s f (Cxt h f a)
t
  [Map v [Cxt h f a]]
substs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry 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') [(Cxt Hole f v, Cxt h f a)]
eqs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. [a] -> [a] -> [a]
(++) [Map v [Cxt h f a]]
substs
matchCxt' Term {} Hole {} = 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 :: 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 Context f v
c1 Cxt h f a
c2 = do
  Map v [Cxt h f a]
res <- 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 = forall k a. Map k a -> [a]
Map.elems Map v [Cxt h f a]
res
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {a}. Eq a => [a] -> Maybe ()
checkEq [[Cxt h f a]]
insts
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall a. [a] -> a
head Map v [Cxt h f a]
res
    where checkEq :: [a] -> Maybe ()
checkEq [] = forall a. Maybe a
Nothing
          checkEq (a
c : [a]
cs)
              | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== a
c) [a]
cs = forall a. a -> Maybe a
Just ()
              | Bool
otherwise = 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 :: forall v (f :: * -> *) h a.
(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
t = 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 (forall (f :: * -> *) v.
(Traversable f, HasVars f v, Ord v) =>
Term f -> Context f v
varsToHoles Term f
t)