git.iko.soy/Idris-dev
on master help sign in
findCalls should find constructors too
228f56cEdwin Brady
libs/contrib/System/Concurrency/Process.idr+8
compare with master
unifiedsplit
@@ -30,24 +30,29 @@ run : Process msg x -> IO x
30run (Lift prog) = prog
30run (Lift prog) = prog
31
31
32||| Get current process ID
32||| Get current process ID
33+export
33myID : Process msg (ProcID msg)
34myID : Process msg (ProcID msg)
34myID = Lift (return (MkPID prim__vm))
35myID = Lift (return (MkPID prim__vm))
35
36
36||| Send a message to another process
37||| Send a message to another process
37||| Returns whether the send was unsuccessful.
38||| Returns whether the send was unsuccessful.
39+export
38send : ProcID msg -> msg -> Process msg Bool
40send : ProcID msg -> msg -> Process msg Bool
39send (MkPID p) m = Lift (do x <- sendToThread p (prim__vm, m)
41send (MkPID p) m = Lift (do x <- sendToThread p (prim__vm, m)
40 return (x == 1))
42 return (x == 1))
41
43
42||| Return whether a message is waiting in the queue
44||| Return whether a message is waiting in the queue
45+export
43msgWaiting : Process msg Bool
46msgWaiting : Process msg Bool
44msgWaiting = Lift checkMsgs
47msgWaiting = Lift checkMsgs
45
48
46||| Return whether a message is waiting in the queue from a specific sender
49||| Return whether a message is waiting in the queue from a specific sender
50+export
47msgWaitingFrom : ProcID msg -> Process msg Bool
51msgWaitingFrom : ProcID msg -> Process msg Bool
48msgWaitingFrom (MkPID p) = Lift (checkMsgsFrom p)
52msgWaitingFrom (MkPID p) = Lift (checkMsgsFrom p)
49
53
50||| Receive a message - blocks if there is no message waiting
54||| Receive a message - blocks if there is no message waiting
55+export
51recv : Process msg msg
56recv : Process msg msg
52recv {msg} = do (senderid, m) <- Lift get
57recv {msg} = do (senderid, m) <- Lift get
53 return m
58 return m
@@ -55,6 +60,7 @@ recv {msg} = do (senderid, m) <- Lift get
55 get = getMsg
60 get = getMsg
56
61
57||| Receive a message from specific sender - blocks if there is no message waiting
62||| Receive a message from specific sender - blocks if there is no message waiting
63+export
58recvFrom : ProcID msg -> Process msg msg
64recvFrom : ProcID msg -> Process msg msg
59recvFrom (MkPID p) {msg} = do (senderid, m) <- Lift get
65recvFrom (MkPID p) {msg} = do (senderid, m) <- Lift get
60 return m
66 return m
@@ -62,6 +68,7 @@ recvFrom (MkPID p) {msg} = do (senderid, m) <- Lift get
62 get = getMsgFrom p
68 get = getMsgFrom p
63
69
64||| receive a message, and return with the sender's process ID.
70||| receive a message, and return with the sender's process ID.
71+export
65recvWithSender : Process msg (ProcID msg, msg)
72recvWithSender : Process msg (ProcID msg, msg)
66recvWithSender {msg}
73recvWithSender {msg}
67 = do (senderid, m) <- Lift get
74 = do (senderid, m) <- Lift get
@@ -69,6 +76,7 @@ recvWithSender {msg}
69 where get : IO (Ptr, msg)
76 where get : IO (Ptr, msg)
70 get = getMsg
77 get = getMsg
71
78
79+export
72create : Process msg () -> Process msg (ProcID msg)
80create : Process msg () -> Process msg (ProcID msg)
73create (Lift p) = do ptr <- Lift (fork p)
81create (Lift p) = do ptr <- Lift (fork p)
74 return (MkPID ptr)
82 return (MkPID ptr)
libs/effects/Effect/Memory.idr+5
@@ -102,10 +102,12 @@ implementation Handler RawMemory (IOExcept String) where
102RAW_MEMORY : Type -> EFFECT
102RAW_MEMORY : Type -> EFFECT
103RAW_MEMORY t = MkEff t RawMemory
103RAW_MEMORY t = MkEff t RawMemory
104
104
105+export
105allocate : (n : Nat) ->
106allocate : (n : Nat) ->
106 Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
107 Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
107allocate size = call $ Allocate size
108allocate size = call $ Allocate size
108
109
110+export
109initialize : {i : Nat} ->
111initialize : {i : Nat} ->
110 {n : Nat} ->
112 {n : Nat} ->
111 Bits8 ->
113 Bits8 ->
@@ -115,9 +117,11 @@ initialize : {i : Nat} ->
115 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
117 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
116initialize c size prf = call $ Initialize c size prf
118initialize c size prf = call $ Initialize c size prf
117
119
120+export
118free : Eff () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])
121free : Eff () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])
119free = call Free
122free = call Free
120
123
124+export
121peek : {i : Nat} ->
125peek : {i : Nat} ->
122 (offset : Nat) ->
126 (offset : Nat) ->
123 (size : Nat) ->
127 (size : Nat) ->
@@ -125,6 +129,7 @@ peek : {i : Nat} ->
125 { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
129 { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
126peek offset size prf = call $ Peek offset size prf
130peek offset size prf = call $ Peek offset size prf
127
131
132+export
128poke : {n : Nat} ->
133poke : {n : Nat} ->
129 {i : Nat} ->
134 {i : Nat} ->
130 (offset : Nat) ->
135 (offset : Nat) ->
libs/prelude/Language/Reflection/Elab.idr+50
@@ -188,31 +188,38 @@ namespace Tactics
188 x >>= f = Prim__BindElab x f
188 x >>= f = Prim__BindElab x f
189
189
190 ||| Halt elaboration with an error
190 ||| Halt elaboration with an error
191+ export
191 fail : List ErrorReportPart -> Elab a
192 fail : List ErrorReportPart -> Elab a
192 fail err = Prim__Fail err
193 fail err = Prim__Fail err
193
194
194 ||| Look up the lexical binding at the focused hole. Fails if no holes are present.
195 ||| Look up the lexical binding at the focused hole. Fails if no holes are present.
196+ export
195 getEnv : Elab (List (TTName, Binder TT))
197 getEnv : Elab (List (TTName, Binder TT))
196 getEnv = Prim__Env
198 getEnv = Prim__Env
197
199
198 ||| Get the name and type of the focused hole. Fails if not holes are present.
200 ||| Get the name and type of the focused hole. Fails if not holes are present.
201+ export
199 getGoal : Elab (TTName, TT)
202 getGoal : Elab (TTName, TT)
200 getGoal = Prim__Goal
203 getGoal = Prim__Goal
201
204
202 ||| Get the hole queue, in order.
205 ||| Get the hole queue, in order.
206+ export
203 getHoles : Elab (List TTName)
207 getHoles : Elab (List TTName)
204 getHoles = Prim__Holes
208 getHoles = Prim__Holes
205
209
206 ||| If the current hole contains a guess, return it. Otherwise, fail.
210 ||| If the current hole contains a guess, return it. Otherwise, fail.
211+ export
207 getGuess : Elab TT
212 getGuess : Elab TT
208 getGuess = Prim__Guess
213 getGuess = Prim__Guess
209
214
210 ||| Look up the types of every overloading of a name.
215 ||| Look up the types of every overloading of a name.
216+ export
211 lookupTy : TTName -> Elab (List (TTName, NameType, TT))
217 lookupTy : TTName -> Elab (List (TTName, NameType, TT))
212 lookupTy n = Prim__LookupTy n
218 lookupTy n = Prim__LookupTy n
213
219
214 ||| Get the type of a fully-qualified name. Fail if it doesn not
220 ||| Get the type of a fully-qualified name. Fail if it doesn not
215 ||| resolve uniquely.
221 ||| resolve uniquely.
222+ export
216 lookupTyExact : TTName -> Elab (TTName, NameType, TT)
223 lookupTyExact : TTName -> Elab (TTName, NameType, TT)
217 lookupTyExact n = case !(lookupTy n) of
224 lookupTyExact n = case !(lookupTy n) of
218 [res] => return res
225 [res] => return res
@@ -221,12 +228,14 @@ namespace Tactics
221
228
222 ||| Find the reflected representation of all datatypes whose names
229 ||| Find the reflected representation of all datatypes whose names
223 ||| are overloadings of some name.
230 ||| are overloadings of some name.
231+ export
224 lookupDatatype : TTName -> Elab (List Datatype)
232 lookupDatatype : TTName -> Elab (List Datatype)
225 lookupDatatype n = Prim__LookupDatatype n
233 lookupDatatype n = Prim__LookupDatatype n
226
234
227 ||| Find the reflected representation of a datatype, given its
235 ||| Find the reflected representation of a datatype, given its
228 ||| fully-qualified name. Fail if the name does not uniquely resolve
236 ||| fully-qualified name. Fail if the name does not uniquely resolve
229 ||| to a datatype.
237 ||| to a datatype.
238+ export
230 lookupDatatypeExact : TTName -> Elab Datatype
239 lookupDatatypeExact : TTName -> Elab Datatype
231 lookupDatatypeExact n = case !(lookupDatatype n) of
240 lookupDatatypeExact n = case !(lookupDatatype n) of
232 [res] => return res
241 [res] => return res
@@ -235,12 +244,14 @@ namespace Tactics
235
244
236 ||| Find the reflected function definition of all functions whose names
245 ||| Find the reflected function definition of all functions whose names
237 ||| are overloadings of some name.
246 ||| are overloadings of some name.
247+ export
238 lookupFunDefn : TTName -> Elab (List (FunDefn TT))
248 lookupFunDefn : TTName -> Elab (List (FunDefn TT))
239 lookupFunDefn n = Prim__LookupFunDefn n
249 lookupFunDefn n = Prim__LookupFunDefn n
240
250
241 ||| Find the reflected function definition of a function, given its
251 ||| Find the reflected function definition of a function, given its
242 ||| fully-qualified name. Fail if the name does not uniquely resolve
252 ||| fully-qualified name. Fail if the name does not uniquely resolve
243 ||| to a function.
253 ||| to a function.
254+ export
244 lookupFunDefnExact : TTName -> Elab (FunDefn TT)
255 lookupFunDefnExact : TTName -> Elab (FunDefn TT)
245 lookupFunDefnExact n = case !(lookupFunDefn n) of
256 lookupFunDefnExact n = case !(lookupFunDefn n) of
246 [res] => return res
257 [res] => return res
@@ -248,11 +259,13 @@ namespace Tactics
248 xs => fail [TextPart "More than one function named", NamePart n]
259 xs => fail [TextPart "More than one function named", NamePart n]
249
260
250 ||| Get the argument specification for each overloading of a name.
261 ||| Get the argument specification for each overloading of a name.
262+ export
251 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
263 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
252 lookupArgs n = Prim__LookupArgs n
264 lookupArgs n = Prim__LookupArgs n
253
265
254 ||| Get the argument specification for a name. Fail if the name does
266 ||| Get the argument specification for a name. Fail if the name does
255 ||| not uniquely resolve.
267 ||| not uniquely resolve.
268+ export
256 lookupArgsExact : TTName -> Elab (TTName, List FunArg, Raw)
269 lookupArgsExact : TTName -> Elab (TTName, List FunArg, Raw)
257 lookupArgsExact n = case !(lookupArgs n) of
270 lookupArgsExact n = case !(lookupArgs n) of
258 [res] => return res
271 [res] => return res
@@ -263,6 +276,7 @@ namespace Tactics
263 |||
276 |||
264 ||| @ env the environment within which to check the type
277 ||| @ env the environment within which to check the type
265 ||| @ tm the term to check
278 ||| @ tm the term to check
279+ export
266 check : (env : List (TTName, Binder TT)) -> (tm : Raw) -> Elab (TT, TT)
280 check : (env : List (TTName, Binder TT)) -> (tm : Raw) -> Elab (TT, TT)
267 check env tm = Prim__Check env tm
281 check env tm = Prim__Check env tm
268
282
@@ -271,15 +285,18 @@ namespace Tactics
271 |||
285 |||
272 ||| **NB**: the generated name is unique _for this run of the
286 ||| **NB**: the generated name is unique _for this run of the
273 ||| elaborator_. Do not assume that they are globally unique.
287 ||| elaborator_. Do not assume that they are globally unique.
288+ export
274 gensym : (hint : String) -> Elab TTName
289 gensym : (hint : String) -> Elab TTName
275 gensym hint = Prim__Gensym hint
290 gensym hint = Prim__Gensym hint
276
291
277 ||| Substitute a guess into a hole.
292 ||| Substitute a guess into a hole.
293+ export
278 solve : Elab ()
294 solve : Elab ()
279 solve = Prim__Solve
295 solve = Prim__Solve
280
296
281 ||| Place a term into a hole, unifying its type. Fails if the focus
297 ||| Place a term into a hole, unifying its type. Fails if the focus
282 ||| is not a hole.
298 ||| is not a hole.
299+ export
283 fill : Raw -> Elab ()
300 fill : Raw -> Elab ()
284 fill tm = Prim__Fill tm
301 fill tm = Prim__Fill tm
285
302
@@ -297,6 +314,7 @@ namespace Tactics
297 ||| @ argSpec instructions for finding the arguments to the term,
314 ||| @ argSpec instructions for finding the arguments to the term,
298 ||| where the Boolean states whether or not to attempt to solve
315 ||| where the Boolean states whether or not to attempt to solve
299 ||| the argument by unification.
316 ||| the argument by unification.
317+ export
300 apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
318 apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
301 apply tm argSpec = map snd <$> Prim__Apply tm argSpec
319 apply tm argSpec = map snd <$> Prim__Apply tm argSpec
302
320
@@ -315,6 +333,7 @@ namespace Tactics
315 ||| where the Boolean states whether or not to attempt to solve
333 ||| where the Boolean states whether or not to attempt to solve
316 ||| the argument by matching.
334 ||| the argument by matching.
317
335
336+ export
318 matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
337 matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
319 matchApply tm argSpec = map snd <$> Prim__Apply tm argSpec
338 matchApply tm argSpec = map snd <$> Prim__Apply tm argSpec
320
339
@@ -322,11 +341,13 @@ namespace Tactics
322 ||| exist.
341 ||| exist.
323 |||
342 |||
324 ||| @ hole the hole to focus on
343 ||| @ hole the hole to focus on
344+ export
325 focus : (hole : TTName) -> Elab ()
345 focus : (hole : TTName) -> Elab ()
326 focus hole = Prim__Focus hole
346 focus hole = Prim__Focus hole
327
347
328 ||| Send the currently-focused hole to the end of the hole queue and
348 ||| Send the currently-focused hole to the end of the hole queue and
329 ||| focus on the next hole.
349 ||| focus on the next hole.
350+ export
330 unfocus : TTName -> Elab ()
351 unfocus : TTName -> Elab ()
331 unfocus hole = Prim__Unfocus hole
352 unfocus hole = Prim__Unfocus hole
332
353
@@ -338,6 +359,7 @@ namespace Tactics
338 ||| binding, or else the scopes of the generated terms won't make
359 ||| binding, or else the scopes of the generated terms won't make
339 ||| sense. This tactic creates a new hole of the proper form, and
360 ||| sense. This tactic creates a new hole of the proper form, and
340 ||| points the old hole at it.
361 ||| points the old hole at it.
362+ export
341 attack : Elab ()
363 attack : Elab ()
342 attack = Prim__Attack
364 attack = Prim__Attack
343
365
@@ -346,6 +368,7 @@ namespace Tactics
346 ||| The new hole will be focused, and the previously-focused hole
368 ||| The new hole will be focused, and the previously-focused hole
347 ||| will be immediately after it in the hole queue. Because this
369 ||| will be immediately after it in the hole queue. Because this
348 ||| tactic introduces a new binding, you may need to `attack` first.
370 ||| tactic introduces a new binding, you may need to `attack` first.
371+ export
349 claim : TTName -> Raw -> Elab ()
372 claim : TTName -> Raw -> Elab ()
350 claim n ty = Prim__Claim n ty
373 claim n ty = Prim__Claim n ty
351
374
@@ -354,6 +377,7 @@ namespace Tactics
354 ||| `attack`).
377 ||| `attack`).
355 |||
378 |||
356 ||| @ n the name to use for the argument
379 ||| @ n the name to use for the argument
380+ export
357 intro : (n : TTName) -> Elab ()
381 intro : (n : TTName) -> Elab ()
358 intro n = Prim__Intro (Just n)
382 intro n = Prim__Intro (Just n)
359
383
@@ -363,6 +387,7 @@ namespace Tactics
363 |||
387 |||
364 ||| Requires that the hole be immediately under its binder (use
388 ||| Requires that the hole be immediately under its binder (use
365 ||| `attack` if it might not be).
389 ||| `attack` if it might not be).
390+ export
366 intro' : Elab ()
391 intro' : Elab ()
367 intro' = Prim__Intro Nothing
392 intro' = Prim__Intro Nothing
368
393
@@ -371,10 +396,12 @@ namespace Tactics
371 |||
396 |||
372 ||| Requires that the hole be immediately under its binder (use
397 ||| Requires that the hole be immediately under its binder (use
373 ||| `attack` if it might not be).
398 ||| `attack` if it might not be).
399+ export
374 forall : TTName -> Raw -> Elab ()
400 forall : TTName -> Raw -> Elab ()
375 forall n ty = Prim__Forall n ty
401 forall n ty = Prim__Forall n ty
376
402
377 ||| Convert a hole into a pattern variable.
403 ||| Convert a hole into a pattern variable.
404+ export
378 patvar : TTName -> Elab ()
405 patvar : TTName -> Elab ()
379 patvar n = Prim__PatVar n
406 patvar n = Prim__PatVar n
380
407
@@ -382,6 +409,7 @@ namespace Tactics
382 |||
409 |||
383 ||| Requires that the hole be immediately under its binder (use
410 ||| Requires that the hole be immediately under its binder (use
384 ||| `attack` if it might not be).
411 ||| `attack` if it might not be).
412+ export
385 patbind : TTName -> Elab ()
413 patbind : TTName -> Elab ()
386 patbind n = Prim__PatBind n
414 patbind n = Prim__PatBind n
387
415
@@ -393,10 +421,12 @@ namespace Tactics
393 ||| @ n the name to let bind
421 ||| @ n the name to let bind
394 ||| @ ty the type of the term to be let-bound
422 ||| @ ty the type of the term to be let-bound
395 ||| @ tm the term to be bound
423 ||| @ tm the term to be bound
424+ export
396 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
425 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
397 letbind n ty tm = Prim__LetBind n ty tm
426 letbind n ty tm = Prim__LetBind n ty tm
398
427
399 ||| Normalise the goal.
428 ||| Normalise the goal.
429+ export
400 compute : Elab ()
430 compute : Elab ()
401 compute = Prim__Compute
431 compute = Prim__Compute
402
432
@@ -404,12 +434,14 @@ namespace Tactics
404 |||
434 |||
405 ||| @ env the environment in which to compute (get one of these from `getEnv`)
435 ||| @ env the environment in which to compute (get one of these from `getEnv`)
406 ||| @ term the term to normalise
436 ||| @ term the term to normalise
437+ export
407 normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
438 normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
408 normalise env term = Prim__Normalise env term
439 normalise env term = Prim__Normalise env term
409
440
410 ||| Reduce a closed term to weak-head normal form
441 ||| Reduce a closed term to weak-head normal form
411 |||
442 |||
412 ||| @ term the term to reduce
443 ||| @ term the term to reduce
444+ export
413 whnf : (term : TT) -> Elab TT
445 whnf : (term : TT) -> Elab TT
414 whnf term = Prim__Whnf term
446 whnf term = Prim__Whnf term
415
447
@@ -419,6 +451,7 @@ namespace Tactics
419 ||| @ env a lexical environment to compare the terms in (see `getEnv`)
451 ||| @ env a lexical environment to compare the terms in (see `getEnv`)
420 ||| @ term1 the first term to convert
452 ||| @ term1 the first term to convert
421 ||| @ term2 the second term to convert
453 ||| @ term2 the second term to convert
454+ export
422 convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab ()
455 convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab ()
423 convertsInEnv env term1 term2 = Prim__Converts env term1 term2
456 convertsInEnv env term1 term2 = Prim__Converts env term1 term2
424
457
@@ -426,14 +459,17 @@ namespace Tactics
426 |||
459 |||
427 ||| @ term1 the first term to convert
460 ||| @ term1 the first term to convert
428 ||| @ term2 the second term to convert
461 ||| @ term2 the second term to convert
462+ export
429 converts : (term1, term2 : TT) -> Elab ()
463 converts : (term1, term2 : TT) -> Elab ()
430 converts term1 term2 = convertsInEnv !getEnv term1 term2
464 converts term1 term2 = convertsInEnv !getEnv term1 term2
431
465
432 ||| Find the source context for the elaboration script
466 ||| Find the source context for the elaboration script
467+ export
433 getSourceLocation : Elab SourceLocation
468 getSourceLocation : Elab SourceLocation
434 getSourceLocation = Prim__SourceLocation
469 getSourceLocation = Prim__SourceLocation
435
470
436 ||| Attempt to solve the current goal with the source code location
471 ||| Attempt to solve the current goal with the source code location
472+ export
437 sourceLocation : Elab ()
473 sourceLocation : Elab ()
438 sourceLocation = do loc <- getSourceLocation
474 sourceLocation = do loc <- getSourceLocation
439 fill (quote loc)
475 fill (quote loc)
@@ -444,6 +480,7 @@ namespace Tactics
444 |||
480 |||
445 ||| The namespace is represented as a reverse-order list of strings,
481 ||| The namespace is represented as a reverse-order list of strings,
446 ||| just as in the representation of names.
482 ||| just as in the representation of names.
483+ export
447 currentNamespace : Elab (List String)
484 currentNamespace : Elab (List String)
448 currentNamespace = Prim__Namespace
485 currentNamespace = Prim__Namespace
449
486
@@ -457,16 +494,19 @@ namespace Tactics
457 ||| Because this tactic internally introduces a `let` binding, it
494 ||| Because this tactic internally introduces a `let` binding, it
458 ||| requires that the hole be immediately under its binder (use
495 ||| requires that the hole be immediately under its binder (use
459 ||| `attack` if it might not be).
496 ||| `attack` if it might not be).
497+ export
460 rewriteWith : Raw -> Elab ()
498 rewriteWith : Raw -> Elab ()
461 rewriteWith rule = Prim__Rewrite rule
499 rewriteWith rule = Prim__Rewrite rule
462
500
463 ||| Add a type declaration to the global context.
501 ||| Add a type declaration to the global context.
502+ export
464 declareType : TyDecl -> Elab ()
503 declareType : TyDecl -> Elab ()
465 declareType decl = Prim__DeclareType decl
504 declareType decl = Prim__DeclareType decl
466
505
467 ||| Define a function in the global context. The function must have
506 ||| Define a function in the global context. The function must have
468 ||| already been declared, either in ordinary Idris code or using
507 ||| already been declared, either in ordinary Idris code or using
469 ||| `declareType`.
508 ||| `declareType`.
509+ export
470 defineFunction : FunDefn Raw -> Elab ()
510 defineFunction : FunDefn Raw -> Elab ()
471 defineFunction defun = Prim__DefineFunction defun
511 defineFunction defun = Prim__DefineFunction defun
472
512
@@ -474,12 +514,14 @@ namespace Tactics
474 |||
514 |||
475 ||| @ ifaceName the name of the interface for which an implementation is being registered
515 ||| @ ifaceName the name of the interface for which an implementation is being registered
476 ||| @ instName the name of the definition to use in implementation search
516 ||| @ instName the name of the definition to use in implementation search
517+ export
477 addInstance : (ifaceName, instName : TTName) -> Elab ()
518 addInstance : (ifaceName, instName : TTName) -> Elab ()
478 addInstance ifaceName instName = Prim__AddInstance ifaceName instName
519 addInstance ifaceName instName = Prim__AddInstance ifaceName instName
479
520
480 ||| Determine whether a name denotes an interface.
521 ||| Determine whether a name denotes an interface.
481 |||
522 |||
482 ||| @ name a name that might denote an interface.
523 ||| @ name a name that might denote an interface.
524+ export
483 isTCName : (name : TTName) -> Elab Bool
525 isTCName : (name : TTName) -> Elab Bool
484 isTCName name = Prim__IsTCName name
526 isTCName name = Prim__IsTCName name
485
527
@@ -487,10 +529,12 @@ namespace Tactics
487 |||
529 |||
488 ||| @ fn the name of the definition being elaborated (to prevent Idris
530 ||| @ fn the name of the definition being elaborated (to prevent Idris
489 ||| from looping)
531 ||| from looping)
532+ export
490 resolveTC : (fn : TTName) -> Elab ()
533 resolveTC : (fn : TTName) -> Elab ()
491 resolveTC fn = Prim__ResolveTC fn
534 resolveTC fn = Prim__ResolveTC fn
492
535
493 ||| Use Idris's internal proof search.
536 ||| Use Idris's internal proof search.
537+ export
494 search : Elab ()
538 search : Elab ()
495 search = Prim__Search 100 []
539 search = Prim__Search 100 []
496
540
@@ -498,6 +542,7 @@ namespace Tactics
498 |||
542 |||
499 ||| @ depth the search depth
543 ||| @ depth the search depth
500 ||| @ hints additional names to try
544 ||| @ hints additional names to try
545+ export
501 search' : (depth : Int) -> (hints : List TTName) -> Elab ()
546 search' : (depth : Int) -> (hints : List TTName) -> Elab ()
502 search' depth hints = Prim__Search depth hints
547 search' depth hints = Prim__Search depth hints
503
548
@@ -507,6 +552,7 @@ namespace Tactics
507 ||| if the string is not a valid operator.
552 ||| if the string is not a valid operator.
508 |||
553 |||
509 ||| @ operator the operator string to look up
554 ||| @ operator the operator string to look up
555+ export
510 operatorFixity : (operator : String) -> Elab Fixity
556 operatorFixity : (operator : String) -> Elab Fixity
511 operatorFixity operator = Prim__Fixity operator
557 operatorFixity operator = Prim__Fixity operator
512
558
@@ -514,6 +560,7 @@ namespace Tactics
514 |||
560 |||
515 ||| This is intended for elaboration script developers, not for
561 ||| This is intended for elaboration script developers, not for
516 ||| end-users. Use `fail` for final scripts.
562 ||| end-users. Use `fail` for final scripts.
563+ export
517 debug : Elab a
564 debug : Elab a
518 debug = Prim__Debug []
565 debug = Prim__Debug []
519
566
@@ -524,18 +571,21 @@ namespace Tactics
524 ||| end-users. Use `fail` for final scripts.
571 ||| end-users. Use `fail` for final scripts.
525 |||
572 |||
526 ||| @ msg the message to display
573 ||| @ msg the message to display
574+ export
527 debugMessage : (msg : List ErrorReportPart) -> Elab a
575 debugMessage : (msg : List ErrorReportPart) -> Elab a
528 debugMessage msg = Prim__Debug msg
576 debugMessage msg = Prim__Debug msg
529
577
530 ||| Create a new top-level metavariable to solve the current hole.
578 ||| Create a new top-level metavariable to solve the current hole.
531 |||
579 |||
532 ||| @ name the name for the top-level variable
580 ||| @ name the name for the top-level variable
581+ export
533 metavar : (name : TTName) -> Elab ()
582 metavar : (name : TTName) -> Elab ()
534 metavar name = Prim__Metavar name
583 metavar name = Prim__Metavar name
535
584
536 ||| Recursively invoke the reflected elaborator with some goal.
585 ||| Recursively invoke the reflected elaborator with some goal.
537 |||
586 |||
538 ||| The result is the final term and its type.
587 ||| The result is the final term and its type.
588+ export
539 runElab : Raw -> Elab () -> Elab (TT, TT)
589 runElab : Raw -> Elab () -> Elab (TT, TT)
540 runElab goal script = Prim__RecursiveElab goal script
590 runElab goal script = Prim__RecursiveElab goal script
541
591
libs/prelude/Prelude/File.idr+29−1
@@ -49,25 +49,31 @@ Show FileError where
49 show (GenericFileError errno) = strError errno
49 show (GenericFileError errno) = strError errno
50
50
51||| Standard input
51||| Standard input
52+export
52stdin : File
53stdin : File
53stdin = FHandle prim__stdin
54stdin = FHandle prim__stdin
54
55
55||| Standard output
56||| Standard output
57+export
56stdout : File
58stdout : File
57stdout = FHandle prim__stdout
59stdout = FHandle prim__stdout
58
60
59||| Standard output
61||| Standard output
62+export
60stderr : File
63stderr : File
61stderr = FHandle prim__stderr
64stderr = FHandle prim__stderr
62
65
66+private
63do_ferror : Ptr -> IO Int
67do_ferror : Ptr -> IO Int
64do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h
68do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h
65
69
70+export
66ferror : File -> IO Bool
71ferror : File -> IO Bool
67ferror (FHandle h) = do err <- do_ferror h
72ferror (FHandle h) = do err <- do_ferror h
68 return (not (err == 0))
73 return (not (err == 0))
69
74
70||| Call the RTS's file opening function
75||| Call the RTS's file opening function
76+private
71do_fopen : String -> String -> IO Ptr
77do_fopen : String -> String -> IO Ptr
72do_fopen f m
78do_fopen f m
73 = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m
79 = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m
@@ -75,6 +81,7 @@ do_fopen f m
75||| Open a file
81||| Open a file
76||| @ f the filename
82||| @ f the filename
77||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)
83||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)
84+export
78fopen : (f : String) -> (m : String) -> IO (Either FileError File)
85fopen : (f : String) -> (m : String) -> IO (Either FileError File)
79fopen f m = do h <- do_fopen f m
86fopen f m = do h <- do_fopen f m
80 if !(nullPtr h)
87 if !(nullPtr h)
@@ -83,6 +90,7 @@ fopen f m = do h <- do_fopen f m
83 else return (Right (FHandle h))
90 else return (Right (FHandle h))
84
91
85||| Check whether a file handle is actually a null pointer
92||| Check whether a file handle is actually a null pointer
93+export
86validFile : File -> IO Bool
94validFile : File -> IO Bool
87validFile (FHandle h) = do x <- nullPtr h
95validFile (FHandle h) = do x <- nullPtr h
88 return (not x)
96 return (not x)
@@ -93,33 +101,41 @@ data Mode = Read | Write | ReadWrite
93||| Open a file
101||| Open a file
94||| @ f the filename
102||| @ f the filename
95||| @ m the mode; either Read, Write, or ReadWrite
103||| @ m the mode; either Read, Write, or ReadWrite
104+export
96openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
105openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
97openFile f m = fopen f (modeStr m) where
106openFile f m = fopen f (modeStr m) where
98 modeStr Read = "r"
107 modeStr Read = "r"
99 modeStr Write = "w"
108 modeStr Write = "w"
100 modeStr ReadWrite = "r+"
109 modeStr ReadWrite = "r+"
101
110
111+private
102do_fclose : Ptr -> IO ()
112do_fclose : Ptr -> IO ()
103do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h
113do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h
104
114
115+export
105closeFile : File -> IO ()
116closeFile : File -> IO ()
106closeFile (FHandle h) = do_fclose h
117closeFile (FHandle h) = do_fclose h
107
118
119+private
108do_fread : Ptr -> IO' l String
120do_fread : Ptr -> IO' l String
109do_fread h = prim_fread h
121do_fread h = prim_fread h
110
122
123+export
111fgetc : File -> IO (Either FileError Char)
124fgetc : File -> IO (Either FileError Char)
112fgetc (FHandle h) = do let c = cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h)
125fgetc (FHandle h) = do let c = cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h)
113 if !(ferror (FHandle h))
126 if !(ferror (FHandle h))
114 then return (Left FileReadError)
127 then return (Left FileReadError)
115 else return (Right c)
128 else return (Right c)
116
129
130+export
117fflush : File -> IO ()
131fflush : File -> IO ()
118fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h
132fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h
119
133
134+private
120do_popen : String -> String -> IO Ptr
135do_popen : String -> String -> IO Ptr
121do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m
136do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m
122
137
138+export
123popen : String -> Mode -> IO (Either FileError File)
139popen : String -> Mode -> IO (Either FileError File)
124popen f m = do ptr <- do_popen f (modeStr m)
140popen f m = do ptr <- do_popen f (modeStr m)
125 if !(nullPtr ptr)
141 if !(nullPtr ptr)
@@ -131,12 +147,14 @@ popen f m = do ptr <- do_popen f (modeStr m)
131 modeStr Write = "w"
147 modeStr Write = "w"
132 modeStr ReadWrite = "r+"
148 modeStr ReadWrite = "r+"
133
149
150+export
134pclose : File -> IO ()
151pclose : File -> IO ()
135pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h
152pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h
136
153
137-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))
154-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))
138-- prim__vm h
155-- prim__vm h
139
156
157+export
140fread : File -> IO (Either FileError String)
158fread : File -> IO (Either FileError String)
141fread (FHandle h) = do str <- do_fread h
159fread (FHandle h) = do str <- do_fread h
142 if !(ferror (FHandle h))
160 if !(ferror (FHandle h))
@@ -145,11 +163,13 @@ fread (FHandle h) = do str <- do_fread h
145
163
146||| Read a line from a file
164||| Read a line from a file
147||| @h a file handle which must be open for reading
165||| @h a file handle which must be open for reading
166+export
148fGetLine : (h : File) -> IO (Either FileError String)
167fGetLine : (h : File) -> IO (Either FileError String)
149fGetLine = fread
168fGetLine = fread
150
169
151%deprecate fread "Use fGetLine instead"
170%deprecate fread "Use fGetLine instead"
152
171
172+private
153do_fwrite : Ptr -> String -> IO (Either FileError ())
173do_fwrite : Ptr -> String -> IO (Either FileError ())
154do_fwrite h s = do res <- prim_fwrite h s
174do_fwrite h s = do res <- prim_fwrite h s
155 if (res /= 0)
175 if (res /= 0)
@@ -160,41 +180,48 @@ do_fwrite h s = do res <- prim_fwrite h s
160 return (Left err)
180 return (Left err)
161 else return (Right ())
181 else return (Right ())
162
182
183+export
163fwrite : File -> String -> IO (Either FileError ())
184fwrite : File -> String -> IO (Either FileError ())
164fwrite (FHandle h) s = do_fwrite h s
185fwrite (FHandle h) s = do_fwrite h s
165
186
166||| Write a line to a file
187||| Write a line to a file
167||| @h a file handle which must be open for writing
188||| @h a file handle which must be open for writing
168||| @str the line to write to the file
189||| @str the line to write to the file
190+export
169fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
191fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
170fPutStr (FHandle h) s = do_fwrite h s
192fPutStr (FHandle h) s = do_fwrite h s
171
193
194+export
172fPutStrLn : File -> String -> IO (Either FileError ())
195fPutStrLn : File -> String -> IO (Either FileError ())
173fPutStrLn (FHandle h) s = do_fwrite h (s ++ "\n")
196fPutStrLn (FHandle h) s = do_fwrite h (s ++ "\n")
174
197
175%deprecate fwrite "Use fPutStr instead"
198%deprecate fwrite "Use fPutStr instead"
176
199
200+private
177do_feof : Ptr -> IO Int
201do_feof : Ptr -> IO Int
178do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
202do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
179
203
180||| Check if a file handle has reached the end
204||| Check if a file handle has reached the end
205+export
181fEOF : File -> IO Bool
206fEOF : File -> IO Bool
182fEOF (FHandle h) = do eof <- do_feof h
207fEOF (FHandle h) = do eof <- do_feof h
183 return (not (eof == 0))
208 return (not (eof == 0))
184
209
185||| Check if a file handle has reached the end
210||| Check if a file handle has reached the end
211+export
186feof : File -> IO Bool
212feof : File -> IO Bool
187feof = fEOF
213feof = fEOF
188
214
189%deprecate feof "Use fEOF instead"
215%deprecate feof "Use fEOF instead"
190
216
217+export
191fpoll : File -> IO Bool
218fpoll : File -> IO Bool
192fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
219fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
193 return (p > 0)
220 return (p > 0)
194
221
195||| Read the contents of a file into a string
222||| Read the contents of a file into a string
196partial -- might be reading something infinitely long like /dev/null ...
223partial -- might be reading something infinitely long like /dev/null ...
197−covering
224+covering export
198readFile : String -> IO (Either FileError String)
225readFile : String -> IO (Either FileError String)
199readFile fn = do Right h <- openFile fn Read
226readFile fn = do Right h <- openFile fn Read
200 | Left err => return (Left err)
227 | Left err => return (Left err)
@@ -212,6 +239,7 @@ readFile fn = do Right h <- openFile fn Read
212 else return (Right contents)
239 else return (Right contents)
213
240
214||| Write a string to a file
241||| Write a string to a file
242+export
215writeFile : (filepath : String) -> (contents : String) ->
243writeFile : (filepath : String) -> (contents : String) ->
216 IO (Either FileError ())
244 IO (Either FileError ())
217writeFile fn contents = do
245writeFile fn contents = do
src/Idris/Core/CaseTree.hs+2−2
@@ -152,10 +152,10 @@ findCalls sc topargs = nub $ nu' topargs sc where
152 nua ps (SucCase _ sc) = nu' ps sc
152 nua ps (SucCase _ sc) = nu' ps sc
153 nua ps (DefaultCase sc) = nu' ps sc
153 nua ps (DefaultCase sc) = nu' ps sc
154
154
155− nut ps (P Ref n _) | n `elem` ps = []
155+ nut ps (P _ n _) | n `elem` ps = []
156 | otherwise = [(n, [])] -- tmp
156 | otherwise = [(n, [])] -- tmp
157 nut ps fn@(App _ f a)
157 nut ps fn@(App _ f a)
158− | (P Ref n _, args) <- unApply fn
158+ | (P _ n _, args) <- unApply fn
159 = if n `elem` ps then nut ps f ++ nut ps a
159 = if n `elem` ps then nut ps f ++ nut ps a
160 else [(n, map argNames args)] ++ concatMap (nut ps) args
160 else [(n, map argNames args)] ++ concatMap (nut ps) args
161 | (P (TCon _ _) n _, _) <- unApply fn = []
161 | (P (TCon _ _) n _, _) <- unApply fn = []
src/Idris/ParseHelpers.hs+2−2
@@ -659,8 +659,8 @@ addAcc n a = do i <- get
659{- | Add accessbility option for data declarations
659{- | Add accessbility option for data declarations
660 (works for classes too - 'abstract' means the data/class is visible but members not) -}
660 (works for classes too - 'abstract' means the data/class is visible but members not) -}
661accData :: Accessibility -> Name -> [Name] -> IdrisParser ()
661accData :: Accessibility -> Name -> [Name] -> IdrisParser ()
662−accData Frozen n ns = do addAcc n Frozen
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
663+ mapM_ (\n -> addAcc n Hidden) ns -- so that they are invisible
664accData a n ns = do addAcc n a
664accData a n ns = do addAcc n a
665 mapM_ (`addAcc` a) ns
665 mapM_ (`addAcc` a) ns
666
666