-- |
-- Module      : AutoProof.Internal.Utils.Parser.Combinator
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Defines parser combinators.
module AutoProof.Internal.Utils.Parser.Combinator
  ( between,
    sepBy,
    sepBy1,
    chainl1,
    chainr1,
    notFollowedBy,
    eof,
  )
where

import AutoProof.Internal.Utils.Parser.Char (anyChar)
import AutoProof.Internal.Utils.Parser.Types (Parser (Parser))
import Control.Applicative (Alternative (many, (<|>)))

-- | @('between' open close p)@ runs @open@, then @p@, then @close@, returning
-- the value parsed by @p@.
between :: Parser b -> Parser c -> Parser a -> Parser a
between :: Parser b -> Parser c -> Parser a -> Parser a
between l :: Parser b
l r :: Parser c
r p :: Parser a
p = Parser b
l Parser b -> Parser a -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
p Parser a -> Parser c -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser c
r

-- | @('sepBy' p sep)@ runs zero or more occurrences of @p@, separated by
-- @sep@, returning the list of values parsed by @p@.
sepBy :: Parser a -> Parser b -> Parser [a]
p :: Parser a
p sepBy :: Parser a -> Parser b -> Parser [a]
`sepBy` sep :: Parser b
sep = Parser a
p Parser a -> Parser b -> Parser [a]
forall a b. Parser a -> Parser b -> Parser [a]
`sepBy1` Parser b
sep Parser [a] -> Parser [a] -> Parser [a]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [a] -> Parser [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

-- | @('sepBy1' p sep)@ runs one or more occurrences of @p@, separated by
-- @sep@, returning the list of values parsed by @p@.
sepBy1 :: Parser a -> Parser b -> Parser [a]
p :: Parser a
p sepBy1 :: Parser a -> Parser b -> Parser [a]
`sepBy1` sep :: Parser b
sep = (:) (a -> [a] -> [a]) -> Parser a -> Parser ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser a
p Parser ([a] -> [a]) -> Parser [a] -> Parser [a]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser a -> Parser [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (Parser b
sep Parser b -> Parser a -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
p)

-- | @('chainl1' p op)@ runs one or more occurrences of @p@, separated by
-- @op@, returning the value obtained by a left-associative application of the
-- functions parsed by @op@ to the values parsed by @p@.
chainl1 :: Parser a -> Parser (a -> a -> a) -> Parser a
chainl1 :: Parser a -> Parser (a -> a -> a) -> Parser a
chainl1 p :: Parser a
p op :: Parser (a -> a -> a)
op = Parser a
p Parser a -> (a -> Parser a) -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Parser a
rest
  where
    rest :: a -> Parser a
rest x :: a
x = (do a -> a -> a
f <- Parser (a -> a -> a)
op; a
y <- Parser a
p; a -> Parser a
rest (a -> a -> a
f a
x a
y)) Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

-- | @('chainr1' p op)@ runs one or more occurrences of @p@, separated by
-- @op@, returning the value obtained by a right-associative application of the
-- functions parsed by @op@ to the values parsed by @p@.
chainr1 :: Parser a -> Parser (a -> a -> a) -> Parser a
chainr1 :: Parser a -> Parser (a -> a -> a) -> Parser a
chainr1 p :: Parser a
p op :: Parser (a -> a -> a)
op = Parser a
p Parser a -> (a -> Parser a) -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Parser a
rest
  where
    rest :: a -> Parser a
rest x :: a
x = (do a -> a -> a
f <- Parser (a -> a -> a)
op; a
y <- Parser a -> Parser (a -> a -> a) -> Parser a
forall a. Parser a -> Parser (a -> a -> a) -> Parser a
chainr1 Parser a
p Parser (a -> a -> a)
op; a -> Parser a
rest (a -> a -> a
f a
x a
y)) Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

-- | @('notFollowedBy' p)@ succeeds if and only if @p@ fails.
notFollowedBy :: Parser a -> Parser ()
notFollowedBy :: Parser a -> Parser ()
notFollowedBy (Parser p :: String -> Maybe (String, a)
p) = (String -> Maybe (String, ())) -> Parser ()
forall a. (String -> Maybe (String, a)) -> Parser a
Parser String -> Maybe (String, ())
q
  where
    q :: String -> Maybe (String, ())
q s :: String
s = case String -> Maybe (String, a)
p String
s of
      Nothing -> (String, ()) -> Maybe (String, ())
forall a. a -> Maybe a
Just (String
s, ())
      Just _ -> Maybe (String, ())
forall a. Maybe a
Nothing

-- | @('eof')@ (end-of-file) only succeeds at the end of input.
eof :: Parser ()
eof :: Parser ()
eof = Parser Char -> Parser ()
forall a. Parser a -> Parser ()
notFollowedBy Parser Char
anyChar