cc1c4ed · Idris-dev · git.iko.soy

CHANGELOG.md+1

compare with master

unifiedsplit

@@ -55,6 +55,7 @@

55+ `Prelude.Doubles.atan2` is now implemented as a primitive instead of

56 being coded in Idris.

57+ Added `Test.Unit` to `contrib` for simple unit testing.

58++ Removed several deprecated items from the libraries shipped with Idris.

58+ Moved `abs` from the `Neg` interface into its own `Abs` interface. `Nat`

59+ Moved `abs` from the `Neg` interface into its own `Abs` interface. `Nat`

59 implements `Abs` with `abs = id`.

60 implements `Abs` with `abs = id`.

60

61

docs/tutorial/views.rst+42−15

@@ -33,24 +33,36 @@ rule, inspired by views in ``Epigram`` [1]_, which takes account of

33the fact that matching on a value in a dependently typed language can

34affect what we know about the forms of other values. In its simplest

35form, the ``with`` rule adds another argument to the function being

36+defined.

37+

36−defined, e.g. we have already seen a vector filter function, defined

38+We have already seen a vector filter function. This time, we define it

37−as follows:

39+using ``with`` as follows:

38

40

39.. code-block:: idris

41.. code-block:: idris

40

42

41 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)

43 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)

42 filter p [] = ( _ ** [] )

44 filter p [] = ( _ ** [] )

43 filter p (x :: xs) with (filter p xs)

45 filter p (x :: xs) with (filter p xs)

44− | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

46+ filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

45

47

46Here, the ``with`` clause allows us to deconstruct the result of

48Here, the ``with`` clause allows us to deconstruct the result of

47−``filter p xs``. Effectively, it adds this value as an extra argument,

49+``filter p xs``. The view refined argument pattern ``filter p (x ::

48−which we place after the vertical bar.

50+xs)`` goes beneath the ``with`` clause, followed by a vertical bar

51+``|``, followed by the deconstructed intermediate result ``( _ ** xs'

52+)``. If the view refined argument pattern is unchanged from the

53+original function argument pattern, then the left side of ``|`` is

54+extraneous and may be omitted:

55+

56+.. code-block:: idris

57+

58+ filter p (x :: xs) with (filter p xs)

59+ | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

49

60

50If the intermediate computation itself has a dependent type, then the

61If the intermediate computation itself has a dependent type, then the

51result can affect the forms of other arguments — we can learn the form

62result can affect the forms of other arguments — we can learn the form

63+of one value by testing another. In these cases, view refined argument

52−of one value by testing another. For example, a ``Nat`` is either even

64+patterns must be explicit. For example, a ``Nat`` is either even or

53−or odd. If it’s even it will be the sum of two equal ``Nat``.

65+odd. If it is even it will be the sum of two equal ``Nat``.

54Otherwise, it is the sum of two equal ``Nat`` plus one:

66Otherwise, it is the sum of two equal ``Nat`` plus one:

55

67

56.. code-block:: idris

68.. code-block:: idris

@@ -80,14 +92,29 @@ rule:

80 natToBin (j + j) | Even = False :: natToBin j

92 natToBin (j + j) | Even = False :: natToBin j

81 natToBin (S (j + j)) | Odd = True :: natToBin j

93 natToBin (S (j + j)) | Odd = True :: natToBin j

82

94

83−The value of the result of ``parity k`` affects the form of ``k``,

95+The value of ``parity k`` affects the form of ``k``, because the

84−because the result of ``parity k`` depends on ``k``. So, as well as

96+result of ``parity k`` depends on ``k``. So, as well as the patterns

85−the patterns for the result of the intermediate computation (``Even``

97+for the result of the intermediate computation (``Even`` and ``Odd``)

86−and ``odd``) right of the ``|``, we also write how the results

98+right of the ``|``, we also write how the results affect the other

87−affect the other patterns left of the ``|``. Note that there is

99+patterns left of the ``|``. That is:

100+

101+- When ``parity k`` evaluates to ``Even``, we can refine the original

102+ argument ``k`` to a refined pattern ``(j + j)`` according to

103+ ``Parity (n + n)`` from the ``Even`` constructor definition. So

104+ ``(j + j)`` replaces ``k`` on the left side of ``|``, and the

105+ ``Even`` constructor appears on the right side. The natural number

106+ ``j`` in the refined pattern can be used on the ride side of the

107+ ``=`` sign.

108+

109+- Otherwise, when ``parity k`` evaluates to ``Odd``, the original

110+ argument ``k`` is refined to ``S (j + j)`` according to ``Parity (S

111+ (n + n))`` from the ``Odd`` constructor definition, and ``Odd`` now

112+ appears on the ride side of ``|``, again with the natural number

113+ ``j`` used on the ride side of the ``=`` sign.

114+

88−a function in the patterns (``+``) and repeated occurrences of

115+Note that there is a function in the patterns (``+``) and repeated

89−``j``—this is allowed because another argument has determined the form

116+occurrences of ``j`` - this is allowed because another argument has

90−of these patterns.

117+determined the form of these patterns.

91

118

92We will return to this function in the next section :ref:`sect-parity` to

119We will return to this function in the next section :ref:`sect-parity` to

93complete the definition of ``parity``.

120complete the definition of ``parity``.

libs/effects/Effects.idr−5

@@ -306,11 +306,6 @@ toEff xs' = id

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

307pure = Value

308

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

310−return = pure

311−

312−%deprecate Effects.return "Please use `pure`."

313−

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

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

315pureM = Value

310pureM = Value

316

311

libs/prelude/Builtins.idr+4−18

@@ -51,14 +51,6 @@ namespace Builtins

51 data DPair : (a : Type) -> (P : a -> Type) -> Type where

52 MkDPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P

53

54− Sigma : (a : Type) -> (P : a -> Type) -> Type

55− Sigma wit prf = DPair wit prf

56− %deprecate Sigma "This name is being deprecated in favour of `DPair`."

57−

58− MkSigma : .{P : a -> Type} -> (x : a) -> (prf : P x) -> DPair a P

59− MkSigma wit prf = MkDPair wit prf

60− %deprecate MkSigma "This constructor is being deprecated in favour of `MkDPair`."

61−

62||| The empty type, also known as the trivially false proposition.

54||| The empty type, also known as the trivially false proposition.

63|||

55|||

64||| Use `void` or `absurd` to prove anything if you have a variable of type `Void` in scope.

56||| Use `void` or `absurd` to prove anything if you have a variable of type `Void` in scope.

@@ -130,14 +122,14 @@ data Delayed : DelayReason -> Type -> Type where

130Force : {t, a : _} -> Delayed t a -> a

122Force : {t, a : _} -> Delayed t a -> a

131Force (Delay x) = x

123Force (Delay x) = x

132

124

133−||| Lazily evaluated values.

125+||| Lazily evaluated values.

134||| At run time, the delayed value will only be computed when required by

126||| At run time, the delayed value will only be computed when required by

135||| a case split.

127||| a case split.

136%error_reverse

128%error_reverse

137Lazy : Type -> Type

129Lazy : Type -> Type

138Lazy t = Delayed LazyValue t

130Lazy t = Delayed LazyValue t

139

131

140−||| Possibly infinite data.

132+||| Possibly infinite data.

141||| A value which may be infinite is accepted by the totality checker if

133||| A value which may be infinite is accepted by the totality checker if

142||| it appears under a data constructor. At run time, the delayed value will

134||| it appears under a data constructor. At run time, the delayed value will

143||| only be computed when required by a case split.

135||| only be computed when required by a case split.

@@ -187,22 +179,16 @@ idris_crash : (msg : String) -> a

187

179

188||| Subvert the type checker. This function is abstract, so it will not reduce in

180||| Subvert the type checker. This function is abstract, so it will not reduce in

189||| the type checker. Use it with care - it can result in segfaults or worse!

181||| the type checker. Use it with care - it can result in segfaults or worse!

190−export

182+export

191believe_me : a -> b

183believe_me : a -> b

192believe_me x = assert_total (prim__believe_me _ _ x)

184believe_me x = assert_total (prim__believe_me _ _ x)

193

185

194||| Subvert the type checker. This function *will* reduce in the type checker.

186||| Subvert the type checker. This function *will* reduce in the type checker.

195||| Use it with extreme care - it can result in segfaults or worse!

187||| Use it with extreme care - it can result in segfaults or worse!

196−public export

188+public export

197really_believe_me : a -> b

189really_believe_me : a -> b

198really_believe_me x = assert_total (prim__believe_me _ _ x)

190really_believe_me x = assert_total (prim__believe_me _ _ x)

199

191

200−||| Deprecated alias for `Double`, for the purpose of backwards

201−||| compatibility. Idris does not support 32 bit floats at present.

202−Float : Type

203−Float = Double

204−%deprecate Float

205−

206-- Pointers as external primitive; there's no literals for these, so no

192-- Pointers as external primitive; there's no literals for these, so no

207-- need for them to be part of the compiler.

193-- need for them to be part of the compiler.

208

194

libs/prelude/Language/Reflection.idr+1−9

@@ -74,14 +74,6 @@ mutual

74 | MetaN TTName TTName

75 %name SpecialName sn, sn'

76

77−InstanceN : TTName -> (List String) -> SpecialName

78−InstanceN = ImplementationN

79−%deprecate InstanceN "`InstanceN` is deprecated, Please use `ImplementationN` instead."

80−

81−InstanceCtorN : TTName -> SpecialName

82−InstanceCtorN = ImplementationCtorN

83−%deprecate InstanceCtorN "`InstanceCtorN` is deprecated, Please use `ImplementationCtorN` instead."

84−

85-- Rather than implement one-off private functions, we make the

77-- Rather than implement one-off private functions, we make the

86-- disjointness of the constructors available to all Idris programs,

78-- disjointness of the constructors available to all Idris programs,

87-- at the cost of a bit of scrolling here.

79-- at the cost of a bit of scrolling here.

@@ -410,7 +402,7 @@ mutual

410 private

402 private

411 implementationNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys)

403 implementationNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys)

412 implementationNInj Refl = (Refl, Refl)

404 implementationNInj Refl = (Refl, Refl)

413−

405+

414 private

406 private

415 parentNInj : (ParentN n x = ParentN n' y) -> (n = n', x = y)

407 parentNInj : (ParentN n x = ParentN n' y) -> (n = n', x = y)

416 parentNInj Refl = (Refl, Refl)

408 parentNInj Refl = (Refl, Refl)

libs/prelude/Language/Reflection/Elab.idr−6

@@ -560,11 +560,6 @@ namespace Tactics

560 addImplementation : (ifaceName, implName : TTName) -> Elab ()

561 addImplementation ifaceName implName = Prim__AddImplementation ifaceName implName

562

563− export

564− addInstance : (ifaceName, implName : TTName) -> Elab ()

565− addInstance = addImplementation

566− %deprecate addInstance "`addInstance` is deprecated, Please use `addImplementation` instead."

567−

568 ||| Determine whether a name denotes an interface.

563 ||| Determine whether a name denotes an interface.

569 |||

564 |||

570 ||| @ name a name that might denote an interface.

565 ||| @ name a name that might denote an interface.

@@ -769,4 +764,3 @@ implementation Quotable Datatype Raw where

769 quotedTy = `(Datatype)

764 quotedTy = `(Datatype)

770 quote (MkDatatype name tyConArgs tyConRes constructors) =

765 quote (MkDatatype name tyConArgs tyConRes constructors) =

771 `(MkDatatype ~(quote name) ~(quote tyConArgs) ~(quote tyConRes) ~(quote constructors))

766 `(MkDatatype ~(quote name) ~(quote tyConArgs) ~(quote tyConRes) ~(quote constructors))

772−

libs/prelude/Prelude/Bits.idr−25

@@ -111,28 +111,3 @@ b32ToBinString c = concatMap b8ToBinString (b32ToBytes c)

111||| Encode `Bits64` as a 64-character binary string.

112b64ToBinString : Bits64 -> String

113b64ToBinString c = concatMap b8ToBinString (b64ToBytes c)

114−

115−

116−--------------------------------------------------------------------------------

117−-- Deprecated String Functions

118−--------------------------------------------------------------------------------

119−

120−||| Encode `Bits8` as a 2-character hex string.

121−b8ToString : Bits8 -> String

122−b8ToString = b8ToHexString

123−%deprecate b8ToString "Please use `b8ToHexString` instead."

124−

125−||| Encode `Bits16` as a 4-character hex string.

126−b16ToString : Bits16 -> String

127−b16ToString = b16ToHexString

128−%deprecate b16ToString "Please use `b16ToHexString` instead."

129−

130−||| Encode `Bits32` as a 8-character hex string.

131−b32ToString : Bits32 -> String

132−b32ToString = b32ToHexString

133−%deprecate b32ToString "Please use `b32ToHexString` instead."

134−

135−||| Encode `Bits64` as a 16-character hex string.

136−b64ToString : Bits64 -> String

137−b64ToString = b64ToHexString

138−%deprecate b64ToString "Please use `b64ToHexString` instead."

libs/prelude/Prelude/File.idr+8−31

@@ -27,7 +27,7 @@ data File : Type where

27||| An error from a file operation

28-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure

29-- the values correspond!

30−

30+

31data FileError = GenericFileError Int -- errno

32 | FileReadError

33 | FileWriteError

@@ -102,10 +102,6 @@ validFile (FHandle h) = do x <- nullPtr h

102||| Modes for opening files

104

105−Write : Mode

106−Write = WriteTruncate

107−%deprecate Write "Please use WriteTruncate instead."

108−

109modeStr : Mode -> String

105modeStr : Mode -> String

110modeStr Read = "r"

106modeStr Read = "r"

111modeStr WriteTruncate = "w"

107modeStr WriteTruncate = "w"

@@ -142,12 +138,12 @@ do_getFileSize h = foreign FFI_C "fileSize" (Ptr -> IO Int) h

142

138

143||| Return the size of a File

139||| Return the size of a File

144||| Returns an error if the File is not an ordinary file (e.g. a directory)

140||| Returns an error if the File is not an ordinary file (e.g. a directory)

145−||| Also note that this currently returns an Int, which may overflow if the

141+||| Also note that this currently returns an Int, which may overflow if the

146||| file is very big

142||| file is very big

147export

143export

148fileSize : File -> IO (Either FileError Int)

144fileSize : File -> IO (Either FileError Int)

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

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

150− if (s < 0)

146+ if (s < 0)

151 then do err <- getFileError

147 then do err <- getFileError

152 pure (Left err)

148 pure (Left err)

153 else pure (Right s)

149 else pure (Right s)

@@ -187,21 +183,16 @@ export

187pclose : File -> IO ()

183pclose : File -> IO ()

188pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h

184pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h

189

185

190−-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))

191−-- prim__vm h

192−

193−export

194−fread : File -> IO (Either FileError String)

195−fread (FHandle h) = do str <- do_fread h

196− if !(ferror (FHandle h))

197− then pure (Left FileReadError)

198− else pure (Right str)

199

186

200||| Read a line from a file

187||| Read a line from a file

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

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

202export

189export

203fGetLine : (h : File) -> IO (Either FileError String)

190fGetLine : (h : File) -> IO (Either FileError String)

204−fGetLine = fread

191+fGetLine (FHandle h) = do

192+ str <- do_fread h

193+ if !(ferror (FHandle h))

194+ then pure (Left FileReadError)

195+ else pure (Right str)

205

196

206||| Read up to a number of characters from a file

197||| Read up to a number of characters from a file

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

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

@@ -212,7 +203,6 @@ fGetChars (FHandle h) len = do str <- do_freadChars h len

212 then pure (Left FileReadError)

203 then pure (Left FileReadError)

213 else pure (Right str)

204 else pure (Right str)

214

205

215−%deprecate fread "Use fGetLine instead"

216

206

217private

207private

218do_fwrite : Ptr -> String -> IO (Either FileError ())

208do_fwrite : Ptr -> String -> IO (Either FileError ())

@@ -225,10 +215,6 @@ do_fwrite h s = do res <- prim_fwrite h s

225 pure (Left err)

215 pure (Left err)

226 else pure (Right ())

216 else pure (Right ())

227

217

228−export

229−fwrite : File -> String -> IO (Either FileError ())

230−fwrite (FHandle h) s = do_fwrite h s

231−

232||| Write a line to a file

218||| Write a line to a file

233||| @h a file handle which must be open for writing

219||| @h a file handle which must be open for writing

234||| @str the line to write to the file

220||| @str the line to write to the file

@@ -240,8 +226,6 @@ export

240fPutStrLn : File -> String -> IO (Either FileError ())

226fPutStrLn : File -> String -> IO (Either FileError ())

241fPutStrLn (FHandle h) s = do_fwrite h (s ++ "\n")

227fPutStrLn (FHandle h) s = do_fwrite h (s ++ "\n")

242

228

243−%deprecate fwrite "Use fPutStr instead"

244−

245private

229private

246do_feof : Ptr -> IO Int

230do_feof : Ptr -> IO Int

247do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h

231do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h

@@ -252,13 +236,6 @@ fEOF : File -> IO Bool

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

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

253 pure (not (eof == 0))

237 pure (not (eof == 0))

254

238

255−||| Check if a file handle has reached the end

256−export

257−feof : File -> IO Bool

258−feof = fEOF

259−

260−%deprecate feof "Use fEOF instead"

261−

262export

239export

263fpoll : File -> IO Bool

240fpoll : File -> IO Bool

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

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

libs/prelude/Prelude/Monad.idr+2−7

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

1+||| Monads and Functors

1module Prelude.Monad

2module Prelude.Monad

2

3

3−-- Monads and Functors

4−

5import Builtins

4import Builtins

6import Prelude.Functor

5import Prelude.Functor

7import public Prelude.Applicative

6import public Prelude.Applicative

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

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

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

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

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

30return = pure

29return = pure

31−%deprecate return "Please use `pure`, which is equivalent."

30+%fragile return "`return` is provided for those coming from Haskell. Please use `pure` instead, which is equivalent."

32−

33−flatten : Monad m => m (m a) -> m a

34−flatten = join

35−%deprecate flatten "Please use `join`, which is the standard name."

36

31

37||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.

32||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.

38||| Consequently, the final value is wrapped in the same `Monad`.

33||| Consequently, the final value is wrapped in the same `Monad`.

libs/prelude/Prelude/Pairs.idr−8

@@ -41,13 +41,5 @@ using (a : Type, P : a -> Type)

41 snd : (x : DPair a P) -> P (fst x)

42 snd (x ** pf) = pf

43

44− getWitness : DPair a P -> a

45− getWitness = fst

46− %deprecate DPair.getWitness "This is being deprecated in favour of `fst`."

47−

48− getProof : (x : DPair a P) -> P (fst x)

49− getProof = snd

50− %deprecate DPair.getProof "This is being deprecated in favour of `snd`."

51−

52 -- Polymorphic (interface-based) projections have been removed

44 -- Polymorphic (interface-based) projections have been removed

53 -- because type-directed name disambiguation works better.

45 -- because type-directed name disambiguation works better.