e3e35a5 · Idris-dev · git.iko.soy

CHANGELOG+2−7

compare with master

unifiedsplit

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

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

11 exported but not the data constructors.

12 - 'public export' means that the entire definition is exported.

13−* Exported names can only refer to things with at least the same level of

14− visibility. That is:

15− - 'private' definitions can refer to anything

16− - 'export' definitions can refer to 'export' or 'public' definitions

17− in their types

18− - 'public export' definitions can refer only to other 'public export'

19− definitions in their types and definitions

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

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

21 directive as before.

14 directive as before.

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

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

22

17

23New in 0.10:

18New in 0.10:

24============

19============

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

92 where

93 pad = getPad {n=3} n

94

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

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

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

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

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

97 | Z = pad8' n prim__shlB8 x c

101 | Z = pad8' n prim__shlB8 x c

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

103shiftLeft : Bits n -> Bits n -> Bits n

107shiftLeft : Bits n -> Bits n -> Bits n

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

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

105

109

110+public export

106shiftRightLogical' : machineTy n -> machineTy n -> machineTy n

111shiftRightLogical' : machineTy n -> machineTy n -> machineTy n

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

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

108 | Z = prim__lshrB8 x c

113 | Z = prim__lshrB8 x c

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

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

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

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

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

117

122

123+public export

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

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

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

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

120 | Z = pad8' n prim__ashrB8 x c

126 | Z = pad8' n prim__ashrB8 x c

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

126shiftRightArithmetic : Bits n -> Bits n -> Bits n

132shiftRightArithmetic : Bits n -> Bits n -> Bits n

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

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

128

134

135+public export

129and' : machineTy n -> machineTy n -> machineTy n

136and' : machineTy n -> machineTy n -> machineTy n

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

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

131 | Z = prim__andB8 x y

138 | Z = prim__andB8 x y

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

137and : Bits n -> Bits n -> Bits n

144and : Bits n -> Bits n -> Bits n

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

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

139

146

147+public export

140or' : machineTy n -> machineTy n -> machineTy n

148or' : machineTy n -> machineTy n -> machineTy n

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

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

142 | Z = prim__orB8 x y

150 | Z = prim__orB8 x y

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

148or : Bits n -> Bits n -> Bits n

156or : Bits n -> Bits n -> Bits n

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

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

150

158

159+public export

151xor' : machineTy n -> machineTy n -> machineTy n

160xor' : machineTy n -> machineTy n -> machineTy n

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

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

153 | Z = prim__xorB8 x y

162 | Z = prim__xorB8 x y

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

159xor : Bits n -> Bits n -> Bits n

168xor : Bits n -> Bits n -> Bits n

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

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

161

170

171+public export

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

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

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

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

164 | Z = pad8 n prim__addB8 x y

174 | Z = pad8 n prim__addB8 x y

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

170plus : Bits n -> Bits n -> Bits n

180plus : Bits n -> Bits n -> Bits n

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

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

172

182

183+public export

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

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

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

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

175 | Z = pad8 n prim__subB8 x y

186 | Z = pad8 n prim__subB8 x y

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

181minus : Bits n -> Bits n -> Bits n

192minus : Bits n -> Bits n -> Bits n

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

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

183

194

195+public export

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

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

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

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

186 | Z = pad8 n prim__mulB8 x y

198 | Z = pad8 n prim__mulB8 x y

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

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

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

194

206

195partial

207partial

208+public export

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

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

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

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

198 | Z = prim__sdivB8 x y

211 | Z = prim__sdivB8 x y

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

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

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

206

219

207partial

220partial

221+public export

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

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

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

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

210 | Z = prim__udivB8 x y

224 | Z = prim__udivB8 x y

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

216udiv : Bits n -> Bits n -> Bits n

230udiv : Bits n -> Bits n -> Bits n

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

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

218

232

219−partial

233+public export partial

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

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

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

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

222 | Z = prim__sremB8 x y

236 | Z = prim__sremB8 x y

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

228srem : Bits n -> Bits n -> Bits n

242srem : Bits n -> Bits n -> Bits n

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

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

230

244

231−partial

245+public export partial

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

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

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

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

234 | Z = prim__uremB8 x y

248 | Z = prim__uremB8 x y

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

276 | S (S Z) = prim__gtB32 x y

290 | S (S Z) = prim__gtB32 x y

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

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

278

292

293+public export

279implementation Eq (Bits n) where

294implementation Eq (Bits n) where

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

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

281

296

297+public export

282implementation Ord (Bits n) where

298implementation Ord (Bits n) where

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

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

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

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

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

291 then EQ

307 then EQ

292 else GT

308 else GT

293

309

310+public export

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

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

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

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

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

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

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

307complement (MkBits x) = MkBits (complement' x)

324complement (MkBits x) = MkBits (complement' x)

308

325

309-- TODO: Prove

326-- TODO: Prove

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

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

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

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

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

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

313 | (Z, Z) = believe_me x

330 | (Z, Z) = believe_me x

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

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

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

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

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

327

344

328−%assert_total

345+public export %assert_total

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

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

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

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

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

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

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

344implementation Cast Integer (Bits n) where

361implementation Cast Integer (Bits n) where

345 cast = intToBits

362 cast = intToBits

346

363

364+public export

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

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

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

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

349 | Z = prim__zextB8_BigInt x

367 | Z = prim__zextB8_BigInt x

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

356bitsToInt (MkBits x) = bitsToInt' x

374bitsToInt (MkBits x) = bitsToInt' x

357

375

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

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

377+public export

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

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

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

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

361

380

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

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

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

399

418

400-- TODO: Prove

419-- TODO: Prove

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

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

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

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

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

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

404 | (Z, Z) = believe_me x

423 | (Z, Z) = believe_me x

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

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

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

150 , SubReport subErr

151 ]

152−total

152+total export

153finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)

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

155 = mkFinIntegerErr (TConst c) m

libs/base/Data/Mod2.idr+1

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

9data Mod2 : Nat -> Type where

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

11

12+public export

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

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

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

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

14

15

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

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

7

8

9%default total

10−%access public export

10+%access export

11

12export data MaxiphobicHeap : Type -> Type where

13 Empty : MaxiphobicHeap a

libs/contrib/Data/SortedMap.idr−1

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

235toList Empty = []

236toList (M _ t) = treeToList t

237

238−export

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

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

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

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

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

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

8%include C "sys/socket.h"

9%include C "netdb.h"

10

11−ByteLength : Type

11+public export ByteLength : Type

12ByteLength = Int

13

14interface ToCode a where

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

65

66data RecvStructPtr = RSPtr Ptr

67data RecvfromStructPtr = RFPtr Ptr

68+

68−data BufPtr = BPtr Ptr

69+export data BufPtr = BPtr Ptr

69−data SockaddrPtr = SAPtr Ptr

70+export data SockaddrPtr = SAPtr Ptr

70

71

71||| Protocol Number.

72||| Protocol Number.

72|||

73|||

libs/effects/Effect/Memory.idr+1

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

155

156data MoveDescriptor = Dst | Src

157

158+export

158move : {dst_size : Nat} ->

159move : {dst_size : Nat} ->

159 {dst_init : Nat} ->

160 {dst_init : Nat} ->

160 {src_size : Nat} ->

161 {src_size : Nat} ->

libs/effects/Effects.idr+25−1

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

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

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

9

10−%access public export

10+%access export

11-- ----------------------------------------------------------------- [ Effects ]

12||| The Effect type describes effectful computations.

13|||

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

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

16||| + The input resource.

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

18+public export

18Effect : Type

19Effect : Type

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

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

20

21

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

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

22||| description into a concrete effect.

23||| description into a concrete effect.

24+public export

23%error_reverse

25%error_reverse

24data EFFECT : Type where

26data EFFECT : Type where

25 MkEff : Type -> Effect -> EFFECT

27 MkEff : Type -> Effect -> EFFECT

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

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

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

31

33

32namespace NoResourceEffect

34namespace NoResourceEffect

35+ public export

33 sig : Effect -> Type -> Type

36 sig : Effect -> Type -> Type

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

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

35

38

36namespace NoUpdateEffect

39namespace NoUpdateEffect

40+ public export

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

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

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

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

39

43

40namespace UpdateEffect

44namespace UpdateEffect

45+ public export

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

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

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

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

43

48

44namespace DepUpdateEffect

49namespace DepUpdateEffect

50+ public export

45 sig : Effect ->

51 sig : Effect ->

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

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

47 sig e r e_in e_out = e r e_in e_out

53 sig e r e_in e_out = e r e_in e_out

48

54

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

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

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

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

57+public export

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

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

52 ||| How to handle the effect.

59 ||| How to handle the effect.

53 |||

60 |||

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

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

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

78

85

79-- --------------------------------------- [ Properties and Proof Construction ]

86-- --------------------------------------- [ Properties and Proof Construction ]

87+public export

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

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

81 SubNil : SubList [] []

89 SubNil : SubList [] []

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

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

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

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

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

89

97

90namespace Env

98namespace Env

99+ public export

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

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

92 Nil : Env m Nil

101 Nil : Env m Nil

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

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

94

103

104+public export

95data EffElem : Effect -> Type ->

105data EffElem : Effect -> Type ->

96 List EFFECT -> Type where

106 List EFFECT -> Type where

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

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

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

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

99

109

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

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

111+private

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

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

102dropEnv [] SubNil = []

113dropEnv [] SubNil = []

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

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

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

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

105

116

117+public export

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

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

107 SubList ys xs -> List a

119 SubList ys xs -> List a

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

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

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

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

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

113

125

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

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

127+private

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

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

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

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

117rebuildEnv [] SubNil env = env

130rebuildEnv [] SubNil env = env

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

123

136

124-- -------------------------------------------------- [ The Effect EDSL itself ]

137-- -------------------------------------------------- [ The Effect EDSL itself ]

125

138

139+public export

126updateResTy : (val : t) ->

140updateResTy : (val : t) ->

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

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

128 List EFFECT

142 List EFFECT

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

131

145

132infix 5 :::, :-, :=

146infix 5 :::, :-, :=

133

147

148+public export

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

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

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

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

136

151

152+public export

137(:::) : lbl -> EFFECT -> EFFECT

153(:::) : lbl -> EFFECT -> EFFECT

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

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

139

155

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

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

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

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

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

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

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

175+public export

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

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

160 -> (es : List EFFECT)

177 -> (es : List EFFECT)

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

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

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

182

199

183namespace SimpleEff

200namespace SimpleEff

184 -- Simple effects, no updates

201 -- Simple effects, no updates

202+ public export

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

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

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

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

187

205

206+ public export

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

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

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

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

190

209

191namespace TransEff

210namespace TransEff

192 -- Dependent effects, updates not dependent on result

211 -- Dependent effects, updates not dependent on result

212+ public export

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

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

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

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

195

215

216+ public export

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

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

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

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

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

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

199

220

200namespace DepEff

221namespace DepEff

201 -- Dependent effects, updates dependent on result

222 -- Dependent effects, updates dependent on result

223+ public export

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

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

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

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

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

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

205

227

228+ public export

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

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

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

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

208 EffT m x es ce = EffM m x es ce

231 EffT m x es ce = EffM m x es ce

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

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

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

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

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

273

296

297+export

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

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

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

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

276eff env (prog `EBind` c) k

300eff env (prog `EBind` c) k

libs/prelude/IO.idr+22−9

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

3import Builtins

4import Prelude.List

5

6−%access public export

6+%access export

7

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

9−export

10data PrimIO : Type -> Type where

9data PrimIO : Type -> Type where

11 Prim__IO : a -> PrimIO a

10 Prim__IO : a -> PrimIO a

12

11

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

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

14−export data World = TheWorld prim__WorldType

13+data World = TheWorld prim__WorldType

15

14

16private

15private

17world : World -> prim__WorldType

16world : World -> prim__WorldType

18world (TheWorld w) = w

17world (TheWorld w) = w

19

18

20−export WorldRes : Type -> Type

19+WorldRes : Type -> Type

21WorldRes x = x

20WorldRes x = x

22

21

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

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

24||| backend handles foreign function calls.

23||| backend handles foreign function calls.

24+public export

25record FFI where

26 constructor MkFFI

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

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

35

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

37||| it.

38−export

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

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

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

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

41

40

41+public export

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

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

44 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

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

55

56%inline

57+private

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

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

58 ForeignPrimType xs env t ->

59 ForeignPrimType xs env t ->

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

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

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

66-- explicit here.

67-- explicit here.

67

68

68%inline

69%inline

70+private

69foreign_prim : (f : FFI) ->

71foreign_prim : (f : FFI) ->

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

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

71foreign_prim f fname (FRet y) env

73foreign_prim f fname (FRet y) env

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

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

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

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

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

93

95

94−export

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

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

96prim_io_bind (Prim__IO v) k = k v

97prim_io_bind (Prim__IO v) k = k v

97

98

98unsafePerformPrimIO : PrimIO a -> a

99unsafePerformPrimIO : PrimIO a -> a

99-- compiled as primitive

100-- compiled as primitive

100

101

101−export

102prim_io_return : a -> PrimIO a

103prim_io_return x = Prim__IO x

104

105−export

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

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

107io_bind (MkIO fn) k

106io_bind (MkIO fn) k

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

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

109 (\ b => case k b of

108 (\ b => case k b of

110 MkIO fkb => fkb w))

109 MkIO fkb => fkb w))

111

110

112−export

113io_return : a -> IO' l a

111io_return : a -> IO' l a

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

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

115

113

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

143

141

144--------- The C FFI

142--------- The C FFI

145namespace FFI_C

143namespace FFI_C

144+ public export

146 data Raw : Type -> Type where

145 data Raw : Type -> Type where

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

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

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

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

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

151 %used MkRaw x

150 %used MkRaw x

152

151

153 ||| Supported C integer types

152 ||| Supported C integer types

153+ public export

154 data C_IntTypes : Type -> Type where

155 C_IntChar : C_IntTypes Char

156 C_IntNative : C_IntTypes Int

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

160 C_IntBits64 : C_IntTypes Bits64

161

162 ||| Supported C foreign types

163+ public export

163 data C_Types : Type -> Type where

164 data C_Types : Type -> Type where

164 C_Str : C_Types String

165 C_Str : C_Types String

165 C_Float : C_Types Double

166 C_Float : C_Types Double

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

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

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

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

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

174 %error_reverse

175 %error_reverse

176+ public export

175 FFI_C : FFI

177 FFI_C : FFI

176 FFI_C = MkFFI C_Types String String

178 FFI_C = MkFFI C_Types String String

177

179

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

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

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

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

180%error_reverse

182%error_reverse

183+public export

181IO : (res : Type) -> Type

184IO : (res : Type) -> Type

182IO = IO' FFI_C

185IO = IO' FFI_C

183

186

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

207

210

208-- Supported JS foreign types

211-- Supported JS foreign types

209mutual

212mutual

213+ public export

210 data JsFn : Type -> Type where

214 data JsFn : Type -> Type where

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

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

212

216

217+ public export

213 data JS_IntTypes : Type -> Type where

218 data JS_IntTypes : Type -> Type where

214 JS_IntChar : JS_IntTypes Char

219 JS_IntChar : JS_IntTypes Char

215 JS_IntNative : JS_IntTypes Int

220 JS_IntNative : JS_IntTypes Int

216

221

222+ public export

217 data JS_FnTypes : Type -> Type where

223 data JS_FnTypes : Type -> Type where

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

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

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

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

220 JS_FnBase : JS_Types t -> JS_FnTypes t

226 JS_FnBase : JS_Types t -> JS_FnTypes t

221

227

228+ public export

222 data JS_Types : Type -> Type where

229 data JS_Types : Type -> Type where

223 JS_Str : JS_Types String

230 JS_Str : JS_Types String

224 JS_Float : JS_Types Double

231 JS_Float : JS_Types Double

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

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

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

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

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

238%error_reverse

245%error_reverse

246+public export

239FFI_JS : FFI

247FFI_JS : FFI

240FFI_JS = MkFFI JS_Types String String

248FFI_JS = MkFFI JS_Types String String

241

249

242%error_reverse

250%error_reverse

251+public export

243JS_IO : Type -> Type

252JS_IO : Type -> Type

244JS_IO = IO' FFI_JS

253JS_IO = IO' FFI_JS

245

254

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

249namespace FFI_Export

258namespace FFI_Export

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

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

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

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

261+ public export

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

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

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

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

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

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

255

265

266+ public export

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

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

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

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

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

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

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

261 %used FFI_ExpType def

272 %used FFI_ExpType def

262 %used FFI_Prim prim

273 %used FFI_Prim prim

263

274

275+ public export

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

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

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

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

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

278 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

271 %used FFI_Fun a

283 %used FFI_Fun a

272 %used FFI_Ret b

284 %used FFI_Ret b

273

285

286+ public export

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

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

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

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

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

289 (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

110implementation ReflConst Bits64 where

111 toConst = B64

112

113−implicit

113+implicit export

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

115reflectConstant = toConst

116

libs/prelude/Prelude.idr+2−1

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

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

271cast_part x = TermPart x

272

273−%error_handler

273+%error_handler export

274cast_error : Err -> Maybe (List ErrorReportPart)

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

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

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

280cast_error _ = Nothing

281

282%error_handler

283+export

283num_error : Err -> Maybe (List ErrorReportPart)

284num_error : Err -> Maybe (List ErrorReportPart)

284num_error (CantResolve `(Num ~x))

285num_error (CantResolve `(Num ~x))

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

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

462 = do let l' = toFDesc l

463 r' <- irTerm vs env r

464 return (l', r')

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

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

466

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

468 toFDesc tm

src/Idris/AbsSyntax.hs+7−2

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

207 let ctxt = setAccess n a (tt_ctxt i)

208 putIState $ i { tt_ctxt = ctxt }

209

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+

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

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

211setTotality n a

216setTotality n a

212 = do i <- getIState

217 = do i <- getIState

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

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

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

1259 cn

1264 cn

1260 cd

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

1262 = PInstance doc argDocs info f

1267 = PInstance doc argDocs info f

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

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

1264− n

1269+ acc n

1265 nfc

1270 nfc

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

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

1267 (expandParams dec ps ns [] ty)

1272 (expandParams dec ps ns [] ty)

src/Idris/AbsSyntaxTree.hs+9−8

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

234 brace_stack :: [Maybe Int],

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

236 idris_parsedSpan :: Maybe FC,

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

237+ hide_list :: Ctxt Accessibility,

238 default_access :: Accessibility,

239 default_total :: Bool,

240 ibc_write :: [IBCWrite],

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

350 emptyContext emptyContext emptyContext emptyContext

351 emptyContext

352 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

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

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

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

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

356 emptyContext S.empty M.empty

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

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

719 SyntaxInfo

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

721+ Accessibility

721 Name -- class

722 Name -- class

722 FC -- precise location of class

723 FC -- precise location of class

723 [t] -- parameters

724 [t] -- parameters

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

876 (map (mapPDeclFC f g) body)

877 (map (mapPDeclFC f g) body)

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

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

878 ctorDoc

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

880 PInstance doc paramDocs syn (f fc)

881 PInstance doc paramDocs syn (f fc)

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

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

883 (mapPTermFC f g instTy)

884 (mapPTermFC f g instTy)

884 instN

885 instN

885 (map (mapPDeclFC f g) body)

886 (map (mapPDeclFC f g) body)

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

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

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

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

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

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

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

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

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

923declared (PDSL n _) = [n]

924declared (PDSL n _) = [n]

924declared (PSyntax _ _) = []

925declared (PSyntax _ _) = []

925declared (PMutual _ ds) = concatMap declared ds

926declared (PMutual _ ds) = concatMap declared ds

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

939tldeclared (PMutual _ ds) = concatMap tldeclared ds

940tldeclared (PMutual _ ds) = concatMap tldeclared ds

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

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

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

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

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

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

943tldeclared _ = []

944tldeclared _ = []

944

945

945defined :: PDecl -> [Name]

946defined :: PDecl -> [Name]

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

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

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

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

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

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

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

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

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

959defined (PDSL n _) = [n]

960defined (PDSL n _) = [n]

960defined (PSyntax _ _) = []

961defined (PSyntax _ _) = []

961defined (PMutual _ ds) = concatMap defined ds

962defined (PMutual _ ds) = concatMap defined ds

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

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

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

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

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

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

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

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

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

2115showDeclImp _ _ = text "..."

2116showDeclImp _ _ = text "..."

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

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

247 | otherwise

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

249 if u then

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

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

251 case val of

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

253 ev ntimes (n:stk) True env tm

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

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

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

319 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,

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

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

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

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

345 = apply ntimes stk top env f args

346

347 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

349 case val of

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

351 let (ns, tree) = getCases cd in

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

371 | otherwise

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

373 if u then

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

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

375 case val of

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

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

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

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

745

746data Accessibility = Public | Frozen | Hidden

747− deriving (Show, Eq)

747+ deriving (Eq, Ord)

748{-!

749deriving instance NFData Accessibility

750!-}

751

752+instance Show Accessibility where

753+ show Public = "public export"

754+ show Frozen = "export"

755+ show Hidden = "private"

756+

752-- | The result of totality checking

757-- | The result of totality checking

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

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

754 | Productive -- ^ productive

759 | Productive -- ^ productive

src/Idris/DeepSeq.hs+2−2

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

466 rnf x9 `seq`

467 rnf x10 `seq`

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

470 = rnf x1 `seq`

471 rnf x2 `seq`

472 rnf x3 `seq`

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

475 rnf x6 `seq`

476 rnf x7 `seq`

477 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` ()

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

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

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

src/Idris/Docs.hs+2−2

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

319 namedInst n@(UN _) = Just n

320 namedInst _ = Nothing

321

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

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

323− getDInst _ = Nothing

323+ getDInst _ = Nothing

324

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

326 = 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

138

139 -- TODO: probably should normalise

140 checkDefaultSuperclassInstance :: PDecl -> Idris ()

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

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

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

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

144 i <- getIState

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

184

185 tydecl (PTy _ _ _ _ _ _ _ _) = True

186 tydecl _ = False

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

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

188 instdecl _ = False

189 clause (PClauses _ _ _ _) = True

190 clause _ = False

src/Idris/Elab/Clause.hs+6

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

259 -- let scg = buildSCG i sc scargs

260 -- add SCG later, when checking totality

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

262 addCalls n calls

268 addCalls n calls

263 addIBC (IBCCG n)

269 addIBC (IBCCG n)

264 _ -> return ()

270 _ -> return ()

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

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

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

56 ElabWhat -> -- phase

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

58+ Accessibility ->

58 Name -> -- the class

59 Name -> -- the class

59 FC -> -- precise location of class name

60 FC -> -- precise location of class name

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

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

61 PTerm -> -- full instance type

62 PTerm -> -- full instance type

62 Maybe Name -> -- explicit name

63 Maybe Name -> -- explicit name

63 [PDecl] -> Idris ()

64 [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

65 i <- getIState

66 i <- getIState

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

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

67 [c] -> return c

68 [c] -> return c

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

70 (CantResolveAlts (map fst cs))

71 (CantResolveAlts (map fst cs))

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

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

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

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

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

75+ i <- getIState

76+

73 let emptyclass = null (class_methods ci)

77 let emptyclass = null (class_methods ci)

74 when (what /= EDefns) $ do

78 when (what /= EDefns) $ do

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

79 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

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

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

160 Just nm -> nm

164 Just nm -> nm

161

165

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

166+ substInstance ips pnames (PInstance doc argDocs syn _ cs acc 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

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

164

168

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

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

166 = case lookupCtxtName n (idris_classes i) of

170 = case lookupCtxtName n (idris_classes i) of

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

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

168 case lookupTy iname (tt_ctxt i) of

172 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

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

103 addIBC (IBCImp n)

104

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

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

106− addCalls n (freeNames cty)

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

107 addIBC (IBCCG n)

115 addIBC (IBCCG n)

108

116

109 when (Constructor `notElem` opts) $ do

117 when (Constructor `notElem` opts) $ do

src/Idris/Elab/Utils.hs+16

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

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

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

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

242 | what /= EDefns

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

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

246 = 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

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

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

250 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

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 131

43+ibcVersion = 132

44

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

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

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

1259 put x10

1260 put x11

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

1263 do putWord8 8

1264 put x1

1265 put x2

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

1272 put x9

1273 put x10

1274 put x11

1275+ put x12

1275 PDSL x1 x2 -> do putWord8 9

1276 PDSL x1 x2 -> do putWord8 9

1276 put x1

1277 put x1

1277 put x2

1278 put x2

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

1386 x9 <- get

1387 x9 <- get

1387 x10 <- get

1388 x10 <- get

1388 x11 <- get

1389 x11 <- get

1390+ x12 <- get

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

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

1390 9 -> do x1 <- get

1392 9 -> do x1 <- get

1391 x2 <- get

1393 x2 <- get

1392 return (PDSL x1 x2)

1394 return (PDSL x1 x2)

src/Idris/ParseData.hs+2−2

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

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

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

50 | (n, d) <- paramDocs ]

51− acc <- optional accessibility

51+ acc <- accessibility

52 opts <- dataOpts []

53 co <- recordI

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

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

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

193 (doc, argDocs) <- option noDocs docComment

194 pushIndent

195− acc <- optional accessibility

195+ acc <- accessibility

196 elim <- dataOpts []

197 co <- dataI

198 ist <- get

src/Idris/ParseHelpers.hs+17−9

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

612 hasNothing = any isNothing

613

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

615−accessibility :: IdrisParser Accessibility

615+accessibility' :: IdrisParser Accessibility

616+accessibility'

616−accessibility = do reserved "public";

617+ = do reserved "public";

617 gotexp <- optional (reserved "export")

618 gotexp <- optional (reserved "export")

618 case gotexp of

619 case gotexp of

619 Just _ -> return ()

620 Just _ -> return ()

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

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

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

636 <?> "accessibility modifier"

637 <?> "accessibility modifier"

637

638

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+

638-- | Adds accessibility option for function

646-- | Adds accessibility option for function

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

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

640addAcc n a = do i <- get

648addAcc 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) })

642

650

643{- | Add accessbility option for data declarations

651{- | Add accessbility option for data declarations

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

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

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

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

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

654+accData Frozen n ns = do addAcc n Frozen

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

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

648accData a n ns = do addAcc n a

656accData a n ns = do addAcc n a

649 mapM_ (`addAcc` a) ns

657 mapM_ (`addAcc` a) ns

650

658

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

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

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

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

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

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

689 = 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')

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

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

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

684collect (d : ds) = d : collect ds

692collect (d : ds) = d : collect ds

685collect [] = []

693collect [] = []

src/Idris/Parser.hs+16−18

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

337 (map (updateNs ns) ds)

338 (updateRecCon ns cname)

339 cdocs

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

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

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

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

342 ps ity (fmap (updateB ns) ni)

343 (map (updateNs ns) ds)

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

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

584 then [TotalFn]

585 else []

586 opts <- fnOpts initOpts

587− acc <- optional accessibility

587+ acc <- accessibility

588 opts' <- fnOpts opts

589 (n_in, nfc) <- fnName

590 let n = expandNS syn n_in

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

698 then [TotalFn]

699 else []

700 opts <- fnOpts initOpts

701− acc <- optional accessibility

701+ acc <- accessibility

702 opts' <- fnOpts opts

703 (n_in, nfc) <- fnName

704 let n = expandNS syn n_in

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

856class_ :: SyntaxInfo -> IdrisParser [PDecl]

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

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

859− acc <- optional accessibility

859+ acc <- accessibility

860 classKeyword

861 return (doc, argDocs, acc))

862 fc <- getFC

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

904-}

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

906instance_ kwopt syn

907+ = do acc <- accessibility

907− = do (doc, argDocs)

908+ (doc, argDocs)

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

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

909 else do instanceKeyword

910 else do instanceKeyword

910 return (Just ()))

911 return (Just ()))

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

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

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

918 let t = bindList (PPi constraint) cs sc

919 let t = bindList (PPi constraint) cs sc

919 ds <- instanceBlock syn

920 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]

921 <?> "implementation declaration"

922 <?> "implementation declaration"

922 where instanceName :: IdrisParser Name

923 where instanceName :: IdrisParser Name

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

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

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

1321 return [PDirective (DHide n)]

1322 return [PDirective (DHide n)]

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

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

1323 return [PDirective (DFreeze n)]

1324 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 }

1325 return [PDirective (DAccess acc)]

1329 return [PDirective (DAccess acc)]

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

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

1327 i <- get

1331 i <- get

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

1769 clearHighlights

1773 clearHighlights

1770 i <- getIState

1774 i <- getIState

1771 putIState (i { default_total = def_total,

1775 putIState (i { default_total = def_total,

1772− hide_list = [] })

1776+ hide_list = emptyContext })

1773 return ()

1777 return ()

1774 where

1778 where

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

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

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

1799 parsedDocs ist = annotCode (tryFullExpr syn ist) docs

1803 parsedDocs ist = annotCode (tryFullExpr syn ist) docs

1800

1804

1801{- | Adds names to hide list -}

1805{- | Adds names to hide list -}

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

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

1803addHides xs = do i <- getIState

1807addHides xs = do i <- getIState

1804 let defh = default_access i

1808 let defh = default_access i

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

1806− mapM_ doHide

1809+ mapM_ doHide (toAlist xs)

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

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

1813 addIBC (IBCAccess n a)

1811 addIBC (IBCAccess n a)

src/Idris/REPL.hs+2−2

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

902 fixClauses :: PDecl' t -> PDecl' t

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

904 PClauses fc opts (getClauseName clause) css

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

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

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

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

907 fixClauses decl = decl

908

909process fn (Undefine names) = undefine names