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

-- | Parse the outermost binding in a Src descriptor of a let-block and return
--   the rest. Ex. on input `let a = 0 let b = a in b` parses `let a = 0 ` and
--   returns the Src descriptor containing `let b = a in b`.
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)

-- | Given an Src of a let expression return the Src containing the type
--   annotation. If the let expression does not have a type annotation return
--   a 0-length Src where we can insert one.
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)

-- | Given an Src of a let expression return the Src containing the bound
--   identifier, i.e. given `let x = ... in ...` return the Src descriptor
--   containing `x`. Returns the original Src if something goes wrong.
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)

-- | Cf. `getLetIdentifier`.
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)

-- | Cf. `getLetIdentifier`.
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)

-- | Given an Src of a import expression return the Src containing the hash
--   annotation. If the import does not have a hash annotation return a 0-length
--   Src where we can insert one.
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)

-- | An expression that is guaranteed not to typecheck. Can be used a
-- placeholder type to emulate 'lazy' contexts, when typechecking something in a
-- only partly well-typed context.
holeExpr :: Expr s a
-- The illegal variable name ensures that it can't be bound by the user!
holeExpr :: Expr s a
holeExpr = Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V Text
"" Int
0)

-- | Approximate the type-checking context at the end of the input. Tries to
-- parse as many binders as possible. Very messy!
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
    -- marks the beginning of the next binder
    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

    -- A binder that is out of scope at the end of the input. Discarded in the
    -- resulting 'binder expression'.
    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 ()

    -- Try to parse as many binders as possible. Skip malformed input and
    -- 'closed' binders that are already out of scope at the end of the input.
    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))

      -- if the bound value does not parse, skip and replace with 'hole'
      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
      -- if the bound type does not parse, skip and replace with 'hole'
      (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
      -- if the bound type does not parse, skip and replace with 'hole'
      (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)