    {-# Language Safe, RankNTypes, MultiParamTypeClasses #-}
    {-# Language FunctionalDependencies #-}
    {-# Language FlexibleInstances #-}
    {-# Language TypeFamilies, UndecidableInstances #-}
    module Cryptol.Utils.Patterns where

    import Control.Monad(liftM,liftM2,ap,MonadPlus(..),guard)
    import Control.Applicative(Alternative(..))

    newtype Match b = Match (forall r. r -> (b -> r) -> r)

    instance Functor Match where
      fmap = liftM

    instance Applicative Match where
      pure a = Match $ \_no yes -> yes a
      (<*>)  = ap

    instance Monad Match where
      fail _ = empty
      Match m >>= f = Match $ \no yes -> m no $ \a ->
                                         let Match n = f a in
                                         n no yes

    instance Alternative Match where
      empty = Match $ \no _ -> no
      Match m <|> Match n = Match $ \no yes -> m (n no yes) yes

    instance MonadPlus Match where

    type Pat a b = a -> Match b

    (|||) :: Pat a b -> Pat a b -> Pat a b
    p ||| q = \a -> p a <|> q a

    -- | Check that a value satisfies multiple patterns.
    -- For example, an "as" pattern is @(__ &&& p)@.
    (&&&) :: Pat a b -> Pat a c -> Pat a (b,c)
    p &&& q = \a -> liftM2 (,) (p a) (q a)

    -- | Match a value, and modify the result.
    (~>) :: Pat a b -> (b -> c) -> Pat a c
    p ~> f = \a -> f <$> p a

    -- | Match a value, and return the given result
    (~~>) :: Pat a b -> c -> Pat a c
    p ~~> f = \a -> f <$ p a

    -- | View pattern.
    (<~) :: (a -> b) -> Pat b c -> Pat a c
    f <~ p = \a -> p (f a)

    -- | Variable pattern.
    __ :: Pat a a
    __ = return

    -- | Constant pattern.
    succeed :: a -> Pat x a
    succeed = const . return

    -- | Predicate pattern
    checkThat :: (a -> Bool) -> Pat a ()
    checkThat p = \a -> guard (p a)

    -- | Check for exact value.
    lit :: Eq a => a -> Pat a ()
    lit x = checkThat (x ==)
    {-# Inline lit #-}

    -- | Match a pattern, using the given default if valure.
    matchDefault :: a -> Match a -> a
    matchDefault a (Match m) = m a id
    {-# Inline matchDefault #-}

    -- | Match an irrefutable pattern.  Crashes on faliure.
    match :: Match a -> a
    match m = matchDefault (error "Pattern match failure.") m
    {-# Inline match #-}

    matchMaybe :: Match a -> Maybe a
    matchMaybe (Match m) = m Nothing Just

    list :: [Pat a b] -> Pat [a] [b]
    list [] = \a ->
      case a of
        [] -> return []
        _  -> mzero
    list (p : ps) = \as ->
      case as of
        []     -> mzero
        x : xs ->
          do a  <- p x
             bs <- list ps xs
             return (a : bs)

    (><) :: Pat a b -> Pat x y -> Pat (a,x) (b,y)
    p >< q = \(a,x) -> do b <- p a
                          y <- q x
                          return (b,y)

    class Matches thing pats res | pats -> thing res where
      matches :: thing -> pats -> Match res

    instance ( f  ~ Pat a a1'
             , a1 ~ Pat a1' r1
             ) => Matches a (f,a1) r1 where
      matches ty (f,a1) = do a1' <- f ty
                             a1 a1'

    instance ( op ~ Pat a (a1',a2')
             , a1 ~ Pat a1' r1
             , a2 ~ Pat a2' r2
             ) => Matches a (op,a1,a2) (r1,r2)
      where
      matches ty (f,a1,a2) = do (a1',a2') <- f ty
                                r1 <- a1 a1'
                                r2 <- a2 a2'
                                return (r1,r2)

    instance ( op ~ Pat a (a1',a2',a3')
             , a1 ~ Pat a1' r1
             , a2 ~ Pat a2' r2
             , a3 ~ Pat a3' r3
             ) => Matches a (op,a1,a2,a3) (r1,r2,r3) where
      matches ty (f,a1,a2,a3) = do (a1',a2',a3') <- f ty
                                   r1 <- a1 a1'
                                   r2 <- a2 a2'
                                   r3 <- a3 a3'
                                   return (r1,r2,r3)