{-|
    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 (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ RawName -> Name
simpleBinaryOperator RawName
">>="
      qThen :: QName
qThen = Name -> QName
QName (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ RawName -> Name
simpleBinaryOperator RawName
">>"
      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 (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 (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. TCMT IO 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.
    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 Expr -> ScopeM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ScopeM Expr) -> Expr -> ScopeM Expr
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 Expr -> ScopeM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ScopeM Expr) -> Expr -> ScopeM Expr
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
    Expr -> ScopeM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ScopeM Expr) -> Expr -> ScopeM Expr
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 = [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. TCMT IO 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 :: TCMT IO a
failure = RawName -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
RawName -> m a
genericError
    RawName
"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) -> 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 (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 :: [Pattern] -> RHS -> Bool -> LamClause
LamClause { lamLHS :: [Pattern]
lamLHS      = [Pattern
p]
                           , lamRHS :: RHS
lamRHS      = Expr -> RHS
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 []           = [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 -> Expr -> Expr
Lam ((Name, Expr) -> Range
forall a. HasRange a => a -> Range
getRange (Name
x, Expr
body)) (LamBinding -> List1 LamBinding
forall el coll. Singleton el coll => el -> coll
singleton LamBinding
bx) Expr
body
  where bx :: LamBinding
bx = NamedArg Binder -> LamBinding
forall a. NamedArg Binder -> LamBinding' a
DomainFree (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
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 (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
  ResolvedName
r <- QName -> ScopeM ResolvedName
resolveName QName
q
  case ResolvedName
r of
    ResolvedName
UnknownName -> RawName -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
RawName -> m a
genericError (RawName -> TCMT IO ()) -> RawName -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      QName -> RawName
forall a. Pretty a => a -> RawName
prettyShow QName
q RawName -> RawName -> RawName
forall a. [a] -> [a] -> [a]
++ RawName
" needs to be in scope to desugar 'do' block"
    ResolvedName
_ -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()