From 2ce0335fd51b84ff7ee1d1235a1dcc2e3815333b Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 4 Jul 2020 22:59:48 +0100 Subject: [PATCH] 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 --- CHANGELOG.md | 2 ++ src/Idris/Desugar.idr | 53 +++++++++++++++++++--------------- src/Idris/Parser.idr | 14 +++++++-- src/Idris/Syntax.idr | 10 +++---- tests/Main.idr | 1 + tests/idris2/basic041/QDo.idr | 9 ++++++ tests/idris2/basic041/expected | 1 + tests/idris2/basic041/run | 3 ++ 8 files changed, 62 insertions(+), 31 deletions(-) create mode 100644 tests/idris2/basic041/QDo.idr create mode 100644 tests/idris2/basic041/expected create mode 100755 tests/idris2/basic041/run diff --git a/CHANGELOG.md b/CHANGELOG.md index 6b34128e7..679d03b4f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -20,6 +20,8 @@ Language changes: * Add `import X as Y` + This imports the module `X`, adding aliases for the definitions in 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: diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index f231d4265..90816f0b4 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -269,8 +269,8 @@ mutual = pure $ IMustUnify fc UserDotted !(desugarB side ps x) desugarB side ps (PImplicit fc) = pure $ Implicit fc True desugarB side ps (PInfer fc) = pure $ Implicit fc False - desugarB side ps (PDoBlock fc block) - = expandDo side ps fc block + desugarB side ps (PDoBlock fc ns block) + = expandDo side ps fc ns block desugarB side ps (PBang fc term) = do itm <- desugarB side ps term bs <- get Bang @@ -319,7 +319,7 @@ mutual [PatClause fc (IVar fc (UN "True")) !(desugar side ps t), PatClause fc (IVar fc (UN "False")) !(desugar side ps e)] 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 guard : PDo -> PDo guard (DoExp fc tm) = DoExp fc (PApp fc (PRef fc (UN "guard")) tm) @@ -379,56 +379,61 @@ mutual = pure $ apply (IVar fc (UN "::")) [!(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} -> {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto m : Ref MD Metadata} -> - Side -> List Name -> FC -> List PDo -> Core RawImp - expandDo side ps fc [] = throw (GenericMsg fc "Do block cannot be empty") - expandDo side ps _ [DoExp fc tm] = desugar side ps tm - expandDo side ps fc [e] + Side -> List Name -> FC -> Maybe (List String) -> List PDo -> Core RawImp + 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 fc ns [e] = throw (GenericMsg (getLoc e) "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 - rest' <- expandDo side ps topfc rest + rest' <- expandDo side ps topfc ns rest -- A free standing 'case' block must return () let ty = case tm' of ICase _ _ _ _ => IVar fc (UN "Unit") _ => Implicit fc False 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 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 - rest' <- expandDo side ps topfc rest - pure $ IApp fc (IApp fc (IVar fc (UN ">>=")) tm') + rest' <- expandDo side ps topfc ns rest + pure $ IApp fc (IApp fc (IVar fc (addNS ns (UN ">>="))) tm') (ILam fc top Explicit (Just n) (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 (newps, bpat) <- bindNames False pat' exp' <- desugar side ps exp alts' <- traverse (desugarClause ps True) alts let ps' = newps ++ ps - rest' <- expandDo side ps' topfc rest - pure $ IApp fc (IApp fc (IVar fc (UN ">>=")) exp') + rest' <- expandDo side ps' topfc ns rest + pure $ IApp fc (IApp fc (IVar fc (addNS ns (UN ">>="))) exp') (ILam fc top Explicit (Just (MN "_" 0)) (Implicit fc False) (ICase fc (IVar fc (MN "_" 0)) (Implicit fc False) (PatClause fc bpat rest' :: 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 tm' <- desugarB side ps tm 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' bd <- get Bang 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 pat' <- desugar LHS ps pat ty' <- desugar side ps ty @@ -436,18 +441,18 @@ mutual tm' <- desugarB side ps tm alts' <- traverse (desugarClause ps True) alts let ps' = newps ++ ps - rest' <- expandDo side ps' topfc rest + rest' <- expandDo side ps' topfc ns rest bd <- get Bang pure $ bindBangs (bangNames bd) $ ICase fc tm' ty' (PatClause fc bpat rest' :: alts') - expandDo side ps topfc (DoLetLocal fc decls :: rest) - = do rest' <- expandDo side ps topfc rest + expandDo side ps topfc ns (DoLetLocal fc decls :: rest) + = do rest' <- expandDo side ps topfc ns rest decls' <- traverse (desugarDecl ps) decls pure $ ILocal fc (concat decls') rest' - expandDo side ps topfc (DoRewrite fc rule :: rest) - = do rest' <- expandDo side ps topfc rest + expandDo side ps topfc ns (DoRewrite fc rule :: rest) + = do rest' <- expandDo side ps topfc ns rest rule' <- desugar side ps rule pure $ IRewrite fc rule' rest' diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index f8cb68c29..d158baf6e 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -122,11 +122,11 @@ mutual appExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm appExpr q fname indents = case_ fname indents + <|> doBlock fname indents <|> lambdaCase fname indents <|> lazy fname indents <|> if_ fname indents <|> with_ fname indents - <|> doBlock fname indents <|> do start <- location f <- simpleExpr fname indents args <- many (argExpr q fname indents) @@ -740,7 +740,17 @@ mutual actions <- block (doAct fname) end <- location 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 "" = False diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index fe7cf53d6..148768039 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -76,7 +76,7 @@ mutual -- Syntactic sugar - PDoBlock : FC -> List PDo -> PTerm + PDoBlock : FC -> Maybe (List String) -> List PDo -> PTerm PBang : FC -> PTerm -> PTerm PIdiom : FC -> PTerm -> PTerm PList : FC -> List PTerm -> PTerm @@ -135,7 +135,7 @@ mutual getPTermLoc (PSectionR fc _ _) = fc getPTermLoc (PEq fc _ _) = fc getPTermLoc (PBracketed fc _) = fc - getPTermLoc (PDoBlock fc _) = fc + getPTermLoc (PDoBlock fc _ _) = fc getPTermLoc (PBang fc _) = fc getPTermLoc (PIdiom fc _) = fc getPTermLoc (PList fc _) = fc @@ -546,7 +546,7 @@ mutual 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 (PBracketed _ tm) = "(" ++ showPrec d tm ++ ")" - showPrec d (PDoBlock _ ds) + showPrec d (PDoBlock _ ns ds) = "do " ++ showSep " ; " (map showDo ds) showPrec d (PBang _ tm) = "!" ++ showPrec d tm showPrec d (PIdiom _ tm) = "[|" ++ showPrec d tm ++ "|]" @@ -828,8 +828,8 @@ mapPTermM f = goPTerm where goPTerm (PBracketed fc x) = PBracketed fc <$> goPTerm x >>= f - goPTerm (PDoBlock fc xs) = - PDoBlock fc <$> goPDos xs + goPTerm (PDoBlock fc ns xs) = + PDoBlock fc ns <$> goPDos xs >>= f goPTerm (PBang fc x) = PBang fc <$> goPTerm x diff --git a/tests/Main.idr b/tests/Main.idr index 9df5ca9e8..3676626aa 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -40,6 +40,7 @@ idrisTests "basic026", "basic027", "basic028", "basic029", "basic030", "basic031", "basic032", "basic033", "basic034", "basic035", "basic036", "basic037", "basic038", "basic039", "basic040", + "basic041", -- Coverage checking "coverage001", "coverage002", "coverage003", "coverage004", "coverage005", "coverage006", "coverage007", "coverage008", diff --git a/tests/idris2/basic041/QDo.idr b/tests/idris2/basic041/QDo.idr new file mode 100644 index 000000000..0adad9cc5 --- /dev/null +++ b/tests/idris2/basic041/QDo.idr @@ -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 diff --git a/tests/idris2/basic041/expected b/tests/idris2/basic041/expected new file mode 100644 index 000000000..38c307f38 --- /dev/null +++ b/tests/idris2/basic041/expected @@ -0,0 +1 @@ +1/1: Building QDo (QDo.idr) diff --git a/tests/idris2/basic041/run b/tests/idris2/basic041/run new file mode 100755 index 000000000..24a0859d4 --- /dev/null +++ b/tests/idris2/basic041/run @@ -0,0 +1,3 @@ +$1 --check QDo.idr + +rm -rf build