    {-|
        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 Control.Monad
    import Data.Maybe

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

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

    import Agda.Utils.Pretty ( prettyShow )
    import Agda.Utils.List   ( initMaybe )

    desugarDoNotation :: Range -> [DoStmt] -> ScopeM Expr
    desugarDoNotation r ss = do
      let qBind = QName $ Name noRange InScope [Hole, Id ">>=", Hole]
          qThen = QName $ Name noRange InScope [Hole, Id ">>", Hole]
          isBind DoBind{} = True
          isBind _        = False
          isThen DoThen{} = True
          isThen _        = 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
      mapM_ ensureInScope $ [qBind | any isBind ss] ++
                            [qThen | any isThen $ fromMaybe ss $ initMaybe ss] -- ignore the last 'DoThen'
      desugarDo qBind qThen ss

    desugarDo :: QName -> QName -> [DoStmt] -> ScopeM Expr

    -- The parser doesn't generate empty 'do' blocks at the moment, but if that
    -- changes throwing the error is the right thing to do.
    desugarDo qBind qThen [] = genericError "Empty 'do' block"

    -- The last statement must be a DoThen
    desugarDo qBind qThen [s]
      | DoThen e <- s = return e
      | otherwise     = genericError "The last statement in a 'do' block must be an expression"

    -- `DoThen` and `DoLet` are easy
    desugarDo qBind qThen (DoThen e   : ss) = appOp qThen e   <$> desugarDo qBind qThen ss
    desugarDo qBind qThen (DoLet r ds : ss) = Let r ds . Just <$> desugarDo qBind qThen ss

    -- `DoBind` requires more work since we want to generate plain lambdas when
    -- possible.
    desugarDo qBind qThen (DoBind r p e [] : ss)
      | Just x <- singleName 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 <- resolveName (QName x)
      let isMatch = case res of
            ConstructorName{}   -> True
            PatternSynResName{} -> True
            _                   -> False
      rest <- desugarDo qBind qThen ss
      if isMatch then return $ matchingBind qBind r p e rest []
                 else return $ nonMatchingBind qBind r x e rest
    desugarDo qBind qThen (DoBind r p e cs : ss) = do
      -- If there are where clauses we have to desugar to a pattern lambda.
      rest <- desugarDo qBind qThen ss
      return $ matchingBind qBind r p e rest cs

    singleName :: Pattern -> Maybe Name
    singleName (IdentP (QName x)) = Just x
    singleName (RawAppP _ [p])    = singleName p
    singleName _                  = Nothing

    matchingBind :: QName -> Range -> Pattern -> Expr -> Expr -> [LamClause] -> Expr
    matchingBind qBind r p e body cs =
      appOp (setRange r qBind) e          -- Set the range of the lambda to that of the
        $ ExtendedLam (getRange cs)       -- where-clauses to make highlighting of overlapping
        $ map addParens (mainClause : cs) -- patterns not highlight the rest of the do-block.
      where
        mainClause = LamClause { lamLHS      = LHS p [] []
                               , lamRHS      = RHS body
                               , lamWhere    = NoWhere
                               , lamCatchAll = False }

        -- Add parens to left-hand sides: there can only be one pattern in these clauses.
        addParens c = c { lamLHS = addP (lamLHS c) }
          where addP (LHS p rw we) = LHS (RawAppP noRange [ParenP noRange p]) rw we

    nonMatchingBind :: QName -> Range -> Name -> Expr -> Expr -> Expr
    nonMatchingBind qBind r x e body =
        appOp (setRange r qBind) e $ Lam (getRange (x, body)) [bx] body
      where bx = DomainFree $ defaultNamedArg $ mkBoundName_ x

    appOp :: QName -> Expr -> Expr -> Expr
    appOp q e1 e2 = app (Ident q) [par e1, par e2]
      where
        par e = Paren (getRange e) e  -- Add parens to get the right precedence context (#3152)
        app e es = foldl (\ e1 e2 -> App (getRange (e1, e2)) e1 (defaultNamedArg e2)) e es

    ensureInScope :: QName -> ScopeM ()
    ensureInScope q = do
      r <- resolveName q
      case r of
        UnknownName -> genericError $
          prettyShow q ++ " needs to be in scope to desugar 'do' block"
        _ -> return ()