    {-# OPTIONS_GHC -Wunused-imports #-}

    {-|
        Desugaring for do-notation. Uses whatever `_>>=_` and `_>>_` happen to be
        in scope.

        Example:

        ```
          foo = do
            x ← m₁
            m₂
            just y ← m₃
              where nothing → m₄
            let z = t
            m₅
        ```
        desugars to
        ```
          foo =
            m₁ >>= λ x →
            m₂ >>
            m₃ >>= λ where
              just y → let z = t in m₅
              nothing → m₄
        ```
     -}
    module Agda.Syntax.DoNotation (desugarDoNotation) where

    import Prelude hiding (null)

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import Agda.Syntax.Concrete

    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Scope.Monad
    import Agda.TypeChecking.Monad

    import Agda.Utils.List1  ( List1, pattern (:|) )
    import qualified Agda.Utils.List1 as List1
    import Agda.Syntax.Common.Pretty ( prettyShow )

    import Agda.Utils.Null
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    desugarDoNotation :: Range -> List1 DoStmt -> ScopeM Expr
    desugarDoNotation :: Range -> List1 DoStmt -> ScopeM Expr
    desugarDoNotation Range
    r List1 DoStmt
    ss = do
      let qBind :: QName
    qBind = Name -> QName
    QName (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Name
    simpleBinaryOperator [Char]
    ">>="
          qThen :: QName
    qThen = Name -> QName
    QName (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Name
    simpleBinaryOperator [Char]
    ">>"
          isBind :: DoStmt -> Bool
    isBind DoBind{} = Bool
    True
          isBind DoStmt
    _        = Bool
    False
          isThen :: DoStmt -> Bool
    isThen DoThen{} = Bool
    True
          isThen DoStmt
    _        = Bool
    False
      -- Only check the operation we actually need. One could imagine to fall back
      -- on _>>=_ if _>>_ is not in scope, but if we are desugaring to _>>_ at all
      -- I think we should throw an error rather than silently switching to _>>=_.
      -- / Ulf
      (QName -> TCMT IO ()) -> [QName] -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ QName -> TCMT IO ()
    ensureInScope ([QName] -> TCMT IO ()) -> [QName] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [QName
    qBind | (DoStmt -> Bool) -> List1 DoStmt -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any DoStmt -> Bool
    isBind List1 DoStmt
    ss] [QName] -> [QName] -> [QName]
    forall a. [a] -> [a] -> [a]
    ++
                            [QName
    qThen | (DoStmt -> Bool) -> [DoStmt] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any DoStmt -> Bool
    isThen ([DoStmt] -> Bool) -> [DoStmt] -> Bool
    forall a b. (a -> b) -> a -> b
    $ List1 DoStmt -> [DoStmt]
    forall a. NonEmpty a -> [a]
    List1.init List1 DoStmt
    ss] -- ignore the last 'DoThen'
      QName -> QName -> List1 DoStmt -> ScopeM Expr
    desugarDo QName
    qBind QName
    qThen List1 DoStmt
    ss

    desugarDo :: QName -> QName -> List1 DoStmt -> ScopeM Expr
    desugarDo :: QName -> QName -> List1 DoStmt -> ScopeM Expr
    desugarDo QName
    qBind QName
    qThen = \case

      -- The last statement must be a DoThen.
      DoThen Expr
    e        :| [] -> Expr -> ScopeM Expr
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr
    e

      -- Or an absurd bind.
      DoBind Range
    r Pattern
    p Expr
    e [] :| [] | Just (Range
    r', Hiding
    NotHidden) <- Pattern -> Maybe (Range, Hiding)
    isAbsurdP Pattern
    p ->
        Expr -> ScopeM Expr
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> ScopeM Expr) -> Expr -> ScopeM Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> Expr -> Expr -> Expr
    appOp (Range -> QName -> QName
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r QName
    qBind) Expr
    e (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Hiding -> Expr
    AbsurdLam Range
    r' Hiding
    NotHidden

      -- Otherwise, sorry.
      DoStmt
    _ :| [] -> ScopeM Expr
    forall {a}. ScopeM a
    failure

      -- `DoThen` and `DoLet` are easy.
      DoThen Expr
    e   :| [DoStmt]
    ss -> QName -> Expr -> Expr -> Expr
    appOp QName
    qThen Expr
    e   (Expr -> Expr) -> ScopeM Expr -> ScopeM Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [DoStmt] -> ScopeM Expr
    desugarDo0 [DoStmt]
    ss
      DoLet Range
    r List1 Declaration
    ds :| [DoStmt]
    ss -> Range -> List1 Declaration -> Maybe Expr -> Expr
    Let Range
    r List1 Declaration
    ds (Maybe Expr -> Expr) -> (Expr -> Maybe Expr) -> Expr -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> Maybe Expr
    forall a. a -> Maybe a
    Just (Expr -> Expr) -> ScopeM Expr -> ScopeM Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [DoStmt] -> ScopeM Expr
    desugarDo0 [DoStmt]
    ss

      -- `DoBind` requires more work since we want to generate plain lambdas when possible.
      DoBind Range
    r Pattern
    p Expr
    e [] :| [DoStmt]
    ss | Just Name
    x <- Pattern -> Maybe Name
    singleName Pattern
    p -> do
        -- In this case we have a single name in the bind pattern and no where clauses.
        -- It could still be a pattern bind though (for instance, `refl ← pure eq`), so
        -- to figure out which one to use we look up the name in the scope; if it's a
        -- constructor or pattern synonym we desugar to a pattern lambda.
        res <- QName -> ScopeM ResolvedName
    resolveName (Name -> QName
    QName Name
    x)
        let isMatch = case ResolvedName
    res of
              ConstructorName{}   -> Bool
    True
              PatternSynResName{} -> Bool
    True
              ResolvedName
    _                   -> Bool
    False
        rest <- desugarDo0 ss
        if isMatch then return $ matchingBind qBind r p e rest []
                   else return $ nonMatchingBind qBind r x e rest

      -- If there are @where@ clauses we have to desugar to a pattern lambda.
      DoBind Range
    r Pattern
    p Expr
    e [LamClause]
    cs :| [DoStmt]
    ss -> do
        rest <- [DoStmt] -> ScopeM Expr
    desugarDo0 [DoStmt]
    ss
        return $ matchingBind qBind r p e rest cs

      where
      desugarDo0 :: [DoStmt] -> ScopeM Expr
      desugarDo0 :: [DoStmt] -> ScopeM Expr
    desugarDo0 [DoStmt]
    ss = [DoStmt]
    -> ScopeM Expr -> (List1 DoStmt -> ScopeM Expr) -> ScopeM Expr
    forall a b. [a] -> b -> (List1 a -> b) -> b
    List1.ifNull [DoStmt]
    ss ScopeM Expr
    forall {a}. ScopeM a
    failure ((List1 DoStmt -> ScopeM Expr) -> ScopeM Expr)
    -> (List1 DoStmt -> ScopeM Expr) -> ScopeM Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> QName -> List1 DoStmt -> ScopeM Expr
    desugarDo QName
    qBind QName
    qThen

      failure :: ScopeM a
    failure = [Char] -> ScopeM a
    forall a. [Char] -> ScopeM a
    doNotationError
        [Char]
    "The last statement in a 'do' block must be an expression or an absurd match."

    singleName :: Pattern -> Maybe Name
    singleName :: Pattern -> Maybe Name
    singleName = \case
      IdentP Bool
    _ (QName Name
    x) -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
      Pattern
    _ -> Maybe Name
    forall a. Maybe a
    Nothing

    matchingBind :: QName -> Range -> Pattern -> Expr -> Expr -> [LamClause] -> Expr
    matchingBind :: QName -> Range -> Pattern -> Expr -> Expr -> [LamClause] -> Expr
    matchingBind QName
    qBind Range
    r Pattern
    p Expr
    e Expr
    body [LamClause]
    cs =
      QName -> Expr -> Expr -> Expr
    appOp (Range -> QName -> QName
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r QName
    qBind) Expr
    e             -- Set the range of the lambda to that of the
        (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Erased -> List1 LamClause -> Expr
    ExtendedLam ([LamClause] -> Range
    forall a. HasRange a => a -> Range
    getRange [LamClause]
    cs)          -- where-clauses to make highlighting of overlapping
            Erased
    defaultErased                    -- patterns not highlight the rest of the do-block.
        (List1 LamClause -> Expr) -> List1 LamClause -> Expr
    forall a b. (a -> b) -> a -> b
    $ (LamClause -> LamClause) -> List1 LamClause -> List1 LamClause
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap LamClause -> LamClause
    addParens (LamClause
    mainClause LamClause -> [LamClause] -> List1 LamClause
    forall a. a -> [a] -> NonEmpty a
    :| [LamClause]
    cs)
      where
        mainClause :: LamClause
    mainClause = LamClause { lamLHS :: [Pattern]
    lamLHS      = [Pattern
    p]
                               , lamRHS :: RHS
    lamRHS      = Expr -> RHS
    forall e. e -> RHS' e
    RHS Expr
    body
                               , lamCatchall :: Catchall
    lamCatchall = Catchall
    forall a. Null a => a
    empty }

        -- Add parens to left-hand sides.
        addParens :: LamClause -> LamClause
    addParens LamClause
    c = LamClause
    c { lamLHS = addP (lamLHS c) }
          where
          addP :: [Pattern] -> [Pattern]
    addP []           = [Pattern]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          addP pps :: [Pattern]
    pps@(Pattern
    p : [Pattern]
    ps) = [Range -> Pattern -> Pattern
    ParenP ([Pattern] -> Range
    forall a. HasRange a => a -> Range
    getRange [Pattern]
    pps) (Pattern -> Pattern) -> Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ List1 Pattern -> Pattern
    rawAppP (List1 Pattern -> Pattern) -> List1 Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Pattern
    p Pattern -> [Pattern] -> List1 Pattern
    forall a. a -> [a] -> NonEmpty a
    :| [Pattern]
    ps ]

    nonMatchingBind :: QName -> Range -> Name -> Expr -> Expr -> Expr
    nonMatchingBind :: QName -> Range -> Name -> Expr -> Expr -> Expr
    nonMatchingBind QName
    qBind Range
    r Name
    x Expr
    e Expr
    body =
        QName -> Expr -> Expr -> Expr
    appOp (Range -> QName -> QName
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r QName
    qBind) Expr
    e (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> List1 (LamBinding' TypedBinding) -> Expr -> Expr
    Lam ((Name, Expr) -> Range
    forall a. HasRange a => a -> Range
    getRange (Name
    x, Expr
    body)) (LamBinding' TypedBinding -> List1 (LamBinding' TypedBinding)
    forall el coll. Singleton el coll => el -> coll
    singleton LamBinding' TypedBinding
    bx) Expr
    body
      where bx :: LamBinding' TypedBinding
    bx = NamedArg Binder -> LamBinding' TypedBinding
    forall a. NamedArg Binder -> LamBinding' a
    DomainFree (NamedArg Binder -> LamBinding' TypedBinding)
    -> NamedArg Binder -> LamBinding' TypedBinding
    forall a b. (a -> b) -> a -> b
    $ Binder -> NamedArg Binder
    forall a. a -> NamedArg a
    defaultNamedArg (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
    forall a b. (a -> b) -> a -> b
    $ Name -> Binder
    mkBinder_ Name
    x

    appOp :: QName -> Expr -> Expr -> Expr
    appOp :: QName -> Expr -> Expr -> Expr
    appOp QName
    q Expr
    e1 Expr
    e2 = Expr -> [Expr] -> Expr
    forall {t :: * -> *}. Foldable t => Expr -> t Expr -> Expr
    app (QName -> Expr
    Ident QName
    q) [Expr -> Expr
    par Expr
    e1, Expr -> Expr
    par Expr
    e2]
      where
        par :: Expr -> Expr
    par Expr
    e = Range -> Expr -> Expr
    Paren (Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e) Expr
    e  -- Add parens to get the right precedence context (#3152)
        app :: Expr -> t Expr -> Expr
    app Expr
    e t Expr
    es = (Expr -> Expr -> Expr) -> Expr -> t Expr -> Expr
    forall b a. (b -> a -> b) -> b -> t a -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (\ Expr
    e1 Expr
    e2 -> Range -> Expr -> NamedArg Expr -> Expr
    App ((Expr, Expr) -> Range
    forall a. HasRange a => a -> Range
    getRange (Expr
    e1, Expr
    e2)) Expr
    e1 (Expr -> NamedArg Expr
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    e2)) Expr
    e t Expr
    es

    ensureInScope :: QName -> ScopeM ()
    ensureInScope :: QName -> TCMT IO ()
    ensureInScope QName
    q = do
      r <- QName -> ScopeM ResolvedName
    resolveName QName
    q
      case r of
        ResolvedName
    UnknownName -> [Char] -> TCMT IO ()
    forall a. [Char] -> ScopeM a
    doNotationError ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " needs to be in scope to desugar 'do' block"
        ResolvedName
    _ -> () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    doNotationError :: String -> ScopeM a
    doNotationError :: forall a. [Char] -> ScopeM a
    doNotationError = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a)
    -> ([Char] -> TypeError) -> [Char] -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> TypeError
    DoNotationError