68c019a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change export qualifier keywords

abstract is now 'export' public is now 'public export' This is mostly to discourage complete public export unless you really mean it, since it means that the definition effectively becomes part of the interface as well as the type.

commit68c019a69ec546db0affd88723b6cb3acd35a736 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 29 Jan 2016, 14:56 (11 years ago) parenta14e4ed

137 files changed+247−222

compare with master

unifiedsplit

CHANGELOG+11−1

@@ -1,12 +1,22 @@

11New in 0.11:

22============

4−* The export rules have been simplified. Now:

4+Updated export rules

5+--------------------

7+* The export rules are:

58 - 'private' means that the definition is not exported at all

69 - 'export' means that the top level type is exported, but not the

710 definition. In the case of 'data', this means the type constructor is

811 exported but not the data constructors.

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

1020* By default, names are 'private'. This can be altered with an %access

1121 directive as before.

1222

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

@@ -3,7 +3,7 @@ module Control.Arrow

33import Data.Morphisms

44import Control.Category

6−%access public

6+%access public export

88infixr 5 <++>

99infixr 3 ***

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

@@ -2,7 +2,7 @@ module Control.Catchable

33import Control.IOExcept

5−%access public

5+%access public export

77interface Catchable (m : Type -> Type) t where

88 throw : t -> m a

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

@@ -2,7 +2,7 @@ module Control.Category

33import Data.Morphisms

5−%access public

5+%access public export

77interface Category (cat : Type -> Type -> Type) where

88 id : cat a a

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

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

11module Control.IOExcept

3−%access public

3+%access public export

55-- An IO monad with exception handling

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

@@ -4,7 +4,7 @@ import Syntax.PreorderReasoning

44import Data.Fin

66%default total

7−%access public

7+%access public export

99||| An isomorphism between two types

1010data Iso : Type -> Type -> Type where

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

@@ -1,8 +1,8 @@

11module Control.Monad.Identity

3−%access public

3+%access public export

5−public record Identity (a : Type) where

5+public export record Identity (a : Type) where

66 constructor Id

77 runIdentity : a

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

@@ -5,7 +5,7 @@ import Control.Monad.State

55import Control.Monad.Writer

66import Control.Monad.Reader

8−%access public

8+%access public export

1010||| A combination of the Reader, Writer, and State monads

1111interface (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

44import Control.Monad.Identity

55import Control.Monad.Trans

7−%access public

7+%access public export

99||| A monad representing a computation that runs in an immutable context

1010interface Monad m => MonadReader r (m : Type -> Type) where

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

@@ -3,7 +3,7 @@ module Control.Monad.State

33import public Control.Monad.Identity

44import public Control.Monad.Trans

6−%access public

6+%access public export

88||| A computation which runs in a context and produces an output

99interface Monad m => MonadState s (m : Type -> Type) | m where

libs/base/Control/Monad/Trans.idr+1−1

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

11module Control.Monad.Trans

3−%access public

3+%access public export

55interface MonadTrans (t : (Type -> Type) -> Type -> Type) where

66 lift : Monad m => m a -> t m a

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

@@ -4,7 +4,7 @@ import Builtins

44import Control.Monad.Identity

55import Control.Monad.Trans

7−%access public

7+%access public export

99||| A monad representing a computation that produces a stream of output

1010interface (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where

libs/base/Data/Bits.idr+27−27

@@ -4,7 +4,7 @@ import Data.Fin

55%default total

7−public

7+public export

88nextPow2 : Nat -> Nat

99nextPow2 Z = Z

1010nextPow2 (S x) = if (S x) == (2 `power` l2x)

@@ -13,11 +13,11 @@ nextPow2 (S x) = if (S x) == (2 `power` l2x)

1313 where

1414 l2x = log2NZ (S x) SIsNotZ

1515

16−public

16+public export

1717nextBytes : Nat -> Nat

1818nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))

1919

20−public

20+public export

2121machineTy : Nat -> Type

2222machineTy Z = Bits8

2323machineTy (S Z) = Bits16

@@ -47,7 +47,7 @@ natToBits {n=n} x with (n)

4747getPad : Nat -> machineTy n

4848getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)

4949

50−public

50+public export

5151data Bits : Nat -> Type where

5252 MkBits : machineTy (nextBytes n) -> Bits n

5353

@@ -99,7 +99,7 @@ shiftLeft' {n=n} x c with (nextBytes n)

9999 | S (S Z) = pad32' n prim__shlB32 x c

100100 | S (S (S _)) = pad64' n prim__shlB64 x c

101101

102−public

102+public export

103103shiftLeft : Bits n -> Bits n -> Bits n

104104shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)

105105

@@ -110,7 +110,7 @@ shiftRightLogical' {n=n} x c with (n)

110110 | S (S Z) = prim__lshrB32 x c

111111 | S (S (S _)) = prim__lshrB64 x c

112112

113−public

113+public export

114114shiftRightLogical : Bits n -> Bits n -> Bits n

115115shiftRightLogical {n} (MkBits x) (MkBits y)

116116 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)

@@ -122,7 +122,7 @@ shiftRightArithmetic' {n=n} x c with (nextBytes n)

122122 | S (S Z) = pad32' n prim__ashrB32 x c

123123 | S (S (S _)) = pad64' n prim__ashrB64 x c

124124

125−public

125+public export

126126shiftRightArithmetic : Bits n -> Bits n -> Bits n

127127shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)

128128

@@ -133,7 +133,7 @@ and' {n=n} x y with (n)

133133 | S (S Z) = prim__andB32 x y

134134 | S (S (S _)) = prim__andB64 x y

135135

136−public

136+public export

137137and : Bits n -> Bits n -> Bits n

138138and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)

139139

@@ -144,7 +144,7 @@ or' {n=n} x y with (n)

144144 | S (S Z) = prim__orB32 x y

145145 | S (S (S _)) = prim__orB64 x y

146146

147−public

147+public export

148148or : Bits n -> Bits n -> Bits n

149149or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)

150150

@@ -155,7 +155,7 @@ xor' {n=n} x y with (n)

155155 | S (S Z) = prim__xorB32 x y

156156 | S (S (S _)) = prim__xorB64 x y

157157

158−public

158+public export

159159xor : Bits n -> Bits n -> Bits n

160160xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)

161161

@@ -166,7 +166,7 @@ plus' {n=n} x y with (nextBytes n)

166166 | S (S Z) = pad32 n prim__addB32 x y

167167 | S (S (S _)) = pad64 n prim__addB64 x y

168168

169−public

169+public export

170170plus : Bits n -> Bits n -> Bits n

171171plus (MkBits x) (MkBits y) = MkBits (plus' x y)

172172

@@ -177,7 +177,7 @@ minus' {n=n} x y with (nextBytes n)

177177 | S (S Z) = pad32 n prim__subB32 x y

178178 | S (S (S _)) = pad64 n prim__subB64 x y

179179

180−public

180+public export

181181minus : Bits n -> Bits n -> Bits n

182182minus (MkBits x) (MkBits y) = MkBits (minus' x y)

183183

@@ -188,7 +188,7 @@ times' {n=n} x y with (nextBytes n)

188188 | S (S Z) = pad32 n prim__mulB32 x y

189189 | S (S (S _)) = pad64 n prim__mulB64 x y

190190

191−public

191+public export

192192times : Bits n -> Bits n -> Bits n

193193times (MkBits x) (MkBits y) = MkBits (times' x y)

194194

@@ -200,7 +200,7 @@ sdiv' {n=n} x y with (nextBytes n)

200200 | S (S Z) = prim__sdivB32 x y

201201 | S (S (S _)) = prim__sdivB64 x y

202202

203−public partial

203+public export partial

204204sdiv : Bits n -> Bits n -> Bits n

205205sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)

206206

@@ -212,7 +212,7 @@ udiv' {n=n} x y with (nextBytes n)

212212 | S (S Z) = prim__udivB32 x y

213213 | S (S (S _)) = prim__udivB64 x y

214214

215−public partial

215+public export partial

216216udiv : Bits n -> Bits n -> Bits n

217217udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)

218218

@@ -224,7 +224,7 @@ srem' {n=n} x y with (nextBytes n)

224224 | S (S Z) = prim__sremB32 x y

225225 | S (S (S _)) = prim__sremB64 x y

226226

227−public partial

227+public export partial

228228srem : Bits n -> Bits n -> Bits n

229229srem (MkBits x) (MkBits y) = MkBits (srem' x y)

230230

@@ -236,7 +236,7 @@ urem' {n=n} x y with (nextBytes n)

236236 | S (S Z) = prim__uremB32 x y

237237 | S (S (S _)) = prim__uremB64 x y

238238

239−public partial

239+public export partial

240240urem : Bits n -> Bits n -> Bits n

241241urem (MkBits x) (MkBits y) = MkBits (urem' x y)

242242

@@ -302,7 +302,7 @@ complement' {n=n} x with (nextBytes n)

302302 | S (S (S _)) = let pad = getPad {n=3} n in

303303 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad

304304

305−public

305+public export

306306complement : Bits n -> Bits n

307307complement (MkBits x) = MkBits (complement' x)

308308

@@ -321,7 +321,7 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

321321 | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))

322322 | (S (S (S _)), S (S (S _))) = believe_me x

323323

324−public

324+public export

325325zeroExtend : Bits n -> Bits (n+m)

326326zeroExtend (MkBits x) = MkBits (zext' x)

327327

@@ -337,7 +337,7 @@ intToBits' {n=n} x with (nextBytes n)

337337 | S (S (S _)) = let pad = getPad {n=3} n in

338338 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad

339339

340−public

340+public export

341341intToBits : Integer -> Bits n

342342intToBits n = MkBits (intToBits' n)

343343

@@ -351,7 +351,7 @@ bitsToInt' {n=n} x with (nextBytes n)

351351 | S (S Z) = prim__zextB32_BigInt x

352352 | S (S (S _)) = prim__zextB64_BigInt x

353353

354−public

354+public export

355355bitsToInt : Bits n -> Integer

356356bitsToInt (MkBits x) = bitsToInt' x

357357

@@ -393,7 +393,7 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

393393 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in

394394 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)

395395

396−--public

396+--public export

397397--signExtend : Bits n -> Bits (n+m)

398398--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))

399399

@@ -412,23 +412,23 @@ trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))

412412 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))

413413 | (S (S (S _)), S (S (S _))) = believe_me x

414414

415−public

415+public export

416416truncate : Bits (m+n) -> Bits n

417417truncate (MkBits x) = MkBits (zeroUnused (trunc' x))

418418

419−public

419+public export

420420bitAt : Fin n -> Bits n

421421bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)

422422

423−public

423+public export

424424getBit : Fin n -> Bits n -> Bool

425425getBit n x = (x `and` (bitAt n)) /= intToBits 0

426426

427−public

427+public export

428428setBit : Fin n -> Bits n -> Bits n

429429setBit n x = x `or` (bitAt n)

430430

431−public

431+public export

432432unsetBit : Fin n -> Bits n -> Bits n

433433unsetBit n x = x `and` complement (bitAt n)

434434

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

@@ -5,7 +5,7 @@

66module Data.Complex

8−%access public

8+%access public export

1010------------------------------ Rectangular form

1111

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

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

11module Data.Erased

3−%access public

3+%access public export

44%default total

66||| The erasure monad.

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

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

11module Data.Fin

33%default total

4−%access public

4+%access public export

66||| Numbers strictly less than some bound. The name comes from "finite sets".

77|||

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

@@ -2,7 +2,7 @@ module Data.HVect

33import public Data.Vect

5−%access public

5+%access public export

66%default total

88||| Heterogeneous vectors where the type index gives, element-wise,

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

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

11module Data.List

3−%access public

3+%access public export

55||| A proof that some element is found in a list.

66|||

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

@@ -2,7 +2,7 @@ module Data.List.Quantifiers

33import Data.List

5−%access public

5+%access public export

77||| A proof that some element of a list satisfies some property

88|||

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

@@ -5,7 +5,7 @@ import Data.Bits

55%default total

77||| Integers modulo 2^n

8−public

8+public export

99data Mod2 : Nat -> Type where

1010 MkMod2 : {n : Nat} -> Bits n -> Mod2 n

1111

@@ -15,16 +15,16 @@ modBin f (MkMod2 x) (MkMod2 y) = MkMod2 (f x y)

1515modComp : (Bits n -> Bits n -> a) -> Mod2 n -> Mod2 n -> a

1616modComp f (MkMod2 x) (MkMod2 y) = f x y

1717

18−public partial

18+public export partial

1919div : Mod2 n -> Mod2 n -> Mod2 n

2020div = modBin udiv

2121

22−public partial

22+public export partial

2323rem : Mod2 n -> Mod2 n -> Mod2 n

2424rem = modBin urem

2525

2626%assert_total

27−public

27+public export

2828intToMod : {n : Nat} -> Integer -> Mod2 n

2929intToMod {n=n} x = MkMod2 (intToBits x)

3030

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

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

11module Data.Morphisms

3−%access public

3+%access public export

55data Morphism : Type -> Type -> Type where

66 Mor : (a -> b) -> Morphism a b

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

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

11module Data.So

33%default total

4−%access public

4+%access public export

66||| Ensure that some run-time Boolean test has been performed.

77|||

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

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

11module Data.String

2−%access public

2+%access public export

44private

55parseNumWithoutSign : List Char -> Integer -> Maybe Integer

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

@@ -3,7 +3,7 @@ module Data.Vect

33import public Data.Fin

44import Language.Reflection

6−%access public

6+%access public export

77%default total

99infixr 7 ::

libs/base/Data/Vect/Quantifiers.idr+1−1

@@ -2,7 +2,7 @@ module Data.Vect.Quantifiers

33import Data.Vect

5−%access public

5+%access public export

77||| A proof that some element of a vector satisfies some property

88|||

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

@@ -7,7 +7,7 @@ import System

77|||

88||| @ loc The source location to display for the error

99||| @ message The error to print

10−partial abstract

10+partial export

1111error : {default (%runElab sourceLocation) loc : SourceLocation} ->

1212 (message : String) ->

1313 a

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

@@ -3,7 +3,7 @@ module Debug.Trace

33||| Print a message for debugging purposes as a side effect

44||| @ msg what to print

55||| @ result the final result

6−abstract

6+export

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

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

libs/base/Language/Reflection/Utils.idr+1−1

@@ -4,7 +4,7 @@ import Language.Reflection

44import Language.Reflection.Elab

55import Language.Reflection.Errors

7−%access public

7+%access public export

99--------------------------------------------------------

1010-- Tactic construction conveniences

libs/base/Syntax/PreorderReasoning.idr+1−1

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

11module Syntax.PreorderReasoning

3−%access public

3+%access public export

55-- QED is first to get the precedence to work out. It's just Refl with an explicit argument.

66syntax [expr] "QED" = qed expr

libs/base/System.idr+1−1

@@ -2,7 +2,7 @@ module System

33%include C "unistd.h"

44%default partial

5−%access public

5+%access public export

77||| Retrieves a value from the environment if the given key is present,

88||| otherwise it returns Nothing.

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

@@ -6,7 +6,7 @@ module System.Concurrency.Raw

77import System

9−%access abstract

9+%access export

1010

1111||| Send a message of any type to the thread with the given thread id

1212||| Returns 1 if the message was sent successfully, 0 otherwise

libs/base/System/Info.idr+3−3

@@ -1,16 +1,16 @@

11module System.Info

33||| The Idris backend in use

4−abstract

4+export

55backend : String

66backend = prim__systemInfo 0

88||| The operating system in use.

9−abstract

9+export

1010os : String

1111os = prim__systemInfo 1

1212

1313||| The triple this program was targeted for

14−abstract

14+export

1515targetTriple : String

1616targetTriple = prim__systemInfo 2

libs/contrib/Classes/Verified.idr+1−1

@@ -4,7 +4,7 @@ import Control.Algebra

44import Control.Algebra.Lattice

55import Control.Algebra.VectorSpace

7−%access public

7+%access public export

99-- Due to these being basically unused and difficult to implement,

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

33infixl 6 <->

44infixl 7 <.>

6−%access public

6+%access public export

88||| Sets equipped with a single binary operation that is associative, along with

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

33import Control.Algebra

44import Data.Heap

6−%access public

6+%access public export

88||| Sets equipped with a binary operation that is commutative, associative and

99||| idempotent. Must satisfy the following laws:

libs/contrib/Control/Algebra/NumericInstances.idr+1−1

@@ -7,7 +7,7 @@ import Control.Algebra.VectorSpace

77import Data.Complex

88import Data.ZZ

10−%access public

10+%access public export

1111

1212Semigroup Integer where

1313 (<+>) = (+)

libs/contrib/Control/Algebra/VectorSpace.idr+1−1

@@ -2,7 +2,7 @@ module Control.Algebra.VectorSpace

33import Control.Algebra

5−%access public

5+%access public export

77infixl 5 <#>

88infixr 2 <||>

libs/contrib/Control/Isomorphism/Primitives.idr+1−1

@@ -4,7 +4,7 @@ import Control.Isomorphism

44import Data.ZZ

66%default total

7−%access public

7+%access public export

99-- This module contains isomorphisms between convenient inductive types and

1010-- Idris primitives. Because primitives lack a convenient structure, these

libs/contrib/Control/Partial.idr+1−1

@@ -7,7 +7,7 @@ module Control.Partial

77||| @ p the predicate to wait for

88||| @ f the function to repeatedly apply

99||| @ v the starting value

10−partial abstract

10+partial export

1111until : (p : a -> Bool) -> (f : a -> a) -> (v : a) -> a

1212until p f v with (p v)

1313 | False = until p f (f v)

libs/contrib/Control/WellFounded.idr+1−1

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

66module Control.WellFounded

88%default total

9−%access public

9+%access public export

1010

1111||| Accessibility: some element `x` is accessible if all `y` such that

1212||| `rel y x` are themselves accessible.

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

@@ -2,7 +2,7 @@ module Data.BoundedList

33import Data.Fin

5−%access public

5+%access public export

66%default total

88||| A list with an upper bound on its length.

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

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

11module Data.CoList

3−%access public

3+%access public export

44%default total

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

33import public Data.Vect

55%default total

6−%access public

6+%access public export

88||| Build an n-ary function type from a Vect of Types and a result type

99Fun : Vect n Type -> Type -> Type

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

@@ -2,7 +2,7 @@ module Data.Hash

33import Data.Vect

5−%access public

5+%access public export

66%default total

88{- A general purpose Hashing library (not cryptographic)

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

@@ -7,9 +7,9 @@ module Data.Heap

99%default total

10−%access public

10+%access public export

1111

12−abstract data MaxiphobicHeap : Type -> Type where

12+export data MaxiphobicHeap : Type -> Type where

1313 Empty : MaxiphobicHeap a

1414 Node : Nat -> MaxiphobicHeap a -> a -> MaxiphobicHeap a -> MaxiphobicHeap a

1515

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

@@ -5,7 +5,7 @@ module Data.Matrix

55import public Data.Vect

77%default total

8−%access public

8+%access public export

1010||| Matrix with n rows and m columns

1111Matrix : Nat -> Nat -> Type -> Type

libs/contrib/Data/Matrix/Algebraic.idr+1−1

@@ -9,7 +9,7 @@ import public Control.Algebra.NumericInstances

1010import public Data.Matrix

1111

12−%access public

12+%access public export

1313%default total

1414

1515infixr 2 <:> -- vector inner product

libs/contrib/Data/Matrix/Numeric.idr+1−1

@@ -5,7 +5,7 @@ module Data.Matrix.Numeric

55import public Data.Matrix

77%default total

8−%access public

8+%access public export

1010infixr 2 <:> -- vector inner product

1111infixr 2 >< -- vector outer product

libs/contrib/Data/Nat/DivMod.idr+1−1

@@ -2,7 +2,7 @@

22module Data.Nat.DivMod

44%default total

5−%access public

5+%access public export

77||| The result of euclidean division of natural numbers

88|||

libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr+1−1

@@ -8,7 +8,7 @@ import Data.So

88import Control.WellFounded

1010%default total

11−%access public

11+%access public export

1212

1313||| A strict less-than relation on `Nat`.

1414|||

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

@@ -2,7 +2,7 @@ module Data.Rel

33import Data.Fun

5−%access public

5+%access public export

77||| Build an n-ary relation type from a Vect of Types

88Rel : Vect n Type -> Type

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

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

11module Data.Sign

3−%access public

3+%access public export

55||| A representation of signs for signed datatypes such as `ZZ`

66data Sign = Plus | Zero | Minus

libs/contrib/Data/SortedMap.idr+8−8

@@ -192,21 +192,21 @@ treeToList = treeToList' (:: [])

192192 treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1

193193 treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1

194194

195−abstract

195+export

196196data SortedMap : Type -> Type -> Type where

197197 Empty : Ord k => SortedMap k v

198198 M : (o : Ord k) => (n:Nat) -> Tree n k v o -> SortedMap k v

199199

200−public

200+export

201201empty : Ord k => SortedMap k v

202202empty = Empty

203203

204−public

204+export

205205lookup : k -> SortedMap k v -> Maybe v

206206lookup _ Empty = Nothing

207207lookup k (M _ t) = treeLookup k t

208208

209−public

209+export

210210insert : k -> v -> SortedMap k v -> SortedMap k v

211211insert k v Empty = M Z (Leaf k v)

212212insert k v (M _ t) =

@@ -214,7 +214,7 @@ insert k v (M _ t) =

214214 Left t' => (M _ t')

215215 Right t' => (M _ t')

216216

217−public

217+export

218218delete : k -> SortedMap k v -> SortedMap k v

219219delete _ Empty = Empty

220220delete k (M Z t) =

@@ -226,16 +226,16 @@ delete k (M (S _) t) =

226226 Left t' => (M _ t')

227227 Right t' => (M _ t')

228228

229−public

229+export

230230fromList : Ord k => List (k, v) -> SortedMap k v

231231fromList l = foldl (flip (uncurry insert)) empty l

232232

233−public

233+export

234234toList : SortedMap k v -> List (k, v)

235235toList Empty = []

236236toList (M _ t) = treeToList t

237237

238−public

238+export

239239treeMap : (a -> b) -> Tree n k a o -> Tree n k b o

240240treeMap f (Leaf k v) = Leaf k (f v)

241241treeMap 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

55-- TODO: add intersection, union, difference

7−abstract

7+export

88data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())

10−public

10+export

1111empty : Ord k => SortedSet k

1212empty = SetWrapper Data.SortedMap.empty

1313

14−public

14+export

1515insert : k -> SortedSet k -> SortedSet k

1616insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)

1717

18−public

18+export

1919delete : k -> SortedSet k -> SortedSet k

2020delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)

2121

22−public

22+export

2323contains : k -> SortedSet k -> Bool

2424contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)

2525

26−public

26+export

2727fromList : Ord k => List k -> SortedSet k

2828fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))

2929

30−public

30+export

3131toList : SortedSet k -> List k

3232toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)

3333

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

@@ -4,7 +4,7 @@ import Decidable.Equality

44import Data.Sign

66%default total

7−%access public

7+%access public export

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

33import Data.Rel

44import Data.Fun

6−%access public

6+%access public export

88--------------------------------------------------------------------------------

99-- Interface for decidable n-ary Relations

libs/contrib/Decidable/Order.idr+1−1

@@ -6,7 +6,7 @@ import Data.Fin

66import Data.Fun

77import Data.Rel

9−%access public

9+%access public export

1010

1111--------------------------------------------------------------------------------

1212-- Utility Lemmas

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

@@ -4,7 +4,7 @@ import System

55%default total

7−public

7+public export

88Vars : Type

99Vars = List (String, String)

1010

@@ -23,7 +23,7 @@ add_Headers str st = record { Headers = Headers st ++ str } st

2323add_Output : String -> CGIInfo -> CGIInfo

2424add_Output str st = record { Output = Output st ++ str } st

2525

26−abstract

26+export

2727data CGI : Type -> Type where

2828 MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a

2929

@@ -51,32 +51,32 @@ setInfo i = MkCGI (\s => return ((), i))

5151getInfo : CGI CGIInfo

5252getInfo = MkCGI (\s => return (s, s))

5353

54−abstract

54+export

5555lift : IO a -> CGI a

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

5757 return (x, st) } )

5858

59−abstract

59+export

6060output : String -> CGI ()

6161output s = do i <- getInfo

6262 setInfo (add_Output s i)

6363

64−abstract

64+export

6565queryVars : CGI Vars

6666queryVars = do i <- getInfo

6767 return (GET i)

6868

69−abstract

69+export

7070postVars : CGI Vars

7171postVars = do i <- getInfo

7272 return (POST i)

7373

74−abstract

74+export

7575cookieVars : CGI Vars

7676cookieVars = do i <- getInfo

7777 return (Cookies i)

7878

79−abstract

79+export

8080queryVar : String -> CGI (Maybe String)

8181queryVar x = do vs <- queryVars

8282 return (lookup x vs)

@@ -89,12 +89,12 @@ getHeaders : CGI String

8989getHeaders = do i <- getInfo

9090 return (Headers i)

9191

92−abstract

92+export

9393flushHeaders : CGI ()

9494flushHeaders = do o <- getHeaders

9595 lift (putStrLn o)

9696

97−abstract

97+export

9898flush : CGI ()

9999flush = do o <- getOutput

100100 lift (putStr o)

@@ -119,7 +119,7 @@ getCgiEnv key = do

119119 val <- getEnv key

120120 return $ maybe "" id val

121121

122−abstract

122+export

123123runCGI : CGI a -> IO a

124124runCGI prog = do

125125 clen_in <- getCgiEnv "CONTENT_LENGTH"

libs/contrib/Network/Socket.idr+3−5

@@ -8,8 +8,6 @@ module IdrisNet.Socket

88%include C "sys/socket.h"

99%include C "netdb.h"

1010

11−%access public

12−

1311ByteLength : Type

1412ByteLength = Int

1513

@@ -120,18 +118,18 @@ record UDPAddrInfo where

120118 remote_port : Port

121119

122120||| Frees a given pointer

123−public

121+export

124122sock_free : BufPtr -> IO ()

125123sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr

126124

127−public

125+export

128126sockaddr_free : SockaddrPtr -> IO ()

129127sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr

130128

131129||| Allocates an amount of memory given by the ByteLength parameter.

132130|||

133131||| Used to allocate a mutable pointer to be given to the Recv functions.

134−public

132+export

135133sock_alloc : ByteLength -> IO BufPtr

136134sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl

137135

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

@@ -4,9 +4,9 @@ module System.Concurrency.Process

55import System.Concurrency.Raw

7−%access public

7+%access public export

9−abstract

9+export

1010data ProcID msg = MkPID Ptr

1111

1212||| Type safe message passing programs. Parameterised over the type of

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

@@ -2,7 +2,7 @@ module Effect.Default

33import Data.Vect

5−%access public

5+%access public export

77interface Default a where

88 default : a

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

@@ -4,7 +4,7 @@ import Effects

44import System

55import Control.IOExcept

7−%access public

7+%access public export

99data Exception : Type -> Effect where

1010 Raise : a -> sig (Exception a) b

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

@@ -4,7 +4,7 @@ module Effect.File

44import Effects

55import Control.IOExcept

7−%access public

7+%access public export

99||| A Dependent type to describe File Handles. File handles are

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

1414import Effects

1515import public Effect.Logging.Level

1616

17−%access public

17+%access public export

1818

1919-- -------------------------------------------------------- [ Logging Resource ]

2020

libs/effects/Effect/Logging/Default.idr+1−1

@@ -15,7 +15,7 @@ module Effect.Logging.Default

1515import Effects

1616import public Effect.Logging.Level

1717

18−%access public

18+%access public export

1919

2020-- ------------------------------------------------------------ [ The Resource ]

2121

libs/effects/Effect/Logging/Level.idr+1−1

@@ -14,7 +14,7 @@

1414||| loggers.

1515module Effect.Logging.Level

1616

17−%access public

17+%access public export

1818%default total

1919

2020-- ---------------------------------------------------- [ Log Level Definition ]

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

@@ -5,13 +5,13 @@ import Control.IOExcept

55import Data.Vect

66import public Data.So

8−%access public

8+%access public export

10−abstract

10+export

1111data MemoryChunk : Nat -> Nat -> Type where

1212 CH : Ptr -> MemoryChunk size initialized

1313

14−abstract

14+export

1515data RawMemory : Effect where

1616 Allocate : (n : Nat) ->

1717 RawMemory () () (\v => MemoryChunk n 0)

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

@@ -2,7 +2,7 @@ module Effect.Monad

33import Effects

5−%access public

5+%access public export

77data MonadEffT : List EFFECT -> (Type -> Type) -> Type -> Type where

88 MkMonadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a

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

@@ -12,7 +12,7 @@ import System

1212import Effects

1313import Effect.Default

1414

15−%access public

15+%access public export

1616

1717-- ---------------------------------------------------- [ Timer Data Structure ]

1818

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

@@ -3,7 +3,7 @@ module Effect.Random

33import Effects

44import Data.Vect

6−%access public

6+%access public export

88data Random : Effect where

99 GetRandom : sig Random Integer Integer

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

@@ -2,7 +2,7 @@ module Effect.Select

33import Effects

5−%access public

5+%access public export

77data Selection : Effect where

88 Select : List a -> sig Selection a ()

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

@@ -2,7 +2,7 @@ module Effect.State

33import Effects

5−%access public

5+%access public export

77data State : Effect where

88 Get : sig State a a

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

@@ -3,7 +3,7 @@ module Effect.StdIO

33import Effects

44import Control.IOExcept

6−%access public

6+%access public export

88-------------------------------------------------------------

99-- IO effects internals

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

@@ -7,7 +7,7 @@ import Effects

77import System

88import Control.IOExcept

10−%access public

10+%access public export

1111

1212data System : Effect where

1313 Args : sig System (List String)

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

@@ -2,7 +2,7 @@ module Effect.Trans

33import Effects

5−%access public

5+%access public export

77data Trans : (Type -> Type) -> Effect where

88 Lift : m a -> sig (Trans m) a

libs/effects/Effects.idr+1−1

@@ -7,7 +7,7 @@ import Data.Vect

77--- Effectful computations are described as algebraic data types that

88--- explain how an effect is interpreted in some underlying context.

10−%access public

10+%access public export

1111-- ----------------------------------------------------------------- [ Effects ]

1212||| The Effect type describes effectful computations.

1313|||

libs/prelude/Builtins.idr+5−5

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

11%unqualified

3−%access public

3+%access public export

44%default total

66||| The canonical single-element type, also known as the trivially

@@ -155,13 +155,13 @@ assert_total x = x

155155

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

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

159159believe_me : a -> b

160160believe_me x = prim__believe_me _ _ x

161161

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

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

164−public %assert_total

164+public export %assert_total

165165really_believe_me : a -> b

166166really_believe_me x = prim__believe_me _ _ x

167167

@@ -174,8 +174,8 @@ Float = Double

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

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

176176

177−abstract data Ptr : Type

178−abstract data ManagedPtr : Type

177+export data Ptr : Type

178+export data ManagedPtr : Type

179179

180180%extern prim__readFile : prim__WorldType -> Ptr -> String

181181%extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int

libs/prelude/Decidable/Equality.idr+1−1

@@ -9,7 +9,7 @@ import Prelude.List

99import Prelude.Nat

1010import Prelude.Maybe

1111

12−%access public

12+%access public export

1313

1414--------------------------------------------------------------------------------

1515-- Utility lemmas

libs/prelude/IO.idr+9−9

@@ -3,21 +3,21 @@

33import Builtins

44import Prelude.List

6−%access public

6+%access public export

88||| Idris's primitive IO, for building abstractions on top of

9−abstract

9+export

1010data PrimIO : Type -> Type where

1111 Prim__IO : a -> PrimIO a

1212

1313||| A token representing the world, for use in `IO`

14−abstract data World = TheWorld prim__WorldType

14+export data World = TheWorld prim__WorldType

1515

1616private

1717world : World -> prim__WorldType

1818world (TheWorld w) = w

1919

20−abstract WorldRes : Type -> Type

20+export WorldRes : Type -> Type

2121WorldRes x = x

2222

2323||| An FFI specifier, which describes how a particular compiler

@@ -35,7 +35,7 @@ record FFI where

3535

3636||| The IO type, parameterised over the FFI that is available within

3737||| it.

38−abstract

38+export

3939data IO' : (lang : FFI) -> Type -> Type where

4040 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a

4141

@@ -91,25 +91,25 @@ foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) ->

9191 {auto fty : FTy f [] ty} -> ty

9292foreign ffi fname ty {fty} = foreign_prim ffi fname fty []

9393

94−abstract

94+export

9595prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b

9696prim_io_bind (Prim__IO v) k = k v

9797

9898unsafePerformPrimIO : PrimIO a -> a

9999-- compiled as primitive

100100

101−abstract

101+export

102102prim_io_return : a -> PrimIO a

103103prim_io_return x = Prim__IO x

104104

105−abstract

105+export

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

107107io_bind (MkIO fn) k

108108 = MkIO (\w => prim_io_bind (fn w)

109109 (\ b => case k b of

110110 MkIO fkb => fkb w))

111111

112−abstract

112+export

113113io_return : a -> IO' l a

114114io_return x = MkIO (\w => prim_io_return x)

115115

libs/prelude/Language/Reflection.idr+2−2

@@ -9,7 +9,7 @@ import Prelude.List

99import Prelude.Nat

1010import Prelude.Traversable

1111

12−%access public

12+%access public export

1313

1414||| A source location in an Idris file

1515record SourceLocation where

@@ -80,7 +80,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

8080 | WorldType | TheWorld

8181%name Const c, c'

8282

83−abstract interface ReflConst (a : Type) where

83+export interface ReflConst (a : Type) where

8484 toConst : a -> Const

8585

8686implementation ReflConst Int where

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

@@ -16,7 +16,7 @@ import Prelude.Monad

1616import Prelude.Nat

1717import Language.Reflection

1818

19−%access public

19+%access public export

2020

2121data Fixity = Infixl Nat | Infixr Nat | Infix Nat | Prefix Nat

2222

@@ -102,7 +102,7 @@ record Datatype where

102102 constructors : List (TTName, List CtorArg, Raw)

103103

104104||| A reflected elaboration script.

105−abstract

105+export

106106data Elab : Type -> Type where

107107 -- obligatory control stuff

108108 Prim__PureElab : a -> Elab a

@@ -166,7 +166,7 @@ data Elab : Type -> Type where

166166-------------

167167-- Public API

168168-------------

169−%access public

169+%access public export

170170namespace Tactics

171171 implementation Functor Elab where

172172 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

88import Prelude.List

99import Prelude.Maybe

1010

11−%access public

11+%access public export

1212

1313data Err = Msg String

1414 | InternalMsg String

libs/prelude/Prelude.idr+1−1

@@ -33,7 +33,7 @@ import public Language.Reflection

3333import public Language.Reflection.Elab

3434import public Language.Reflection.Errors

3535

36−%access public

36+%access public export

3737%default total

3838

3939-- Things that can't be elsewhere for import cycle reasons

libs/prelude/Prelude/Algebra.idr+1−1

@@ -4,7 +4,7 @@ import Builtins

55infixl 6 <+>

7−%access public

7+%access public export

99--------------------------------------------------------------------------------

1010-- A modest interface hierarchy

libs/prelude/Prelude/Applicative.idr+1−1

@@ -8,7 +8,7 @@ import Prelude.Interfaces

88import Prelude.Foldable

99import Prelude.Functor

1010

11−%access public

11+%access public export

1212

1313---- Applicative functors/Idioms

1414

libs/prelude/Prelude/Basics.idr+1−1

@@ -2,7 +2,7 @@ module Prelude.Basics

33import Builtins

5−%access public

5+%access public export

77Not : Type -> Type

88Not a = a -> Void

libs/prelude/Prelude/Bits.idr+1−1

@@ -12,7 +12,7 @@ import Prelude.Nat

1212import Prelude.List

1313import Prelude.Strings

1414

15−%access public

15+%access public export

1616%default total

1717

1818b8ToString : Bits8 -> String

libs/prelude/Prelude/Bool.idr+1−1

@@ -4,7 +4,7 @@ import Builtins

55import Prelude.Uninhabited

7−%access public

7+%access public export

99||| Boolean Data Type

1010%case data Bool = False | True

libs/prelude/Prelude/Cast.idr+1−1

@@ -3,7 +3,7 @@ module Prelude.Cast

33import Prelude.Bool

44import public Builtins

6−%access public

6+%access public export

88||| Interface for transforming an instance of a data type to another type.

99interface Cast from to where

libs/prelude/Prelude/Chars.idr+1−1

@@ -7,7 +7,7 @@ import Prelude.List

77import Prelude.Cast

88import Builtins

10−%access public

10+%access public export

1111

1212||| Convert the number to its ASCII equivalent.

1313chr : Int -> Char

libs/prelude/Prelude/Doubles.idr+1−1

@@ -3,7 +3,7 @@ module Prelude.Doubles

33import Builtins

44import Prelude.Interfaces

6−%access public

6+%access public export

77%default total

99%include C "math.h"

libs/prelude/Prelude/Either.idr+1−1

@@ -8,7 +8,7 @@ import Prelude.Interfaces

88import Prelude.Maybe

99import Prelude.List

1010

11−%access public

11+%access public export

1212

1313||| A sum type

1414%elim data Either : (a, b : Type) -> Type where

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

@@ -14,10 +14,10 @@ import Prelude.Either

1414import Prelude.Show

1515import IO

1616

17−%access public

17+%access public export

1818

1919||| A file handle

20−abstract

20+export

2121data File : Type where

2222 FHandle : (p : Ptr) -> File

2323

libs/prelude/Prelude/Foldable.idr+1−1

@@ -6,7 +6,7 @@ import Prelude.Basics

66import Prelude.Interfaces

77import Prelude.Algebra

9−%access public

9+%access public export

1010%default total

1111

1212interface Foldable (t : Type -> Type) where

libs/prelude/Prelude/Functor.idr+1−1

@@ -2,7 +2,7 @@ module Prelude.Functor

33import Prelude.Basics

5−%access public

5+%access public export

77||| Functors allow a uniform action over a parameterised type.

88||| @ f a parameterised type

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

@@ -21,7 +21,7 @@ import Prelude.Either

2121import Prelude.Monad

2222import IO

2323

24−%access public

24+%access public export

2525

2626---- some basic io

2727

libs/prelude/Prelude/Interfaces.idr+1−1

@@ -4,7 +4,7 @@ import Builtins

44import Prelude.Basics

55import Prelude.Bool

7−%access public

7+%access public export

99-- Numerical Operator Precedence

1010infixl 5 ==, /=

libs/prelude/Prelude/List.idr+1−1

@@ -12,7 +12,7 @@ import Prelude.Maybe

1212import Prelude.Uninhabited

1313import Prelude.Nat

1414

15−%access public

15+%access public export

1616%default total

1717

1818infix 5 \\

libs/prelude/Prelude/Maybe.idr+1−1

@@ -8,7 +8,7 @@ import Prelude.Cast

88import Prelude.Interfaces

99import Prelude.Foldable

1010

11−%access public

11+%access public export

1212%default total

1313

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

88import Prelude.Basics

99import IO

1010

11−%access public

11+%access public export

1212

1313infixl 5 >>=

1414

libs/prelude/Prelude/Nat.idr+1−1

@@ -9,7 +9,7 @@ import Prelude.Cast

99import Prelude.Interfaces

1010import Prelude.Uninhabited

1111

12−%access public

12+%access public export

1313%default total

1414

1515||| Natural numbers: unbounded, unsigned integers which can be pattern

libs/prelude/Prelude/Pairs.idr+1−1

@@ -2,7 +2,7 @@ module Prelude.Pairs

33import Builtins

5−%access public

5+%access public export

66%default total

88swap : (a, b) -> (b, a)

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

@@ -4,10 +4,10 @@ import Prelude.Functor

44import Prelude.Applicative

55import Prelude.Monad

7−%access public

7+%access public export

99||| Type providers must build one of these in an IO computation.

10−public

10+public export

1111data Provider : (a : Type) -> Type where

1212 ||| Return a term to be spliced in

1313 ||| @ x the term to be spliced (i.e. the proof)

libs/prelude/Prelude/Show.idr+1−1

@@ -14,7 +14,7 @@ import Prelude.Either

1414import Prelude.Nat

1515import Prelude.Strings

1616

17−%access public

17+%access public export

1818

1919%default total

2020

libs/prelude/Prelude/Stream.idr+1−1

@@ -9,7 +9,7 @@ import Prelude.Monad

99import Prelude.Nat

1010import Prelude.List

1111

12−%access public

12+%access public export

1313%default total

1414

1515||| An infinite stream

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

@@ -17,7 +17,7 @@ import Prelude.Nat

1717import Prelude.Monad

1818import Decidable.Equality

1919

20−%access public

20+%access public export

2121

2222partial

2323foldr1 : (a -> a -> a) -> List a -> a

libs/prelude/Prelude/Traversable.idr+1−1

@@ -7,7 +7,7 @@ import Prelude.Applicative

77import Prelude.Foldable

88import Prelude.Functor

10−%access public

10+%access public export

1111

1212traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()

1313traverse_ f = foldr ((*>) . f) (pure ())

libs/prelude/Prelude/Uninhabited.idr+1−1

@@ -5,7 +5,7 @@ module Prelude.Uninhabited

66import Builtins

8−%access public

8+%access public export

1010||| A canonical proof that some type is empty

1111interface Uninhabited t where

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

@@ -5,7 +5,7 @@ module Pruviloj.Core

66import Language.Reflection.Utils

8−%access public

8+%access public export

1010||| Run something for effects, throwing away the return value

1111ignore : Functor f => f a -> f ()

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

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

133133||| equality.

134134|||

135135||| @ fn the name of the function whose type has been declared

136−abstract partial -- because of mkRhs

136+export partial -- because of mkRhs

137137deriveDecEq : (fn : TTName) -> Elab ()

138138deriveDecEq fn =

139139 do (_, Ref, sig') <- lookupTyExact fn

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

@@ -248,7 +248,7 @@ getElimClauses info elimn ctors =

248248 in traverse (\(i, con) => getElimClause info elimn methodCount con i)

249249 (enumerate ctors)

250250

251−abstract

251+export

252252deriveElim : (tyn, elimn : TTName) -> Elab ()

253253deriveElim tyn elimn =

254254 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

6767

6868||| Solve a goal of the form `(C1 x1 x2 ... xn = C2 x1 x2 ... xn) ->

6969||| Void` for disjoint constructors `C1` and `C2`.

70−public covering

70+public export covering

7171disjoint : Elab ()

7272disjoint =

7373 do compute

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

@@ -125,7 +125,7 @@ makeMotive info sub subjTy goal =

125125

126126||| Perform induction on some expression to solve the current

127127||| goal. Return a list of new holes to be solved.

128−public

128+public export

129129induction : Raw -> Elab (List TTName)

130130induction subj =

131131 do g <- goalType

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

@@ -92,7 +92,7 @@ countBinders _ = Z

9292|||

9393||| @ tm the equality to exploit injectivity on

9494||| @ n the name at which to bind the result

95−covering public

95+covering public export

9696injective : (tm : Raw) -> (n : TTName) -> Elab ()

9797injective tm n =

9898 do (_, ty) <- check !getEnv tm

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

@@ -7,7 +7,7 @@ import Pruviloj.Renamers

88import Data.Vect

10−%access public

10+%access public export

1111

1212||| Get the name of a reflected type constructor argument.

1313tyConArgName : TyConArg -> TTName

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

@@ -6,7 +6,7 @@ import Pruviloj.Renamers

77import Language.Reflection.Utils

9−%access public

9+%access public export

1010

1111||| A representation of a type constructor in which all argument names

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

33import Language.Reflection.Utils

5−%access public

5+%access public export

77||| A renamer keeps track of names to be substituted

88Renamer : Type

src/Idris/Docs.hs+1−1

@@ -19,7 +19,7 @@ import Data.Maybe

1919import Data.List

2020import qualified Data.Text as T

2121

22−-- TODO: Only include names with public/abstract accessibility

22+-- TODO: Only include names with public/export accessibility

2323--

2424-- Issue #1573 on the Issue tracker.

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

248248 "where", "with", "syntax", "proof", "postulate",

249249 "using", "namespace", "class", "instance",

250250 "interface", "implementation", "parameters",

251− "public", "private", "abstract", "implicit",

251+ "public", "private", "export", "abstract", "implicit",

252252 "quoteGoal", "constructor",

253253 "if", "then", "else"]

254254

@@ -613,8 +613,25 @@ notOpenBraces = do ist <- get

613613

614614{- | Parses an accessibilty modifier (e.g. public, private) -}

615615accessibility :: IdrisParser Accessibility

616−accessibility = do reserved "public"; return Public

617− <|> do reserved "abstract"; return Frozen

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

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

618635 <|> do reserved "private"; return Hidden

619636 <?> "accessibility modifier"

620637

test/basic009/A.idr+1−1

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

11module A

3−public

3+public export

44num : Nat

55num = 0

test/basic009/B/C.idr+1−1

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

11module B.C

3−public

3+public export

44num : Nat

55num = 1

test/dsl002/Resimp.idr+1−1

@@ -3,7 +3,7 @@ module Resimp

33import public Data.Vect

44import public Data.Fin

6−%access public

6+%access public export

88-- IO operations which read a resource

99data Reader : Type -> Type where

test/effects003/VectMissing.idr+1−1

@@ -6,7 +6,7 @@ import Data.Vect

66implementation Uninhabited (Elem x []) where

77 uninhabited Here impossible

9−abstract

9+export

1010shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a

1111shrink (x :: ys) Here = ys

1212shrink (y :: []) (There p) = absurd p

test/idrisdoc002/TestFunctions.idr+1−1

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

11module TestFunctions

33||| Test function

4−public

4+public export

55test : ()

66test = ()

test/idrisdoc003/TestDatatypes.idr+1−1

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

11module TestDatatypes

33||| This is another test

4−public

4+public export

55data Test : Type where

66 ||| Test constructor

77 ATest : Test

test/idrisdoc004/TestTypeclasses.idr+1−1

@@ -3,7 +3,7 @@ module TestTypeclasses

33||| This is a test

44|||

55||| @ a Test arg

6−public

6+public export

77interface Test a where

88 ||| Test function

99 test : a -> Int

test/idrisdoc005/TestTracing.idr+1−1

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

11module TestTracing

3−public

3+public export

44test : Bool

55test = True

test/idrisdoc006/A/fully/Qualified/NAME.idr+1−1

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

11module A.fully.Qualified.NAME

33||| This is another test

4−public data Test : Type where

4+public export data Test : Type where

55 ||| Test constructor

66 ATest : Test

test/idrisdoc006/B.idr+1−1

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

11module B

33||| Test function

4−public

4+public export

55test : ()

66test = ()

test/idrisdoc008/Abstract.idr+2−2

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

11module Abstract

3−abstract

3+export

44frozen : ()

5−frozen = ()

5+frozen = ()

test/idrisdoc008/Visible.idr+2−2

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

11module Visible

3−public

3+public export

44visible : ()

5−visible = ()

5+visible = ()

test/idrisdoc009/Test.idr+1−1

@@ -23,7 +23,7 @@

2323module Test

2424import Data.Complex

2525

26−%access public

26+%access public export

2727

2828myplus : Nat -> Nat -> Nat

2929myplus Z j = j

test/literate001/Lit.lidr+2−2

@@ -2,12 +2,12 @@

33Test some string primitives while we're at it

5−> abstract st : String

5+> export st : String

66> st = "abcdefg"

88Literate main program

10−> abstract main : IO ()

10+> export main : IO ()

1111> main = do { putStrLn (show (strHead st))

1212> putStrLn (show (strIndex st 3))

1313> putStrLn (strCons 'z' st)

test/proof002/Reflect.idr+1−1

@@ -2,7 +2,7 @@ module Reflect

33import Decidable.Equality

5−%access public

5+%access public export

66%default total

88using (xs : List a, ys : List a, G : List (List a))

test/proof003/Parity.idr+1−1

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

11module Parity

3−%access public

3+%access public export

55data Parity : Nat -> Type where

66 Even : {n : Nat} -> Parity (n + n)

test/proofsearch002/Process.idr+1−1

@@ -3,7 +3,7 @@ module Process

33import System.Concurrency.Raw

44import public Data.List -- public, to get proof search machinery

6−%access public

6+%access public export

88-- Process IDs are parameterised by their interface. A request of type

99-- 'iface t' will get a response of type 't'

test/reg007/A.lidr+1−1

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

11> module A

3−> public n : Nat

3+> public export n : Nat

44> n = ?lala