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

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.List   ( initMaybe )
import Agda.Utils.List1  ( List1, pattern (:|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Pretty ( prettyShow )
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 forall a b. (a -> b) -> a -> b
$ [Char] -> Name
simpleBinaryOperator [Char]
">>="
      qThen :: QName
qThen = Name -> QName
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
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> TCMT IO ()
ensureInScope forall a b. (a -> b) -> a -> b
$ [QName
qBind | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any DoStmt -> Bool
isBind List1 DoStmt
ss] forall a. [a] -> [a] -> [a]
++
                        [QName
qThen | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any DoStmt -> Bool
isThen forall a b. (a -> b) -> a -> b
$ 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        :| [] -> 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 ->
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Expr -> Expr -> Expr
appOp (forall a. SetRange a => Range -> a -> a
setRange Range
r QName
qBind) Expr
e forall a b. (a -> b) -> a -> b
$ Range -> Hiding -> Expr
AbsurdLam Range
r' Hiding
NotHidden

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

  -- `DoThen` and `DoLet` are easy.
  DoThen Expr
e   :| [DoStmt]
ss -> QName -> Expr -> Expr -> Expr
appOp QName
qThen Expr
e   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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just 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.
    ResolvedName
res <- QName -> ScopeM ResolvedName
resolveName (Name -> QName
QName Name
x)
    let isMatch :: Bool
isMatch = case ResolvedName
res of
          ConstructorName{}   -> Bool
True
          PatternSynResName{} -> Bool
True
          ResolvedName
_                   -> Bool
False
    Expr
rest <- [DoStmt] -> ScopeM Expr
desugarDo0 [DoStmt]
ss
    if Bool
isMatch then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Range -> Pattern -> Expr -> Expr -> [LamClause] -> Expr
matchingBind QName
qBind Range
r Pattern
p Expr
e Expr
rest []
               else forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Range -> Name -> Expr -> Expr -> Expr
nonMatchingBind QName
qBind Range
r Name
x Expr
e Expr
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
    Expr
rest <- [DoStmt] -> ScopeM Expr
desugarDo0 [DoStmt]
ss
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Range -> Pattern -> Expr -> Expr -> [LamClause] -> Expr
matchingBind QName
qBind Range
r Pattern
p Expr
e Expr
rest [LamClause]
cs

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

  failure :: TCMT IO a
failure = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError
    [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 (QName Name
x) -> forall a. a -> Maybe a
Just Name
x
  Pattern
_ -> 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 (forall a. SetRange a => Range -> a -> a
setRange Range
r QName
qBind) Expr
e             -- Set the range of the lambda to that of the
    forall a b. (a -> b) -> a -> b
$ Range -> Erased -> List1 LamClause -> Expr
ExtendedLam (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.
    forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LamClause -> LamClause
addParens (LamClause
mainClause forall a. a -> [a] -> NonEmpty a
:| [LamClause]
cs)
  where
    mainClause :: LamClause
mainClause = LamClause { lamLHS :: [Pattern]
lamLHS      = [Pattern
p]
                           , lamRHS :: RHS
lamRHS      = forall e. e -> RHS' e
RHS Expr
body
                           , lamCatchAll :: Bool
lamCatchAll = Bool
False }

    -- Add parens to left-hand sides.
    addParens :: LamClause -> LamClause
addParens LamClause
c = LamClause
c { lamLHS :: [Pattern]
lamLHS = [Pattern] -> [Pattern]
addP (LamClause -> [Pattern]
lamLHS LamClause
c) }
      where
      addP :: [Pattern] -> [Pattern]
addP []           = forall a. HasCallStack => a
__IMPOSSIBLE__
      addP pps :: [Pattern]
pps@(Pattern
p : [Pattern]
ps) = [Range -> Pattern -> Pattern
ParenP (forall a. HasRange a => a -> Range
getRange [Pattern]
pps) forall a b. (a -> b) -> a -> b
$ List1 Pattern -> Pattern
rawAppP forall a b. (a -> b) -> a -> b
$ Pattern
p 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 (forall a. SetRange a => Range -> a -> a
setRange Range
r QName
qBind) Expr
e forall a b. (a -> b) -> a -> b
$ Range -> List1 (LamBinding' TypedBinding) -> Expr -> Expr
Lam (forall a. HasRange a => a -> Range
getRange (Name
x, Expr
body)) (forall el coll. Singleton el coll => el -> coll
singleton LamBinding' TypedBinding
bx) Expr
body
  where bx :: LamBinding' TypedBinding
bx = forall a. NamedArg Binder -> LamBinding' a
DomainFree forall a b. (a -> b) -> a -> b
$ forall a. a -> NamedArg a
defaultNamedArg 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 = 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 (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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ Expr
e1 Expr
e2 -> Range -> Expr -> NamedArg Expr -> Expr
App (forall a. HasRange a => a -> Range
getRange (Expr
e1, Expr
e2)) Expr
e1 (forall a. a -> NamedArg a
defaultNamedArg Expr
e2)) Expr
e t Expr
es

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