-- |
--
-- Module:      Control.Egison.Matcher.Collection
-- Description: Matchers for collection data types
-- Stability:   experimental

module Control.Egison.Matcher.Collection
  ( CollectionPattern(..)
  , List(..)
  , Multiset(..)
  , Set(..)
  )
where

import           Data.List                      ( tails )
import           Control.Monad                  ( MonadPlus(..) )
import           Control.Monad.Search
import           Control.Egison.Match
import           Control.Egison.Matcher
import           Control.Egison.Matcher.Pair
import           Control.Egison.QQ

-- | Class for collection pattern constructors.
class CollectionPattern m t where
  -- | Matcher for the elements.
  type ElemM m
  -- | Type of the target elements.
  type ElemT t
  -- | Pattern that matches with empty collections.
  -- @[]@ is desugared into 'nil' by the quasi-quoter.
  nil :: Pattern () m t ()
  nilM :: m -> t -> ()
  default nilM :: m -> t -> ()
  {-# INLINE nilM #-}
  nilM m
_ t
_ = ()
  -- | Pattern that destructs collections into its head and tail.
  -- @:@ is desugared into 'cons' by the quasi-quoter.
  cons :: Pattern (PP (ElemT t), PP t) m t (ElemT t, t)
  consM :: m -> t -> (ElemM m, m)
  -- | Pattern that destructs collections into its initial prefix and remaining suffix.
  -- @++@ is desugared into 'join' by the quasi-quoter.
  join :: Pattern (PP t, PP t) m t (t, t)
  joinM :: m -> t -> (m, m)
  default joinM :: m -> t -> (m, m)
  {-# INLINE joinM #-}
  joinM m
m t
_ = (m
m, m
m)
  elm :: Pattern (PP (ElemT t)) m t (ElemT t)
  elmM :: m -> t -> ElemM m
  joinCons :: Pattern (PP t, PP (ElemT t), PP t) m t (t, ElemT t, t)
  joinConsM :: m -> t -> (m, ElemM m, m)
  app :: Pattern (PP t, PP t) m t (t -> t, t)
  appM :: m -> t -> (Something, m)
  default appM :: m -> t -> (Something, m)
  {-# INLINE appM #-}
  appM m
m t
_ = (Something
Something, m
m)
  appCons :: Pattern (PP (t -> t), PP (ElemT t), PP t) m t (t -> t, ElemT t, t)
  appConsM :: m -> t -> (Something, ElemM m, m)

-- | 'List' matcher is a matcher for collections that matches as if they're normal lists.
newtype List m = List m

instance Matcher m t => Matcher (List m) [t]

instance Matcher m t => CollectionPattern (List m) [t] where
  {-# SPECIALIZE instance Matcher m t => CollectionPattern (List m) [t] #-}
  type ElemM (List m) = m
  type ElemT [t] = t
  {-# INLINE nil #-}
  nil :: Pattern () (List m) [t] ()
nil ()
_ List m
_ [] = () -> [()]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  nil ()
_ List m
_ [t]
_  = [()]
forall a. [a]
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  {-# INLINE cons #-}
  cons :: Pattern (PP (ElemT [t]), PP [t]) (List m) [t] (ElemT [t], [t])
cons (PP (ElemT [t]), PP [t])
_ List m
_        []       = [(t, [t])]
[(ElemT [t], [t])]
forall a. [a]
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  cons (PP (ElemT [t]), PP [t])
_ (List m
_) (t
x : [t]
xs) = (t, [t]) -> [(t, [t])]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t
x, [t]
xs)
  {-# INLINE consM #-}
  consM :: List m -> [t] -> (ElemM (List m), List m)
consM (List m
m) [t]
_ = (m
ElemM (List m)
m, m -> List m
forall m. m -> List m
List m
m)
  {-# INLINABLE join #-}
  join :: Pattern (PP [t], PP [t]) (List m) [t] ([t], [t])
join (PP [t]
WC, PP [t]
_) List m
_ [t]
xs       = ([t] -> ([t], [t])) -> [[t]] -> [([t], [t])]
forall a b. (a -> b) -> [a] -> [b]
map (\[t]
ts -> ([t]
forall a. HasCallStack => a
undefined, [t]
ts)) ([t] -> [[t]]
forall a. [a] -> [[a]]
tails [t]
xs)
  join (PP [t], PP [t])
_       List m
_ []       = ([t], [t]) -> [([t], [t])]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], [])
  join (PP [t], PP [t])
ps      List m
m (t
x : [t]
xs) = ([t], [t]) -> [([t], [t])]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], t
x t -> [t] -> [t]
forall a. a -> [a] -> [a]
: [t]
xs) [([t], [t])] -> [([t], [t])] -> [([t], [t])]
forall a. [a] -> [a] -> [a]
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` do
    ([t]
ys, [t]
zs) <- Pattern (PP [t], PP [t]) (List m) [t] ([t], [t])
forall m t.
CollectionPattern m t =>
Pattern (PP t, PP t) m t (t, t)
join (PP [t], PP [t])
ps List m
m [t]
xs
    ([t], [t]) -> [([t], [t])]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t
x t -> [t] -> [t]
forall a. a -> [a] -> [a]
: [t]
ys, [t]
zs)
  {-# INLINE elm #-}
  elm :: Pattern (PP (ElemT [t])) (List m) [t] (ElemT [t])
elm PP (ElemT [t])
_ (List m
_) [t]
xs = [t]
[ElemT [t]]
xs
  {-# INLINE elmM #-}
  elmM :: List m -> [t] -> ElemM (List m)
elmM (List m
m) [t]
_ = m
ElemM (List m)
m
  {-# INLINE joinCons #-}
  joinCons :: Pattern
  (PP [t], PP (ElemT [t]), PP [t]) (List m) [t] ([t], ElemT [t], [t])
joinCons (PP [t]
WC, PP (ElemT [t])
_, PP [t]
WC) (List m
_) [t]
tgt = [ ([t]
forall a. HasCallStack => a
undefined, t
ElemT [t]
x, [t]
forall a. HasCallStack => a
undefined) | t
x <- [t]
tgt ]
  joinCons (PP [t]
WC, PP (ElemT [t])
_, PP [t]
_) (List m
_) [t]
tgt  = [ ([t]
forall a. HasCallStack => a
undefined, t
ElemT [t]
x, [t]
rs) | (t
x:[t]
rs) <- [t] -> [[t]]
forall a. [a] -> [[a]]
tails [t]
tgt ]
  joinCons (PP [t]
_, PP (ElemT [t])
_, PP [t]
_) (List m
_) [t]
tgt   = [t] -> [t] -> [([t], t, [t])]
forall {a}. [a] -> [a] -> [([a], a, [a])]
f [] [t]
tgt
   where
    f :: [a] -> [a] -> [([a], a, [a])]
f [a]
_ [] = []
    f [a]
rhs (a
x : [a]
ts) = ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
rhs, a
x, [a]
ts) ([a], a, [a]) -> [([a], a, [a])] -> [([a], a, [a])]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [([a], a, [a])]
f (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rhs) [a]
ts
  {-# INLINE joinConsM #-}
  joinConsM :: List m -> [t] -> (List m, ElemM (List m), List m)
joinConsM (List m
m) [t]
_ = (m -> List m
forall m. m -> List m
List m
m, m
ElemM (List m)
m, m -> List m
forall m. m -> List m
List m
m)
  {-# INLINABLE app #-}
  app :: Pattern (PP [t], PP [t]) (List m) [t] ([t] -> [t], [t])
app (PP [t]
WC, PP [t]
_) List m
_ [t]
xs       = ([t] -> ([t] -> [t], [t])) -> [[t]] -> [([t] -> [t], [t])]
forall a b. (a -> b) -> [a] -> [b]
map (\[t]
ts -> ([t] -> [t]
forall a. HasCallStack => a
undefined, [t]
ts)) ([t] -> [[t]]
forall a. [a] -> [[a]]
tails [t]
xs)
  app (PP [t], PP [t])
_       List m
_ []       = ([t] -> [t], [t]) -> [([t] -> [t], [t])]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([t] -> [t]
forall a. a -> a
id, [])
  app (PP [t], PP [t])
ps      List m
m (t
x : [t]
xs) = ([t] -> [t], [t]) -> [([t] -> [t], [t])]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([t] -> [t]
forall a. a -> a
id, t
x t -> [t] -> [t]
forall a. a -> [a] -> [a]
: [t]
xs) [([t] -> [t], [t])] -> [([t] -> [t], [t])] -> [([t] -> [t], [t])]
forall a. [a] -> [a] -> [a]
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` do
    ([t] -> [t]
ys, [t]
zs) <- Pattern (PP [t], PP [t]) (List m) [t] ([t] -> [t], [t])
forall m t.
CollectionPattern m t =>
Pattern (PP t, PP t) m t (t -> t, t)
app (PP [t], PP [t])
ps List m
m [t]
xs
    ([t] -> [t], [t]) -> [([t] -> [t], [t])]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (\[t]
ls -> t
x t -> [t] -> [t]
forall a. a -> [a] -> [a]
: [t] -> [t]
ys [t]
ls, [t]
zs)
  {-# INLINABLE appCons #-}
  appCons :: Pattern
  (PP ([t] -> [t]), PP (ElemT [t]), PP [t])
  (List m)
  [t]
  ([t] -> [t], ElemT [t], [t])
appCons (PP ([t] -> [t])
WC, PP (ElemT [t])
_, PP [t]
WC) (List m
_) [t]
tgt = [ ([t] -> [t]
forall a. HasCallStack => a
undefined, t
ElemT [t]
x, [t]
forall a. HasCallStack => a
undefined) | t
x <- [t]
tgt ]
  appCons (PP ([t] -> [t])
WC, PP (ElemT [t])
_, PP [t]
_) (List m
_) [t]
tgt  = [ ([t] -> [t]
forall a. HasCallStack => a
undefined, t
ElemT [t]
x, [t]
rs) | (t
x:[t]
rs) <- [t] -> [[t]]
forall a. [a] -> [[a]]
tails [t]
tgt ]
  appCons (PP ([t] -> [t])
_, PP (ElemT [t])
_, PP [t]
_) (List m
_) [t]
tgt   = ([t] -> [t]) -> [t] -> [([t] -> [t], t, [t])]
forall {a} {c}. ([a] -> c) -> [a] -> [([a] -> c, a, [a])]
f [t] -> [t]
forall a. a -> a
id [t]
tgt
   where
    f :: ([a] -> c) -> [a] -> [([a] -> c, a, [a])]
f [a] -> c
_ [] = []
    f [a] -> c
hs (a
x : [a]
ts) = ([a] -> c
hs, a
x, [a]
ts) ([a] -> c, a, [a]) -> [([a] -> c, a, [a])] -> [([a] -> c, a, [a])]
forall a. a -> [a] -> [a]
: ([a] -> c) -> [a] -> [([a] -> c, a, [a])]
f ([a] -> c
hs ([a] -> c) -> ([a] -> [a]) -> [a] -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:)) [a]
ts
  {-# INLINABLE appConsM #-}
  appConsM :: List m -> [t] -> (Something, ElemM (List m), List m)
appConsM (List m
m) [t]
_ = (Something
Something, m
ElemM (List m)
m, m -> List m
forall m. m -> List m
List m
m)

instance (Eq a, Matcher m a, ValuePattern m a) => ValuePattern (List m) [a] where
  value :: [a] -> Pattern () (List m) [a] ()
value [a]
e () (List m
m) [a]
v = if List m -> List m -> [a] -> [a] -> Bool
forall m1 t1 m2 t2.
(Matcher m1 t1, Matcher m2 t2, ValuePattern (ElemM m2) (ElemT t2),
 ElemT t1 ~ ElemT t2, CollectionPattern m1 t1,
 CollectionPattern m2 t2) =>
m1 -> m2 -> t1 -> t2 -> Bool
eqAs (m -> List m
forall m. m -> List m
List m
m) (m -> List m
forall m. m -> List m
List m
m) [a]
e [a]
v then () -> [()]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure () else [()]
forall a. [a]
forall (m :: * -> *) a. MonadPlus m => m a
mzero

newtype Multiset m = Multiset m

instance Matcher m t => Matcher (Multiset m) [t]

instance Matcher m t => CollectionPattern (Multiset m) [t] where
  {-# SPECIALIZE instance Matcher m t => CollectionPattern (Multiset m) [t] #-}
  type ElemM (Multiset m) = m
  type ElemT [t] = t
  {-# INLINE nil #-}
  nil :: Pattern () (Multiset m) [t] ()
nil ()
_ Multiset m
_ [] = () -> [()]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  nil ()
_ Multiset m
_ [t]
_  = [()]
forall a. [a]
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  {-# INLINE cons #-}
  cons :: Pattern (PP (ElemT [t]), PP [t]) (Multiset m) [t] (ElemT [t], [t])
cons (PP (ElemT [t])
_, PP [t]
WC) (Multiset m
_) [t]
xs = (t -> (t, [t])) -> [t] -> [(t, [t])]
forall a b. (a -> b) -> [a] -> [b]
map (\t
x -> (t
x, [t]
forall a. HasCallStack => a
undefined)) [t]
xs
  cons (PP (ElemT [t]), PP [t])
_       (Multiset m
_) [t]
xs = ((List Something, [t]) -> DFS (List Something, [t]))
-> [t]
-> List Something
-> [(List Something, [t]) -> DFS (t, [t])]
-> [(t, [t])]
forall m t (s :: * -> *) r.
(Matcher m t, MonadSearch s) =>
((m, t) -> s (m, t)) -> t -> m -> [(m, t) -> s r] -> [r]
matchAll
    (List Something, [t]) -> DFS (List Something, [t])
forall a. a -> DFS a
dfs
    [t]
xs
    (Something -> List Something
forall m. m -> List m
List Something
Something)
    [(List Something, [t]) -> DFS (t, [t])
[mc| $hs ++ $x : $ts -> (x, hs ++ ts) |]]
  {-# INLINE consM #-}
  consM :: Multiset m -> [t] -> (ElemM (Multiset m), Multiset m)
consM (Multiset m
m) [t]
_ = (m
ElemM (Multiset m)
m, m -> Multiset m
forall m. m -> Multiset m
Multiset m
m)
  {-# INLINABLE join #-}
  join :: Pattern (PP [t], PP [t]) (Multiset m) [t] ([t], [t])
join = Pattern (PP [t], PP [t]) (Multiset m) [t] ([t], [t])
forall a. HasCallStack => a
undefined
  elm :: Pattern (PP (ElemT [t])) (Multiset m) [t] (ElemT [t])
elm = Pattern (PP t) (Multiset m) [t] t
Pattern (PP (ElemT [t])) (Multiset m) [t] (ElemT [t])
forall a. HasCallStack => a
undefined
  elmM :: Multiset m -> [t] -> ElemM (Multiset m)
elmM = Multiset m -> [t] -> m
Multiset m -> [t] -> ElemM (Multiset m)
forall a. HasCallStack => a
undefined
  joinCons :: Pattern
  (PP [t], PP (ElemT [t]), PP [t])
  (Multiset m)
  [t]
  ([t], ElemT [t], [t])
joinCons = Pattern (PP [t], PP t, PP [t]) (Multiset m) [t] ([t], t, [t])
Pattern
  (PP [t], PP (ElemT [t]), PP [t])
  (Multiset m)
  [t]
  ([t], ElemT [t], [t])
forall a. HasCallStack => a
undefined
  joinConsM :: Multiset m -> [t] -> (Multiset m, ElemM (Multiset m), Multiset m)
joinConsM = Multiset m -> [t] -> (Multiset m, m, Multiset m)
Multiset m -> [t] -> (Multiset m, ElemM (Multiset m), Multiset m)
forall a. HasCallStack => a
undefined
  app :: Pattern (PP [t], PP [t]) (Multiset m) [t] ([t] -> [t], [t])
app = Pattern (PP [t], PP [t]) (Multiset m) [t] ([t] -> [t], [t])
forall a. HasCallStack => a
undefined
  appCons :: Pattern
  (PP ([t] -> [t]), PP (ElemT [t]), PP [t])
  (Multiset m)
  [t]
  ([t] -> [t], ElemT [t], [t])
appCons = Pattern
  (PP ([t] -> [t]), PP t, PP [t])
  (Multiset m)
  [t]
  ([t] -> [t], t, [t])
Pattern
  (PP ([t] -> [t]), PP (ElemT [t]), PP [t])
  (Multiset m)
  [t]
  ([t] -> [t], ElemT [t], [t])
forall a. HasCallStack => a
undefined
  appConsM :: Multiset m -> [t] -> (Something, ElemM (Multiset m), Multiset m)
appConsM = Multiset m -> [t] -> (Something, m, Multiset m)
Multiset m -> [t] -> (Something, ElemM (Multiset m), Multiset m)
forall a. HasCallStack => a
undefined

instance (Eq a, Matcher m a, ValuePattern m a) => ValuePattern (Multiset m) [a] where
  value :: [a] -> Pattern () (Multiset m) [a] ()
value [a]
e () (Multiset m
m) [a]
v =
    if List m -> Multiset m -> [a] -> [a] -> Bool
forall m1 t1 m2 t2.
(Matcher m1 t1, Matcher m2 t2, ValuePattern (ElemM m2) (ElemT t2),
 ElemT t1 ~ ElemT t2, CollectionPattern m1 t1,
 CollectionPattern m2 t2) =>
m1 -> m2 -> t1 -> t2 -> Bool
eqAs (m -> List m
forall m. m -> List m
List m
m) (m -> Multiset m
forall m. m -> Multiset m
Multiset m
m) [a]
e [a]
v then () -> [()]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure () else [()]
forall a. [a]
forall (m :: * -> *) a. MonadPlus m => m a
mzero

newtype Set m = Set m

instance Matcher m t => Matcher (Set m) [t]

instance Matcher m t => CollectionPattern (Set m) [t] where
  {-# SPECIALIZE instance Matcher m t => CollectionPattern (Set m) [t] #-}
  type ElemM (Set m) = m
  type ElemT [t] = t
  {-# INLINE nil #-}
  nil :: Pattern () (Set m) [t] ()
nil ()
_ Set m
_ [] = () -> [()]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  nil ()
_ Set m
_ [t]
_  = [()]
forall a. [a]
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  {-# INLINE cons #-}
  cons :: Pattern (PP (ElemT [t]), PP [t]) (Set m) [t] (ElemT [t], [t])
cons (PP (ElemT [t])
_, PP [t]
WC) (Set m
_) [t]
xs = (t -> (t, [t])) -> [t] -> [(t, [t])]
forall a b. (a -> b) -> [a] -> [b]
map (\t
x -> (t
x, [t]
forall a. HasCallStack => a
undefined)) [t]
xs
  cons (PP (ElemT [t]), PP [t])
_       (Set m
_) [t]
xs = (t -> (t, [t])) -> [t] -> [(t, [t])]
forall a b. (a -> b) -> [a] -> [b]
map (\t
x -> (t
x, [t]
xs)) [t]
xs
  {-# INLINE consM #-}
  consM :: Set m -> [t] -> (ElemM (Set m), Set m)
consM (Set m
m) [t]
_ = (m
ElemM (Set m)
m, m -> Set m
forall m. m -> Set m
Set m
m)
  {-# INLINABLE join #-}
  join :: Pattern (PP [t], PP [t]) (Set m) [t] ([t], [t])
join = Pattern (PP [t], PP [t]) (Set m) [t] ([t], [t])
forall a. HasCallStack => a
undefined
  elm :: Pattern (PP (ElemT [t])) (Set m) [t] (ElemT [t])
elm = Pattern (PP t) (Set m) [t] t
Pattern (PP (ElemT [t])) (Set m) [t] (ElemT [t])
forall a. HasCallStack => a
undefined
  elmM :: Set m -> [t] -> ElemM (Set m)
elmM = Set m -> [t] -> m
Set m -> [t] -> ElemM (Set m)
forall a. HasCallStack => a
undefined
  joinCons :: Pattern
  (PP [t], PP (ElemT [t]), PP [t]) (Set m) [t] ([t], ElemT [t], [t])
joinCons = Pattern (PP [t], PP t, PP [t]) (Set m) [t] ([t], t, [t])
Pattern
  (PP [t], PP (ElemT [t]), PP [t]) (Set m) [t] ([t], ElemT [t], [t])
forall a. HasCallStack => a
undefined
  joinConsM :: Set m -> [t] -> (Set m, ElemM (Set m), Set m)
joinConsM = Set m -> [t] -> (Set m, m, Set m)
Set m -> [t] -> (Set m, ElemM (Set m), Set m)
forall a. HasCallStack => a
undefined
  app :: Pattern (PP [t], PP [t]) (Set m) [t] ([t] -> [t], [t])
app = Pattern (PP [t], PP [t]) (Set m) [t] ([t] -> [t], [t])
forall a. HasCallStack => a
undefined
  appCons :: Pattern
  (PP ([t] -> [t]), PP (ElemT [t]), PP [t])
  (Set m)
  [t]
  ([t] -> [t], ElemT [t], [t])
appCons = Pattern
  (PP ([t] -> [t]), PP t, PP [t]) (Set m) [t] ([t] -> [t], t, [t])
Pattern
  (PP ([t] -> [t]), PP (ElemT [t]), PP [t])
  (Set m)
  [t]
  ([t] -> [t], ElemT [t], [t])
forall a. HasCallStack => a
undefined
  appConsM :: Set m -> [t] -> (Something, ElemM (Set m), Set m)
appConsM = Set m -> [t] -> (Something, m, Set m)
Set m -> [t] -> (Something, ElemM (Set m), Set m)
forall a. HasCallStack => a
undefined

instance (Eq a, Matcher m a, ValuePattern m a) => ValuePattern (Set m) [a] where
  value :: [a] -> Pattern () (Set m) [a] ()
value [a]
e () (Set m
m) [a]
v = if List m -> Set m -> [a] -> [a] -> Bool
forall m1 t1 m2 t2.
(Matcher m1 t1, Matcher m2 t2, ValuePattern (ElemM m2) (ElemT t2),
 ElemT t1 ~ ElemT t2, CollectionPattern m1 t1,
 CollectionPattern m2 t2) =>
m1 -> m2 -> t1 -> t2 -> Bool
eqAs (m -> List m
forall m. m -> List m
List m
m) (m -> Set m
forall m. m -> Set m
Set m
m) [a]
e [a]
v then () -> [()]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure () else [()]
forall a. [a]
forall (m :: * -> *) a. MonadPlus m => m a
mzero

eqAs :: (Matcher m1 t1, Matcher m2 t2,
         ValuePattern (ElemM m2) (ElemT t2), ElemT t1 ~ ElemT t2,
         CollectionPattern m1 t1, CollectionPattern m2 t2) =>
        m1 -> m2 -> t1 -> t2 -> Bool
eqAs :: forall m1 t1 m2 t2.
(Matcher m1 t1, Matcher m2 t2, ValuePattern (ElemM m2) (ElemT t2),
 ElemT t1 ~ ElemT t2, CollectionPattern m1 t1,
 CollectionPattern m2 t2) =>
m1 -> m2 -> t1 -> t2 -> Bool
eqAs m1
m1 m2
m2 t1
xs t2
ys = (((m1, m2), (t1, t2)) -> DFS ((m1, m2), (t1, t2)))
-> (t1, t2)
-> (m1, m2)
-> [((m1, m2), (t1, t2)) -> DFS Bool]
-> Bool
forall m t (s :: * -> *) r.
(Matcher m t, MonadSearch s) =>
((m, t) -> s (m, t)) -> t -> m -> [(m, t) -> s r] -> r
match
  ((m1, m2), (t1, t2)) -> DFS ((m1, m2), (t1, t2))
forall a. a -> DFS a
dfs
  (t1
xs, t2
ys)
  (m1
m1, m2
m2)
  [ ((m1, m2), (t1, t2)) -> DFS Bool
[mc| ([], []) -> True |]
  , ((m1, m2), (t1, t2)) -> DFS Bool
[mc| ($x : $xs, #x : $ys) -> eqAs m1 m2 xs ys |]
  , ((m1, m2), (t1, t2)) -> DFS Bool
[mc| _ -> False |]
  ]