d1fae54 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #4260 from Melvar/let-alternatives

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

commitd1fae54cd2afe306ab8200afe29901843031296a authorMelvar Chen <Melvar.Chen@googlemail.com> dateThu 4 Jan 2018, 23:31 (9 years ago) parentf71664e b17c634

10 files changed+54−18

compare with master

unifiedsplit

CHANGELOG.md+9 src/Idris/AbsSyntaxTree.hs+6−5 src/Idris/DSL.hs+2−2 src/Idris/Elab/Quasiquote.hs+1−1 src/Idris/Error.hs+2−1 src/Idris/IdrisDoc.hs+3−1 src/Idris/Parser/Expr.hs+17−7 test/sugar004/expected+1 test/sugar004/run+1 test/sugar004/sugar004.idr+12−1

CHANGELOG.md+9

@@ -34,6 +34,15 @@

3434+ The deprecated keywords `%assert_total`, `abstract`, and `[static]` have

3535 been removed as well as the use of "public" instead of "public export" to

3636 expose a symbol.

37++ The syntax for pattern-match alternatives now works for `let` statements in

38+ `do` blocks in addition to `let` expressions and `<-` statements, e.g.

39+ ```idris

40+ do …

41+ let Just x = expr | Nothing => empty

42+ …

43+ ```

44+ This means that a `with`-application (using `|`) cannot be used in that

45+ position anymore.

3746

3847## Library Updates

3948

src/Idris/AbsSyntaxTree.hs+6−5

@@ -1041,7 +1041,8 @@ mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)

10411041 mapPDoFC (DoBindP fc t1 t2 alts) =

10421042 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)

10431043 mapPDoFC (DoLet fc rc n nfc t1 t2) = DoLet (f fc) rc n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)

1044− mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)

1044+ mapPDoFC (DoLetP fc t1 t2 alts) =

1045+ DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r) -> (mapPTermFC f g l, mapPTermFC f g r)) alts)

10451046 mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)

10461047mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)

10471048mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n

@@ -1166,7 +1167,7 @@ data PDo' t = DoExp FC t

11661167 | DoBind FC Name FC t -- ^ second FC is precise name location

11671168 | DoBindP FC t t [(t,t)]

11681169 | DoLet FC RigCount Name FC t t -- ^ second FC is precise name location

1169− | DoLetP FC t t

1170+ | DoLetP FC t t [(t,t)]

11701171 | DoRewrite FC t -- rewrite in do block

11711172 deriving (Eq, Ord, Functor, Data, Generic, Typeable)

11721173{-!

@@ -1178,7 +1179,7 @@ instance Sized a => Sized (PDo' a) where

11781179 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t

11791180 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts

11801181 size (DoLet fc rc nm nfc l r) = 1 + size fc + size nm + size l + size r

1181− size (DoLetP fc l r) = 1 + size fc + size l + size r

1182+ size (DoLetP fc l r alts) = 1 + size fc + size l + size r + size alts

11821183 size (DoRewrite fc h) = 1 + size fc + size h

11831184

11841185type PDo = PDo' PTerm

@@ -1274,7 +1275,7 @@ highestFC (PDoBlock lines) =

12741275 getDoFC (DoBind fc nm nfc t) = fc

12751276 getDoFC (DoBindP fc l r alts) = fc

12761277 getDoFC (DoLet fc rc nm nfc l r) = fc

1277− getDoFC (DoLetP fc l r) = fc

1278+ getDoFC (DoLetP fc l r alts) = fc

12781279 getDoFC (DoRewrite fc h) = fc

12791280

12801281highestFC (PIdiom fc _) = Just fc

@@ -1955,7 +1956,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

19551956 else text "=") <+>

19561957 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :

19571958 ppdo ((ln, False):bnd) dos

1958− ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab

1959+ ppdo bnd (DoLetP _ _ _ _ : dos) = -- ok because never made by delab

19591960 text "no pretty printer for pattern-matching do binding" :

19601961 ppdo bnd dos

19611962 ppdo bnd (DoRewrite _ _ : dos) = -- ok because never made by delab

src/Idris/DSL.hs+2−2

@@ -105,8 +105,8 @@ expandSugar dsl (PDoBlock ds)

105105 ((p, block b rest) : alts)))]

106106 block b (DoLet fc rc n nfc ty tm : rest)

107107 = PLet fc rc n nfc ty tm (block b rest)

108− block b (DoLetP fc p tm : rest)

109− = PCase fc tm [(p, block b rest)]

108+ block b (DoLetP fc p tm alts : rest)

109+ = PCase fc tm ((p, block b rest) : alts)

110110 block b (DoRewrite fc h : rest)

111111 = PRewrite fc Nothing h (block b rest) Nothing

112112 block b (DoExp fc tm : rest)

src/Idris/Elab/Quasiquote.hs+1−1

@@ -74,7 +74,7 @@ extractDoUnquotes d (DoLet fc rc n nfc v b)

7474 = do (v', ex1) <- extractUnquotes d v

7575 (b', ex2) <- extractUnquotes d b

7676 return (DoLet fc rc n nfc v' b', ex1 ++ ex2)

77−extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"

77+extractDoUnquotes d (DoLetP fc t t' alts) = fail "Pattern-matching lets cannot be quasiquoted"

7878extractDoUnquotes d (DoRewrite fc h) = fail "Rewrites in Do block cannot be quasiquoted"

7979

8080

src/Idris/Error.hs+2−1

@@ -131,7 +131,8 @@ warnDisamb ist (PDoBlock steps) = mapM_ wStep steps

131131 wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>

132132 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs

133133 wStep (DoLet _ _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y

134− wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y

134+ wStep (DoLetP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>

135+ mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs

135136 wStep (DoRewrite _ h) = warnDisamb ist h

136137warnDisamb ist (PIdiom _ x) = warnDisamb ist x

137138warnDisamb ist (PMetavar _ _) = return ()

src/Idris/IdrisDoc.hs+3−1

@@ -331,7 +331,9 @@ extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps

331331 ps' = ps1 ++ ps2

332332 in concatMap extract (p1 : p2 : ps')

333333extractPDo (DoLet _ _ n _ p1 p2) = n : concatMap extract [p1, p2]

334−extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]

334+extractPDo (DoLetP _ p1 p2 ps) = let (ps1, ps2) = unzip ps

335+ ps' = ps1 ++ ps2

336+ in concatMap extract (p1 : p2 : ps')

335337extractPDo (DoRewrite _ p) = extract p

336338

337339-- | Helper function for extractPTermNames

src/Idris/Parser/Expr.hs+17−7

@@ -211,7 +211,9 @@ updateSynMatch = update

211211 upd ns (DoBindP fc i t ts)

212212 = DoBindP fc (update ns i) (update ns t)

213213 (map (\(l,r) -> (update ns l, update ns r)) ts)

214− upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)

214+ upd ns (DoLetP fc i t ts)

215+ = DoLetP fc (update ns i) (update ns t)

216+ (map (\(l,r) -> (update ns l, update ns r)) ts)

215217 upd ns (DoRewrite fc h) = DoRewrite fc (update ns h)

216218 update ns (PIdiom fc t) = PIdiom fc $ update ns t

217219 update ns (PMetavar fc n) = uncurry (flip PMetavar) $ updateB ns (n, fc)

@@ -1288,16 +1290,24 @@ do_ :: SyntaxInfo -> IdrisParser PDo

12881290do_ syn

12891291 = P.try (do keyword "let"

12901292 (i, ifc) <- withExtent name

1291− ty <- P.option Placeholder (do lchar ':'

1292− expr' syn)

1293+ ty' <- P.optional (do lchar ':'

1294+ expr' syn)

12931295 reservedOp "="

1294− (e, fc) <- withExtent $ expr syn

1295− return (DoLet fc RigW i ifc ty e))

1296+ (e, fc) <- withExtent $ expr (syn { withAppAllowed = False })

1297+ -- If there is an explicit type, this can’t be a pattern-matching let, so do not parse alternatives

1298+ P.option (DoLet fc RigW i ifc (fromMaybe Placeholder ty') e)

1299+ (do lchar '|'

1300+ when (isJust ty') $ fail "a pattern-matching let may not have an explicit type annotation"

1301+ ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1302+ return (DoLetP fc (PRef ifc [ifc] i) e ts)))

12961303 <|> P.try (do keyword "let"

12971304 i <- expr' syn

12981305 reservedOp "="

1299− (sc, fc) <- withExtent $ expr syn

1300− return (DoLetP fc i sc))

1306+ (e, fc) <- withExtent $ expr (syn { withAppAllowed = False })

1307+ P.option (DoLetP fc i e [])

1308+ (do lchar '|'

1309+ ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1310+ return (DoLetP fc i e ts)))

13011311 <|> P.try (do (sc, fc) <- withExtent (keyword "rewrite" *> expr syn)

13021312 return (DoRewrite fc sc))

13031313 <|> P.try (do (i, ifc) <- withExtent name

test/sugar004/expected+1

@@ -1,3 +1,4 @@

11No arguments!

2+Not an integer!

2342

34Too many arguments!

test/sugar004/run+1

@@ -1,6 +1,7 @@

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ sugar004.idr -o sugar004

33./sugar004

4+./sugar004 foo

45./sugar004 42

56./sugar004 42 100

67rm -f sugar004 *.ibc

test/sugar004/sugar004.idr+12−1

@@ -1,5 +1,6 @@

11module Main

3+import Data.String

34import System

56total

@@ -9,7 +10,8 @@ foo x = let Just x' = x | Nothing => 100 in x'

910main : IO ()

1011main = do [p, a] <- getArgs | [p] => putStrLn "No arguments!"

1112 | (x :: y :: _) => putStrLn "Too many arguments!"

12− printLn (foo (Just (cast a)))

13+ let Just a' = parseInteger {a = Int} a | Nothing => putStrLn "Not an integer!"

14+ printLn (foo (Just a'))

1315

1416{-

1517

@@ -31,6 +33,15 @@ do x <- val

3133 pat => p

3234 <alternatives>

3335

36+do let pat = val | <alternatives>

37+ p

38+

39+...becomes...

40+

41+do case val of

42+ pat => p

43+ <alternatives>

44+

3445-}

3546

3647