{-|
    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.Pretty ( prettyShow )
import Agda.Utils.List   ( initMaybe )

desugarDoNotation :: Range -> [DoStmt] -> ScopeM Expr
desugarDoNotation :: Range -> [DoStmt] -> ScopeM Expr
desugarDoNotation Range
r [DoStmt]
ss = do
  let qBind :: QName
qBind = Name -> QName
QName (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ Range -> NameInScope -> [NamePart] -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope [NamePart
Hole, RawName -> NamePart
Id RawName
">>=", NamePart
Hole]
      qThen :: QName
qThen = Name -> QName
QName (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ Range -> NameInScope -> [NamePart] -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope [NamePart
Hole, RawName -> NamePart
Id RawName
">>", NamePart
Hole]
      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) -> [DoStmt] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any DoStmt -> Bool
isBind [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
$ [DoStmt] -> Maybe [DoStmt] -> [DoStmt]
forall a. a -> Maybe a -> a
fromMaybe [DoStmt]
ss (Maybe [DoStmt] -> [DoStmt]) -> Maybe [DoStmt] -> [DoStmt]
forall a b. (a -> b) -> a -> b
$ [DoStmt] -> Maybe [DoStmt]
forall a. [a] -> Maybe [a]
initMaybe [DoStmt]
ss] -- ignore the last 'DoThen'
  QName -> QName -> [DoStmt] -> ScopeM Expr
desugarDo QName
qBind QName
qThen [DoStmt]
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 :: QName -> QName -> [DoStmt] -> ScopeM Expr
desugarDo QName
qBind QName
qThen [] = RawName -> ScopeM Expr
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
RawName -> m a
genericError RawName
"Empty 'do' block"

-- The last statement must be a DoThen
desugarDo QName
qBind QName
qThen [DoStmt
s]
  | DoThen Expr
e              <- DoStmt
s           = Expr -> ScopeM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
  | DoBind Range
r Pattern
p Expr
e []       <- DoStmt
s
  , 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 t. SetRange t => Range -> t -> t
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
  | Bool
otherwise                            =
      RawName -> ScopeM Expr
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
RawName -> m a
genericError RawName
"The last statement in a 'do' block must be an expression or an absurd match."

-- `DoThen` and `DoLet` are easy
desugarDo QName
qBind QName
qThen (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
<$> QName -> QName -> [DoStmt] -> ScopeM Expr
desugarDo QName
qBind QName
qThen [DoStmt]
ss
desugarDo QName
qBind QName
qThen (DoLet Range
r [Declaration]
ds : [DoStmt]
ss) = Range -> [Declaration] -> Maybe Expr -> Expr
Let Range
r [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
<$> QName -> QName -> [DoStmt] -> ScopeM Expr
desugarDo QName
qBind QName
qThen [DoStmt]
ss

-- `DoBind` requires more work since we want to generate plain lambdas when
-- possible.
desugarDo QName
qBind QName
qThen (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 <- QName -> QName -> [DoStmt] -> ScopeM Expr
desugarDo QName
qBind QName
qThen [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
desugarDo QName
qBind QName
qThen (DoBind Range
r Pattern
p Expr
e [LamClause]
cs : [DoStmt]
ss) = do
  -- If there are where clauses we have to desugar to a pattern lambda.
  Expr
rest <- QName -> QName -> [DoStmt] -> ScopeM Expr
desugarDo QName
qBind QName
qThen [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

singleName :: Pattern -> Maybe Name
singleName :: Pattern -> Maybe Name
singleName (IdentP (QName Name
x)) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
singleName (RawAppP Range
_ [Pattern
p])    = Pattern -> Maybe Name
singleName Pattern
p
singleName 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 t. SetRange t => Range -> t -> t
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 -> [LamClause] -> Expr
ExtendedLam ([LamClause] -> Range
forall t. HasRange t => t -> Range
getRange [LamClause]
cs)       -- where-clauses to make highlighting of overlapping
    ([LamClause] -> Expr) -> [LamClause] -> Expr
forall a b. (a -> b) -> a -> b
$ (LamClause -> LamClause) -> [LamClause] -> [LamClause]
forall a b. (a -> b) -> [a] -> [b]
map LamClause -> LamClause
addParens (LamClause
mainClause LamClause -> [LamClause] -> [LamClause]
forall a. a -> [a] -> [a]
: [LamClause]
cs) -- patterns not highlight the rest of the do-block.
  where
    mainClause :: LamClause
mainClause = LamClause :: LHS -> RHS -> WhereClause -> Bool -> LamClause
LamClause { lamLHS :: LHS
lamLHS      = Pattern
-> [RewriteEqn] -> [WithHiding Expr] -> ExpandedEllipsis -> LHS
LHS Pattern
p [] [] ExpandedEllipsis
NoEllipsis
                           , lamRHS :: RHS
lamRHS      = Expr -> RHS
forall e. e -> RHS' e
RHS Expr
body
                           , lamWhere :: WhereClause
lamWhere    = WhereClause
forall decls. WhereClause' decls
NoWhere
                           , lamCatchAll :: Bool
lamCatchAll = Bool
False }

    -- Add parens to left-hand sides: there can only be one pattern in these clauses.
    addParens :: LamClause -> LamClause
addParens LamClause
c = LamClause
c { lamLHS :: LHS
lamLHS = LHS -> LHS
addP (LamClause -> LHS
lamLHS LamClause
c) }
      where addP :: LHS -> LHS
addP (LHS Pattern
p [RewriteEqn]
rw [WithHiding Expr]
we ExpandedEllipsis
ell) = Pattern
-> [RewriteEqn] -> [WithHiding Expr] -> ExpandedEllipsis -> LHS
LHS (Range -> [Pattern] -> Pattern
RawAppP Range
forall a. Range' a
noRange [Range -> Pattern -> Pattern
ParenP Range
forall a. Range' a
noRange Pattern
p]) [RewriteEqn]
rw [WithHiding Expr]
we ExpandedEllipsis
ell

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 t. SetRange t => Range -> t -> t
setRange Range
r QName
qBind) Expr
e (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> [LamBinding] -> Expr -> Expr
Lam ((Name, Expr) -> Range
forall t. HasRange t => t -> Range
getRange (Name
x, Expr
body)) [LamBinding
forall a. LamBinding' a
bx] Expr
body
  where bx :: LamBinding' a
bx = NamedArg Binder -> LamBinding' a
forall a. NamedArg Binder -> LamBinding' a
DomainFree (NamedArg Binder -> LamBinding' a)
-> NamedArg Binder -> LamBinding' a
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 t. HasRange t => t -> 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 t. HasRange t => t -> 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 ()