{-# 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 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 :: (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 :: 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
  <*> :: 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 >>= :: 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 :: String -> Match a
fail String
_ = Match a
forall (f :: * -> *) a. Alternative f => f a
empty

instance Alternative Match where
  empty :: 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 <|> :: 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 ||| :: 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 (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 &&& :: 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 ~> :: 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 ~~> :: Pat a b -> c -> Pat a c
~~> c
f = \a
a -> c
f c -> Match b -> Match c
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 <~ :: (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
__ :: Pat a a
__ = Pat a a
forall (m :: * -> *) a. Monad m => a -> m a
return

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

-- | Predicate pattern
checkThat :: (a -> Bool) -> Pat a ()
checkThat :: (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 :: 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 :: 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 :: 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 :: 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 :: [Pat a b] -> Pat [a] [b]
list [] = \[a]
a ->
  case [a]
a of
    [] -> [b] -> Match [b]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    [a]
_  -> Match [b]
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 (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] -> Pat [a] [b]
forall a b. [Pat a b] -> Pat [a] [b]
list [Pat a b]
ps [a]
xs
         [b] -> Match [b]
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 >< :: 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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return (r1
r1,r2
r2,r3
r3)