d1fae54 · Idris-dev · git.iko.soy

CHANGELOG.md+9

compare with master

unifiedsplit

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

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

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

36 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.

37

46

38## Library Updates

47## Library Updates

39

48

src/Idris/AbsSyntaxTree.hs+6−5

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

1041 mapPDoFC (DoBindP fc t1 t2 alts) =

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

1043 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 alts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1169 | 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)]

1170 | DoRewrite FC t -- rewrite in do block

1171 | DoRewrite FC t -- rewrite in do block

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

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

1172{-!

1173{-!

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

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

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

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

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

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

1181 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

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

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

1183

1184

1184type PDo = PDo' PTerm

1185type PDo = PDo' PTerm

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

1274 getDoFC (DoBind fc nm nfc t) = fc

1275 getDoFC (DoBind fc nm nfc t) = fc

1275 getDoFC (DoBindP fc l r alts) = fc

1276 getDoFC (DoBindP fc l r alts) = fc

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

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

1277− getDoFC (DoLetP fc l r) = fc

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

1278 getDoFC (DoRewrite fc h) = fc

1279 getDoFC (DoRewrite fc h) = fc

1279

1280

1280highestFC (PIdiom fc _) = Just fc

1281highestFC (PIdiom fc _) = Just fc

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

1955 else text "=") <+>

1956 else text "=") <+>

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

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

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

1958 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

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

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

1960 ppdo bnd dos

1961 ppdo bnd dos

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

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

src/Idris/DSL.hs+2−2

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

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

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

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

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

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

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

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

110 block b (DoRewrite fc h : rest)

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

112 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)

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

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

76 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"

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

79

80

src/Idris/Error.hs+2−1

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

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

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

133 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

135 wStep (DoRewrite _ h) = warnDisamb ist h

136 wStep (DoRewrite _ h) = warnDisamb ist h

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

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

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

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

src/Idris/IdrisDoc.hs+3−1

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

331 ps' = ps1 ++ ps2

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

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

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

335+ ps' = ps1 ++ ps2

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

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

335extractPDo (DoRewrite _ p) = extract p

337extractPDo (DoRewrite _ p) = extract p

336

338

337-- | Helper function for extractPTermNames

339-- | Helper function for extractPTermNames

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

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

211 upd ns (DoBindP fc i t ts)

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

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

214+ upd ns (DoLetP fc i t ts)

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

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

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

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

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

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

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

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

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

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

1288do_ syn

1290do_ syn

1289 = P.try (do keyword "let"

1291 = P.try (do keyword "let"

1290 (i, ifc) <- withExtent name

1292 (i, ifc) <- withExtent name

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

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

1292− expr' syn)

1294+ expr' syn)

1293 reservedOp "="

1295 reservedOp "="

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

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

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

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)))

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

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

1297 i <- expr' syn

1304 i <- expr' syn

1298 reservedOp "="

1305 reservedOp "="

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

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 '|')

1300− return (DoLetP fc i sc))

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

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

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

1302 return (DoRewrite fc sc))

1312 return (DoRewrite fc sc))

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

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

test/sugar004/expected+1

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

1No arguments!

2+Not an integer!

242

342

3Too many arguments!

4Too many arguments!

test/sugar004/run+1

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

1#!/usr/bin/env bash

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

3./sugar004

4+./sugar004 foo

4./sugar004 42

5./sugar004 42

5./sugar004 42 100

6./sugar004 42 100

6rm -f sugar004 *.ibc

7rm -f sugar004 *.ibc

test/sugar004/sugar004.idr+12−1

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

1module Main

2

3+import Data.String

3import System

4import System

4

5

5total

6total

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

9main : IO ()

10main : IO ()

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

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

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

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

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

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

14+ printLn (foo (Just a'))

13

15

14{-

16{-

15

17

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

31 pat => p

33 pat => p

32 <alternatives>

34 <alternatives>

33

35

36+do let pat = val | <alternatives>

37+ p

38+

39+...becomes...

40+

41+do case val of

42+ pat => p

43+ <alternatives>

44+

34-}

45-}

35

46

36

47