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)