f754d9c · Idris-dev · git.iko.soy

CHANGELOG.md+2

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

28* `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.

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

30

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

32+

31## Tool updates

33## Tool updates

32

34

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

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

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

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

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

35

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

37− arrow f = Kleisli (return . f)

37+ arrow f = Kleisli (pure . f)

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

39− return (x, b)

39+ pure (x, b)

40

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

42− return (a, x)

42+ pure (a, x)

43

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

45 y <- g b

46− return (x, y)

46+ pure (x, y)

47

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

49 y <- g a

50− return (x, y)

50+ pure (x, y)

51

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

53 zeroArrow : arr a b

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

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

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

25 case p' of

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

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

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

28 throw = ioe_fail

29

30implementation Catchable List () where

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

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

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

16

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

18− id = Kleisli (return . id)

18+ id = Kleisli (pure . id)

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

20

21infixr 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

17

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

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

21

22implementation (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)

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

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

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

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

27

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

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

30 let MkRWST ka = k a

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

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

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

33

34implementation (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)

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

37

38implementation (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)

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

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

44

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

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

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

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

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

48

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

50

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

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

39 ka r

40

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

42− ask = RD return

42+ ask = RD pure

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

44

45implementation MonadTrans (ReaderT r) where

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

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

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

50asks f = do r <- ask

51− return (f r)

51+ pure (f r)

52

53||| The reader monad. See MonadReader

54Reader : Type -> Type -> Type

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

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

27

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

29 (b, t) <- a r

30− return (g b, t))

30+ pure (g b, t))

31

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

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

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

35 kv st')

36

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

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

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

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

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

40

41implementation MonadTrans (StateT stateType) where

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

43− return (r, st))

43+ pure (r, st))

44

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

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

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

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

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

52gets f = do s <- get

53− return (f s)

53+ pure (f s)

54

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

56State : (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

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

37 let WR ka = k a

38 (b, w') <- ka

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

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

40

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

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

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

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

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

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

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

46− return (a, f w)

46+ pure (a, f w)

47

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

49 lift x = WR $ do r <- x

50− return (r, neutral)

50+ pure (r, neutral)

51

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

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

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

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

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

57− return (a, f' w)

57+ pure (a, f' w)

58

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

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

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

62− return (a, f)

62+ pure (a, f)

63

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

65Writer : Type -> Type -> Type

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

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

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

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

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

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

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

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

47

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

86 do

87 w <- cast <$> parseInteger whole

88 e <- parseInteger exp

89− return (w, 0, e)

89+ pure (w, 0, e)

90 (whole::[]) =>

91 do

92 w <- cast <$> parseInteger whole

93− return (w, 0, 0)

93+ pure (w, 0, 0)

94 _ => Nothing

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

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

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

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

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

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

105 (frac::[]) =>

106 do

107 w <- cast <$> parseInteger whole

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

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

111 _ => Nothing

112 _ => Nothing

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

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

5||| @ result the final result

6export

7trace : (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)

9

10

libs/base/System.idr+4−4

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

22setEnv : String -> String -> IO Bool

23setEnv key value = do

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

25− return (ok == 0)

25+ pure (ok == 0)

26

27||| Unsets an environment variable.

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

29unsetEnv : String -> IO Bool

30unsetEnv key = do

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

32− return (ok == 0)

32+ pure (ok == 0)

33

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

35getEnvironment = getAllPairs 0 []

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

49 envPair <- getEnvPair n

50 is_nil <- nullStr envPair

51 if is_nil

52− then return $ reverse $ map splitEq acc

52+ then pure $ reverse $ map splitEq acc

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

54

55||| Quit with a particular exit code

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

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

60time : IO Integer

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

62− return t

62+ pure t

63

64usleep : Int -> IO ()

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

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

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

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

24 prim__vm

25 null <- nullPtr msgs

26− return (not null)

26+ pure (not null)

27

28||| Check for messages in the process inbox

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

@@ -32,7 +32,7 @@ checkMsgsTimeout timeout

32 = do msgs <- foreign FFI_C "idris_checkMessagesTimeout"

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

34 null <- nullPtr msgs

35− return (not null)

35+ pure (not null)

36

37private

38sender : Ptr -> IO Ptr

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

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

62 prim__vm channel sender

63 null <- nullPtr msgs

64− return (not null)

64+ pure (not null)

65

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

67||| arrives.

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

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

72 (Ptr -> IO Ptr) prim__vm

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

74− return x

74+ pure x

75

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

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

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

85 vm <- sender m

86 chan <- channel_id m

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

88− return (vm, chan, x)

88+ pure (vm, chan, x)

89

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

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

33

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

35alloc : Composite -> IO CPtr

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

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

37

38||| Free memory allocated with alloc

39free : CPtr -> IO ()

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

63||| Write to memory

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

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

66− return ()

66+ pure ()

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

68− return ()

68+ pure ()

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

70− return ()

70+ pure ()

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

72− return ()

72+ pure ()

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

74− return ()

74+ pure ()

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

76− return ()

76+ pure ()

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

78− return ()

78+ pure ()

79

80||| Update memory with a function.

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

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

83− out <- return $ f val

83+ out <- pure $ f val

84 poke ty cp out

85

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

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

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

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

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

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

176− return ()

176+ pure ()

177-}

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

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

14 peek p offset = prim_peek8 p offset

15 poke p offset val = do

16 _ <- prim_poke8 p offset val

17− return ()

17+ pure ()

18

19Storable Bits16 where

20 sizeOf _ = 2

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

22 peek p offset = prim_peek16 p offset

23 poke p offset val = do

24 _ <- prim_poke16 p offset val

25− return ()

25+ pure ()

26

27Storable Bits32 where

28 sizeOf _ = 4

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

30 peek p offset = prim_peek32 p offset

31 poke p offset val = do

32 _ <- prim_poke32 p offset val

33− return ()

33+ pure ()

34

35Storable Bits64 where

36 sizeOf _ = 8

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

38 peek p offset = prim_peek64 p offset

39 poke p offset val = do

40 _ <- 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

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

36 mx >>= \x =>

37 pure (f x)

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

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

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

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

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

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

42

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

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

32

33implementation Functor CGI where

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

35− return (f a, i))

35+ pure (f a, i))

36

37implementation Applicative CGI where

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

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

39

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

41 (c, j) <- b i

42− return (f c, j))

42+ pure (f c, j))

43

44implementation Monad CGI where

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

46 getAction (k (fst v)) (snd v))

47

48setInfo : CGIInfo -> CGI ()

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

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

50

51getInfo : CGI CGIInfo

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

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

53

54export

55lift : IO a -> CGI a

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

57− return (x, st) } )

57+ pure (x, st) } )

58

59export

60output : String -> CGI ()

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

64export

65queryVars : CGI Vars

66queryVars = do i <- getInfo

67− return (GET i)

67+ pure (GET i)

68

69export

70postVars : CGI Vars

71postVars = do i <- getInfo

72− return (POST i)

72+ pure (POST i)

73

74export

75cookieVars : CGI Vars

76cookieVars = do i <- getInfo

77− return (Cookies i)

77+ pure (Cookies i)

78

79export

80queryVar : String -> CGI (Maybe String)

81queryVar x = do vs <- queryVars

82− return (lookup x vs)

82+ pure (lookup x vs)

83

84getOutput : CGI String

85getOutput = do i <- getInfo

86− return (Output i)

86+ pure (Output i)

87

88getHeaders : CGI String

89getHeaders = do i <- getInfo

90− return (Headers i)

90+ pure (Headers i)

91

92export

93flushHeaders : CGI ()

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

110getContent : Int -> IO String

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

112 getC : Nat -> String -> IO String

113− getC Z acc = return $ reverse acc

113+ getC Z acc = pure $ reverse acc

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

115 getC k (strCons x acc)

116

117getCgiEnv : String -> IO String

118getCgiEnv key = do

119 val <- getEnv key

120− return $ maybe "" id val

120+ pure $ maybe "" id val

121

122export

123runCGI : CGI a -> IO a

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

138 "")

139 putStrLn (Headers st)

140 putStr (Output st)

141− return v

141+ pure v

142

143

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

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

219

220 if socket_res == -1

221 then map Left getErrno

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

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

223

224||| Close a socket

225export

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

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

246 if bind_res == (-1)

247 then getErrno

248− else return 0

248+ else pure 0

249

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

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

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

261

262 if conn_res == (-1)

263 then getErrno

264− else return 0

264+ else pure 0

265

266||| Listens on a bound socket.

267|||

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

273 (descriptor sock) BACKLOG

274 if listen_res == (-1)

275 then getErrno

276− else return 0

276+ else pure 0

277

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

279parseIPv4 : String -> SocketAddress

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

305 (Ptr -> IO String)

306 ptr

307

308− return $ parseIPv4 ipv4_addr

308+ pure $ parseIPv4 ipv4_addr

309− Just AF_INET6 => return IPv6Addr

309+ Just AF_INET6 => pure IPv6Addr

310− Just AF_UNSPEC => return InvalidAddress)

310+ Just AF_UNSPEC => pure InvalidAddress)

311

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

313|||

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

337 let (MkSocket _ fam ty p_num) = sock

338 sockaddr <- getSockAddr (SAPtr sockaddr_ptr)

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

341

342||| Send data on the specified socket.

343|||

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

357

358 if send_res == (-1)

359 then map Left getErrno

360− else return $ Right send_res

360+ else pure $ Right send_res

361

362freeRecvStruct : RecvStructPtr -> IO ()

363freeRecvStruct (RSPtr p) =

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

400 then do

401 errno <- getErrno

402 freeRecvStruct (RSPtr recv_struct_ptr)

403− return $ Left errno

403+ pure $ Left errno

404 else

405 if recv_res == 0

406 then do

407 freeRecvStruct (RSPtr recv_struct_ptr)

408− return $ Left 0

408+ pure $ Left 0

409 else do

410 payload <- foreign FFI_C "idrnet_get_recv_payload"

411 (Ptr -> IO String)

412 recv_struct_ptr

413 freeRecvStruct (RSPtr recv_struct_ptr)

414− return $ Right (payload, recv_res)

414+ pure $ Right (payload, recv_res)

415

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

417|||

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

432

433 if send_res == (-1)

434 then map Left getErrno

435− else return $ Right send_res

435+ else pure $ Right send_res

436

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

438|||

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

453

454 if (recv_res == (-1))

455 then map Left getErrno

456− else return $ Right recv_res

456+ else pure $ Right recv_res

457

458||| Send a message.

459|||

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

477

478 if sendto_res == (-1)

479 then map Left getErrno

480− else return $ Right sendto_res

480+ else pure $ Right sendto_res

481

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

483|||

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

502

503 if sendto_res == (-1)

504 then map Left getErrno

505− else return $ Right sendto_res

505+ else pure $ Right sendto_res

506

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

508foreignGetRecvfromPayload : RecvfromStructPtr -> IO String

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

528 port <- foreign FFI_C "idrnet_sockaddr_ipv4_port"

529 (Ptr -> IO Int)

530 sockaddr_ptr

531− return port

531+ pure port

532

533

534||| Receive a message.

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

568 port <- foreignGetRecvfromPort recv_ptr'

569 addr <- foreignGetRecvfromAddr recv_ptr'

570 freeRecvfromStruct recv_ptr'

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

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

572

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

574|||

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

606 port <- foreignGetRecvfromPort recv_ptr'

607 addr <- foreignGetRecvfromAddr recv_ptr'

608 freeRecvfromStruct recv_ptr'

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

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

610

611-- --------------------------------------------------------------------- [ EOF ]

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

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

18 map f (Lift a) = Lift (map f a)

19

20implementation Applicative (Process msg) where

21− pure = Lift . return

21+ pure = Lift . pure

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

23

24implementation Monad (Process msg) where

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

32||| Get current process ID

33export

34myID : Process msg (ProcID msg)

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

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

36

37||| Send a message to another process

38||| Returns whether the send was unsuccessful.

39export

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

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

42− return (x /= 0))

42+ pure (x /= 0))

43

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

45export

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

55export

56recv : Process msg msg

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

58− return m

58+ pure m

59 where get : IO (Ptr, msg)

60 get = getMsg

61

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

74recvWithSender : Process msg (ProcID msg, msg)

75recvWithSender {msg}

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

77− return (MkPID senderid, m)

77+ pure (MkPID senderid, m)

78 where get : IO (Ptr, msg)

79 get = getMsg

80

81export

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

83create (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)

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

46 fail <- ioe_lift $ nullPtr ptr

47 if fail then ioe_fail "Cannot allocate memory"

48− else return ptr

48+ else pure ptr

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

50

51private

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

66

67private

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

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

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

70do_peek ptr offset (S n)

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

72 bs <- do_peek ptr (S offset) n

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

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

74

75private

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

77−do_poke _ _ [] = return ()

77+do_poke _ _ [] = pure ()

78do_poke ptr offset (b::bs)

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

80 do_poke ptr (S offset) bs

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

179move dst_offset src_offset size dst_bounds src_bounds

180 = do src_ptr <- Src :- getRawPtr

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

182− return ()

182+ pure ()

183

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

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

106perfLog res msg =

107 if livePerf res

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

109− else return ()

109+ else pure ()

110

111-- ------------------------------------------------------- [ Effect Definition ]

112

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

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

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

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

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

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

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

25

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

27|||

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

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

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

31− return (toFin v)

31+ pure (toFin v)

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

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

34 Just v => v

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

36

37||| Select a random element from a vector

38rndSelect' : 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)

40

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

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

43−rndSelect [] = return Nothing

43+rndSelect [] = pure Nothing

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

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

45

46||| Sets the random seed

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

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

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

36 putM newst

37 val <- prog

38 putM st

39− return val

39+ pure val

40

libs/effects/Effects.idr+6−6

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

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

304toEff xs' = id

305

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

307−return x = Value x

308−

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

310−

311infixl 2 <*>

306infixl 2 <*>

312

307

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

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

314pure = Value

309pure = Value

315

310

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

312+return = pure

313+

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

315+

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

317pureM = Value

318

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

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

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

322 arg <- v

323− return (fn arg)

323+ pure (fn arg)

324

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

326 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

18 believe_me (exit 1)

19

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

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

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

22

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

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

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

44 fail <- ioe_lift $ nullPtr ptr

45 if fail then ioe_fail "Cannot allocate memory"

46− else return ptr

46+ else pure ptr

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

48

49private

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

64

65private

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

68do_peek ptr offset (S n)

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

70 bs <- do_peek ptr (S offset) n

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

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

72

73private

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

75−do_poke _ _ [] = return ()

75+do_poke _ _ [] = pure ()

76do_poke ptr offset (b::bs)

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

78 do_poke ptr (S offset) bs

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

171move dst_offset src_offset size dst_bounds src_bounds

172 = do src_ptr <- Src :- getRawPtr

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

174− return ()

174+ pure ()

175

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

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

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

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

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

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

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

23

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

25|||

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

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

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

29− return (toFin v)

29+ pure (toFin v)

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

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

32 Just v => v

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

34

35||| Select a random element from a vector

36rndSelect' : 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)

38

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

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

41−rndSelect [] = return Nothing

41+rndSelect [] = pure Nothing

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

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

43

44||| Sets the random seed

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

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

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

36 putM newst

37 val <- prog

38 putM st

39− return val

39+ pure val

40

libs/prelude/IO.idr+26−26

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

98unsafePerformPrimIO : PrimIO a -> a

99-- compiled as primitive

100

101−prim_io_return : a -> PrimIO a

101+prim_io_pure : a -> PrimIO a

102−prim_io_return x = Prim__IO x

102+prim_io_pure x = Prim__IO x

103

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

105io_bind (MkIO fn) k

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

107 (\ b => case k b of

108 MkIO fkb => fkb w))

109

110−io_return : a -> IO' l a

110+io_pure : a -> IO' l a

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

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

112

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

114liftPrimIO = MkIO

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

122

123unsafePerformIO : IO' ffi a -> a

124unsafePerformIO (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))

126

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

129

130prim_write : String -> IO' l Int

131prim_write s

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

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

133

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

136

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

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

140

141--------- The C FFI

142namespace FFI_C

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

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

206

207prim_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

209

210namespace IO

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

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

213 (prim_fork (prim_io_bind (f w)

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

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

215− (\x => prim_io_return x))

215+ (\x => prim_io_pure x))

216

217 forceGC : IO ()

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

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

316

317-- Accessing memory

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

320

321prim_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 (

323 prim__poke8 (world w) ptr offset val))

324

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

327

328prim_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 (

330 prim__poke16 (world w) ptr offset val))

331

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

334

335prim_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 (

337 prim__poke32 (world w) ptr offset val))

338

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

341

342prim_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 (

344 prim__poke64 (world w) ptr offset val))

345

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

348

349prim_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 (

351 prim__pokePtr (world w) ptr offset val))

352

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

355

356prim_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 (

358 prim__pokeDouble (world w) ptr offset val))

359

360||| Single precision floats are marshalled to Doubles

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

363

364||| Single precision floats are marshalled to Doubles

365prim_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 (

367 prim__pokeSingle (world w) ptr offset val))

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

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

253 export

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

255 lookupTyExact n = case !(lookupTy n) of

256− [res] => return res

256+ [res] => pure res

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

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

259

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

269 export

270 lookupDatatypeExact : TTName -> Elab Datatype

271 lookupDatatypeExact n = case !(lookupDatatype n) of

272− [res] => return res

272+ [res] => pure res

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

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

275

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

285 export

286 lookupFunDefnExact : TTName -> Elab (FunDefn TT)

287 lookupFunDefnExact n = case !(lookupFunDefn n) of

288− [res] => return res

288+ [res] => pure res

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

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

291

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

299 export

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

301 lookupArgsExact n = case !(lookupArgs n) of

302− [res] => return res

302+ [res] => pure res

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

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

305

libs/prelude/Prelude.idr+7−7

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

50---- Functor implementations

51

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

54

55Functor Maybe where

56 map f (Just x) = Just (f x)

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

63---- Applicative implementations

64

65Applicative PrimIO where

66− pure = prim_io_return

66+ pure = prim_io_pure

67

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

69

70Applicative Maybe where

71 pure = Just

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

252 partial

253 nullPtr : Ptr -> JS_IO Bool

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

255− return (ok /= 0)

255+ pure (ok /= 0)

256

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

258 partial

259 nullStr : String -> JS_IO Bool

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

261− return (ok /= 0)

261+ pure (ok /= 0)

262

263

264||| Pointer equality

265eqPtr : Ptr -> Ptr -> IO Bool

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

267− return (eq /= 0)

267+ pure (eq /= 0)

268

269||| Loop while some test is true

270|||

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

275while t b = do v <- t

276 if v then do b

277 while t b

278− else return ()

278+ else pure ()

279

280------- Some error rewriting

281

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

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

42getFileError : IO FileError

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

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

45− return err

45+ pure err

46

47Show FileError where

48 show FileReadError = "File Read Error"

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

73export

74ferror : File -> IO Bool

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

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

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

77

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

79private

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

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

90 if !(nullPtr h)

91 then do err <- getFileError

92− return (Left err)

92+ pure (Left err)

93− else return (Right (FHandle h))

93+ else pure (Right (FHandle h))

94

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

96export

97validFile : File -> IO Bool

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

99− return (not x)

99+ pure (not x)

100

101||| Modes for opening files

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

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

149 if (s < 0)

150 then do err <- getFileError

151− return (Left err)

151+ pure (Left err)

152− else return (Right s)

152+ else pure (Right s)

153

154private

155do_fread : Ptr -> IO' l String

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

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

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

161 if !(ferror (FHandle h))

162− then return (Left FileReadError)

162+ then pure (Left FileReadError)

163− else return (Right c)

163+ else pure (Right c)

164

165export

166fflush : File -> IO ()

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

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

176 if !(nullPtr ptr)

177 then do err <- getFileError

178− return (Left err)

178+ pure (Left err)

179− else return (Right (FHandle ptr))

179+ else pure (Right (FHandle ptr))

180

181export

182pclose : File -> IO ()

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

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

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

191 if !(ferror (FHandle h))

192− then return (Left FileReadError)

192+ then pure (Left FileReadError)

193− else return (Right str)

193+ else pure (Right str)

194

195||| Read a line from a file

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

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

206 if (res /= 0)

207 then do errno <- getErrno

208 if errno == 0

209− then return (Left FileWriteError)

209+ then pure (Left FileWriteError)

210 else do err <- getFileError

211− return (Left err)

211+ pure (Left err)

212− else return (Right ())

212+ else pure (Right ())

213

214export

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

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

236export

237fEOF : File -> IO Bool

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

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

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

240

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

242export

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

248export

249fpoll : File -> IO Bool

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

251− return (p > 0)

251+ pure (p > 0)

252

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

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

258export

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

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

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

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

262 Right max <- fileSize h

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

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

264 c <- readFile' h max ""

265 closeFile h

266− return c

266+ pure c

267 where

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

269 readFile' h max contents =

270 do x <- fEOF h

271 if not x && max > 0

272 then do Right l <- fGetLine h

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

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

274 assert_total $

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

276− else return (Right contents)

276+ else pure (Right contents)

277

278||| Write a string to a file

279export

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

281 IO (Either FileError ())

282writeFile fn contents = do

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

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

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

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

285 closeFile h

286− return (Right ())

286+ pure (Right ())

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

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

29||| descriptor

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

31putStr' x = do prim_write x

32− return ()

32+ pure ()

33

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

35putStr : String -> IO ()

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

66||| descriptor

67getLine' : IO' ffi String

68getLine' = do x <- prim_read

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

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

70 where trimNL : String -> String

71 trimNL str with (strM str)

72 trimNL "" | StrNil = ""

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

103

104 partial

105 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

107 do arg <- getArg i

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

109

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

155 case fn acc x of

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

157 replWith acc' prompt fn

158− Nothing => return ()

158+ Nothing => pure ()

159

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

161||| @ prompt the prompt to show

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

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

4

5import Builtins

6import Prelude.Functor

7−import Prelude.Applicative

7+import public Prelude.Applicative

8import Prelude.Basics

9import IO

10

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

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

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

29return = pure

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

30

31

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

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

32flatten = join

33flatten = join

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

36-- Prelude modules other than the top level.

37-- Prelude modules other than the top level.

37

38

38Functor (IO' ffi) where

39Functor (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))

40

41

41Applicative (IO' ffi) where

42Applicative (IO' ffi) where

42− pure x = io_return x

43+ pure x = io_pure x

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

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

44 io_bind a (\a' =>

45 io_bind a (\a' =>

45− io_return (f' a')))

46+ io_pure (f' a')))

46

47

48

48Monad (IO' ffi) where

49Monad (IO' ffi) where

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

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

358partial

359nullPtr : Ptr -> IO Bool

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

361− return (ok /= 0)

361+ pure (ok /= 0)

362

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

364partial

365nullStr : String -> IO Bool

366nullStr 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

87newHole hint ty =

88 do hn <- gensym hint

89 claim hn ty

90− return hn

90+ pure hn

91

92||| Use a term to solve a hole

93|||

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

105 do n' <- nameFrom n

106 intro n'

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

108− go _ = return []

108+ go _ = pure []

109

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

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

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

113inHole h todo =

114 if (h `elem` !getHoles)

115 then do focus h; Just <$> todo

116− else return Nothing

116+ else pure Nothing

117

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

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

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

132 claim h newGoal

133 fill (Var h); solve

134 focus h

135− return h

135+ pure h

136

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

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

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

149 claim todo ty

150 letbind n ty (Var todo)

151 focus todo

152− return todo

152+ pure todo

153

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

155||| the first attempt; succeeds otherwise.

156repeatUntilFail : Elab () -> Elab ()

157repeatUntilFail tac =

158 do tac

159− repeatUntilFail tac <|> return ()

159+ repeatUntilFail tac <|> pure ()

160

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

162||| expected name. Otherwise fail.

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

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

182inferType tac =

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

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

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

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

186 where

187 startInfer : Elab ()

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

219 newHoles <- apply tm (replicate argCount True)

220 solve

221 actualHoles <- getHoles

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

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

223

224 where countPi : Raw -> Nat

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

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

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

116 focus a1; fill rTm1; solve

117 focus a2; fill rTm2; solve

118 focus dH; resolveTC fn

119− return (Var eq)

119+ pure (Var eq)

120 matchCase tms

121 _ => fail [TextPart "Inapplicable"]

122

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

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

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

167 (reverse rest)

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

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

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

170 , c2 <- constructors datatype]

171 clauses <- for todo

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

178 isConstr : Raw -> Elab Bool

179 isConstr tm = case headName tm of

180 Just n => isTCName n

181− Nothing => return False

181+ Nothing => pure False

182

183 partial -- mkRhs

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

20bindIndices : TyConInfo -> Elab Renamer

21bindIndices info = bind' (getIndices info) noRenames

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

23− bind' [] ren = return ren

23+ bind' [] ren = pure ren

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

25 forall n' (alphaRaw ren t)

26 bind' ixs (extend ren n n')

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

31bindTarget info = do ren <- bindIndices info

32 tn <- gensym "target"

33 forall tn (alphaRaw ren $ result info)

34− return (tn, ren)

34+ pure (tn, ren)

35

36elabMotive : TyConInfo -> Elab ()

37elabMotive info = do attack

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

75 fill argTm; solve

76 solve -- attack

77 solve -- ihT

78− else return ()

78+ else pure ()

79

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

81elabMethodTy info motiveName [] res ctorApp =

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

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

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

148 case arg of

149− CtorParameter _ => return ()

149+ CtorParameter _ => pure ()

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

151 unfocus (name arg)

152

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

187 for args

188 (\x =>

189 case x of

190− CtorParameter _ => return List.Nil

190+ CtorParameter _ => pure List.Nil

191 CtorField arg =>

192 do let n = name arg

193 let t = type arg

194 (argArgs, argRes) <- stealBindings t noRenames

195 if headsMatch argRes (result info) --recursive

196− then return [ NormalArgument n

196+ then pure [ NormalArgument n

197− , IHArgument n

197+ , IHArgument n

198− ]

198+ ]

199− else return [NormalArgument n])

199+ else pure [NormalArgument n])

200

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

202 solve

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

261 clauses <- getElimClauses info elimn ctors

262

263 defineFunction $ DefineFun elimn clauses

264− return ()

264+ pure ()

265

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

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

30

31 where exists : Elab TTName

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

33− return yep

33+ pure yep

34

35 notConstructor : TTName -> Elab a

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

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

58 h <- gensym "h"

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

60 defineFunction $ DefineFun fn []

61− return fn

61+ pure fn

62

63----------------------

64-- PUBLIC INTERFACE --

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

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

63

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

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

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

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

67 where

68 mutual

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

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

71− then return (Var var)

71+ then pure (Var var)

72 else breakAndRecurse var outer inner

73

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

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

87 do n' <- nameFrom n

88 b' <- genB var b inner

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

90− return $ RBind n' b' body'

90+ pure $ RBind n' b' body'

91 breakAndRecurse var (RApp tm tm') inner =

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

93− breakAndRecurse var other inner = return other

93+ breakAndRecurse var other inner = pure other

94

95

96countBinders : TT -> Nat

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

105 let argsTogether = zip tyArgs (args info)

106 (argVal, TyConIndex _) <- argsTogether

107 | _ => empty

108− return argVal

108+ pure argVal

109

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

111makeMotive info sub subjTy goal =

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

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

155 focus motiveH; makeMotive info subj ty' g

156

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

27 where exists : Elab TTName

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

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

30− return fn

30+ pure fn

31

32 covering

33 declare : Elab TTName

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

73 search -- rhs is conjunction of Refls

74 defineFunction $

75 DefineFun fn [clause]

76− return fn

76+ pure fn

77

78countBinders : TT -> Nat

79countBinders (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,

33stealBindings (RBind n b tm) nsubst =

34 do n' <- nameFrom n

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

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

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

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

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

38

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

40last : List a -> Elab a

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

42−last [x] = return x

42+last [x] = pure x

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

44

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

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

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

111 rhsTm <- runElab (bindPatTys pvars rhsTy) $

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

113− repeatUntilFail bindPat <|> return ()

113+ repeatUntilFail bindPat <|> pure ()

114 rhs

115 realRhs <- forget (fst rhsTm)

116− return $ MkFunClause (bindPats pvars lhsTm) realRhs

116+ pure $ MkFunClause (bindPats pvars lhsTm) realRhs

117

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

119intro1 : Elab TTName

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

121 case g of

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

123 intro n'

124− return n'

124+ pure n'

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

126 , TermPart g

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

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

134

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

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

137−zipH [] [] = return []

137+zipH [] [] = pure []

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

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

140

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

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

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

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

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

145

146

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

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

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

52

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

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

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

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

56 do let n = tyConArgName tcArg

57 n' <- nameFrom n

58 let ren' = extend ren n n'

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

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

61− return $ alphaTyConInfo ren' $

61+ pure $ alphaTyConInfo ren' $

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

63

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

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

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

69processCtorArgs info (cn, cargs, resTy) =

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

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

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

72 where

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

74 ||| by comparing positions in the TyConInfo

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

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

77 if n == paramN

78− then return (name a)

78+ then pure (name a)

79 else findParam paramN args tcArgs

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

81 findParam paramN args tcArgs

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

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

88 List CtorArg -> Raw ->

89 TyConInfo -> Elab (List CtorArg, Raw)

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

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

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

92 do n' <- nameFrom (name a)

93 let a' = record {

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

96 } a

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

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

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

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

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

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

102 let a' = record {

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

105 } a

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

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

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

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

src/Idris/AbsSyntax.hs−1

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

2275 match (PTactics _) _ = return []

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

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

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

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

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

2280 ms <- match' s s'

2279 ms <- match' s s'

2281 return (mt ++ ms)

2280 return (mt ++ ms)

src/Idris/AbsSyntaxTree.hs−7

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

1088 | Placeholder -- ^ Underscore

1089 | PDoBlock [PDo] -- ^ Do notation

1090 | PIdiom FC PTerm -- ^ Idiom brackets

1091− | PReturn FC

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

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

1093 | PProof [PTactic] -- ^ Proof script

1092 | PProof [PTactic] -- ^ Proof script

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1393,7 +1391,6 @@ highestFC (PDoBlock lines) =

1393 getDoFC (DoLetP fc l r) = fc

1391 getDoFC (DoLetP fc l r) = fc

1394

1392

1395highestFC (PIdiom fc _) = Just fc

1393highestFC (PIdiom fc _) = Just fc

1396−highestFC (PReturn fc) = Just fc

1397highestFC (PMetavar fc _) = Just fc

1394highestFC (PMetavar fc _) = Just fc

1398highestFC (PProof _) = Nothing

1395highestFC (PProof _) = Nothing

1399highestFC (PTactics _) = Nothing

1396highestFC (PTactics _) = Nothing

@@ -1459,7 +1456,6 @@ deriving instance NFData OptInfo

1459-- | Syntactic sugar info

1456-- | Syntactic sugar info

1460data DSL' t = DSL {

1457data DSL' t = DSL {

1461 dsl_bind :: t

1458 dsl_bind :: t

1462− , dsl_return :: t

1463 , dsl_apply :: t

1459 , dsl_apply :: t

1464 , dsl_pure :: t

1460 , dsl_pure :: t

1465 , dsl_var :: Maybe t

1461 , dsl_var :: Maybe t

@@ -1560,7 +1556,6 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules

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

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

1561

1557

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

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

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

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

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

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

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

1566 Nothing

1561 Nothing

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

2025 prettySe d p bnd (PTactics ts) =

2020 prettySe d p bnd (PTactics ts) =

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

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

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

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

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

2029 prettySe d p bnd PImpossible = kwd "impossible"

2023 prettySe d p bnd PImpossible = kwd "impossible"

2030 prettySe d p bnd Placeholder = text "_"

2024 prettySe d p bnd Placeholder = text "_"

2031 prettySe d p bnd (PDoBlock dos) =

2025 prettySe d p bnd (PDoBlock dos) =

@@ -2347,7 +2341,6 @@ instance Sized PTerm where

2347 size Placeholder = 1

2341 size Placeholder = 1

2348 size (PDoBlock dos) = 1 + size dos

2342 size (PDoBlock dos) = 1 + size dos

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

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

2350− size (PReturn fc) = 1

2351 size (PMetavar _ name) = 1

2344 size (PMetavar _ name) = 1

2352 size (PProof tactics) = size tactics

2345 size (PProof tactics) = size tactics

2353 size (PElabError err) = size err

2346 size (PElabError err) = size err

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

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

1133lookupDefAcc n mkpublic ctxt

1134 = map mkp $ lookupCtxt n (definitions ctxt)

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

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

1138

1139lookupDefAccExact :: Name -> Bool -> Context ->

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

1141lookupDefAccExact n mkpublic ctxt

1142 = fmap mkp $ lookupCtxtExact n (definitions ctxt)

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

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

1146

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

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

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

443pstdin = sUN "prim__stdin"

444pstdout = sUN "prim__stdout"

445mkfprim = sUN "mkForeignPrim"

446−pioret = sUN "prim_io_return"

446+pioret = sUN "prim_io_pure"

447piobind = sUN "prim_io_bind"

448upio = sUN "unsafePerformPrimIO"

449delay = sUN "Delay"

src/Idris/DSL.hs−1

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

95expandSugar dsl (PNoImplicits t) = PNoImplicits (expandSugar dsl t)

96expandSugar dsl (PUnifyLog t) = PUnifyLog (expandSugar dsl t)

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

98−expandSugar dsl (PReturn fc) = dsl_return dsl

99expandSugar dsl (PRewrite fc by r t ty)

98expandSugar dsl (PRewrite fc by r t ty)

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

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

101expandSugar dsl (PGoal fc r n sc)

100expandSugar dsl (PGoal fc r n sc)

src/Idris/Error.hs−1

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

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

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

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

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

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

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

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

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

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

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

src/Idris/IBC.hs+3−9

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

49import Debug.Trace

50

51ibcVersion :: Word16

52−ibcVersion = 147

52+ibcVersion = 148

53

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

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

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

1853 PIdiom x1 x2 -> do putWord8 27

1854 put x1

1855 put x2

1856− PReturn x1 -> do putWord8 28

1857− put x1

1858 PMetavar x1 x2 -> do putWord8 29

1856 PMetavar x1 x2 -> do putWord8 29

1859 put x1

1857 put x1

1860 put x2

1858 put x2

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

2006 27 -> do x1 <- get

2004 27 -> do x1 <- get

2007 x2 <- get

2005 x2 <- get

2008 return (PIdiom x1 x2)

2006 return (PIdiom x1 x2)

2009− 28 -> do x1 <- get

2010− return (PReturn x1)

2011 29 -> do x1 <- get

2007 29 -> do x1 <- get

2012 x2 <- get

2008 x2 <- get

2013 return (PMetavar x1 x2)

2009 return (PMetavar x1 x2)

@@ -2450,7 +2446,7 @@ instance Binary Syntax where

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

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

2451

2447

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

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

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

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

2454 = do put x1

2450 = do put x1

2455 put x2

2451 put x2

2456 put x3

2452 put x3

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

2460 put x7

2456 put x7

2461 put x8

2457 put x8

2462 put x9

2458 put x9

2463− put x10

2464 get

2459 get

2465 = do x1 <- get

2460 = do x1 <- get

2466 x2 <- get

2461 x2 <- get

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

2471 x7 <- get

2466 x7 <- get

2472 x8 <- get

2467 x8 <- get

2473 x9 <- get

2468 x9 <- get

2474− x10 <- get

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

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

2476

2470

2477instance Binary SSymbol where

2471instance Binary SSymbol where

2478 put x

2472 put x

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

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

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

1288 lchar ']'

1289 return (PDoBlock (map addGuard qs ++

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

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

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

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

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

src/Idris/Providers.hs+2−2

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

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

25

26ioret :: Name

27−ioret = sUN "prim_io_return"

27+ioret = sUN "prim_io_pure"

28

29ermod :: Name

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

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

48 , pioret == ioret && nm == prmod

49 = return . Provide $ res

50 | 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" ++

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

test/basic008/test036.idr+2−2

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

10doTest : Maybe Nat

11doTest = do

12 a <- Nothing

13− unused a (return 3)

13+ unused a (pure 3)

14− `maybechoice` return 2

14+ `maybechoice` pure 2

15

16main : IO ()

17main = putStrLn . show $ doTest

test/docs002/docs002.idr+2−2

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

4%language TypeProviders

5

6getType : Int -> IO (Provider Type)

7−getType 0 = return (Provide Int)

7+getType 0 = pure (Provide Int)

8−getType _ = return (Provide Bool)

8+getType _ = pure (Provide Bool)

9

10||| Some documentation

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

117 Res gam (update gam p c) t

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

119 Res gam gam (R ()) -> Res gam gam (R ())

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

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

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

122 Res gam gam'' (R t)

123

124 ioret : a -> IO a

125− ioret = return

125+ ioret = pure

126

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

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

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

134 interp env (Update method x) k

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

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

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

137 interp env (Use method x) k

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

139− k env (return x')

139+ k env (pure x')

140 interp env (Lift io) k

141 = k env io

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

148 (\env', result =>

149 do r <- result

150 if (not r)

151− then (k env' (return ()))

151+ then (k env' (pure ()))

152 else (interp env' body

153 (\env'', body' =>

154 do v <- body' -- make sure it's evalled

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

157 interp env (v >>= f) k

158 = interp env v (\env', v' => do n <- v'

159 interp env' (f n) k)

test/dsl002/test014.idr+4−4

@@ -16,16 +16,16 @@ syntax "ifM" [test] "then" [t] "else" [e]

16

17open : String -> (p:Purpose) -> Creator (Either () (FILE p))

18open fn p = ioc (do Right h <- fopen fn (pstring p)

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

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

20− return (Right (OpenH h)))

20+ pure (Right (OpenH h)))

21

22close : FILE p -> Updater ()

23close (OpenH h) = iou (closeFile h)

24

25readLine : FILE Reading -> Reader String

26readLine (OpenH h) = ior (do Right str <- fGetLine h

27− | return ""

27+ | pure ""

28− return str)

28+ pure str)

29

30eof : FILE Reading -> Reader Bool

31eof (OpenH h) = ior (fEOF h)

test/dsl004/Door0.idr+2−2

@@ -21,7 +21,7 @@ data DoorCmd : Type -> Type where

21 Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)

22

23data DoorLang : Type -> Type where

24− Return : a -> DoorLang a

24+ Pure : a -> DoorLang a

25 Action : DoorCmd a -> DoorLang a

26 (>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b

27

@@ -29,5 +29,5 @@ testProg : DoorH CLOSED -> DoorLang ()

29testProg h = do h <- Action (Knock h)

30 h <- Action (Open h)

31 h <- Action (Close h)

32− Return ()

32+ Pure ()

33

test/dsl004/Door1.idr+2−2

@@ -21,7 +21,7 @@ data DoorCmd : AnyType -> AnyType where

21 Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)

22

23data DoorLang : AnyType -> AnyType where

24− Return : {a : AnyType} -> a -> DoorLang a

24+ Pure : {a : AnyType} -> a -> DoorLang a

25 Action : DoorCmd a -> DoorLang a

26 (>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b

27

@@ -33,5 +33,5 @@ testProg : DoorH CLOSED -> DoorLang ()

33testProg h = with Main, Show do -- h <- Knock h

34 h <- Open h

35 -- h <- Close h

36− Return ()

36+ Pure ()

37

test/dsl004/Door2.idr+2−2

@@ -19,7 +19,7 @@ data DoorCmd : AnyType -> AnyType where

19 Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)

20

21data DoorLang : AnyType -> AnyType where

22− Return : a -> DoorLang a

22+ Pure : a -> DoorLang a

23 Action : DoorCmd a -> DoorLang a

24 (>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b

25

@@ -33,5 +33,5 @@ testProg h = do h <- Action (Knock h)

33 (True @@ h) <- Action (Open h)

34 | (False @@ h) => testProg h

35 h <- Action (Close h)

36− Return ()

36+ Pure ()

37

test/dsl004/Door3.idr+2−2

@@ -18,13 +18,13 @@ data DoorCmd : AnyType -> AnyType where

18 Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)

19

20data DoorLang : AnyType -> AnyType where

21− Return : {a : AnyType} -> a -> DoorLang a

21+ Pure : {a : AnyType} -> a -> DoorLang a

22 Action : DoorCmd a -> DoorLang a

23 (>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b

24

25testProg : DoorH CLOSED -> DoorLang (DoorH CLOSED)

26testProg h = do h <- Action (Knock h)

27 (True @@ h) <- Action (Open h)

28− | (False @@ h) => Return h

28+ | (False @@ h) => Pure h

29 Action (Close h)

30

test/effects001/test021a.idr+3−3

@@ -22,12 +22,12 @@ eval : Expr -> Eff Integer [EXCEPTION String, STDIO, RND, STATE Env]

22eval (Var x) = do vs <- get

23 case lookup x vs of

24 Nothing => raise ("No such variable " ++ x)

25− Just val => return val

25+ Just val => pure val

26−eval (Val x) = return x

26+eval (Val x) = pure x

27eval (Add l r) = [| eval l + eval r |]

28eval (Random upper) = do val <- rndInt 0 upper

29 putStrLn (show val)

30− return val

30+ pure val

31

32testExpr : Expr

33testExpr = Add (Add (Var "foo") (Val 42)) (Random 100)

test/effects002/test025.idr+1−1

@@ -26,7 +26,7 @@ testMemory = do Src :- allocate 5

26 Dst :- poke 4 (sub1 end) Oh

27 res <- Dst :- peek 1 (S(S(S(S Z)))) Oh

28 Dst :- free

29− return (map (prim__zextB8_Int) res)

29+ pure (map (prim__zextB8_Int) res)

30

31main : IO ()

32main = ioe_run (runInit [Dst := (), Src := ()] testMemory)

test/error002/test031.idr+1−1

@@ -5,4 +5,4 @@ module Main

5%language ErrorReflection

6

7main : IO ()

8−main = return ()

8+main = pure ()

test/error003/ErrorReflection.idr+1−1

@@ -47,7 +47,7 @@ reifyTy : TT -> Maybe Ty'

47reifyTy (P (DCon _ _) (NS (UN "TUnit") _) _) = Just TUnit

48reifyTy (App (App (P (DCon _ _) (NS (UN "TFun") _) _) t1) t2) = do ty1 <- reifyTy t1

49 ty2 <- reifyTy t2

50− return $ TFun ty1 ty2

50+ pure $ TFun ty1 ty2

51reifyTy (P _ (MN i n) _) = Just (TVar i n)

52reifyTy _ = Nothing

53

test/error004/FunErrTest.idr+4−4

@@ -22,10 +22,10 @@ extractList t = Just t -- Nothing

22total

23has2elts : Err -> Maybe (List ErrorReportPart)

24has2elts (CantSolveGoal tm _) = do lst <- extractList tm

25− return [ TextPart "Could not prove that"

25+ pure [ TextPart "Could not prove that"

26− , TermPart lst

26+ , TermPart lst

27− , TextPart "has at least two elements."

27+ , TextPart "has at least two elements."

28− ]

28+ ]

29has2elts e = Just [TextPart (show e)]

30

31%error_handlers cadr cons1 has2elts

test/ffi002/test023.idr+2−2

@@ -6,7 +6,7 @@ module Main

6

7-- Provide the Unit type

8goodProvider : IO (Provider Type)

9−goodProvider = return (Provide (the Type ()))

9+goodProvider = pure (Provide (the Type ()))

10

11%provide (Unit' : Type) with goodProvider

12

@@ -15,7 +15,7 @@ foo = ()

15

16-- Always fail

17badProvider : IO (Provider Type)

18−badProvider = return (Error "Always fails")

18+badProvider = pure (Error "Always fails")

19

20%provide (t : Type) with badProvider

21

test/ffi004/test026.idr+2−2

@@ -11,8 +11,8 @@ strToType _ = Nat

11-- If the file contains "Int", provide Int as a type, otherwise provide Nat

12fromFile : String -> IO (Provider Type)

13fromFile fname = do Right str <- readFile fname

14− | Left err => return (Provide Void)

14+ | Left err => pure (Provide Void)

15− return (Provide (strToType (trim str)))

15+ pure (Provide (strToType (trim str)))

16

17%provide (T1 : Type) with fromFile "theType"

18%provide (T2 : Type) with fromFile "theOtherType"

test/ffi005/Postulate.idr+1−1

@@ -3,7 +3,7 @@ module Main

3%language TypeProviders

4

5bad : IO (Provider Type)

6−bad = return $ pure Void

6+bad = pure $ pure Void

7

8%provide postulate oops with bad

9

test/ffi006/ffi006.idr+1−1

@@ -11,7 +11,7 @@ cons x xs = x :: xs

11

12show' : List Int -> IO String

13show' xs = do putStrLn "Ready to show..."

14− return (show xs)

14+ pure (show xs)

15

16testList : FFI_Export FFI_C "testHdr.h" []

17testList = Data (List Int) "ListInt" $

test/ffi007/ffi007.idr+1−1

@@ -55,4 +55,4 @@ main = do

55 i <- test7 fptr 3

56 printLn i

57 test8

58− return ()

58+ pure ()

test/ffi008/ffi008.idr+2−2

@@ -35,12 +35,12 @@ main : IO ()

35main = do

36 printLn $ sizeOf test1 == !size1

37 printLn $ sizeOf test2 == !size2

38− fms <- return $ (test2#0) !mystruct

38+ fms <- pure $ (test2#0) !mystruct

39 poke I32 fms 122

40 print_mystruct

41 printLn $ fields test3

42 withAlloc test2 $ \p => do

43− f1 <- return $ (test2 # 0) p

43+ f1 <- pure $ (test2 # 0) p

44 poke I32 f1 8

45 update I32 f1 (* 2)

46 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

10

11infixr 1 =<<

12interface Functor c m => Monad (c: k -> k -> Type) (m: k -> k) where

13− return: c x (m x)

13+ pure: c x (m x)

14 join: c (m (m x)) (m x)

15 (=<<) : c x (m y) -> c (m x) (m y)

16

test/io001/test004.idr+2−2

@@ -5,13 +5,13 @@ mwhile t b = do v <- t

5 case v of

6 True => do b

7 mwhile t b

8− False => return ()

8+ False => pure ()

9

10dumpFile : String -> IO ()

11dumpFile fn = do { Right h <- openFile fn Read

12 mwhile (do { -- putStrLn "TEST"

13 x <- fEOF h

14− return (not x) })

14+ pure (not x) })

15 (do { Right l <- fGetLine h

16 putStr l })

17 closeFile h }

test/io002/test008.idr+1−1

@@ -14,7 +14,7 @@ foo = (4, "foo")

14

15

16ioVals : IO (String, String)

17−ioVals = do { return ("First", "second") }

17+ioVals = do { pure ("First", "second") }

18

19main : IO ()

20main = do (a, b) <- ioVals

test/io003/test018.idr+2−2

@@ -11,11 +11,11 @@ pong = do (sender, x) <- recvMsg

11 putStrLn x

12 putStrLn "Received"

13 sendToThread sender 0 "Hello to you too!"

14− return ()

14+ pure ()

15

16ping : Ptr -> IO ()

17ping thread = do sendToThread thread 0 (prim__vm, "Hello!")

18− return ()

18+ pure ()

19

20pingpong : IO ()

21pingpong

test/io003/test018a.idr+4−4

@@ -11,24 +11,24 @@ ping main proc

11 msg <- recv

12 Lift (putStrLn ("Reply: " ++ show msg))

13 send main "Done"

14− return ()

14+ pure ()

15

16pong : Process String ()

17pong = do -- Lift (putStrLn "Waiting for message")

18 (sender, m) <- recvWithSender

19 Lift $ putStrLn ("Received " ++ m)

20 send sender ("Hello back!")

21− return ()

21+ pure ()

22

23mainProc : Process String ()

24mainProc = do mainID <- myID

25 pongth <- create pong

26 pingth <- create (ping mainID pongth)

27 recv -- block until everything done

28− return ()

28+ pure ()

29

30repeatIO : Int -> IO ()

31−repeatIO 0 = return ()

31+repeatIO 0 = pure ()

32repeatIO n = do printLn n

33 run mainProc

34 repeatIO (n - 1)

test/meta001/Finite.idr+17−17

@@ -23,9 +23,9 @@ acceptableConstructor _ = False

23

24mkFin : Nat -> Nat -> Elab Raw

25mkFin 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)})

27mkFin (S k) (S j) = do i <- mkFin k j

28− return `(FS {k=~(quote k)} ~i)

28+ pure `(FS {k=~(quote k)} ~i)

29

30mkToClause : TTName -> (size, i : Nat) ->

31 (constr : (TTName, List CtorArg, Raw)) ->

@@ -40,14 +40,14 @@ mkFromClause : TTName -> (size, i : Nat) ->

40 (constr : (TTName, List CtorArg, Raw)) ->

41 Elab (FunClause Raw)

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

44mkFromClause fn size i (n, _, ty) =

45 fail [TextPart "unsupported constructor", NamePart n]

46

47

48mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)

49mkOk1Clause fn size i (n, [], Var ty) =

50− return $ MkFunClause (RApp (Var fn) (Var n))

50+ pure $ MkFunClause (RApp (Var fn) (Var n))

51 [| (Var (UN "Refl")) (Var ty) (Var n) |]

52mkOk1Clause fn size i (n, _, ty) =

53 fail [TextPart "unsupported constructor", NamePart n]

@@ -55,7 +55,7 @@ mkOk1Clause fn size i (n, _, ty) =

55

56mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)

57mkOk2Clause fn size i (n, [], Var ty) =

58− return $ MkFunClause (RApp (Var fn) !(mkFin size i))

58+ pure $ MkFunClause (RApp (Var fn) !(mkFin size i))

59 [| (Var `{Refl}) `(Fin ~(quote size))

60 !(mkFin size i) |]

61mkOk2Clause fn size i (n, _, ty) =

@@ -65,10 +65,10 @@ mkOk2Clause fn size i (n, _, ty) =

65mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

66mkToClauses fn size xs = mkToClauses' Z xs

67 where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

68− mkToClauses' k [] = return []

68+ mkToClauses' k [] = pure []

69 mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs

70 clause <- mkToClause fn size k x

71− return $ clause :: rest

71+ pure $ clause :: rest

72

73||| Generate a clause for the end of a pattern-match on Fins that

74||| declares its own impossibility.

@@ -84,11 +84,11 @@ mkAbsurdFinClause fn goal size =

84 (RApp (Var fn) lhsArg)

85 let rhs = RBind pv (PVar `(Fin Z : Type))

86 `(FinZElim {a=~(goal lhsArg)} ~(Var pv))

87− return $ MkFunClause lhs rhs

87+ pure $ MkFunClause lhs rhs

88 where lhsBody : TTName -> Nat -> Elab Raw

89− lhsBody f Z = return $ Var f

89+ lhsBody f Z = pure $ Var f

90 lhsBody f (S k) = do smaller <- lhsBody f k

91− return `(FS {k=~(quote k)} ~smaller)

91+ pure `(FS {k=~(quote k)} ~smaller)

92

93

94mkFromClauses : TTName -> TTName -> Nat ->

@@ -96,26 +96,26 @@ mkFromClauses : TTName -> TTName -> Nat ->

96mkFromClauses fn ty size xs = mkFromClauses' Z xs

97 where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

98 mkFromClauses' k [] =

99− return [!(mkAbsurdFinClause fn (const (Var ty)) size)]

99+ pure [!(mkAbsurdFinClause fn (const (Var ty)) size)]

100 mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs

101 clause <- mkFromClause fn size k x

102− return $ clause :: rest

102+ pure $ clause :: rest

103

104mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

105mkOk1Clauses fn size xs = mkOk1Clauses' Z xs

106 where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

107− mkOk1Clauses' k [] = return []

107+ mkOk1Clauses' k [] = pure []

108 mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs

109 clause <- mkOk1Clause fn size k x

110− return $ clause :: rest

110+ pure $ clause :: rest

111

112mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List (FunClause Raw))

113mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs

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

116 mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs

117 clause <- mkOk2Clause fn size k x

118− return $ clause :: rest

118+ pure $ clause :: rest

119

120

121genToFin : (to, from, ok1, ok2, ty : TTName) -> Elab ()

@@ -153,7 +153,7 @@ genToFin to from ok1 ok2 ty =

153 ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy

154 defineFunction $ DefineFun ok2 ok2Clauses

155

156− return ()

156+ pure ()

157

158

159deriveFinite : Elab ()

test/meta002/AgdaStyleReflection.idr+3−3

@@ -73,10 +73,10 @@ covering

73quoteTerm' : List TTName -> Raw -> Elab Term

74quoteTerm' env (Var n) =

75 case findIndex (==n) env of

76− Just i => return (Var i [])

76+ Just i => pure (Var i [])

77 Nothing =>

78 case findIndex (\(n', _) => n == n') !getEnv of

79− Just i => return (Var i [])

79+ Just i => pure (Var i [])

80 Nothing => do [(n', nt, ty)] <- lookupTy n

81 | [] => fail [TextPart "No such variable", NamePart n]

82 | vs => fail ([TextPart "Can't disambiguate"] ++

@@ -136,7 +136,7 @@ resolveVar k =

136

137 where getVar : Nat -> List TTName -> Elab TTName

138 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!

140 getVar (S k) (_ :: env) = getVar k env

141

142||| Prepare to apply a global by matching its argument plicities to

test/meta002/Tacs.idr+5−5

@@ -26,7 +26,7 @@ intros : Elab ()

26intros = do g <- getGoal

27 case snd g of

28 `(~_ -> ~_) => intro'

29− _ => return ()

29+ _ => pure ()

30

31foo : Nat -> Nat

32foo = %runElab (do intro (UN "fnord")

@@ -36,7 +36,7 @@ foo = %runElab (do intro (UN "fnord")

36

37%runElab (do n <- isTCName `{Nat}

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

40

41-- Note that <|> is equivalent to "try" in the old tactics.

42-- In these tactics, we use ordinary do notation and ordinary documentation strings!

@@ -121,7 +121,7 @@ namespace STLC

121 mkTypeHole hint = do holeName <- gensym hint

122 claim holeName RType

123 unfocus holeName

124− return holeName

124+ pure holeName

125

126 -- FIXME: Removing the let-bound Elab script showed a deficiency in

127 -- how accessible arguments are identified in type signatures. It

@@ -217,13 +217,13 @@ namespace STLC

217 mkEnvH = do envH <- gensym "env"

218 claim envH `(List Ty)

219 unfocus envH

220− return envH

220+ pure envH

221

222 mkTyH : Elab TTName

223 mkTyH = do tyH <- gensym "ty"

224 claim tyH `(Ty)

225 unfocus tyH

226− return tyH

226+ pure tyH

227

228 mkIx : Fin n -> Elab ()

229 mkIx FZ = do envH <- mkEnvH

test/primitives006/Data/ByteArray.idr+10−10

@@ -31,7 +31,7 @@ export

31allocate : Int -> IO ByteArray

32allocate sz = do

33 ptr <- foreign FFI_C "array_alloc" (Int -> IO CData) sz

34− return $ BA ptr sz

34+ pure $ BA ptr sz

35

36export

37reallocate : Int -> ByteArray -> IO ()

@@ -42,42 +42,42 @@ export

42peek : Int -> ByteArray -> IO Byte

43peek ofs (BA ptr sz)

44 = if (ofs < 0 || ofs >= sz)

45− then return 0

45+ then pure 0

46 else foreign FFI_C "array_peek" (Int -> CData -> IO Byte) ofs ptr

47

48export

49peekInt : Int -> ByteArray -> IO Int

50peekInt ofs (BA ptr sz)

51 = if (ofs < 0 || ofs+bytesPerInt > sz)

52− then return 0

52+ then pure 0

53 else foreign FFI_C "array_peek_int" (Int -> CData -> IO Int) ofs ptr

54

55export

56poke : Int -> Byte -> ByteArray -> IO ()

57poke ofs b (BA ptr sz)

58 = if (ofs < 0 || ofs >= sz)

59− then return ()

59+ then pure ()

60 else foreign FFI_C "array_poke" (Int -> Byte -> CData -> IO ()) ofs b ptr

61

62export

63pokeInt : Int -> Int -> ByteArray -> IO ()

64pokeInt ofs i (BA ptr sz)

65 = if (ofs < 0 || ofs+bytesPerInt > sz)

66− then return ()

66+ then pure ()

67 else foreign FFI_C "array_poke_int" (Int -> Int -> CData -> IO ()) ofs i ptr

68

69export

70copy : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO ()

71copy (BA srcPtr srcSz, srcIx) (BA dstPtr dstSz, dstIx) count

72 = if (srcIx < 0 || dstIx < 0 || (srcIx+count) > srcSz || (dstIx+count) > dstSz)

73− then return ()

73+ then pure ()

74 else foreign FFI_C "array_copy" (CData -> Int -> CData -> Int -> Int -> IO ()) srcPtr srcIx dstPtr dstIx count

75

76export

77fill : Int -> Int -> Byte -> ByteArray -> IO ()

78fill ofs count b (BA ptr sz)

79 = if (ofs < 0 || ofs+count > sz)

80− then return ()

80+ then pure ()

81 else foreign FFI_C "array_fill" (Int -> Int -> Byte -> CData -> IO ()) ofs count b ptr

82

83export

@@ -88,7 +88,7 @@ export

88compare : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO Int

89compare (BA ptrL szL, ofsL) (BA ptrR szR, ofsR) count

90 = if (ofsL < 0 || ofsL+count > szL || ofsR < 0 || ofsR+count > szR)

91− then return 0

91+ then pure 0

92 else foreign FFI_C "array_compare" (CData -> Int -> CData -> Int -> Int -> IO Int) ptrL ofsL ptrR ofsR count

93

94export

@@ -96,5 +96,5 @@ find : Byte -> ByteArray -> Int -> Int -> IO (Maybe Int)

96find b (BA ptr sz) ofs end = do

97 ofs <- foreign FFI_C "array_find" (Byte -> CData -> Int -> Int -> IO Int) b ptr ofs end

98 if ofs < 0

99− then return $ Nothing

99+ then pure $ Nothing

100− else return $ Just ofs

100+ else pure $ Just ofs

test/primitives006/Data/Bytes.idr+11−11

@@ -30,7 +30,7 @@ allocate capacity = do

30 arr <- BA.allocate (BA.bytesPerInt + capacity)

31 BA.pokeInt 0 dataOfs arr

32 BA.fill dataOfs capacity 0 arr -- zero the array

33− return $ B arr dataOfs dataOfs

33+ pure $ B arr dataOfs dataOfs

34

35export

36length : Bytes -> Int

@@ -59,7 +59,7 @@ grow factor (B arr ofs end) = do

59 else BA.size arr - ofs

60 B arr' ofs' end' <- allocate $ (factor*bytesAvailable) `max` minimalCapacity

61 BA.copy (arr, ofs) (arr', ofs') bytesUsed

62− return $ B arr' ofs' (ofs' + bytesUsed)

62+ pure $ B arr' ofs' (ofs' + bytesUsed)

63

64export

65snoc : Bytes -> Byte -> Bytes

@@ -68,17 +68,17 @@ snoc bs@(B arr ofs end) byte

68 if end >= BA.size arr

69 then unsafePerformIO $ do -- need more space

70 grown <- grow 2 bs

71− return $ snoc grown byte

71+ pure $ snoc grown byte

72 else unsafePerformIO $ do

73 maxUsed <- BA.peekInt 0 arr

74 if maxUsed > end

75 then do -- someone already took the headroom, need copying

76 copy <- grow 2 bs

77− return $ snoc copy byte

77+ pure $ snoc copy byte

78 else do -- can mutate

79 BA.pokeInt 0 (end+1) arr

80 BA.poke end byte arr

81− return $ B arr ofs (end+1)

81+ pure $ B arr ofs (end+1)

82

83infixl 7 |>

84export

@@ -97,7 +97,7 @@ namespace SnocView

97 then SnocView.Nil

98 else unsafePerformIO $ do

99 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

101

102namespace ConsView

103 data ConsView : Type where

@@ -111,7 +111,7 @@ namespace ConsView

111 then ConsView.Nil

112 else unsafePerformIO $ do

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

115

116infixr 7 ++

117export

@@ -121,17 +121,17 @@ export

121 if endL + countR > BA.size arrL

122 then unsafePerformIO $ do -- need more space

123 grown <- grow 2 bsL

124− return $ grown ++ bsR

124+ pure $ grown ++ bsR

125 else unsafePerformIO $ do

126 maxUsedL <- BA.peekInt 0 arrL

127 if maxUsedL > endL

128 then do -- headroom taken

129 copyL <- grow 2 bsL

130− return $ copyL ++ bsR

130+ pure $ copyL ++ bsR

131 else do -- can mutate

132 BA.pokeInt 0 (endL + countR) arrL

133 BA.copy (arrR, ofsR) (arrL, endL) countR

134− return $ B arrL ofsL (endL + countR)

134+ pure $ B arrL ofsL (endL + countR)

135

136export

137dropPrefix : Int -> Bytes -> Bytes

@@ -245,7 +245,7 @@ cmp (B arrL ofsL endL) (B arrR ofsR endR) = unsafePerformIO $ do

245 let countR = endR - ofsR

246 let commonCount = countL `min` countR

247 result <- BA.compare (arrL, ofsL) (arrR, ofsR) commonCount

248− return $

248+ pure $

249 if result /= 0

250 then i2o result

251 else compare countL countR

test/primitives006/load-test.idr+1−1

@@ -26,7 +26,7 @@ unit n b =

26 in printLn $ (show b ++ "/" ++ show n, length expanded, length elines)

27

28alloc : Int -> Int -> IO Int

29−alloc x 0 = return x

29+alloc x 0 = pure x

30alloc x i = do

31 -- allocate an array

32 arr <- BA.allocate (64 * 1024 * 1024)

test/proof003/test015.idr+1−1

@@ -68,7 +68,7 @@ readNum : IO Nat

68readNum = do putStr "Enter a number:"

69 i <- getLine

70 let n : Integer = cast i

71− return (fromInteger n)

71+ pure (fromInteger n)

72

73main : IO ()

74main = 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

347getRequest : EvalState iface hs -> Maybe (Ptr, (ty ** (Nat, iface ty)), EvalState iface hs)

348getRequest (MkEvalState queue reply clients nh)

349 = do (pid, req, queue') <- removeReq [] queue

350− return (pid, req, MkEvalState queue' reply clients nh)

350+ pure (pid, req, MkEvalState queue' reply clients nh)

351

352countClients : EvalState iface hs -> (Nat, EvalState iface hs)

353countClients (MkEvalState queue reply clients nh)

test/reg040/reg040.idr+1−1

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

1-- The regression that this tests for is defunct unsafePerformIO

2

3io : IO Int

4−io = return 42

4+io = pure 42

5

6main : IO ()

7main = printLn $ unsafePerformIO io

test/reg048/reg048.idr+1−1

@@ -10,7 +10,7 @@ test xs = do let lst = Data.SortedMap.toList mp

10 if length found /= n

11 then putStrLn $ "some lost in " ++ show xs ++ ": res=" ++ show res

12 ++ " toList=" ++ show lst

13− else return ()

13+ else pure ()

14

15 where

16 mp : SortedMap Int ()

test/reg052/reg052.idr+2−2

@@ -1,8 +1,8 @@

1impure_op : Bits64 -> IO Bits64

2−impure_op foo = return $ foo + 1

2+impure_op foo = pure $ foo + 1

3

4impure_int : IO Int

5−impure_int = return 41

5+impure_int = pure 41

6

7main : IO ()

8main = impure_int >>= impure_op . prim__zextInt_B64 >>= printLn

test/sugar003/test013.idr+1−1

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

1module Main

2

3forLoop : List a -> (a -> IO ()) -> IO ()

4−forLoop [] f = return ()

4+forLoop [] f = pure ()

5forLoop (x :: xs) f = do f x

6 forLoop xs f

7

test/unique004/unique002.idr+1−1

@@ -15,6 +15,6 @@ foo : UList Int -> IO ()

15foo xs = do -- let f = \x : Int => showU xs

16 putStrLn $ free xs

17 putStrLn $ f 42 xs

18− return ()

18+ pure ()

19 where f : Int -> Borrowed (UList Int) -> String

20 f x xs = showU xs

test/unique004/unique002a.idr+1−1

@@ -15,4 +15,4 @@ foo : UList Int -> IO ()

15foo xs = do let f = \x : Int => showU xs

16 putStrLn $ free xs

17 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

19 putStrLn (f 10)

20 putStrLn $ free xs

21 putStrLn (f 10)

22− return ()

22+ pure ()