module Dhall.LSP.Backend.Parsing
( getImportLink
, getImportHash
, getLetInner
, getLetAnnot
, getLetIdentifier
, getLamIdentifier
, getForallIdentifier
, binderExprFromText
, holeExpr
)
where
import Control.Applicative (optional, (<|>))
import Data.Functor (void)
import Data.Text (Text)
import Dhall.Core
( Binding (..)
, Expr (..)
, Import
, Var (..)
, makeFunctionBinding
)
import Dhall.Parser
import Dhall.Parser.Expression (importHash_, importType_, localOnly)
import Dhall.Parser.Token hiding (text)
import Text.Megaparsec
( SourcePos (..)
, anySingle
, eof
, lookAhead
, notFollowedBy
, skipManyTill
, takeRest
, try
)
import qualified Text.Megaparsec as Megaparsec
getLetInner :: Src -> Maybe Src
getLetInner :: Src -> Maybe Src
getLetInner (Src SourcePos
left SourcePos
_ Text
text) = Parsec Void Text Src -> Text -> Maybe Src
forall e s a. (Ord e, Stream s) => Parsec e s a -> s -> Maybe a
Megaparsec.parseMaybe (Parser Src -> Parsec Void Text Src
forall a. Parser a -> Parsec Void Text a
unParser Parser Src
parseLetInnerOffset) Text
text
where parseLetInnerOffset :: Parser Src
parseLetInnerOffset = do
SourcePos -> Parser ()
setSourcePos SourcePos
left
Parser ()
_let
Parser ()
nonemptyWhitespace
Text
_ <- Parser Text
label
Parser ()
whitespace
Maybe ()
_ <- Parser () -> Parser (Maybe ())
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do
()
_ <- Parser ()
_colon
Parser ()
nonemptyWhitespace
Expr Src Import
_ <- Parser (Expr Src Import)
expr
Parser ()
whitespace)
Parser ()
_equal
Parser ()
whitespace
Expr Src Import
_ <- Parser (Expr Src Import)
expr
Parser ()
whitespace
Maybe ()
_ <- Parser () -> Parser (Maybe ())
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional Parser ()
_in
Parser ()
whitespace
SourcePos
begin <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
Text
tokens <- Parser Text
forall e s (m :: * -> *). MonadParsec e s m => m (Tokens s)
Megaparsec.takeRest
SourcePos
end <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
Src -> Parser Src
forall (m :: * -> *) a. Monad m => a -> m a
return (SourcePos -> SourcePos -> Text -> Src
Src SourcePos
begin SourcePos
end Text
tokens)
getLetAnnot :: Src -> Maybe Src
getLetAnnot :: Src -> Maybe Src
getLetAnnot (Src SourcePos
left SourcePos
_ Text
text) = Parsec Void Text Src -> Text -> Maybe Src
forall e s a. (Ord e, Stream s) => Parsec e s a -> s -> Maybe a
Megaparsec.parseMaybe (Parser Src -> Parsec Void Text Src
forall a. Parser a -> Parsec Void Text a
unParser Parser Src
parseLetAnnot) Text
text
where parseLetAnnot :: Parser Src
parseLetAnnot = do
SourcePos -> Parser ()
setSourcePos SourcePos
left
Parser ()
_let
Parser ()
nonemptyWhitespace
Text
_ <- Parser Text
label
Parser ()
whitespace
SourcePos
begin <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
(Text
tokens, Maybe ()
_) <- Parser (Maybe ()) -> Parser (Tokens Text, Maybe ())
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> m (Tokens s, a)
Megaparsec.match (Parser (Maybe ()) -> Parser (Tokens Text, Maybe ()))
-> Parser (Maybe ()) -> Parser (Tokens Text, Maybe ())
forall a b. (a -> b) -> a -> b
$ Parser () -> Parser (Maybe ())
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do
()
_ <- Parser ()
_colon
Parser ()
nonemptyWhitespace
Expr Src Import
_ <- Parser (Expr Src Import)
expr
Parser ()
whitespace)
SourcePos
end <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
Text
_ <- Parser Text
forall e s (m :: * -> *). MonadParsec e s m => m (Tokens s)
Megaparsec.takeRest
Src -> Parser Src
forall (m :: * -> *) a. Monad m => a -> m a
return (SourcePos -> SourcePos -> Text -> Src
Src SourcePos
begin SourcePos
end Text
tokens)
getLetIdentifier :: Src -> Src
getLetIdentifier :: Src -> Src
getLetIdentifier src :: Src
src@(Src SourcePos
left SourcePos
_ Text
text) =
case Parsec Void Text Src -> Text -> Maybe Src
forall e s a. (Ord e, Stream s) => Parsec e s a -> s -> Maybe a
Megaparsec.parseMaybe (Parser Src -> Parsec Void Text Src
forall a. Parser a -> Parsec Void Text a
unParser Parser Src
parseLetIdentifier) Text
text of
Maybe Src
Nothing -> Src
src
Just Src
e -> Src
e
where parseLetIdentifier :: Parser Src
parseLetIdentifier = do
SourcePos -> Parser ()
setSourcePos SourcePos
left
Parser ()
_let
Parser ()
nonemptyWhitespace
SourcePos
begin <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
(Text
tokens, Text
_) <- Parser Text -> Parser (Tokens Text, Text)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> m (Tokens s, a)
Megaparsec.match Parser Text
label
SourcePos
end <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
Text
_ <- Parser Text
forall e s (m :: * -> *). MonadParsec e s m => m (Tokens s)
Megaparsec.takeRest
Src -> Parser Src
forall (m :: * -> *) a. Monad m => a -> m a
return (SourcePos -> SourcePos -> Text -> Src
Src SourcePos
begin SourcePos
end Text
tokens)
getLamIdentifier :: Src -> Maybe Src
getLamIdentifier :: Src -> Maybe Src
getLamIdentifier (Src SourcePos
left SourcePos
_ Text
text) =
Parsec Void Text Src -> Text -> Maybe Src
forall e s a. (Ord e, Stream s) => Parsec e s a -> s -> Maybe a
Megaparsec.parseMaybe (Parser Src -> Parsec Void Text Src
forall a. Parser a -> Parsec Void Text a
unParser Parser Src
parseLetIdentifier) Text
text
where parseLetIdentifier :: Parser Src
parseLetIdentifier = do
SourcePos -> Parser ()
setSourcePos SourcePos
left
CharacterSet
_ <- Parser CharacterSet
_lambda
Parser ()
whitespace
Parser ()
_openParens
Parser ()
whitespace
SourcePos
begin <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
(Text
tokens, Text
_) <- Parser Text -> Parser (Tokens Text, Text)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> m (Tokens s, a)
Megaparsec.match Parser Text
label
SourcePos
end <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
Text
_ <- Parser Text
forall e s (m :: * -> *). MonadParsec e s m => m (Tokens s)
Megaparsec.takeRest
Src -> Parser Src
forall (m :: * -> *) a. Monad m => a -> m a
return (SourcePos -> SourcePos -> Text -> Src
Src SourcePos
begin SourcePos
end Text
tokens)
getForallIdentifier :: Src -> Maybe Src
getForallIdentifier :: Src -> Maybe Src
getForallIdentifier (Src SourcePos
left SourcePos
_ Text
text) =
Parsec Void Text Src -> Text -> Maybe Src
forall e s a. (Ord e, Stream s) => Parsec e s a -> s -> Maybe a
Megaparsec.parseMaybe (Parser Src -> Parsec Void Text Src
forall a. Parser a -> Parsec Void Text a
unParser Parser Src
parseLetIdentifier) Text
text
where parseLetIdentifier :: Parser Src
parseLetIdentifier = do
SourcePos -> Parser ()
setSourcePos SourcePos
left
CharacterSet
_ <- Parser CharacterSet
_forall
Parser ()
whitespace
Parser ()
_openParens
Parser ()
whitespace
SourcePos
begin <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
(Text
tokens, Text
_) <- Parser Text -> Parser (Tokens Text, Text)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> m (Tokens s, a)
Megaparsec.match Parser Text
label
SourcePos
end <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
Text
_ <- Parser Text
forall e s (m :: * -> *). MonadParsec e s m => m (Tokens s)
Megaparsec.takeRest
Src -> Parser Src
forall (m :: * -> *) a. Monad m => a -> m a
return (SourcePos -> SourcePos -> Text -> Src
Src SourcePos
begin SourcePos
end Text
tokens)
getImportHash :: Src -> Maybe Src
getImportHash :: Src -> Maybe Src
getImportHash (Src SourcePos
left SourcePos
_ Text
text) =
Parsec Void Text Src -> Text -> Maybe Src
forall e s a. (Ord e, Stream s) => Parsec e s a -> s -> Maybe a
Megaparsec.parseMaybe (Parser Src -> Parsec Void Text Src
forall a. Parser a -> Parsec Void Text a
unParser Parser Src
parseImportHashPosition) Text
text
where parseImportHashPosition :: Parser Src
parseImportHashPosition = do
SourcePos -> Parser ()
setSourcePos SourcePos
left
ImportType
_ <- Parser ImportType
importType_
Parser ()
whitespace
SourcePos
begin <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
(Text
tokens, Maybe SHA256Digest
_) <- Parser (Maybe SHA256Digest)
-> Parser (Tokens Text, Maybe SHA256Digest)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> m (Tokens s, a)
Megaparsec.match (Parser (Maybe SHA256Digest)
-> Parser (Tokens Text, Maybe SHA256Digest))
-> Parser (Maybe SHA256Digest)
-> Parser (Tokens Text, Maybe SHA256Digest)
forall a b. (a -> b) -> a -> b
$ Parser SHA256Digest -> Parser (Maybe SHA256Digest)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional Parser SHA256Digest
importHash_
SourcePos
end <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
Text
_ <- Parser Text
forall e s (m :: * -> *). MonadParsec e s m => m (Tokens s)
Megaparsec.takeRest
Src -> Parser Src
forall (m :: * -> *) a. Monad m => a -> m a
return (SourcePos -> SourcePos -> Text -> Src
Src SourcePos
begin SourcePos
end Text
tokens)
setSourcePos :: SourcePos -> Parser ()
setSourcePos :: SourcePos -> Parser ()
setSourcePos SourcePos
src =
(State Text Void -> State Text Void) -> Parser ()
forall e s (m :: * -> *).
MonadParsec e s m =>
(State s e -> State s e) -> m ()
Megaparsec.updateParserState ((State Text Void -> State Text Void) -> Parser ())
-> (State Text Void -> State Text Void) -> Parser ()
forall a b. (a -> b) -> a -> b
$ \State Text Void
state ->
let posState :: PosState Text
posState = (State Text Void -> PosState Text
forall s e. State s e -> PosState s
Megaparsec.statePosState State Text Void
state) { pstateSourcePos :: SourcePos
Megaparsec.pstateSourcePos = SourcePos
src }
in State Text Void
state { statePosState :: PosState Text
Megaparsec.statePosState = PosState Text
posState }
getImportLink :: Src -> Src
getImportLink :: Src -> Src
getImportLink src :: Src
src@(Src SourcePos
left SourcePos
_ Text
text) =
case Parsec Void Text Src -> Text -> Maybe Src
forall e s a. (Ord e, Stream s) => Parsec e s a -> s -> Maybe a
Megaparsec.parseMaybe (Parser Src -> Parsec Void Text Src
forall a. Parser a -> Parsec Void Text a
unParser Parser Src
parseImportLink) Text
text of
Just Src
v -> Src
v
Maybe Src
Nothing -> Src
src
where
parseImportLink :: Parser Src
parseImportLink = do
SourcePos -> Parser ()
setSourcePos SourcePos
left
SourcePos
begin <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
(Text
tokens, ()
_) <-
Parser () -> Parser (Tokens Text, ())
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> m (Tokens s, a)
Megaparsec.match (Parser () -> Parser (Tokens Text, ()))
-> Parser () -> Parser (Tokens Text, ())
forall a b. (a -> b) -> a -> b
$ (Parser ImportType
localOnly Parser ImportType -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> Parser ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Parser URL
httpRaw Parser URL -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> Parser ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
SourcePos
end <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
Megaparsec.getSourcePos
Text
_ <- Parser Text
forall e s (m :: * -> *). MonadParsec e s m => m (Tokens s)
Megaparsec.takeRest
Src -> Parser Src
forall (m :: * -> *) a. Monad m => a -> m a
return (SourcePos -> SourcePos -> Text -> Src
Src SourcePos
begin SourcePos
end Text
tokens)
holeExpr :: Expr s a
holeExpr :: Expr s a
holeExpr = Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V Text
"" Int
0)
binderExprFromText :: Text -> Expr Src Import
binderExprFromText :: Text -> Expr Src Import
binderExprFromText Text
txt =
case Parsec Void Text (Expr Src Import)
-> Text -> Maybe (Expr Src Import)
forall e s a. (Ord e, Stream s) => Parsec e s a -> s -> Maybe a
Megaparsec.parseMaybe (Parser (Expr Src Import) -> Parsec Void Text (Expr Src Import)
forall a. Parser a -> Parsec Void Text a
unParser Parser (Expr Src Import)
parseBinderExpr) (Text
txt Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ") of
Maybe (Expr Src Import)
Nothing -> Expr Src Import
forall s a. Expr s a
holeExpr
Just Expr Src Import
s -> Expr Src Import
s
where
boundary :: Parser ()
boundary = Parser ()
_let Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser CharacterSet -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Parser CharacterSet
_forall Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser CharacterSet -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Parser CharacterSet
_lambda
closedBinder :: Parser ()
closedBinder = Parser ()
closedLet Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ()
closedLambda Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ()
closedPi
closedLet :: Parser ()
closedLet = do
Parser ()
_let
Parser ()
nonemptyWhitespace
Text
_ <- Parser Text
label
Parser ()
whitespace
Maybe (Expr Src Import)
_ <- Parser (Expr Src Import) -> Parser (Maybe (Expr Src Import))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do
Parser ()
_colon
Parser ()
nonemptyWhitespace
Parser (Expr Src Import)
expr)
Parser ()
_equal
Parser ()
whitespace
Expr Src Import
_ <- Parser (Expr Src Import)
expr
Parser ()
whitespace
(do
Parser ()
_in
Parser ()
nonemptyWhitespace
Expr Src Import
_ <- Parser (Expr Src Import)
expr
() -> Parser ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ()
closedLet
closedLambda :: Parser ()
closedLambda = do
CharacterSet
_ <- Parser CharacterSet
_lambda
Parser ()
whitespace
Parser ()
_openParens
Parser ()
whitespace
Text
_ <- Parser Text
label
Parser ()
whitespace
Parser ()
_colon
Parser ()
nonemptyWhitespace
Expr Src Import
_ <- Parser (Expr Src Import)
expr
Parser ()
whitespace
Parser ()
_closeParens
Parser ()
whitespace
CharacterSet
_ <- Parser CharacterSet
_arrow
Parser ()
whitespace
Expr Src Import
_ <- Parser (Expr Src Import)
expr
() -> Parser ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
closedPi :: Parser ()
closedPi = do
CharacterSet
_ <- Parser CharacterSet
_forall
Parser ()
whitespace
Parser ()
_openParens
Parser ()
whitespace
Text
_ <- Parser Text
label
Parser ()
whitespace
Parser ()
_colon
Parser ()
nonemptyWhitespace
Expr Src Import
_ <- Parser (Expr Src Import)
expr
Parser ()
whitespace
Parser ()
_closeParens
Parser ()
whitespace
CharacterSet
_ <- Parser CharacterSet
_arrow
Parser ()
whitespace
Expr Src Import
_ <- Parser (Expr Src Import)
expr
() -> Parser ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
parseBinderExpr :: Parser (Expr Src Import)
parseBinderExpr =
Parser (Expr Src Import) -> Parser (Expr Src Import)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (do
Parser Char -> Parser () -> Parser ()
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m end
skipManyTill Parser Char
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
anySingle (Parser () -> Parser ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
lookAhead Parser ()
boundary)
Parser (Expr Src Import) -> Parser (Expr Src Import)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (do
Parser ()
closedBinder
Parser () -> Parser ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy Parser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof
Parser (Expr Src Import)
parseBinderExpr)
Parser (Expr Src Import)
-> Parser (Expr Src Import) -> Parser (Expr Src Import)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Expr Src Import) -> Parser (Expr Src Import)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser (Expr Src Import)
letBinder Parser (Expr Src Import)
-> Parser (Expr Src Import) -> Parser (Expr Src Import)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Expr Src Import)
lambdaBinder Parser (Expr Src Import)
-> Parser (Expr Src Import) -> Parser (Expr Src Import)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Expr Src Import)
forallBinder)
Parser (Expr Src Import)
-> Parser (Expr Src Import) -> Parser (Expr Src Import)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do
Parser ()
boundary
Parser (Expr Src Import)
parseBinderExpr))
Parser (Expr Src Import)
-> Parser (Expr Src Import) -> Parser (Expr Src Import)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do
Text
_ <- Parser Text
forall e s (m :: * -> *). MonadParsec e s m => m (Tokens s)
takeRest
Expr Src Import -> Parser (Expr Src Import)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr Src Import
forall s a. Expr s a
holeExpr)
letBinder :: Parser (Expr Src Import)
letBinder = do
Parser ()
_let
Parser ()
nonemptyWhitespace
Text
name <- Parser Text
label
Parser ()
whitespace
Maybe (Maybe Src, Expr Src Import)
mType <- Parser (Maybe Src, Expr Src Import)
-> Parser (Maybe (Maybe Src, Expr Src Import))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do Parser ()
_colon; Parser ()
nonemptyWhitespace; Expr Src Import
_type <- Parser (Expr Src Import)
expr; Parser ()
whitespace; (Maybe Src, Expr Src Import) -> Parser (Maybe Src, Expr Src Import)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Src
forall a. Maybe a
Nothing, Expr Src Import
_type))
Expr Src Import
value <- Parser (Expr Src Import) -> Parser (Expr Src Import)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (do Parser ()
_equal; Parser ()
whitespace; Parser (Expr Src Import)
expr Parser (Expr Src Import) -> Parser () -> Parser (Expr Src Import)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
whitespace)
Parser (Expr Src Import)
-> Parser (Expr Src Import) -> Parser (Expr Src Import)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do Parser Char -> Parser () -> Parser ()
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m end
skipManyTill Parser Char
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
anySingle (Parser () -> Parser ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
lookAhead Parser ()
boundary Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ()
_in); Expr Src Import -> Parser (Expr Src Import)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr Src Import
forall s a. Expr s a
holeExpr)
Expr Src Import
inner <- Parser (Expr Src Import)
parseBinderExpr
Expr Src Import -> Parser (Expr Src Import)
forall (m :: * -> *) a. Monad m => a -> m a
return (Binding Src Import -> Expr Src Import -> Expr Src Import
forall s a. Binding s a -> Expr s a -> Expr s a
Let (Maybe Src
-> Text
-> Maybe Src
-> Maybe (Maybe Src, Expr Src Import)
-> Maybe Src
-> Expr Src Import
-> Binding Src Import
forall s a.
Maybe s
-> Text
-> Maybe s
-> Maybe (Maybe s, Expr s a)
-> Maybe s
-> Expr s a
-> Binding s a
Binding Maybe Src
forall a. Maybe a
Nothing Text
name Maybe Src
forall a. Maybe a
Nothing Maybe (Maybe Src, Expr Src Import)
mType Maybe Src
forall a. Maybe a
Nothing Expr Src Import
value) Expr Src Import
inner)
forallBinder :: Parser (Expr Src Import)
forallBinder = do
CharacterSet
cs <- Parser CharacterSet
_forall
Parser ()
whitespace
Parser ()
_openParens
Parser ()
whitespace
Text
name <- Parser Text
label
Parser ()
whitespace
Parser ()
_colon
Parser ()
nonemptyWhitespace
(CharacterSet
cs', Expr Src Import
typ) <-
Parser (CharacterSet, Expr Src Import)
-> Parser (CharacterSet, Expr Src Import)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (do Expr Src Import
e <- Parser (Expr Src Import)
expr; Parser ()
whitespace; Parser ()
_closeParens; Parser ()
whitespace; CharacterSet
cs' <- Parser CharacterSet
_arrow; (CharacterSet, Expr Src Import)
-> Parser (CharacterSet, Expr Src Import)
forall (m :: * -> *) a. Monad m => a -> m a
return (CharacterSet
cs', Expr Src Import
e))
Parser (CharacterSet, Expr Src Import)
-> Parser (CharacterSet, Expr Src Import)
-> Parser (CharacterSet, Expr Src Import)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do CharacterSet
cs' <- Parser Char -> Parser CharacterSet -> Parser CharacterSet
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m end
skipManyTill Parser Char
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
anySingle Parser CharacterSet
_arrow; (CharacterSet, Expr Src Import)
-> Parser (CharacterSet, Expr Src Import)
forall (m :: * -> *) a. Monad m => a -> m a
return (CharacterSet
cs', Expr Src Import
forall s a. Expr s a
holeExpr))
Parser ()
whitespace
Expr Src Import
inner <- Parser (Expr Src Import)
parseBinderExpr
Expr Src Import -> Parser (Expr Src Import)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe CharacterSet
-> Text -> Expr Src Import -> Expr Src Import -> Expr Src Import
forall s a.
Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
Pi (CharacterSet -> Maybe CharacterSet
forall a. a -> Maybe a
Just (CharacterSet
cs CharacterSet -> CharacterSet -> CharacterSet
forall a. Semigroup a => a -> a -> a
<> CharacterSet
cs')) Text
name Expr Src Import
typ Expr Src Import
inner)
lambdaBinder :: Parser (Expr Src Import)
lambdaBinder = do
CharacterSet
cs <- Parser CharacterSet
_lambda
Parser ()
whitespace
Parser ()
_openParens
Parser ()
whitespace
Text
name <- Parser Text
label
Parser ()
whitespace
Parser ()
_colon
Parser ()
nonemptyWhitespace
(CharacterSet
cs', Expr Src Import
typ) <-
Parser (CharacterSet, Expr Src Import)
-> Parser (CharacterSet, Expr Src Import)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (do Expr Src Import
e <- Parser (Expr Src Import)
expr; Parser ()
whitespace; Parser ()
_closeParens; Parser ()
whitespace; CharacterSet
cs' <- Parser CharacterSet
_arrow; (CharacterSet, Expr Src Import)
-> Parser (CharacterSet, Expr Src Import)
forall (m :: * -> *) a. Monad m => a -> m a
return (CharacterSet
cs', Expr Src Import
e))
Parser (CharacterSet, Expr Src Import)
-> Parser (CharacterSet, Expr Src Import)
-> Parser (CharacterSet, Expr Src Import)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do CharacterSet
cs' <- Parser Char -> Parser CharacterSet -> Parser CharacterSet
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m end
skipManyTill Parser Char
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
anySingle Parser CharacterSet
_arrow; (CharacterSet, Expr Src Import)
-> Parser (CharacterSet, Expr Src Import)
forall (m :: * -> *) a. Monad m => a -> m a
return (CharacterSet
cs', Expr Src Import
forall s a. Expr s a
holeExpr))
Parser ()
whitespace
Expr Src Import
inner <- Parser (Expr Src Import)
parseBinderExpr
Expr Src Import -> Parser (Expr Src Import)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe CharacterSet
-> FunctionBinding Src Import -> Expr Src Import -> Expr Src Import
forall s a.
Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
Lam (CharacterSet -> Maybe CharacterSet
forall a. a -> Maybe a
Just (CharacterSet
cs CharacterSet -> CharacterSet -> CharacterSet
forall a. Semigroup a => a -> a -> a
<> CharacterSet
cs')) (Text -> Expr Src Import -> FunctionBinding Src Import
forall s a. Text -> Expr s a -> FunctionBinding s a
makeFunctionBinding Text
name Expr Src Import
typ) Expr Src Import
inner)