228f56c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

findCalls should find constructors too

Need to detect non-exported constructor names

commit228f56cc6351a18b0c641bf4b7d8bd886826d1d3 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 29 Jan 2016, 22:31 (11 years ago) parent5259edc

6 files changed+96−5

compare with master

unifiedsplit

libs/contrib/System/Concurrency/Process.idr+8 libs/effects/Effect/Memory.idr+5 libs/prelude/Language/Reflection/Elab.idr+50 libs/prelude/Prelude/File.idr+29−1 src/Idris/Core/CaseTree.hs+2−2 src/Idris/ParseHelpers.hs+2−2

libs/contrib/System/Concurrency/Process.idr+8

@@ -30,24 +30,29 @@ run : Process msg x -> IO x

3030run (Lift prog) = prog

3131

3232||| Get current process ID

33+export

3334myID : Process msg (ProcID msg)

3435myID = Lift (return (MkPID prim__vm))

3536

3637||| Send a message to another process

3738||| Returns whether the send was unsuccessful.

39+export

3840send : ProcID msg -> msg -> Process msg Bool

3941send (MkPID p) m = Lift (do x <- sendToThread p (prim__vm, m)

4042 return (x == 1))

4143

4244||| Return whether a message is waiting in the queue

45+export

4346msgWaiting : Process msg Bool

4447msgWaiting = Lift checkMsgs

4548

4649||| Return whether a message is waiting in the queue from a specific sender

50+export

4751msgWaitingFrom : ProcID msg -> Process msg Bool

4852msgWaitingFrom (MkPID p) = Lift (checkMsgsFrom p)

4953

5054||| Receive a message - blocks if there is no message waiting

55+export

5156recv : Process msg msg

5257recv {msg} = do (senderid, m) <- Lift get

5358 return m

@@ -55,6 +60,7 @@ recv {msg} = do (senderid, m) <- Lift get

5560 get = getMsg

5661

5762||| Receive a message from specific sender - blocks if there is no message waiting

63+export

5864recvFrom : ProcID msg -> Process msg msg

5965recvFrom (MkPID p) {msg} = do (senderid, m) <- Lift get

6066 return m

@@ -62,6 +68,7 @@ recvFrom (MkPID p) {msg} = do (senderid, m) <- Lift get

6268 get = getMsgFrom p

6369

6470||| receive a message, and return with the sender's process ID.

71+export

6572recvWithSender : Process msg (ProcID msg, msg)

6673recvWithSender {msg}

6774 = do (senderid, m) <- Lift get

@@ -69,6 +76,7 @@ recvWithSender {msg}

6976 where get : IO (Ptr, msg)

7077 get = getMsg

7178

79+export

7280create : Process msg () -> Process msg (ProcID msg)

7381create (Lift p) = do ptr <- Lift (fork p)

7482 return (MkPID ptr)

libs/effects/Effect/Memory.idr+5

@@ -102,10 +102,12 @@ implementation Handler RawMemory (IOExcept String) where

102102RAW_MEMORY : Type -> EFFECT

103103RAW_MEMORY t = MkEff t RawMemory

104104

105+export

105106allocate : (n : Nat) ->

106107 Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])

107108allocate size = call $ Allocate size

108109

110+export

109111initialize : {i : Nat} ->

110112 {n : Nat} ->

111113 Bits8 ->

@@ -115,9 +117,11 @@ initialize : {i : Nat} ->

115117 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])

116118initialize c size prf = call $ Initialize c size prf

117119

120+export

118121free : Eff () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])

119122free = call Free

120123

124+export

121125peek : {i : Nat} ->

122126 (offset : Nat) ->

123127 (size : Nat) ->

@@ -125,6 +129,7 @@ peek : {i : Nat} ->

125129 { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)

126130peek offset size prf = call $ Peek offset size prf

127131

132+export

128133poke : {n : Nat} ->

129134 {i : Nat} ->

130135 (offset : Nat) ->

libs/prelude/Language/Reflection/Elab.idr+50

@@ -188,31 +188,38 @@ namespace Tactics

188188 x >>= f = Prim__BindElab x f

189189

190190 ||| Halt elaboration with an error

191+ export

191192 fail : List ErrorReportPart -> Elab a

192193 fail err = Prim__Fail err

193194

194195 ||| Look up the lexical binding at the focused hole. Fails if no holes are present.

196+ export

195197 getEnv : Elab (List (TTName, Binder TT))

196198 getEnv = Prim__Env

197199

198200 ||| Get the name and type of the focused hole. Fails if not holes are present.

201+ export

199202 getGoal : Elab (TTName, TT)

200203 getGoal = Prim__Goal

201204

202205 ||| Get the hole queue, in order.

206+ export

203207 getHoles : Elab (List TTName)

204208 getHoles = Prim__Holes

205209

206210 ||| If the current hole contains a guess, return it. Otherwise, fail.

211+ export

207212 getGuess : Elab TT

208213 getGuess = Prim__Guess

209214

210215 ||| Look up the types of every overloading of a name.

216+ export

211217 lookupTy : TTName -> Elab (List (TTName, NameType, TT))

212218 lookupTy n = Prim__LookupTy n

213219

214220 ||| Get the type of a fully-qualified name. Fail if it doesn not

215221 ||| resolve uniquely.

222+ export

216223 lookupTyExact : TTName -> Elab (TTName, NameType, TT)

217224 lookupTyExact n = case !(lookupTy n) of

218225 [res] => return res

@@ -221,12 +228,14 @@ namespace Tactics

221228

222229 ||| Find the reflected representation of all datatypes whose names

223230 ||| are overloadings of some name.

231+ export

224232 lookupDatatype : TTName -> Elab (List Datatype)

225233 lookupDatatype n = Prim__LookupDatatype n

226234

227235 ||| Find the reflected representation of a datatype, given its

228236 ||| fully-qualified name. Fail if the name does not uniquely resolve

229237 ||| to a datatype.

238+ export

230239 lookupDatatypeExact : TTName -> Elab Datatype

231240 lookupDatatypeExact n = case !(lookupDatatype n) of

232241 [res] => return res

@@ -235,12 +244,14 @@ namespace Tactics

235244

236245 ||| Find the reflected function definition of all functions whose names

237246 ||| are overloadings of some name.

247+ export

238248 lookupFunDefn : TTName -> Elab (List (FunDefn TT))

239249 lookupFunDefn n = Prim__LookupFunDefn n

240250

241251 ||| Find the reflected function definition of a function, given its

242252 ||| fully-qualified name. Fail if the name does not uniquely resolve

243253 ||| to a function.

254+ export

244255 lookupFunDefnExact : TTName -> Elab (FunDefn TT)

245256 lookupFunDefnExact n = case !(lookupFunDefn n) of

246257 [res] => return res

@@ -248,11 +259,13 @@ namespace Tactics

248259 xs => fail [TextPart "More than one function named", NamePart n]

249260

250261 ||| Get the argument specification for each overloading of a name.

262+ export

251263 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))

252264 lookupArgs n = Prim__LookupArgs n

253265

254266 ||| Get the argument specification for a name. Fail if the name does

255267 ||| not uniquely resolve.

268+ export

256269 lookupArgsExact : TTName -> Elab (TTName, List FunArg, Raw)

257270 lookupArgsExact n = case !(lookupArgs n) of

258271 [res] => return res

@@ -263,6 +276,7 @@ namespace Tactics

263276 |||

264277 ||| @ env the environment within which to check the type

265278 ||| @ tm the term to check

279+ export

266280 check : (env : List (TTName, Binder TT)) -> (tm : Raw) -> Elab (TT, TT)

267281 check env tm = Prim__Check env tm

268282

@@ -271,15 +285,18 @@ namespace Tactics

271285 |||

272286 ||| **NB**: the generated name is unique _for this run of the

273287 ||| elaborator_. Do not assume that they are globally unique.

288+ export

274289 gensym : (hint : String) -> Elab TTName

275290 gensym hint = Prim__Gensym hint

276291

277292 ||| Substitute a guess into a hole.

293+ export

278294 solve : Elab ()

279295 solve = Prim__Solve

280296

281297 ||| Place a term into a hole, unifying its type. Fails if the focus

282298 ||| is not a hole.

299+ export

283300 fill : Raw -> Elab ()

284301 fill tm = Prim__Fill tm

285302

@@ -297,6 +314,7 @@ namespace Tactics

297314 ||| @ argSpec instructions for finding the arguments to the term,

298315 ||| where the Boolean states whether or not to attempt to solve

299316 ||| the argument by unification.

317+ export

300318 apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)

301319 apply tm argSpec = map snd <$> Prim__Apply tm argSpec

302320

@@ -315,6 +333,7 @@ namespace Tactics

315333 ||| where the Boolean states whether or not to attempt to solve

316334 ||| the argument by matching.

317335

336+ export

318337 matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)

319338 matchApply tm argSpec = map snd <$> Prim__Apply tm argSpec

320339

@@ -322,11 +341,13 @@ namespace Tactics

322341 ||| exist.

323342 |||

324343 ||| @ hole the hole to focus on

344+ export

325345 focus : (hole : TTName) -> Elab ()

326346 focus hole = Prim__Focus hole

327347

328348 ||| Send the currently-focused hole to the end of the hole queue and

329349 ||| focus on the next hole.

350+ export

330351 unfocus : TTName -> Elab ()

331352 unfocus hole = Prim__Unfocus hole

332353

@@ -338,6 +359,7 @@ namespace Tactics

338359 ||| binding, or else the scopes of the generated terms won't make

339360 ||| sense. This tactic creates a new hole of the proper form, and

340361 ||| points the old hole at it.

362+ export

341363 attack : Elab ()

342364 attack = Prim__Attack

343365

@@ -346,6 +368,7 @@ namespace Tactics

346368 ||| The new hole will be focused, and the previously-focused hole

347369 ||| will be immediately after it in the hole queue. Because this

348370 ||| tactic introduces a new binding, you may need to `attack` first.

371+ export

349372 claim : TTName -> Raw -> Elab ()

350373 claim n ty = Prim__Claim n ty

351374

@@ -354,6 +377,7 @@ namespace Tactics

354377 ||| `attack`).

355378 |||

356379 ||| @ n the name to use for the argument

380+ export

357381 intro : (n : TTName) -> Elab ()

358382 intro n = Prim__Intro (Just n)

359383

@@ -363,6 +387,7 @@ namespace Tactics

363387 |||

364388 ||| Requires that the hole be immediately under its binder (use

365389 ||| `attack` if it might not be).

390+ export

366391 intro' : Elab ()

367392 intro' = Prim__Intro Nothing

368393

@@ -371,10 +396,12 @@ namespace Tactics

371396 |||

372397 ||| Requires that the hole be immediately under its binder (use

373398 ||| `attack` if it might not be).

399+ export

374400 forall : TTName -> Raw -> Elab ()

375401 forall n ty = Prim__Forall n ty

376402

377403 ||| Convert a hole into a pattern variable.

404+ export

378405 patvar : TTName -> Elab ()

379406 patvar n = Prim__PatVar n

380407

@@ -382,6 +409,7 @@ namespace Tactics

382409 |||

383410 ||| Requires that the hole be immediately under its binder (use

384411 ||| `attack` if it might not be).

412+ export

385413 patbind : TTName -> Elab ()

386414 patbind n = Prim__PatBind n

387415

@@ -393,10 +421,12 @@ namespace Tactics

393421 ||| @ n the name to let bind

394422 ||| @ ty the type of the term to be let-bound

395423 ||| @ tm the term to be bound

424+ export

396425 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()

397426 letbind n ty tm = Prim__LetBind n ty tm

398427

399428 ||| Normalise the goal.

429+ export

400430 compute : Elab ()

401431 compute = Prim__Compute

402432

@@ -404,12 +434,14 @@ namespace Tactics

404434 |||

405435 ||| @ env the environment in which to compute (get one of these from `getEnv`)

406436 ||| @ term the term to normalise

437+ export

407438 normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT

408439 normalise env term = Prim__Normalise env term

409440

410441 ||| Reduce a closed term to weak-head normal form

411442 |||

412443 ||| @ term the term to reduce

444+ export

413445 whnf : (term : TT) -> Elab TT

414446 whnf term = Prim__Whnf term

415447

@@ -419,6 +451,7 @@ namespace Tactics

419451 ||| @ env a lexical environment to compare the terms in (see `getEnv`)

420452 ||| @ term1 the first term to convert

421453 ||| @ term2 the second term to convert

454+ export

422455 convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab ()

423456 convertsInEnv env term1 term2 = Prim__Converts env term1 term2

424457

@@ -426,14 +459,17 @@ namespace Tactics

426459 |||

427460 ||| @ term1 the first term to convert

428461 ||| @ term2 the second term to convert

462+ export

429463 converts : (term1, term2 : TT) -> Elab ()

430464 converts term1 term2 = convertsInEnv !getEnv term1 term2

431465

432466 ||| Find the source context for the elaboration script

467+ export

433468 getSourceLocation : Elab SourceLocation

434469 getSourceLocation = Prim__SourceLocation

435470

436471 ||| Attempt to solve the current goal with the source code location

472+ export

437473 sourceLocation : Elab ()

438474 sourceLocation = do loc <- getSourceLocation

439475 fill (quote loc)

@@ -444,6 +480,7 @@ namespace Tactics

444480 |||

445481 ||| The namespace is represented as a reverse-order list of strings,

446482 ||| just as in the representation of names.

483+ export

447484 currentNamespace : Elab (List String)

448485 currentNamespace = Prim__Namespace

449486

@@ -457,16 +494,19 @@ namespace Tactics

457494 ||| Because this tactic internally introduces a `let` binding, it

458495 ||| requires that the hole be immediately under its binder (use

459496 ||| `attack` if it might not be).

497+ export

460498 rewriteWith : Raw -> Elab ()

461499 rewriteWith rule = Prim__Rewrite rule

462500

463501 ||| Add a type declaration to the global context.

502+ export

464503 declareType : TyDecl -> Elab ()

465504 declareType decl = Prim__DeclareType decl

466505

467506 ||| Define a function in the global context. The function must have

468507 ||| already been declared, either in ordinary Idris code or using

469508 ||| `declareType`.

509+ export

470510 defineFunction : FunDefn Raw -> Elab ()

471511 defineFunction defun = Prim__DefineFunction defun

472512

@@ -474,12 +514,14 @@ namespace Tactics

474514 |||

475515 ||| @ ifaceName the name of the interface for which an implementation is being registered

476516 ||| @ instName the name of the definition to use in implementation search

517+ export

477518 addInstance : (ifaceName, instName : TTName) -> Elab ()

478519 addInstance ifaceName instName = Prim__AddInstance ifaceName instName

479520

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

481522 |||

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

524+ export

483525 isTCName : (name : TTName) -> Elab Bool

484526 isTCName name = Prim__IsTCName name

485527

@@ -487,10 +529,12 @@ namespace Tactics

487529 |||

488530 ||| @ fn the name of the definition being elaborated (to prevent Idris

489531 ||| from looping)

532+ export

490533 resolveTC : (fn : TTName) -> Elab ()

491534 resolveTC fn = Prim__ResolveTC fn

492535

493536 ||| Use Idris's internal proof search.

537+ export

494538 search : Elab ()

495539 search = Prim__Search 100 []

496540

@@ -498,6 +542,7 @@ namespace Tactics

498542 |||

499543 ||| @ depth the search depth

500544 ||| @ hints additional names to try

545+ export

501546 search' : (depth : Int) -> (hints : List TTName) -> Elab ()

502547 search' depth hints = Prim__Search depth hints

503548

@@ -507,6 +552,7 @@ namespace Tactics

507552 ||| if the string is not a valid operator.

508553 |||

509554 ||| @ operator the operator string to look up

555+ export

510556 operatorFixity : (operator : String) -> Elab Fixity

511557 operatorFixity operator = Prim__Fixity operator

512558

@@ -514,6 +560,7 @@ namespace Tactics

514560 |||

515561 ||| This is intended for elaboration script developers, not for

516562 ||| end-users. Use `fail` for final scripts.

563+ export

517564 debug : Elab a

518565 debug = Prim__Debug []

519566

@@ -524,18 +571,21 @@ namespace Tactics

524571 ||| end-users. Use `fail` for final scripts.

525572 |||

526573 ||| @ msg the message to display

574+ export

527575 debugMessage : (msg : List ErrorReportPart) -> Elab a

528576 debugMessage msg = Prim__Debug msg

529577

530578 ||| Create a new top-level metavariable to solve the current hole.

531579 |||

532580 ||| @ name the name for the top-level variable

581+ export

533582 metavar : (name : TTName) -> Elab ()

534583 metavar name = Prim__Metavar name

535584

536585 ||| Recursively invoke the reflected elaborator with some goal.

537586 |||

538587 ||| The result is the final term and its type.

588+ export

539589 runElab : Raw -> Elab () -> Elab (TT, TT)

540590 runElab goal script = Prim__RecursiveElab goal script

541591

libs/prelude/Prelude/File.idr+29−1

@@ -49,25 +49,31 @@ Show FileError where

4949 show (GenericFileError errno) = strError errno

5050

5151||| Standard input

52+export

5253stdin : File

5354stdin = FHandle prim__stdin

5455

5556||| Standard output

57+export

5658stdout : File

5759stdout = FHandle prim__stdout

5860

5961||| Standard output

62+export

6063stderr : File

6164stderr = FHandle prim__stderr

6265

66+private

6367do_ferror : Ptr -> IO Int

6468do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h

6569

70+export

6671ferror : File -> IO Bool

6772ferror (FHandle h) = do err <- do_ferror h

6873 return (not (err == 0))

6974

7075||| Call the RTS's file opening function

76+private

7177do_fopen : String -> String -> IO Ptr

7278do_fopen f m

7379 = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m

@@ -75,6 +81,7 @@ do_fopen f m

7581||| Open a file

7682||| @ f the filename

7783||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)

84+export

7885fopen : (f : String) -> (m : String) -> IO (Either FileError File)

7986fopen f m = do h <- do_fopen f m

8087 if !(nullPtr h)

@@ -83,6 +90,7 @@ fopen f m = do h <- do_fopen f m

8390 else return (Right (FHandle h))

8491

8592||| Check whether a file handle is actually a null pointer

93+export

8694validFile : File -> IO Bool

8795validFile (FHandle h) = do x <- nullPtr h

8896 return (not x)

@@ -93,33 +101,41 @@ data Mode = Read | Write | ReadWrite

93101||| Open a file

94102||| @ f the filename

95103||| @ m the mode; either Read, Write, or ReadWrite

104+export

96105openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)

97106openFile f m = fopen f (modeStr m) where

98107 modeStr Read = "r"

99108 modeStr Write = "w"

100109 modeStr ReadWrite = "r+"

101110

111+private

102112do_fclose : Ptr -> IO ()

103113do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h

104114

115+export

105116closeFile : File -> IO ()

106117closeFile (FHandle h) = do_fclose h

107118

119+private

108120do_fread : Ptr -> IO' l String

109121do_fread h = prim_fread h

110122

123+export

111124fgetc : File -> IO (Either FileError Char)

112125fgetc (FHandle h) = do let c = cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h)

113126 if !(ferror (FHandle h))

114127 then return (Left FileReadError)

115128 else return (Right c)

116129

130+export

117131fflush : File -> IO ()

118132fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h

119133

134+private

120135do_popen : String -> String -> IO Ptr

121136do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m

122137

138+export

123139popen : String -> Mode -> IO (Either FileError File)

124140popen f m = do ptr <- do_popen f (modeStr m)

125141 if !(nullPtr ptr)

@@ -131,12 +147,14 @@ popen f m = do ptr <- do_popen f (modeStr m)

131147 modeStr Write = "w"

132148 modeStr ReadWrite = "r+"

133149

150+export

134151pclose : File -> IO ()

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

136153

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

138155-- prim__vm h

139156

157+export

140158fread : File -> IO (Either FileError String)

141159fread (FHandle h) = do str <- do_fread h

142160 if !(ferror (FHandle h))

@@ -145,11 +163,13 @@ fread (FHandle h) = do str <- do_fread h

145163

146164||| Read a line from a file

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

166+export

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

149168fGetLine = fread

150169

151170%deprecate fread "Use fGetLine instead"

152171

172+private

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

154174do_fwrite h s = do res <- prim_fwrite h s

155175 if (res /= 0)

@@ -160,41 +180,48 @@ do_fwrite h s = do res <- prim_fwrite h s

160180 return (Left err)

161181 else return (Right ())

162182

183+export

163184fwrite : File -> String -> IO (Either FileError ())

164185fwrite (FHandle h) s = do_fwrite h s

165186

166187||| Write a line to a file

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

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

190+export

169191fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())

170192fPutStr (FHandle h) s = do_fwrite h s

171193

194+export

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

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

174197

175198%deprecate fwrite "Use fPutStr instead"

176199

200+private

177201do_feof : Ptr -> IO Int

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

179203

180204||| Check if a file handle has reached the end

205+export

181206fEOF : File -> IO Bool

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

183208 return (not (eof == 0))

184209

185210||| Check if a file handle has reached the end

211+export

186212feof : File -> IO Bool

187213feof = fEOF

188214

189215%deprecate feof "Use fEOF instead"

190216

217+export

191218fpoll : File -> IO Bool

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

193220 return (p > 0)

194221

195222||| Read the contents of a file into a string

196223partial -- might be reading something infinitely long like /dev/null ...

197−covering

224+covering export

198225readFile : String -> IO (Either FileError String)

199226readFile fn = do Right h <- openFile fn Read

200227 | Left err => return (Left err)

@@ -212,6 +239,7 @@ readFile fn = do Right h <- openFile fn Read

212239 else return (Right contents)

213240

214241||| Write a string to a file

242+export

215243writeFile : (filepath : String) -> (contents : String) ->

216244 IO (Either FileError ())

217245writeFile fn contents = do

src/Idris/Core/CaseTree.hs+2−2

@@ -152,10 +152,10 @@ findCalls sc topargs = nub $ nu' topargs sc where

152152 nua ps (SucCase _ sc) = nu' ps sc

153153 nua ps (DefaultCase sc) = nu' ps sc

154154

155− nut ps (P Ref n _) | n `elem` ps = []

155+ nut ps (P _ n _) | n `elem` ps = []

156156 | otherwise = [(n, [])] -- tmp

157157 nut ps fn@(App _ f a)

158− | (P Ref n _, args) <- unApply fn

158+ | (P _ n _, args) <- unApply fn

159159 = if n `elem` ps then nut ps f ++ nut ps a

160160 else [(n, map argNames args)] ++ concatMap (nut ps) args

161161 | (P (TCon _ _) n _, _) <- unApply fn = []

src/Idris/ParseHelpers.hs+2−2

@@ -659,8 +659,8 @@ addAcc n a = do i <- get

659659{- | Add accessbility option for data declarations

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

661661accData :: Accessibility -> Name -> [Name] -> IdrisParser ()

662−accData Frozen n ns = do addAcc n Frozen

663− mapM_ (\n -> addAcc n Hidden) ns

662+accData Frozen n ns = do addAcc n Public -- so that it can be used in public definitions

663+ mapM_ (\n -> addAcc n Hidden) ns -- so that they are invisible

664664accData a n ns = do addAcc n a

665665 mapM_ (`addAcc` a) ns

666666