{-# LANGUAGE TupleSections #-}
-- |
-- Module      : AutoProof.Internal.Utils.Parser.Types
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Defines a lightweight parser type.
module AutoProof.Internal.Utils.Parser.Types
  ( Parser (Parser, runParser),
    parse,
  )
where

import Control.Applicative (Alternative (empty, (<|>)))
import Control.Monad ((>=>))

-- The parser type and its instances

-- | The 'Parser' type is a simple state monad with state type 'String' and
-- inner monad 'Maybe'.
newtype Parser a = Parser {Parser a -> String -> Maybe (String, a)
runParser :: String -> Maybe (String, a)}

instance Functor Parser where
  fmap :: (a -> b) -> Parser a -> Parser b
fmap f :: a -> b
f (Parser p :: String -> Maybe (String, a)
p) = (String -> Maybe (String, b)) -> Parser b
forall a. (String -> Maybe (String, a)) -> Parser a
Parser ((String -> Maybe (String, b)) -> Parser b)
-> (String -> Maybe (String, b)) -> Parser b
forall a b. (a -> b) -> a -> b
$ (((String, a) -> (String, b))
-> Maybe (String, a) -> Maybe (String, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((String, a) -> (String, b))
 -> Maybe (String, a) -> Maybe (String, b))
-> ((a -> b) -> (String, a) -> (String, b))
-> (a -> b)
-> Maybe (String, a)
-> Maybe (String, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> (String, a) -> (String, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) a -> b
f (Maybe (String, a) -> Maybe (String, b))
-> (String -> Maybe (String, a)) -> String -> Maybe (String, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe (String, a)
p

instance Applicative Parser where
  pure :: a -> Parser a
pure x :: a
x = (String -> Maybe (String, a)) -> Parser a
forall a. (String -> Maybe (String, a)) -> Parser a
Parser ((String -> Maybe (String, a)) -> Parser a)
-> (String -> Maybe (String, a)) -> Parser a
forall a b. (a -> b) -> a -> b
$ (String, a) -> Maybe (String, a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((String, a) -> Maybe (String, a))
-> (String -> (String, a)) -> String -> Maybe (String, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,a
x)

  (Parser p :: String -> Maybe (String, a -> b)
p) <*> :: Parser (a -> b) -> Parser a -> Parser b
<*> (Parser p' :: String -> Maybe (String, a)
p') = (String -> Maybe (String, b)) -> Parser b
forall a. (String -> Maybe (String, a)) -> Parser a
Parser ((String -> Maybe (String, b)) -> Parser b)
-> (String -> Maybe (String, b)) -> Parser b
forall a b. (a -> b) -> a -> b
$ \s :: String
s -> do
    (s' :: String
s', f :: a -> b
f) <- String -> Maybe (String, a -> b)
p String
s
    (s'' :: String
s'', x :: a
x) <- String -> Maybe (String, a)
p' String
s'
    (String, b) -> Maybe (String, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
s'', a -> b
f a
x)

instance Monad Parser where
  (Parser p :: String -> Maybe (String, a)
p) >>= :: Parser a -> (a -> Parser b) -> Parser b
>>= f :: a -> Parser b
f = (String -> Maybe (String, b)) -> Parser b
forall a. (String -> Maybe (String, a)) -> Parser a
Parser ((String -> Maybe (String, b)) -> Parser b)
-> (String -> Maybe (String, b)) -> Parser b
forall a b. (a -> b) -> a -> b
$ String -> Maybe (String, a)
p (String -> Maybe (String, a))
-> ((String, a) -> Maybe (String, b))
-> String
-> Maybe (String, b)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \(s :: String
s, x :: a
x) -> Parser b -> String -> Maybe (String, b)
forall a. Parser a -> String -> Maybe (String, a)
runParser (a -> Parser b
f a
x) String
s

instance Alternative Parser where
  empty :: Parser a
empty = (String -> Maybe (String, a)) -> Parser a
forall a. (String -> Maybe (String, a)) -> Parser a
Parser ((String -> Maybe (String, a)) -> Parser a)
-> (String -> Maybe (String, a)) -> Parser a
forall a b. (a -> b) -> a -> b
$ Maybe (String, a) -> String -> Maybe (String, a)
forall a b. a -> b -> a
const Maybe (String, a)
forall (f :: * -> *) a. Alternative f => f a
empty

  <|> :: Parser a -> Parser a -> Parser a
(<|>) (Parser p :: String -> Maybe (String, a)
p) (Parser p' :: String -> Maybe (String, a)
p') = (String -> Maybe (String, a)) -> Parser a
forall a. (String -> Maybe (String, a)) -> Parser a
Parser ((String -> Maybe (String, a)) -> Parser a)
-> (String -> Maybe (String, a)) -> Parser a
forall a b. (a -> b) -> a -> b
$ \s :: String
s -> String -> Maybe (String, a)
p String
s Maybe (String, a) -> Maybe (String, a) -> Maybe (String, a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Maybe (String, a)
p' String
s

-- | Run a parser on a string, discarding any unparsed suffix
parse :: Parser a -> String -> Maybe a
parse :: Parser a -> String -> Maybe a
parse (Parser p :: String -> Maybe (String, a)
p) = ((String, a) -> a) -> Maybe (String, a) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String, a) -> a
forall a b. (a, b) -> b
snd (Maybe (String, a) -> Maybe a)
-> (String -> Maybe (String, a)) -> String -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe (String, a)
p