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

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

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

    instance Functor Match where
      fmap :: forall a b. (a -> b) -> Match a -> Match b
    fmap = (a -> b) -> Match a -> Match b
    forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
    liftM

    instance Applicative Match where
      pure :: forall a. a -> Match a
    pure a
    a = (forall r. r -> (a -> r) -> r) -> Match a
    forall b. (forall r. r -> (b -> r) -> r) -> Match b
    Match ((forall r. r -> (a -> r) -> r) -> Match a)
    -> (forall r. r -> (a -> r) -> r) -> Match a
    forall a b. (a -> b) -> a -> b
    $ \r
    _no a -> r
    yes -> a -> r
    yes a
    a
      <*> :: forall a b. Match (a -> b) -> Match a -> Match b
    (<*>)  = Match (a -> b) -> Match a -> Match b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    instance Monad Match where
      Match forall r. r -> (a -> r) -> r
    m >>= :: forall a b. Match a -> (a -> Match b) -> Match b
    >>= a -> Match b
    f = (forall r. r -> (b -> r) -> r) -> Match b
    forall b. (forall r. r -> (b -> r) -> r) -> Match b
    Match ((forall r. r -> (b -> r) -> r) -> Match b)
    -> (forall r. r -> (b -> r) -> r) -> Match b
    forall a b. (a -> b) -> a -> b
    $ \r
    no b -> r
    yes -> r -> (a -> r) -> r
    forall r. r -> (a -> r) -> r
    m r
    no ((a -> r) -> r) -> (a -> r) -> r
    forall a b. (a -> b) -> a -> b
    $ \a
    a ->
                                         let Match forall r. r -> (b -> r) -> r
    n = a -> Match b
    f a
    a in
                                         r -> (b -> r) -> r
    forall r. r -> (b -> r) -> r
    n r
    no b -> r
    yes

    instance Fail.MonadFail Match where
      fail :: forall a. String -> Match a
    fail String
    _ = Match a
    forall a. Match a
    forall (f :: * -> *) a. Alternative f => f a
    empty

    instance Alternative Match where
      empty :: forall a. Match a
    empty = (forall r. r -> (a -> r) -> r) -> Match a
    forall b. (forall r. r -> (b -> r) -> r) -> Match b
    Match ((forall r. r -> (a -> r) -> r) -> Match a)
    -> (forall r. r -> (a -> r) -> r) -> Match a
    forall a b. (a -> b) -> a -> b
    $ \r
    no a -> r
    _ -> r
    no
      Match forall r. r -> (a -> r) -> r
    m <|> :: forall a. Match a -> Match a -> Match a
    <|> Match forall r. r -> (a -> r) -> r
    n = (forall r. r -> (a -> r) -> r) -> Match a
    forall b. (forall r. r -> (b -> r) -> r) -> Match b
    Match ((forall r. r -> (a -> r) -> r) -> Match a)
    -> (forall r. r -> (a -> r) -> r) -> Match a
    forall a b. (a -> b) -> a -> b
    $ \r
    no a -> r
    yes -> r -> (a -> r) -> r
    forall r. r -> (a -> r) -> r
    m (r -> (a -> r) -> r
    forall r. r -> (a -> r) -> r
    n r
    no a -> r
    yes) a -> r
    yes

    instance MonadPlus Match where

    type Pat a b = a -> Match b

    (|||) :: Pat a b -> Pat a b -> Pat a b
    Pat a b
    p ||| :: forall a b. Pat a b -> Pat a b -> Pat a b
    ||| Pat a b
    q = \a
    a -> Pat a b
    p a
    a Match b -> Match b -> Match b
    forall a. Match a -> Match a -> Match a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Pat a b
    q a
    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)
    Pat a b
    p &&& :: forall a b c. Pat a b -> Pat a c -> Pat a (b, c)
    &&& Pat a c
    q = \a
    a -> (b -> c -> (b, c)) -> Match b -> Match c -> Match (b, c)
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 (,) (Pat a b
    p a
    a) (Pat a c
    q a
    a)

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

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

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

    -- | Variable pattern.
    __ :: Pat a a
    __ :: forall a. a -> Match a
    __ = a -> Match a
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    -- | Constant pattern.
    succeed :: a -> Pat x a
    succeed :: forall a x. a -> Pat x a
    succeed = Match a -> x -> Match a
    forall a b. a -> b -> a
    const (Match a -> x -> Match a) -> (a -> Match a) -> a -> x -> Match a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Match a
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    -- | Predicate pattern
    checkThat :: (a -> Bool) -> Pat a ()
    checkThat :: forall a. (a -> Bool) -> Pat a ()
    checkThat a -> Bool
    p = \a
    a -> Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (a -> Bool
    p a
    a)

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

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

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

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

    list :: [Pat a b] -> Pat [a] [b]
    list :: forall a b. [Pat a b] -> Pat [a] [b]
    list [] = \[a]
    a ->
      case [a]
    a of
        [] -> [b] -> Match [b]
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        [a]
    _  -> Match [b]
    forall a. Match a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
    list (Pat a b
    p : [Pat a b]
    ps) = \[a]
    as ->
      case [a]
    as of
        []     -> Match [b]
    forall a. Match a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        a
    x : [a]
    xs ->
          do b
    a  <- Pat a b
    p a
    x
             [b]
    bs <- [Pat a b] -> [a] -> Match [b]
    forall a b. [Pat a b] -> Pat [a] [b]
    list [Pat a b]
    ps [a]
    xs
             [b] -> Match [b]
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (b
    a b -> [b] -> [b]
    forall a. a -> [a] -> [a]
    : [b]
    bs)

    (><) :: Pat a b -> Pat x y -> Pat (a,x) (b,y)
    Pat a b
    p >< :: forall a b x y. Pat a b -> Pat x y -> Pat (a, x) (b, y)
    >< Pat x y
    q = \(a
    a,x
    x) -> do b
    b <- Pat a b
    p a
    a
                          y
    y <- Pat x y
    q x
    x
                          (b, y) -> Match (b, y)
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (b
    b,y
    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 :: a -> (f, a1) -> Match r1
    matches a
    ty (f
    f,a1
    a1) = do a1'
    a1' <- f
    Pat a a1'
    f a
    ty
                             a1
    Pat a1' r1
    a1 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 :: a -> (op, a1, a2) -> Match (r1, r2)
    matches a
    ty (op
    f,a1
    a1,a2
    a2) = do (a1'
    a1',a2'
    a2') <- op
    Pat a (a1', a2')
    f a
    ty
                                r1
    r1 <- a1
    Pat a1' r1
    a1 a1'
    a1'
                                r2
    r2 <- a2
    Pat a2' r2
    a2 a2'
    a2'
                                (r1, r2) -> Match (r1, r2)
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (r1
    r1,r2
    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 :: a -> (op, a1, a2, a3) -> Match (r1, r2, r3)
    matches a
    ty (op
    f,a1
    a1,a2
    a2,a3
    a3) = do (a1'
    a1',a2'
    a2',a3'
    a3') <- op
    Pat a (a1', a2', a3')
    f a
    ty
                                   r1
    r1 <- a1
    Pat a1' r1
    a1 a1'
    a1'
                                   r2
    r2 <- a2
    Pat a2' r2
    a2 a2'
    a2'
                                   r3
    r3 <- a3
    Pat a3' r3
    a3 a3'
    a3'
                                   (r1, r2, r3) -> Match (r1, r2, r3)
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (r1
    r1,r2
    r2,r3
    r3)