Implement qualified do

This allows do blocks to be qualified with the namespace that the (>>=)
operator is defined in. Inspired by Purescript's version of the same
thing, and this ghc proposal:
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0216-qualified-do.rst
This commit is contained in:
Edwin Brady 2020-07-04 22:59:48 +01:00
parent a5c9250524
commit 2ce0335fd5
8 changed files with 62 additions and 31 deletions

View File

@ -20,6 +20,8 @@ Language changes:
* Add `import X as Y` * Add `import X as Y`
+ This imports the module `X`, adding aliases for the definitions in + This imports the module `X`, adding aliases for the definitions in
namespace `Y`, so they can be referred to as `Y`. namespace `Y`, so they can be referred to as `Y`.
* `do` notation can now be qualified with a namespace
+ `MyDo.do` opens a `do` block where the `>>=` operator used is `MyDo.(>>=)`
Library changes: Library changes:

View File

@ -269,8 +269,8 @@ mutual
= pure $ IMustUnify fc UserDotted !(desugarB side ps x) = pure $ IMustUnify fc UserDotted !(desugarB side ps x)
desugarB side ps (PImplicit fc) = pure $ Implicit fc True desugarB side ps (PImplicit fc) = pure $ Implicit fc True
desugarB side ps (PInfer fc) = pure $ Implicit fc False desugarB side ps (PInfer fc) = pure $ Implicit fc False
desugarB side ps (PDoBlock fc block) desugarB side ps (PDoBlock fc ns block)
= expandDo side ps fc block = expandDo side ps fc ns block
desugarB side ps (PBang fc term) desugarB side ps (PBang fc term)
= do itm <- desugarB side ps term = do itm <- desugarB side ps term
bs <- get Bang bs <- get Bang
@ -319,7 +319,7 @@ mutual
[PatClause fc (IVar fc (UN "True")) !(desugar side ps t), [PatClause fc (IVar fc (UN "True")) !(desugar side ps t),
PatClause fc (IVar fc (UN "False")) !(desugar side ps e)] PatClause fc (IVar fc (UN "False")) !(desugar side ps e)]
desugarB side ps (PComprehension fc ret conds) desugarB side ps (PComprehension fc ret conds)
= desugarB side ps (PDoBlock fc (map guard conds ++ [toPure ret])) = desugarB side ps (PDoBlock fc Nothing (map guard conds ++ [toPure ret]))
where where
guard : PDo -> PDo guard : PDo -> PDo
guard (DoExp fc tm) = DoExp fc (PApp fc (PRef fc (UN "guard")) tm) guard (DoExp fc tm) = DoExp fc (PApp fc (PRef fc (UN "guard")) tm)
@ -379,56 +379,61 @@ mutual
= pure $ apply (IVar fc (UN "::")) = pure $ apply (IVar fc (UN "::"))
[!(desugarB side ps x), !(expandList side ps fc xs)] [!(desugarB side ps x), !(expandList side ps fc xs)]
addNS : Maybe (List String) -> Name -> Name
addNS (Just ns) n@(NS _ _) = n
addNS (Just ns) n = NS ns n
addNS _ n = n
expandDo : {auto s : Ref Syn SyntaxInfo} -> expandDo : {auto s : Ref Syn SyntaxInfo} ->
{auto c : Ref Ctxt Defs} -> {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
Side -> List Name -> FC -> List PDo -> Core RawImp Side -> List Name -> FC -> Maybe (List String) -> List PDo -> Core RawImp
expandDo side ps fc [] = throw (GenericMsg fc "Do block cannot be empty") expandDo side ps fc ns [] = throw (GenericMsg fc "Do block cannot be empty")
expandDo side ps _ [DoExp fc tm] = desugar side ps tm expandDo side ps _ _ [DoExp fc tm] = desugar side ps tm
expandDo side ps fc [e] expandDo side ps fc ns [e]
= throw (GenericMsg (getLoc e) = throw (GenericMsg (getLoc e)
"Last statement in do block must be an expression") "Last statement in do block must be an expression")
expandDo side ps topfc (DoExp fc tm :: rest) expandDo side ps topfc ns (DoExp fc tm :: rest)
= do tm' <- desugar side ps tm = do tm' <- desugar side ps tm
rest' <- expandDo side ps topfc rest rest' <- expandDo side ps topfc ns rest
-- A free standing 'case' block must return () -- A free standing 'case' block must return ()
let ty = case tm' of let ty = case tm' of
ICase _ _ _ _ => IVar fc (UN "Unit") ICase _ _ _ _ => IVar fc (UN "Unit")
_ => Implicit fc False _ => Implicit fc False
gam <- get Ctxt gam <- get Ctxt
pure $ IApp fc (IApp fc (IVar fc (UN ">>=")) tm') pure $ IApp fc (IApp fc (IVar fc (addNS ns (UN ">>="))) tm')
(ILam fc top Explicit Nothing (ILam fc top Explicit Nothing
ty rest') ty rest')
expandDo side ps topfc (DoBind fc n tm :: rest) expandDo side ps topfc ns (DoBind fc n tm :: rest)
= do tm' <- desugar side ps tm = do tm' <- desugar side ps tm
rest' <- expandDo side ps topfc rest rest' <- expandDo side ps topfc ns rest
pure $ IApp fc (IApp fc (IVar fc (UN ">>=")) tm') pure $ IApp fc (IApp fc (IVar fc (addNS ns (UN ">>="))) tm')
(ILam fc top Explicit (Just n) (ILam fc top Explicit (Just n)
(Implicit fc False) rest') (Implicit fc False) rest')
expandDo side ps topfc (DoBindPat fc pat exp alts :: rest) expandDo side ps topfc ns (DoBindPat fc pat exp alts :: rest)
= do pat' <- desugar LHS ps pat = do pat' <- desugar LHS ps pat
(newps, bpat) <- bindNames False pat' (newps, bpat) <- bindNames False pat'
exp' <- desugar side ps exp exp' <- desugar side ps exp
alts' <- traverse (desugarClause ps True) alts alts' <- traverse (desugarClause ps True) alts
let ps' = newps ++ ps let ps' = newps ++ ps
rest' <- expandDo side ps' topfc rest rest' <- expandDo side ps' topfc ns rest
pure $ IApp fc (IApp fc (IVar fc (UN ">>=")) exp') pure $ IApp fc (IApp fc (IVar fc (addNS ns (UN ">>="))) exp')
(ILam fc top Explicit (Just (MN "_" 0)) (ILam fc top Explicit (Just (MN "_" 0))
(Implicit fc False) (Implicit fc False)
(ICase fc (IVar fc (MN "_" 0)) (ICase fc (IVar fc (MN "_" 0))
(Implicit fc False) (Implicit fc False)
(PatClause fc bpat rest' (PatClause fc bpat rest'
:: alts'))) :: alts')))
expandDo side ps topfc (DoLet fc n rig ty tm :: rest) expandDo side ps topfc ns (DoLet fc n rig ty tm :: rest)
= do b <- newRef Bang initBangs = do b <- newRef Bang initBangs
tm' <- desugarB side ps tm tm' <- desugarB side ps tm
ty' <- desugar side ps ty ty' <- desugar side ps ty
rest' <- expandDo side ps topfc rest rest' <- expandDo side ps topfc ns rest
let bind = ILet fc rig n ty' tm' rest' let bind = ILet fc rig n ty' tm' rest'
bd <- get Bang bd <- get Bang
pure $ bindBangs (bangNames bd) bind pure $ bindBangs (bangNames bd) bind
expandDo side ps topfc (DoLetPat fc pat ty tm alts :: rest) expandDo side ps topfc ns (DoLetPat fc pat ty tm alts :: rest)
= do b <- newRef Bang initBangs = do b <- newRef Bang initBangs
pat' <- desugar LHS ps pat pat' <- desugar LHS ps pat
ty' <- desugar side ps ty ty' <- desugar side ps ty
@ -436,18 +441,18 @@ mutual
tm' <- desugarB side ps tm tm' <- desugarB side ps tm
alts' <- traverse (desugarClause ps True) alts alts' <- traverse (desugarClause ps True) alts
let ps' = newps ++ ps let ps' = newps ++ ps
rest' <- expandDo side ps' topfc rest rest' <- expandDo side ps' topfc ns rest
bd <- get Bang bd <- get Bang
pure $ bindBangs (bangNames bd) $ pure $ bindBangs (bangNames bd) $
ICase fc tm' ty' ICase fc tm' ty'
(PatClause fc bpat rest' (PatClause fc bpat rest'
:: alts') :: alts')
expandDo side ps topfc (DoLetLocal fc decls :: rest) expandDo side ps topfc ns (DoLetLocal fc decls :: rest)
= do rest' <- expandDo side ps topfc rest = do rest' <- expandDo side ps topfc ns rest
decls' <- traverse (desugarDecl ps) decls decls' <- traverse (desugarDecl ps) decls
pure $ ILocal fc (concat decls') rest' pure $ ILocal fc (concat decls') rest'
expandDo side ps topfc (DoRewrite fc rule :: rest) expandDo side ps topfc ns (DoRewrite fc rule :: rest)
= do rest' <- expandDo side ps topfc rest = do rest' <- expandDo side ps topfc ns rest
rule' <- desugar side ps rule rule' <- desugar side ps rule
pure $ IRewrite fc rule' rest' pure $ IRewrite fc rule' rest'

View File

@ -122,11 +122,11 @@ mutual
appExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm appExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
appExpr q fname indents appExpr q fname indents
= case_ fname indents = case_ fname indents
<|> doBlock fname indents
<|> lambdaCase fname indents <|> lambdaCase fname indents
<|> lazy fname indents <|> lazy fname indents
<|> if_ fname indents <|> if_ fname indents
<|> with_ fname indents <|> with_ fname indents
<|> doBlock fname indents
<|> do start <- location <|> do start <- location
f <- simpleExpr fname indents f <- simpleExpr fname indents
args <- many (argExpr q fname indents) args <- many (argExpr q fname indents)
@ -740,7 +740,17 @@ mutual
actions <- block (doAct fname) actions <- block (doAct fname)
end <- location end <- location
end <- pure $ fromMaybe end $ map (endPos . getLoc) $ join $ last' <$> last' actions end <- pure $ fromMaybe end $ map (endPos . getLoc) $ join $ last' <$> last' actions
pure (PDoBlock (MkFC fname start end) (concat actions)) pure (PDoBlock (MkFC fname start end) Nothing (concat actions))
<|> do start <- location
nsdo <- namespacedIdent
the (SourceEmptyRule PTerm) $ case nsdo of
("do" :: ns) =>
do actions <- block (doAct fname)
end <- location
end <- pure $ fromMaybe end $ map (endPos . getLoc) $ join $ last' <$> last' actions
pure (PDoBlock (MkFC fname start end)
(Just (reverse ns)) (concat actions))
_ => fail "Not a namespaced 'do'"
lowerFirst : String -> Bool lowerFirst : String -> Bool
lowerFirst "" = False lowerFirst "" = False

View File

@ -76,7 +76,7 @@ mutual
-- Syntactic sugar -- Syntactic sugar
PDoBlock : FC -> List PDo -> PTerm PDoBlock : FC -> Maybe (List String) -> List PDo -> PTerm
PBang : FC -> PTerm -> PTerm PBang : FC -> PTerm -> PTerm
PIdiom : FC -> PTerm -> PTerm PIdiom : FC -> PTerm -> PTerm
PList : FC -> List PTerm -> PTerm PList : FC -> List PTerm -> PTerm
@ -135,7 +135,7 @@ mutual
getPTermLoc (PSectionR fc _ _) = fc getPTermLoc (PSectionR fc _ _) = fc
getPTermLoc (PEq fc _ _) = fc getPTermLoc (PEq fc _ _) = fc
getPTermLoc (PBracketed fc _) = fc getPTermLoc (PBracketed fc _) = fc
getPTermLoc (PDoBlock fc _) = fc getPTermLoc (PDoBlock fc _ _) = fc
getPTermLoc (PBang fc _) = fc getPTermLoc (PBang fc _) = fc
getPTermLoc (PIdiom fc _) = fc getPTermLoc (PIdiom fc _) = fc
getPTermLoc (PList fc _) = fc getPTermLoc (PList fc _) = fc
@ -546,7 +546,7 @@ mutual
showPrec d (PSectionR _ x op) = "(" ++ showPrec d x ++ " " ++ showPrec d op ++ ")" showPrec d (PSectionR _ x op) = "(" ++ showPrec d x ++ " " ++ showPrec d op ++ ")"
showPrec d (PEq fc l r) = showPrec d l ++ " = " ++ showPrec d r showPrec d (PEq fc l r) = showPrec d l ++ " = " ++ showPrec d r
showPrec d (PBracketed _ tm) = "(" ++ showPrec d tm ++ ")" showPrec d (PBracketed _ tm) = "(" ++ showPrec d tm ++ ")"
showPrec d (PDoBlock _ ds) showPrec d (PDoBlock _ ns ds)
= "do " ++ showSep " ; " (map showDo ds) = "do " ++ showSep " ; " (map showDo ds)
showPrec d (PBang _ tm) = "!" ++ showPrec d tm showPrec d (PBang _ tm) = "!" ++ showPrec d tm
showPrec d (PIdiom _ tm) = "[|" ++ showPrec d tm ++ "|]" showPrec d (PIdiom _ tm) = "[|" ++ showPrec d tm ++ "|]"
@ -828,8 +828,8 @@ mapPTermM f = goPTerm where
goPTerm (PBracketed fc x) = goPTerm (PBracketed fc x) =
PBracketed fc <$> goPTerm x PBracketed fc <$> goPTerm x
>>= f >>= f
goPTerm (PDoBlock fc xs) = goPTerm (PDoBlock fc ns xs) =
PDoBlock fc <$> goPDos xs PDoBlock fc ns <$> goPDos xs
>>= f >>= f
goPTerm (PBang fc x) = goPTerm (PBang fc x) =
PBang fc <$> goPTerm x PBang fc <$> goPTerm x

View File

@ -40,6 +40,7 @@ idrisTests
"basic026", "basic027", "basic028", "basic029", "basic030", "basic026", "basic027", "basic028", "basic029", "basic030",
"basic031", "basic032", "basic033", "basic034", "basic035", "basic031", "basic032", "basic033", "basic034", "basic035",
"basic036", "basic037", "basic038", "basic039", "basic040", "basic036", "basic037", "basic038", "basic039", "basic040",
"basic041",
-- Coverage checking -- Coverage checking
"coverage001", "coverage002", "coverage003", "coverage004", "coverage001", "coverage002", "coverage003", "coverage004",
"coverage005", "coverage006", "coverage007", "coverage008", "coverage005", "coverage006", "coverage007", "coverage008",

View File

@ -0,0 +1,9 @@
namespace MyDo
export
(>>=) : a -> (a -> IO b) -> IO b
(>>=) val k = k val
foo : IO ()
foo = MyDo.do
x <- "Silly"
putStrLn x

View File

@ -0,0 +1 @@
1/1: Building QDo (QDo.idr)

3
tests/idris2/basic041/run Executable file
View File

@ -0,0 +1,3 @@
$1 --check QDo.idr
rm -rf build