module LambdaCube.SystemF.Parser
  ( pTopTerm
  , pTopType
  ) where

import           Data.Foldable            (Foldable (foldl'))
import           Data.Function            ((&))
import           Data.Functor             (($>))
import           Data.Maybe               (isJust)
import           LambdaCube.Common.Parser
import           LambdaCube.SystemF.Ast
import           Text.Megaparsec
import qualified Data.Text as Text

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
pTLam Parser ExtLCTerm -> Parser ExtLCTerm -> Parser ExtLCTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ExtLCTerm
pLam Parser ExtLCTerm -> Parser ExtLCTerm -> Parser ExtLCTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ExtLCTerm
pApp

pTLam :: Parser ExtLCTerm
pTLam :: Parser ExtLCTerm
pTLam =
  Text -> ExtLCTerm -> ExtLCTerm
ExtLCTLam
  (Text -> ExtLCTerm -> ExtLCTerm)
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity (ExtLCTerm -> ExtLCTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ParsecT Void Text Identity Text
atsignBackslash ParsecT Void Text Identity Text
-> 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 Text
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Void Text Identity Char
colon ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Void Text Identity Char
asterisk)
  ParsecT Void Text Identity (ExtLCTerm -> ExtLCTerm)
-> Parser ExtLCTerm -> Parser ExtLCTerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ParsecT Void Text Identity Char
dot ParsecT Void Text Identity Char
-> Parser ExtLCTerm -> Parser ExtLCTerm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ExtLCTerm
pTerm)

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
<$> (ParsecT Void Text Identity Char
backslash ParsecT Void Text Identity 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
<*> (ParsecT Void Text Identity Char
colon ParsecT Void Text Identity 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
<*> (ParsecT Void Text Identity Char
dot ParsecT Void Text Identity 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 -> ExtLCTerm] -> ExtLCTerm
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ExtLCTerm -> (ExtLCTerm -> ExtLCTerm) -> ExtLCTerm
forall a b. a -> (a -> b) -> b
(&) (ExtLCTerm -> [ExtLCTerm -> ExtLCTerm] -> ExtLCTerm)
-> Parser ExtLCTerm
-> ParsecT
     Void Text Identity ([ExtLCTerm -> ExtLCTerm] -> ExtLCTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser ExtLCTerm
pATerm ParsecT Void Text Identity ([ExtLCTerm -> ExtLCTerm] -> ExtLCTerm)
-> ParsecT Void Text Identity [ExtLCTerm -> ExtLCTerm]
-> Parser ExtLCTerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Void Text Identity (ExtLCTerm -> ExtLCTerm)
-> ParsecT Void Text Identity [ExtLCTerm -> ExtLCTerm]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many ParsecT Void Text Identity (ExtLCTerm -> ExtLCTerm)
pAppArg

pAppArg :: Parser (ExtLCTerm -> ExtLCTerm)
pAppArg :: ParsecT Void Text Identity (ExtLCTerm -> ExtLCTerm)
pAppArg = do
  Bool
isType <- Maybe Char -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Char -> Bool)
-> ParsecT Void Text Identity (Maybe Char)
-> ParsecT Void Text Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity (Maybe Char)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional ParsecT Void Text Identity Char
atsign
  if Bool
isType
    then (ExtLCTerm -> ExtLCType -> ExtLCTerm)
-> ExtLCType -> ExtLCTerm -> ExtLCTerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip ExtLCTerm -> ExtLCType -> ExtLCTerm
ExtLCTApp (ExtLCType -> ExtLCTerm -> ExtLCTerm)
-> ParsecT Void Text Identity ExtLCType
-> ParsecT Void Text Identity (ExtLCTerm -> ExtLCTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity ExtLCType
pAType
    else (ExtLCTerm -> ExtLCTerm -> ExtLCTerm)
-> ExtLCTerm -> ExtLCTerm -> ExtLCTerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip 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

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
<$> (ParsecT Void Text Identity Char
dollarsign ParsecT Void Text Identity 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
pUniv 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

pUniv :: Parser ExtLCType
pUniv :: ParsecT Void Text Identity ExtLCType
pUniv =
  Text -> ExtLCType -> ExtLCType
ExtLCUniv
  (Text -> ExtLCType -> ExtLCType)
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity (ExtLCType -> ExtLCType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ParsecT Void Text Identity Char
exclamationMark ParsecT Void Text Identity 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 Text
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Void Text Identity Char
colon ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Void Text Identity Char
asterisk)
  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 Char
comma ParsecT Void Text Identity 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
pAType ParsecT Void Text Identity Text
rightArrow

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 = ParsecT Void Text Identity Char
sharp ParsecT Void Text Identity 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
<$> (ParsecT Void Text Identity Char
dollarsign ParsecT Void Text Identity 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)