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
mapM_ ensureInScope $ [qBind | any isBind ss] ++
[qThen | any isThen $ fromMaybe ss $ initMaybe ss]
desugarDo qBind qThen ss
desugarDo :: QName -> QName -> [DoStmt] -> ScopeM Expr
desugarDo qBind qThen [] = genericError "Empty 'do' block"
desugarDo qBind qThen [s]
| DoThen e <- s = return e
| otherwise = genericError "The last statement in a 'do' block must be an expression"
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
desugarDo qBind qThen (DoBind r p e [] : ss)
| Just x <- singleName p = do
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
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
$ ExtendedLam (getRange cs)
$ map addParens (mainClause : cs)
where
mainClause = LamClause { lamLHS = LHS p [] []
, lamRHS = RHS body
, lamWhere = NoWhere
, lamCatchAll = False }
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
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 ()