{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
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_)
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
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
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)