git.iko.soy/Idris-dev
on master help sign in
Tidy up name warnings in Prelude
commit53f46510bcf5d2a9a769cf7eea24757025c3aeb9 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 17 Oct 2015, 22:39 (11 years ago) parent47b83b8
7 files changed+163−163
compare with master
unifiedsplit
libs/base/Control/Catchable.idr+3−3 libs/base/Control/IOExcept.idr+9−9 libs/effects/Effect/Exception.idr+1−1 libs/prelude/IO.idr+3−3 libs/prelude/Language/Reflection/Elab.idr+94−94 libs/prelude/Prelude/Nat.idr+10−10 src/Idris/Elab/Term.hs+43−43
libs/base/Control/Catchable.idr+3−3
@@ -19,11 +19,11 @@ instance Catchable (Either a) a where
1919 throw x = Left x
2020
2121instance Catchable (IOExcept err) err where
22− catch (ioM prog) h = ioM (do p' <- prog
22+ catch (IOM prog) h = IOM (do p' <- prog
2323 case p' of
24− Left e => let ioM he = h e in he
24+ Left e => let IOM he = h e in he
2525 Right val => return (Right val))
26− throw x = ioM (return (Left x))
26+ throw x = IOM (return (Left x))
2727
2828instance Catchable List () where
2929 catch [] h = h ()
libs/base/Control/IOExcept.idr+9−9
@@ -3,32 +3,32 @@ module Control.IOExcept
33-- An IO monad with exception handling
44
55data IOExcept : Type -> Type -> Type where
6− ioM : IO (Either err a) -> IOExcept err a
6+ IOM : IO (Either err a) -> IOExcept err a
77
88instance Functor (IOExcept e) where
9− map f (ioM fn) = ioM (map (map f) fn)
9+ map f (IOM fn) = IOM (map (map f) fn)
1010
1111instance Applicative (IOExcept e) where
12− pure x = ioM (pure (pure x))
13− (ioM f) <*> (ioM a) = ioM (do f' <- f; a' <- a
12+ pure x = IOM (pure (pure x))
13+ (IOM f) <*> (IOM a) = IOM (do f' <- f; a' <- a
1414 return (f' <*> a'))
1515
1616instance Monad (IOExcept e) where
17− (ioM x) >>= k = ioM (do x' <- x;
17+ (IOM x) >>= k = IOM (do x' <- x;
1818 case x' of
19− Right a => let (ioM ka) = k a in
19+ Right a => let (IOM ka) = k a in
2020 ka
2121 Left err => return (Left err))
2222
2323ioe_lift : IO a -> IOExcept err a
24−ioe_lift op = ioM (do op' <- op
24+ioe_lift op = IOM (do op' <- op
2525 return (Right op'))
2626
2727ioe_fail : err -> IOExcept err a
28−ioe_fail e = ioM (return (Left e))
28+ioe_fail e = IOM (return (Left e))
2929
3030ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b
31−ioe_run (ioM act) err ok = do act' <- act
31+ioe_run (IOM act) err ok = do act' <- act
3232 case act' of
3333 Left e => err e
3434 Right v => ok v
libs/effects/Effect/Exception.idr+1−1
@@ -18,7 +18,7 @@ instance Show a => Handler (Exception a) IO where
1818 believe_me (exit 1)
1919
2020instance Handler (Exception a) (IOExcept a) where
21− handle _ (Raise e) k = ioM (return (Left e))
21+ handle _ (Raise e) k = IOM (return (Left e))
2222
2323instance Handler (Exception a) (Either a) where
2424 handle _ (Raise e) k = Left e
libs/prelude/IO.idr+3−3
@@ -8,7 +8,7 @@ import Prelude.List
88||| Idris's primitive IO, for building abstractions on top of
99abstract
1010data PrimIO : Type -> Type where
11− prim__IO : a -> PrimIO a
11+ Prim__IO : a -> PrimIO a
1212
1313||| A token representing the world, for use in `IO`
1414abstract data World = TheWorld prim__WorldType
@@ -94,14 +94,14 @@ foreign ffi fname ty {fty} = foreign_prim ffi fname fty []
9494
9595abstract
9696prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
97−prim_io_bind (prim__IO v) k = k v
97+prim_io_bind (Prim__IO v) k = k v
9898
9999unsafePerformPrimIO : PrimIO a -> a
100100-- compiled as primitive
101101
102102abstract
103103prim_io_return : a -> PrimIO a
104−prim_io_return x = prim__IO x
104+prim_io_return x = Prim__IO x
105105
106106abstract
107107io_bind : IO' l a -> (a -> IO' l b) -> IO' l b
libs/prelude/Language/Reflection/Elab.idr+94−94
@@ -104,62 +104,62 @@ record Datatype where
104104abstract
105105data Elab : Type -> Type where
106106 -- obligatory control stuff
107− prim__PureElab : a -> Elab a
108− prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b
107+ Prim__PureElab : a -> Elab a
108+ Prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b
109109
110− prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a
111− prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a
110+ Prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a
111+ Prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a
112112
113− prim__Env : Elab (List (TTName, Binder TT))
114− prim__Goal : Elab (TTName, TT)
115− prim__Holes : Elab (List TTName)
116− prim__Guess : Elab (Maybe TT)
117− prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
118− prim__LookupDatatype : TTName -> Elab (List Datatype)
119− prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
113+ Prim__Env : Elab (List (TTName, Binder TT))
114+ Prim__Goal : Elab (TTName, TT)
115+ Prim__Holes : Elab (List TTName)
116+ Prim__Guess : Elab (Maybe TT)
117+ Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
118+ Prim__LookupDatatype : TTName -> Elab (List Datatype)
119+ Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
120120
121− prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)
121+ Prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)
122122
123− prim__SourceLocation : Elab SourceLocation
124− prim__Namespace : Elab (List String)
123+ Prim__SourceLocation : Elab SourceLocation
124+ Prim__Namespace : Elab (List String)
125125
126− prim__Gensym : String -> Elab TTName
126+ Prim__Gensym : String -> Elab TTName
127127
128− prim__Solve : Elab ()
129− prim__Fill : Raw -> Elab ()
130− prim__Apply : Raw -> List Bool -> Elab (List (TTName, TTName))
131− prim__MatchApply : Raw -> List Bool -> Elab (List (TTName, TTName))
132− prim__Focus : TTName -> Elab ()
133− prim__Unfocus : TTName -> Elab ()
134− prim__Attack : Elab ()
128+ Prim__Solve : Elab ()
129+ Prim__Fill : Raw -> Elab ()
130+ Prim__Apply : Raw -> List Bool -> Elab (List (TTName, TTName))
131+ Prim__MatchApply : Raw -> List Bool -> Elab (List (TTName, TTName))
132+ Prim__Focus : TTName -> Elab ()
133+ Prim__Unfocus : TTName -> Elab ()
134+ Prim__Attack : Elab ()
135135
136− prim__Rewrite : Raw -> Elab ()
136+ Prim__Rewrite : Raw -> Elab ()
137137
138− prim__Claim : TTName -> Raw -> Elab ()
139− prim__Intro : Maybe TTName -> Elab ()
140− prim__Forall : TTName -> Raw -> Elab ()
141− prim__PatVar : TTName -> Elab ()
142− prim__PatBind : TTName -> Elab ()
143− prim__LetBind : TTName -> Raw -> Raw -> Elab ()
138+ Prim__Claim : TTName -> Raw -> Elab ()
139+ Prim__Intro : Maybe TTName -> Elab ()
140+ Prim__Forall : TTName -> Raw -> Elab ()
141+ Prim__PatVar : TTName -> Elab ()
142+ Prim__PatBind : TTName -> Elab ()
143+ Prim__LetBind : TTName -> Raw -> Raw -> Elab ()
144144
145− prim__Compute : Elab ()
146− prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
147− prim__Whnf : TT -> Elab TT
148− prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()
145+ Prim__Compute : Elab ()
146+ Prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
147+ Prim__Whnf : TT -> Elab TT
148+ Prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()
149149
150− prim__DeclareType : TyDecl -> Elab ()
151− prim__DefineFunction : FunDefn -> Elab ()
152− prim__AddInstance : TTName -> TTName -> Elab ()
153− prim__IsTCName : TTName -> Elab Bool
150+ Prim__DeclareType : TyDecl -> Elab ()
151+ Prim__DefineFunction : FunDefn -> Elab ()
152+ Prim__AddInstance : TTName -> TTName -> Elab ()
153+ Prim__IsTCName : TTName -> Elab Bool
154154
155− prim__ResolveTC : TTName -> Elab ()
156− prim__Search : Int -> List TTName -> Elab ()
157− prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)
155+ Prim__ResolveTC : TTName -> Elab ()
156+ Prim__Search : Int -> List TTName -> Elab ()
157+ Prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)
158158
159− prim__Fixity : String -> Elab Fixity
159+ Prim__Fixity : String -> Elab Fixity
160160
161− prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a
162− prim__Metavar : TTName -> Elab ()
161+ Prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a
162+ Prim__Metavar : TTName -> Elab ()
163163
164164-------------
165165-- Public API
@@ -167,47 +167,47 @@ data Elab : Type -> Type where
167167%access public
168168namespace Tactics
169169 instance Functor Elab where
170− map f t = prim__BindElab t (\x => prim__PureElab (f x))
170+ map f t = Prim__BindElab t (\x => Prim__PureElab (f x))
171171
172172 instance Applicative Elab where
173− pure x = prim__PureElab x
174− f <*> x = prim__BindElab f $ \g =>
175− prim__BindElab x $ \y =>
176− prim__PureElab $ g y
173+ pure x = Prim__PureElab x
174+ f <*> x = Prim__BindElab f $ \g =>
175+ Prim__BindElab x $ \y =>
176+ Prim__PureElab $ g y
177177
178178 ||| The Alternative instance on Elab represents left-biased error
179179 ||| handling. In other words, `t <|> t'` will run `t`, and if it
180180 ||| fails, roll back the elaboration state and run `t'`.
181181 instance Alternative Elab where
182− empty = prim__Fail [TextPart "empty"]
183− x <|> y = prim__Try x y
182+ empty = Prim__Fail [TextPart "empty"]
183+ x <|> y = Prim__Try x y
184184
185185 instance Monad Elab where
186− x >>= f = prim__BindElab x f
186+ x >>= f = Prim__BindElab x f
187187
188188 ||| Halt elaboration with an error
189189 fail : List ErrorReportPart -> Elab a
190− fail err = prim__Fail err
190+ fail err = Prim__Fail err
191191
192192 ||| Look up the lexical binding at the focused hole. Fails if no holes are present.
193193 getEnv : Elab (List (TTName, Binder TT))
194− getEnv = prim__Env
194+ getEnv = Prim__Env
195195
196196 ||| Get the name and type of the focused hole. Fails if not holes are present.
197197 getGoal : Elab (TTName, TT)
198− getGoal = prim__Goal
198+ getGoal = Prim__Goal
199199
200200 ||| Get the hole queue, in order.
201201 getHoles : Elab (List TTName)
202− getHoles = prim__Holes
202+ getHoles = Prim__Holes
203203
204204 ||| If the current hole contains a guess, return it. Otherwise, fail.
205205 getGuess : Elab (Maybe TT)
206− getGuess = prim__Guess
206+ getGuess = Prim__Guess
207207
208208 ||| Look up the types of every overloading of a name.
209209 lookupTy : TTName -> Elab (List (TTName, NameType, TT))
210− lookupTy n = prim__LookupTy n
210+ lookupTy n = Prim__LookupTy n
211211
212212 ||| Get the type of a fully-qualified name. Fail if it doesn not
213213 ||| resolve uniquely.
@@ -220,7 +220,7 @@ namespace Tactics
220220 ||| Find the reflected representation of all datatypes whose names
221221 ||| are overloadings of some name.
222222 lookupDatatype : TTName -> Elab (List Datatype)
223− lookupDatatype n = prim__LookupDatatype n
223+ lookupDatatype n = Prim__LookupDatatype n
224224
225225 ||| Find the reflected representation of a datatype, given its
226226 ||| fully-qualified name. Fail if the name does not uniquely resolve
@@ -234,7 +234,7 @@ namespace Tactics
234234
235235 ||| Get the argument specification for each overloading of a name.
236236 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
237− lookupArgs n = prim__LookupArgs n
237+ lookupArgs n = Prim__LookupArgs n
238238
239239 ||| Get the argument specification for a name. Fail if the name does
240240 ||| not uniquely resolve.
@@ -249,7 +249,7 @@ namespace Tactics
249249 ||| @ env the environment within which to check the type
250250 ||| @ tm the term to check
251251 check : (env : List (TTName, Binder TT)) -> (tm : Raw) -> Elab (TT, TT)
252− check env tm = prim__Check env tm
252+ check env tm = Prim__Check env tm
253253
254254
255255 ||| Generate a unique name based on some hint.
@@ -257,16 +257,16 @@ namespace Tactics
257257 ||| **NB**: the generated name is unique _for this run of the
258258 ||| elaborator_. Do not assume that they are globally unique.
259259 gensym : (hint : String) -> Elab TTName
260− gensym hint = prim__Gensym hint
260+ gensym hint = Prim__Gensym hint
261261
262262 ||| Substitute a guess into a hole.
263263 solve : Elab ()
264− solve = prim__Solve
264+ solve = Prim__Solve
265265
266266 ||| Place a term into a hole, unifying its type. Fails if the focus
267267 ||| is not a hole.
268268 fill : Raw -> Elab ()
269− fill tm = prim__Fill tm
269+ fill tm = Prim__Fill tm
270270
271271 ||| Attempt to apply an operator to fill the current hole,
272272 ||| potentially solving arguments by unification.
@@ -283,7 +283,7 @@ namespace Tactics
283283 ||| where the Boolean states whether or not to attempt to solve
284284 ||| the argument by unification.
285285 apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
286− apply tm argSpec = map snd <$> prim__Apply tm argSpec
286+ apply tm argSpec = map snd <$> Prim__Apply tm argSpec
287287
288288 ||| Attempt to apply an operator to fill the current hole,
289289 ||| potentially solving arguments by matching.
@@ -301,19 +301,19 @@ namespace Tactics
301301 ||| the argument by matching.
302302
303303 matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
304− matchApply tm argSpec = map snd <$> prim__Apply tm argSpec
304+ matchApply tm argSpec = map snd <$> Prim__Apply tm argSpec
305305
306306 ||| Move the focus to the specified hole. Fails if the hole does not
307307 ||| exist.
308308 |||
309309 ||| @ hole the hole to focus on
310310 focus : (hole : TTName) -> Elab ()
311− focus hole = prim__Focus hole
311+ focus hole = Prim__Focus hole
312312
313313 ||| Send the currently-focused hole to the end of the hole queue and
314314 ||| focus on the next hole.
315315 unfocus : TTName -> Elab ()
316− unfocus hole = prim__Unfocus hole
316+ unfocus hole = Prim__Unfocus hole
317317
318318 ||| Convert a hole to make it suitable for bindings - that is,
319319 ||| transform it such that it has the form `?h : t . h` as opposed to
@@ -324,7 +324,7 @@ namespace Tactics
324324 ||| sense. This tactic creates a new hole of the proper form, and
325325 ||| points the old hole at it.
326326 attack : Elab ()
327− attack = prim__Attack
327+ attack = Prim__Attack
328328
329329 ||| Introduce a new hole with a specified name and type.
330330 |||
@@ -332,7 +332,7 @@ namespace Tactics
332332 ||| will be immediately after it in the hole queue. Because this
333333 ||| tactic introduces a new binding, you may need to `attack` first.
334334 claim : TTName -> Raw -> Elab ()
335− claim n ty = prim__Claim n ty
335+ claim n ty = Prim__Claim n ty
336336
337337 ||| Introduce a lambda binding around the current hole and focus on
338338 ||| the body. Requires that the hole be in binding form (use
@@ -340,7 +340,7 @@ namespace Tactics
340340 |||
341341 ||| @ n the name to use for the argument
342342 intro : (n : TTName) -> Elab ()
343− intro n = prim__Intro (Just n)
343+ intro n = Prim__Intro (Just n)
344344
345345 ||| Introduce a lambda binding around the current hole and focus on
346346 ||| the body, using the name provided by the type of the
@@ -349,7 +349,7 @@ namespace Tactics
349349 ||| Requires that the hole be immediately under its binder (use
350350 ||| `attack` if it might not be).
351351 intro' : Elab ()
352− intro' = prim__Intro Nothing
352+ intro' = Prim__Intro Nothing
353353
354354 ||| Introduce a dependent function type binding into the current hole,
355355 ||| and focus on the body.
@@ -357,18 +357,18 @@ namespace Tactics
357357 ||| Requires that the hole be immediately under its binder (use
358358 ||| `attack` if it might not be).
359359 forall : TTName -> Raw -> Elab ()
360− forall n ty = prim__Forall n ty
360+ forall n ty = Prim__Forall n ty
361361
362362 ||| Convert a hole into a pattern variable.
363363 patvar : TTName -> Elab ()
364− patvar n = prim__PatVar n
364+ patvar n = Prim__PatVar n
365365
366366 ||| Introduce a new pattern binding.
367367 |||
368368 ||| Requires that the hole be immediately under its binder (use
369369 ||| `attack` if it might not be).
370370 patbind : TTName -> Elab ()
371− patbind n = prim__PatBind n
371+ patbind n = Prim__PatBind n
372372
373373 ||| Introduce a new let binding.
374374 |||
@@ -379,24 +379,24 @@ namespace Tactics
379379 ||| @ ty the type of the term to be let-bound
380380 ||| @ tm the term to be bound
381381 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
382− letbind n ty tm = prim__LetBind n ty tm
382+ letbind n ty tm = Prim__LetBind n ty tm
383383
384384 ||| Normalise the goal.
385385 compute : Elab ()
386− compute = prim__Compute
386+ compute = Prim__Compute
387387
388388 ||| Normalise a term in some lexical environment
389389 |||
390390 ||| @ env the environment in which to compute (get one of these from `getEnv`)
391391 ||| @ term the term to normalise
392392 normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
393− normalise env term = prim__Normalise env term
393+ normalise env term = Prim__Normalise env term
394394
395395 ||| Reduce a closed term to weak-head normal form
396396 |||
397397 ||| @ term the term to reduce
398398 whnf : (term : TT) -> Elab TT
399− whnf term = prim__Whnf term
399+ whnf term = Prim__Whnf term
400400
401401 ||| Check that two terms are convertable in the current context and
402402 ||| in some environment.
@@ -405,7 +405,7 @@ namespace Tactics
405405 ||| @ term1 the first term to convert
406406 ||| @ term2 the second term to convert
407407 convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab ()
408− convertsInEnv env term1 term2 = prim__Converts env term1 term2
408+ convertsInEnv env term1 term2 = Prim__Converts env term1 term2
409409
410410 ||| Check that two terms are convertable in the current context and environment
411411 |||
@@ -416,7 +416,7 @@ namespace Tactics
416416
417417 ||| Find the source context for the elaboration script
418418 getSourceLocation : Elab SourceLocation
419− getSourceLocation = prim__SourceLocation
419+ getSourceLocation = Prim__SourceLocation
420420
421421 ||| Attempt to solve the current goal with the source code location
422422 sourceLocation : Elab ()
@@ -430,7 +430,7 @@ namespace Tactics
430430 ||| The namespace is represented as a reverse-order list of strings,
431431 ||| just as in the representation of names.
432432 currentNamespace : Elab (List String)
433− currentNamespace = prim__Namespace
433+ currentNamespace = Prim__Namespace
434434
435435 ||| Attempt to rewrite the goal using an equality.
436436 |||
@@ -443,48 +443,48 @@ namespace Tactics
443443 ||| requires that the hole be immediately under its binder (use
444444 ||| `attack` if it might not be).
445445 rewriteWith : Raw -> Elab ()
446− rewriteWith rule = prim__Rewrite rule
446+ rewriteWith rule = Prim__Rewrite rule
447447
448448 ||| Add a type declaration to the global context.
449449 declareType : TyDecl -> Elab ()
450− declareType decl = prim__DeclareType decl
450+ declareType decl = Prim__DeclareType decl
451451
452452 ||| Define a function in the global context. The function must have
453453 ||| already been declared, either in ordinary Idris code or using
454454 ||| `declareType`.
455455 defineFunction : FunDefn -> Elab ()
456− defineFunction defun = prim__DefineFunction defun
456+ defineFunction defun = Prim__DefineFunction defun
457457
458458 ||| Register a new instance for type class resolution.
459459 |||
460460 ||| @ className the name of the class for which an instance is being registered
461461 ||| @ instName the name of the definition to use in instance search
462462 addInstance : (className, instName : TTName) -> Elab ()
463− addInstance className instName = prim__AddInstance className instName
463+ addInstance className instName = Prim__AddInstance className instName
464464
465465 ||| Determine whether a name denotes a class.
466466 |||
467467 ||| @ name a name that might denote a class.
468468 isTCName : (name : TTName) -> Elab Bool
469− isTCName name = prim__IsTCName name
469+ isTCName name = Prim__IsTCName name
470470
471471 ||| Attempt to solve the current goal with a type class dictionary
472472 |||
473473 ||| @ fn the name of the definition being elaborated (to prevent Idris
474474 ||| from looping)
475475 resolveTC : (fn : TTName) -> Elab ()
476− resolveTC fn = prim__ResolveTC fn
476+ resolveTC fn = Prim__ResolveTC fn
477477
478478 ||| Use Idris's internal proof search.
479479 search : Elab ()
480− search = prim__Search 100 []
480+ search = Prim__Search 100 []
481481
482482 ||| Use Idris's internal proof search, with more control.
483483 |||
484484 ||| @ depth the search depth
485485 ||| @ hints additional names to try
486486 search' : (depth : Int) -> (hints : List TTName) -> Elab ()
487− search' depth hints = prim__Search depth hints
487+ search' depth hints = Prim__Search depth hints
488488
489489 ||| Look up the declared fixity for an operator.
490490 |||
@@ -493,14 +493,14 @@ namespace Tactics
493493 |||
494494 ||| @ operator the operator string to look up
495495 operatorFixity : (operator : String) -> Elab Fixity
496− operatorFixity operator = prim__Fixity operator
496+ operatorFixity operator = Prim__Fixity operator
497497
498498 ||| Halt elaboration, dumping the internal state for inspection.
499499 |||
500500 ||| This is intended for elaboration script developers, not for
501501 ||| end-users. Use `fail` for final scripts.
502502 debug : Elab a
503− debug = prim__Debug []
503+ debug = Prim__Debug []
504504
505505 ||| Halt elaboration, dumping the internal state and displaying a
506506 ||| message.
@@ -510,17 +510,17 @@ namespace Tactics
510510 |||
511511 ||| @ msg the message to display
512512 debugMessage : (msg : List ErrorReportPart) -> Elab a
513− debugMessage msg = prim__Debug msg
513+ debugMessage msg = Prim__Debug msg
514514
515515 ||| Create a new top-level metavariable to solve the current hole.
516516 |||
517517 ||| @ name the name for the top-level variable
518518 metavar : (name : TTName) -> Elab ()
519− metavar name = prim__Metavar name
519+ metavar name = Prim__Metavar name
520520
521521 ||| Recursively invoke the reflected elaborator with some goal.
522522 |||
523523 ||| The result is the final term and its type.
524524 runElab : Raw -> Elab () -> Elab (TT, TT)
525− runElab goal script = prim__RecursiveElab goal script
525+ runElab goal script = Prim__RecursiveElab goal script
526526
libs/prelude/Prelude/Nat.idr+10−10
@@ -216,45 +216,45 @@ instance Cast Integer Nat where
216216
217217||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
218218record Multiplicative where
219− constructor getMultiplicative
219+ constructor GetMultiplicative
220220 _ : Nat
221221
222222||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)
223223record Additive where
224− constructor getAdditive
224+ constructor GetAdditive
225225 _ : Nat
226226
227227instance Semigroup Multiplicative where
228− (<+>) left right = getMultiplicative $ left' * right'
228+ (<+>) left right = GetMultiplicative $ left' * right'
229229 where
230230 left' : Nat
231231 left' =
232232 case left of
233− getMultiplicative m => m
233+ GetMultiplicative m => m
234234
235235 right' : Nat
236236 right' =
237237 case right of
238− getMultiplicative m => m
238+ GetMultiplicative m => m
239239
240240instance Semigroup Additive where
241− left <+> right = getAdditive $ left' + right'
241+ left <+> right = GetAdditive $ left' + right'
242242 where
243243 left' : Nat
244244 left' =
245245 case left of
246− getAdditive m => m
246+ GetAdditive m => m
247247
248248 right' : Nat
249249 right' =
250250 case right of
251− getAdditive m => m
251+ GetAdditive m => m
252252
253253instance Monoid Multiplicative where
254− neutral = getMultiplicative $ S Z
254+ neutral = GetMultiplicative $ S Z
255255
256256instance Monoid Additive where
257− neutral = getAdditive Z
257+ neutral = GetAdditive Z
258258
259259||| Casts negative `Ints` to 0.
260260instance Cast Int Nat where
src/Idris/Elab/Term.hs+43−43
@@ -1802,10 +1802,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
18021802 -- step, the output is the (reflected) term returned.
18031803 runTacTm :: Term -> ElabD Term
18041804 runTacTm (unApply -> tac@(P _ n _, args))
1805− | n == tacN "prim__Solve", [] <- args
1805+ | n == tacN "Prim__Solve", [] <- args
18061806 = do solve
18071807 returnUnit
1808− | n == tacN "prim__Goal", [] <- args
1808+ | n == tacN "Prim__Goal", [] <- args
18091809 = do hs <- get_holes
18101810 case hs of
18111811 (h : _) -> do t <- goal
@@ -1815,11 +1815,11 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
18151815 [] -> lift . tfail . Msg $
18161816 "Elaboration is complete. There are no goals."
18171817
1818− | n == tacN "prim__Holes", [] <- args
1818+ | n == tacN "Prim__Holes", [] <- args
18191819 = do hs <- get_holes
18201820 fmap fst . checkClosed $
18211821 mkList (Var $ reflm "TTName") (map reflectName hs)
1822− | n == tacN "prim__Guess", [] <- args
1822+ | n == tacN "Prim__Guess", [] <- args
18231823 = do ok <- is_guess
18241824 if ok
18251825 then do guess <- fmap forget get_guess
@@ -1830,7 +1830,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
18301830 else fmap fst . checkClosed $
18311831 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
18321832 (Var (reflm "TT"))
1833− | n == tacN "prim__LookupTy", [n] <- args
1833+ | n == tacN "Prim__LookupTy", [n] <- args
18341834 = do n' <- reifyTTName n
18351835 ctxt <- get_context
18361836 let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
@@ -1852,14 +1852,14 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
18521852 , raw_apply (Var pairTy) [ Var (reflm "NameType")
18531853 , Var (reflm "TT")]])
18541854 defs
1855− | n == tacN "prim__LookupDatatype", [name] <- args
1855+ | n == tacN "Prim__LookupDatatype", [name] <- args
18561856 = do n' <- reifyTTName name
18571857 datatypes <- get_datatypes
18581858 ctxt <- get_context
18591859 fmap fst . checkClosed $
18601860 rawList (Var (tacN "Datatype"))
18611861 (map reflectDatatype (buildDatatypes ist n'))
1862− | n == tacN "prim__LookupArgs", [name] <- args
1862+ | n == tacN "Prim__LookupArgs", [name] <- args
18631863 = do n' <- reifyTTName name
18641864 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
18651865 listFunArg = RApp listTy (Var (tacN "FunArg"))
@@ -1883,39 +1883,39 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
18831883 (Var (tacN "FunArg"))
18841884 , Var (reflm "Raw")]])
18851885 out
1886− | n == tacN "prim__SourceLocation", [] <- args
1886+ | n == tacN "Prim__SourceLocation", [] <- args
18871887 = fmap fst . checkClosed $
18881888 reflectFC fc
1889− | n == tacN "prim__Namespace", [] <- args
1889+ | n == tacN "Prim__Namespace", [] <- args
18901890 = fmap fst . checkClosed $
18911891 rawList (RConstant StrType) (map (RConstant . Str) ns)
1892− | n == tacN "prim__Env", [] <- args
1892+ | n == tacN "Prim__Env", [] <- args
18931893 = do env <- get_env
18941894 fmap fst . checkClosed $ reflectEnv env
1895− | n == tacN "prim__Fail", [_a, errs] <- args
1895+ | n == tacN "Prim__Fail", [_a, errs] <- args
18961896 = do errs' <- eval errs
18971897 parts <- reifyReportParts errs'
18981898 lift . tfail $ ReflectionError [parts] (Msg "")
1899− | n == tacN "prim__PureElab", [_a, tm] <- args
1899+ | n == tacN "Prim__PureElab", [_a, tm] <- args
19001900 = return tm
1901− | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args
1901+ | n == tacN "Prim__BindElab", [_a, _b, first, andThen] <- args
19021902 = do first' <- eval first
19031903 res <- eval =<< runTacTm first'
19041904 next <- eval (App Complete andThen res)
19051905 runTacTm next
1906− | n == tacN "prim__Try", [_a, first, alt] <- args
1906+ | n == tacN "Prim__Try", [_a, first, alt] <- args
19071907 = do first' <- eval first
19081908 alt' <- eval alt
19091909 try' (runTacTm first') (runTacTm alt') True
1910− | n == tacN "prim__Fill", [raw] <- args
1910+ | n == tacN "Prim__Fill", [raw] <- args
19111911 = do raw' <- reifyRaw =<< eval raw
19121912 apply raw' []
19131913 returnUnit
1914− | n == tacN "prim__Apply" || n == tacN "prim__MatchApply"
1914+ | n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"
19151915 , [raw, argSpec] <- args
19161916 = do raw' <- reifyRaw =<< eval raw
19171917 argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec
1918− let op = if n == tacN "prim__Apply"
1918+ let op = if n == tacN "Prim__Apply"
19191919 then apply
19201920 else match_apply
19211921 ns <- op raw' argSpec'
@@ -1925,19 +1925,19 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
19251925 (reflectName n1, reflectName n2)
19261926 | (n1, n2) <- ns
19271927 ]
1928− | n == tacN "prim__Gensym", [hint] <- args
1928+ | n == tacN "Prim__Gensym", [hint] <- args
19291929 = do hintStr <- eval hint
19301930 case hintStr of
19311931 Constant (Str h) -> do
19321932 n <- getNameFrom (sMN 0 h)
19331933 fmap fst $ get_type_val (reflectName n)
19341934 _ -> fail "no hint"
1935− | n == tacN "prim__Claim", [n, ty] <- args
1935+ | n == tacN "Prim__Claim", [n, ty] <- args
19361936 = do n' <- reifyTTName n
19371937 ty' <- reifyRaw ty
19381938 claim n' ty'
19391939 returnUnit
1940− | n == tacN "prim__Check", [env', raw] <- args
1940+ | n == tacN "Prim__Check", [env', raw] <- args
19411941 = do env <- reifyEnv env'
19421942 raw' <- reifyRaw =<< eval raw
19431943 ctxt <- get_context
@@ -1945,68 +1945,68 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
19451945 fmap fst . checkClosed $
19461946 rawPair (Var (reflm "TT"), Var (reflm "TT"))
19471947 (reflect tm, reflect ty)
1948− | n == tacN "prim__Attack", [] <- args
1948+ | n == tacN "Prim__Attack", [] <- args
19491949 = do attack
19501950 returnUnit
1951− | n == tacN "prim__Rewrite", [rule] <- args
1951+ | n == tacN "Prim__Rewrite", [rule] <- args
19521952 = do r <- reifyRaw rule
19531953 rewrite r
19541954 returnUnit
1955− | n == tacN "prim__Focus", [what] <- args
1955+ | n == tacN "Prim__Focus", [what] <- args
19561956 = do n' <- reifyTTName what
19571957 hs <- get_holes
19581958 if elem n' hs
19591959 then focus n' >> returnUnit
19601960 else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
1961− | n == tacN "prim__Unfocus", [what] <- args
1961+ | n == tacN "Prim__Unfocus", [what] <- args
19621962 = do n' <- reifyTTName what
19631963 movelast n'
19641964 returnUnit
1965− | n == tacN "prim__Intro", [mn] <- args
1965+ | n == tacN "Prim__Intro", [mn] <- args
19661966 = do n <- case fromTTMaybe mn of
19671967 Nothing -> return Nothing
19681968 Just name -> fmap Just $ reifyTTName name
19691969 intro n
19701970 returnUnit
1971− | n == tacN "prim__Forall", [n, ty] <- args
1971+ | n == tacN "Prim__Forall", [n, ty] <- args
19721972 = do n' <- reifyTTName n
19731973 ty' <- reifyRaw ty
19741974 forall n' Nothing ty'
19751975 returnUnit
1976− | n == tacN "prim__PatVar", [n] <- args
1976+ | n == tacN "Prim__PatVar", [n] <- args
19771977 = do n' <- reifyTTName n
19781978 patvar' n'
19791979 returnUnit
1980− | n == tacN "prim__PatBind", [n] <- args
1980+ | n == tacN "Prim__PatBind", [n] <- args
19811981 = do n' <- reifyTTName n
19821982 patbind n'
19831983 returnUnit
1984− | n == tacN "prim__LetBind", [n, ty, tm] <- args
1984+ | n == tacN "Prim__LetBind", [n, ty, tm] <- args
19851985 = do n' <- reifyTTName n
19861986 ty' <- reifyRaw ty
19871987 tm' <- reifyRaw tm
19881988 letbind n' ty' tm'
19891989 returnUnit
1990− | n == tacN "prim__Compute", [] <- args
1990+ | n == tacN "Prim__Compute", [] <- args
19911991 = do compute ; returnUnit
1992− | n == tacN "prim__Normalise", [env, tm] <- args
1992+ | n == tacN "Prim__Normalise", [env, tm] <- args
19931993 = do env' <- reifyEnv env
19941994 tm' <- reifyTT tm
19951995 ctxt <- get_context
19961996 let out = normaliseAll ctxt env' (finalise tm')
19971997 fmap fst . checkClosed $ reflect out
1998− | n == tacN "prim__Whnf", [tm] <- args
1998+ | n == tacN "Prim__Whnf", [tm] <- args
19991999 = do tm' <- reifyTT tm
20002000 ctxt <- get_context
20012001 fmap fst . checkClosed . reflect $ whnf ctxt tm'
2002− | n == tacN "prim__Converts", [env, tm1, tm2] <- args
2002+ | n == tacN "Prim__Converts", [env, tm1, tm2] <- args
20032003 = do env' <- reifyEnv env
20042004 tm1' <- reifyTT tm1
20052005 tm2' <- reifyTT tm2
20062006 ctxt <- get_context
20072007 lift $ converts ctxt env' tm1' tm2'
20082008 returnUnit
2009− | n == tacN "prim__DeclareType", [decl] <- args
2009+ | n == tacN "Prim__DeclareType", [decl] <- args
20102010 = do (RDeclare n args res) <- reifyTyDecl decl
20112011 ctxt <- get_context
20122012 let mkPi arg res = RBind (argName arg)
@@ -2029,27 +2029,27 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20292029 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
20302030 new_tyDecls e }
20312031 returnUnit
2032− | n == tacN "prim__DefineFunction", [decl] <- args
2032+ | n == tacN "Prim__DefineFunction", [decl] <- args
20332033 = do defn <- reifyFunDefn decl
20342034 defineFunction defn
20352035 returnUnit
2036− | n == tacN "prim__AddInstance", [cls, inst] <- args
2036+ | n == tacN "Prim__AddInstance", [cls, inst] <- args
20372037 = do className <- reifyTTName cls
20382038 instName <- reifyTTName inst
20392039 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
20402040 new_tyDecls e}
20412041 returnUnit
2042− | n == tacN "prim__IsTCName", [n] <- args
2042+ | n == tacN "Prim__IsTCName", [n] <- args
20432043 = do n' <- reifyTTName n
20442044 case lookupCtxtExact n' (idris_classes ist) of
20452045 Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
20462046 Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
2047− | n == tacN "prim__ResolveTC", [fn] <- args
2047+ | n == tacN "Prim__ResolveTC", [fn] <- args
20482048 = do g <- goal
20492049 fn <- reifyTTName fn
20502050 resolveTC' False True 100 g fn ist
20512051 returnUnit
2052− | n == tacN "prim__Search", [depth, hints] <- args
2052+ | n == tacN "Prim__Search", [depth, hints] <- args
20532053 = do d <- eval depth
20542054 hints' <- eval hints
20552055 case (d, unList hints') of
@@ -2062,7 +2062,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20622062 (Constant (I _), Nothing ) ->
20632063 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
20642064 (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d
2065− | n == tacN "prim__RecursiveElab", [goal, script] <- args
2065+ | n == tacN "Prim__RecursiveElab", [goal, script] <- args
20662066 = do goal' <- reifyRaw goal
20672067 ctxt <- get_context
20682068 script <- eval script
@@ -2093,7 +2093,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20932093 fmap fst . checkClosed $
20942094 rawPair (Var $ reflm "TT", Var $ reflm "TT")
20952095 (tm', ty')
2096− | n == tacN "prim__Metavar", [n] <- args
2096+ | n == tacN "Prim__Metavar", [n] <- args
20972097 = do n' <- reifyTTName n
20982098 ctxt <- get_context
20992099 ptm <- get_term
@@ -2104,7 +2104,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
21042104 defer unique_used mvn
21052105 solve
21062106 returnUnit
2107− | n == tacN "prim__Fixity", [op'] <- args
2107+ | n == tacN "Prim__Fixity", [op'] <- args
21082108 = do opTm <- eval op'
21092109 case opTm of
21102110 Constant (Str op) ->
@@ -2118,7 +2118,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
21182118 [f] -> fmap fst . checkClosed $ reflectFixity f
21192119 many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many
21202120 _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm
2121− | n == tacN "prim__Debug", [ty, msg] <- args
2121+ | n == tacN "Prim__Debug", [ty, msg] <- args
21222122 = do msg' <- eval msg
21232123 parts <- reifyReportParts msg
21242124 debugElaborator parts