git.iko.soy/Idris-dev
on master help sign in
Change export qualifier keywords
68c019aEdwin Brady
CHANGELOG+11−1
compare with master
unifiedsplit
@@ -1,12 +1,22 @@
1New in 0.11:
1New in 0.11:
2============
2============
3
3
4+Updated export rules
5+--------------------
6+
4−* The export rules have been simplified. Now:
7+* The export rules are:
5 - 'private' means that the definition is not exported at all
8 - 'private' means that the definition is not exported at all
6 - 'export' means that the top level type is exported, but not the
9 - 'export' means that the top level type is exported, but not the
7 definition. In the case of 'data', this means the type constructor is
10 definition. In the case of 'data', this means the type constructor is
8 exported but not the data constructors.
11 exported but not the data constructors.
9 - 'public export' means that the entire definition is exported.
12 - 'public export' means that the entire definition is exported.
13+* Exported names can only refer to things with at least the same level of
14+ visibility. That is:
15+ - 'private' definitions can refer to anything
16+ - 'export' definitions can refer to 'export' or 'public' definitions
17+ in their types
18+ - 'public export' definitions can refer only to other 'public export'
19+ definitions in their types and definitions
10* By default, names are 'private'. This can be altered with an %access
20* By default, names are 'private'. This can be altered with an %access
11 directive as before.
21 directive as before.
12
22
libs/base/Control/Arrow.idr+1−1
@@ -3,7 +3,7 @@ module Control.Arrow
3import Data.Morphisms
3import Data.Morphisms
4import Control.Category
4import Control.Category
5
5
6−%access public
6+%access public export
7
7
8infixr 5 <++>
8infixr 5 <++>
9infixr 3 ***
9infixr 3 ***
libs/base/Control/Catchable.idr+1−1
@@ -2,7 +2,7 @@ module Control.Catchable
2
2
3import Control.IOExcept
3import Control.IOExcept
4
4
5−%access public
5+%access public export
6
6
7interface Catchable (m : Type -> Type) t where
7interface Catchable (m : Type -> Type) t where
8 throw : t -> m a
8 throw : t -> m a
libs/base/Control/Category.idr+1−1
@@ -2,7 +2,7 @@ module Control.Category
2
2
3import Data.Morphisms
3import Data.Morphisms
4
4
5−%access public
5+%access public export
6
6
7interface Category (cat : Type -> Type -> Type) where
7interface Category (cat : Type -> Type -> Type) where
8 id : cat a a
8 id : cat a a
libs/base/Control/IOExcept.idr+1−1
@@ -1,6 +1,6 @@
1module Control.IOExcept
1module Control.IOExcept
2
2
3−%access public
3+%access public export
4
4
5-- An IO monad with exception handling
5-- An IO monad with exception handling
6
6
libs/base/Control/Isomorphism.idr+1−1
@@ -4,7 +4,7 @@ import Syntax.PreorderReasoning
4import Data.Fin
4import Data.Fin
5
5
6%default total
6%default total
7−%access public
7+%access public export
8
8
9||| An isomorphism between two types
9||| An isomorphism between two types
10data Iso : Type -> Type -> Type where
10data Iso : Type -> Type -> Type where
libs/base/Control/Monad/Identity.idr+2−2
@@ -1,8 +1,8 @@
1module Control.Monad.Identity
1module Control.Monad.Identity
2
2
3−%access public
3+%access public export
4
4
5−public record Identity (a : Type) where
5+public export record Identity (a : Type) where
6 constructor Id
6 constructor Id
7 runIdentity : a
7 runIdentity : a
8
8
libs/base/Control/Monad/RWS.idr+1−1
@@ -5,7 +5,7 @@ import Control.Monad.State
5import Control.Monad.Writer
5import Control.Monad.Writer
6import Control.Monad.Reader
6import Control.Monad.Reader
7
7
8−%access public
8+%access public export
9
9
10||| A combination of the Reader, Writer, and State monads
10||| A combination of the Reader, Writer, and State monads
11interface (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) where {}
11interface (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) where {}
libs/base/Control/Monad/Reader.idr+1−1
@@ -4,7 +4,7 @@ import Builtins
4import Control.Monad.Identity
4import Control.Monad.Identity
5import Control.Monad.Trans
5import Control.Monad.Trans
6
6
7−%access public
7+%access public export
8
8
9||| A monad representing a computation that runs in an immutable context
9||| A monad representing a computation that runs in an immutable context
10interface Monad m => MonadReader r (m : Type -> Type) where
10interface Monad m => MonadReader r (m : Type -> Type) where
libs/base/Control/Monad/State.idr+1−1
@@ -3,7 +3,7 @@ module Control.Monad.State
3import public Control.Monad.Identity
3import public Control.Monad.Identity
4import public Control.Monad.Trans
4import public Control.Monad.Trans
5
5
6−%access public
6+%access public export
7
7
8||| A computation which runs in a context and produces an output
8||| A computation which runs in a context and produces an output
9interface Monad m => MonadState s (m : Type -> Type) | m where
9interface Monad m => MonadState s (m : Type -> Type) | m where
libs/base/Control/Monad/Trans.idr+1−1
@@ -1,6 +1,6 @@
1module Control.Monad.Trans
1module Control.Monad.Trans
2
2
3−%access public
3+%access public export
4
4
5interface MonadTrans (t : (Type -> Type) -> Type -> Type) where
5interface MonadTrans (t : (Type -> Type) -> Type -> Type) where
6 lift : Monad m => m a -> t m a
6 lift : Monad m => m a -> t m a
libs/base/Control/Monad/Writer.idr+1−1
@@ -4,7 +4,7 @@ import Builtins
4import Control.Monad.Identity
4import Control.Monad.Identity
5import Control.Monad.Trans
5import Control.Monad.Trans
6
6
7−%access public
7+%access public export
8
8
9||| A monad representing a computation that produces a stream of output
9||| A monad representing a computation that produces a stream of output
10interface (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where
10interface (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where
libs/base/Data/Bits.idr+27−27
@@ -4,7 +4,7 @@ import Data.Fin
4
4
5%default total
5%default total
6
6
7−public
7+public export
8nextPow2 : Nat -> Nat
8nextPow2 : Nat -> Nat
9nextPow2 Z = Z
9nextPow2 Z = Z
10nextPow2 (S x) = if (S x) == (2 `power` l2x)
10nextPow2 (S x) = if (S x) == (2 `power` l2x)
@@ -13,11 +13,11 @@ nextPow2 (S x) = if (S x) == (2 `power` l2x)
13 where
13 where
14 l2x = log2NZ (S x) SIsNotZ
14 l2x = log2NZ (S x) SIsNotZ
15
15
16−public
16+public export
17nextBytes : Nat -> Nat
17nextBytes : Nat -> Nat
18nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
18nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
19
19
20−public
20+public export
21machineTy : Nat -> Type
21machineTy : Nat -> Type
22machineTy Z = Bits8
22machineTy Z = Bits8
23machineTy (S Z) = Bits16
23machineTy (S Z) = Bits16
@@ -47,7 +47,7 @@ natToBits {n=n} x with (n)
47getPad : Nat -> machineTy n
47getPad : Nat -> machineTy n
48getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)
48getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)
49
49
50−public
50+public export
51data Bits : Nat -> Type where
51data Bits : Nat -> Type where
52 MkBits : machineTy (nextBytes n) -> Bits n
52 MkBits : machineTy (nextBytes n) -> Bits n
53
53
@@ -99,7 +99,7 @@ shiftLeft' {n=n} x c with (nextBytes n)
99 | S (S Z) = pad32' n prim__shlB32 x c
99 | S (S Z) = pad32' n prim__shlB32 x c
100 | S (S (S _)) = pad64' n prim__shlB64 x c
100 | S (S (S _)) = pad64' n prim__shlB64 x c
101
101
102−public
102+public export
103shiftLeft : Bits n -> Bits n -> Bits n
103shiftLeft : Bits n -> Bits n -> Bits n
104shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
104shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
105
105
@@ -110,7 +110,7 @@ shiftRightLogical' {n=n} x c with (n)
110 | S (S Z) = prim__lshrB32 x c
110 | S (S Z) = prim__lshrB32 x c
111 | S (S (S _)) = prim__lshrB64 x c
111 | S (S (S _)) = prim__lshrB64 x c
112
112
113−public
113+public export
114shiftRightLogical : Bits n -> Bits n -> Bits n
114shiftRightLogical : Bits n -> Bits n -> Bits n
115shiftRightLogical {n} (MkBits x) (MkBits y)
115shiftRightLogical {n} (MkBits x) (MkBits y)
116 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)
116 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)
@@ -122,7 +122,7 @@ shiftRightArithmetic' {n=n} x c with (nextBytes n)
122 | S (S Z) = pad32' n prim__ashrB32 x c
122 | S (S Z) = pad32' n prim__ashrB32 x c
123 | S (S (S _)) = pad64' n prim__ashrB64 x c
123 | S (S (S _)) = pad64' n prim__ashrB64 x c
124
124
125−public
125+public export
126shiftRightArithmetic : Bits n -> Bits n -> Bits n
126shiftRightArithmetic : Bits n -> Bits n -> Bits n
127shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
127shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
128
128
@@ -133,7 +133,7 @@ and' {n=n} x y with (n)
133 | S (S Z) = prim__andB32 x y
133 | S (S Z) = prim__andB32 x y
134 | S (S (S _)) = prim__andB64 x y
134 | S (S (S _)) = prim__andB64 x y
135
135
136−public
136+public export
137and : Bits n -> Bits n -> Bits n
137and : Bits n -> Bits n -> Bits n
138and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
138and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
139
139
@@ -144,7 +144,7 @@ or' {n=n} x y with (n)
144 | S (S Z) = prim__orB32 x y
144 | S (S Z) = prim__orB32 x y
145 | S (S (S _)) = prim__orB64 x y
145 | S (S (S _)) = prim__orB64 x y
146
146
147−public
147+public export
148or : Bits n -> Bits n -> Bits n
148or : Bits n -> Bits n -> Bits n
149or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
149or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
150
150
@@ -155,7 +155,7 @@ xor' {n=n} x y with (n)
155 | S (S Z) = prim__xorB32 x y
155 | S (S Z) = prim__xorB32 x y
156 | S (S (S _)) = prim__xorB64 x y
156 | S (S (S _)) = prim__xorB64 x y
157
157
158−public
158+public export
159xor : Bits n -> Bits n -> Bits n
159xor : Bits n -> Bits n -> Bits n
160xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
160xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
161
161
@@ -166,7 +166,7 @@ plus' {n=n} x y with (nextBytes n)
166 | S (S Z) = pad32 n prim__addB32 x y
166 | S (S Z) = pad32 n prim__addB32 x y
167 | S (S (S _)) = pad64 n prim__addB64 x y
167 | S (S (S _)) = pad64 n prim__addB64 x y
168
168
169−public
169+public export
170plus : Bits n -> Bits n -> Bits n
170plus : Bits n -> Bits n -> Bits n
171plus (MkBits x) (MkBits y) = MkBits (plus' x y)
171plus (MkBits x) (MkBits y) = MkBits (plus' x y)
172
172
@@ -177,7 +177,7 @@ minus' {n=n} x y with (nextBytes n)
177 | S (S Z) = pad32 n prim__subB32 x y
177 | S (S Z) = pad32 n prim__subB32 x y
178 | S (S (S _)) = pad64 n prim__subB64 x y
178 | S (S (S _)) = pad64 n prim__subB64 x y
179
179
180−public
180+public export
181minus : Bits n -> Bits n -> Bits n
181minus : Bits n -> Bits n -> Bits n
182minus (MkBits x) (MkBits y) = MkBits (minus' x y)
182minus (MkBits x) (MkBits y) = MkBits (minus' x y)
183
183
@@ -188,7 +188,7 @@ times' {n=n} x y with (nextBytes n)
188 | S (S Z) = pad32 n prim__mulB32 x y
188 | S (S Z) = pad32 n prim__mulB32 x y
189 | S (S (S _)) = pad64 n prim__mulB64 x y
189 | S (S (S _)) = pad64 n prim__mulB64 x y
190
190
191−public
191+public export
192times : Bits n -> Bits n -> Bits n
192times : Bits n -> Bits n -> Bits n
193times (MkBits x) (MkBits y) = MkBits (times' x y)
193times (MkBits x) (MkBits y) = MkBits (times' x y)
194
194
@@ -200,7 +200,7 @@ sdiv' {n=n} x y with (nextBytes n)
200 | S (S Z) = prim__sdivB32 x y
200 | S (S Z) = prim__sdivB32 x y
201 | S (S (S _)) = prim__sdivB64 x y
201 | S (S (S _)) = prim__sdivB64 x y
202
202
203−public partial
203+public export partial
204sdiv : Bits n -> Bits n -> Bits n
204sdiv : Bits n -> Bits n -> Bits n
205sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
205sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
206
206
@@ -212,7 +212,7 @@ udiv' {n=n} x y with (nextBytes n)
212 | S (S Z) = prim__udivB32 x y
212 | S (S Z) = prim__udivB32 x y
213 | S (S (S _)) = prim__udivB64 x y
213 | S (S (S _)) = prim__udivB64 x y
214
214
215−public partial
215+public export partial
216udiv : Bits n -> Bits n -> Bits n
216udiv : Bits n -> Bits n -> Bits n
217udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
217udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
218
218
@@ -224,7 +224,7 @@ srem' {n=n} x y with (nextBytes n)
224 | S (S Z) = prim__sremB32 x y
224 | S (S Z) = prim__sremB32 x y
225 | S (S (S _)) = prim__sremB64 x y
225 | S (S (S _)) = prim__sremB64 x y
226
226
227−public partial
227+public export partial
228srem : Bits n -> Bits n -> Bits n
228srem : Bits n -> Bits n -> Bits n
229srem (MkBits x) (MkBits y) = MkBits (srem' x y)
229srem (MkBits x) (MkBits y) = MkBits (srem' x y)
230
230
@@ -236,7 +236,7 @@ urem' {n=n} x y with (nextBytes n)
236 | S (S Z) = prim__uremB32 x y
236 | S (S Z) = prim__uremB32 x y
237 | S (S (S _)) = prim__uremB64 x y
237 | S (S (S _)) = prim__uremB64 x y
238
238
239−public partial
239+public export partial
240urem : Bits n -> Bits n -> Bits n
240urem : Bits n -> Bits n -> Bits n
241urem (MkBits x) (MkBits y) = MkBits (urem' x y)
241urem (MkBits x) (MkBits y) = MkBits (urem' x y)
242
242
@@ -302,7 +302,7 @@ complement' {n=n} x with (nextBytes n)
302 | S (S (S _)) = let pad = getPad {n=3} n in
302 | S (S (S _)) = let pad = getPad {n=3} n in
303 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
303 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
304
304
305−public
305+public export
306complement : Bits n -> Bits n
306complement : Bits n -> Bits n
307complement (MkBits x) = MkBits (complement' x)
307complement (MkBits x) = MkBits (complement' x)
308
308
@@ -321,7 +321,7 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
321 | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))
321 | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))
322 | (S (S (S _)), S (S (S _))) = believe_me x
322 | (S (S (S _)), S (S (S _))) = believe_me x
323
323
324−public
324+public export
325zeroExtend : Bits n -> Bits (n+m)
325zeroExtend : Bits n -> Bits (n+m)
326zeroExtend (MkBits x) = MkBits (zext' x)
326zeroExtend (MkBits x) = MkBits (zext' x)
327
327
@@ -337,7 +337,7 @@ intToBits' {n=n} x with (nextBytes n)
337 | S (S (S _)) = let pad = getPad {n=3} n in
337 | S (S (S _)) = let pad = getPad {n=3} n in
338 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad
338 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad
339
339
340−public
340+public export
341intToBits : Integer -> Bits n
341intToBits : Integer -> Bits n
342intToBits n = MkBits (intToBits' n)
342intToBits n = MkBits (intToBits' n)
343
343
@@ -351,7 +351,7 @@ bitsToInt' {n=n} x with (nextBytes n)
351 | S (S Z) = prim__zextB32_BigInt x
351 | S (S Z) = prim__zextB32_BigInt x
352 | S (S (S _)) = prim__zextB64_BigInt x
352 | S (S (S _)) = prim__zextB64_BigInt x
353
353
354−public
354+public export
355bitsToInt : Bits n -> Integer
355bitsToInt : Bits n -> Integer
356bitsToInt (MkBits x) = bitsToInt' x
356bitsToInt (MkBits x) = bitsToInt' x
357
357
@@ -393,7 +393,7 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
393 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
393 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
394 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
394 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
395
395
396−--public
396+--public export
397--signExtend : Bits n -> Bits (n+m)
397--signExtend : Bits n -> Bits (n+m)
398--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
398--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
399
399
@@ -412,23 +412,23 @@ trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))
412 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
412 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
413 | (S (S (S _)), S (S (S _))) = believe_me x
413 | (S (S (S _)), S (S (S _))) = believe_me x
414
414
415−public
415+public export
416truncate : Bits (m+n) -> Bits n
416truncate : Bits (m+n) -> Bits n
417truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
417truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
418
418
419−public
419+public export
420bitAt : Fin n -> Bits n
420bitAt : Fin n -> Bits n
421bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
421bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
422
422
423−public
423+public export
424getBit : Fin n -> Bits n -> Bool
424getBit : Fin n -> Bits n -> Bool
425getBit n x = (x `and` (bitAt n)) /= intToBits 0
425getBit n x = (x `and` (bitAt n)) /= intToBits 0
426
426
427−public
427+public export
428setBit : Fin n -> Bits n -> Bits n
428setBit : Fin n -> Bits n -> Bits n
429setBit n x = x `or` (bitAt n)
429setBit n x = x `or` (bitAt n)
430
430
431−public
431+public export
432unsetBit : Fin n -> Bits n -> Bits n
432unsetBit : Fin n -> Bits n -> Bits n
433unsetBit n x = x `and` complement (bitAt n)
433unsetBit n x = x `and` complement (bitAt n)
434
434
libs/base/Data/Complex.idr+1−1
@@ -5,7 +5,7 @@
5
5
6module Data.Complex
6module Data.Complex
7
7
8−%access public
8+%access public export
9
9
10------------------------------ Rectangular form
10------------------------------ Rectangular form
11
11
libs/base/Data/Erased.idr+1−1
@@ -1,6 +1,6 @@
1module Data.Erased
1module Data.Erased
2
2
3−%access public
3+%access public export
4%default total
4%default total
5
5
6||| The erasure monad.
6||| The erasure monad.
libs/base/Data/Fin.idr+1−1
@@ -1,7 +1,7 @@
1module Data.Fin
1module Data.Fin
2
2
3%default total
3%default total
4−%access public
4+%access public export
5
5
6||| Numbers strictly less than some bound. The name comes from "finite sets".
6||| Numbers strictly less than some bound. The name comes from "finite sets".
7|||
7|||
libs/base/Data/HVect.idr+1−1
@@ -2,7 +2,7 @@ module Data.HVect
2
2
3import public Data.Vect
3import public Data.Vect
4
4
5−%access public
5+%access public export
6%default total
6%default total
7
7
8||| Heterogeneous vectors where the type index gives, element-wise,
8||| Heterogeneous vectors where the type index gives, element-wise,
libs/base/Data/List.idr+1−1
@@ -1,6 +1,6 @@
1module Data.List
1module Data.List
2
2
3−%access public
3+%access public export
4
4
5||| A proof that some element is found in a list.
5||| A proof that some element is found in a list.
6|||
6|||
libs/base/Data/List/Quantifiers.idr+1−1
@@ -2,7 +2,7 @@ module Data.List.Quantifiers
2
2
3import Data.List
3import Data.List
4
4
5−%access public
5+%access public export
6
6
7||| A proof that some element of a list satisfies some property
7||| A proof that some element of a list satisfies some property
8|||
8|||
libs/base/Data/Mod2.idr+4−4
@@ -5,7 +5,7 @@ import Data.Bits
5%default total
5%default total
6
6
7||| Integers modulo 2^n
7||| Integers modulo 2^n
8−public
8+public export
9data Mod2 : Nat -> Type where
9data Mod2 : Nat -> Type where
10 MkMod2 : {n : Nat} -> Bits n -> Mod2 n
10 MkMod2 : {n : Nat} -> Bits n -> Mod2 n
11
11
@@ -15,16 +15,16 @@ modBin f (MkMod2 x) (MkMod2 y) = MkMod2 (f x y)
15modComp : (Bits n -> Bits n -> a) -> Mod2 n -> Mod2 n -> a
15modComp : (Bits n -> Bits n -> a) -> Mod2 n -> Mod2 n -> a
16modComp f (MkMod2 x) (MkMod2 y) = f x y
16modComp f (MkMod2 x) (MkMod2 y) = f x y
17
17
18−public partial
18+public export partial
19div : Mod2 n -> Mod2 n -> Mod2 n
19div : Mod2 n -> Mod2 n -> Mod2 n
20div = modBin udiv
20div = modBin udiv
21
21
22−public partial
22+public export partial
23rem : Mod2 n -> Mod2 n -> Mod2 n
23rem : Mod2 n -> Mod2 n -> Mod2 n
24rem = modBin urem
24rem = modBin urem
25
25
26%assert_total
26%assert_total
27−public
27+public export
28intToMod : {n : Nat} -> Integer -> Mod2 n
28intToMod : {n : Nat} -> Integer -> Mod2 n
29intToMod {n=n} x = MkMod2 (intToBits x)
29intToMod {n=n} x = MkMod2 (intToBits x)
30
30
libs/base/Data/Morphisms.idr+1−1
@@ -1,6 +1,6 @@
1module Data.Morphisms
1module Data.Morphisms
2
2
3−%access public
3+%access public export
4
4
5data Morphism : Type -> Type -> Type where
5data Morphism : Type -> Type -> Type where
6 Mor : (a -> b) -> Morphism a b
6 Mor : (a -> b) -> Morphism a b
libs/base/Data/So.idr+1−1
@@ -1,7 +1,7 @@
1module Data.So
1module Data.So
2
2
3%default total
3%default total
4−%access public
4+%access public export
5
5
6||| Ensure that some run-time Boolean test has been performed.
6||| Ensure that some run-time Boolean test has been performed.
7|||
7|||
libs/base/Data/String.idr+1−1
@@ -1,5 +1,5 @@
1module Data.String
1module Data.String
2−%access public
2+%access public export
3
3
4private
4private
5parseNumWithoutSign : List Char -> Integer -> Maybe Integer
5parseNumWithoutSign : List Char -> Integer -> Maybe Integer
libs/base/Data/Vect.idr+1−1
@@ -3,7 +3,7 @@ module Data.Vect
3import public Data.Fin
3import public Data.Fin
4import Language.Reflection
4import Language.Reflection
5
5
6−%access public
6+%access public export
7%default total
7%default total
8
8
9infixr 7 ::
9infixr 7 ::
libs/base/Data/Vect/Quantifiers.idr+1−1
@@ -2,7 +2,7 @@ module Data.Vect.Quantifiers
2
2
3import Data.Vect
3import Data.Vect
4
4
5−%access public
5+%access public export
6
6
7||| A proof that some element of a vector satisfies some property
7||| A proof that some element of a vector satisfies some property
8|||
8|||
libs/base/Debug/Error.idr+1−1
@@ -7,7 +7,7 @@ import System
7|||
7|||
8||| @ loc The source location to display for the error
8||| @ loc The source location to display for the error
9||| @ message The error to print
9||| @ message The error to print
10−partial abstract
10+partial export
11error : {default (%runElab sourceLocation) loc : SourceLocation} ->
11error : {default (%runElab sourceLocation) loc : SourceLocation} ->
12 (message : String) ->
12 (message : String) ->
13 a
13 a
libs/base/Debug/Trace.idr+1−1
@@ -3,7 +3,7 @@ module Debug.Trace
3||| Print a message for debugging purposes as a side effect
3||| Print a message for debugging purposes as a side effect
4||| @ msg what to print
4||| @ msg what to print
5||| @ result the final result
5||| @ result the final result
6−abstract
6+export
7trace : (msg : String) -> (result : a) -> a
7trace : (msg : String) -> (result : a) -> a
8trace x val = unsafePerformIO {ffi=FFI_C} (do putStrLn x; return val)
8trace x val = unsafePerformIO {ffi=FFI_C} (do putStrLn x; return val)
9
9
libs/base/Language/Reflection/Utils.idr+1−1
@@ -4,7 +4,7 @@ import Language.Reflection
4import Language.Reflection.Elab
4import Language.Reflection.Elab
5import Language.Reflection.Errors
5import Language.Reflection.Errors
6
6
7−%access public
7+%access public export
8
8
9--------------------------------------------------------
9--------------------------------------------------------
10-- Tactic construction conveniences
10-- Tactic construction conveniences
libs/base/Syntax/PreorderReasoning.idr+1−1
@@ -1,6 +1,6 @@
1module Syntax.PreorderReasoning
1module Syntax.PreorderReasoning
2
2
3−%access public
3+%access public export
4
4
5-- QED is first to get the precedence to work out. It's just Refl with an explicit argument.
5-- QED is first to get the precedence to work out. It's just Refl with an explicit argument.
6syntax [expr] "QED" = qed expr
6syntax [expr] "QED" = qed expr
libs/base/System.idr+1−1
@@ -2,7 +2,7 @@ module System
2
2
3%include C "unistd.h"
3%include C "unistd.h"
4%default partial
4%default partial
5−%access public
5+%access public export
6
6
7||| Retrieves a value from the environment if the given key is present,
7||| Retrieves a value from the environment if the given key is present,
8||| otherwise it returns Nothing.
8||| otherwise it returns Nothing.
libs/base/System/Concurrency/Raw.idr+1−1
@@ -6,7 +6,7 @@ module System.Concurrency.Raw
6
6
7import System
7import System
8
8
9−%access abstract
9+%access export
10
10
11||| Send a message of any type to the thread with the given thread id
11||| Send a message of any type to the thread with the given thread id
12||| Returns 1 if the message was sent successfully, 0 otherwise
12||| Returns 1 if the message was sent successfully, 0 otherwise
libs/base/System/Info.idr+3−3
@@ -1,16 +1,16 @@
1module System.Info
1module System.Info
2
2
3||| The Idris backend in use
3||| The Idris backend in use
4−abstract
4+export
5backend : String
5backend : String
6backend = prim__systemInfo 0
6backend = prim__systemInfo 0
7
7
8||| The operating system in use.
8||| The operating system in use.
9−abstract
9+export
10os : String
10os : String
11os = prim__systemInfo 1
11os = prim__systemInfo 1
12
12
13||| The triple this program was targeted for
13||| The triple this program was targeted for
14−abstract
14+export
15targetTriple : String
15targetTriple : String
16targetTriple = prim__systemInfo 2
16targetTriple = prim__systemInfo 2
libs/contrib/Classes/Verified.idr+1−1
@@ -4,7 +4,7 @@ import Control.Algebra
4import Control.Algebra.Lattice
4import Control.Algebra.Lattice
5import Control.Algebra.VectorSpace
5import Control.Algebra.VectorSpace
6
6
7−%access public
7+%access public export
8
8
9-- Due to these being basically unused and difficult to implement,
9-- Due to these being basically unused and difficult to implement,
10-- they're in contrib for a bit. Once a design is found that lets them
10-- they're in contrib for a bit. Once a design is found that lets them
libs/contrib/Control/Algebra.idr+1−1
@@ -3,7 +3,7 @@ module Control.Algebra
3infixl 6 <->
3infixl 6 <->
4infixl 7 <.>
4infixl 7 <.>
5
5
6−%access public
6+%access public export
7
7
8||| Sets equipped with a single binary operation that is associative, along with
8||| Sets equipped with a single binary operation that is associative, along with
9||| a neutral element for that binary operation and inverses for all elements.
9||| a neutral element for that binary operation and inverses for all elements.
libs/contrib/Control/Algebra/Lattice.idr+1−1
@@ -3,7 +3,7 @@ module Control.Algebra.Lattice
3import Control.Algebra
3import Control.Algebra
4import Data.Heap
4import Data.Heap
5
5
6−%access public
6+%access public export
7
7
8||| Sets equipped with a binary operation that is commutative, associative and
8||| Sets equipped with a binary operation that is commutative, associative and
9||| idempotent. Must satisfy the following laws:
9||| idempotent. Must satisfy the following laws:
libs/contrib/Control/Algebra/NumericInstances.idr+1−1
@@ -7,7 +7,7 @@ import Control.Algebra.VectorSpace
7import Data.Complex
7import Data.Complex
8import Data.ZZ
8import Data.ZZ
9
9
10−%access public
10+%access public export
11
11
12Semigroup Integer where
12Semigroup Integer where
13 (<+>) = (+)
13 (<+>) = (+)
libs/contrib/Control/Algebra/VectorSpace.idr+1−1
@@ -2,7 +2,7 @@ module Control.Algebra.VectorSpace
2
2
3import Control.Algebra
3import Control.Algebra
4
4
5−%access public
5+%access public export
6
6
7infixl 5 <#>
7infixl 5 <#>
8infixr 2 <||>
8infixr 2 <||>
libs/contrib/Control/Isomorphism/Primitives.idr+1−1
@@ -4,7 +4,7 @@ import Control.Isomorphism
4import Data.ZZ
4import Data.ZZ
5
5
6%default total
6%default total
7−%access public
7+%access public export
8
8
9-- This module contains isomorphisms between convenient inductive types and
9-- This module contains isomorphisms between convenient inductive types and
10-- Idris primitives. Because primitives lack a convenient structure, these
10-- Idris primitives. Because primitives lack a convenient structure, these
libs/contrib/Control/Partial.idr+1−1
@@ -7,7 +7,7 @@ module Control.Partial
7||| @ p the predicate to wait for
7||| @ p the predicate to wait for
8||| @ f the function to repeatedly apply
8||| @ f the function to repeatedly apply
9||| @ v the starting value
9||| @ v the starting value
10−partial abstract
10+partial export
11until : (p : a -> Bool) -> (f : a -> a) -> (v : a) -> a
11until : (p : a -> Bool) -> (f : a -> a) -> (v : a) -> a
12until p f v with (p v)
12until p f v with (p v)
13 | False = until p f (f v)
13 | False = until p f (f v)
libs/contrib/Control/WellFounded.idr+1−1
@@ -6,7 +6,7 @@
6module Control.WellFounded
6module Control.WellFounded
7
7
8%default total
8%default total
9−%access public
9+%access public export
10
10
11||| Accessibility: some element `x` is accessible if all `y` such that
11||| Accessibility: some element `x` is accessible if all `y` such that
12||| `rel y x` are themselves accessible.
12||| `rel y x` are themselves accessible.
libs/contrib/Data/BoundedList.idr+1−1
@@ -2,7 +2,7 @@ module Data.BoundedList
2
2
3import Data.Fin
3import Data.Fin
4
4
5−%access public
5+%access public export
6%default total
6%default total
7
7
8||| A list with an upper bound on its length.
8||| A list with an upper bound on its length.
libs/contrib/Data/CoList.idr+1−1
@@ -1,6 +1,6 @@
1module Data.CoList
1module Data.CoList
2
2
3−%access public
3+%access public export
4%default total
4%default total
5
5
6||| Idris will know that it always can produce a new element in finite time
6||| Idris will know that it always can produce a new element in finite time
libs/contrib/Data/Fun.idr+1−1
@@ -3,7 +3,7 @@ module Data.Fun
3import public Data.Vect
3import public Data.Vect
4
4
5%default total
5%default total
6−%access public
6+%access public export
7
7
8||| Build an n-ary function type from a Vect of Types and a result type
8||| Build an n-ary function type from a Vect of Types and a result type
9Fun : Vect n Type -> Type -> Type
9Fun : Vect n Type -> Type -> Type
libs/contrib/Data/Hash.idr+1−1
@@ -2,7 +2,7 @@ module Data.Hash
2
2
3import Data.Vect
3import Data.Vect
4
4
5−%access public
5+%access public export
6%default total
6%default total
7
7
8{- A general purpose Hashing library (not cryptographic)
8{- A general purpose Hashing library (not cryptographic)
libs/contrib/Data/Heap.idr+2−2
@@ -7,9 +7,9 @@ module Data.Heap
7
7
8
8
9%default total
9%default total
10−%access public
10+%access public export
11
11
12−abstract data MaxiphobicHeap : Type -> Type where
12+export data MaxiphobicHeap : Type -> Type where
13 Empty : MaxiphobicHeap a
13 Empty : MaxiphobicHeap a
14 Node : Nat -> MaxiphobicHeap a -> a -> MaxiphobicHeap a -> MaxiphobicHeap a
14 Node : Nat -> MaxiphobicHeap a -> a -> MaxiphobicHeap a -> MaxiphobicHeap a
15
15
libs/contrib/Data/Matrix.idr+1−1
@@ -5,7 +5,7 @@ module Data.Matrix
5import public Data.Vect
5import public Data.Vect
6
6
7%default total
7%default total
8−%access public
8+%access public export
9
9
10||| Matrix with n rows and m columns
10||| Matrix with n rows and m columns
11Matrix : Nat -> Nat -> Type -> Type
11Matrix : Nat -> Nat -> Type -> Type
libs/contrib/Data/Matrix/Algebraic.idr+1−1
@@ -9,7 +9,7 @@ import public Control.Algebra.NumericInstances
9
9
10import public Data.Matrix
10import public Data.Matrix
11
11
12−%access public
12+%access public export
13%default total
13%default total
14
14
15infixr 2 <:> -- vector inner product
15infixr 2 <:> -- vector inner product
libs/contrib/Data/Matrix/Numeric.idr+1−1
@@ -5,7 +5,7 @@ module Data.Matrix.Numeric
5import public Data.Matrix
5import public Data.Matrix
6
6
7%default total
7%default total
8−%access public
8+%access public export
9
9
10infixr 2 <:> -- vector inner product
10infixr 2 <:> -- vector inner product
11infixr 2 >< -- vector outer product
11infixr 2 >< -- vector outer product
libs/contrib/Data/Nat/DivMod.idr+1−1
@@ -2,7 +2,7 @@
2module Data.Nat.DivMod
2module Data.Nat.DivMod
3
3
4%default total
4%default total
5−%access public
5+%access public export
6
6
7||| The result of euclidean division of natural numbers
7||| The result of euclidean division of natural numbers
8|||
8|||
libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr+1−1
@@ -8,7 +8,7 @@ import Data.So
8import Control.WellFounded
8import Control.WellFounded
9
9
10%default total
10%default total
11−%access public
11+%access public export
12
12
13||| A strict less-than relation on `Nat`.
13||| A strict less-than relation on `Nat`.
14|||
14|||
libs/contrib/Data/Rel.idr+1−1
@@ -2,7 +2,7 @@ module Data.Rel
2
2
3import Data.Fun
3import Data.Fun
4
4
5−%access public
5+%access public export
6
6
7||| Build an n-ary relation type from a Vect of Types
7||| Build an n-ary relation type from a Vect of Types
8Rel : Vect n Type -> Type
8Rel : Vect n Type -> Type
libs/contrib/Data/Sign.idr+1−1
@@ -1,6 +1,6 @@
1module Data.Sign
1module Data.Sign
2
2
3−%access public
3+%access public export
4
4
5||| A representation of signs for signed datatypes such as `ZZ`
5||| A representation of signs for signed datatypes such as `ZZ`
6data Sign = Plus | Zero | Minus
6data Sign = Plus | Zero | Minus
libs/contrib/Data/SortedMap.idr+8−8
@@ -192,21 +192,21 @@ treeToList = treeToList' (:: [])
192 treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
192 treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
193 treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
193 treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
194
194
195−abstract
195+export
196data SortedMap : Type -> Type -> Type where
196data SortedMap : Type -> Type -> Type where
197 Empty : Ord k => SortedMap k v
197 Empty : Ord k => SortedMap k v
198 M : (o : Ord k) => (n:Nat) -> Tree n k v o -> SortedMap k v
198 M : (o : Ord k) => (n:Nat) -> Tree n k v o -> SortedMap k v
199
199
200−public
200+export
201empty : Ord k => SortedMap k v
201empty : Ord k => SortedMap k v
202empty = Empty
202empty = Empty
203
203
204−public
204+export
205lookup : k -> SortedMap k v -> Maybe v
205lookup : k -> SortedMap k v -> Maybe v
206lookup _ Empty = Nothing
206lookup _ Empty = Nothing
207lookup k (M _ t) = treeLookup k t
207lookup k (M _ t) = treeLookup k t
208
208
209−public
209+export
210insert : k -> v -> SortedMap k v -> SortedMap k v
210insert : k -> v -> SortedMap k v -> SortedMap k v
211insert k v Empty = M Z (Leaf k v)
211insert k v Empty = M Z (Leaf k v)
212insert k v (M _ t) =
212insert k v (M _ t) =
@@ -214,7 +214,7 @@ insert k v (M _ t) =
214 Left t' => (M _ t')
214 Left t' => (M _ t')
215 Right t' => (M _ t')
215 Right t' => (M _ t')
216
216
217−public
217+export
218delete : k -> SortedMap k v -> SortedMap k v
218delete : k -> SortedMap k v -> SortedMap k v
219delete _ Empty = Empty
219delete _ Empty = Empty
220delete k (M Z t) =
220delete k (M Z t) =
@@ -226,16 +226,16 @@ delete k (M (S _) t) =
226 Left t' => (M _ t')
226 Left t' => (M _ t')
227 Right t' => (M _ t')
227 Right t' => (M _ t')
228
228
229−public
229+export
230fromList : Ord k => List (k, v) -> SortedMap k v
230fromList : Ord k => List (k, v) -> SortedMap k v
231fromList l = foldl (flip (uncurry insert)) empty l
231fromList l = foldl (flip (uncurry insert)) empty l
232
232
233−public
233+export
234toList : SortedMap k v -> List (k, v)
234toList : SortedMap k v -> List (k, v)
235toList Empty = []
235toList Empty = []
236toList (M _ t) = treeToList t
236toList (M _ t) = treeToList t
237
237
238−public
238+export
239treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
239treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
240treeMap f (Leaf k v) = Leaf k (f v)
240treeMap f (Leaf k v) = Leaf k (f v)
241treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
241treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
libs/contrib/Data/SortedSet.idr+7−7
@@ -4,30 +4,30 @@ import Data.SortedMap
4
4
5-- TODO: add intersection, union, difference
5-- TODO: add intersection, union, difference
6
6
7−abstract
7+export
8data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
8data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
9
9
10−public
10+export
11empty : Ord k => SortedSet k
11empty : Ord k => SortedSet k
12empty = SetWrapper Data.SortedMap.empty
12empty = SetWrapper Data.SortedMap.empty
13
13
14−public
14+export
15insert : k -> SortedSet k -> SortedSet k
15insert : k -> SortedSet k -> SortedSet k
16insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)
16insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)
17
17
18−public
18+export
19delete : k -> SortedSet k -> SortedSet k
19delete : k -> SortedSet k -> SortedSet k
20delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)
20delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)
21
21
22−public
22+export
23contains : k -> SortedSet k -> Bool
23contains : k -> SortedSet k -> Bool
24contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)
24contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)
25
25
26−public
26+export
27fromList : Ord k => List k -> SortedSet k
27fromList : Ord k => List k -> SortedSet k
28fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))
28fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))
29
29
30−public
30+export
31toList : SortedSet k -> List k
31toList : SortedSet k -> List k
32toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
32toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
33
33
libs/contrib/Data/ZZ.idr+1−1
@@ -4,7 +4,7 @@ import Decidable.Equality
4import Data.Sign
4import Data.Sign
5
5
6%default total
6%default total
7−%access public
7+%access public export
8
8
9
9
10||| An integer is either a positive `Nat` or the negated successor of a `Nat`.
10||| An integer is either a positive `Nat` or the negated successor of a `Nat`.
libs/contrib/Decidable/Decidable.idr+1−1
@@ -3,7 +3,7 @@ module Decidable.Decidable
3import Data.Rel
3import Data.Rel
4import Data.Fun
4import Data.Fun
5
5
6−%access public
6+%access public export
7
7
8--------------------------------------------------------------------------------
8--------------------------------------------------------------------------------
9-- Interface for decidable n-ary Relations
9-- Interface for decidable n-ary Relations
libs/contrib/Decidable/Order.idr+1−1
@@ -6,7 +6,7 @@ import Data.Fin
6import Data.Fun
6import Data.Fun
7import Data.Rel
7import Data.Rel
8
8
9−%access public
9+%access public export
10
10
11--------------------------------------------------------------------------------
11--------------------------------------------------------------------------------
12-- Utility Lemmas
12-- Utility Lemmas
libs/contrib/Network/Cgi.idr+11−11
@@ -4,7 +4,7 @@ import System
4
4
5%default total
5%default total
6
6
7−public
7+public export
8Vars : Type
8Vars : Type
9Vars = List (String, String)
9Vars = List (String, String)
10
10
@@ -23,7 +23,7 @@ add_Headers str st = record { Headers = Headers st ++ str } st
23add_Output : String -> CGIInfo -> CGIInfo
23add_Output : String -> CGIInfo -> CGIInfo
24add_Output str st = record { Output = Output st ++ str } st
24add_Output str st = record { Output = Output st ++ str } st
25
25
26−abstract
26+export
27data CGI : Type -> Type where
27data CGI : Type -> Type where
28 MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a
28 MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a
29
29
@@ -51,32 +51,32 @@ setInfo i = MkCGI (\s => return ((), i))
51getInfo : CGI CGIInfo
51getInfo : CGI CGIInfo
52getInfo = MkCGI (\s => return (s, s))
52getInfo = MkCGI (\s => return (s, s))
53
53
54−abstract
54+export
55lift : IO a -> CGI a
55lift : IO a -> CGI a
56lift op = MkCGI (\st => do { x <- op
56lift op = MkCGI (\st => do { x <- op
57 return (x, st) } )
57 return (x, st) } )
58
58
59−abstract
59+export
60output : String -> CGI ()
60output : String -> CGI ()
61output s = do i <- getInfo
61output s = do i <- getInfo
62 setInfo (add_Output s i)
62 setInfo (add_Output s i)
63
63
64−abstract
64+export
65queryVars : CGI Vars
65queryVars : CGI Vars
66queryVars = do i <- getInfo
66queryVars = do i <- getInfo
67 return (GET i)
67 return (GET i)
68
68
69−abstract
69+export
70postVars : CGI Vars
70postVars : CGI Vars
71postVars = do i <- getInfo
71postVars = do i <- getInfo
72 return (POST i)
72 return (POST i)
73
73
74−abstract
74+export
75cookieVars : CGI Vars
75cookieVars : CGI Vars
76cookieVars = do i <- getInfo
76cookieVars = do i <- getInfo
77 return (Cookies i)
77 return (Cookies i)
78
78
79−abstract
79+export
80queryVar : String -> CGI (Maybe String)
80queryVar : String -> CGI (Maybe String)
81queryVar x = do vs <- queryVars
81queryVar x = do vs <- queryVars
82 return (lookup x vs)
82 return (lookup x vs)
@@ -89,12 +89,12 @@ getHeaders : CGI String
89getHeaders = do i <- getInfo
89getHeaders = do i <- getInfo
90 return (Headers i)
90 return (Headers i)
91
91
92−abstract
92+export
93flushHeaders : CGI ()
93flushHeaders : CGI ()
94flushHeaders = do o <- getHeaders
94flushHeaders = do o <- getHeaders
95 lift (putStrLn o)
95 lift (putStrLn o)
96
96
97−abstract
97+export
98flush : CGI ()
98flush : CGI ()
99flush = do o <- getOutput
99flush = do o <- getOutput
100 lift (putStr o)
100 lift (putStr o)
@@ -119,7 +119,7 @@ getCgiEnv key = do
119 val <- getEnv key
119 val <- getEnv key
120 return $ maybe "" id val
120 return $ maybe "" id val
121
121
122−abstract
122+export
123runCGI : CGI a -> IO a
123runCGI : CGI a -> IO a
124runCGI prog = do
124runCGI prog = do
125 clen_in <- getCgiEnv "CONTENT_LENGTH"
125 clen_in <- getCgiEnv "CONTENT_LENGTH"
libs/contrib/Network/Socket.idr+3−5
@@ -8,8 +8,6 @@ module IdrisNet.Socket
8%include C "sys/socket.h"
8%include C "sys/socket.h"
9%include C "netdb.h"
9%include C "netdb.h"
10
10
11−%access public
12−
13ByteLength : Type
11ByteLength : Type
14ByteLength = Int
12ByteLength = Int
15
13
@@ -120,18 +118,18 @@ record UDPAddrInfo where
120 remote_port : Port
118 remote_port : Port
121
119
122||| Frees a given pointer
120||| Frees a given pointer
123−public
121+export
124sock_free : BufPtr -> IO ()
122sock_free : BufPtr -> IO ()
125sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
123sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
126
124
127−public
125+export
128sockaddr_free : SockaddrPtr -> IO ()
126sockaddr_free : SockaddrPtr -> IO ()
129sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
127sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
130
128
131||| Allocates an amount of memory given by the ByteLength parameter.
129||| Allocates an amount of memory given by the ByteLength parameter.
132|||
130|||
133||| Used to allocate a mutable pointer to be given to the Recv functions.
131||| Used to allocate a mutable pointer to be given to the Recv functions.
134−public
132+export
135sock_alloc : ByteLength -> IO BufPtr
133sock_alloc : ByteLength -> IO BufPtr
136sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
134sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
137
135
libs/contrib/System/Concurrency/Process.idr+2−2
@@ -4,9 +4,9 @@ module System.Concurrency.Process
4
4
5import System.Concurrency.Raw
5import System.Concurrency.Raw
6
6
7−%access public
7+%access public export
8
8
9−abstract
9+export
10data ProcID msg = MkPID Ptr
10data ProcID msg = MkPID Ptr
11
11
12||| Type safe message passing programs. Parameterised over the type of
12||| Type safe message passing programs. Parameterised over the type of
libs/effects/Effect/Default.idr+1−1
@@ -2,7 +2,7 @@ module Effect.Default
2
2
3import Data.Vect
3import Data.Vect
4
4
5−%access public
5+%access public export
6
6
7interface Default a where
7interface Default a where
8 default : a
8 default : a
libs/effects/Effect/Exception.idr+1−1
@@ -4,7 +4,7 @@ import Effects
4import System
4import System
5import Control.IOExcept
5import Control.IOExcept
6
6
7−%access public
7+%access public export
8
8
9data Exception : Type -> Effect where
9data Exception : Type -> Effect where
10 Raise : a -> sig (Exception a) b
10 Raise : a -> sig (Exception a) b
libs/effects/Effect/File.idr+1−1
@@ -4,7 +4,7 @@ module Effect.File
4import Effects
4import Effects
5import Control.IOExcept
5import Control.IOExcept
6
6
7−%access public
7+%access public export
8
8
9||| A Dependent type to describe File Handles. File handles are
9||| A Dependent type to describe File Handles. File handles are
10||| parameterised with the current state of the file: Closed; Open for
10||| parameterised with the current state of the file: Closed; Open for
libs/effects/Effect/Logging/Category.idr+1−1
@@ -14,7 +14,7 @@ module Effect.Logging.Category
14import Effects
14import Effects
15import public Effect.Logging.Level
15import public Effect.Logging.Level
16
16
17−%access public
17+%access public export
18
18
19-- -------------------------------------------------------- [ Logging Resource ]
19-- -------------------------------------------------------- [ Logging Resource ]
20
20
libs/effects/Effect/Logging/Default.idr+1−1
@@ -15,7 +15,7 @@ module Effect.Logging.Default
15import Effects
15import Effects
16import public Effect.Logging.Level
16import public Effect.Logging.Level
17
17
18−%access public
18+%access public export
19
19
20-- ------------------------------------------------------------ [ The Resource ]
20-- ------------------------------------------------------------ [ The Resource ]
21
21
libs/effects/Effect/Logging/Level.idr+1−1
@@ -14,7 +14,7 @@
14||| loggers.
14||| loggers.
15module Effect.Logging.Level
15module Effect.Logging.Level
16
16
17−%access public
17+%access public export
18%default total
18%default total
19
19
20-- ---------------------------------------------------- [ Log Level Definition ]
20-- ---------------------------------------------------- [ Log Level Definition ]
libs/effects/Effect/Memory.idr+3−3
@@ -5,13 +5,13 @@ import Control.IOExcept
5import Data.Vect
5import Data.Vect
6import public Data.So
6import public Data.So
7
7
8−%access public
8+%access public export
9
9
10−abstract
10+export
11data MemoryChunk : Nat -> Nat -> Type where
11data MemoryChunk : Nat -> Nat -> Type where
12 CH : Ptr -> MemoryChunk size initialized
12 CH : Ptr -> MemoryChunk size initialized
13
13
14−abstract
14+export
15data RawMemory : Effect where
15data RawMemory : Effect where
16 Allocate : (n : Nat) ->
16 Allocate : (n : Nat) ->
17 RawMemory () () (\v => MemoryChunk n 0)
17 RawMemory () () (\v => MemoryChunk n 0)
libs/effects/Effect/Monad.idr+1−1
@@ -2,7 +2,7 @@ module Effect.Monad
2
2
3import Effects
3import Effects
4
4
5−%access public
5+%access public export
6
6
7data MonadEffT : List EFFECT -> (Type -> Type) -> Type -> Type where
7data MonadEffT : List EFFECT -> (Type -> Type) -> Type -> Type where
8 MkMonadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a
8 MkMonadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a
libs/effects/Effect/Perf.idr+1−1
@@ -12,7 +12,7 @@ import System
12import Effects
12import Effects
13import Effect.Default
13import Effect.Default
14
14
15−%access public
15+%access public export
16
16
17-- ---------------------------------------------------- [ Timer Data Structure ]
17-- ---------------------------------------------------- [ Timer Data Structure ]
18
18
libs/effects/Effect/Random.idr+1−1
@@ -3,7 +3,7 @@ module Effect.Random
3import Effects
3import Effects
4import Data.Vect
4import Data.Vect
5
5
6−%access public
6+%access public export
7
7
8data Random : Effect where
8data Random : Effect where
9 GetRandom : sig Random Integer Integer
9 GetRandom : sig Random Integer Integer
libs/effects/Effect/Select.idr+1−1
@@ -2,7 +2,7 @@ module Effect.Select
2
2
3import Effects
3import Effects
4
4
5−%access public
5+%access public export
6
6
7data Selection : Effect where
7data Selection : Effect where
8 Select : List a -> sig Selection a ()
8 Select : List a -> sig Selection a ()
libs/effects/Effect/State.idr+1−1
@@ -2,7 +2,7 @@ module Effect.State
2
2
3import Effects
3import Effects
4
4
5−%access public
5+%access public export
6
6
7data State : Effect where
7data State : Effect where
8 Get : sig State a a
8 Get : sig State a a
libs/effects/Effect/StdIO.idr+1−1
@@ -3,7 +3,7 @@ module Effect.StdIO
3import Effects
3import Effects
4import Control.IOExcept
4import Control.IOExcept
5
5
6−%access public
6+%access public export
7
7
8-------------------------------------------------------------
8-------------------------------------------------------------
9-- IO effects internals
9-- IO effects internals
libs/effects/Effect/System.idr+1−1
@@ -7,7 +7,7 @@ import Effects
7import System
7import System
8import Control.IOExcept
8import Control.IOExcept
9
9
10−%access public
10+%access public export
11
11
12data System : Effect where
12data System : Effect where
13 Args : sig System (List String)
13 Args : sig System (List String)
libs/effects/Effect/Trans.idr+1−1
@@ -2,7 +2,7 @@ module Effect.Trans
2
2
3import Effects
3import Effects
4
4
5−%access public
5+%access public export
6
6
7data Trans : (Type -> Type) -> Effect where
7data Trans : (Type -> Type) -> Effect where
8 Lift : m a -> sig (Trans m) a
8 Lift : m a -> sig (Trans m) a
libs/effects/Effects.idr+1−1
@@ -7,7 +7,7 @@ import Data.Vect
7--- Effectful computations are described as algebraic data types that
7--- Effectful computations are described as algebraic data types that
8--- explain how an effect is interpreted in some underlying context.
8--- explain how an effect is interpreted in some underlying context.
9
9
10−%access public
10+%access public export
11-- ----------------------------------------------------------------- [ Effects ]
11-- ----------------------------------------------------------------- [ Effects ]
12||| The Effect type describes effectful computations.
12||| The Effect type describes effectful computations.
13|||
13|||
libs/prelude/Builtins.idr+5−5
@@ -1,6 +1,6 @@
1%unqualified
1%unqualified
2
2
3−%access public
3+%access public export
4%default total
4%default total
5
5
6||| The canonical single-element type, also known as the trivially
6||| The canonical single-element type, also known as the trivially
@@ -155,13 +155,13 @@ assert_total x = x
155
155
156||| Subvert the type checker. This function is abstract, so it will not reduce in
156||| Subvert the type checker. This function is abstract, so it will not reduce in
157||| the type checker. Use it with care - it can result in segfaults or worse!
157||| the type checker. Use it with care - it can result in segfaults or worse!
158−abstract %assert_total -- need to pretend
158+export %assert_total -- need to pretend
159believe_me : a -> b
159believe_me : a -> b
160believe_me x = prim__believe_me _ _ x
160believe_me x = prim__believe_me _ _ x
161
161
162||| Subvert the type checker. This function *will* reduce in the type checker.
162||| Subvert the type checker. This function *will* reduce in the type checker.
163||| Use it with extreme care - it can result in segfaults or worse!
163||| Use it with extreme care - it can result in segfaults or worse!
164−public %assert_total
164+public export %assert_total
165really_believe_me : a -> b
165really_believe_me : a -> b
166really_believe_me x = prim__believe_me _ _ x
166really_believe_me x = prim__believe_me _ _ x
167
167
@@ -174,8 +174,8 @@ Float = Double
174-- Pointers as external primitive; there's no literals for these, so no
174-- Pointers as external primitive; there's no literals for these, so no
175-- need for them to be part of the compiler.
175-- need for them to be part of the compiler.
176
176
177−abstract data Ptr : Type
177+export data Ptr : Type
178−abstract data ManagedPtr : Type
178+export data ManagedPtr : Type
179
179
180%extern prim__readFile : prim__WorldType -> Ptr -> String
180%extern prim__readFile : prim__WorldType -> Ptr -> String
181%extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int
181%extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int
libs/prelude/Decidable/Equality.idr+1−1
@@ -9,7 +9,7 @@ import Prelude.List
9import Prelude.Nat
9import Prelude.Nat
10import Prelude.Maybe
10import Prelude.Maybe
11
11
12−%access public
12+%access public export
13
13
14--------------------------------------------------------------------------------
14--------------------------------------------------------------------------------
15-- Utility lemmas
15-- Utility lemmas
libs/prelude/IO.idr+9−9
@@ -3,21 +3,21 @@
3import Builtins
3import Builtins
4import Prelude.List
4import Prelude.List
5
5
6−%access public
6+%access public export
7
7
8||| Idris's primitive IO, for building abstractions on top of
8||| Idris's primitive IO, for building abstractions on top of
9−abstract
9+export
10data PrimIO : Type -> Type where
10data PrimIO : Type -> Type where
11 Prim__IO : a -> PrimIO a
11 Prim__IO : a -> PrimIO a
12
12
13||| A token representing the world, for use in `IO`
13||| A token representing the world, for use in `IO`
14−abstract data World = TheWorld prim__WorldType
14+export data World = TheWorld prim__WorldType
15
15
16private
16private
17world : World -> prim__WorldType
17world : World -> prim__WorldType
18world (TheWorld w) = w
18world (TheWorld w) = w
19
19
20−abstract WorldRes : Type -> Type
20+export WorldRes : Type -> Type
21WorldRes x = x
21WorldRes x = x
22
22
23||| An FFI specifier, which describes how a particular compiler
23||| An FFI specifier, which describes how a particular compiler
@@ -35,7 +35,7 @@ record FFI where
35
35
36||| The IO type, parameterised over the FFI that is available within
36||| The IO type, parameterised over the FFI that is available within
37||| it.
37||| it.
38−abstract
38+export
39data IO' : (lang : FFI) -> Type -> Type where
39data IO' : (lang : FFI) -> Type -> Type where
40 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
40 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
41
41
@@ -91,25 +91,25 @@ foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) ->
91 {auto fty : FTy f [] ty} -> ty
91 {auto fty : FTy f [] ty} -> ty
92foreign ffi fname ty {fty} = foreign_prim ffi fname fty []
92foreign ffi fname ty {fty} = foreign_prim ffi fname fty []
93
93
94−abstract
94+export
95prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
95prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
96prim_io_bind (Prim__IO v) k = k v
96prim_io_bind (Prim__IO v) k = k v
97
97
98unsafePerformPrimIO : PrimIO a -> a
98unsafePerformPrimIO : PrimIO a -> a
99-- compiled as primitive
99-- compiled as primitive
100
100
101−abstract
101+export
102prim_io_return : a -> PrimIO a
102prim_io_return : a -> PrimIO a
103prim_io_return x = Prim__IO x
103prim_io_return x = Prim__IO x
104
104
105−abstract
105+export
106io_bind : IO' l a -> (a -> IO' l b) -> IO' l b
106io_bind : IO' l a -> (a -> IO' l b) -> IO' l b
107io_bind (MkIO fn) k
107io_bind (MkIO fn) k
108 = MkIO (\w => prim_io_bind (fn w)
108 = MkIO (\w => prim_io_bind (fn w)
109 (\ b => case k b of
109 (\ b => case k b of
110 MkIO fkb => fkb w))
110 MkIO fkb => fkb w))
111
111
112−abstract
112+export
113io_return : a -> IO' l a
113io_return : a -> IO' l a
114io_return x = MkIO (\w => prim_io_return x)
114io_return x = MkIO (\w => prim_io_return x)
115
115
libs/prelude/Language/Reflection.idr+2−2
@@ -9,7 +9,7 @@ import Prelude.List
9import Prelude.Nat
9import Prelude.Nat
10import Prelude.Traversable
10import Prelude.Traversable
11
11
12−%access public
12+%access public export
13
13
14||| A source location in an Idris file
14||| A source location in an Idris file
15record SourceLocation where
15record SourceLocation where
@@ -80,7 +80,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
80 | WorldType | TheWorld
80 | WorldType | TheWorld
81%name Const c, c'
81%name Const c, c'
82
82
83−abstract interface ReflConst (a : Type) where
83+export interface ReflConst (a : Type) where
84 toConst : a -> Const
84 toConst : a -> Const
85
85
86implementation ReflConst Int where
86implementation ReflConst Int where
libs/prelude/Language/Reflection/Elab.idr+3−3
@@ -16,7 +16,7 @@ import Prelude.Monad
16import Prelude.Nat
16import Prelude.Nat
17import Language.Reflection
17import Language.Reflection
18
18
19−%access public
19+%access public export
20
20
21data Fixity = Infixl Nat | Infixr Nat | Infix Nat | Prefix Nat
21data Fixity = Infixl Nat | Infixr Nat | Infix Nat | Prefix Nat
22
22
@@ -102,7 +102,7 @@ record Datatype where
102 constructors : List (TTName, List CtorArg, Raw)
102 constructors : List (TTName, List CtorArg, Raw)
103
103
104||| A reflected elaboration script.
104||| A reflected elaboration script.
105−abstract
105+export
106data Elab : Type -> Type where
106data Elab : Type -> Type where
107 -- obligatory control stuff
107 -- obligatory control stuff
108 Prim__PureElab : a -> Elab a
108 Prim__PureElab : a -> Elab a
@@ -166,7 +166,7 @@ data Elab : Type -> Type where
166-------------
166-------------
167-- Public API
167-- Public API
168-------------
168-------------
169−%access public
169+%access public export
170namespace Tactics
170namespace Tactics
171 implementation Functor Elab where
171 implementation Functor Elab where
172 map f t = Prim__BindElab t (\x => Prim__PureElab (f x))
172 map f t = Prim__BindElab t (\x => Prim__PureElab (f x))
libs/prelude/Language/Reflection/Errors.idr+1−1
@@ -8,7 +8,7 @@ import Prelude.Bool
8import Prelude.List
8import Prelude.List
9import Prelude.Maybe
9import Prelude.Maybe
10
10
11−%access public
11+%access public export
12
12
13data Err = Msg String
13data Err = Msg String
14 | InternalMsg String
14 | InternalMsg String
libs/prelude/Prelude.idr+1−1
@@ -33,7 +33,7 @@ import public Language.Reflection
33import public Language.Reflection.Elab
33import public Language.Reflection.Elab
34import public Language.Reflection.Errors
34import public Language.Reflection.Errors
35
35
36−%access public
36+%access public export
37%default total
37%default total
38
38
39-- Things that can't be elsewhere for import cycle reasons
39-- Things that can't be elsewhere for import cycle reasons
libs/prelude/Prelude/Algebra.idr+1−1
@@ -4,7 +4,7 @@ import Builtins
4
4
5infixl 6 <+>
5infixl 6 <+>
6
6
7−%access public
7+%access public export
8
8
9--------------------------------------------------------------------------------
9--------------------------------------------------------------------------------
10-- A modest interface hierarchy
10-- A modest interface hierarchy
libs/prelude/Prelude/Applicative.idr+1−1
@@ -8,7 +8,7 @@ import Prelude.Interfaces
8import Prelude.Foldable
8import Prelude.Foldable
9import Prelude.Functor
9import Prelude.Functor
10
10
11−%access public
11+%access public export
12
12
13---- Applicative functors/Idioms
13---- Applicative functors/Idioms
14
14
libs/prelude/Prelude/Basics.idr+1−1
@@ -2,7 +2,7 @@ module Prelude.Basics
2
2
3import Builtins
3import Builtins
4
4
5−%access public
5+%access public export
6
6
7Not : Type -> Type
7Not : Type -> Type
8Not a = a -> Void
8Not a = a -> Void
libs/prelude/Prelude/Bits.idr+1−1
@@ -12,7 +12,7 @@ import Prelude.Nat
12import Prelude.List
12import Prelude.List
13import Prelude.Strings
13import Prelude.Strings
14
14
15−%access public
15+%access public export
16%default total
16%default total
17
17
18b8ToString : Bits8 -> String
18b8ToString : Bits8 -> String
libs/prelude/Prelude/Bool.idr+1−1
@@ -4,7 +4,7 @@ import Builtins
4
4
5import Prelude.Uninhabited
5import Prelude.Uninhabited
6
6
7−%access public
7+%access public export
8
8
9||| Boolean Data Type
9||| Boolean Data Type
10%case data Bool = False | True
10%case data Bool = False | True
libs/prelude/Prelude/Cast.idr+1−1
@@ -3,7 +3,7 @@ module Prelude.Cast
3import Prelude.Bool
3import Prelude.Bool
4import public Builtins
4import public Builtins
5
5
6−%access public
6+%access public export
7
7
8||| Interface for transforming an instance of a data type to another type.
8||| Interface for transforming an instance of a data type to another type.
9interface Cast from to where
9interface Cast from to where
libs/prelude/Prelude/Chars.idr+1−1
@@ -7,7 +7,7 @@ import Prelude.List
7import Prelude.Cast
7import Prelude.Cast
8import Builtins
8import Builtins
9
9
10−%access public
10+%access public export
11
11
12||| Convert the number to its ASCII equivalent.
12||| Convert the number to its ASCII equivalent.
13chr : Int -> Char
13chr : Int -> Char
libs/prelude/Prelude/Doubles.idr+1−1
@@ -3,7 +3,7 @@ module Prelude.Doubles
3import Builtins
3import Builtins
4import Prelude.Interfaces
4import Prelude.Interfaces
5
5
6−%access public
6+%access public export
7%default total
7%default total
8
8
9%include C "math.h"
9%include C "math.h"
libs/prelude/Prelude/Either.idr+1−1
@@ -8,7 +8,7 @@ import Prelude.Interfaces
8import Prelude.Maybe
8import Prelude.Maybe
9import Prelude.List
9import Prelude.List
10
10
11−%access public
11+%access public export
12
12
13||| A sum type
13||| A sum type
14%elim data Either : (a, b : Type) -> Type where
14%elim data Either : (a, b : Type) -> Type where
libs/prelude/Prelude/File.idr+2−2
@@ -14,10 +14,10 @@ import Prelude.Either
14import Prelude.Show
14import Prelude.Show
15import IO
15import IO
16
16
17−%access public
17+%access public export
18
18
19||| A file handle
19||| A file handle
20−abstract
20+export
21data File : Type where
21data File : Type where
22 FHandle : (p : Ptr) -> File
22 FHandle : (p : Ptr) -> File
23
23
libs/prelude/Prelude/Foldable.idr+1−1
@@ -6,7 +6,7 @@ import Prelude.Basics
6import Prelude.Interfaces
6import Prelude.Interfaces
7import Prelude.Algebra
7import Prelude.Algebra
8
8
9−%access public
9+%access public export
10%default total
10%default total
11
11
12interface Foldable (t : Type -> Type) where
12interface Foldable (t : Type -> Type) where
libs/prelude/Prelude/Functor.idr+1−1
@@ -2,7 +2,7 @@ module Prelude.Functor
2
2
3import Prelude.Basics
3import Prelude.Basics
4
4
5−%access public
5+%access public export
6
6
7||| Functors allow a uniform action over a parameterised type.
7||| Functors allow a uniform action over a parameterised type.
8||| @ f a parameterised type
8||| @ f a parameterised type
libs/prelude/Prelude/Interactive.idr+1−1
@@ -21,7 +21,7 @@ import Prelude.Either
21import Prelude.Monad
21import Prelude.Monad
22import IO
22import IO
23
23
24−%access public
24+%access public export
25
25
26---- some basic io
26---- some basic io
27
27
libs/prelude/Prelude/Interfaces.idr+1−1
@@ -4,7 +4,7 @@ import Builtins
4import Prelude.Basics
4import Prelude.Basics
5import Prelude.Bool
5import Prelude.Bool
6
6
7−%access public
7+%access public export
8
8
9-- Numerical Operator Precedence
9-- Numerical Operator Precedence
10infixl 5 ==, /=
10infixl 5 ==, /=
libs/prelude/Prelude/List.idr+1−1
@@ -12,7 +12,7 @@ import Prelude.Maybe
12import Prelude.Uninhabited
12import Prelude.Uninhabited
13import Prelude.Nat
13import Prelude.Nat
14
14
15−%access public
15+%access public export
16%default total
16%default total
17
17
18infix 5 \\
18infix 5 \\
libs/prelude/Prelude/Maybe.idr+1−1
@@ -8,7 +8,7 @@ import Prelude.Cast
8import Prelude.Interfaces
8import Prelude.Interfaces
9import Prelude.Foldable
9import Prelude.Foldable
10
10
11−%access public
11+%access public export
12%default total
12%default total
13
13
14||| An optional value. This can be used to represent the possibility of
14||| An optional value. This can be used to represent the possibility of
libs/prelude/Prelude/Monad.idr+1−1
@@ -8,7 +8,7 @@ import Prelude.Applicative
8import Prelude.Basics
8import Prelude.Basics
9import IO
9import IO
10
10
11−%access public
11+%access public export
12
12
13infixl 5 >>=
13infixl 5 >>=
14
14
libs/prelude/Prelude/Nat.idr+1−1
@@ -9,7 +9,7 @@ import Prelude.Cast
9import Prelude.Interfaces
9import Prelude.Interfaces
10import Prelude.Uninhabited
10import Prelude.Uninhabited
11
11
12−%access public
12+%access public export
13%default total
13%default total
14
14
15||| Natural numbers: unbounded, unsigned integers which can be pattern
15||| Natural numbers: unbounded, unsigned integers which can be pattern
libs/prelude/Prelude/Pairs.idr+1−1
@@ -2,7 +2,7 @@ module Prelude.Pairs
2
2
3import Builtins
3import Builtins
4
4
5−%access public
5+%access public export
6%default total
6%default total
7
7
8swap : (a, b) -> (b, a)
8swap : (a, b) -> (b, a)
libs/prelude/Prelude/Providers.idr+2−2
@@ -4,10 +4,10 @@ import Prelude.Functor
4import Prelude.Applicative
4import Prelude.Applicative
5import Prelude.Monad
5import Prelude.Monad
6
6
7−%access public
7+%access public export
8
8
9||| Type providers must build one of these in an IO computation.
9||| Type providers must build one of these in an IO computation.
10−public
10+public export
11data Provider : (a : Type) -> Type where
11data Provider : (a : Type) -> Type where
12 ||| Return a term to be spliced in
12 ||| Return a term to be spliced in
13 ||| @ x the term to be spliced (i.e. the proof)
13 ||| @ x the term to be spliced (i.e. the proof)
libs/prelude/Prelude/Show.idr+1−1
@@ -14,7 +14,7 @@ import Prelude.Either
14import Prelude.Nat
14import Prelude.Nat
15import Prelude.Strings
15import Prelude.Strings
16
16
17−%access public
17+%access public export
18
18
19%default total
19%default total
20
20
libs/prelude/Prelude/Stream.idr+1−1
@@ -9,7 +9,7 @@ import Prelude.Monad
9import Prelude.Nat
9import Prelude.Nat
10import Prelude.List
10import Prelude.List
11
11
12−%access public
12+%access public export
13%default total
13%default total
14
14
15||| An infinite stream
15||| An infinite stream
libs/prelude/Prelude/Strings.idr+1−1
@@ -17,7 +17,7 @@ import Prelude.Nat
17import Prelude.Monad
17import Prelude.Monad
18import Decidable.Equality
18import Decidable.Equality
19
19
20−%access public
20+%access public export
21
21
22partial
22partial
23foldr1 : (a -> a -> a) -> List a -> a
23foldr1 : (a -> a -> a) -> List a -> a
libs/prelude/Prelude/Traversable.idr+1−1
@@ -7,7 +7,7 @@ import Prelude.Applicative
7import Prelude.Foldable
7import Prelude.Foldable
8import Prelude.Functor
8import Prelude.Functor
9
9
10−%access public
10+%access public export
11
11
12traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
12traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
13traverse_ f = foldr ((*>) . f) (pure ())
13traverse_ f = foldr ((*>) . f) (pure ())
libs/prelude/Prelude/Uninhabited.idr+1−1
@@ -5,7 +5,7 @@ module Prelude.Uninhabited
5
5
6import Builtins
6import Builtins
7
7
8−%access public
8+%access public export
9
9
10||| A canonical proof that some type is empty
10||| A canonical proof that some type is empty
11interface Uninhabited t where
11interface Uninhabited t where
libs/pruviloj/Pruviloj/Core.idr+1−1
@@ -5,7 +5,7 @@ module Pruviloj.Core
5
5
6import Language.Reflection.Utils
6import Language.Reflection.Utils
7
7
8−%access public
8+%access public export
9
9
10||| Run something for effects, throwing away the return value
10||| Run something for effects, throwing away the return value
11ignore : Functor f => f a -> f ()
11ignore : Functor f => f a -> f ()
libs/pruviloj/Pruviloj/Derive/DecEq.idr+1−1
@@ -133,7 +133,7 @@ mkRhs fn fam k =
133||| equality.
133||| equality.
134|||
134|||
135||| @ fn the name of the function whose type has been declared
135||| @ fn the name of the function whose type has been declared
136−abstract partial -- because of mkRhs
136+export partial -- because of mkRhs
137deriveDecEq : (fn : TTName) -> Elab ()
137deriveDecEq : (fn : TTName) -> Elab ()
138deriveDecEq fn =
138deriveDecEq fn =
139 do (_, Ref, sig') <- lookupTyExact fn
139 do (_, Ref, sig') <- lookupTyExact fn
libs/pruviloj/Pruviloj/Derive/Eliminators.idr+1−1
@@ -248,7 +248,7 @@ getElimClauses info elimn ctors =
248 in traverse (\(i, con) => getElimClause info elimn methodCount con i)
248 in traverse (\(i, con) => getElimClause info elimn methodCount con i)
249 (enumerate ctors)
249 (enumerate ctors)
250
250
251−abstract
251+export
252deriveElim : (tyn, elimn : TTName) -> Elab ()
252deriveElim : (tyn, elimn : TTName) -> Elab ()
253deriveElim tyn elimn =
253deriveElim tyn elimn =
254 do -- Begin with some basic sanity checking: the type name uniquely
254 do -- Begin with some basic sanity checking: the type name uniquely
libs/pruviloj/Pruviloj/Disjoint.idr+1−1
@@ -67,7 +67,7 @@ getDisjointness l r = exists <|> declare
67
67
68||| Solve a goal of the form `(C1 x1 x2 ... xn = C2 x1 x2 ... xn) ->
68||| Solve a goal of the form `(C1 x1 x2 ... xn = C2 x1 x2 ... xn) ->
69||| Void` for disjoint constructors `C1` and `C2`.
69||| Void` for disjoint constructors `C1` and `C2`.
70−public covering
70+public export covering
71disjoint : Elab ()
71disjoint : Elab ()
72disjoint =
72disjoint =
73 do compute
73 do compute
libs/pruviloj/Pruviloj/Induction.idr+1−1
@@ -125,7 +125,7 @@ makeMotive info sub subjTy goal =
125
125
126||| Perform induction on some expression to solve the current
126||| Perform induction on some expression to solve the current
127||| goal. Return a list of new holes to be solved.
127||| goal. Return a list of new holes to be solved.
128−public
128+public export
129induction : Raw -> Elab (List TTName)
129induction : Raw -> Elab (List TTName)
130induction subj =
130induction subj =
131 do g <- goalType
131 do g <- goalType
libs/pruviloj/Pruviloj/Injective.idr+1−1
@@ -92,7 +92,7 @@ countBinders _ = Z
92|||
92|||
93||| @ tm the equality to exploit injectivity on
93||| @ tm the equality to exploit injectivity on
94||| @ n the name at which to bind the result
94||| @ n the name at which to bind the result
95−covering public
95+covering public export
96injective : (tm : Raw) -> (n : TTName) -> Elab ()
96injective : (tm : Raw) -> (n : TTName) -> Elab ()
97injective tm n =
97injective tm n =
98 do (_, ty) <- check !getEnv tm
98 do (_, ty) <- check !getEnv tm
libs/pruviloj/Pruviloj/Internals.idr+1−1
@@ -7,7 +7,7 @@ import Pruviloj.Renamers
7
7
8import Data.Vect
8import Data.Vect
9
9
10−%access public
10+%access public export
11
11
12||| Get the name of a reflected type constructor argument.
12||| Get the name of a reflected type constructor argument.
13tyConArgName : TyConArg -> TTName
13tyConArgName : TyConArg -> TTName
libs/pruviloj/Pruviloj/Internals/TyConInfo.idr+1−1
@@ -6,7 +6,7 @@ import Pruviloj.Renamers
6
6
7import Language.Reflection.Utils
7import Language.Reflection.Utils
8
8
9−%access public
9+%access public export
10
10
11||| A representation of a type constructor in which all argument names
11||| A representation of a type constructor in which all argument names
12||| are made unique and they are separated into params and then
12||| are made unique and they are separated into params and then
libs/pruviloj/Pruviloj/Renamers.idr+1−1
@@ -2,7 +2,7 @@ module Pruviloj.Renamers
2
2
3import Language.Reflection.Utils
3import Language.Reflection.Utils
4
4
5−%access public
5+%access public export
6
6
7||| A renamer keeps track of names to be substituted
7||| A renamer keeps track of names to be substituted
8Renamer : Type
8Renamer : Type
src/Idris/Docs.hs+1−1
@@ -19,7 +19,7 @@ import Data.Maybe
19import Data.List
19import Data.List
20import qualified Data.Text as T
20import qualified Data.Text as T
21
21
22−-- TODO: Only include names with public/abstract accessibility
22+-- TODO: Only include names with public/export accessibility
23--
23--
24-- Issue #1573 on the Issue tracker.
24-- Issue #1573 on the Issue tracker.
25-- https://github.com/idris-lang/Idris-dev/issues/1573
25-- https://github.com/idris-lang/Idris-dev/issues/1573
src/Idris/ParseHelpers.hs+20−3
@@ -248,7 +248,7 @@ idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved
248 "where", "with", "syntax", "proof", "postulate",
248 "where", "with", "syntax", "proof", "postulate",
249 "using", "namespace", "class", "instance",
249 "using", "namespace", "class", "instance",
250 "interface", "implementation", "parameters",
250 "interface", "implementation", "parameters",
251− "public", "private", "abstract", "implicit",
251+ "public", "private", "export", "abstract", "implicit",
252 "quoteGoal", "constructor",
252 "quoteGoal", "constructor",
253 "if", "then", "else"]
253 "if", "then", "else"]
254
254
@@ -613,8 +613,25 @@ notOpenBraces = do ist <- get
613
613
614{- | Parses an accessibilty modifier (e.g. public, private) -}
614{- | Parses an accessibilty modifier (e.g. public, private) -}
615accessibility :: IdrisParser Accessibility
615accessibility :: IdrisParser Accessibility
616−accessibility = do reserved "public"; return Public
616+accessibility = do reserved "public";
617+ gotexp <- optional (reserved "export")
618+ case gotexp of
619+ Just _ -> return ()
620+ Nothing -> do
621+ ist <- get
622+ fc <- getFC
623+ put ist { parserWarnings =
624+ (fc, Msg "'public' is deprecated. Use 'public export' instead.")
625+ : parserWarnings ist }
626+ return Public
617− <|> do reserved "abstract"; return Frozen
627+ <|> do reserved "abstract";
628+ ist <- get
629+ fc <- getFC
630+ put ist { parserWarnings =
631+ (fc, Msg "The 'abstract' keyword is deprecated. Use 'export' instead.")
632+ : parserWarnings ist }
633+ return Frozen
634+ <|> do reserved "export"; return Frozen
618 <|> do reserved "private"; return Hidden
635 <|> do reserved "private"; return Hidden
619 <?> "accessibility modifier"
636 <?> "accessibility modifier"
620
637
test/basic009/A.idr+1−1
@@ -1,5 +1,5 @@
1module A
1module A
2
2
3−public
3+public export
4num : Nat
4num : Nat
5num = 0
5num = 0
test/basic009/B/C.idr+1−1
@@ -1,5 +1,5 @@
1module B.C
1module B.C
2
2
3−public
3+public export
4num : Nat
4num : Nat
5num = 1
5num = 1
test/dsl002/Resimp.idr+1−1
@@ -3,7 +3,7 @@ module Resimp
3import public Data.Vect
3import public Data.Vect
4import public Data.Fin
4import public Data.Fin
5
5
6−%access public
6+%access public export
7
7
8-- IO operations which read a resource
8-- IO operations which read a resource
9data Reader : Type -> Type where
9data Reader : Type -> Type where
test/effects003/VectMissing.idr+1−1
@@ -6,7 +6,7 @@ import Data.Vect
6implementation Uninhabited (Elem x []) where
6implementation Uninhabited (Elem x []) where
7 uninhabited Here impossible
7 uninhabited Here impossible
8
8
9−abstract
9+export
10shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a
10shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a
11shrink (x :: ys) Here = ys
11shrink (x :: ys) Here = ys
12shrink (y :: []) (There p) = absurd p
12shrink (y :: []) (There p) = absurd p
test/idrisdoc002/TestFunctions.idr+1−1
@@ -1,6 +1,6 @@
1module TestFunctions
1module TestFunctions
2
2
3||| Test function
3||| Test function
4−public
4+public export
5test : ()
5test : ()
6test = ()
6test = ()
test/idrisdoc003/TestDatatypes.idr+1−1
@@ -1,7 +1,7 @@
1module TestDatatypes
1module TestDatatypes
2
2
3||| This is another test
3||| This is another test
4−public
4+public export
5data Test : Type where
5data Test : Type where
6 ||| Test constructor
6 ||| Test constructor
7 ATest : Test
7 ATest : Test
test/idrisdoc004/TestTypeclasses.idr+1−1
@@ -3,7 +3,7 @@ module TestTypeclasses
3||| This is a test
3||| This is a test
4|||
4|||
5||| @ a Test arg
5||| @ a Test arg
6−public
6+public export
7interface Test a where
7interface Test a where
8 ||| Test function
8 ||| Test function
9 test : a -> Int
9 test : a -> Int
test/idrisdoc005/TestTracing.idr+1−1
@@ -1,5 +1,5 @@
1module TestTracing
1module TestTracing
2
2
3−public
3+public export
4test : Bool
4test : Bool
5test = True
5test = True
test/idrisdoc006/A/fully/Qualified/NAME.idr+1−1
@@ -1,6 +1,6 @@
1module A.fully.Qualified.NAME
1module A.fully.Qualified.NAME
2
2
3||| This is another test
3||| This is another test
4−public data Test : Type where
4+public export data Test : Type where
5 ||| Test constructor
5 ||| Test constructor
6 ATest : Test
6 ATest : Test
test/idrisdoc006/B.idr+1−1
@@ -1,6 +1,6 @@
1module B
1module B
2
2
3||| Test function
3||| Test function
4−public
4+public export
5test : ()
5test : ()
6test = ()
6test = ()
test/idrisdoc008/Abstract.idr+2−2
@@ -1,5 +1,5 @@
1module Abstract
1module Abstract
2
2
3−abstract
3+export
4frozen : ()
4frozen : ()
5−frozen = ()
5+frozen = ()
test/idrisdoc008/Visible.idr+2−2
@@ -1,5 +1,5 @@
1module Visible
1module Visible
2
2
3−public
3+public export
4visible : ()
4visible : ()
5−visible = ()
5+visible = ()
test/idrisdoc009/Test.idr+1−1
@@ -23,7 +23,7 @@
23module Test
23module Test
24import Data.Complex
24import Data.Complex
25
25
26−%access public
26+%access public export
27
27
28myplus : Nat -> Nat -> Nat
28myplus : Nat -> Nat -> Nat
29myplus Z j = j
29myplus Z j = j
test/literate001/Lit.lidr+2−2
@@ -2,12 +2,12 @@
2
2
3Test some string primitives while we're at it
3Test some string primitives while we're at it
4
4
5−> abstract st : String
5+> export st : String
6> st = "abcdefg"
6> st = "abcdefg"
7
7
8Literate main program
8Literate main program
9
9
10−> abstract main : IO ()
10+> export main : IO ()
11> main = do { putStrLn (show (strHead st))
11> main = do { putStrLn (show (strHead st))
12> putStrLn (show (strIndex st 3))
12> putStrLn (show (strIndex st 3))
13> putStrLn (strCons 'z' st)
13> putStrLn (strCons 'z' st)
test/proof002/Reflect.idr+1−1
@@ -2,7 +2,7 @@ module Reflect
2
2
3import Decidable.Equality
3import Decidable.Equality
4
4
5−%access public
5+%access public export
6%default total
6%default total
7
7
8using (xs : List a, ys : List a, G : List (List a))
8using (xs : List a, ys : List a, G : List (List a))
test/proof003/Parity.idr+1−1
@@ -1,6 +1,6 @@
1module Parity
1module Parity
2
2
3−%access public
3+%access public export
4
4
5data Parity : Nat -> Type where
5data Parity : Nat -> Type where
6 Even : {n : Nat} -> Parity (n + n)
6 Even : {n : Nat} -> Parity (n + n)
test/proofsearch002/Process.idr+1−1
@@ -3,7 +3,7 @@ module Process
3import System.Concurrency.Raw
3import System.Concurrency.Raw
4import public Data.List -- public, to get proof search machinery
4import public Data.List -- public, to get proof search machinery
5
5
6−%access public
6+%access public export
7
7
8-- Process IDs are parameterised by their interface. A request of type
8-- Process IDs are parameterised by their interface. A request of type
9-- 'iface t' will get a response of type 't'
9-- 'iface t' will get a response of type 't'
test/reg007/A.lidr+1−1
@@ -1,5 +1,5 @@
1> module A
1> module A
2
2
3−> public n : Nat
3+> public export n : Nat
4> n = ?lala
4> n = ?lala
5
5