Merge pull request #4260 from Melvar/let-alternatives

Add alternatives syntax to `let` in `do` blocks

Author: Melvar

CHANGELOG.md

@@ -34,6 +34,15 @@
 + The deprecated keywords `%assert_total`, `abstract`, and `[static]` have
   been removed as well as the use of "public" instead of "public export" to
   expose a symbol.
++ The syntax for pattern-match alternatives now works for `let` statements in
+  `do` blocks in addition to `let` expressions and `<-` statements, e.g.
+  ```idris
+    do …
+       let Just x = expr | Nothing => empty
+       …
+  ```
+  This means that a `with`-application (using `|`) cannot be used in that
+  position anymore.
 
 ## Library Updates
 

src/Idris/AbsSyntaxTree.hs

@@ -1041,7 +1041,8 @@ mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
         mapPDoFC (DoBindP fc t1 t2 alts) =
           DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
         mapPDoFC (DoLet fc rc n nfc t1 t2) = DoLet (f fc) rc n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
-        mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
+        mapPDoFC (DoLetP fc t1 t2 alts) =
+          DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r) -> (mapPTermFC f g l, mapPTermFC f g r)) alts)
         mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)
 mapPTermFC f g (PIdiom fc t)                  = PIdiom (f fc) (mapPTermFC f g t)
 mapPTermFC f g (PMetavar fc n)                = PMetavar (g fc) n
@@ -1166,7 +1167,7 @@ data PDo' t = DoExp  FC t
             | DoBind FC Name FC t     -- ^ second FC is precise name location
             | DoBindP FC t t [(t,t)]
             | DoLet  FC RigCount Name FC t t   -- ^ second FC is precise name location
-            | DoLetP FC t t
+            | DoLetP FC t t [(t,t)]
             | DoRewrite FC t          -- rewrite in do block
     deriving (Eq, Ord, Functor, Data, Generic, Typeable)
 {-!
@@ -1178,7 +1179,7 @@ instance Sized a => Sized (PDo' a) where
   size (DoBind fc nm nfc t)   = 1 + size fc + size nm + size nfc + size t
   size (DoBindP fc l r alts)  = 1 + size fc + size l  + size r   + size alts
   size (DoLet fc rc nm nfc l r)  = 1 + size fc + size nm + size l   + size r
-  size (DoLetP fc l r)        = 1 + size fc + size l  + size r
+  size (DoLetP fc l r alts)   = 1 + size fc + size l  + size r + size alts
   size (DoRewrite fc h)       = 1 + size fc + size h
 
 type PDo = PDo' PTerm
@@ -1274,7 +1275,7 @@ highestFC (PDoBlock lines) =
     getDoFC (DoBind fc nm nfc t)  = fc
     getDoFC (DoBindP fc l r alts) = fc
     getDoFC (DoLet fc rc nm nfc l r) = fc
-    getDoFC (DoLetP fc l r)       = fc
+    getDoFC (DoLetP fc l r alts)  = fc
     getDoFC (DoRewrite fc h)      = fc
 
 highestFC (PIdiom fc _)           = Just fc
@@ -1955,7 +1956,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
                    else text "=") <+>
                 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
                ppdo ((ln, False):bnd) dos
-             ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
+             ppdo bnd (DoLetP _ _ _ _ : dos) = -- ok because never made by delab
                text "no pretty printer for pattern-matching do binding" :
                ppdo bnd dos
              ppdo bnd (DoRewrite _ _ : dos) = -- ok because never made by delab

src/Idris/DSL.hs

@@ -105,8 +105,8 @@ expandSugar dsl (PDoBlock ds)
                                              ((p, block b rest) : alts)))]
     block b (DoLet fc rc n nfc ty tm : rest)
         = PLet fc rc n nfc ty tm (block b rest)
-    block b (DoLetP fc p tm : rest)
-        = PCase fc tm [(p, block b rest)]
+    block b (DoLetP fc p tm alts : rest)
+        = PCase fc tm ((p, block b rest) : alts)
     block b (DoRewrite fc h : rest)
         = PRewrite fc Nothing h (block b rest) Nothing
     block b (DoExp fc tm : rest)

src/Idris/Elab/Quasiquote.hs

@@ -74,7 +74,7 @@ extractDoUnquotes d (DoLet  fc rc n nfc v b)
   = do (v', ex1) <- extractUnquotes d v
        (b', ex2) <- extractUnquotes d b
        return (DoLet fc rc n nfc v' b', ex1 ++ ex2)
-extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"
+extractDoUnquotes d (DoLetP fc t t' alts) = fail "Pattern-matching lets cannot be quasiquoted"
 extractDoUnquotes d (DoRewrite fc h) = fail "Rewrites in Do block cannot be quasiquoted"
 
 

src/Idris/Error.hs

@@ -131,7 +131,8 @@ warnDisamb ist (PDoBlock steps) = mapM_ wStep steps
         wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>
                                    mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
         wStep (DoLet _ _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
-        wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y
+        wStep (DoLetP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>
+                                  mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
         wStep (DoRewrite _ h) = warnDisamb ist h
 warnDisamb ist (PIdiom _ x) = warnDisamb ist x
 warnDisamb ist (PMetavar _ _) = return ()

src/Idris/IdrisDoc.hs

@@ -331,7 +331,9 @@ extractPDo (DoBindP _ p1 p2 ps)  = let (ps1, ps2) = unzip ps
                                        ps'        = ps1 ++ ps2
                                    in  concatMap extract (p1 : p2 : ps')
 extractPDo (DoLet _ _ n _ p1 p2) = n : concatMap extract [p1, p2]
-extractPDo (DoLetP  _ p1 p2)     = concatMap extract [p1, p2]
+extractPDo (DoLetP  _ p1 p2 ps)  = let (ps1, ps2) = unzip ps
+                                       ps'        = ps1 ++ ps2
+                                   in  concatMap extract (p1 : p2 : ps')
 extractPDo (DoRewrite  _ p)      = extract p
 
 -- | Helper function for extractPTermNames

src/Idris/Parser/Expr.hs

@@ -211,7 +211,9 @@ updateSynMatch = update
             upd ns (DoBindP fc i t ts)
                     = DoBindP fc (update ns i) (update ns t)
                                  (map (\(l,r) -> (update ns l, update ns r)) ts)
-            upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)
+            upd ns (DoLetP fc i t ts)
+                    = DoLetP fc (update ns i) (update ns t)
+                                (map (\(l,r) -> (update ns l, update ns r)) ts)
             upd ns (DoRewrite fc h) = DoRewrite fc (update ns h)
     update ns (PIdiom fc t) = PIdiom fc $ update ns t
     update ns (PMetavar fc n) = uncurry (flip PMetavar) $ updateB ns (n, fc)
@@ -1288,16 +1290,24 @@ do_ :: SyntaxInfo -> IdrisParser PDo
 do_ syn
      = P.try (do keyword "let"
                  (i, ifc) <- withExtent name
-                 ty <- P.option Placeholder (do lchar ':'
-                                                expr' syn)
+                 ty' <- P.optional (do lchar ':'
+                                       expr' syn)
                  reservedOp "="
-                 (e, fc) <- withExtent $ expr syn
-                 return (DoLet fc RigW i ifc ty e))
+                 (e, fc) <- withExtent $ expr (syn { withAppAllowed = False })
+                 -- If there is an explicit type, this can’t be a pattern-matching let, so do not parse alternatives
+                 P.option (DoLet fc RigW i ifc (fromMaybe Placeholder ty') e)
+                          (do lchar '|'
+                              when (isJust ty') $ fail "a pattern-matching let may not have an explicit type annotation"
+                              ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')
+                              return (DoLetP fc (PRef ifc [ifc] i) e ts)))
    <|> P.try (do keyword "let"
                  i <- expr' syn
                  reservedOp "="
-                 (sc, fc) <- withExtent $ expr syn
-                 return (DoLetP fc i sc))
+                 (e, fc) <- withExtent $ expr (syn { withAppAllowed = False })
+                 P.option (DoLetP fc i e [])
+                          (do lchar '|'
+                              ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')
+                              return (DoLetP fc i e ts)))
    <|> P.try (do (sc, fc) <- withExtent (keyword "rewrite" *> expr syn)
                  return (DoRewrite fc sc))
    <|> P.try (do (i, ifc) <- withExtent name

test/sugar004/expected

@@ -1,3 +1,4 @@
 No arguments!
+Not an integer!
 42
 Too many arguments!

test/sugar004/run

@@ -1,6 +1,7 @@
 #!/usr/bin/env bash
 ${IDRIS:-idris} $@ sugar004.idr -o sugar004
 ./sugar004
+./sugar004 foo
 ./sugar004 42
 ./sugar004 42 100
 rm -f sugar004 *.ibc

test/sugar004/sugar004.idr

@@ -1,5 +1,6 @@
 module Main
 
+import Data.String
 import System
 
 total
@@ -9,7 +10,8 @@ foo x = let Just x' = x | Nothing => 100 in x'
 main : IO ()
 main = do [p, a] <- getArgs | [p] => putStrLn "No arguments!"
                             | (x :: y :: _) => putStrLn "Too many arguments!"
-          printLn (foo (Just (cast a)))
+          let Just a' = parseInteger {a = Int} a | Nothing => putStrLn "Not an integer!"
+          printLn (foo (Just a'))
 
 {-
 
@@ -31,6 +33,15 @@ do x <- val
         pat => p
         <alternatives>
 
+do let pat = val | <alternatives>
+   p
+
+...becomes...
+
+do case val of
+        pat => p
+        <alternatives>
+
 -}