content: {-# OPTIONS_GHC -Wunused-imports #-}
  {-# OPTIONS_GHC -Wunused-matches #-}
  
  {-|
      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 :: List1 DoStmt -> ScopeM Expr
  desugarDoNotation ss = do
    let qBind = QName $ simpleBinaryOperator ">>="
        qThen = QName $ simpleBinaryOperator ">>"
        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 $ List1.init ss] -- ignore the last 'DoThen'
    desugarDo qBind qThen ss
  
  desugarDo :: QName -> QName -> List1 DoStmt -> ScopeM Expr
  desugarDo qBind qThen = \case
  
    -- The last statement must be a DoThen.
    DoThen e        :| [] -> return e
  
    -- Or an absurd bind.
    DoBind r p e [] :| [] | Just (r', NotHidden) <- isAbsurdP p ->
      return $ appOp (setRange r qBind) e $ AbsurdLam r' NotHidden
  
    -- Otherwise, sorry.
    _ :| [] -> failure
  
    -- `DoThen` and `DoLet` are easy.
    DoThen e   :| ss -> appOp qThen e   <$> desugarDo0 ss
    DoLet r ds :| ss -> Let r ds . Just <$> desugarDo0 ss
  
    -- `DoBind` requires more work since we want to generate plain lambdas when possible.
    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 <- 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 r p e cs :| ss -> do
      rest <- desugarDo0 ss
      return $ matchingBind qBind r p e rest cs
  
    where
    desugarDo0 :: [DoStmt] -> ScopeM Expr
    desugarDo0 ss = List1.ifNull ss failure $ desugarDo qBind qThen
  
    failure = doNotationError
      "The last statement in a 'do' block must be an expression or an absurd match."
  
  singleName :: Pattern -> Maybe Name
  singleName = \case
    IdentP _ (QName x) -> Just x
    _ -> 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
          defaultErased                    -- patterns not highlight the rest of the do-block.
      $ fmap addParens (mainClause :| cs)
    where
      mainClause = LamClause { lamLHS      = [p]
                             , lamRHS      = RHS body
                             , lamCatchall = empty }
  
      -- Add parens to left-hand sides.
      addParens c = c { lamLHS = addP (lamLHS c) }
        where
        addP []           = __IMPOSSIBLE__
        addP pps@(p : ps) = [ParenP (getRange pps) $ rawAppP $ p :| ps ]
  
  nonMatchingBind :: QName -> Range -> Name -> Expr -> Expr -> Expr
  nonMatchingBind qBind r x e body =
      appOp (setRange r qBind) e $ Lam (getRange (x, body)) (singleton bx) body
    where bx = DomainFree $ defaultNamedArg $ mkBinder_ 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 -> doNotationError $
        prettyShow q ++ " needs to be in scope to desugar 'do' block"
      _ -> return ()
  
  doNotationError :: String -> ScopeM a
  doNotationError = typeError . DoNotationError
  