e3e35a5 · Idris-dev · git.iko.soy

CHANGELOG+2−7

@@ -10,15 +10,10 @@ Updated export rules

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

1111 exported but not the data constructors.

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

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

2114 directive as before.

15+* Exported types can only refer to other exported names

16+* Publicly exported definitions can only refer to publicly exported names

2217

2318New in 0.10:

2419============

libs/base/Data/Bits.idr+24−5

@@ -92,6 +92,10 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad

9292 where

9393 pad = getPad {n=3} n

9494

95+-- TODO: This (and all the other functions along these lings) is public export

96+-- because it is used by public export things. Do they really need to be

97+-- public export, or is export good enough?

98+public export

9599shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

96100shiftLeft' {n=n} x c with (nextBytes n)

97101 | Z = pad8' n prim__shlB8 x c

@@ -103,6 +107,7 @@ public export

103107shiftLeft : Bits n -> Bits n -> Bits n

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

105109

110+public export

106111shiftRightLogical' : machineTy n -> machineTy n -> machineTy n

107112shiftRightLogical' {n=n} x c with (n)

108113 | Z = prim__lshrB8 x c

@@ -115,6 +120,7 @@ shiftRightLogical : Bits n -> Bits n -> Bits n

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

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

117122

123+public export

118124shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

119125shiftRightArithmetic' {n=n} x c with (nextBytes n)

120126 | Z = pad8' n prim__ashrB8 x c

@@ -126,6 +132,7 @@ public export

126132shiftRightArithmetic : Bits n -> Bits n -> Bits n

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

128134

135+public export

129136and' : machineTy n -> machineTy n -> machineTy n

130137and' {n=n} x y with (n)

131138 | Z = prim__andB8 x y

@@ -137,6 +144,7 @@ public export

137144and : Bits n -> Bits n -> Bits n

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

139146

147+public export

140148or' : machineTy n -> machineTy n -> machineTy n

141149or' {n=n} x y with (n)

142150 | Z = prim__orB8 x y

@@ -148,6 +156,7 @@ public export

148156or : Bits n -> Bits n -> Bits n

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

150158

159+public export

151160xor' : machineTy n -> machineTy n -> machineTy n

152161xor' {n=n} x y with (n)

153162 | Z = prim__xorB8 x y

@@ -159,6 +168,7 @@ public export

159168xor : Bits n -> Bits n -> Bits n

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

161170

171+public export

162172plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

163173plus' {n=n} x y with (nextBytes n)

164174 | Z = pad8 n prim__addB8 x y

@@ -170,6 +180,7 @@ public export

170180plus : Bits n -> Bits n -> Bits n

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

172182

183+public export

173184minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

174185minus' {n=n} x y with (nextBytes n)

175186 | Z = pad8 n prim__subB8 x y

@@ -181,6 +192,7 @@ public export

181192minus : Bits n -> Bits n -> Bits n

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

183194

195+public export

184196times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

185197times' {n=n} x y with (nextBytes n)

186198 | Z = pad8 n prim__mulB8 x y

@@ -193,6 +205,7 @@ times : Bits n -> Bits n -> Bits n

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

194206

195207partial

208+public export

196209sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

197210sdiv' {n=n} x y with (nextBytes n)

198211 | Z = prim__sdivB8 x y

@@ -205,6 +218,7 @@ sdiv : Bits n -> Bits n -> Bits n

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

206219

207220partial

221+public export

208222udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

209223udiv' {n=n} x y with (nextBytes n)

210224 | Z = prim__udivB8 x y

@@ -216,7 +230,7 @@ public export partial

216230udiv : Bits n -> Bits n -> Bits n

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

218232

219−partial

233+public export partial

220234srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

221235srem' {n=n} x y with (nextBytes n)

222236 | Z = prim__sremB8 x y

@@ -228,7 +242,7 @@ public export partial

228242srem : Bits n -> Bits n -> Bits n

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

230244

231−partial

245+public export partial

232246urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

233247urem' {n=n} x y with (nextBytes n)

234248 | Z = prim__uremB8 x y

@@ -276,9 +290,11 @@ gt {n=n} x y with (nextBytes n)

276290 | S (S Z) = prim__gtB32 x y

277291 | S (S (S _)) = prim__gtB64 x y

278292

293+public export

279294implementation Eq (Bits n) where

280295 (MkBits x) == (MkBits y) = boolOp eq x y

281296

297+public export

282298implementation Ord (Bits n) where

283299 (MkBits x) < (MkBits y) = boolOp lt x y

284300 (MkBits x) <= (MkBits y) = boolOp lte x y

@@ -291,6 +307,7 @@ implementation Ord (Bits n) where

291307 then EQ

292308 else GT

293309

310+public export

294311complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)

295312complement' {n=n} x with (nextBytes n)

296313 | Z = let pad = getPad {n=0} n in

@@ -307,7 +324,7 @@ complement : Bits n -> Bits n

307324complement (MkBits x) = MkBits (complement' x)

308325

309326-- TODO: Prove

310−%assert_total -- can't verify coverage of with block

327+public export %assert_total -- can't verify coverage of with block

311328zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

312329zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

313330 | (Z, Z) = believe_me x

@@ -325,7 +342,7 @@ public export

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

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

327344

328−%assert_total

345+public export %assert_total

329346intToBits' : Integer -> machineTy (nextBytes n)

330347intToBits' {n=n} x with (nextBytes n)

331348 | Z = let pad = getPad {n=0} n in

@@ -344,6 +361,7 @@ intToBits n = MkBits (intToBits' n)

344361implementation Cast Integer (Bits n) where

345362 cast = intToBits

346363

364+public export

347365bitsToInt' : machineTy (nextBytes n) -> Integer

348366bitsToInt' {n=n} x with (nextBytes n)

349367 | Z = prim__zextB8_BigInt x

@@ -356,6 +374,7 @@ bitsToInt : Bits n -> Integer

356374bitsToInt (MkBits x) = bitsToInt' x

357375

358376-- Zero out the high bits of a truncated bitstring

377+public export

359378zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)

360379zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)

361380

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

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

399418

400419-- TODO: Prove

401−%assert_total -- can't verify coverage of with block

420+public export %assert_total -- can't verify coverage of with block

402421trunc' : machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)

403422trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))

404423 | (Z, Z) = believe_me x

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

@@ -149,7 +149,7 @@ mkFinIntegerErr lit finSize subErr

149149 , TermPart `(Fin ~(getNat finSize))

150150 , SubReport subErr

151151 ]

152−total

152+total export

153153finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)

154154finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(TConst c) ~m)) err xs y)

155155 = mkFinIntegerErr (TConst c) m

libs/base/Data/Mod2.idr+1

@@ -9,6 +9,7 @@ public export

99data Mod2 : Nat -> Type where

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

1111

12+public export

1213modBin : (Bits n -> Bits n -> Bits n) -> Mod2 n -> Mod2 n -> Mod2 n

1314modBin f (MkMod2 x) (MkMod2 y) = MkMod2 (f x y)

1415

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

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

77

88

99%default total

10−%access public export

10+%access export

1111

1212export data MaxiphobicHeap : Type -> Type where

1313 Empty : MaxiphobicHeap a

libs/contrib/Data/SortedMap.idr−1

@@ -235,7 +235,6 @@ toList : SortedMap k v -> List (k, v)

235235toList Empty = []

236236toList (M _ t) = treeToList t

237237

238−export

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

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

241240treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)

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

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

88%include C "sys/socket.h"

99%include C "netdb.h"

1010

11−ByteLength : Type

11+public export ByteLength : Type

1212ByteLength = Int

1313

1414interface ToCode a where

@@ -65,8 +65,9 @@ implementation ToCode SocketType where

6565

6666data RecvStructPtr = RSPtr Ptr

6767data RecvfromStructPtr = RFPtr Ptr

68−data BufPtr = BPtr Ptr

69−data SockaddrPtr = SAPtr Ptr

68+

69+export data BufPtr = BPtr Ptr

70+export data SockaddrPtr = SAPtr Ptr

7071

7172||| Protocol Number.

7273|||

libs/effects/Effect/Memory.idr+1

@@ -155,6 +155,7 @@ move' src_ptr dst_offset src_offset size dst_bounds src_bounds

155155

156156data MoveDescriptor = Dst | Src

157157

158+export

158159move : {dst_size : Nat} ->

159160 {dst_init : Nat} ->

160161 {src_size : Nat} ->

libs/effects/Effects.idr+25−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.

99

10−%access public export

10+%access export

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

1212||| The Effect type describes effectful computations.

1313|||

@@ -15,11 +15,13 @@ import Data.Vect

1515||| + The return type of the computation.

1616||| + The input resource.

1717||| + The computation to run on the resource given the return value.

18+public export

1819Effect : Type

1920Effect = (x : Type) -> Type -> (x -> Type) -> Type

2021

2122||| The `EFFECT` Data type describes how to promote the Effect

2223||| description into a concrete effect.

24+public export

2325%error_reverse

2426data EFFECT : Type where

2527 MkEff : Type -> Effect -> EFFECT

@@ -30,24 +32,29 @@ data EFFECT : Type where

3032-- or a dependent change. These are easily disambiguated by type.

3133

3234namespace NoResourceEffect

35+ public export

3336 sig : Effect -> Type -> Type

3437 sig e r = e r () (\v => ())

3538

3639namespace NoUpdateEffect

40+ public export

3741 sig : Effect -> (ret : Type) -> (resource : Type) -> Type

3842 sig e r e_in = e r e_in (\v => e_in)

3943

4044namespace UpdateEffect

45+ public export

4146 sig : Effect -> (ret : Type) -> (res_in : Type) -> (res_out : Type) -> Type

4247 sig e r e_in e_out = e r e_in (\v => e_out)

4348

4449namespace DepUpdateEffect

50+ public export

4551 sig : Effect ->

4652 (ret : Type) -> (res_in : Type) -> (res_out : ret -> Type) -> Type

4753 sig e r e_in e_out = e r e_in e_out

4854

4955||| Handler interfaces describe how an effect `e` is translated to the

5056||| underlying computation context `m` for execution.

57+public export

5158interface Handler (e : Effect) (m : Type -> Type) where

5259 ||| How to handle the effect.

5360 |||

@@ -77,6 +84,7 @@ syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]

7784syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)

7885

7986-- --------------------------------------- [ Properties and Proof Construction ]

87+public export

8088data SubList : List a -> List a -> Type where

8189 SubNil : SubList [] []

8290 Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)

@@ -88,21 +96,25 @@ subListId {xs = Nil} = SubNil

8896subListId {xs = x :: xs} = Keep subListId

8997

9098namespace Env

99+ public export

91100 data Env : (m : Type -> Type) -> List EFFECT -> Type where

92101 Nil : Env m Nil

93102 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)

94103

104+public export

95105data EffElem : Effect -> Type ->

96106 List EFFECT -> Type where

97107 Here : EffElem x a (MkEff a x :: xs)

98108 There : EffElem x a xs -> EffElem x a (y :: xs)

99109

100110||| make an environment corresponding to a sub-list

111+private

101112dropEnv : Env m ys -> SubList xs ys -> Env m xs

102113dropEnv [] SubNil = []

103114dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest

104115dropEnv (v :: vs) (Drop rest) = dropEnv vs rest

105116

117+public export

106118updateWith : (ys' : List a) -> (xs : List a) ->

107119 SubList ys xs -> List a

108120updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest

@@ -112,6 +124,7 @@ updateWith (y :: ys) [] SubNil = y :: ys

112124updateWith [] (x :: xs) (Keep rest) = []

113125

114126||| Put things back, replacing old with new in the sub-environment

127+private

115128rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->

116129 Env m xs -> Env m (updateWith ys' xs prf)

117130rebuildEnv [] SubNil env = env

@@ -123,6 +136,7 @@ rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env

123136

124137-- -------------------------------------------------- [ The Effect EDSL itself ]

125138

139+public export

126140updateResTy : (val : t) ->

127141 (xs : List EFFECT) -> EffElem e a xs -> e t a b ->

128142 List EFFECT

@@ -131,9 +145,11 @@ updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n

131145

132146infix 5 :::, :-, :=

133147

148+public export

134149data LRes : lbl -> Type -> Type where

135150 (:=) : (x : lbl) -> res -> LRes x res

136151

152+public export

137153(:::) : lbl -> EFFECT -> EFFECT

138154(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e

139155

@@ -156,6 +172,7 @@ relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs

156172||| @ x The return type of the result.

157173||| @ es The list of allowed side-effects.

158174||| @ ce Function to compute a new list of allowed side-effects.

175+public export

159176data EffM : (m : Type -> Type) -> (x : Type)

160177 -> (es : List EFFECT)

161178 -> (ce : x -> List EFFECT) -> Type where

@@ -182,27 +199,33 @@ data EffM : (m : Type -> Type) -> (x : Type)

182199

183200namespace SimpleEff

184201 -- Simple effects, no updates

202+ public export

185203 Eff : (x : Type) -> (es : List EFFECT) -> Type

186204 Eff x es = {m : Type -> Type} -> EffM m x es (\v => es)

187205

206+ public export

188207 EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT) -> Type

189208 EffT m x es = EffM m x es (\v => es)

190209

191210namespace TransEff

192211 -- Dependent effects, updates not dependent on result

212+ public export

193213 Eff : (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type

194214 Eff x es ce = {m : Type -> Type} -> EffM m x es (\_ => ce)

195215

216+ public export

196217 EffT : (m : Type -> Type) ->

197218 (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type

198219 EffT m x es ce = EffM m x es (\_ => ce)

199220

200221namespace DepEff

201222 -- Dependent effects, updates dependent on result

223+ public export

202224 Eff : (x : Type) -> (es : List EFFECT)

203225 -> (ce : x -> List EFFECT) -> Type

204226 Eff x es ce = {m : Type -> Type} -> EffM m x es ce

205227

228+ public export

206229 EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT)

207230 -> (ce : x -> List EFFECT) -> Type

208231 EffT m x es ce = EffM m x es ce

@@ -271,6 +294,7 @@ execEff (val :: env) (There p) eff k

271294-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

272295-- updates can be propagated even through failing computations?

273296

297+export

274298eff : Env m xs -> EffM m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b

275299eff env (Value x) k = k x env

276300eff env (prog `EBind` c) k

libs/prelude/IO.idr+22−9

@@ -3,25 +3,25 @@

33import Builtins

44import Prelude.List

55

6−%access public export

6+%access export

77

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

9−export

109data PrimIO : Type -> Type where

1110 Prim__IO : a -> PrimIO a

1211

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

14−export data World = TheWorld prim__WorldType

13+data World = TheWorld prim__WorldType

1514

1615private

1716world : World -> prim__WorldType

1817world (TheWorld w) = w

1918

20−export WorldRes : Type -> Type

19+WorldRes : Type -> Type

2120WorldRes x = x

2221

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

2423||| backend handles foreign function calls.

24+public export

2525record FFI where

2626 constructor MkFFI

2727 ||| A family describing which types are available in the FFI

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

3535

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

3737||| it.

38−export

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

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

4140

41+public export

4242data FTy : FFI -> List Type -> Type -> Type where

4343 FRet : ffi_types f t -> FTy f xs (IO' f t)

4444 FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)

@@ -54,6 +54,7 @@ ForeignPrimType {ffi} (x :: xs) ((a, _) :: env) t

5454 = (ffi_types ffi x, x) -> ForeignPrimType xs env t

5555

5656%inline

57+private

5758applyEnv : (env : FEnv ffi xs) ->

5859 ForeignPrimType xs env t ->

5960 World -> ffi_fn ffi -> ffi_types ffi t -> PrimIO t

@@ -66,6 +67,7 @@ mkForeignPrim : {xs : _} -> {ffi : _} -> {env : FEnv ffi xs} -> {t : Type} ->

6667-- explicit here.

6768

6869%inline

70+private

6971foreign_prim : (f : FFI) ->

7072 (fname : ffi_fn f) -> FTy f xs ty -> FEnv f xs -> ty

7173foreign_prim f fname (FRet y) env

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

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

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

9395

94−export

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

9697prim_io_bind (Prim__IO v) k = k v

9798

9899unsafePerformPrimIO : PrimIO a -> a

99100-- compiled as primitive

100101

101−export

102102prim_io_return : a -> PrimIO a

103103prim_io_return x = Prim__IO x

104104

105−export

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

107106io_bind (MkIO fn) k

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

109108 (\ b => case k b of

110109 MkIO fkb => fkb w))

111110

112−export

113111io_return : a -> IO' l a

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

115113

@@ -143,6 +141,7 @@ prim_fwrite h s

143141

144142--------- The C FFI

145143namespace FFI_C

144+ public export

146145 data Raw : Type -> Type where

147146 -- code generated can assume it's compiled just as 't'

148147 MkRaw : (x : t) -> Raw t

@@ -151,6 +150,7 @@ namespace FFI_C

151150 %used MkRaw x

152151

153152 ||| Supported C integer types

153+ public export

154154 data C_IntTypes : Type -> Type where

155155 C_IntChar : C_IntTypes Char

156156 C_IntNative : C_IntTypes Int

@@ -160,6 +160,7 @@ namespace FFI_C

160160 C_IntBits64 : C_IntTypes Bits64

161161

162162 ||| Supported C foreign types

163+ public export

163164 data C_Types : Type -> Type where

164165 C_Str : C_Types String

165166 C_Float : C_Types Double

@@ -172,12 +173,14 @@ namespace FFI_C

172173 ||| A descriptor for the C FFI. See the constructors of `C_Types`

173174 ||| and `C_IntTypes` for the concrete types that are available.

174175 %error_reverse

176+ public export

175177 FFI_C : FFI

176178 FFI_C = MkFFI C_Types String String

177179

178180||| Interactive programs, describing I/O actions and returning a value.

179181||| @res The result type of the program

180182%error_reverse

183+public export

181184IO : (res : Type) -> Type

182185IO = IO' FFI_C

183186

@@ -207,18 +210,22 @@ namespace IO

207210

208211-- Supported JS foreign types

209212mutual

213+ public export

210214 data JsFn : Type -> Type where

211215 MkJsFn : (x : t) -> JsFn t

212216

217+ public export

213218 data JS_IntTypes : Type -> Type where

214219 JS_IntChar : JS_IntTypes Char

215220 JS_IntNative : JS_IntTypes Int

216221

222+ public export

217223 data JS_FnTypes : Type -> Type where

218224 JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)

219225 JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)

220226 JS_FnBase : JS_Types t -> JS_FnTypes t

221227

228+ public export

222229 data JS_Types : Type -> Type where

223230 JS_Str : JS_Types String

224231 JS_Float : JS_Types Double

@@ -236,10 +243,12 @@ mutual

236243||| JavaScript code snippets, into which the arguments are substituted

237244||| for the placeholders `%0`, `%1`, etc.

238245%error_reverse

246+public export

239247FFI_JS : FFI

240248FFI_JS = MkFFI JS_Types String String

241249

242250%error_reverse

251+public export

243252JS_IO : Type -> Type

244253JS_IO = IO' FFI_JS

245254

@@ -249,10 +258,12 @@ JS_IO = IO' FFI_JS

249258namespace FFI_Export

250259-- It's just like Data.List.Elem, but we don't need all the other stuff

251260-- that comes with it, just a proof that a data type is defined.

261+ public export

252262 data DataDefined : Type -> List (Type, s) -> s -> Type where

253263 DHere : DataDefined x ((x, t) :: xs) t

254264 DThere : DataDefined x xs t -> DataDefined x (y :: xs) t

255265

266+ public export

256267 data FFI_Base : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where

257268 FFI_ExpType : {n : ffi_data f} -> (def : DataDefined t xs n) -> FFI_Base f xs t

258269 FFI_Prim : (prim : ffi_types f t) -> FFI_Base f xs t

@@ -261,6 +272,7 @@ namespace FFI_Export

261272 %used FFI_ExpType def

262273 %used FFI_Prim prim

263274

275+ public export

264276 data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where

265277 FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO' f t)

266278 FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)

@@ -271,6 +283,7 @@ namespace FFI_Export

271283 %used FFI_Fun a

272284 %used FFI_Ret b

273285

286+ public export

274287 data FFI_Export : (f : FFI) -> String -> List (Type, ffi_data f) -> Type where

275288 Data : (x : Type) -> (n : ffi_data f) ->

276289 (es : FFI_Export f h ((x, n) :: xs)) -> FFI_Export f h xs

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

@@ -110,7 +110,7 @@ implementation ReflConst Bits32 where

110110implementation ReflConst Bits64 where

111111 toConst = B64

112112

113−implicit

113+implicit export

114114reflectConstant: (ReflConst a) => a -> Const

115115reflectConstant = toConst

116116

libs/prelude/Prelude.idr+2−1

@@ -270,7 +270,7 @@ cast_part : TT -> ErrorReportPart

270270cast_part (P Bound n t) = TextPart "unknown type"

271271cast_part x = TermPart x

272272

273−%error_handler

273+%error_handler export

274274cast_error : Err -> Maybe (List ErrorReportPart)

275275cast_error (CantResolve `(Cast ~x ~y))

276276 = Just [TextPart "Can't cast from",

@@ -280,6 +280,7 @@ cast_error (CantResolve `(Cast ~x ~y))

280280cast_error _ = Nothing

281281

282282%error_handler

283+export

283284num_error : Err -> Maybe (List ErrorReportPart)

284285num_error (CantResolve `(Num ~x))

285286 = Just [TermPart x, TextPart "is not a numeric type"]

src/IRTS/Compiler.hs+1−1

@@ -462,7 +462,7 @@ doForeign vs env (ret : fname : world : args)

462462 = do let l' = toFDesc l

463463 r' <- irTerm vs env r

464464 return (l', r')

465− splitArg _ = ifail "Badly formed foreign function call"

465+ splitArg _ = ifail $ "Badly formed foreign function call"

466466

467467 toFDesc (Constant (Str str)) = FStr str

468468 toFDesc tm

src/Idris/AbsSyntax.hs+7−2

@@ -207,6 +207,11 @@ setAccessibility n a

207207 let ctxt = setAccess n a (tt_ctxt i)

208208 putIState $ i { tt_ctxt = ctxt }

209209

210+-- | get the accessibility of a name outside this module

211+getFromHideList :: Name -> Idris (Maybe Accessibility)

212+getFromHideList n = do i <- getIState

213+ return $ lookupCtxtExact n (hide_list i)

214+

210215setTotality :: Name -> Totality -> Idris ()

211216setTotality n a

212217 = do i <- getIState

@@ -1258,10 +1263,10 @@ expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds dec

12581263 (map (expandParamsD rhs ist dec ps ns) decls)

12591264 cn

12601265 cd

1261−expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n nfc params ty cn decls)

1266+expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs acc n nfc params ty cn decls)

12621267 = PInstance doc argDocs info f

12631268 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

1264− n

1269+ acc n

12651270 nfc

12661271 (map (expandParams dec ps ns []) params)

12671272 (expandParams dec ps ns [] ty)

src/Idris/AbsSyntaxTree.hs+9−8

@@ -234,7 +234,7 @@ data IState = IState {

234234 brace_stack :: [Maybe Int],

235235 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?

236236 idris_parsedSpan :: Maybe FC,

237− hide_list :: [(Name, Maybe Accessibility)],

237+ hide_list :: Ctxt Accessibility,

238238 default_access :: Accessibility,

239239 default_total :: Bool,

240240 ibc_write :: [IBCWrite],

@@ -350,7 +350,7 @@ idrisInit = IState initContext S.empty []

350350 emptyContext emptyContext emptyContext emptyContext

351351 emptyContext

352352 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

353− [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

353+ [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Hidden False [] Nothing [] []

354354 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

355355 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []

356356 emptyContext S.empty M.empty

@@ -718,6 +718,7 @@ data PDecl' t

718718 [(Name, Docstring (Either Err t))] -- Parameter docs

719719 SyntaxInfo

720720 FC [(Name, t)] -- constraints

721+ Accessibility

721722 Name -- class

722723 FC -- precise location of class

723724 [t] -- parameters

@@ -876,10 +877,10 @@ mapPDeclFC f g (PClass doc syn fc constrs n nfc params paramDocs det body ctor c

876877 (map (mapPDeclFC f g) body)

877878 (fmap (\(n, nfc) -> (n, g nfc)) ctor)

878879 ctorDoc

879−mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn cnfc params instTy instN body) =

880+mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn acc cnfc params instTy instN body) =

880881 PInstance doc paramDocs syn (f fc)

881882 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)

882− cn (g cnfc) (map (mapPTermFC f g) params)

883+ cn acc (g cnfc) (map (mapPTermFC f g) params)

883884 (mapPTermFC f g instTy)

884885 instN

885886 (map (mapPDeclFC f g) body)

@@ -919,7 +920,7 @@ declared (PParams _ _ ds) = concatMap declared ds

919920declared (PNamespace _ _ ds) = concatMap declared ds

920921declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

921922declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)

922−declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []

923+declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []

923924declared (PDSL n _) = [n]

924925declared (PSyntax _ _) = []

925926declared (PMutual _ ds) = concatMap declared ds

@@ -939,7 +940,7 @@ tldeclared (PParams _ _ ds) = []

939940tldeclared (PMutual _ ds) = concatMap tldeclared ds

940941tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds

941942tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)

942−tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []

943+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []

943944tldeclared _ = []

944945

945946defined :: PDecl -> [Name]

@@ -955,7 +956,7 @@ defined (PParams _ _ ds) = concatMap defined ds

955956defined (PNamespace _ _ ds) = concatMap defined ds

956957defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

957958defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)

958−defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []

959+defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []

959960defined (PDSL n _) = [n]

960961defined (PSyntax _ _) = []

961962defined (PMutual _ ds) = concatMap defined ds

@@ -2110,7 +2111,7 @@ showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line

21102111showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

21112112showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)

21122113 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

2113−showDeclImp o (PInstance _ _ _ _ cs n _ _ t _ ds)

2114+showDeclImp o (PInstance _ _ _ _ cs acc n _ _ t _ ds)

21142115 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

21152116showDeclImp _ _ = text "..."

21162117-- showDeclImp (PImport o) = "import " ++ o

src/Idris/Core/Evaluate.hs+10−5

@@ -247,7 +247,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

247247 | otherwise

248248 = do (u, ntimes) <- usable spec n ntimes_in

249249 if u then

250− do let val = lookupDefAcc n (spec || atRepl) ctxt

250+ do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt

251251 case val of

252252 [(Function _ tm, _)] | sUN "assert_total" `elem` stk ->

253253 ev ntimes (n:stk) True env tm

@@ -317,7 +317,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

317317 evApply ntimes' stk top env [l',t',arg'] d'

318318 -- Treat "assert_total" specially, as long as it's defined!

319319 ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)

320− | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl) ctxt,

320+ | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl || runtime) ctxt,

321321 at == txt "assert_total" && not simpl

322322 = ev ntimes (n : stk) top env arg

323323 ev ntimes stk top env (App _ f a)

@@ -345,7 +345,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

345345 = apply ntimes stk top env f args

346346

347347 reapply ntimes stk top env f@(VP Ref n ty) args

348− = let val = lookupDefAcc n (spec || atRepl) ctxt in

348+ = let val = lookupDefAcc n (spec || atRepl || runtime) ctxt in

349349 case val of

350350 [(CaseOp ci _ _ _ _ cd, acc)] ->

351351 let (ns, tree) = getCases cd in

@@ -371,7 +371,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

371371 | otherwise

372372 = do (u, ntimes) <- usable spec n ntimes_in

373373 if u then

374− do let val = lookupDefAcc n (spec || atRepl) ctxt

374+ do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt

375375 case val of

376376 [(CaseOp ci _ _ _ _ cd, acc)]

377377 | acc == Public || sUN "assert_total" `elem` stk ->

@@ -744,11 +744,16 @@ instance Show Def where

744744-- Hidden => doesn't reduce and invisible to type checker

745745

746746data Accessibility = Public | Frozen | Hidden

747− deriving (Show, Eq)

747+ deriving (Eq, Ord)

748748{-!

749749deriving instance NFData Accessibility

750750!-}

751751

752+instance Show Accessibility where

753+ show Public = "public export"

754+ show Frozen = "export"

755+ show Hidden = "private"

756+

752757-- | The result of totality checking

753758data Totality = Total [Int] -- ^ well-founded arguments

754759 | Productive -- ^ productive

src/Idris/DeepSeq.hs+2−2

@@ -466,7 +466,7 @@ instance (NFData t) => NFData (PDecl' t) where

466466 rnf x9 `seq`

467467 rnf x10 `seq`

468468 rnf x11 `seq` rnf x12 `seq` ()

469− rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

469+ rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

470470 = rnf x1 `seq`

471471 rnf x2 `seq`

472472 rnf x3 `seq`

@@ -475,7 +475,7 @@ instance (NFData t) => NFData (PDecl' t) where

475475 rnf x6 `seq`

476476 rnf x7 `seq`

477477 rnf x8 `seq`

478− rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

478+ rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()

479479 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

480480 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

481481 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/Docs.hs+2−2

@@ -319,8 +319,8 @@ docClass n ci

319319 namedInst n@(UN _) = Just n

320320 namedInst _ = Nothing

321321

322− getDInst (PInstance _ _ _ _ _ _ _ _ t _ _) = Just t

323− getDInst _ = Nothing

322+ getDInst (PInstance _ _ _ _ _ _ _ _ _ t _ _) = Just t

323+ getDInst _ = Nothing

324324

325325 isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))

326326 = nm == n && map getTm args == map getTm args'

src/Idris/Elab/Class.hs+2−2

@@ -138,7 +138,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

138138

139139 -- TODO: probably should normalise

140140 checkDefaultSuperclassInstance :: PDecl -> Idris ()

141− checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n _ ps _ _ _)

141+ checkDefaultSuperclassInstance (PInstance _ _ _ fc cs _ n _ ps _ _ _)

142142 = do when (not $ null cs) . tclift

143143 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

144144 i <- getIState

@@ -184,7 +184,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

184184

185185 tydecl (PTy _ _ _ _ _ _ _ _) = True

186186 tydecl _ = False

187− instdecl (PInstance _ _ _ _ _ _ _ _ _ _ _) = True

187+ instdecl (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = True

188188 instdecl _ = False

189189 clause (PClauses _ _ _ _) = True

190190 clause _ = False

src/Idris/Elab/Clause.hs+6

@@ -259,6 +259,12 @@ elabClauses info' fc opts n_in cs =

259259 -- let scg = buildSCG i sc scargs

260260 -- add SCG later, when checking totality

261261 logElab 2 $ "Called names: " ++ show calls

262+ -- if the definition is public, make sure

263+ -- it only uses public names

264+ nvis <- getFromHideList n

265+ case nvis of

266+ Just Public -> mapM_ (checkVisibility fc n Public Public) calls

267+ _ -> return ()

262268 addCalls n calls

263269 addIBC (IBCCG n)

264270 _ -> return ()

src/Idris/Elab/Instance.hs+8−4

@@ -55,13 +55,14 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

5555 [(Name, Docstring (Either Err PTerm))] ->

5656 ElabWhat -> -- phase

5757 FC -> [(Name, PTerm)] -> -- constraints

58+ Accessibility ->

5859 Name -> -- the class

5960 FC -> -- precise location of class name

6061 [PTerm] -> -- class parameters (i.e. instance)

6162 PTerm -> -- full instance type

6263 Maybe Name -> -- explicit name

6364 [PDecl] -> Idris ()

64−elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

65+elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do

6566 i <- getIState

6667 (n, ci) <- case lookupCtxtName n (idris_classes i) of

6768 [c] -> return c

@@ -70,6 +71,9 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

7071 (CantResolveAlts (map fst cs))

7172 let constraint = PApp fc (PRef fc [] n) (map pexp ps)

7273 let iname = mkiname n (namespace info) ps expn

74+ putIState (i { hide_list = addDef iname acc (hide_list i) })

75+ i <- getIState

76+

7377 let emptyclass = null (class_methods ci)

7478 when (what /= EDefns) $ do

7579 nty <- elabType' True info syn doc argDocs fc [] iname NoFC t

@@ -159,10 +163,10 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

159163 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

160164 Just nm -> nm

161165

162− substInstance ips pnames (PInstance doc argDocs syn _ cs n nfc ps t expn ds)

163− = PInstance doc argDocs syn fc cs n nfc (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

166+ substInstance ips pnames (PInstance doc argDocs syn _ cs acc n nfc ps t expn ds)

167+ = PInstance doc argDocs syn fc cs acc n nfc (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

164168

165− isOverlapping i (PInstance doc argDocs syn _ _ n nfc ps t expn _)

169+ isOverlapping i (PInstance doc argDocs syn _ _ _ n nfc ps t expn _)

166170 = case lookupCtxtName n (idris_classes i) of

167171 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

168172 case lookupTy iname (tt_ctxt i) of

src/Idris/Elab/Type.hs+10−2

@@ -102,8 +102,16 @@ buildType info syn fc opts n ty' = do

102102 logElab 3 ("Implicit " ++ show n ++ " " ++ show impls)

103103 addIBC (IBCImp n)

104104

105− -- Add the names referenced to the call graph

106− addCalls n (freeNames cty)

105+ -- Add the names referenced to the call graph, and check we're not

106+ -- referring to anything less visible

107+ -- In particular, a public/export type can not refer to anything

108+ -- private, but can refer to any public/export

109+ let refs = freeNames cty

110+ nvis <- getFromHideList n

111+ case nvis of

112+ Nothing -> return ()

113+ Just acc -> mapM_ (checkVisibility fc n (max Frozen acc) acc) refs

114+ addCalls n refs

107115 addIBC (IBCCG n)

108116

109117 when (Constructor `notElem` opts) $ do

src/Idris/Elab/Utils.hs+16

@@ -314,3 +314,19 @@ mkStaticTy ns (PPi p n fc ty sc)

314314 | n `elem` ns = PPi (p { pstatic = Static }) n fc ty (mkStaticTy ns sc)

315315 | otherwise = PPi p n fc ty (mkStaticTy ns sc)

316316mkStaticTy ns t = t

317+

318+-- Check that a name has the minimum required accessibility

319+checkVisibility :: FC -> Name -> Accessibility -> Accessibility -> Name -> Idris ()

320+checkVisibility fc n minAcc acc ref

321+ = do nvis <- getFromHideList ref

322+ case nvis of

323+ Nothing -> return ()

324+ Just acc' -> if acc' > minAcc

325+ then tclift $ tfail (At fc

326+ (Msg $ show acc ++ " " ++ show n ++

327+ " can't refer to " ++

328+ show acc' ++ " " ++ show ref))

329+ else return ()

330+

331+

332+

src/Idris/ElabDecls.hs+2−2

@@ -242,9 +242,9 @@ elabDecl' what info (PClass doc s f cs n nfc ps pdocs fds ds cn cd)

242242 | what /= EDefns

243243 = do logElab 1 $ "Elaborating class " ++ show n

244244 elabClass info (s { syn_params = [] }) doc f cs n nfc ps pdocs fds ds cn cd

245−elabDecl' what info (PInstance doc argDocs s f cs n nfc ps t expn ds)

245+elabDecl' what info (PInstance doc argDocs s f cs acc n nfc ps t expn ds)

246246 = do logElab 1 $ "Elaborating instance " ++ show n

247− elabInstance info s doc argDocs what f cs n nfc ps t expn ds

247+ elabInstance info s doc argDocs what f cs acc n nfc ps t expn ds

248248elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)

249249 = do logElab 1 $ "Elaborating record " ++ show name

250250 elabRecord info what doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn

src/Idris/IBC.hs+5−3

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 131

43+ibcVersion = 132

4444

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

4646-- structures/definitions) depending on which phase we're in

@@ -1259,7 +1259,7 @@ instance (Binary t) => Binary (PDecl' t) where

12591259 put x10

12601260 put x11

12611261 put x12

1262− PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ->

1262+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ->

12631263 do putWord8 8

12641264 put x1

12651265 put x2

@@ -1272,6 +1272,7 @@ instance (Binary t) => Binary (PDecl' t) where

12721272 put x9

12731273 put x10

12741274 put x11

1275+ put x12

12751276 PDSL x1 x2 -> do putWord8 9

12761277 put x1

12771278 put x2

@@ -1386,7 +1387,8 @@ instance (Binary t) => Binary (PDecl' t) where

13861387 x9 <- get

13871388 x10 <- get

13881389 x11 <- get

1389− return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

1390+ x12 <- get

1391+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

13901392 9 -> do x1 <- get

13911393 x2 <- get

13921394 return (PDSL x1 x2)

src/Idris/ParseData.hs+2−2

@@ -48,7 +48,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

4848 let doc' = annotCode (tryFullExpr syn ist) doc

4949 paramDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

5050 | (n, d) <- paramDocs ]

51− acc <- optional accessibility

51+ acc <- accessibility

5252 opts <- dataOpts []

5353 co <- recordI

5454 return (doc', paramDocs', acc, opts ++ co))

@@ -192,7 +192,7 @@ data_ :: SyntaxInfo -> IdrisParser PDecl

192192data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

193193 (doc, argDocs) <- option noDocs docComment

194194 pushIndent

195− acc <- optional accessibility

195+ acc <- accessibility

196196 elim <- dataOpts []

197197 co <- dataI

198198 ist <- get

src/Idris/ParseHelpers.hs+17−9

@@ -612,8 +612,9 @@ notOpenBraces = do ist <- get

612612 hasNothing = any isNothing

613613

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

615−accessibility :: IdrisParser Accessibility

616−accessibility = do reserved "public";

615+accessibility' :: IdrisParser Accessibility

616+accessibility'

617+ = do reserved "public";

617618 gotexp <- optional (reserved "export")

618619 case gotexp of

619620 Just _ -> return ()

@@ -635,16 +636,23 @@ accessibility = do reserved "public";

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

636637 <?> "accessibility modifier"

637638

639+accessibility :: IdrisParser Accessibility

640+accessibility = do acc <- optional accessibility'

641+ case acc of

642+ Just a -> return a

643+ Nothing -> do ist <- get

644+ return (default_access ist)

645+

638646-- | Adds accessibility option for function

639−addAcc :: Name -> Maybe Accessibility -> IdrisParser ()

647+addAcc :: Name -> Accessibility -> IdrisParser ()

640648addAcc n a = do i <- get

641− put (i { hide_list = (n, a) : hide_list i })

649+ put (i { hide_list = addDef n a (hide_list i) })

642650

643651{- | Add accessbility option for data declarations

644652 (works for classes too - 'abstract' means the data/class is visible but members not) -}

645−accData :: Maybe Accessibility -> Name -> [Name] -> IdrisParser ()

646−accData (Just Frozen) n ns = do addAcc n (Just Frozen)

647− mapM_ (\n -> addAcc n (Just Hidden)) ns

653+accData :: Accessibility -> Name -> [Name] -> IdrisParser ()

654+accData Frozen n ns = do addAcc n Frozen

655+ mapM_ (\n -> addAcc n Hidden) ns

648656accData a n ns = do addAcc n a

649657 mapM_ (`addAcc` a) ns

650658

@@ -679,7 +687,7 @@ collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

679687collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds

680688collect (PClass doc f s cs n nfc ps pdocs fds ds cn cd : ds')

681689 = PClass doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'

682−collect (PInstance doc argDocs f s cs n nfc ps t en ds : ds')

683− = PInstance doc argDocs f s cs n nfc ps t en (collect ds) : collect ds'

690+collect (PInstance doc argDocs f s cs acc n nfc ps t en ds : ds')

691+ = PInstance doc argDocs f s cs acc n nfc ps t en (collect ds) : collect ds'

684692collect (d : ds) = d : collect ds

685693collect [] = []

src/Idris/Parser.hs+16−18

@@ -337,8 +337,8 @@ declExtension syn ns rules =

337337 (map (updateNs ns) ds)

338338 (updateRecCon ns cname)

339339 cdocs

340− updateNs ns (PInstance docs pdocs s fc cs cn fc' ps ity ni ds)

341− = PInstance docs pdocs s fc cs (updateB ns cn) fc'

340+ updateNs ns (PInstance docs pdocs s fc cs acc cn fc' ps ity ni ds)

341+ = PInstance docs pdocs s fc cs acc (updateB ns cn) fc'

342342 ps ity (fmap (updateB ns) ni)

343343 (map (updateNs ns) ds)

344344 updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)

@@ -584,7 +584,7 @@ fnDecl' syn = checkFixity $

584584 then [TotalFn]

585585 else []

586586 opts <- fnOpts initOpts

587− acc <- optional accessibility

587+ acc <- accessibility

588588 opts' <- fnOpts opts

589589 (n_in, nfc) <- fnName

590590 let n = expandNS syn n_in

@@ -698,7 +698,7 @@ postulate syn = do (doc, ext)

698698 then [TotalFn]

699699 else []

700700 opts <- fnOpts initOpts

701− acc <- optional accessibility

701+ acc <- accessibility

702702 opts' <- fnOpts opts

703703 (n_in, nfc) <- fnName

704704 let n = expandNS syn n_in

@@ -856,7 +856,7 @@ Class ::=

856856class_ :: SyntaxInfo -> IdrisParser [PDecl]

857857class_ syn = do (doc, argDocs, acc)

858858 <- try (do (doc, argDocs) <- docstring syn

859− acc <- optional accessibility

859+ acc <- accessibility

860860 classKeyword

861861 return (doc, argDocs, acc))

862862 fc <- getFC

@@ -904,7 +904,8 @@ InstanceName ::= '[' Name ']';

904904-}

905905instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

906906instance_ kwopt syn

907− = do (doc, argDocs)

907+ = do acc <- accessibility

908+ (doc, argDocs)

908909 <- try (docstring syn <* if kwopt then optional instanceKeyword

909910 else do instanceKeyword

910911 return (Just ()))

@@ -917,7 +918,7 @@ instance_ kwopt syn

917918 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)

918919 let t = bindList (PPi constraint) cs sc

919920 ds <- instanceBlock syn

920− return [PInstance doc argDocs syn fc cs' cn cnfc args t en ds]

921+ return [PInstance doc argDocs syn fc cs' acc cn cnfc args t en ds]

921922 <?> "implementation declaration"

922923 where instanceName :: IdrisParser Name

923924 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

@@ -1321,7 +1322,10 @@ directive syn = do try (lchar '%' *> reserved "lib")

13211322 return [PDirective (DHide n)]

13221323 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []

13231324 return [PDirective (DFreeze n)]

1324− <|> do try (lchar '%' *> reserved "access"); acc <- accessibility

1325+ <|> do try (lchar '%' *> reserved "access")

1326+ acc <- accessibility

1327+ ist <- get

1328+ put ist { default_access = acc }

13251329 return [PDirective (DAccess acc)]

13261330 <|> do try (lchar '%' *> reserved "default"); tot <- totality

13271331 i <- get

@@ -1769,7 +1773,7 @@ loadSource lidr f toline

17691773 clearHighlights

17701774 i <- getIState

17711775 putIState (i { default_total = def_total,

1772− hide_list = [] })

1776+ hide_list = emptyContext })

17731777 return ()

17741778 where

17751779 namespaces :: [String] -> [PDecl] -> [PDecl]

@@ -1799,15 +1803,9 @@ loadSource lidr f toline

17991803 parsedDocs ist = annotCode (tryFullExpr syn ist) docs

18001804

18011805{- | Adds names to hide list -}

1802−addHides :: [(Name, Maybe Accessibility)] -> Idris ()

1806+addHides :: Ctxt Accessibility -> Idris ()

18031807addHides xs = do i <- getIState

18041808 let defh = default_access i

1805− let (hs, as) = partition isNothing xs

1806− mapM_ doHide

1807− (map (\ (n, _) -> (n, defh)) hs ++

1808− map (\ (n, Just a) -> (n, a)) as)

1809− where isNothing (_, Nothing) = True

1810− isNothing _ = False

1811−

1812− doHide (n, a) = do setAccessibility n a

1809+ mapM_ doHide (toAlist xs)

1810+ where doHide (n, a) = do setAccessibility n a

18131811 addIBC (IBCAccess n a)

src/Idris/REPL.hs+2−2

@@ -902,8 +902,8 @@ process fn (NewDefn decls) = do

902902 fixClauses :: PDecl' t -> PDecl' t

903903 fixClauses (PClauses fc opts _ css@(clause:cs)) =

904904 PClauses fc opts (getClauseName clause) css

905− fixClauses (PInstance doc argDocs syn fc constraints cls nfc parms ty instName decls) =

906− PInstance doc argDocs syn fc constraints cls nfc parms ty instName (map fixClauses decls)

905+ fixClauses (PInstance doc argDocs syn fc constraints acc cls nfc parms ty instName decls) =

906+ PInstance doc argDocs syn fc constraints acc cls nfc parms ty instName (map fixClauses decls)

907907 fixClauses decl = decl

908908

909909process fn (Undefine names) = undefine names