{-# 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' :: 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
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
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)