{-# LANGUAGE GADTs             #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications  #-}
{-# LANGUAGE TypeOperators     #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | Common functions for parsers of UPLC, PLC, and PIR.

module PlutusCore.ParserCommon where

import Data.Char (isAlphaNum)
import Data.Map qualified as M
import Data.Text qualified as T
import PlutusCore qualified as PLC
import PlutusCore.Parsable qualified as PLC
import PlutusPrelude
import Text.Megaparsec hiding (ParseError, State, parse)
import Text.Megaparsec.Char (char, letterChar, space1, string)
import Text.Megaparsec.Char.Lexer qualified as Lex

import Control.Monad.State (MonadState (get, put), StateT, evalStateT)

import Data.Proxy (Proxy (Proxy))


newtype ParserState = ParserState { ParserState -> Map Text Unique
identifiers :: M.Map T.Text PLC.Unique }
    deriving (Int -> ParserState -> ShowS
[ParserState] -> ShowS
ParserState -> String
(Int -> ParserState -> ShowS)
-> (ParserState -> String)
-> ([ParserState] -> ShowS)
-> Show ParserState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ParserState] -> ShowS
$cshowList :: [ParserState] -> ShowS
show :: ParserState -> String
$cshow :: ParserState -> String
showsPrec :: Int -> ParserState -> ShowS
$cshowsPrec :: Int -> ParserState -> ShowS
Show)

-- With the alex lexer @ann@ could be @AlexPosn@ or @SourcePos@.
-- We should un-generalize it when we know it can only be @SourcePos@.
type Parser ann =
    ParsecT (PLC.ParseError ann) T.Text (StateT ParserState PLC.Quote)

instance (Stream s, PLC.MonadQuote m) => PLC.MonadQuote (ParsecT e s m)
instance (Ord ann, Pretty ann) => ShowErrorComponent (PLC.ParseError ann) where
    showErrorComponent :: ParseError ann -> String
showErrorComponent ParseError ann
err = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ ParseError ann -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty ParseError ann
err

topSourcePos :: SourcePos
topSourcePos :: SourcePos
topSourcePos = String -> SourcePos
initialPos String
"top"

initial :: ParserState
initial :: ParserState
initial = Map Text Unique -> ParserState
ParserState Map Text Unique
forall k a. Map k a
M.empty

-- | Return the unique identifier of a name.
-- If it's not in the current parser state, map the name to a fresh id
-- and add it to the state. Used in the Name parser.
intern :: (MonadState ParserState m, PLC.MonadQuote m)
    => T.Text -> m PLC.Unique
intern :: Text -> m Unique
intern Text
n = do
    ParserState
st <- m ParserState
forall s (m :: * -> *). MonadState s m => m s
get
    case Text -> Map Text Unique -> Maybe Unique
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
n (ParserState -> Map Text Unique
identifiers ParserState
st) of
        Just Unique
u -> Unique -> m Unique
forall (m :: * -> *) a. Monad m => a -> m a
return Unique
u
        Maybe Unique
Nothing -> do
            Unique
fresh <- m Unique
forall (m :: * -> *). MonadQuote m => m Unique
PLC.freshUnique
            let identifiers' :: Map Text Unique
identifiers' = Text -> Unique -> Map Text Unique -> Map Text Unique
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Text
n Unique
fresh (Map Text Unique -> Map Text Unique)
-> Map Text Unique -> Map Text Unique
forall a b. (a -> b) -> a -> b
$ ParserState -> Map Text Unique
identifiers ParserState
st
            ParserState -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ParserState -> m ()) -> ParserState -> m ()
forall a b. (a -> b) -> a -> b
$ Map Text Unique -> ParserState
ParserState Map Text Unique
identifiers'
            Unique -> m Unique
forall (m :: * -> *) a. Monad m => a -> m a
return Unique
fresh

parse :: Parser SourcePos a -> String -> T.Text -> Either (ParseErrorBundle T.Text (PLC.ParseError SourcePos)) a
parse :: Parser SourcePos a
-> String
-> Text
-> Either (ParseErrorBundle Text (ParseError SourcePos)) a
parse Parser SourcePos a
p String
file Text
str = Quote (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
-> Either (ParseErrorBundle Text (ParseError SourcePos)) a
forall a. Quote a -> a
PLC.runQuote (Quote (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
 -> Either (ParseErrorBundle Text (ParseError SourcePos)) a)
-> Quote (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
-> Either (ParseErrorBundle Text (ParseError SourcePos)) a
forall a b. (a -> b) -> a -> b
$ Parser SourcePos a
-> String
-> Text
-> Quote (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
forall a.
Parser SourcePos a
-> String
-> Text
-> Quote (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
parseQuoted Parser SourcePos a
p String
file Text
str

parseQuoted :: Parser SourcePos a -> String -> T.Text -> PLC.Quote
                   (Either (ParseErrorBundle T.Text (PLC.ParseError SourcePos)) a)
parseQuoted :: Parser SourcePos a
-> String
-> Text
-> Quote (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
parseQuoted Parser SourcePos a
p String
file Text
str = (StateT
   ParserState
   Quote
   (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
 -> ParserState
 -> Quote (Either (ParseErrorBundle Text (ParseError SourcePos)) a))
-> ParserState
-> StateT
     ParserState
     Quote
     (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
-> Quote (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
  ParserState
  Quote
  (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
-> ParserState
-> Quote (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ParserState
initial (StateT
   ParserState
   Quote
   (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
 -> Quote (Either (ParseErrorBundle Text (ParseError SourcePos)) a))
-> StateT
     ParserState
     Quote
     (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
-> Quote (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
forall a b. (a -> b) -> a -> b
$ Parser SourcePos a
-> String
-> Text
-> StateT
     ParserState
     Quote
     (Either (ParseErrorBundle Text (ParseError SourcePos)) a)
forall (m :: * -> *) e s a.
Monad m =>
ParsecT e s m a
-> String -> s -> m (Either (ParseErrorBundle s e) a)
runParserT Parser SourcePos a
p String
file Text
str

whitespace :: Parser SourcePos ()
whitespace :: Parser SourcePos ()
whitespace = Parser SourcePos ()
-> Parser SourcePos ()
-> Parser SourcePos ()
-> Parser SourcePos ()
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> m () -> m () -> m ()
Lex.space Parser SourcePos ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space1 (Tokens Text -> Parser SourcePos ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Tokens s -> m ()
Lex.skipLineComment Tokens Text
"--") (Tokens Text -> Tokens Text -> Parser SourcePos ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Tokens s -> Tokens s -> m ()
Lex.skipBlockCommentNested Tokens Text
"{-" Tokens Text
"-}")

lexeme :: Parser SourcePos a -> Parser SourcePos a
lexeme :: Parser SourcePos a -> Parser SourcePos a
lexeme = Parser SourcePos () -> Parser SourcePos a -> Parser SourcePos a
forall e s (m :: * -> *) a. MonadParsec e s m => m () -> m a -> m a
Lex.lexeme Parser SourcePos ()
whitespace

symbol :: T.Text -> Parser SourcePos T.Text
symbol :: Text -> Parser SourcePos Text
symbol = Parser SourcePos ()
-> Tokens Text
-> ParsecT
     (ParseError SourcePos)
     Text
     (StateT ParserState Quote)
     (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> Tokens s -> m (Tokens s)
Lex.symbol Parser SourcePos ()
whitespace

lparen :: Parser SourcePos T.Text
lparen :: Parser SourcePos Text
lparen = Text -> Parser SourcePos Text
symbol Text
"("
rparen :: Parser SourcePos T.Text
rparen :: Parser SourcePos Text
rparen = Text -> Parser SourcePos Text
symbol Text
")"

lbracket :: Parser SourcePos T.Text
lbracket :: Parser SourcePos Text
lbracket = Text -> Parser SourcePos Text
symbol Text
"["
rbracket :: Parser SourcePos T.Text
rbracket :: Parser SourcePos Text
rbracket = Text -> Parser SourcePos Text
symbol Text
"]"

lbrace :: Parser SourcePos T.Text
lbrace :: Parser SourcePos Text
lbrace = Text -> Parser SourcePos Text
symbol Text
"{"
rbrace :: Parser SourcePos T.Text
rbrace :: Parser SourcePos Text
rbrace = Text -> Parser SourcePos Text
symbol Text
"}"

inParens :: Parser SourcePos a -> Parser SourcePos a
inParens :: Parser SourcePos a -> Parser SourcePos a
inParens = Parser SourcePos Text
-> Parser SourcePos Text
-> Parser SourcePos a
-> Parser SourcePos a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between Parser SourcePos Text
lparen Parser SourcePos Text
rparen

inBrackets :: Parser SourcePos a -> Parser SourcePos a
inBrackets :: Parser SourcePos a -> Parser SourcePos a
inBrackets = Parser SourcePos Text
-> Parser SourcePos Text
-> Parser SourcePos a
-> Parser SourcePos a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between Parser SourcePos Text
lbracket Parser SourcePos Text
rbracket

inBraces :: Parser SourcePos a-> Parser SourcePos a
inBraces :: Parser SourcePos a -> Parser SourcePos a
inBraces = Parser SourcePos Text
-> Parser SourcePos Text
-> Parser SourcePos a
-> Parser SourcePos a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between Parser SourcePos Text
lbrace Parser SourcePos Text
rbrace

isIdentifierChar :: Char -> Bool
isIdentifierChar :: Char -> Bool
isIdentifierChar Char
c = Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\''

-- | Create a parser that matches the input word and returns its source position.
-- This is for attaching source positions to parsed terms/programs.
-- getSourcePos is not cheap, don't call it on matching of every token.
wordPos ::
    -- | The word to match
    T.Text -> Parser SourcePos SourcePos
wordPos :: Text -> Parser SourcePos SourcePos
wordPos Text
w = Parser SourcePos SourcePos -> Parser SourcePos SourcePos
forall a. Parser SourcePos a -> Parser SourcePos a
lexeme (Parser SourcePos SourcePos -> Parser SourcePos SourcePos)
-> Parser SourcePos SourcePos -> Parser SourcePos SourcePos
forall a b. (a -> b) -> a -> b
$ Parser SourcePos SourcePos -> Parser SourcePos SourcePos
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser SourcePos SourcePos -> Parser SourcePos SourcePos)
-> Parser SourcePos SourcePos -> Parser SourcePos SourcePos
forall a b. (a -> b) -> a -> b
$ Parser SourcePos SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos Parser SourcePos SourcePos
-> Parser SourcePos Text -> Parser SourcePos SourcePos
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Text -> Parser SourcePos Text
symbol Text
w

builtinFunction :: (Bounded fun, Enum fun, Pretty fun) => Parser SourcePos fun
builtinFunction :: Parser SourcePos fun
builtinFunction = Parser SourcePos fun -> Parser SourcePos fun
forall a. Parser SourcePos a -> Parser SourcePos a
lexeme (Parser SourcePos fun -> Parser SourcePos fun)
-> Parser SourcePos fun -> Parser SourcePos fun
forall a b. (a -> b) -> a -> b
$ [Parser SourcePos fun] -> Parser SourcePos fun
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ([Parser SourcePos fun] -> Parser SourcePos fun)
-> [Parser SourcePos fun] -> Parser SourcePos fun
forall a b. (a -> b) -> a -> b
$ (fun -> Parser SourcePos fun) -> [fun] -> [Parser SourcePos fun]
forall a b. (a -> b) -> [a] -> [b]
map fun -> Parser SourcePos fun
forall (m :: * -> *) e s a.
(MonadParsec e s m, Pretty a, Render (Tokens s)) =>
a -> m a
parseBuiltin [fun
forall a. Bounded a => a
minBound .. fun
forall a. Bounded a => a
maxBound]
    where parseBuiltin :: a -> m a
parseBuiltin a
builtin = m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Tokens s -> m (Tokens s)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string (a -> Tokens s
forall str a. (Pretty a, Render str) => a -> str
display a
builtin) m (Tokens s) -> m a -> m a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
builtin

version :: Parser SourcePos (PLC.Version SourcePos)
version :: Parser SourcePos (Version SourcePos)
version = Parser SourcePos (Version SourcePos)
-> Parser SourcePos (Version SourcePos)
forall a. Parser SourcePos a -> Parser SourcePos a
lexeme (Parser SourcePos (Version SourcePos)
 -> Parser SourcePos (Version SourcePos))
-> Parser SourcePos (Version SourcePos)
-> Parser SourcePos (Version SourcePos)
forall a b. (a -> b) -> a -> b
$ do
    SourcePos
p <- Parser SourcePos SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
    Natural
x <- ParsecT
  (ParseError SourcePos) Text (StateT ParserState Quote) Natural
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
Lex.decimal
    ParsecT (ParseError SourcePos) Text (StateT ParserState Quote) Char
-> Parser SourcePos ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT
   (ParseError SourcePos) Text (StateT ParserState Quote) Char
 -> Parser SourcePos ())
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) Char
-> Parser SourcePos ()
forall a b. (a -> b) -> a -> b
$ Token Text
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'.'
    Natural
y <- ParsecT
  (ParseError SourcePos) Text (StateT ParserState Quote) Natural
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
Lex.decimal
    ParsecT (ParseError SourcePos) Text (StateT ParserState Quote) Char
-> Parser SourcePos ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT
   (ParseError SourcePos) Text (StateT ParserState Quote) Char
 -> Parser SourcePos ())
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) Char
-> Parser SourcePos ()
forall a b. (a -> b) -> a -> b
$ Token Text
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'.'
    SourcePos -> Natural -> Natural -> Natural -> Version SourcePos
forall ann. ann -> Natural -> Natural -> Natural -> Version ann
PLC.Version SourcePos
p Natural
x Natural
y (Natural -> Version SourcePos)
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) Natural
-> Parser SourcePos (Version SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT
  (ParseError SourcePos) Text (StateT ParserState Quote) Natural
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
Lex.decimal

name :: Parser SourcePos PLC.Name
name :: Parser SourcePos Name
name = Parser SourcePos Name -> Parser SourcePos Name
forall a. Parser SourcePos a -> Parser SourcePos a
lexeme (Parser SourcePos Name -> Parser SourcePos Name)
-> Parser SourcePos Name -> Parser SourcePos Name
forall a b. (a -> b) -> a -> b
$ Parser SourcePos Name -> Parser SourcePos Name
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser SourcePos Name -> Parser SourcePos Name)
-> Parser SourcePos Name -> Parser SourcePos Name
forall a b. (a -> b) -> a -> b
$ do
    ParsecT (ParseError SourcePos) Text (StateT ParserState Quote) Char
-> Parser SourcePos ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT
   (ParseError SourcePos) Text (StateT ParserState Quote) Char
 -> Parser SourcePos ())
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) Char
-> Parser SourcePos ()
forall a b. (a -> b) -> a -> b
$ ParsecT (ParseError SourcePos) Text (StateT ParserState Quote) Char
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) Char
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
lookAhead ParsecT (ParseError SourcePos) Text (StateT ParserState Quote) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
letterChar
    Text
str <- Maybe String
-> (Token Text -> Bool)
-> ParsecT
     (ParseError SourcePos)
     Text
     (StateT ParserState Quote)
     (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhileP (String -> Maybe String
forall a. a -> Maybe a
Just String
"identifier") Char -> Bool
Token Text -> Bool
isIdentifierChar
    Text -> Unique -> Name
PLC.Name Text
str (Unique -> Name)
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) Unique
-> Parser SourcePos Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) Unique
forall (m :: * -> *).
(MonadState ParserState m, MonadQuote m) =>
Text -> m Unique
intern Text
str

tyName :: Parser SourcePos PLC.TyName
tyName :: Parser SourcePos TyName
tyName = Name -> TyName
PLC.TyName (Name -> TyName)
-> Parser SourcePos Name -> Parser SourcePos TyName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser SourcePos Name
name

-- | Turn a parser that can succeed without consuming any input into one that fails in this case.
enforce :: Parser SourcePos a -> Parser SourcePos a
enforce :: Parser SourcePos a -> Parser SourcePos a
enforce Parser SourcePos a
p = do
    (Text
input, a
x) <- Parser SourcePos a
-> ParsecT
     (ParseError SourcePos)
     Text
     (StateT ParserState Quote)
     (Tokens Text, a)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> m (Tokens s, a)
match Parser SourcePos a
p
    Bool -> Parser SourcePos ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Parser SourcePos ())
-> (Bool -> Bool) -> Bool -> Parser SourcePos ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Parser SourcePos ()) -> Bool -> Parser SourcePos ()
forall a b. (a -> b) -> a -> b
$ Text -> Bool
T.null Text
input
    a -> Parser SourcePos a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x

-- | Consume a chunk of text and either stop on whitespace (and consume it) or on a \')\' (without
-- consuming it). We need this for collecting a @Text@ to pass it to 'PLC.parse' in order to
-- parse a built-in type or a constant. This is neither efficient (because of @manyTill anySingle@),
-- nor future-proof (what if some future built-in type has parens in its syntax?). A good way of
-- resolving this would be to turn 'PLC.parse' into a proper parser rather than just a function
-- from @Text@ - this will happen as SCP-2251 gets done.
-- Note that this also fails on @(con string \"yes (no)\")@ as well as @con unit ()@, so it really
-- should be fixed somehow.
-- (For @con unit ()@, @kwxm suggested replacing it with @unitval@ or @one@ or *)
closedChunk :: Parser SourcePos T.Text
closedChunk :: Parser SourcePos Text
closedChunk = String -> Text
T.pack (String -> Text)
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) String
-> Parser SourcePos Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT (ParseError SourcePos) Text (StateT ParserState Quote) Char
-> Parser SourcePos ()
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) String
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
manyTill ParsecT (ParseError SourcePos) Text (StateT ParserState Quote) Char
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
anySingle Parser SourcePos ()
end where
    end :: Parser SourcePos ()
end = Parser SourcePos () -> Parser SourcePos ()
forall a. Parser SourcePos a -> Parser SourcePos a
enforce Parser SourcePos ()
whitespace Parser SourcePos () -> Parser SourcePos () -> Parser SourcePos ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT (ParseError SourcePos) Text (StateT ParserState Quote) Char
-> Parser SourcePos ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT (ParseError SourcePos) Text (StateT ParserState Quote) Char
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) Char
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
lookAhead (ParsecT
   (ParseError SourcePos) Text (StateT ParserState Quote) Char
 -> ParsecT
      (ParseError SourcePos) Text (StateT ParserState Quote) Char)
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) Char
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) Char
forall a b. (a -> b) -> a -> b
$ Token Text
-> ParsecT
     (ParseError SourcePos) Text (StateT ParserState Quote) (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
')')

-- | Parse a type tag by feeding the output of 'closedChunk' to 'PLC.parse'.
builtinTypeTag
    :: forall uni.
    PLC.Parsable (PLC.SomeTypeIn (PLC.Kinded uni))
    => Parser SourcePos (PLC.SomeTypeIn (PLC.Kinded uni))
builtinTypeTag :: Parser SourcePos (SomeTypeIn (Kinded uni))
builtinTypeTag = do
    Text
uniText <- Parser SourcePos Text
closedChunk
    case Text -> Maybe (SomeTypeIn (Kinded uni))
forall a. Parsable a => Text -> Maybe a
PLC.parse Text
uniText of
        Maybe (SomeTypeIn (Kinded uni))
Nothing  -> do
            SourcePos
ann <- Text -> Parser SourcePos SourcePos
wordPos Text
uniText
            ParseError SourcePos -> Parser SourcePos (SomeTypeIn (Kinded uni))
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure (ParseError SourcePos
 -> Parser SourcePos (SomeTypeIn (Kinded uni)))
-> ParseError SourcePos
-> Parser SourcePos (SomeTypeIn (Kinded uni))
forall a b. (a -> b) -> a -> b
$ SourcePos -> Text -> ParseError SourcePos
forall ann. ann -> Text -> ParseError ann
PLC.UnknownBuiltinType SourcePos
ann Text
uniText
        Just SomeTypeIn (Kinded uni)
uni -> SomeTypeIn (Kinded uni)
-> Parser SourcePos (SomeTypeIn (Kinded uni))
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeTypeIn (Kinded uni)
uni

-- | Parse a constant by parsing a type tag first and using the type-specific parser of constants.
-- Uses 'PLC.parse' under the hood for both types and constants.
-- @kwxm: this'll have problems with some built-in constants like strings and characters.
-- The existing parser has special cases involving complicated regular expressions
-- to deal with those (see Lexer.x), but things got more complicated recently when
-- @effectfully added built-in lists and pairs that can have other constants
-- nested inside them...We're probably still going to need special parsers
-- for things like quoted strings that can contain escape sequences.
-- @thealmarty will hopefully deal with these in SCP-2251.
constant
    :: forall uni.
       ( PLC.Parsable (PLC.SomeTypeIn (PLC.Kinded uni))
       , PLC.Closed uni, uni `PLC.Everywhere` PLC.Parsable
       )
    => Parser SourcePos (PLC.Some (PLC.ValueOf uni))
constant :: Parser SourcePos (Some (ValueOf uni))
constant = do
    -- We use 'match' for remembering the textual representation of the parsed type tag,
    -- so that we can show it in the error message if the constant fails to parse.
    (Text
uniText, PLC.SomeTypeIn (PLC.Kinded uni)) <- ParsecT
  (ParseError SourcePos)
  Text
  (StateT ParserState Quote)
  (SomeTypeIn (Kinded uni))
-> ParsecT
     (ParseError SourcePos)
     Text
     (StateT ParserState Quote)
     (Tokens Text, SomeTypeIn (Kinded uni))
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> m (Tokens s, a)
match ParsecT
  (ParseError SourcePos)
  Text
  (StateT ParserState Quote)
  (SomeTypeIn (Kinded uni))
forall (uni :: * -> *).
Parsable (SomeTypeIn (Kinded uni)) =>
Parser SourcePos (SomeTypeIn (Kinded uni))
builtinTypeTag
    -- See Note [Decoding universes].
    case uni (Esc a) -> Maybe (k :~: *)
forall (uni :: * -> *) a (x :: a).
Typeable a =>
uni (Esc x) -> Maybe (a :~: *)
PLC.checkStar @uni uni (Esc a)
uni of
        Maybe (k :~: *)
Nothing -> do
            SourcePos
ann <- Text -> Parser SourcePos SourcePos
wordPos Text
uniText
            ParseError SourcePos -> Parser SourcePos (Some (ValueOf uni))
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure (ParseError SourcePos -> Parser SourcePos (Some (ValueOf uni)))
-> ParseError SourcePos -> Parser SourcePos (Some (ValueOf uni))
forall a b. (a -> b) -> a -> b
$ SourcePos -> Text -> ParseError SourcePos
forall ann. ann -> Text -> ParseError ann
PLC.BuiltinTypeNotAStar SourcePos
ann Text
uniText
        Just k :~: *
PLC.Refl -> do
            Text
conText <- Parser SourcePos Text
closedChunk
            case Proxy Parsable -> uni (Esc a) -> (Parsable a => Maybe a) -> Maybe a
forall (uni :: * -> *) (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
PLC.bring (Proxy Parsable
forall k (t :: k). Proxy t
Proxy @PLC.Parsable) uni (Esc a)
uni (Esc a)
uni ((Parsable a => Maybe a) -> Maybe a)
-> (Parsable a => Maybe a) -> Maybe a
forall a b. (a -> b) -> a -> b
$ Text -> Maybe a
forall a. Parsable a => Text -> Maybe a
PLC.parse Text
conText of
                Maybe a
Nothing  -> do
                    SourcePos
ann <- Text -> Parser SourcePos SourcePos
wordPos Text
uniText
                    ParseError SourcePos -> Parser SourcePos (Some (ValueOf uni))
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure (ParseError SourcePos -> Parser SourcePos (Some (ValueOf uni)))
-> ParseError SourcePos -> Parser SourcePos (Some (ValueOf uni))
forall a b. (a -> b) -> a -> b
$ SourcePos -> Text -> Text -> ParseError SourcePos
forall ann. ann -> Text -> Text -> ParseError ann
PLC.InvalidBuiltinConstant SourcePos
ann Text
uniText Text
conText
                Just a
con -> Some (ValueOf uni) -> Parser SourcePos (Some (ValueOf uni))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Some (ValueOf uni) -> Parser SourcePos (Some (ValueOf uni)))
-> (ValueOf uni a -> Some (ValueOf uni))
-> ValueOf uni a
-> Parser SourcePos (Some (ValueOf uni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValueOf uni a -> Some (ValueOf uni)
forall k (tag :: k -> *) (a :: k). tag a -> Some tag
PLC.Some (ValueOf uni a -> Parser SourcePos (Some (ValueOf uni)))
-> ValueOf uni a -> Parser SourcePos (Some (ValueOf uni))
forall a b. (a -> b) -> a -> b
$ uni (Esc a) -> a -> ValueOf uni a
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
PLC.ValueOf uni (Esc a)
uni (Esc a)
uni a
con