module LambdaCube.SystemFw_.Parser
  ( pTopTerm
  , pTopType
  , pTopKind
  ) where

import           Data.Foldable            (Foldable (foldl'))
import           Data.Functor             (($>))
import qualified Data.Text                as Text
import           LambdaCube.Common.Parser
import           LambdaCube.SystemFw_.Ast
import           Text.Megaparsec

pTopTerm :: Parser ExtLCTerm
pTopTerm :: Parser ExtLCTerm
pTopTerm = Parser ExtLCTerm -> Parser ExtLCTerm
forall a. Parser a -> Parser a
topParser Parser ExtLCTerm
pTerm

pTerm :: Parser ExtLCTerm
pTerm :: Parser ExtLCTerm
pTerm = Parser ExtLCTerm
pLam Parser ExtLCTerm -> Parser ExtLCTerm -> Parser ExtLCTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ExtLCTerm
pApp

pLam :: Parser ExtLCTerm
pLam :: Parser ExtLCTerm
pLam =
  Text -> ExtLCType -> ExtLCTerm -> ExtLCTerm
ExtLCLam
  (Text -> ExtLCType -> ExtLCTerm -> ExtLCTerm)
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity (ExtLCType -> ExtLCTerm -> ExtLCTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Char
backslash Parser Char
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity Text
identifier)
  ParsecT Void Text Identity (ExtLCType -> ExtLCTerm -> ExtLCTerm)
-> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity (ExtLCTerm -> ExtLCTerm)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser Char
colon Parser Char
-> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity ExtLCType
pType)
  ParsecT Void Text Identity (ExtLCTerm -> ExtLCTerm)
-> Parser ExtLCTerm -> Parser ExtLCTerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser Char
dot Parser Char -> Parser ExtLCTerm -> Parser ExtLCTerm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ExtLCTerm
pTerm)

pApp :: Parser ExtLCTerm
pApp :: Parser ExtLCTerm
pApp = (ExtLCTerm -> ExtLCTerm -> ExtLCTerm)
-> ExtLCTerm -> [ExtLCTerm] -> ExtLCTerm
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ExtLCTerm -> ExtLCTerm -> ExtLCTerm
ExtLCApp (ExtLCTerm -> [ExtLCTerm] -> ExtLCTerm)
-> Parser ExtLCTerm
-> ParsecT Void Text Identity ([ExtLCTerm] -> ExtLCTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser ExtLCTerm
pATerm ParsecT Void Text Identity ([ExtLCTerm] -> ExtLCTerm)
-> ParsecT Void Text Identity [ExtLCTerm] -> Parser ExtLCTerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser ExtLCTerm -> ParsecT Void Text Identity [ExtLCTerm]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser ExtLCTerm
pATerm

pATerm :: Parser ExtLCTerm
pATerm :: Parser ExtLCTerm
pATerm = Parser ExtLCTerm
pVar Parser ExtLCTerm -> Parser ExtLCTerm -> Parser ExtLCTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ExtLCTerm
pMVar Parser ExtLCTerm -> Parser ExtLCTerm -> Parser ExtLCTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ExtLCTerm -> Parser ExtLCTerm
forall a. Parser a -> Parser a
parenthesized Parser ExtLCTerm
pTerm

pVar :: Parser ExtLCTerm
pVar :: Parser ExtLCTerm
pVar = Text -> ExtLCTerm
ExtLCVar (Text -> ExtLCTerm)
-> ParsecT Void Text Identity Text -> Parser ExtLCTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Text
identifier

pMVar :: Parser ExtLCTerm
pMVar :: Parser ExtLCTerm
pMVar = String -> ExtLCTerm
ExtLCMVar (String -> ExtLCTerm)
-> ParsecT Void Text Identity String -> Parser ExtLCTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Char
dollarsign Parser Char
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> String)
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> String
Text.unpack ParsecT Void Text Identity Text
identifier)

pTopType :: Parser ExtLCType
pTopType :: ParsecT Void Text Identity ExtLCType
pTopType = ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
forall a. Parser a -> Parser a
topParser ParsecT Void Text Identity ExtLCType
pType

pType :: Parser ExtLCType
pType :: ParsecT Void Text Identity ExtLCType
pType = ParsecT Void Text Identity ExtLCType
pTTLam ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT Void Text Identity ExtLCType
pArr

pTTLam :: Parser ExtLCType
pTTLam :: ParsecT Void Text Identity ExtLCType
pTTLam =
  Text -> ExtLCKind -> ExtLCType -> ExtLCType
ExtLCTTLam
  (Text -> ExtLCKind -> ExtLCType -> ExtLCType)
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity (ExtLCKind -> ExtLCType -> ExtLCType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Char
backslash Parser Char
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity Text
identifier)
  ParsecT Void Text Identity (ExtLCKind -> ExtLCType -> ExtLCType)
-> ParsecT Void Text Identity ExtLCKind
-> ParsecT Void Text Identity (ExtLCType -> ExtLCType)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser Char
colon Parser Char
-> ParsecT Void Text Identity ExtLCKind
-> ParsecT Void Text Identity ExtLCKind
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity ExtLCKind
pKind)
  ParsecT Void Text Identity (ExtLCType -> ExtLCType)
-> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser Char
dot Parser Char
-> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity ExtLCType
pType)

pArr :: Parser ExtLCType
pArr :: ParsecT Void Text Identity ExtLCType
pArr = (ExtLCType -> ExtLCType -> ExtLCType) -> [ExtLCType] -> ExtLCType
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ExtLCType -> ExtLCType -> ExtLCType
ExtLCArr ([ExtLCType] -> ExtLCType)
-> ParsecT Void Text Identity [ExtLCType]
-> ParsecT Void Text Identity ExtLCType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity [ExtLCType]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy1 ParsecT Void Text Identity ExtLCType
pTTApp ParsecT Void Text Identity Text
rightArrow

pTTApp :: Parser ExtLCType
pTTApp :: ParsecT Void Text Identity ExtLCType
pTTApp = (ExtLCType -> ExtLCType -> ExtLCType)
-> ExtLCType -> [ExtLCType] -> ExtLCType
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ExtLCType -> ExtLCType -> ExtLCType
ExtLCTTApp (ExtLCType -> [ExtLCType] -> ExtLCType)
-> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ([ExtLCType] -> ExtLCType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity ExtLCType
pAType ParsecT Void Text Identity ([ExtLCType] -> ExtLCType)
-> ParsecT Void Text Identity [ExtLCType]
-> ParsecT Void Text Identity ExtLCType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity [ExtLCType]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many ParsecT Void Text Identity ExtLCType
pAType

pAType :: Parser ExtLCType
pAType :: ParsecT Void Text Identity ExtLCType
pAType = ParsecT Void Text Identity ExtLCType
pBase ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT Void Text Identity ExtLCType
pTVar ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT Void Text Identity ExtLCType
pMTVar ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity ExtLCType
forall a. Parser a -> Parser a
parenthesized ParsecT Void Text Identity ExtLCType
pType

pBase :: Parser ExtLCType
pBase :: ParsecT Void Text Identity ExtLCType
pBase = Parser Char
sharp Parser Char -> ExtLCType -> ParsecT Void Text Identity ExtLCType
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ExtLCType
ExtLCBase

pTVar :: Parser ExtLCType
pTVar :: ParsecT Void Text Identity ExtLCType
pTVar = Text -> ExtLCType
ExtLCTVar (Text -> ExtLCType)
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity ExtLCType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Text
identifier

pMTVar :: Parser ExtLCType
pMTVar :: ParsecT Void Text Identity ExtLCType
pMTVar = String -> ExtLCType
ExtLCMTVar (String -> ExtLCType)
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity ExtLCType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Char
dollarsign Parser Char
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> String)
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> String
Text.unpack ParsecT Void Text Identity Text
identifier)

pTopKind :: Parser ExtLCKind
pTopKind :: ParsecT Void Text Identity ExtLCKind
pTopKind = ParsecT Void Text Identity ExtLCKind
-> ParsecT Void Text Identity ExtLCKind
forall a. Parser a -> Parser a
topParser ParsecT Void Text Identity ExtLCKind
pKind

pKind :: Parser ExtLCKind
pKind :: ParsecT Void Text Identity ExtLCKind
pKind = (ExtLCKind -> ExtLCKind -> ExtLCKind) -> [ExtLCKind] -> ExtLCKind
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ExtLCKind -> ExtLCKind -> ExtLCKind
ExtLCKArr ([ExtLCKind] -> ExtLCKind)
-> ParsecT Void Text Identity [ExtLCKind]
-> ParsecT Void Text Identity ExtLCKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity ExtLCKind
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity [ExtLCKind]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy1 ParsecT Void Text Identity ExtLCKind
pAKind ParsecT Void Text Identity Text
rightArrow

pAKind :: Parser ExtLCKind
pAKind :: ParsecT Void Text Identity ExtLCKind
pAKind = ParsecT Void Text Identity ExtLCKind
pStar ParsecT Void Text Identity ExtLCKind
-> ParsecT Void Text Identity ExtLCKind
-> ParsecT Void Text Identity ExtLCKind
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT Void Text Identity ExtLCKind
pMKVar ParsecT Void Text Identity ExtLCKind
-> ParsecT Void Text Identity ExtLCKind
-> ParsecT Void Text Identity ExtLCKind
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT Void Text Identity ExtLCKind
-> ParsecT Void Text Identity ExtLCKind
forall a. Parser a -> Parser a
parenthesized ParsecT Void Text Identity ExtLCKind
pKind

pStar :: Parser ExtLCKind
pStar :: ParsecT Void Text Identity ExtLCKind
pStar = Parser Char
asterisk Parser Char -> ExtLCKind -> ParsecT Void Text Identity ExtLCKind
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ExtLCKind
ExtLCStar

pMKVar :: Parser ExtLCKind
pMKVar :: ParsecT Void Text Identity ExtLCKind
pMKVar = String -> ExtLCKind
ExtLCMKVar (String -> ExtLCKind)
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity ExtLCKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Char
dollarsign Parser Char
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> String)
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> String
Text.unpack ParsecT Void Text Identity Text
identifier)