e0c893c · Idris-dev · git.iko.soy

CHANGELOG.md+2

@@ -28,6 +28,8 @@

2828* `natEnumFromThen` and `natEnumFromTo` have been updated to correctly calculate reverse ranges. Range syntax `[a,b..c]` now can be used again to generate reverse ranges.

2929* `divBN` and `modBN` now can only be used for unsigned numbers.

3030

31+* `return`, which has been an alias for `pure` for many releases, is now deprecated.

32+

3133## Tool updates

3234

3335* Idris' documentation system now displays the documentation for auto

libs/base/Control/Arrow.idr+5−5

@@ -34,20 +34,20 @@ implementation Arrow Morphism where

3434 (Mor f) &&& (Mor g) = Mor $ \a => (f a, g a)

3535

3636implementation Monad m => Arrow (Kleislimorphism m) where

37− arrow f = Kleisli (return . f)

37+ arrow f = Kleisli (pure . f)

3838 first (Kleisli f) = Kleisli $ \(a, b) => do x <- f a

39− return (x, b)

39+ pure (x, b)

4040

4141 second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b

42− return (a, x)

42+ pure (a, x)

4343

4444 (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a

4545 y <- g b

46− return (x, y)

46+ pure (x, y)

4747

4848 (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a

4949 y <- g a

50− return (x, y)

50+ pure (x, y)

5151

5252interface Arrow arr => ArrowZero (arr : Type -> Type -> Type) where

5353 zeroArrow : arr a b

libs/base/Control/Catchable.idr+1−1

@@ -24,7 +24,7 @@ implementation Catchable (IOExcept err) err where

2424 catch (IOM prog) h = IOM (do p' <- prog

2525 case p' of

2626 Left e => let IOM he = h e in he

27− Right val => return (Right val))

27+ Right val => pure (Right val))

2828 throw = ioe_fail

2929

3030implementation Catchable List () where

libs/base/Control/Category.idr+1−1

@@ -15,7 +15,7 @@ implementation Category Morphism where

1515 (Mor f) . (Mor g) = with Basics (Mor (f . g))

1616

1717implementation Monad m => Category (Kleislimorphism m) where

18− id = Kleisli (return . id)

18+ id = Kleisli (pure . id)

1919 (Kleisli f) . (Kleisli g) = Kleisli $ \a => g a >>= f

2020

2121infixr 1 >>>

libs/base/Control/Monad/RWS.idr+10−10

@@ -17,34 +17,34 @@ record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where

1717

1818implementation Monad m => Functor (RWST r w s m) where

1919 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s

20− return (f a, s', w)

20+ pure (f a, s', w)

2121

2222implementation (Monoid w, Monad m) => Applicative (RWST r w s m) where

23− pure a = MkRWST $ \_,s => return (a, s, neutral)

23+ pure a = MkRWST $ \_,s => pure (a, s, neutral)

2424 (MkRWST f) <*> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s

2525 (fn, ss, w') <- f r s

26− return (fn a, ss, w <+> w')

26+ pure (fn a, ss, w <+> w')

2727

2828implementation (Monoid w, Monad m) => Monad (RWST r w s m) where

2929 (MkRWST m) >>= k = MkRWST $ \r,s => do (a, s', w) <- m r s

3030 let MkRWST ka = k a

3131 (b, ss, w') <- ka r s'

32− return (b, ss, w <+> w')

32+ pure (b, ss, w <+> w')

3333

3434implementation (Monoid w, Monad m) => MonadReader r (RWST r w s m) where

35− ask = MkRWST $ \r,s => return (r, s, neutral)

35+ ask = MkRWST $ \r,s => pure (r, s, neutral)

3636 local f (MkRWST m) = MkRWST $ \r,s => m (f r) s

3737

3838implementation (Monoid w, Monad m) => MonadWriter w (RWST r w s m) where

39− tell w = MkRWST $ \_,s => return ((), s, w)

39+ tell w = MkRWST $ \_,s => pure ((), s, w)

4040 listen (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s

41− return ((a, w), s', w)

41+ pure ((a, w), s', w)

4242 pass (MkRWST m) = MkRWST $ \r,s => do ((a, f), s', w) <- m r s

43− return (a, s', f w)

43+ pure (a, s', f w)

4444

4545implementation (Monoid w, Monad m) => MonadState s (RWST r w s m) where

46− get = MkRWST $ \_,s => return (s, s, neutral)

47− put s = MkRWST $ \_,_ => return ((), s, neutral)

46+ get = MkRWST $ \_,s => pure (s, s, neutral)

47+ put s = MkRWST $ \_,_ => pure ((), s, neutral)

4848

4949implementation (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}

5050

libs/base/Control/Monad/Reader.idr+2−2

@@ -39,7 +39,7 @@ implementation Monad m => Monad (ReaderT r m) where

3939 ka r

4040

4141implementation Monad m => MonadReader r (ReaderT r m) where

42− ask = RD return

42+ ask = RD pure

4343 local f (RD m) = RD $ m . f

4444

4545implementation MonadTrans (ReaderT r) where

@@ -48,7 +48,7 @@ implementation MonadTrans (ReaderT r) where

4848||| Evaluate a function in the context of a Reader monad

4949asks : MonadReader r m => (r -> a) -> m a

5050asks f = do r <- ask

51− return (f r)

51+ pure (f r)

5252

5353||| The reader monad. See MonadReader

5454Reader : Type -> Type -> Type

libs/base/Control/Monad/State.idr+5−5

@@ -27,7 +27,7 @@ implementation Monad f => Applicative (StateT stateType f) where

2727

2828 (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st

2929 (b, t) <- a r

30− return (g b, t))

30+ pure (g b, t))

3131

3232implementation Monad m => Monad (StateT stateType m) where

3333 (ST f) >>= k = ST (\st => do (v, st') <- f st

@@ -35,12 +35,12 @@ implementation Monad m => Monad (StateT stateType m) where

3535 kv st')

3636

3737implementation Monad m => MonadState stateType (StateT stateType m) where

38− get = ST (\x => return (x, x))

39− put x = ST (\y => return ((), x))

38+ get = ST (\x => pure (x, x))

39+ put x = ST (\y => pure ((), x))

4040

4141implementation MonadTrans (StateT stateType) where

4242 lift x = ST (\st => do r <- x

43− return (r, st))

43+ pure (r, st))

4444

4545||| Apply a function to modify the context of this computation

4646modify : MonadState stateType m => (stateType -> stateType) -> m ()

@@ -50,7 +50,7 @@ modify f = do s <- get

5050||| Evaluate a function in the context held by this computation

5151gets : MonadState stateType m => (stateType -> a) -> m a

5252gets f = do s <- get

53− return (f s)

53+ pure (f s)

5454

5555||| The State monad. See the MonadState interface

5656State : (stateType : Type) -> (ty : Type) -> Type

libs/base/Control/Monad/Writer.idr+7−7

@@ -36,30 +36,30 @@ implementation (Monoid w, Monad m) => Monad (WriterT w m) where

3636 (WR m) >>= k = WR $ do (a, w) <- m

3737 let WR ka = k a

3838 (b, w') <- ka

39− return (b, w <+> w')

39+ pure (b, w <+> w')

4040

4141implementation (Monoid w, Monad m) => MonadWriter w (WriterT w m) where

42− tell w = WR $ return ((), w)

42+ tell w = WR $ pure ((), w)

4343 listen (WR m) = WR $ do (a, w) <- m

44− return ((a, w), w)

44+ pure ((a, w), w)

4545 pass (WR m) = WR $ do ((a, f), w) <- m

46− return (a, f w)

46+ pure (a, f w)

4747

4848implementation Monoid w => MonadTrans (WriterT w) where

4949 lift x = WR $ do r <- x

50− return (r, neutral)

50+ pure (r, neutral)

5151

5252||| Run an action in the Writer monad and transform the written output

5353listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)

5454listens {m} f act = listens' f (listen act) where

5555 listens' : (w -> b) -> m (a, w) -> m (a, b)

5656 listens' f' ma = do (a, w) <- ma

57− return (a, f' w)

57+ pure (a, f' w)

5858

5959||| Run an action, apply a function to it's output, and return it's value

6060censor : MonadWriter w m => (w -> w) -> m a -> m a

6161censor f m = pass $ do a <- m

62− return (a, f)

62+ pure (a, f)

6363

6464||| The Writer monad itself. See the MonadWriter interface

6565Writer : Type -> Type -> Type

libs/base/Data/List.idr+1−1

@@ -42,7 +42,7 @@ isElem x (y :: xs) with (decEq x y)

4242||| @xs The list to be removed from

4343||| @p A proof that the element to be removed is in the list

4444dropElem : (xs : List a) -> (p : Elem x xs) -> List a

45−dropElem (x :: ys) Here = ys

45+dropElem (x :: ys) Here = ys

4646dropElem (x :: ys) (There p) = x :: dropElem ys p

4747

4848||| The intersectBy function returns the intersect of two lists by user-supplied equality predicate.

libs/base/Data/String.idr+4−4

@@ -86,11 +86,11 @@ parseDouble = mkDouble . wfe . trim

8686 do

8787 w <- cast <$> parseInteger whole

8888 e <- parseInteger exp

89− return (w, 0, e)

89+ pure (w, 0, e)

9090 (whole::[]) =>

9191 do

9292 w <- cast <$> parseInteger whole

93− return (w, 0, 0)

93+ pure (w, 0, 0)

9494 _ => Nothing

9595 (whole::fracAndExp::[]) =>

9696 case split (\c => c == 'e' || c == 'E') fracAndExp of

@@ -101,12 +101,12 @@ parseDouble = mkDouble . wfe . trim

101101 f <- (/ (pow 10 (length frac))) <$>

102102 (cast <$> parseNumWithoutSign (unpack frac) 0)

103103 e <- parseInteger exp

104− return (w, if w < 0 then (-f) else f, e)

104+ pure (w, if w < 0 then (-f) else f, e)

105105 (frac::[]) =>

106106 do

107107 w <- cast <$> parseInteger whole

108108 f <- (/ (pow 10 (length frac))) <$>

109109 (cast <$> parseNumWithoutSign (unpack frac) 0)

110− return (w, if w < 0 then (-f) else f, 0)

110+ pure (w, if w < 0 then (-f) else f, 0)

111111 _ => Nothing

112112 _ => Nothing

libs/base/Debug/Trace.idr+1−1

@@ -5,6 +5,6 @@ module Debug.Trace

55||| @ result the final result

66export

77trace : (msg : String) -> (result : a) -> a

8−trace x val = unsafePerformIO {ffi=FFI_C} (do putStrLn x; return val)

8+trace x val = unsafePerformIO {ffi=FFI_C} (do putStrLn x; pure val)

99

1010

libs/base/System.idr+4−4

@@ -22,14 +22,14 @@ getEnv key = do

2222setEnv : String -> String -> IO Bool

2323setEnv key value = do

2424 ok <- foreign FFI_C "setenv" (String -> String -> Int -> IO Int) key value 1

25− return (ok == 0)

25+ pure (ok == 0)

2626

2727||| Unsets an environment variable.

2828||| Returns true if the variable was able to be unset.

2929unsetEnv : String -> IO Bool

3030unsetEnv key = do

3131 ok <- foreign FFI_C "unsetenv" (String -> IO Int) key

32− return (ok == 0)

32+ pure (ok == 0)

3333

3434getEnvironment : IO (List (String, String))

3535getEnvironment = getAllPairs 0 []

@@ -49,7 +49,7 @@ getEnvironment = getAllPairs 0 []

4949 envPair <- getEnvPair n

5050 is_nil <- nullStr envPair

5151 if is_nil

52− then return $ reverse $ map splitEq acc

52+ then pure $ reverse $ map splitEq acc

5353 else getAllPairs (n + 1) (envPair :: acc)

5454

5555||| Quit with a particular exit code

@@ -59,7 +59,7 @@ exit code = foreign FFI_C "exit" (Int -> IO ()) code

5959||| Get the numbers of seconds since 1st January 1970, 00:00 UTC

6060time : IO Integer

6161time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))

62− return t

62+ pure t

6363

6464usleep : Int -> IO ()

6565usleep i = foreign FFI_C "usleep" (Int -> IO ()) i

libs/base/System/Concurrency/Raw.idr+5−5

@@ -21,7 +21,7 @@ checkMsgs : IO Bool

2121checkMsgs = do msgs <- foreign FFI_C "idris_checkMessages" (Ptr -> IO Ptr)

2222 prim__vm

2323 null <- nullPtr msgs

24− return (not null)

24+ pure (not null)

2525

2626||| Check for messages in the process inbox

2727||| If no messages, waits for the given number of seconds

@@ -30,7 +30,7 @@ checkMsgsTimeout timeout

3030 = do msgs <- foreign FFI_C "idris_checkMessagesTimeout"

3131 (Ptr -> Int -> IO Ptr) prim__vm timeout

3232 null <- nullPtr msgs

33− return (not null)

33+ pure (not null)

3434

3535private

3636sender : Ptr -> IO Ptr

@@ -59,7 +59,7 @@ checkMsgsFrom sender channel

5959 = do msgs <- foreign FFI_C "idris_checkMessagesFrom" (Ptr -> Int -> Ptr -> IO Ptr)

6060 prim__vm channel sender

6161 null <- nullPtr msgs

62− return (not null)

62+ pure (not null)

6363

6464||| Check inbox for messages. If there are none, blocks until a message

6565||| arrives.

@@ -69,7 +69,7 @@ getMsg : IO a

6969getMsg {a} = do m <- foreign FFI_C "idris_recvMessage"

7070 (Ptr -> IO Ptr) prim__vm

7171 MkRaw x <- foreign FFI_C "idris_getMsg" (Ptr -> IO (Raw a)) m

72− return x

72+ pure x

7373

7474||| Check inbox for messages. If there are none, blocks until a message

7575||| arrives. Return triple of sender's ID, channel ID, and the message.

@@ -83,7 +83,7 @@ getMsgWithSender {a}

8383 vm <- sender m

8484 chan <- channel_id m

8585 foreign FFI_C "idris_freeMsg" (Ptr -> IO ()) m

86− return (vm, chan, x)

86+ pure (vm, chan, x)

8787

8888||| Check inbox for messages on a particular channel. If there are none,

8989||| blocks until a message arrives. Returns `Nothing` if the sender isn't

libs/contrib/CFFI/Memory.idr+9−9

@@ -33,7 +33,7 @@ mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr

3333

3434||| Allocate enough memory to hold an instance of a C typr

3535alloc : Composite -> IO CPtr

36−alloc t = return $ CPt !(calloc 1 (sizeOf t)) 0

36+alloc t = pure $ CPt !(calloc 1 (sizeOf t)) 0

3737

3838||| Free memory allocated with alloc

3939free : CPtr -> IO ()

@@ -63,24 +63,24 @@ peek PTR (CPt p o) = prim_peekPtr p o

6363||| Write to memory

6464poke : (t : CType) -> CPtr -> translate t -> IO ()

6565poke I8 (CPt p o) x = do _ <- prim_poke8 p o x

66− return ()

66+ pure ()

6767poke I16 (CPt p o) x = do _ <- prim_poke16 p o x

68− return ()

68+ pure ()

6969poke I32 (CPt p o) x = do _ <- prim_poke32 p o x

70− return ()

70+ pure ()

7171poke I64 (CPt p o) x = do _ <- prim_poke64 p o x

72− return ()

72+ pure ()

7373poke PTR (CPt p o) x = do _ <- prim_pokePtr p o x

74− return ()

74+ pure ()

7575poke FLOAT (CPt p o) x = do _ <- prim_pokeSingle p o x

76− return ()

76+ pure ()

7777poke DOUBLE (CPt p o) x = do _ <- prim_pokeDouble p o x

78− return ()

78+ pure ()

7979

8080||| Update memory with a function.

8181update : (t: CType) -> CPtr -> (translate t -> translate t) -> IO ()

8282update ty cp f = do val <- peek ty cp

83− out <- return $ f val

83+ out <- pure $ f val

8484 poke ty cp out

8585

8686||| Get a pointer to a field in a composite value

libs/contrib/Data/Heap.idr+1−1

@@ -173,5 +173,5 @@ main = do

173173 _ <- printLn $ main.sort [10, 3, 7, 2, 9, 1, 8, 0, 6, 4, 5]

174174 _ <- printLn $ main.sort ["orange", "apple", "pear", "lime", "durian"]

175175 _ <- printLn $ main.sort [("jim", 19, "cs"), ("alice", 20, "english"), ("bob", 50, "engineering")]

176− return ()

176+ pure ()

177177-}

libs/contrib/Data/Storable.idr+4−4

@@ -14,7 +14,7 @@ Storable Bits8 where

1414 peek p offset = prim_peek8 p offset

1515 poke p offset val = do

1616 _ <- prim_poke8 p offset val

17− return ()

17+ pure ()

1818

1919Storable Bits16 where

2020 sizeOf _ = 2

@@ -22,7 +22,7 @@ Storable Bits16 where

2222 peek p offset = prim_peek16 p offset

2323 poke p offset val = do

2424 _ <- prim_poke16 p offset val

25− return ()

25+ pure ()

2626

2727Storable Bits32 where

2828 sizeOf _ = 4

@@ -30,7 +30,7 @@ Storable Bits32 where

3030 peek p offset = prim_peek32 p offset

3131 poke p offset val = do

3232 _ <- prim_poke32 p offset val

33− return ()

33+ pure ()

3434

3535Storable Bits64 where

3636 sizeOf _ = 8

@@ -38,4 +38,4 @@ Storable Bits64 where

3838 peek p offset = prim_peek64 p offset

3939 poke p offset val = do

4040 _ <- prim_poke64 p offset val

41− return ()

41+ pure ()

libs/contrib/Interfaces/Verified.idr+2−2

@@ -35,8 +35,8 @@ interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) w

3535 mf <*> mx = mf >>= \f =>

3636 mx >>= \x =>

3737 pure (f x)

38− monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x

39− monadRightIdentity : (mx : m a) -> mx >>= Monad.return = mx

38+ monadLeftIdentity : (x : a) -> (f : a -> m b) -> pure x >>= f = f x

39+ monadRightIdentity : (mx : m a) -> mx >>= pure = mx

4040 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->

4141 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)

4242

libs/contrib/Network/Cgi.idr+15−15

@@ -32,29 +32,29 @@ getAction (MkCGI act) = act

3232

3333implementation Functor CGI where

3434 map f (MkCGI c) = MkCGI (\s => do (a, i) <- c s

35− return (f a, i))

35+ pure (f a, i))

3636

3737implementation Applicative CGI where

38− pure v = MkCGI (\s => return (v, s))

38+ pure v = MkCGI (\s => pure (v, s))

3939

4040 (MkCGI a) <*> (MkCGI b) = MkCGI (\s => do (f, i) <- a s

4141 (c, j) <- b i

42− return (f c, j))

42+ pure (f c, j))

4343

4444implementation Monad CGI where

4545 (>>=) (MkCGI f) k = MkCGI (\s => do v <- f s

4646 getAction (k (fst v)) (snd v))

4747

4848setInfo : CGIInfo -> CGI ()

49−setInfo i = MkCGI (\s => return ((), i))

49+setInfo i = MkCGI (\s => pure ((), i))

5050

5151getInfo : CGI CGIInfo

52−getInfo = MkCGI (\s => return (s, s))

52+getInfo = MkCGI (\s => pure (s, s))

5353

5454export

5555lift : IO a -> CGI a

5656lift op = MkCGI (\st => do { x <- op

57− return (x, st) } )

57+ pure (x, st) } )

5858

5959export

6060output : String -> CGI ()

@@ -64,30 +64,30 @@ output s = do i <- getInfo

6464export

6565queryVars : CGI Vars

6666queryVars = do i <- getInfo

67− return (GET i)

67+ pure (GET i)

6868

6969export

7070postVars : CGI Vars

7171postVars = do i <- getInfo

72− return (POST i)

72+ pure (POST i)

7373

7474export

7575cookieVars : CGI Vars

7676cookieVars = do i <- getInfo

77− return (Cookies i)

77+ pure (Cookies i)

7878

7979export

8080queryVar : String -> CGI (Maybe String)

8181queryVar x = do vs <- queryVars

82− return (lookup x vs)

82+ pure (lookup x vs)

8383

8484getOutput : CGI String

8585getOutput = do i <- getInfo

86− return (Output i)

86+ pure (Output i)

8787

8888getHeaders : CGI String

8989getHeaders = do i <- getInfo

90− return (Headers i)

90+ pure (Headers i)

9191

9292export

9393flushHeaders : CGI ()

@@ -110,14 +110,14 @@ getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)

110110getContent : Int -> IO String

111111getContent x = getC (cast x) "" where

112112 getC : Nat -> String -> IO String

113− getC Z acc = return $ reverse acc

113+ getC Z acc = pure $ reverse acc

114114 getC (S k) acc = do x <- getChar

115115 getC k (strCons x acc)

116116

117117getCgiEnv : String -> IO String

118118getCgiEnv key = do

119119 val <- getEnv key

120− return $ maybe "" id val

120+ pure $ maybe "" id val

121121

122122export

123123runCGI : CGI a -> IO a

@@ -138,6 +138,6 @@ runCGI prog = do

138138 "")

139139 putStrLn (Headers st)

140140 putStr (Output st)

141− return v

141+ pure v

142142

143143

libs/contrib/Network/Socket.idr+19−19

@@ -219,7 +219,7 @@ socket sf st pn = do

219219

220220 if socket_res == -1

221221 then map Left getErrno

222− else return $ Right (MkSocket socket_res sf st pn)

222+ else pure $ Right (MkSocket socket_res sf st pn)

223223

224224||| Close a socket

225225export

@@ -245,7 +245,7 @@ bind sock addr port = do

245245 (toCode $ socketType sock) (saString addr) port

246246 if bind_res == (-1)

247247 then getErrno

248− else return 0

248+ else pure 0

249249

250250||| Connects to a given address and port.

251251||| Returns 0 on success, and an error number on error.

@@ -261,7 +261,7 @@ connect sock addr port = do

261261

262262 if conn_res == (-1)

263263 then getErrno

264− else return 0

264+ else pure 0

265265

266266||| Listens on a bound socket.

267267|||

@@ -273,7 +273,7 @@ listen sock = do

273273 (descriptor sock) BACKLOG

274274 if listen_res == (-1)

275275 then getErrno

276− else return 0

276+ else pure 0

277277

278278||| Parses a textual representation of an IPv4 address into a SocketAddress

279279parseIPv4 : String -> SocketAddress

@@ -305,9 +305,9 @@ getSockAddr (SAPtr ptr) = do

305305 (Ptr -> IO String)

306306 ptr

307307

308− return $ parseIPv4 ipv4_addr

309− Just AF_INET6 => return IPv6Addr

310− Just AF_UNSPEC => return InvalidAddress)

308+ pure $ parseIPv4 ipv4_addr

309+ Just AF_INET6 => pure IPv6Addr

310+ Just AF_UNSPEC => pure InvalidAddress)

311311

312312||| Accept a connection on the provided socket.

313313|||

@@ -337,7 +337,7 @@ accept sock = do

337337 let (MkSocket _ fam ty p_num) = sock

338338 sockaddr <- getSockAddr (SAPtr sockaddr_ptr)

339339 sockaddr_free (SAPtr sockaddr_ptr)

340− return $ Right ((MkSocket accept_res fam ty p_num), sockaddr)

340+ pure $ Right ((MkSocket accept_res fam ty p_num), sockaddr)

341341

342342||| Send data on the specified socket.

343343|||

@@ -357,7 +357,7 @@ send sock dat = do

357357

358358 if send_res == (-1)

359359 then map Left getErrno

360− else return $ Right send_res

360+ else pure $ Right send_res

361361

362362freeRecvStruct : RecvStructPtr -> IO ()

363363freeRecvStruct (RSPtr p) =

@@ -400,18 +400,18 @@ recv sock len = do

400400 then do

401401 errno <- getErrno

402402 freeRecvStruct (RSPtr recv_struct_ptr)

403− return $ Left errno

403+ pure $ Left errno

404404 else

405405 if recv_res == 0

406406 then do

407407 freeRecvStruct (RSPtr recv_struct_ptr)

408− return $ Left 0

408+ pure $ Left 0

409409 else do

410410 payload <- foreign FFI_C "idrnet_get_recv_payload"

411411 (Ptr -> IO String)

412412 recv_struct_ptr

413413 freeRecvStruct (RSPtr recv_struct_ptr)

414− return $ Right (payload, recv_res)

414+ pure $ Right (payload, recv_res)

415415

416416||| Sends the data in a given memory location

417417|||

@@ -432,7 +432,7 @@ sendBuf sock (BPtr ptr) len = do

432432

433433 if send_res == (-1)

434434 then map Left getErrno

435− else return $ Right send_res

435+ else pure $ Right send_res

436436

437437||| Receive data from a given memory location.

438438|||

@@ -453,7 +453,7 @@ recvBuf sock (BPtr ptr) len = do

453453

454454 if (recv_res == (-1))

455455 then map Left getErrno

456− else return $ Right recv_res

456+ else pure $ Right recv_res

457457

458458||| Send a message.

459459|||

@@ -477,7 +477,7 @@ sendTo sock addr p dat = do

477477

478478 if sendto_res == (-1)

479479 then map Left getErrno

480− else return $ Right sendto_res

480+ else pure $ Right sendto_res

481481

482482||| Send a message stored in some buffer.

483483|||

@@ -502,7 +502,7 @@ sendToBuf sock addr p (BPtr dat) len = do

502502

503503 if sendto_res == (-1)

504504 then map Left getErrno

505− else return $ Right sendto_res

505+ else pure $ Right sendto_res

506506

507507||| Utility function to get the payload of the sent message as a `String`.

508508foreignGetRecvfromPayload : RecvfromStructPtr -> IO String

@@ -528,7 +528,7 @@ foreignGetRecvfromPort (RFPtr p) = do

528528 port <- foreign FFI_C "idrnet_sockaddr_ipv4_port"

529529 (Ptr -> IO Int)

530530 sockaddr_ptr

531− return port

531+ pure port

532532

533533

534534||| Receive a message.

@@ -568,7 +568,7 @@ recvFrom sock bl = do

568568 port <- foreignGetRecvfromPort recv_ptr'

569569 addr <- foreignGetRecvfromAddr recv_ptr'

570570 freeRecvfromStruct recv_ptr'

571− return $ Right (MkUDPAddrInfo addr port, payload, result)

571+ pure $ Right (MkUDPAddrInfo addr port, payload, result)

572572

573573||| Receive a message placed on a 'known' buffer.

574574|||

@@ -606,6 +606,6 @@ recvFromBuf sock (BPtr ptr) bl = do

606606 port <- foreignGetRecvfromPort recv_ptr'

607607 addr <- foreignGetRecvfromAddr recv_ptr'

608608 freeRecvfromStruct recv_ptr'

609− return $ Right (MkUDPAddrInfo addr port, result + 1)

609+ pure $ Right (MkUDPAddrInfo addr port, result + 1)

610610

611611-- --------------------------------------------------------------------- [ EOF ]

libs/contrib/System/Concurrency/Process.idr+6−6

@@ -18,7 +18,7 @@ implementation Functor (Process msg) where

1818 map f (Lift a) = Lift (map f a)

1919

2020implementation Applicative (Process msg) where

21− pure = Lift . return

21+ pure = Lift . pure

2222 (Lift f) <*> (Lift a) = Lift (f <*> a)

2323

2424implementation Monad (Process msg) where

@@ -32,14 +32,14 @@ run (Lift prog) = prog

3232||| Get current process ID

3333export

3434myID : Process msg (ProcID msg)

35−myID = Lift (return (MkPID prim__vm))

35+myID = Lift (pure (MkPID prim__vm))

3636

3737||| Send a message to another process

3838||| Returns whether the send was unsuccessful.

3939export

4040send : ProcID msg -> msg -> Process msg Bool

4141send (MkPID p) m = Lift (do x <- sendToThread p 0 (prim__vm, m)

42− return (x /= 0))

42+ pure (x /= 0))

4343

4444||| Return whether a message is waiting in the queue

4545export

@@ -55,7 +55,7 @@ msgWaitingFrom (MkPID p) = Lift (checkMsgsFrom p 0)

5555export

5656recv : Process msg msg

5757recv {msg} = do (senderid, m) <- Lift get

58− return m

58+ pure m

5959 where get : IO (Ptr, msg)

6060 get = getMsg

6161

@@ -74,11 +74,11 @@ export

7474recvWithSender : Process msg (ProcID msg, msg)

7575recvWithSender {msg}

7676 = do (senderid, m) <- Lift get

77− return (MkPID senderid, m)

77+ pure (MkPID senderid, m)

7878 where get : IO (Ptr, msg)

7979 get = getMsg

8080

8181export

8282create : Process msg () -> Process msg (ProcID msg)

8383create (Lift p) = do ptr <- Lift (fork p)

84− return (MkPID ptr)

84+ pure (MkPID ptr)

libs/effects/Effect/Memory.idr+5−5

@@ -45,7 +45,7 @@ do_malloc size with (fromInteger (cast size) == size)

4545 | True = do ptr <- ioe_lift $ foreign FFI_C "malloc" (Int -> IO Ptr) (fromInteger $ cast size)

4646 fail <- ioe_lift $ nullPtr ptr

4747 if fail then ioe_fail "Cannot allocate memory"

48− else return ptr

48+ else pure ptr

4949 | False = ioe_fail "The target architecture does not support adressing enough memory"

5050

5151private

@@ -66,15 +66,15 @@ do_memmove dest src dest_offset src_offset size

6666

6767private

6868do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect size Bits8)

69−do_peek _ _ Z = return (Vect.Nil)

69+do_peek _ _ Z = pure (Vect.Nil)

7070do_peek ptr offset (S n)

7171 = do b <- foreign FFI_C "idris_peek" (Ptr -> Int -> IO Bits8) ptr (fromInteger $ cast offset)

7272 bs <- do_peek ptr (S offset) n

73− Monad.return (Vect.(::) b bs)

73+ Applicative.pure (Vect.(::) b bs)

7474

7575private

7676do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()

77−do_poke _ _ [] = return ()

77+do_poke _ _ [] = pure ()

7878do_poke ptr offset (b::bs)

7979 = do foreign FFI_C "idris_poke" (Ptr -> Int -> Bits8 -> IO ()) ptr (fromInteger $ cast offset) b

8080 do_poke ptr (S offset) bs

@@ -179,5 +179,5 @@ move : {dst_size : Nat} ->

179179move dst_offset src_offset size dst_bounds src_bounds

180180 = do src_ptr <- Src :- getRawPtr

181181 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

182− return ()

182+ pure ()

183183

libs/effects/Effect/Perf.idr+1−1

@@ -106,7 +106,7 @@ perfLog : PMetrics -> String -> IO ()

106106perfLog res msg =

107107 if livePerf res

108108 then putStrLn $ unwords ["PERF:", msg]

109− else return ()

109+ else pure ()

110110

111111-- ------------------------------------------------------- [ Effect Definition ]

112112

libs/effects/Effect/Random.idr+5−5

@@ -21,14 +21,14 @@ RND = MkEff Integer Random

2121||| Generates a random Integer in a given range

2222rndInt : Integer -> Integer -> Eff Integer [RND]

2323rndInt lower upper = do v <- call $ GetRandom

24− return ((v `prim__sremBigInt` (upper - lower)) + lower)

24+ pure ((v `prim__sremBigInt` (upper - lower)) + lower)

2525

2626||| Generate a random number in Fin (S `k`)

2727|||

2828||| Note that rndFin k takes values 0, 1, ..., k.

2929rndFin : (k : Nat) -> Eff (Fin (S k)) [RND]

3030rndFin k = do let v = assert_total $ !(call GetRandom) `prim__sremBigInt` (cast (S k))

31− return (toFin v)

31+ pure (toFin v)

3232 where toFin : Integer -> Fin (S k)

3333 toFin x = case integerToFin x (S k) of

3434 Just v => v

@@ -36,12 +36,12 @@ rndFin k = do let v = assert_total $ !(call GetRandom) `prim__sremBigInt` (cast

3636

3737||| Select a random element from a vector

3838rndSelect' : Vect (S k) a -> Eff a [RND]

39−rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)

39+rndSelect' {k} xs = pure (Vect.index !(rndFin k) xs)

4040

4141||| Select a random element from a list, or Nothing if the list is empty

4242rndSelect : List a -> Eff (Maybe a) [RND]

43−rndSelect [] = return Nothing

44−rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

43+rndSelect [] = pure Nothing

44+rndSelect (x::xs) = pure (Just !(rndSelect' (x::(fromList xs))))

4545

4646||| Sets the random seed

4747srand : Integer -> Eff () [RND]

libs/effects/Effect/State.idr+1−1

@@ -36,5 +36,5 @@ locally newst prog = do st <- get

3636 putM newst

3737 val <- prog

3838 putM st

39− return val

39+ pure val

4040

libs/effects/Effects.idr+6−6

@@ -303,16 +303,16 @@ staticEff = id

303303toEff : .(xs' : List EFFECT) -> EffM m a xs (\v => xs') -> EffM m a xs (\v => xs')

304304toEff xs' = id

305305

306−return : a -> EffM m a xs (\v => xs)

307−return x = Value x

308−

309−-- ------------------------------------------------------ [ for idiom brackets ]

310−

311306infixl 2 <*>

312307

313308pure : a -> EffM m a xs (\v => xs)

314309pure = Value

315310

311+return : a -> EffM m a xs (\v => xs)

312+return = pure

313+

314+%deprecate Effects.return "Please use `pure`."

315+

316316pureM : (val : a) -> EffM m a (xs val) xs

317317pureM = Value

318318

@@ -320,7 +320,7 @@ pureM = Value

320320 EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)

321321(<*>) prog v = do fn <- prog

322322 arg <- v

323− return (fn arg)

323+ pure (fn arg)

324324

325325(<$>) : (a -> b) ->

326326 EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)

libs/oldeffects/Effect/Exception.idr+1−1

@@ -18,7 +18,7 @@ instance Show a => Handler (Exception a) IO where

1818 believe_me (exit 1)

1919

2020instance Handler (Exception a) (IOExcept a) where

21− handle _ (Raise e) k = ioM (return (Left e))

21+ handle _ (Raise e) k = ioM (pure (Left e))

2222

2323instance Handler (Exception a) (Either a) where

2424 handle _ (Raise e) k = Left e

libs/oldeffects/Effect/Memory.idr+5−5

@@ -43,7 +43,7 @@ do_malloc size with (fromInteger (cast size) == size)

4343 | True = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt] FPtr) (fromInteger $ cast size)

4444 fail <- ioe_lift $ nullPtr ptr

4545 if fail then ioe_fail "Cannot allocate memory"

46− else return ptr

46+ else pure ptr

4747 | False = ioe_fail "The target architecture does not support adressing enough memory"

4848

4949private

@@ -64,15 +64,15 @@ do_memmove dest src dest_offset src_offset size

6464

6565private

6666do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect size Bits8)

67−do_peek _ _ Z = return (Prelude.Vect.Nil)

67+do_peek _ _ Z = pure (Prelude.Vect.Nil)

6868do_peek ptr offset (S n)

6969 = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)

7070 bs <- do_peek ptr (S offset) n

71− Prelude.Monad.return (Prelude.Vect.(::) b bs)

71+ Prelude.Applicative.pure (Prelude.Vect.(::) b bs)

7272

7373private

7474do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()

75−do_poke _ _ [] = return ()

75+do_poke _ _ [] = pure ()

7676do_poke ptr offset (b::bs)

7777 = do mkForeign (FFun "idris_poke" [FPtr, FInt, FByte] FUnit) ptr (fromInteger $ cast offset) b

7878 do_poke ptr (S offset) bs

@@ -171,5 +171,5 @@ move : {dst_size : Nat} ->

171171move dst_offset src_offset size dst_bounds src_bounds

172172 = do src_ptr <- Src :- getRawPtr

173173 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

174− return ()

174+ pure ()

175175

libs/oldeffects/Effect/Random.idr+5−5

@@ -19,14 +19,14 @@ RND = MkEff Integer Random

1919||| Generates a random Integer in a given range

2020rndInt : Integer -> Integer -> { [RND] } Eff m Integer

2121rndInt lower upper = do v <- call $ getRandom

22− return (v `prim__sremBigInt` (upper - lower) + lower)

22+ pure (v `prim__sremBigInt` (upper - lower) + lower)

2323

2424||| Generate a random number in Fin (S `k`)

2525|||

2626||| Note that rndFin k takes values 0, 1, ..., k.

2727rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))

2828rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))

29− return (toFin v)

29+ pure (toFin v)

3030 where toFin : Integer -> Fin (S k)

3131 toFin x = case integerToFin x (S k) of

3232 Just v => v

@@ -34,12 +34,12 @@ rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast

3434

3535||| Select a random element from a vector

3636rndSelect' : Vect (S k) a -> { [RND] } Eff IO a

37−rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)

37+rndSelect' {k} xs = pure (Vect.index !(rndFin k) xs)

3838

3939||| Select a random element from a list, or Nothing if the list is empty

4040rndSelect : List a -> { [RND] } Eff IO (Maybe a)

41−rndSelect [] = return Nothing

42−rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

41+rndSelect [] = pure Nothing

42+rndSelect (x::xs) = pure (Just !(rndSelect' (x::(fromList xs))))

4343

4444||| Sets the random seed

4545srand : Integer -> { [RND] } Eff m ()

libs/oldeffects/Effect/State.idr+1−1

@@ -36,5 +36,5 @@ locally newst prog = do st <- get

3636 putM newst

3737 val <- prog

3838 putM st

39− return val

39+ pure val

4040

libs/prelude/IO.idr+26−26

@@ -98,8 +98,8 @@ prim_io_bind (Prim__IO v) k = k v

9898unsafePerformPrimIO : PrimIO a -> a

9999-- compiled as primitive

100100

101−prim_io_return : a -> PrimIO a

102−prim_io_return x = Prim__IO x

101+prim_io_pure : a -> PrimIO a

102+prim_io_pure x = Prim__IO x

103103

104104io_bind : IO' l a -> (a -> IO' l b) -> IO' l b

105105io_bind (MkIO fn) k

@@ -107,8 +107,8 @@ io_bind (MkIO fn) k

107107 (\ b => case k b of

108108 MkIO fkb => fkb w))

109109

110−io_return : a -> IO' l a

111−io_return x = MkIO (\w => prim_io_return x)

110+io_pure : a -> IO' l a

111+io_pure x = MkIO (\w => prim_io_pure x)

112112

113113liftPrimIO : (World -> PrimIO a) -> IO' l a

114114liftPrimIO = MkIO

@@ -122,21 +122,21 @@ run__IO f = call__IO f

122122

123123unsafePerformIO : IO' ffi a -> a

124124unsafePerformIO (MkIO f) = unsafePerformPrimIO

125− (prim_io_bind (f (TheWorld prim__TheWorld)) (\ b => prim_io_return b))

125+ (prim_io_bind (f (TheWorld prim__TheWorld)) (\ b => prim_io_pure b))

126126

127127prim_read : IO' l String

128−prim_read = MkIO (\w => prim_io_return (prim__readString (world w)))

128+prim_read = MkIO (\w => prim_io_pure (prim__readString (world w)))

129129

130130prim_write : String -> IO' l Int

131131prim_write s

132− = MkIO (\w => prim_io_return (prim__writeString (world w) s))

132+ = MkIO (\w => prim_io_pure (prim__writeString (world w) s))

133133

134134prim_fread : Ptr -> IO' l String

135−prim_fread h = MkIO (\w => prim_io_return (prim__readFile (world w) h))

135+prim_fread h = MkIO (\w => prim_io_pure (prim__readFile (world w) h))

136136

137137prim_fwrite : Ptr -> String -> IO' l Int

138138prim_fwrite h s

139− = MkIO (\w => prim_io_return (prim__writeFile (world w) h s))

139+ = MkIO (\w => prim_io_pure (prim__writeFile (world w) h s))

140140

141141--------- The C FFI

142142namespace FFI_C

@@ -205,14 +205,14 @@ run__provider : IO a -> PrimIO a

205205run__provider (MkIO f) = f (TheWorld prim__TheWorld)

206206

207207prim_fork : PrimIO () -> PrimIO Ptr

208−prim_fork x = prim_io_return prim__vm -- compiled specially

208+prim_fork x = prim_io_pure prim__vm -- compiled specially

209209

210210namespace IO

211211 fork : IO' l () -> IO' l Ptr

212212 fork (MkIO f) = MkIO (\w => prim_io_bind

213213 (prim_fork (prim_io_bind (f w)

214− (\ x => prim_io_return x)))

215− (\x => prim_io_return x))

214+ (\ x => prim_io_pure x)))

215+ (\x => prim_io_pure x))

216216

217217 forceGC : IO ()

218218 forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm

@@ -316,52 +316,52 @@ namespace FFI_Export

316316

317317-- Accessing memory

318318prim_peek8 : Ptr -> Int -> IO Bits8

319−prim_peek8 ptr offset = MkIO (\w => prim_io_return (prim__peek8 (world w) ptr offset))

319+prim_peek8 ptr offset = MkIO (\w => prim_io_pure (prim__peek8 (world w) ptr offset))

320320

321321prim_poke8 : Ptr -> Int -> Bits8 -> IO Int

322−prim_poke8 ptr offset val = MkIO (\w => prim_io_return (

322+prim_poke8 ptr offset val = MkIO (\w => prim_io_pure (

323323 prim__poke8 (world w) ptr offset val))

324324

325325prim_peek16 : Ptr -> Int -> IO Bits16

326−prim_peek16 ptr offset = MkIO (\w => prim_io_return (prim__peek16 (world w) ptr offset))

326+prim_peek16 ptr offset = MkIO (\w => prim_io_pure (prim__peek16 (world w) ptr offset))

327327

328328prim_poke16 : Ptr -> Int -> Bits16 -> IO Int

329−prim_poke16 ptr offset val = MkIO (\w => prim_io_return (

329+prim_poke16 ptr offset val = MkIO (\w => prim_io_pure (

330330 prim__poke16 (world w) ptr offset val))

331331

332332prim_peek32 : Ptr -> Int -> IO Bits32

333−prim_peek32 ptr offset = MkIO (\w => prim_io_return (prim__peek32 (world w) ptr offset))

333+prim_peek32 ptr offset = MkIO (\w => prim_io_pure (prim__peek32 (world w) ptr offset))

334334

335335prim_poke32 : Ptr -> Int -> Bits32 -> IO Int

336−prim_poke32 ptr offset val = MkIO (\w => prim_io_return (

336+prim_poke32 ptr offset val = MkIO (\w => prim_io_pure (

337337 prim__poke32 (world w) ptr offset val))

338338

339339prim_peek64 : Ptr -> Int -> IO Bits64

340−prim_peek64 ptr offset = MkIO (\w => prim_io_return (prim__peek64 (world w) ptr offset))

340+prim_peek64 ptr offset = MkIO (\w => prim_io_pure (prim__peek64 (world w) ptr offset))

341341

342342prim_poke64 : Ptr -> Int -> Bits64 -> IO Int

343−prim_poke64 ptr offset val = MkIO (\w => prim_io_return (

343+prim_poke64 ptr offset val = MkIO (\w => prim_io_pure (

344344 prim__poke64 (world w) ptr offset val))

345345

346346prim_peekPtr : Ptr -> Int -> IO Ptr

347−prim_peekPtr ptr offset = MkIO (\w => prim_io_return (prim__peekPtr (world w) ptr offset))

347+prim_peekPtr ptr offset = MkIO (\w => prim_io_pure (prim__peekPtr (world w) ptr offset))

348348

349349prim_pokePtr : Ptr -> Int -> Ptr -> IO Int

350−prim_pokePtr ptr offset val = MkIO (\w => prim_io_return (

350+prim_pokePtr ptr offset val = MkIO (\w => prim_io_pure (

351351 prim__pokePtr (world w) ptr offset val))

352352

353353prim_peekDouble : Ptr -> Int -> IO Double

354−prim_peekDouble ptr offset = MkIO (\w => prim_io_return (prim__peekDouble (world w) ptr offset))

354+prim_peekDouble ptr offset = MkIO (\w => prim_io_pure (prim__peekDouble (world w) ptr offset))

355355

356356prim_pokeDouble : Ptr -> Int -> Double -> IO Int

357−prim_pokeDouble ptr offset val = MkIO (\w => prim_io_return (

357+prim_pokeDouble ptr offset val = MkIO (\w => prim_io_pure (

358358 prim__pokeDouble (world w) ptr offset val))

359359

360360||| Single precision floats are marshalled to Doubles

361361prim_peekSingle : Ptr -> Int -> IO Double

362−prim_peekSingle ptr offset = MkIO (\w => prim_io_return (prim__peekSingle (world w) ptr offset))

362+prim_peekSingle ptr offset = MkIO (\w => prim_io_pure (prim__peekSingle (world w) ptr offset))

363363

364364||| Single precision floats are marshalled to Doubles

365365prim_pokeSingle : Ptr -> Int -> Double -> IO Int

366−prim_pokeSingle ptr offset val = MkIO (\w => prim_io_return (

366+prim_pokeSingle ptr offset val = MkIO (\w => prim_io_pure (

367367 prim__pokeSingle (world w) ptr offset val))

libs/prelude/Language/Reflection/Elab.idr+4−4

@@ -253,7 +253,7 @@ namespace Tactics

253253 export

254254 lookupTyExact : TTName -> Elab (TTName, NameType, TT)

255255 lookupTyExact n = case !(lookupTy n) of

256− [res] => return res

256+ [res] => pure res

257257 [] => fail [NamePart n, TextPart "is not defined."]

258258 xs => fail [NamePart n, TextPart "is ambiguous."]

259259

@@ -269,7 +269,7 @@ namespace Tactics

269269 export

270270 lookupDatatypeExact : TTName -> Elab Datatype

271271 lookupDatatypeExact n = case !(lookupDatatype n) of

272− [res] => return res

272+ [res] => pure res

273273 [] => fail [TextPart "No datatype named", NamePart n]

274274 xs => fail [TextPart "More than one datatype named", NamePart n]

275275

@@ -285,7 +285,7 @@ namespace Tactics

285285 export

286286 lookupFunDefnExact : TTName -> Elab (FunDefn TT)

287287 lookupFunDefnExact n = case !(lookupFunDefn n) of

288− [res] => return res

288+ [res] => pure res

289289 [] => fail [TextPart "No function named", NamePart n]

290290 xs => fail [TextPart "More than one function named", NamePart n]

291291

@@ -299,7 +299,7 @@ namespace Tactics

299299 export

300300 lookupArgsExact : TTName -> Elab (TTName, List FunArg, Raw)

301301 lookupArgsExact n = case !(lookupArgs n) of

302− [res] => return res

302+ [res] => pure res

303303 [] => fail [NamePart n, TextPart "is not defined."]

304304 xs => fail [NamePart n, TextPart "is ambiguous."]

305305

libs/prelude/Prelude.idr+7−7

@@ -50,7 +50,7 @@ decAsBool (No _) = False

5050---- Functor implementations

5151

5252Functor PrimIO where

53− map f io = prim_io_bind io (prim_io_return . f)

53+ map f io = prim_io_bind io (prim_io_pure . f)

5454

5555Functor Maybe where

5656 map f (Just x) = Just (f x)

@@ -63,9 +63,9 @@ Functor (Either e) where

6363---- Applicative implementations

6464

6565Applicative PrimIO where

66− pure = prim_io_return

66+ pure = prim_io_pure

6767

68− am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))

68+ am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_pure . f))

6969

7070Applicative Maybe where

7171 pure = Just

@@ -252,19 +252,19 @@ namespace JSNull

252252 partial

253253 nullPtr : Ptr -> JS_IO Bool

254254 nullPtr p = do ok <- foreign FFI_JS "isNull" (Ptr -> JS_IO Int) p

255− return (ok /= 0)

255+ pure (ok /= 0)

256256

257257 ||| Check if a supposed string was actually a null pointer

258258 partial

259259 nullStr : String -> JS_IO Bool

260260 nullStr p = do ok <- foreign FFI_JS "isNull" (String -> JS_IO Int) p

261− return (ok /= 0)

261+ pure (ok /= 0)

262262

263263

264264||| Pointer equality

265265eqPtr : Ptr -> Ptr -> IO Bool

266266eqPtr x y = do eq <- foreign FFI_C "idris_eqPtr" (Ptr -> Ptr -> IO Int) x y

267− return (eq /= 0)

267+ pure (eq /= 0)

268268

269269||| Loop while some test is true

270270|||

@@ -275,7 +275,7 @@ while : (test : IO' l Bool) -> (body : IO' l ()) -> IO' l ()

275275while t b = do v <- t

276276 if v then do b

277277 while t b

278− else return ()

278+ else pure ()

279279

280280------- Some error rewriting

281281

libs/prelude/Prelude/File.idr+26−26

@@ -42,7 +42,7 @@ strError err = unsafePerformIO -- yeah, yeah...

4242getFileError : IO FileError

4343getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"

4444 (Ptr -> IO (Raw FileError)) prim__vm

45− return err

45+ pure err

4646

4747Show FileError where

4848 show FileReadError = "File Read Error"

@@ -73,7 +73,7 @@ do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h

7373export

7474ferror : File -> IO Bool

7575ferror (FHandle h) = do err <- do_ferror h

76− return (not (err == 0))

76+ pure (not (err == 0))

7777

7878||| Call the RTS's file opening function

7979private

@@ -89,14 +89,14 @@ fopen : (f : String) -> (m : String) -> IO (Either FileError File)

8989fopen f m = do h <- do_fopen f m

9090 if !(nullPtr h)

9191 then do err <- getFileError

92− return (Left err)

93− else return (Right (FHandle h))

92+ pure (Left err)

93+ else pure (Right (FHandle h))

9494

9595||| Check whether a file handle is actually a null pointer

9696export

9797validFile : File -> IO Bool

9898validFile (FHandle h) = do x <- nullPtr h

99− return (not x)

99+ pure (not x)

100100

101101||| Modes for opening files

@@ -148,8 +148,8 @@ fileSize : File -> IO (Either FileError Int)

148148fileSize (FHandle h) = do s <- do_getFileSize h

149149 if (s < 0)

150150 then do err <- getFileError

151− return (Left err)

152− else return (Right s)

151+ pure (Left err)

152+ else pure (Right s)

153153

154154private

155155do_fread : Ptr -> IO' l String

@@ -159,8 +159,8 @@ export

159159fgetc : File -> IO (Either FileError Char)

160160fgetc (FHandle h) = do let c = cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h)

161161 if !(ferror (FHandle h))

162− then return (Left FileReadError)

163− else return (Right c)

162+ then pure (Left FileReadError)

163+ else pure (Right c)

164164

165165export

166166fflush : File -> IO ()

@@ -175,8 +175,8 @@ popen : String -> Mode -> IO (Either FileError File)

175175popen f m = do ptr <- do_popen f (modeStr m)

176176 if !(nullPtr ptr)

177177 then do err <- getFileError

178− return (Left err)

179− else return (Right (FHandle ptr))

178+ pure (Left err)

179+ else pure (Right (FHandle ptr))

180180

181181export

182182pclose : File -> IO ()

@@ -189,8 +189,8 @@ export

189189fread : File -> IO (Either FileError String)

190190fread (FHandle h) = do str <- do_fread h

191191 if !(ferror (FHandle h))

192− then return (Left FileReadError)

193− else return (Right str)

192+ then pure (Left FileReadError)

193+ else pure (Right str)

194194

195195||| Read a line from a file

196196||| @h a file handle which must be open for reading

@@ -206,10 +206,10 @@ do_fwrite h s = do res <- prim_fwrite h s

206206 if (res /= 0)

207207 then do errno <- getErrno

208208 if errno == 0

209− then return (Left FileWriteError)

209+ then pure (Left FileWriteError)

210210 else do err <- getFileError

211− return (Left err)

212− else return (Right ())

211+ pure (Left err)

212+ else pure (Right ())

213213

214214export

215215fwrite : File -> String -> IO (Either FileError ())

@@ -236,7 +236,7 @@ do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h

236236export

237237fEOF : File -> IO Bool

238238fEOF (FHandle h) = do eof <- do_feof h

239− return (not (eof == 0))

239+ pure (not (eof == 0))

240240

241241||| Check if a file handle has reached the end

242242export

@@ -248,7 +248,7 @@ feof = fEOF

248248export

249249fpoll : File -> IO Bool

250250fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h

251− return (p > 0)

251+ pure (p > 0)

252252

253253||| Read the contents of a file into a string

254254||| This checks the size of the file before beginning to read, and only

@@ -258,29 +258,29 @@ fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h

258258export

259259readFile : (filepath : String) -> IO (Either FileError String)

260260readFile fn = do Right h <- openFile fn Read

261− | Left err => return (Left err)

261+ | Left err => pure (Left err)

262262 Right max <- fileSize h

263− | Left err => return (Left err)

263+ | Left err => pure (Left err)

264264 c <- readFile' h max ""

265265 closeFile h

266− return c

266+ pure c

267267 where

268268 readFile' : File -> Int -> String -> IO (Either FileError String)

269269 readFile' h max contents =

270270 do x <- fEOF h

271271 if not x && max > 0

272272 then do Right l <- fGetLine h

273− | Left err => return (Left err)

273+ | Left err => pure (Left err)

274274 assert_total $

275275 readFile' h (max - cast (length l)) (contents ++ l)

276− else return (Right contents)

276+ else pure (Right contents)

277277

278278||| Write a string to a file

279279export

280280writeFile : (filepath : String) -> (contents : String) ->

281281 IO (Either FileError ())

282282writeFile fn contents = do

283− Right h <- openFile fn WriteTruncate | Left err => return (Left err)

284− Right () <- fPutStr h contents | Left err => return (Left err)

283+ Right h <- openFile fn WriteTruncate | Left err => pure (Left err)

284+ Right () <- fPutStr h contents | Left err => pure (Left err)

285285 closeFile h

286− return (Right ())

286+ pure (Right ())

libs/prelude/Prelude/Interactive.idr+4−4

@@ -29,7 +29,7 @@ import IO

2929||| descriptor

3030putStr' : String -> IO' ffi ()

3131putStr' x = do prim_write x

32− return ()

32+ pure ()

3333

3434||| Output a string to stdout without a trailing newline

3535putStr : String -> IO ()

@@ -66,7 +66,7 @@ printLn = printLn'

6666||| descriptor

6767getLine' : IO' ffi String

6868getLine' = do x <- prim_read

69− return (reverse (trimNL (reverse x)))

69+ pure (reverse (trimNL (reverse x)))

7070 where trimNL : String -> String

7171 trimNL str with (strM str)

7272 trimNL "" | StrNil = ""

@@ -103,7 +103,7 @@ getArgs = do n <- numArgs

103103

104104 partial

105105 ga' : List String -> Int -> Int -> IO (List String)

106− ga' acc i n = if (i == n) then (return $ reverse acc) else

106+ ga' acc i n = if (i == n) then (pure $ reverse acc) else

107107 do arg <- getArg i

108108 ga' (arg :: acc) (i+1) n

109109

@@ -155,7 +155,7 @@ replWith acc prompt fn

155155 case fn acc x of

156156 Just (out, acc') => do putStr out

157157 replWith acc' prompt fn

158− Nothing => return ()

158+ Nothing => pure ()

159159

160160||| A basic read-eval-print loop

161161||| @ prompt the prompt to show

libs/prelude/Prelude/Monad.idr+5−4

@@ -4,7 +4,7 @@ module Prelude.Monad

44

55import Builtins

66import Prelude.Functor

7−import Prelude.Applicative

7+import public Prelude.Applicative

88import Prelude.Basics

99import IO

1010

@@ -27,6 +27,7 @@ interface Applicative m => Monad (m : Type -> Type) where

2727||| define `return` and `pure` differently!

2828return : Monad m => a -> m a

2929return = pure

30+%deprecate return "Please use `pure`, which is equivalent."

3031

3132flatten : Monad m => m (m a) -> m a

3233flatten = join

@@ -36,13 +37,13 @@ flatten = join

3637-- Prelude modules other than the top level.

3738

3839Functor (IO' ffi) where

39− map f io = io_bind io (\b => io_return (f b))

40+ map f io = io_bind io (\b => io_pure (f b))

4041

4142Applicative (IO' ffi) where

42− pure x = io_return x

43+ pure x = io_pure x

4344 f <*> a = io_bind f (\f' =>

4445 io_bind a (\a' =>

45− io_return (f' a')))

46+ io_pure (f' a')))

4647

4748

4849Monad (IO' ffi) where

libs/prelude/Prelude/Strings.idr+2−2

@@ -358,10 +358,10 @@ isInfixOf a b = isInfixOf (unpack a) (unpack b)

358358partial

359359nullPtr : Ptr -> IO Bool

360360nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p

361− return (ok /= 0)

361+ pure (ok /= 0)

362362

363363||| Check if a supposed string was actually a null pointer

364364partial

365365nullStr : String -> IO Bool

366366nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p

367− return (ok /= 0)

367+ pure (ok /= 0)

libs/pruviloj/Pruviloj/Core.idr+8−8

@@ -87,7 +87,7 @@ newHole : (hint : String) -> (ty : Raw) -> Elab TTName

8787newHole hint ty =

8888 do hn <- gensym hint

8989 claim hn ty

90− return hn

90+ pure hn

9191

9292||| Use a term to solve a hole

9393|||

@@ -105,7 +105,7 @@ intros = do g <- snd <$> getGoal

105105 do n' <- nameFrom n

106106 intro n'

107107 (n' ::) <$> go body

108− go _ = return []

108+ go _ = pure []

109109

110110||| Run a tactic inside of a particular hole, if it still exists. If

111111||| it has been solved, do nothing.

@@ -113,7 +113,7 @@ inHole : TTName -> Elab a -> Elab (Maybe a)

113113inHole h todo =

114114 if (h `elem` !getHoles)

115115 then do focus h; Just <$> todo

116− else return Nothing

116+ else pure Nothing

117117

118118||| Restrict a polymorphic type to () for contexts where it doesn't

119119||| matter. This is nice for sticking `debug` in a context where

@@ -132,7 +132,7 @@ equiv newGoal =

132132 claim h newGoal

133133 fill (Var h); solve

134134 focus h

135− return h

135+ pure h

136136

137137||| Remember a term built with elaboration for later use. If the

138138||| current goal is `h`, then `remember n ty` puts a fresh hole at

@@ -149,14 +149,14 @@ remember n ty =

149149 claim todo ty

150150 letbind n ty (Var todo)

151151 focus todo

152− return todo

152+ pure todo

153153

154154||| Repeat a given tactic until it fails. Fails if the tactic fails on

155155||| the first attempt; succeeds otherwise.

156156repeatUntilFail : Elab () -> Elab ()

157157repeatUntilFail tac =

158158 do tac

159− repeatUntilFail tac <|> return ()

159+ repeatUntilFail tac <|> pure ()

160160

161161||| If the current goal is a pattern-bound variable, bind it with the

162162||| expected name. Otherwise fail.

@@ -181,7 +181,7 @@ total

181181inferType : (tac : Elab ()) -> Elab (TT, TT)

182182inferType tac =

183183 case fst !(runElab `(Infer) (do startInfer; tac)) of

184− `(MkInfer ~ty ~tm) => return (tm, ty)

184+ `(MkInfer ~ty ~tm) => pure (tm, ty)

185185 _ => fail [TextPart "Not infer"]

186186 where

187187 startInfer : Elab ()

@@ -219,7 +219,7 @@ refine tm =

219219 newHoles <- apply tm (replicate argCount True)

220220 solve

221221 actualHoles <- getHoles

222− return (filter (flip elem actualHoles) newHoles)

222+ pure (filter (flip elem actualHoles) newHoles)

223223

224224 where countPi : Raw -> Nat

225225 countPi (RBind _ (Pi _ _) body) = S (countPi body)

libs/pruviloj/Pruviloj/Derive/DecEq.idr+3−3

@@ -116,7 +116,7 @@ mkRhs fn fam k =

116116 focus a1; fill rTm1; solve

117117 focus a2; fill rTm2; solve

118118 focus dH; resolveTC fn

119− return (Var eq)

119+ pure (Var eq)

120120 matchCase tms

121121 _ => fail [TextPart "Inapplicable"]

122122

@@ -165,7 +165,7 @@ deriveDecEq fn =

165165 (a2 :: a1 :: rest) =>

166166 do (constrs, bindings) <- partitionM (\x => isConstr (binderTy (snd x)))

167167 (reverse rest)

168− return (bindings, constrs, a1, a2)

168+ pure (bindings, constrs, a1, a2)

169169 let todo = [(c1, c2) | c1 <- constructors datatype

170170 , c2 <- constructors datatype]

171171 clauses <- for todo

@@ -178,7 +178,7 @@ deriveDecEq fn =

178178 isConstr : Raw -> Elab Bool

179179 isConstr tm = case headName tm of

180180 Just n => isTCName n

181− Nothing => return False

181+ Nothing => pure False

182182

183183 partial -- mkRhs

184184 mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe (FunClause Raw))

libs/pruviloj/Pruviloj/Derive/Eliminators.idr+10−10

@@ -20,7 +20,7 @@ bindParams info = traverse_ (uncurry forall) (getParams info)

2020bindIndices : TyConInfo -> Elab Renamer

2121bindIndices info = bind' (getIndices info) noRenames

2222 where bind' : List (TTName, Raw) -> Renamer -> Elab Renamer

23− bind' [] ren = return ren

23+ bind' [] ren = pure ren

2424 bind' ((n, t) :: ixs) ren = do n' <- nameFrom n

2525 forall n' (alphaRaw ren t)

2626 bind' ixs (extend ren n n')

@@ -31,7 +31,7 @@ bindTarget : TyConInfo -> Elab (TTName, Renamer)

3131bindTarget info = do ren <- bindIndices info

3232 tn <- gensym "target"

3333 forall tn (alphaRaw ren $ result info)

34− return (tn, ren)

34+ pure (tn, ren)

3535

3636elabMotive : TyConInfo -> Elab ()

3737elabMotive info = do attack

@@ -75,7 +75,7 @@ mkIh info motiveName recArg argty fam =

7575 fill argTm; solve

7676 solve -- attack

7777 solve -- ihT

78− else return ()

78+ else pure ()

7979

8080elabMethodTy : TyConInfo -> TTName -> List CtorArg -> Raw -> Raw -> Elab ()

8181elabMethodTy info motiveName [] res ctorApp =

@@ -146,7 +146,7 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =

146146 -- Establish a hole for each argument to the constructor

147147 for {b=()} args $ \arg =>

148148 case arg of

149− CtorParameter _ => return ()

149+ CtorParameter _ => pure ()

150150 CtorField arg => do claim (name arg) (type arg)

151151 unfocus (name arg)

152152

@@ -187,16 +187,16 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =

187187 for args

188188 (\x =>

189189 case x of

190− CtorParameter _ => return List.Nil

190+ CtorParameter _ => pure List.Nil

191191 CtorField arg =>

192192 do let n = name arg

193193 let t = type arg

194194 (argArgs, argRes) <- stealBindings t noRenames

195195 if headsMatch argRes (result info) --recursive

196− then return [ NormalArgument n

197− , IHArgument n

198− ]

199− else return [NormalArgument n])

196+ then pure [ NormalArgument n

197+ , IHArgument n

198+ ]

199+ else pure [NormalArgument n])

200200

201201 argHs <- apply (Var methN) (replicate (List.length argSpec) True)

202202 solve

@@ -261,5 +261,5 @@ deriveElim tyn elimn =

261261 clauses <- getElimClauses info elimn ctors

262262

263263 defineFunction $ DefineFun elimn clauses

264− return ()

264+ pure ()

265265

libs/pruviloj/Pruviloj/Disjoint.idr+2−2

@@ -30,7 +30,7 @@ getDisjointness l r = exists <|> declare

3030

3131 where exists : Elab TTName

3232 exists = do (yep, _, _) <- lookupTyExact (disjointName l r)

33− return yep

33+ pure yep

3434

3535 notConstructor : TTName -> Elab a

3636 notConstructor c = fail [NamePart c, TextPart "is not a constructor"]

@@ -58,7 +58,7 @@ getDisjointness l r = exists <|> declare

5858 h <- gensym "h"

5959 declareType $ Declare fn (args ++ [MkFunArg h eq Explicit NotErased]) `(Void)

6060 defineFunction $ DefineFun fn []

61− return fn

61+ pure fn

6262

6363----------------------

6464-- PUBLIC INTERFACE --

libs/pruviloj/Pruviloj/Induction.idr+6−6

@@ -63,12 +63,12 @@ mutual

6363

6464generalize : (hint : String) -> (ctxt, subject : Raw) -> Elab (TTName, Raw)

6565generalize hint ctxt subj = do n <- gensym hint

66− return (n, !(gen' n ctxt subj))

66+ pure (n, !(gen' n ctxt subj))

6767 where

6868 mutual

6969 gen' : TTName -> Raw -> Raw -> Elab Raw

7070 gen' var outer inner = if alphaEqual (const Nothing) outer inner

71− then return (Var var)

71+ then pure (Var var)

7272 else breakAndRecurse var outer inner

7373

7474 genB : TTName -> Binder Raw -> Raw -> Elab (Binder Raw)

@@ -87,10 +87,10 @@ generalize hint ctxt subj = do n <- gensym hint

8787 do n' <- nameFrom n

8888 b' <- genB var b inner

8989 body' <- gen' var (alphaRaw (rename n n') tm) inner

90− return $ RBind n' b' body'

90+ pure $ RBind n' b' body'

9191 breakAndRecurse var (RApp tm tm') inner =

9292 [| RApp (gen' var tm inner) (gen' var tm' inner) |]

93− breakAndRecurse var other inner = return other

93+ breakAndRecurse var other inner = pure other

9494

9595

9696countBinders : TT -> Nat

@@ -105,7 +105,7 @@ indexVals tm info =

105105 let argsTogether = zip tyArgs (args info)

106106 (argVal, TyConIndex _) <- argsTogether

107107 | _ => empty

108− return argVal

108+ pure argVal

109109

110110makeMotive : (info : TyConInfo) -> (subj, subjTy, goal : Raw) -> Elab ()

111111makeMotive info sub subjTy goal =

@@ -154,4 +154,4 @@ induction subj =

154154 motiveH <- unsafeNth (length (args info) + 1) argHoles

155155 focus motiveH; makeMotive info subj ty' g

156156

157− return (drop (2 + length (tyConArgs tydef)) argHoles)

157+ pure (drop (2 + length (tyConArgs tydef)) argHoles)

libs/pruviloj/Pruviloj/Injective.idr+2−2

@@ -27,7 +27,7 @@ getInjectivity cn = exists <|> declare

2727 where exists : Elab TTName

2828 exists = do (fn, Ref, _) <- lookupTyExact (injName cn)

2929 | (fn, _, _) => fail [TextPart "Bad earlier declaration of", NamePart fn]

30− return fn

30+ pure fn

3131

3232 covering

3333 declare : Elab TTName

@@ -73,7 +73,7 @@ getInjectivity cn = exists <|> declare

7373 search -- rhs is conjunction of Refls

7474 defineFunction $

7575 DefineFun fn [clause]

76− return fn

76+ pure fn

7777

7878countBinders : TT -> Nat

7979countBinders (Bind _ _ body) = S (countBinders body)

libs/pruviloj/Pruviloj/Internals.idr+8−8

@@ -33,13 +33,13 @@ stealBindings : Raw -> (nsubst : TTName -> Maybe TTName) -> Elab (List (TTName,

3333stealBindings (RBind n b tm) nsubst =

3434 do n' <- nameFrom n

3535 (bindings, result) <- stealBindings tm (extend nsubst n n')

36− return ((n', map (alphaRaw nsubst) b) :: bindings, result)

37−stealBindings tm nsubst = return ([], alphaRaw nsubst tm)

36+ pure ((n', map (alphaRaw nsubst) b) :: bindings, result)

37+stealBindings tm nsubst = pure ([], alphaRaw nsubst tm)

3838

3939||| Get the last element of a list. Fail on empty lists.

4040last : List a -> Elab a

4141last [] = fail [TextPart "Unexpected empty list"]

42−last [x] = return x

42+last [x] = pure x

4343last (_::x::xs) = last (x::xs)

4444

4545||| Grab the binders from around a term, assuming that they have been

@@ -110,10 +110,10 @@ elabPatternClause lhs rhs =

110110 | fail [TextPart "Couldn't infer type of left-hand pattern"]

111111 rhsTm <- runElab (bindPatTys pvars rhsTy) $

112112 do -- Introduce all the pattern variables from the LHS

113− repeatUntilFail bindPat <|> return ()

113+ repeatUntilFail bindPat <|> pure ()

114114 rhs

115115 realRhs <- forget (fst rhsTm)

116− return $ MkFunClause (bindPats pvars lhsTm) realRhs

116+ pure $ MkFunClause (bindPats pvars lhsTm) realRhs

117117

118118||| Introduce a unique binder name, returning it

119119intro1 : Elab TTName

@@ -121,7 +121,7 @@ intro1 = do g <- snd <$> getGoal

121121 case g of

122122 Bind n (Pi _ _) _ => do n' <- nameFrom n

123123 intro n'

124− return n'

124+ pure n'

125125 _ => fail [ TextPart "Can't intro1 because goal"

126126 , TermPart g

127127 , TextPart "isn't a function type."]

@@ -134,13 +134,13 @@ doTimes (S k) x = [| x :: (doTimes k x) |]

134134

135135||| Zip two lists, failing if their lengths don't match.

136136zipH : List a -> List b -> Elab (List (a, b))

137−zipH [] [] = return []

137+zipH [] [] = pure []

138138zipH (x::xs) (y::ys) = ((x, y) ::) <$> zipH xs ys

139139zipH _ _ = fail [TextPart "length mismatch"]

140140

141141unsafeNth : Nat -> List a -> Elab a

142142unsafeNth _ [] = fail [TextPart "Ran out of list elements"]

143−unsafeNth Z (x :: _) = return x

143+unsafeNth Z (x :: _) = pure x

144144unsafeNth (S k) (_ :: xs) = unsafeNth k xs

145145

146146

libs/pruviloj/Pruviloj/Internals/TyConInfo.idr+7−7

@@ -51,14 +51,14 @@ alphaTyConInfo ren (MkTyConInfo (tcArg::tcArgs) res) =

5151 in MkTyConInfo (tcArg'::tcArgs') res'

5252

5353getTyConInfo' : List TyConArg -> Raw -> (TTName -> Maybe TTName) -> Elab TyConInfo

54−getTyConInfo' [] res _ = return (MkTyConInfo [] res)

54+getTyConInfo' [] res _ = pure (MkTyConInfo [] res)

5555getTyConInfo' (tcArg::tcArgs) res ren =

5656 do let n = tyConArgName tcArg

5757 n' <- nameFrom n

5858 let ren' = extend ren n n'

5959 -- n' is globally unique so we don't worry about scope

6060 next <- getTyConInfo' tcArgs (RApp res (Var n')) ren'

61− return $ alphaTyConInfo ren' $

61+ pure $ alphaTyConInfo ren' $

6262 record {args = setTyConArgName tcArg n' :: args next} next

6363

6464getTyConInfo : List TyConArg -> Raw -> Elab TyConInfo

@@ -68,14 +68,14 @@ getTyConInfo args res = getTyConInfo' args res (const Nothing)

6868processCtorArgs : TyConInfo -> (TTName, List CtorArg, Raw) -> Elab (TTName, List CtorArg, Raw)

6969processCtorArgs info (cn, cargs, resTy) =

7070 do (args', ty') <- convert' (const Nothing) cargs resTy info

71− return (cn, args', ty')

71+ pure (cn, args', ty')

7272 where

7373 ||| Find the name that was assigned to a given parameter

7474 ||| by comparing positions in the TyConInfo

7575 findParam : TTName -> List Raw -> List TyConArg -> Elab TTName

7676 findParam paramN (Var n :: args) (TyConParameter a :: tcArgs) =

7777 if n == paramN

78− then return (name a)

78+ then pure (name a)

7979 else findParam paramN args tcArgs

8080 findParam paramN (_ :: args) (_ :: tcArgs) =

8181 findParam paramN args tcArgs

@@ -87,7 +87,7 @@ processCtorArgs info (cn, cargs, resTy) =

8787 convert' : (TTName -> Maybe TTName) ->

8888 List CtorArg -> Raw ->

8989 TyConInfo -> Elab (List CtorArg, Raw)

90− convert' subst [] ty info = return ([], alphaRaw subst ty)

90+ convert' subst [] ty info = pure ([], alphaRaw subst ty)

9191 convert' subst (CtorField a :: args) ty info =

9292 do n' <- nameFrom (name a)

9393 let a' = record {

@@ -96,7 +96,7 @@ processCtorArgs info (cn, cargs, resTy) =

9696 } a

9797 let subst' = extend subst (name a) n'

9898 (args', ty') <- convert' subst' args ty info

99− return (CtorField a' :: args', ty')

99+ pure (CtorField a' :: args', ty')

100100 convert' subst (CtorParameter a :: ctorArgs) ty info =

101101 do n' <- findParam (name a) (snd (unApply ty)) (args info)

102102 let a' = record {

@@ -105,4 +105,4 @@ processCtorArgs info (cn, cargs, resTy) =

105105 } a

106106 let subst' = extend subst (name a) n'

107107 (args', ty') <- convert' subst' ctorArgs ty info

108− return (CtorParameter a' :: args', ty')

108+ pure (CtorParameter a' :: args', ty')

rts/idris_rts.h+1−1

@@ -213,7 +213,7 @@ typedef void(*func)(VM*, VAL*);

213213

214214typedef intptr_t i_int;

215215

216−#define MKINT(x) ((void*)((x)<<1)+1)

216+#define MKINT(x) ((void*)((i_int)(((x)<<1)+1)))

217217#define GETINT(x) ((i_int)(x)>>1)

218218#define ISINT(x) ((((i_int)x)&1) == 1)

219219#define ISSTR(x) (GETTY(x) == CT_STRING)

src/Idris/AbsSyntax.hs−1

@@ -2275,7 +2275,6 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

22752275 match (PTactics _) _ = return []

22762276 match (PResolveTC _) (PResolveTC _) = return []

22772277 match (PTrue _ _) (PTrue _ _) = return []

2278− match (PReturn _) (PReturn _) = return []

22792278 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'

22802279 ms <- match' s s'

22812280 return (mt ++ ms)

src/Idris/AbsSyntaxTree.hs−7

@@ -1089,7 +1089,6 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the

10891089 | Placeholder -- ^ Underscore

10901090 | PDoBlock [PDo] -- ^ Do notation

10911091 | PIdiom FC PTerm -- ^ Idiom brackets

1092− | PReturn FC

10931092 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location

10941093 | PProof [PTactic] -- ^ Proof script

10951094 | PTactics [PTactic] -- ^ As PProof, but no auto solving

@@ -1158,7 +1157,6 @@ mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)

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

11591158 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)

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

1161−mapPTermFC f g (PReturn fc) = PReturn (f fc)

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

11631161mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)

11641162mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)

@@ -1394,7 +1392,6 @@ highestFC (PDoBlock lines) =

13941392 getDoFC (DoLetP fc l r) = fc

13951393

13961394highestFC (PIdiom fc _) = Just fc

1397−highestFC (PReturn fc) = Just fc

13981395highestFC (PMetavar fc _) = Just fc

13991396highestFC (PProof _) = Nothing

14001397highestFC (PTactics _) = Nothing

@@ -1460,7 +1457,6 @@ deriving instance NFData OptInfo

14601457-- | Syntactic sugar info

14611458data DSL' t = DSL {

14621459 dsl_bind :: t

1463− , dsl_return :: t

14641460 , dsl_apply :: t

14651461 , dsl_pure :: t

14661462 , dsl_var :: Maybe t

@@ -1561,7 +1557,6 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules

15611557 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2

15621558

15631559initDSL = DSL (PRef f [] (sUN ">>="))

1564− (PRef f [] (sUN "return"))

15651560 (PRef f [] (sUN "<*>"))

15661561 (PRef f [] (sUN "pure"))

15671562 Nothing

@@ -2026,7 +2021,6 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

20262021 prettySe d p bnd (PTactics ts) =

20272022 kwd "tactics" <+> lbrace <> ellipsis <> rbrace

20282023 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n

2029− prettySe d p bnd (PReturn f) = kwd "return"

20302024 prettySe d p bnd PImpossible = kwd "impossible"

20312025 prettySe d p bnd Placeholder = text "_"

20322026 prettySe d p bnd (PDoBlock dos) =

@@ -2348,7 +2342,6 @@ instance Sized PTerm where

23482342 size Placeholder = 1

23492343 size (PDoBlock dos) = 1 + size dos

23502344 size (PIdiom fc term) = 1 + size term

2351− size (PReturn fc) = 1

23522345 size (PMetavar _ name) = 1

23532346 size (PProof tactics) = size tactics

23542347 size (PElabError err) = size err

src/Idris/Core/Evaluate.hs+2−2

@@ -1133,7 +1133,7 @@ lookupDefAcc :: Name -> Bool -> Context ->

11331133lookupDefAcc n mkpublic ctxt

11341134 = map mkp $ lookupCtxt n (definitions ctxt)

11351135 -- io_bind a special case for REPL prettiness

1136− where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

1136+ where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))

11371137 then (d, Public) else (d, a)

11381138

11391139lookupDefAccExact :: Name -> Bool -> Context ->

@@ -1141,7 +1141,7 @@ lookupDefAccExact :: Name -> Bool -> Context ->

11411141lookupDefAccExact n mkpublic ctxt

11421142 = fmap mkp $ lookupCtxtExact n (definitions ctxt)

11431143 -- io_bind a special case for REPL prettiness

1144− where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

1144+ where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))

11451145 then (d, Public) else (d, a)

11461146

11471147lookupTotal :: Name -> Context -> [Totality]

src/Idris/Core/Execute.hs+1−1

@@ -443,7 +443,7 @@ pbm = sUN "prim__believe_me"

443443pstdin = sUN "prim__stdin"

444444pstdout = sUN "prim__stdout"

445445mkfprim = sUN "mkForeignPrim"

446−pioret = sUN "prim_io_return"

446+pioret = sUN "prim_io_pure"

447447piobind = sUN "prim_io_bind"

448448upio = sUN "unsafePerformPrimIO"

449449delay = sUN "Delay"

src/Idris/DSL.hs−1

@@ -95,7 +95,6 @@ expandSugar dsl (PHidden t) = PHidden (expandSugar dsl t)

9595expandSugar dsl (PNoImplicits t) = PNoImplicits (expandSugar dsl t)

9696expandSugar dsl (PUnifyLog t) = PUnifyLog (expandSugar dsl t)

9797expandSugar dsl (PDisamb ns t) = PDisamb ns (expandSugar dsl t)

98−expandSugar dsl (PReturn fc) = dsl_return dsl

9998expandSugar dsl (PRewrite fc by r t ty)

10099 = PRewrite fc by r (expandSugar dsl t) ty

101100expandSugar dsl (PGoal fc r n sc)

src/Idris/Error.hs−1

@@ -133,7 +133,6 @@ warnDisamb ist (PDoBlock steps) = mapM_ wStep steps

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

134134 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y

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

136−warnDisamb ist (PReturn _) = return ()

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

138137warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs

139138warnDisamb ist (PTactics tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs

src/Idris/IBC.hs+3−9

@@ -49,7 +49,7 @@ import Codec.Archive.Zip

4949import Debug.Trace

5050

5151ibcVersion :: Word16

52−ibcVersion = 147

52+ibcVersion = 148

5353

5454-- | When IBC is being loaded - we'll load different things (and omit

5555-- different structures/definitions) depending on which phase we're in.

@@ -1855,8 +1855,6 @@ instance Binary PTerm where

18551855 PIdiom x1 x2 -> do putWord8 27

18561856 put x1

18571857 put x2

1858− PReturn x1 -> do putWord8 28

1859− put x1

18601858 PMetavar x1 x2 -> do putWord8 29

18611859 put x1

18621860 put x2

@@ -2008,8 +2006,6 @@ instance Binary PTerm where

20082006 27 -> do x1 <- get

20092007 x2 <- get

20102008 return (PIdiom x1 x2)

2011− 28 -> do x1 <- get

2012− return (PReturn x1)

20132009 29 -> do x1 <- get

20142010 x2 <- get

20152011 return (PMetavar x1 x2)

@@ -2452,7 +2448,7 @@ instance Binary Syntax where

24522448 _ -> error "Corrupted binary data for Syntax"

24532449

24542450instance (Binary t) => Binary (DSL' t) where

2455− put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

2451+ put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

24562452 = do put x1

24572453 put x2

24582454 put x3

@@ -2462,7 +2458,6 @@ instance (Binary t) => Binary (DSL' t) where

24622458 put x7

24632459 put x8

24642460 put x9

2465− put x10

24662461 get

24672462 = do x1 <- get

24682463 x2 <- get

@@ -2473,8 +2468,7 @@ instance (Binary t) => Binary (DSL' t) where

24732468 x7 <- get

24742469 x8 <- get

24752470 x9 <- get

2476− x10 <- get

2477− return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

2471+ return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

24782472

24792473instance Binary SSymbol where

24802474 put x

src/Idris/Parser/Expr.hs+1−1

@@ -1287,7 +1287,7 @@ listExpr syn = do (FC f (l, c) _) <- getFC

12871287 qs <- sepBy1 (do_ syn) (lchar ',')

12881288 lchar ']'

12891289 return (PDoBlock (map addGuard qs ++

1290− [DoExp fc (PApp fc (PRef fc [] (sUN "return"))

1290+ [DoExp fc (PApp fc (PRef fc [] (sUN "pure"))

12911291 [pexp x])]))) <|>

12921292 (do xs <- many (do (FC fn (sl, sc) _) <- getFC

12931293 lchar ',' <?> "list element"

src/Idris/Providers.hs+2−2

@@ -24,7 +24,7 @@ providerTy fc tm

2424 = PApp fc (PRef fc [] $ sNS (sUN "Provider" ) ["Providers", "Prelude"]) [PExp 0 [] (sMN 0 "pvarg") tm]

2525

2626ioret :: Name

27−ioret = sUN "prim_io_return"

27+ioret = sUN "prim_io_pure"

2828

2929ermod :: Name

3030ermod = sNS (sUN "Error") ["Providers", "Prelude"]

@@ -48,5 +48,5 @@ getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

4848 , pioret == ioret && nm == prmod

4949 = return . Provide $ res

5050 | otherwise = ifail $ "Internal type provider error: result was not " ++

51− "IO (Provider a), or perhaps missing normalisation." ++

51+ "IO (Provider a), or perhaps missing normalisation.\n" ++

5252 "Term: " ++ take 1000 (show tm)

test/basic008/test036.idr+2−2

@@ -10,8 +10,8 @@ unused _ s = s

1010doTest : Maybe Nat

1111doTest = do

1212 a <- Nothing

13− unused a (return 3)

14− `maybechoice` return 2

13+ unused a (pure 3)

14+ `maybechoice` pure 2

1515

1616main : IO ()

1717main = putStrLn . show $ doTest

test/docs002/docs002.idr+2−2

@@ -4,8 +4,8 @@ module Main

44%language TypeProviders

55

66getType : Int -> IO (Provider Type)

7−getType 0 = return (Provide Int)

8−getType _ = return (Provide Bool)

7+getType 0 = pure (Provide Int)

8+getType _ = pure (Provide Bool)

99

1010||| Some documentation

1111%provide (T1 : Type) with getType 0

test/dsl002/Resimp.idr+6−6

@@ -117,12 +117,12 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

117117 Res gam (update gam p c) t

118118 While : Res gam gam (R Bool) ->

119119 Res gam gam (R ()) -> Res gam gam (R ())

120− Return : a -> Res gam gam (R a)

120+ Pure : a -> Res gam gam (R a)

121121 (>>=) : Res gam gam' (R a) -> (a -> Res gam' gam'' (R t)) ->

122122 Res gam gam'' (R t)

123123

124124 ioret : a -> IO a

125− ioret = return

125+ ioret = pure

126126

127127 interp : Env gam -> %static (e : Res gam gam' t) ->

128128 (Env gam' -> interpTy t -> IO u) -> IO u

@@ -133,10 +133,10 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

133133 (\env', scope' => k (envTail env') scope')

134134 interp env (Update method x) k

135135 = do x' <- getUpdater (method (envLookup x env))

136− k (envUpdateVal x x' env) (return ())

136+ k (envUpdateVal x x' env) (pure ())

137137 interp env (Use method x) k

138138 = do x' <- getReader (method (envLookup x env))

139− k env (return x')

139+ k env (pure x')

140140 interp env (Lift io) k

141141 = k env io

142142 interp env (Check x left right) k =

@@ -148,12 +148,12 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

148148 (\env', result =>

149149 do r <- result

150150 if (not r)

151− then (k env' (return ()))

151+ then (k env' (pure ()))

152152 else (interp env' body

153153 (\env'', body' =>

154154 do v <- body' -- make sure it's evalled

155155 interp env'' (While test body) k )))

156− interp env (Return v) k = k env (return v)

156+ interp env (Pure v) k = k env (pure v)

157157 interp env (v >>= f) k

158158 = interp env v (\env', v' => do n <- v'

159159 interp env' (f n) k)

test/dsl002/test014.idr+4−4

@@ -16,16 +16,16 @@ syntax "ifM" [test] "then" [t] "else" [e]

1616

1717open : String -> (p:Purpose) -> Creator (Either () (FILE p))

1818open fn p = ioc (do Right h <- fopen fn (pstring p)

19− | Left err => return (Left ())

20− return (Right (OpenH h)))

19+ | Left err => pure (Left ())

20+ pure (Right (OpenH h)))

2121

2222close : FILE p -> Updater ()

2323close (OpenH h) = iou (closeFile h)

2424

2525readLine : FILE Reading -> Reader String

2626readLine (OpenH h) = ior (do Right str <- fGetLine h

27− | return ""

28− return str)

27+ | pure ""

28+ pure str)

2929

3030eof : FILE Reading -> Reader Bool

3131eof (OpenH h) = ior (fEOF h)

test/dsl004/Door0.idr+2−2

@@ -21,7 +21,7 @@ data DoorCmd : Type -> Type where

2121 Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)

2222

2323data DoorLang : Type -> Type where

24− Return : a -> DoorLang a

24+ Pure : a -> DoorLang a

2525 Action : DoorCmd a -> DoorLang a

2626 (>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b

2727

@@ -29,5 +29,5 @@ testProg : DoorH CLOSED -> DoorLang ()

2929testProg h = do h <- Action (Knock h)

3030 h <- Action (Open h)

3131 h <- Action (Close h)

32− Return ()

32+ Pure ()

3333

test/dsl004/Door1.idr+2−2

@@ -21,7 +21,7 @@ data DoorCmd : AnyType -> AnyType where

2121 Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)

2222

2323data DoorLang : AnyType -> AnyType where

24− Return : {a : AnyType} -> a -> DoorLang a

24+ Pure : {a : AnyType} -> a -> DoorLang a

2525 Action : DoorCmd a -> DoorLang a

2626 (>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b

2727

@@ -33,5 +33,5 @@ testProg : DoorH CLOSED -> DoorLang ()

3333testProg h = with Main, Show do -- h <- Knock h

3434 h <- Open h

3535 -- h <- Close h

36− Return ()

36+ Pure ()

3737

test/dsl004/Door2.idr+2−2

@@ -19,7 +19,7 @@ data DoorCmd : AnyType -> AnyType where

1919 Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)

2020

2121data DoorLang : AnyType -> AnyType where

22− Return : a -> DoorLang a

22+ Pure : a -> DoorLang a

2323 Action : DoorCmd a -> DoorLang a

2424 (>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b

2525

@@ -33,5 +33,5 @@ testProg h = do h <- Action (Knock h)

3333 (True @@ h) <- Action (Open h)

3434 | (False @@ h) => testProg h

3535 h <- Action (Close h)

36− Return ()

36+ Pure ()

3737

test/dsl004/Door3.idr+2−2

@@ -18,13 +18,13 @@ data DoorCmd : AnyType -> AnyType where

1818 Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)

1919

2020data DoorLang : AnyType -> AnyType where

21− Return : {a : AnyType} -> a -> DoorLang a

21+ Pure : {a : AnyType} -> a -> DoorLang a

2222 Action : DoorCmd a -> DoorLang a

2323 (>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b

2424

2525testProg : DoorH CLOSED -> DoorLang (DoorH CLOSED)

2626testProg h = do h <- Action (Knock h)

2727 (True @@ h) <- Action (Open h)

28− | (False @@ h) => Return h

28+ | (False @@ h) => Pure h

2929 Action (Close h)

3030

test/effects001/test021a.idr+3−3

@@ -22,12 +22,12 @@ eval : Expr -> Eff Integer [EXCEPTION String, STDIO, RND, STATE Env]

2222eval (Var x) = do vs <- get

2323 case lookup x vs of

2424 Nothing => raise ("No such variable " ++ x)

25− Just val => return val

26−eval (Val x) = return x

25+ Just val => pure val

26+eval (Val x) = pure x

2727eval (Add l r) = [| eval l + eval r |]

2828eval (Random upper) = do val <- rndInt 0 upper

2929 putStrLn (show val)

30− return val

30+ pure val

3131

3232testExpr : Expr

3333testExpr = Add (Add (Var "foo") (Val 42)) (Random 100)

test/effects002/test025.idr+1−1

@@ -26,7 +26,7 @@ testMemory = do Src :- allocate 5

2626 Dst :- poke 4 (sub1 end) Oh

2727 res <- Dst :- peek 1 (S(S(S(S Z)))) Oh

2828 Dst :- free

29− return (map (prim__zextB8_Int) res)

29+ pure (map (prim__zextB8_Int) res)

3030

3131main : IO ()

3232main = ioe_run (runInit [Dst := (), Src := ()] testMemory)

test/error002/test031.idr+1−1

@@ -5,4 +5,4 @@ module Main

55%language ErrorReflection

66

77main : IO ()

8−main = return ()

8+main = pure ()

test/error003/ErrorReflection.idr+1−1

@@ -47,7 +47,7 @@ reifyTy : TT -> Maybe Ty'

4747reifyTy (P (DCon _ _) (NS (UN "TUnit") _) _) = Just TUnit

4848reifyTy (App (App (P (DCon _ _) (NS (UN "TFun") _) _) t1) t2) = do ty1 <- reifyTy t1

4949 ty2 <- reifyTy t2

50− return $ TFun ty1 ty2

50+ pure $ TFun ty1 ty2

5151reifyTy (P _ (MN i n) _) = Just (TVar i n)

5252reifyTy _ = Nothing

5353

test/error004/FunErrTest.idr+4−4

@@ -22,10 +22,10 @@ extractList t = Just t -- Nothing

2222total

2323has2elts : Err -> Maybe (List ErrorReportPart)

2424has2elts (CantSolveGoal tm _) = do lst <- extractList tm

25− return [ TextPart "Could not prove that"

26− , TermPart lst

27− , TextPart "has at least two elements."

28− ]

25+ pure [ TextPart "Could not prove that"

26+ , TermPart lst

27+ , TextPart "has at least two elements."

28+ ]

2929has2elts e = Just [TextPart (show e)]

3030

3131%error_handlers cadr cons1 has2elts

test/ffi002/test023.idr+2−2

@@ -6,7 +6,7 @@ module Main

66

77-- Provide the Unit type

88goodProvider : IO (Provider Type)

9−goodProvider = return (Provide (the Type ()))

9+goodProvider = pure (Provide (the Type ()))

1010

1111%provide (Unit' : Type) with goodProvider

1212

@@ -15,7 +15,7 @@ foo = ()

1515

1616-- Always fail

1717badProvider : IO (Provider Type)

18−badProvider = return (Error "Always fails")

18+badProvider = pure (Error "Always fails")

1919

2020%provide (t : Type) with badProvider

2121

test/ffi004/test026.idr+2−2

@@ -11,8 +11,8 @@ strToType _ = Nat

1111-- If the file contains "Int", provide Int as a type, otherwise provide Nat

1212fromFile : String -> IO (Provider Type)

1313fromFile fname = do Right str <- readFile fname

14− | Left err => return (Provide Void)

15− return (Provide (strToType (trim str)))

14+ | Left err => pure (Provide Void)

15+ pure (Provide (strToType (trim str)))

1616

1717%provide (T1 : Type) with fromFile "theType"

1818%provide (T2 : Type) with fromFile "theOtherType"

test/ffi005/Postulate.idr+1−1

@@ -3,7 +3,7 @@ module Main

33%language TypeProviders

44

55bad : IO (Provider Type)

6−bad = return $ pure Void

6+bad = pure $ pure Void

77

88%provide postulate oops with bad

99

test/ffi006/ffi006.idr+1−1

@@ -11,7 +11,7 @@ cons x xs = x :: xs

1111

1212show' : List Int -> IO String

1313show' xs = do putStrLn "Ready to show..."

14− return (show xs)

14+ pure (show xs)

1515

1616testList : FFI_Export FFI_C "testHdr.h" []

1717testList = Data (List Int) "ListInt" $

test/ffi007/ffi007.idr+1−1

@@ -55,4 +55,4 @@ main = do

5555 i <- test7 fptr 3

5656 printLn i

5757 test8

58− return ()

58+ pure ()

test/ffi008/ffi008.idr+2−2

@@ -35,12 +35,12 @@ main : IO ()

3535main = do

3636 printLn $ sizeOf test1 == !size1

3737 printLn $ sizeOf test2 == !size2

38− fms <- return $ (test2#0) !mystruct

38+ fms <- pure $ (test2#0) !mystruct

3939 poke I32 fms 122

4040 print_mystruct

4141 printLn $ fields test3

4242 withAlloc test2 $ \p => do

43− f1 <- return $ (test2 # 0) p

43+ f1 <- pure $ (test2 # 0) p

4444 poke I32 f1 8

4545 update I32 f1 (* 2)

4646 print !(peek I32 f1)

test/interfaces006/interfaces006.idr+1−1

@@ -10,7 +10,7 @@ interface Category c => Functor (c: k -> k -> Type) (f: k -> k) where

1010

1111infixr 1 =<<

1212interface Functor c m => Monad (c: k -> k -> Type) (m: k -> k) where

13− return: c x (m x)

13+ pure: c x (m x)

1414 join: c (m (m x)) (m x)

1515 (=<<) : c x (m y) -> c (m x) (m y)

1616

test/io001/test004.idr+2−2

@@ -5,13 +5,13 @@ mwhile t b = do v <- t

55 case v of

66 True => do b

77 mwhile t b

8− False => return ()

8+ False => pure ()

99

1010dumpFile : String -> IO ()

1111dumpFile fn = do { Right h <- openFile fn Read

1212 mwhile (do { -- putStrLn "TEST"

1313 x <- fEOF h

14− return (not x) })

14+ pure (not x) })

1515 (do { Right l <- fGetLine h

1616 putStr l })

1717 closeFile h }

test/io002/test008.idr+1−1

@@ -14,7 +14,7 @@ foo = (4, "foo")

1414

1515

1616ioVals : IO (String, String)

17−ioVals = do { return ("First", "second") }

17+ioVals = do { pure ("First", "second") }

1818

1919main : IO ()

2020main = do (a, b) <- ioVals

test/io003/test018.idr+2−2

@@ -11,11 +11,11 @@ pong = do (sender, x) <- recvMsg

1111 putStrLn x

1212 putStrLn "Received"

1313 sendToThread sender 0 "Hello to you too!"

14− return ()

14+ pure ()

1515

1616ping : Ptr -> IO ()

1717ping thread = do sendToThread thread 0 (prim__vm, "Hello!")

18− return ()

18+ pure ()

1919

2020pingpong : IO ()

2121pingpong

test/io003/test018a.idr+4−4

@@ -11,24 +11,24 @@ ping main proc

1111 msg <- recv

1212 Lift (putStrLn ("Reply: " ++ show msg))

1313 send main "Done"

14− return ()

14+ pure ()

1515

1616pong : Process String ()

1717pong = do -- Lift (putStrLn "Waiting for message")

1818 (sender, m) <- recvWithSender

1919 Lift $ putStrLn ("Received " ++ m)

2020 send sender ("Hello back!")

21− return ()

21+ pure ()

2222

2323mainProc : Process String ()

2424mainProc = do mainID <- myID

2525 pongth <- create pong

2626 pingth <- create (ping mainID pongth)

2727 recv -- block until everything done

28− return ()

28+ pure ()

2929

3030repeatIO : Int -> IO ()

31−repeatIO 0 = return ()

31+repeatIO 0 = pure ()

3232repeatIO n = do printLn n

3333 run mainProc

3434 repeatIO (n - 1)

test/meta001/Finite.idr+17−17

@@ -23,9 +23,9 @@ acceptableConstructor _ = False

2323

2424mkFin : Nat -> Nat -> Elab Raw

2525mkFin Z j = fail [TermPart `(Fin Z), TextPart "is uninhabitable!"]

26−mkFin (S k) Z = return `(FZ {k=~(quote k)})

26+mkFin (S k) Z = pure `(FZ {k=~(quote k)})

2727mkFin (S k) (S j) = do i <- mkFin k j

28− return `(FS {k=~(quote k)} ~i)

28+ pure `(FS {k=~(quote k)} ~i)

2929

3030mkToClause : TTName -> (size, i : Nat) ->

3131 (constr : (TTName, List CtorArg, Raw)) ->

@@ -40,14 +40,14 @@ mkFromClause : TTName -> (size, i : Nat) ->

4040 (constr : (TTName, List CtorArg, Raw)) ->

4141 Elab (FunClause Raw)

4242mkFromClause fn size i (n, [], Var ty) =

43− return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)

43+ pure $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)

4444mkFromClause fn size i (n, _, ty) =

4545 fail [TextPart "unsupported constructor", NamePart n]

4646

4747

4848mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)

4949mkOk1Clause fn size i (n, [], Var ty) =

50− return $ MkFunClause (RApp (Var fn) (Var n))

50+ pure $ MkFunClause (RApp (Var fn) (Var n))

5151 [| (Var (UN "Refl")) (Var ty) (Var n) |]

5252mkOk1Clause fn size i (n, _, ty) =

5353 fail [TextPart "unsupported constructor", NamePart n]

@@ -55,7 +55,7 @@ mkOk1Clause fn size i (n, _, ty) =

5555

5656mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)

5757mkOk2Clause fn size i (n, [], Var ty) =

58− return $ MkFunClause (RApp (Var fn) !(mkFin size i))

58+ pure $ MkFunClause (RApp (Var fn) !(mkFin size i))

5959 [| (Var `{Refl}) `(Fin ~(quote size))

6060 !(mkFin size i) |]

6161mkOk2Clause fn size i (n, _, ty) =

@@ -65,10 +65,10 @@ mkOk2Clause fn size i (n, _, ty) =

6565mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

6666mkToClauses fn size xs = mkToClauses' Z xs

6767 where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

68− mkToClauses' k [] = return []

68+ mkToClauses' k [] = pure []

6969 mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs

7070 clause <- mkToClause fn size k x

71− return $ clause :: rest

71+ pure $ clause :: rest

7272

7373||| Generate a clause for the end of a pattern-match on Fins that

7474||| declares its own impossibility.

@@ -84,11 +84,11 @@ mkAbsurdFinClause fn goal size =

8484 (RApp (Var fn) lhsArg)

8585 let rhs = RBind pv (PVar `(Fin Z : Type))

8686 `(FinZElim {a=~(goal lhsArg)} ~(Var pv))

87− return $ MkFunClause lhs rhs

87+ pure $ MkFunClause lhs rhs

8888 where lhsBody : TTName -> Nat -> Elab Raw

89− lhsBody f Z = return $ Var f

89+ lhsBody f Z = pure $ Var f

9090 lhsBody f (S k) = do smaller <- lhsBody f k

91− return `(FS {k=~(quote k)} ~smaller)

91+ pure `(FS {k=~(quote k)} ~smaller)

9292

9393

9494mkFromClauses : TTName -> TTName -> Nat ->

@@ -96,26 +96,26 @@ mkFromClauses : TTName -> TTName -> Nat ->

9696mkFromClauses fn ty size xs = mkFromClauses' Z xs

9797 where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

9898 mkFromClauses' k [] =

99− return [!(mkAbsurdFinClause fn (const (Var ty)) size)]

99+ pure [!(mkAbsurdFinClause fn (const (Var ty)) size)]

100100 mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs

101101 clause <- mkFromClause fn size k x

102− return $ clause :: rest

102+ pure $ clause :: rest

103103

104104mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

105105mkOk1Clauses fn size xs = mkOk1Clauses' Z xs

106106 where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

107− mkOk1Clauses' k [] = return []

107+ mkOk1Clauses' k [] = pure []

108108 mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs

109109 clause <- mkOk1Clause fn size k x

110− return $ clause :: rest

110+ pure $ clause :: rest

111111

112112mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List (FunClause Raw))

113113mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs

114114 where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

115− mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]

115+ mkOk2Clauses' k [] = pure [!(mkAbsurdFinClause fn resTy size)]

116116 mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs

117117 clause <- mkOk2Clause fn size k x

118− return $ clause :: rest

118+ pure $ clause :: rest

119119

120120

121121genToFin : (to, from, ok1, ok2, ty : TTName) -> Elab ()

@@ -153,7 +153,7 @@ genToFin to from ok1 ok2 ty =

153153 ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy

154154 defineFunction $ DefineFun ok2 ok2Clauses

155155

156− return ()

156+ pure ()

157157

158158

159159deriveFinite : Elab ()

test/meta002/AgdaStyleReflection.idr+3−3

@@ -73,10 +73,10 @@ covering

7373quoteTerm' : List TTName -> Raw -> Elab Term

7474quoteTerm' env (Var n) =

7575 case findIndex (==n) env of

76− Just i => return (Var i [])

76+ Just i => pure (Var i [])

7777 Nothing =>

7878 case findIndex (\(n', _) => n == n') !getEnv of

79− Just i => return (Var i [])

79+ Just i => pure (Var i [])

8080 Nothing => do [(n', nt, ty)] <- lookupTy n

8181 | [] => fail [TextPart "No such variable", NamePart n]

8282 | vs => fail ([TextPart "Can't disambiguate"] ++

@@ -136,7 +136,7 @@ resolveVar k =

136136

137137 where getVar : Nat -> List TTName -> Elab TTName

138138 getVar _ [] = fail [TextPart "Variable out of scope"]

139− getVar Z (n :: _ ) = return n -- NB assumes unique names!

139+ getVar Z (n :: _ ) = pure n -- NB assumes unique names!

140140 getVar (S k) (_ :: env) = getVar k env

141141

142142||| Prepare to apply a global by matching its argument plicities to

test/meta002/Tacs.idr+5−5

@@ -26,7 +26,7 @@ intros : Elab ()

2626intros = do g <- getGoal

2727 case snd g of

2828 `(~_ -> ~_) => intro'

29− _ => return ()

29+ _ => pure ()

3030

3131foo : Nat -> Nat

3232foo = %runElab (do intro (UN "fnord")

@@ -36,7 +36,7 @@ foo = %runElab (do intro (UN "fnord")

3636

3737%runElab (do n <- isTCName `{Nat}

3838 s <- isTCName `{Show}

39− if n || not s then fail [TextPart "nope"] else return ())

39+ if n || not s then fail [TextPart "nope"] else pure ())

4040

4141-- Note that <|> is equivalent to "try" in the old tactics.

4242-- In these tactics, we use ordinary do notation and ordinary documentation strings!

@@ -121,7 +121,7 @@ namespace STLC

121121 mkTypeHole hint = do holeName <- gensym hint

122122 claim holeName RType

123123 unfocus holeName

124− return holeName

124+ pure holeName

125125

126126 -- FIXME: Removing the let-bound Elab script showed a deficiency in

127127 -- how accessible arguments are identified in type signatures. It

@@ -217,13 +217,13 @@ namespace STLC

217217 mkEnvH = do envH <- gensym "env"

218218 claim envH `(List Ty)

219219 unfocus envH

220− return envH

220+ pure envH

221221

222222 mkTyH : Elab TTName

223223 mkTyH = do tyH <- gensym "ty"

224224 claim tyH `(Ty)

225225 unfocus tyH

226− return tyH

226+ pure tyH

227227

228228 mkIx : Fin n -> Elab ()

229229 mkIx FZ = do envH <- mkEnvH

test/primitives006/Data/ByteArray.idr+10−10

@@ -31,7 +31,7 @@ export

3131allocate : Int -> IO ByteArray

3232allocate sz = do

3333 ptr <- foreign FFI_C "array_alloc" (Int -> IO CData) sz

34− return $ BA ptr sz

34+ pure $ BA ptr sz

3535

3636export

3737reallocate : Int -> ByteArray -> IO ()

@@ -42,42 +42,42 @@ export

4242peek : Int -> ByteArray -> IO Byte

4343peek ofs (BA ptr sz)

4444 = if (ofs < 0 || ofs >= sz)

45− then return 0

45+ then pure 0

4646 else foreign FFI_C "array_peek" (Int -> CData -> IO Byte) ofs ptr

4747

4848export

4949peekInt : Int -> ByteArray -> IO Int

5050peekInt ofs (BA ptr sz)

5151 = if (ofs < 0 || ofs+bytesPerInt > sz)

52− then return 0

52+ then pure 0

5353 else foreign FFI_C "array_peek_int" (Int -> CData -> IO Int) ofs ptr

5454

5555export

5656poke : Int -> Byte -> ByteArray -> IO ()

5757poke ofs b (BA ptr sz)

5858 = if (ofs < 0 || ofs >= sz)

59− then return ()

59+ then pure ()

6060 else foreign FFI_C "array_poke" (Int -> Byte -> CData -> IO ()) ofs b ptr

6161

6262export

6363pokeInt : Int -> Int -> ByteArray -> IO ()

6464pokeInt ofs i (BA ptr sz)

6565 = if (ofs < 0 || ofs+bytesPerInt > sz)

66− then return ()

66+ then pure ()

6767 else foreign FFI_C "array_poke_int" (Int -> Int -> CData -> IO ()) ofs i ptr

6868

6969export

7070copy : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO ()

7171copy (BA srcPtr srcSz, srcIx) (BA dstPtr dstSz, dstIx) count

7272 = if (srcIx < 0 || dstIx < 0 || (srcIx+count) > srcSz || (dstIx+count) > dstSz)

73− then return ()

73+ then pure ()

7474 else foreign FFI_C "array_copy" (CData -> Int -> CData -> Int -> Int -> IO ()) srcPtr srcIx dstPtr dstIx count

7575

7676export

7777fill : Int -> Int -> Byte -> ByteArray -> IO ()

7878fill ofs count b (BA ptr sz)

7979 = if (ofs < 0 || ofs+count > sz)

80− then return ()

80+ then pure ()

8181 else foreign FFI_C "array_fill" (Int -> Int -> Byte -> CData -> IO ()) ofs count b ptr

8282

8383export

@@ -88,7 +88,7 @@ export

8888compare : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO Int

8989compare (BA ptrL szL, ofsL) (BA ptrR szR, ofsR) count

9090 = if (ofsL < 0 || ofsL+count > szL || ofsR < 0 || ofsR+count > szR)

91− then return 0

91+ then pure 0

9292 else foreign FFI_C "array_compare" (CData -> Int -> CData -> Int -> Int -> IO Int) ptrL ofsL ptrR ofsR count

9393

9494export

@@ -96,5 +96,5 @@ find : Byte -> ByteArray -> Int -> Int -> IO (Maybe Int)

9696find b (BA ptr sz) ofs end = do

9797 ofs <- foreign FFI_C "array_find" (Byte -> CData -> Int -> Int -> IO Int) b ptr ofs end

9898 if ofs < 0

99− then return $ Nothing

100− else return $ Just ofs

99+ then pure $ Nothing

100+ else pure $ Just ofs

test/primitives006/Data/Bytes.idr+11−11

@@ -30,7 +30,7 @@ allocate capacity = do

3030 arr <- BA.allocate (BA.bytesPerInt + capacity)

3131 BA.pokeInt 0 dataOfs arr

3232 BA.fill dataOfs capacity 0 arr -- zero the array

33− return $ B arr dataOfs dataOfs

33+ pure $ B arr dataOfs dataOfs

3434

3535export

3636length : Bytes -> Int

@@ -59,7 +59,7 @@ grow factor (B arr ofs end) = do

5959 else BA.size arr - ofs

6060 B arr' ofs' end' <- allocate $ (factor*bytesAvailable) `max` minimalCapacity

6161 BA.copy (arr, ofs) (arr', ofs') bytesUsed

62− return $ B arr' ofs' (ofs' + bytesUsed)

62+ pure $ B arr' ofs' (ofs' + bytesUsed)

6363

6464export

6565snoc : Bytes -> Byte -> Bytes

@@ -68,17 +68,17 @@ snoc bs@(B arr ofs end) byte

6868 if end >= BA.size arr

6969 then unsafePerformIO $ do -- need more space

7070 grown <- grow 2 bs

71− return $ snoc grown byte

71+ pure $ snoc grown byte

7272 else unsafePerformIO $ do

7373 maxUsed <- BA.peekInt 0 arr

7474 if maxUsed > end

7575 then do -- someone already took the headroom, need copying

7676 copy <- grow 2 bs

77− return $ snoc copy byte

77+ pure $ snoc copy byte

7878 else do -- can mutate

7979 BA.pokeInt 0 (end+1) arr

8080 BA.poke end byte arr

81− return $ B arr ofs (end+1)

81+ pure $ B arr ofs (end+1)

8282

8383infixl 7 |>

8484export

@@ -97,7 +97,7 @@ namespace SnocView

9797 then SnocView.Nil

9898 else unsafePerformIO $ do

9999 last <- BA.peek (end-1) arr

100− return $ SnocView.Snoc (B arr ofs (end-1)) last

100+ pure $ SnocView.Snoc (B arr ofs (end-1)) last

101101

102102namespace ConsView

103103 data ConsView : Type where

@@ -111,7 +111,7 @@ namespace ConsView

111111 then ConsView.Nil

112112 else unsafePerformIO $ do

113113 first <- BA.peek ofs arr

114− return $ ConsView.Cons first (B arr (ofs+1) end)

114+ pure $ ConsView.Cons first (B arr (ofs+1) end)

115115

116116infixr 7 ++

117117export

@@ -121,17 +121,17 @@ export

121121 if endL + countR > BA.size arrL

122122 then unsafePerformIO $ do -- need more space

123123 grown <- grow 2 bsL

124− return $ grown ++ bsR

124+ pure $ grown ++ bsR

125125 else unsafePerformIO $ do

126126 maxUsedL <- BA.peekInt 0 arrL

127127 if maxUsedL > endL

128128 then do -- headroom taken

129129 copyL <- grow 2 bsL

130− return $ copyL ++ bsR

130+ pure $ copyL ++ bsR

131131 else do -- can mutate

132132 BA.pokeInt 0 (endL + countR) arrL

133133 BA.copy (arrR, ofsR) (arrL, endL) countR

134− return $ B arrL ofsL (endL + countR)

134+ pure $ B arrL ofsL (endL + countR)

135135

136136export

137137dropPrefix : Int -> Bytes -> Bytes

@@ -245,7 +245,7 @@ cmp (B arrL ofsL endL) (B arrR ofsR endR) = unsafePerformIO $ do

245245 let countR = endR - ofsR

246246 let commonCount = countL `min` countR

247247 result <- BA.compare (arrL, ofsL) (arrR, ofsR) commonCount

248− return $

248+ pure $

249249 if result /= 0

250250 then i2o result

251251 else compare countL countR

test/primitives006/load-test.idr+1−1

@@ -26,7 +26,7 @@ unit n b =

2626 in printLn $ (show b ++ "/" ++ show n, length expanded, length elines)

2727

2828alloc : Int -> Int -> IO Int

29−alloc x 0 = return x

29+alloc x 0 = pure x

3030alloc x i = do

3131 -- allocate an array

3232 arr <- BA.allocate (64 * 1024 * 1024)

test/proof003/test015.idr+1−1

@@ -68,7 +68,7 @@ readNum : IO Nat

6868readNum = do putStr "Enter a number:"

6969 i <- getLine

7070 let n : Integer = cast i

71− return (fromInteger n)

71+ pure (fromInteger n)

7272

7373main : IO ()

7474main = do let Just bin1 = natToBin 8 42

test/proofsearch002/Process.idr+1−1

@@ -347,7 +347,7 @@ removeConn cl acc (x :: xs) = removeConn cl (x :: acc) xs

347347getRequest : EvalState iface hs -> Maybe (Ptr, (ty ** (Nat, iface ty)), EvalState iface hs)

348348getRequest (MkEvalState queue reply clients nh)

349349 = do (pid, req, queue') <- removeReq [] queue

350− return (pid, req, MkEvalState queue' reply clients nh)

350+ pure (pid, req, MkEvalState queue' reply clients nh)

351351

352352countClients : EvalState iface hs -> (Nat, EvalState iface hs)

353353countClients (MkEvalState queue reply clients nh)

test/reg040/reg040.idr+1−1

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

11-- The regression that this tests for is defunct unsafePerformIO

22

33io : IO Int

4−io = return 42

4+io = pure 42

55

66main : IO ()

77main = printLn $ unsafePerformIO io

test/reg048/reg048.idr+1−1

@@ -10,7 +10,7 @@ test xs = do let lst = Data.SortedMap.toList mp

1010 if length found /= n

1111 then putStrLn $ "some lost in " ++ show xs ++ ": res=" ++ show res

1212 ++ " toList=" ++ show lst

13− else return ()

13+ else pure ()

1414

1515 where

1616 mp : SortedMap Int ()

test/reg052/reg052.idr+2−2

@@ -1,8 +1,8 @@

11impure_op : Bits64 -> IO Bits64

2−impure_op foo = return $ foo + 1

2+impure_op foo = pure $ foo + 1

33

44impure_int : IO Int

5−impure_int = return 41

5+impure_int = pure 41

66

77main : IO ()

88main = impure_int >>= impure_op . prim__zextInt_B64 >>= printLn

test/sugar003/test013.idr+1−1

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

11module Main

22

33forLoop : List a -> (a -> IO ()) -> IO ()

4−forLoop [] f = return ()

4+forLoop [] f = pure ()

55forLoop (x :: xs) f = do f x

66 forLoop xs f

77

test/unique004/unique002.idr+1−1

@@ -15,6 +15,6 @@ foo : UList Int -> IO ()

1515foo xs = do -- let f = \x : Int => showU xs

1616 putStrLn $ free xs

1717 putStrLn $ f 42 xs

18− return ()

18+ pure ()

1919 where f : Int -> Borrowed (UList Int) -> String

2020 f x xs = showU xs

test/unique004/unique002a.idr+1−1

@@ -15,4 +15,4 @@ foo : UList Int -> IO ()

1515foo xs = do let f = \x : Int => showU xs

1616 putStrLn $ free xs

1717 putStrLn $ f 42

18− return ()

18+ pure ()

test/unique004/unique003.idr+1−1

@@ -19,4 +19,4 @@ foo xs = do let f = \x : Int => showU xs -- can't build this in unique context

1919 putStrLn (f 10)

2020 putStrLn $ free xs

2121 putStrLn (f 10)

22− return ()

22+ pure ()