git.iko.soy/Idris-dev
on master help sign in
Tidy up name warnings in Prelude
53f4651Edwin Brady
libs/base/Control/Catchable.idr+3−3
compare with master
unifiedsplit
@@ -19,11 +19,11 @@ instance Catchable (Either a) a where
19 throw x = Left x
19 throw x = Left x
20
20
21instance Catchable (IOExcept err) err where
21instance Catchable (IOExcept err) err where
22− catch (ioM prog) h = ioM (do p' <- prog
22+ catch (IOM prog) h = IOM (do p' <- prog
23 case p' of
23 case p' of
24− Left e => let ioM he = h e in he
24+ Left e => let IOM he = h e in he
25 Right val => return (Right val))
25 Right val => return (Right val))
26− throw x = ioM (return (Left x))
26+ throw x = IOM (return (Left x))
27
27
28instance Catchable List () where
28instance Catchable List () where
29 catch [] h = h ()
29 catch [] h = h ()
libs/base/Control/IOExcept.idr+9−9
@@ -3,32 +3,32 @@ module Control.IOExcept
3-- An IO monad with exception handling
3-- An IO monad with exception handling
4
4
5data IOExcept : Type -> Type -> Type where
5data IOExcept : Type -> Type -> Type where
6− ioM : IO (Either err a) -> IOExcept err a
6+ IOM : IO (Either err a) -> IOExcept err a
7
7
8instance Functor (IOExcept e) where
8instance Functor (IOExcept e) where
9− map f (ioM fn) = ioM (map (map f) fn)
9+ map f (IOM fn) = IOM (map (map f) fn)
10
10
11instance Applicative (IOExcept e) where
11instance Applicative (IOExcept e) where
12− pure x = ioM (pure (pure x))
12+ pure x = IOM (pure (pure x))
13− (ioM f) <*> (ioM a) = ioM (do f' <- f; a' <- a
13+ (IOM f) <*> (IOM a) = IOM (do f' <- f; a' <- a
14 return (f' <*> a'))
14 return (f' <*> a'))
15
15
16instance Monad (IOExcept e) where
16instance Monad (IOExcept e) where
17− (ioM x) >>= k = ioM (do x' <- x;
17+ (IOM x) >>= k = IOM (do x' <- x;
18 case x' of
18 case x' of
19− Right a => let (ioM ka) = k a in
19+ Right a => let (IOM ka) = k a in
20 ka
20 ka
21 Left err => return (Left err))
21 Left err => return (Left err))
22
22
23ioe_lift : IO a -> IOExcept err a
23ioe_lift : IO a -> IOExcept err a
24−ioe_lift op = ioM (do op' <- op
24+ioe_lift op = IOM (do op' <- op
25 return (Right op'))
25 return (Right op'))
26
26
27ioe_fail : err -> IOExcept err a
27ioe_fail : err -> IOExcept err a
28−ioe_fail e = ioM (return (Left e))
28+ioe_fail e = IOM (return (Left e))
29
29
30ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b
30ioe_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
32 case act' of
32 case act' of
33 Left e => err e
33 Left e => err e
34 Right v => ok v
34 Right v => ok v
libs/effects/Effect/Exception.idr+1−1
@@ -18,7 +18,7 @@ instance Show a => Handler (Exception a) IO where
18 believe_me (exit 1)
18 believe_me (exit 1)
19
19
20instance Handler (Exception a) (IOExcept a) where
20instance Handler (Exception a) (IOExcept a) where
21− handle _ (Raise e) k = ioM (return (Left e))
21+ handle _ (Raise e) k = IOM (return (Left e))
22
22
23instance Handler (Exception a) (Either a) where
23instance Handler (Exception a) (Either a) where
24 handle _ (Raise e) k = Left e
24 handle _ (Raise e) k = Left e
libs/prelude/IO.idr+3−3
@@ -8,7 +8,7 @@ import Prelude.List
8||| Idris's primitive IO, for building abstractions on top of
8||| Idris's primitive IO, for building abstractions on top of
9abstract
9abstract
10data PrimIO : Type -> Type where
10data PrimIO : Type -> Type where
11− prim__IO : a -> PrimIO a
11+ Prim__IO : a -> PrimIO a
12
12
13||| A token representing the world, for use in `IO`
13||| A token representing the world, for use in `IO`
14abstract data World = TheWorld prim__WorldType
14abstract data World = TheWorld prim__WorldType
@@ -94,14 +94,14 @@ foreign ffi fname ty {fty} = foreign_prim ffi fname fty []
94
94
95abstract
95abstract
96prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
96prim_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
98
98
99unsafePerformPrimIO : PrimIO a -> a
99unsafePerformPrimIO : PrimIO a -> a
100-- compiled as primitive
100-- compiled as primitive
101
101
102abstract
102abstract
103prim_io_return : a -> PrimIO a
103prim_io_return : a -> PrimIO a
104−prim_io_return x = prim__IO x
104+prim_io_return x = Prim__IO x
105
105
106abstract
106abstract
107io_bind : IO' l a -> (a -> IO' l b) -> IO' l b
107io_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
104abstract
104abstract
105data Elab : Type -> Type where
105data Elab : Type -> Type where
106 -- obligatory control stuff
106 -- obligatory control stuff
107− prim__PureElab : a -> Elab a
107+ Prim__PureElab : a -> Elab a
108− prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b
108+ Prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b
109
109
110− prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a
110+ Prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a
111− prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a
111+ Prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a
112
112
113− prim__Env : Elab (List (TTName, Binder TT))
113+ Prim__Env : Elab (List (TTName, Binder TT))
114− prim__Goal : Elab (TTName, TT)
114+ Prim__Goal : Elab (TTName, TT)
115− prim__Holes : Elab (List TTName)
115+ Prim__Holes : Elab (List TTName)
116− prim__Guess : Elab (Maybe TT)
116+ Prim__Guess : Elab (Maybe TT)
117− prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
117+ Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
118− prim__LookupDatatype : TTName -> Elab (List Datatype)
118+ Prim__LookupDatatype : TTName -> Elab (List Datatype)
119− prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
119+ Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
120
120
121− prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)
121+ Prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)
122
122
123− prim__SourceLocation : Elab SourceLocation
123+ Prim__SourceLocation : Elab SourceLocation
124− prim__Namespace : Elab (List String)
124+ Prim__Namespace : Elab (List String)
125
125
126− prim__Gensym : String -> Elab TTName
126+ Prim__Gensym : String -> Elab TTName
127
127
128− prim__Solve : Elab ()
128+ Prim__Solve : Elab ()
129− prim__Fill : Raw -> Elab ()
129+ Prim__Fill : Raw -> Elab ()
130− prim__Apply : Raw -> List Bool -> Elab (List (TTName, TTName))
130+ Prim__Apply : Raw -> List Bool -> Elab (List (TTName, TTName))
131− prim__MatchApply : Raw -> List Bool -> Elab (List (TTName, TTName))
131+ Prim__MatchApply : Raw -> List Bool -> Elab (List (TTName, TTName))
132− prim__Focus : TTName -> Elab ()
132+ Prim__Focus : TTName -> Elab ()
133− prim__Unfocus : TTName -> Elab ()
133+ Prim__Unfocus : TTName -> Elab ()
134− prim__Attack : Elab ()
134+ Prim__Attack : Elab ()
135
135
136− prim__Rewrite : Raw -> Elab ()
136+ Prim__Rewrite : Raw -> Elab ()
137
137
138− prim__Claim : TTName -> Raw -> Elab ()
138+ Prim__Claim : TTName -> Raw -> Elab ()
139− prim__Intro : Maybe TTName -> Elab ()
139+ Prim__Intro : Maybe TTName -> Elab ()
140− prim__Forall : TTName -> Raw -> Elab ()
140+ Prim__Forall : TTName -> Raw -> Elab ()
141− prim__PatVar : TTName -> Elab ()
141+ Prim__PatVar : TTName -> Elab ()
142− prim__PatBind : TTName -> Elab ()
142+ Prim__PatBind : TTName -> Elab ()
143− prim__LetBind : TTName -> Raw -> Raw -> Elab ()
143+ Prim__LetBind : TTName -> Raw -> Raw -> Elab ()
144
144
145− prim__Compute : Elab ()
145+ Prim__Compute : Elab ()
146− prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
146+ Prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
147− prim__Whnf : TT -> Elab TT
147+ Prim__Whnf : TT -> Elab TT
148− prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()
148+ Prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()
149
149
150− prim__DeclareType : TyDecl -> Elab ()
150+ Prim__DeclareType : TyDecl -> Elab ()
151− prim__DefineFunction : FunDefn -> Elab ()
151+ Prim__DefineFunction : FunDefn -> Elab ()
152− prim__AddInstance : TTName -> TTName -> Elab ()
152+ Prim__AddInstance : TTName -> TTName -> Elab ()
153− prim__IsTCName : TTName -> Elab Bool
153+ Prim__IsTCName : TTName -> Elab Bool
154
154
155− prim__ResolveTC : TTName -> Elab ()
155+ Prim__ResolveTC : TTName -> Elab ()
156− prim__Search : Int -> List TTName -> Elab ()
156+ Prim__Search : Int -> List TTName -> Elab ()
157− prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)
157+ Prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)
158
158
159− prim__Fixity : String -> Elab Fixity
159+ Prim__Fixity : String -> Elab Fixity
160
160
161− prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a
161+ Prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a
162− prim__Metavar : TTName -> Elab ()
162+ Prim__Metavar : TTName -> Elab ()
163
163
164-------------
164-------------
165-- Public API
165-- Public API
@@ -167,47 +167,47 @@ data Elab : Type -> Type where
167%access public
167%access public
168namespace Tactics
168namespace Tactics
169 instance Functor Elab where
169 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))
171
171
172 instance Applicative Elab where
172 instance Applicative Elab where
173− pure x = prim__PureElab x
173+ pure x = Prim__PureElab x
174− f <*> x = prim__BindElab f $ \g =>
174+ f <*> x = Prim__BindElab f $ \g =>
175− prim__BindElab x $ \y =>
175+ Prim__BindElab x $ \y =>
176− prim__PureElab $ g y
176+ Prim__PureElab $ g y
177
177
178 ||| The Alternative instance on Elab represents left-biased error
178 ||| The Alternative instance on Elab represents left-biased error
179 ||| handling. In other words, `t <|> t'` will run `t`, and if it
179 ||| handling. In other words, `t <|> t'` will run `t`, and if it
180 ||| fails, roll back the elaboration state and run `t'`.
180 ||| fails, roll back the elaboration state and run `t'`.
181 instance Alternative Elab where
181 instance Alternative Elab where
182− empty = prim__Fail [TextPart "empty"]
182+ empty = Prim__Fail [TextPart "empty"]
183− x <|> y = prim__Try x y
183+ x <|> y = Prim__Try x y
184
184
185 instance Monad Elab where
185 instance Monad Elab where
186− x >>= f = prim__BindElab x f
186+ x >>= f = Prim__BindElab x f
187
187
188 ||| Halt elaboration with an error
188 ||| Halt elaboration with an error
189 fail : List ErrorReportPart -> Elab a
189 fail : List ErrorReportPart -> Elab a
190− fail err = prim__Fail err
190+ fail err = Prim__Fail err
191
191
192 ||| Look up the lexical binding at the focused hole. Fails if no holes are present.
192 ||| Look up the lexical binding at the focused hole. Fails if no holes are present.
193 getEnv : Elab (List (TTName, Binder TT))
193 getEnv : Elab (List (TTName, Binder TT))
194− getEnv = prim__Env
194+ getEnv = Prim__Env
195
195
196 ||| Get the name and type of the focused hole. Fails if not holes are present.
196 ||| Get the name and type of the focused hole. Fails if not holes are present.
197 getGoal : Elab (TTName, TT)
197 getGoal : Elab (TTName, TT)
198− getGoal = prim__Goal
198+ getGoal = Prim__Goal
199
199
200 ||| Get the hole queue, in order.
200 ||| Get the hole queue, in order.
201 getHoles : Elab (List TTName)
201 getHoles : Elab (List TTName)
202− getHoles = prim__Holes
202+ getHoles = Prim__Holes
203
203
204 ||| If the current hole contains a guess, return it. Otherwise, fail.
204 ||| If the current hole contains a guess, return it. Otherwise, fail.
205 getGuess : Elab (Maybe TT)
205 getGuess : Elab (Maybe TT)
206− getGuess = prim__Guess
206+ getGuess = Prim__Guess
207
207
208 ||| Look up the types of every overloading of a name.
208 ||| Look up the types of every overloading of a name.
209 lookupTy : TTName -> Elab (List (TTName, NameType, TT))
209 lookupTy : TTName -> Elab (List (TTName, NameType, TT))
210− lookupTy n = prim__LookupTy n
210+ lookupTy n = Prim__LookupTy n
211
211
212 ||| Get the type of a fully-qualified name. Fail if it doesn not
212 ||| Get the type of a fully-qualified name. Fail if it doesn not
213 ||| resolve uniquely.
213 ||| resolve uniquely.
@@ -220,7 +220,7 @@ namespace Tactics
220 ||| Find the reflected representation of all datatypes whose names
220 ||| Find the reflected representation of all datatypes whose names
221 ||| are overloadings of some name.
221 ||| are overloadings of some name.
222 lookupDatatype : TTName -> Elab (List Datatype)
222 lookupDatatype : TTName -> Elab (List Datatype)
223− lookupDatatype n = prim__LookupDatatype n
223+ lookupDatatype n = Prim__LookupDatatype n
224
224
225 ||| Find the reflected representation of a datatype, given its
225 ||| Find the reflected representation of a datatype, given its
226 ||| fully-qualified name. Fail if the name does not uniquely resolve
226 ||| fully-qualified name. Fail if the name does not uniquely resolve
@@ -234,7 +234,7 @@ namespace Tactics
234
234
235 ||| Get the argument specification for each overloading of a name.
235 ||| Get the argument specification for each overloading of a name.
236 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
236 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
237− lookupArgs n = prim__LookupArgs n
237+ lookupArgs n = Prim__LookupArgs n
238
238
239 ||| Get the argument specification for a name. Fail if the name does
239 ||| Get the argument specification for a name. Fail if the name does
240 ||| not uniquely resolve.
240 ||| not uniquely resolve.
@@ -249,7 +249,7 @@ namespace Tactics
249 ||| @ env the environment within which to check the type
249 ||| @ env the environment within which to check the type
250 ||| @ tm the term to check
250 ||| @ tm the term to check
251 check : (env : List (TTName, Binder TT)) -> (tm : Raw) -> Elab (TT, TT)
251 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
253
253
254
254
255 ||| Generate a unique name based on some hint.
255 ||| Generate a unique name based on some hint.
@@ -257,16 +257,16 @@ namespace Tactics
257 ||| **NB**: the generated name is unique _for this run of the
257 ||| **NB**: the generated name is unique _for this run of the
258 ||| elaborator_. Do not assume that they are globally unique.
258 ||| elaborator_. Do not assume that they are globally unique.
259 gensym : (hint : String) -> Elab TTName
259 gensym : (hint : String) -> Elab TTName
260− gensym hint = prim__Gensym hint
260+ gensym hint = Prim__Gensym hint
261
261
262 ||| Substitute a guess into a hole.
262 ||| Substitute a guess into a hole.
263 solve : Elab ()
263 solve : Elab ()
264− solve = prim__Solve
264+ solve = Prim__Solve
265
265
266 ||| Place a term into a hole, unifying its type. Fails if the focus
266 ||| Place a term into a hole, unifying its type. Fails if the focus
267 ||| is not a hole.
267 ||| is not a hole.
268 fill : Raw -> Elab ()
268 fill : Raw -> Elab ()
269− fill tm = prim__Fill tm
269+ fill tm = Prim__Fill tm
270
270
271 ||| Attempt to apply an operator to fill the current hole,
271 ||| Attempt to apply an operator to fill the current hole,
272 ||| potentially solving arguments by unification.
272 ||| potentially solving arguments by unification.
@@ -283,7 +283,7 @@ namespace Tactics
283 ||| where the Boolean states whether or not to attempt to solve
283 ||| where the Boolean states whether or not to attempt to solve
284 ||| the argument by unification.
284 ||| the argument by unification.
285 apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
285 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
287
287
288 ||| Attempt to apply an operator to fill the current hole,
288 ||| Attempt to apply an operator to fill the current hole,
289 ||| potentially solving arguments by matching.
289 ||| potentially solving arguments by matching.
@@ -301,19 +301,19 @@ namespace Tactics
301 ||| the argument by matching.
301 ||| the argument by matching.
302
302
303 matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
303 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
305
305
306 ||| Move the focus to the specified hole. Fails if the hole does not
306 ||| Move the focus to the specified hole. Fails if the hole does not
307 ||| exist.
307 ||| exist.
308 |||
308 |||
309 ||| @ hole the hole to focus on
309 ||| @ hole the hole to focus on
310 focus : (hole : TTName) -> Elab ()
310 focus : (hole : TTName) -> Elab ()
311− focus hole = prim__Focus hole
311+ focus hole = Prim__Focus hole
312
312
313 ||| Send the currently-focused hole to the end of the hole queue and
313 ||| Send the currently-focused hole to the end of the hole queue and
314 ||| focus on the next hole.
314 ||| focus on the next hole.
315 unfocus : TTName -> Elab ()
315 unfocus : TTName -> Elab ()
316− unfocus hole = prim__Unfocus hole
316+ unfocus hole = Prim__Unfocus hole
317
317
318 ||| Convert a hole to make it suitable for bindings - that is,
318 ||| Convert a hole to make it suitable for bindings - that is,
319 ||| transform it such that it has the form `?h : t . h` as opposed to
319 ||| transform it such that it has the form `?h : t . h` as opposed to
@@ -324,7 +324,7 @@ namespace Tactics
324 ||| sense. This tactic creates a new hole of the proper form, and
324 ||| sense. This tactic creates a new hole of the proper form, and
325 ||| points the old hole at it.
325 ||| points the old hole at it.
326 attack : Elab ()
326 attack : Elab ()
327− attack = prim__Attack
327+ attack = Prim__Attack
328
328
329 ||| Introduce a new hole with a specified name and type.
329 ||| Introduce a new hole with a specified name and type.
330 |||
330 |||
@@ -332,7 +332,7 @@ namespace Tactics
332 ||| will be immediately after it in the hole queue. Because this
332 ||| will be immediately after it in the hole queue. Because this
333 ||| tactic introduces a new binding, you may need to `attack` first.
333 ||| tactic introduces a new binding, you may need to `attack` first.
334 claim : TTName -> Raw -> Elab ()
334 claim : TTName -> Raw -> Elab ()
335− claim n ty = prim__Claim n ty
335+ claim n ty = Prim__Claim n ty
336
336
337 ||| Introduce a lambda binding around the current hole and focus on
337 ||| Introduce a lambda binding around the current hole and focus on
338 ||| the body. Requires that the hole be in binding form (use
338 ||| the body. Requires that the hole be in binding form (use
@@ -340,7 +340,7 @@ namespace Tactics
340 |||
340 |||
341 ||| @ n the name to use for the argument
341 ||| @ n the name to use for the argument
342 intro : (n : TTName) -> Elab ()
342 intro : (n : TTName) -> Elab ()
343− intro n = prim__Intro (Just n)
343+ intro n = Prim__Intro (Just n)
344
344
345 ||| Introduce a lambda binding around the current hole and focus on
345 ||| Introduce a lambda binding around the current hole and focus on
346 ||| the body, using the name provided by the type of the
346 ||| the body, using the name provided by the type of the
@@ -349,7 +349,7 @@ namespace Tactics
349 ||| Requires that the hole be immediately under its binder (use
349 ||| Requires that the hole be immediately under its binder (use
350 ||| `attack` if it might not be).
350 ||| `attack` if it might not be).
351 intro' : Elab ()
351 intro' : Elab ()
352− intro' = prim__Intro Nothing
352+ intro' = Prim__Intro Nothing
353
353
354 ||| Introduce a dependent function type binding into the current hole,
354 ||| Introduce a dependent function type binding into the current hole,
355 ||| and focus on the body.
355 ||| and focus on the body.
@@ -357,18 +357,18 @@ namespace Tactics
357 ||| Requires that the hole be immediately under its binder (use
357 ||| Requires that the hole be immediately under its binder (use
358 ||| `attack` if it might not be).
358 ||| `attack` if it might not be).
359 forall : TTName -> Raw -> Elab ()
359 forall : TTName -> Raw -> Elab ()
360− forall n ty = prim__Forall n ty
360+ forall n ty = Prim__Forall n ty
361
361
362 ||| Convert a hole into a pattern variable.
362 ||| Convert a hole into a pattern variable.
363 patvar : TTName -> Elab ()
363 patvar : TTName -> Elab ()
364− patvar n = prim__PatVar n
364+ patvar n = Prim__PatVar n
365
365
366 ||| Introduce a new pattern binding.
366 ||| Introduce a new pattern binding.
367 |||
367 |||
368 ||| Requires that the hole be immediately under its binder (use
368 ||| Requires that the hole be immediately under its binder (use
369 ||| `attack` if it might not be).
369 ||| `attack` if it might not be).
370 patbind : TTName -> Elab ()
370 patbind : TTName -> Elab ()
371− patbind n = prim__PatBind n
371+ patbind n = Prim__PatBind n
372
372
373 ||| Introduce a new let binding.
373 ||| Introduce a new let binding.
374 |||
374 |||
@@ -379,24 +379,24 @@ namespace Tactics
379 ||| @ ty the type of the term to be let-bound
379 ||| @ ty the type of the term to be let-bound
380 ||| @ tm the term to be bound
380 ||| @ tm the term to be bound
381 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
381 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
383
383
384 ||| Normalise the goal.
384 ||| Normalise the goal.
385 compute : Elab ()
385 compute : Elab ()
386− compute = prim__Compute
386+ compute = Prim__Compute
387
387
388 ||| Normalise a term in some lexical environment
388 ||| Normalise a term in some lexical environment
389 |||
389 |||
390 ||| @ env the environment in which to compute (get one of these from `getEnv`)
390 ||| @ env the environment in which to compute (get one of these from `getEnv`)
391 ||| @ term the term to normalise
391 ||| @ term the term to normalise
392 normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
392 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
394
394
395 ||| Reduce a closed term to weak-head normal form
395 ||| Reduce a closed term to weak-head normal form
396 |||
396 |||
397 ||| @ term the term to reduce
397 ||| @ term the term to reduce
398 whnf : (term : TT) -> Elab TT
398 whnf : (term : TT) -> Elab TT
399− whnf term = prim__Whnf term
399+ whnf term = Prim__Whnf term
400
400
401 ||| Check that two terms are convertable in the current context and
401 ||| Check that two terms are convertable in the current context and
402 ||| in some environment.
402 ||| in some environment.
@@ -405,7 +405,7 @@ namespace Tactics
405 ||| @ term1 the first term to convert
405 ||| @ term1 the first term to convert
406 ||| @ term2 the second term to convert
406 ||| @ term2 the second term to convert
407 convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab ()
407 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
409
409
410 ||| Check that two terms are convertable in the current context and environment
410 ||| Check that two terms are convertable in the current context and environment
411 |||
411 |||
@@ -416,7 +416,7 @@ namespace Tactics
416
416
417 ||| Find the source context for the elaboration script
417 ||| Find the source context for the elaboration script
418 getSourceLocation : Elab SourceLocation
418 getSourceLocation : Elab SourceLocation
419− getSourceLocation = prim__SourceLocation
419+ getSourceLocation = Prim__SourceLocation
420
420
421 ||| Attempt to solve the current goal with the source code location
421 ||| Attempt to solve the current goal with the source code location
422 sourceLocation : Elab ()
422 sourceLocation : Elab ()
@@ -430,7 +430,7 @@ namespace Tactics
430 ||| The namespace is represented as a reverse-order list of strings,
430 ||| The namespace is represented as a reverse-order list of strings,
431 ||| just as in the representation of names.
431 ||| just as in the representation of names.
432 currentNamespace : Elab (List String)
432 currentNamespace : Elab (List String)
433− currentNamespace = prim__Namespace
433+ currentNamespace = Prim__Namespace
434
434
435 ||| Attempt to rewrite the goal using an equality.
435 ||| Attempt to rewrite the goal using an equality.
436 |||
436 |||
@@ -443,48 +443,48 @@ namespace Tactics
443 ||| requires that the hole be immediately under its binder (use
443 ||| requires that the hole be immediately under its binder (use
444 ||| `attack` if it might not be).
444 ||| `attack` if it might not be).
445 rewriteWith : Raw -> Elab ()
445 rewriteWith : Raw -> Elab ()
446− rewriteWith rule = prim__Rewrite rule
446+ rewriteWith rule = Prim__Rewrite rule
447
447
448 ||| Add a type declaration to the global context.
448 ||| Add a type declaration to the global context.
449 declareType : TyDecl -> Elab ()
449 declareType : TyDecl -> Elab ()
450− declareType decl = prim__DeclareType decl
450+ declareType decl = Prim__DeclareType decl
451
451
452 ||| Define a function in the global context. The function must have
452 ||| Define a function in the global context. The function must have
453 ||| already been declared, either in ordinary Idris code or using
453 ||| already been declared, either in ordinary Idris code or using
454 ||| `declareType`.
454 ||| `declareType`.
455 defineFunction : FunDefn -> Elab ()
455 defineFunction : FunDefn -> Elab ()
456− defineFunction defun = prim__DefineFunction defun
456+ defineFunction defun = Prim__DefineFunction defun
457
457
458 ||| Register a new instance for type class resolution.
458 ||| Register a new instance for type class resolution.
459 |||
459 |||
460 ||| @ className the name of the class for which an instance is being registered
460 ||| @ className the name of the class for which an instance is being registered
461 ||| @ instName the name of the definition to use in instance search
461 ||| @ instName the name of the definition to use in instance search
462 addInstance : (className, instName : TTName) -> Elab ()
462 addInstance : (className, instName : TTName) -> Elab ()
463− addInstance className instName = prim__AddInstance className instName
463+ addInstance className instName = Prim__AddInstance className instName
464
464
465 ||| Determine whether a name denotes a class.
465 ||| Determine whether a name denotes a class.
466 |||
466 |||
467 ||| @ name a name that might denote a class.
467 ||| @ name a name that might denote a class.
468 isTCName : (name : TTName) -> Elab Bool
468 isTCName : (name : TTName) -> Elab Bool
469− isTCName name = prim__IsTCName name
469+ isTCName name = Prim__IsTCName name
470
470
471 ||| Attempt to solve the current goal with a type class dictionary
471 ||| Attempt to solve the current goal with a type class dictionary
472 |||
472 |||
473 ||| @ fn the name of the definition being elaborated (to prevent Idris
473 ||| @ fn the name of the definition being elaborated (to prevent Idris
474 ||| from looping)
474 ||| from looping)
475 resolveTC : (fn : TTName) -> Elab ()
475 resolveTC : (fn : TTName) -> Elab ()
476− resolveTC fn = prim__ResolveTC fn
476+ resolveTC fn = Prim__ResolveTC fn
477
477
478 ||| Use Idris's internal proof search.
478 ||| Use Idris's internal proof search.
479 search : Elab ()
479 search : Elab ()
480− search = prim__Search 100 []
480+ search = Prim__Search 100 []
481
481
482 ||| Use Idris's internal proof search, with more control.
482 ||| Use Idris's internal proof search, with more control.
483 |||
483 |||
484 ||| @ depth the search depth
484 ||| @ depth the search depth
485 ||| @ hints additional names to try
485 ||| @ hints additional names to try
486 search' : (depth : Int) -> (hints : List TTName) -> Elab ()
486 search' : (depth : Int) -> (hints : List TTName) -> Elab ()
487− search' depth hints = prim__Search depth hints
487+ search' depth hints = Prim__Search depth hints
488
488
489 ||| Look up the declared fixity for an operator.
489 ||| Look up the declared fixity for an operator.
490 |||
490 |||
@@ -493,14 +493,14 @@ namespace Tactics
493 |||
493 |||
494 ||| @ operator the operator string to look up
494 ||| @ operator the operator string to look up
495 operatorFixity : (operator : String) -> Elab Fixity
495 operatorFixity : (operator : String) -> Elab Fixity
496− operatorFixity operator = prim__Fixity operator
496+ operatorFixity operator = Prim__Fixity operator
497
497
498 ||| Halt elaboration, dumping the internal state for inspection.
498 ||| Halt elaboration, dumping the internal state for inspection.
499 |||
499 |||
500 ||| This is intended for elaboration script developers, not for
500 ||| This is intended for elaboration script developers, not for
501 ||| end-users. Use `fail` for final scripts.
501 ||| end-users. Use `fail` for final scripts.
502 debug : Elab a
502 debug : Elab a
503− debug = prim__Debug []
503+ debug = Prim__Debug []
504
504
505 ||| Halt elaboration, dumping the internal state and displaying a
505 ||| Halt elaboration, dumping the internal state and displaying a
506 ||| message.
506 ||| message.
@@ -510,17 +510,17 @@ namespace Tactics
510 |||
510 |||
511 ||| @ msg the message to display
511 ||| @ msg the message to display
512 debugMessage : (msg : List ErrorReportPart) -> Elab a
512 debugMessage : (msg : List ErrorReportPart) -> Elab a
513− debugMessage msg = prim__Debug msg
513+ debugMessage msg = Prim__Debug msg
514
514
515 ||| Create a new top-level metavariable to solve the current hole.
515 ||| Create a new top-level metavariable to solve the current hole.
516 |||
516 |||
517 ||| @ name the name for the top-level variable
517 ||| @ name the name for the top-level variable
518 metavar : (name : TTName) -> Elab ()
518 metavar : (name : TTName) -> Elab ()
519− metavar name = prim__Metavar name
519+ metavar name = Prim__Metavar name
520
520
521 ||| Recursively invoke the reflected elaborator with some goal.
521 ||| Recursively invoke the reflected elaborator with some goal.
522 |||
522 |||
523 ||| The result is the final term and its type.
523 ||| The result is the final term and its type.
524 runElab : Raw -> Elab () -> Elab (TT, TT)
524 runElab : Raw -> Elab () -> Elab (TT, TT)
525− runElab goal script = prim__RecursiveElab goal script
525+ runElab goal script = Prim__RecursiveElab goal script
526
526
libs/prelude/Prelude/Nat.idr+10−10
@@ -216,45 +216,45 @@ instance Cast Integer Nat where
216
216
217||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
217||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
218record Multiplicative where
218record Multiplicative where
219− constructor getMultiplicative
219+ constructor GetMultiplicative
220 _ : Nat
220 _ : Nat
221
221
222||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)
222||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)
223record Additive where
223record Additive where
224− constructor getAdditive
224+ constructor GetAdditive
225 _ : Nat
225 _ : Nat
226
226
227instance Semigroup Multiplicative where
227instance Semigroup Multiplicative where
228− (<+>) left right = getMultiplicative $ left' * right'
228+ (<+>) left right = GetMultiplicative $ left' * right'
229 where
229 where
230 left' : Nat
230 left' : Nat
231 left' =
231 left' =
232 case left of
232 case left of
233− getMultiplicative m => m
233+ GetMultiplicative m => m
234
234
235 right' : Nat
235 right' : Nat
236 right' =
236 right' =
237 case right of
237 case right of
238− getMultiplicative m => m
238+ GetMultiplicative m => m
239
239
240instance Semigroup Additive where
240instance Semigroup Additive where
241− left <+> right = getAdditive $ left' + right'
241+ left <+> right = GetAdditive $ left' + right'
242 where
242 where
243 left' : Nat
243 left' : Nat
244 left' =
244 left' =
245 case left of
245 case left of
246− getAdditive m => m
246+ GetAdditive m => m
247
247
248 right' : Nat
248 right' : Nat
249 right' =
249 right' =
250 case right of
250 case right of
251− getAdditive m => m
251+ GetAdditive m => m
252
252
253instance Monoid Multiplicative where
253instance Monoid Multiplicative where
254− neutral = getMultiplicative $ S Z
254+ neutral = GetMultiplicative $ S Z
255
255
256instance Monoid Additive where
256instance Monoid Additive where
257− neutral = getAdditive Z
257+ neutral = GetAdditive Z
258
258
259||| Casts negative `Ints` to 0.
259||| Casts negative `Ints` to 0.
260instance Cast Int Nat where
260instance 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
1802 -- step, the output is the (reflected) term returned.
1802 -- step, the output is the (reflected) term returned.
1803 runTacTm :: Term -> ElabD Term
1803 runTacTm :: Term -> ElabD Term
1804 runTacTm (unApply -> tac@(P _ n _, args))
1804 runTacTm (unApply -> tac@(P _ n _, args))
1805− | n == tacN "prim__Solve", [] <- args
1805+ | n == tacN "Prim__Solve", [] <- args
1806 = do solve
1806 = do solve
1807 returnUnit
1807 returnUnit
1808− | n == tacN "prim__Goal", [] <- args
1808+ | n == tacN "Prim__Goal", [] <- args
1809 = do hs <- get_holes
1809 = do hs <- get_holes
1810 case hs of
1810 case hs of
1811 (h : _) -> do t <- goal
1811 (h : _) -> do t <- goal
@@ -1815,11 +1815,11 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1815 [] -> lift . tfail . Msg $
1815 [] -> lift . tfail . Msg $
1816 "Elaboration is complete. There are no goals."
1816 "Elaboration is complete. There are no goals."
1817
1817
1818− | n == tacN "prim__Holes", [] <- args
1818+ | n == tacN "Prim__Holes", [] <- args
1819 = do hs <- get_holes
1819 = do hs <- get_holes
1820 fmap fst . checkClosed $
1820 fmap fst . checkClosed $
1821 mkList (Var $ reflm "TTName") (map reflectName hs)
1821 mkList (Var $ reflm "TTName") (map reflectName hs)
1822− | n == tacN "prim__Guess", [] <- args
1822+ | n == tacN "Prim__Guess", [] <- args
1823 = do ok <- is_guess
1823 = do ok <- is_guess
1824 if ok
1824 if ok
1825 then do guess <- fmap forget get_guess
1825 then do guess <- fmap forget get_guess
@@ -1830,7 +1830,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1830 else fmap fst . checkClosed $
1830 else fmap fst . checkClosed $
1831 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1831 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1832 (Var (reflm "TT"))
1832 (Var (reflm "TT"))
1833− | n == tacN "prim__LookupTy", [n] <- args
1833+ | n == tacN "Prim__LookupTy", [n] <- args
1834 = do n' <- reifyTTName n
1834 = do n' <- reifyTTName n
1835 ctxt <- get_context
1835 ctxt <- get_context
1836 let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
1836 let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
@@ -1852,14 +1852,14 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1852 , raw_apply (Var pairTy) [ Var (reflm "NameType")
1852 , raw_apply (Var pairTy) [ Var (reflm "NameType")
1853 , Var (reflm "TT")]])
1853 , Var (reflm "TT")]])
1854 defs
1854 defs
1855− | n == tacN "prim__LookupDatatype", [name] <- args
1855+ | n == tacN "Prim__LookupDatatype", [name] <- args
1856 = do n' <- reifyTTName name
1856 = do n' <- reifyTTName name
1857 datatypes <- get_datatypes
1857 datatypes <- get_datatypes
1858 ctxt <- get_context
1858 ctxt <- get_context
1859 fmap fst . checkClosed $
1859 fmap fst . checkClosed $
1860 rawList (Var (tacN "Datatype"))
1860 rawList (Var (tacN "Datatype"))
1861 (map reflectDatatype (buildDatatypes ist n'))
1861 (map reflectDatatype (buildDatatypes ist n'))
1862− | n == tacN "prim__LookupArgs", [name] <- args
1862+ | n == tacN "Prim__LookupArgs", [name] <- args
1863 = do n' <- reifyTTName name
1863 = do n' <- reifyTTName name
1864 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
1864 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
1865 listFunArg = RApp listTy (Var (tacN "FunArg"))
1865 listFunArg = RApp listTy (Var (tacN "FunArg"))
@@ -1883,39 +1883,39 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1883 (Var (tacN "FunArg"))
1883 (Var (tacN "FunArg"))
1884 , Var (reflm "Raw")]])
1884 , Var (reflm "Raw")]])
1885 out
1885 out
1886− | n == tacN "prim__SourceLocation", [] <- args
1886+ | n == tacN "Prim__SourceLocation", [] <- args
1887 = fmap fst . checkClosed $
1887 = fmap fst . checkClosed $
1888 reflectFC fc
1888 reflectFC fc
1889− | n == tacN "prim__Namespace", [] <- args
1889+ | n == tacN "Prim__Namespace", [] <- args
1890 = fmap fst . checkClosed $
1890 = fmap fst . checkClosed $
1891 rawList (RConstant StrType) (map (RConstant . Str) ns)
1891 rawList (RConstant StrType) (map (RConstant . Str) ns)
1892− | n == tacN "prim__Env", [] <- args
1892+ | n == tacN "Prim__Env", [] <- args
1893 = do env <- get_env
1893 = do env <- get_env
1894 fmap fst . checkClosed $ reflectEnv env
1894 fmap fst . checkClosed $ reflectEnv env
1895− | n == tacN "prim__Fail", [_a, errs] <- args
1895+ | n == tacN "Prim__Fail", [_a, errs] <- args
1896 = do errs' <- eval errs
1896 = do errs' <- eval errs
1897 parts <- reifyReportParts errs'
1897 parts <- reifyReportParts errs'
1898 lift . tfail $ ReflectionError [parts] (Msg "")
1898 lift . tfail $ ReflectionError [parts] (Msg "")
1899− | n == tacN "prim__PureElab", [_a, tm] <- args
1899+ | n == tacN "Prim__PureElab", [_a, tm] <- args
1900 = return tm
1900 = return tm
1901− | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args
1901+ | n == tacN "Prim__BindElab", [_a, _b, first, andThen] <- args
1902 = do first' <- eval first
1902 = do first' <- eval first
1903 res <- eval =<< runTacTm first'
1903 res <- eval =<< runTacTm first'
1904 next <- eval (App Complete andThen res)
1904 next <- eval (App Complete andThen res)
1905 runTacTm next
1905 runTacTm next
1906− | n == tacN "prim__Try", [_a, first, alt] <- args
1906+ | n == tacN "Prim__Try", [_a, first, alt] <- args
1907 = do first' <- eval first
1907 = do first' <- eval first
1908 alt' <- eval alt
1908 alt' <- eval alt
1909 try' (runTacTm first') (runTacTm alt') True
1909 try' (runTacTm first') (runTacTm alt') True
1910− | n == tacN "prim__Fill", [raw] <- args
1910+ | n == tacN "Prim__Fill", [raw] <- args
1911 = do raw' <- reifyRaw =<< eval raw
1911 = do raw' <- reifyRaw =<< eval raw
1912 apply raw' []
1912 apply raw' []
1913 returnUnit
1913 returnUnit
1914− | n == tacN "prim__Apply" || n == tacN "prim__MatchApply"
1914+ | n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"
1915 , [raw, argSpec] <- args
1915 , [raw, argSpec] <- args
1916 = do raw' <- reifyRaw =<< eval raw
1916 = do raw' <- reifyRaw =<< eval raw
1917 argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec
1917 argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec
1918− let op = if n == tacN "prim__Apply"
1918+ let op = if n == tacN "Prim__Apply"
1919 then apply
1919 then apply
1920 else match_apply
1920 else match_apply
1921 ns <- op raw' argSpec'
1921 ns <- op raw' argSpec'
@@ -1925,19 +1925,19 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1925 (reflectName n1, reflectName n2)
1925 (reflectName n1, reflectName n2)
1926 | (n1, n2) <- ns
1926 | (n1, n2) <- ns
1927 ]
1927 ]
1928− | n == tacN "prim__Gensym", [hint] <- args
1928+ | n == tacN "Prim__Gensym", [hint] <- args
1929 = do hintStr <- eval hint
1929 = do hintStr <- eval hint
1930 case hintStr of
1930 case hintStr of
1931 Constant (Str h) -> do
1931 Constant (Str h) -> do
1932 n <- getNameFrom (sMN 0 h)
1932 n <- getNameFrom (sMN 0 h)
1933 fmap fst $ get_type_val (reflectName n)
1933 fmap fst $ get_type_val (reflectName n)
1934 _ -> fail "no hint"
1934 _ -> fail "no hint"
1935− | n == tacN "prim__Claim", [n, ty] <- args
1935+ | n == tacN "Prim__Claim", [n, ty] <- args
1936 = do n' <- reifyTTName n
1936 = do n' <- reifyTTName n
1937 ty' <- reifyRaw ty
1937 ty' <- reifyRaw ty
1938 claim n' ty'
1938 claim n' ty'
1939 returnUnit
1939 returnUnit
1940− | n == tacN "prim__Check", [env', raw] <- args
1940+ | n == tacN "Prim__Check", [env', raw] <- args
1941 = do env <- reifyEnv env'
1941 = do env <- reifyEnv env'
1942 raw' <- reifyRaw =<< eval raw
1942 raw' <- reifyRaw =<< eval raw
1943 ctxt <- get_context
1943 ctxt <- get_context
@@ -1945,68 +1945,68 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1945 fmap fst . checkClosed $
1945 fmap fst . checkClosed $
1946 rawPair (Var (reflm "TT"), Var (reflm "TT"))
1946 rawPair (Var (reflm "TT"), Var (reflm "TT"))
1947 (reflect tm, reflect ty)
1947 (reflect tm, reflect ty)
1948− | n == tacN "prim__Attack", [] <- args
1948+ | n == tacN "Prim__Attack", [] <- args
1949 = do attack
1949 = do attack
1950 returnUnit
1950 returnUnit
1951− | n == tacN "prim__Rewrite", [rule] <- args
1951+ | n == tacN "Prim__Rewrite", [rule] <- args
1952 = do r <- reifyRaw rule
1952 = do r <- reifyRaw rule
1953 rewrite r
1953 rewrite r
1954 returnUnit
1954 returnUnit
1955− | n == tacN "prim__Focus", [what] <- args
1955+ | n == tacN "Prim__Focus", [what] <- args
1956 = do n' <- reifyTTName what
1956 = do n' <- reifyTTName what
1957 hs <- get_holes
1957 hs <- get_holes
1958 if elem n' hs
1958 if elem n' hs
1959 then focus n' >> returnUnit
1959 then focus n' >> returnUnit
1960 else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
1960 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
1962 = do n' <- reifyTTName what
1962 = do n' <- reifyTTName what
1963 movelast n'
1963 movelast n'
1964 returnUnit
1964 returnUnit
1965− | n == tacN "prim__Intro", [mn] <- args
1965+ | n == tacN "Prim__Intro", [mn] <- args
1966 = do n <- case fromTTMaybe mn of
1966 = do n <- case fromTTMaybe mn of
1967 Nothing -> return Nothing
1967 Nothing -> return Nothing
1968 Just name -> fmap Just $ reifyTTName name
1968 Just name -> fmap Just $ reifyTTName name
1969 intro n
1969 intro n
1970 returnUnit
1970 returnUnit
1971− | n == tacN "prim__Forall", [n, ty] <- args
1971+ | n == tacN "Prim__Forall", [n, ty] <- args
1972 = do n' <- reifyTTName n
1972 = do n' <- reifyTTName n
1973 ty' <- reifyRaw ty
1973 ty' <- reifyRaw ty
1974 forall n' Nothing ty'
1974 forall n' Nothing ty'
1975 returnUnit
1975 returnUnit
1976− | n == tacN "prim__PatVar", [n] <- args
1976+ | n == tacN "Prim__PatVar", [n] <- args
1977 = do n' <- reifyTTName n
1977 = do n' <- reifyTTName n
1978 patvar' n'
1978 patvar' n'
1979 returnUnit
1979 returnUnit
1980− | n == tacN "prim__PatBind", [n] <- args
1980+ | n == tacN "Prim__PatBind", [n] <- args
1981 = do n' <- reifyTTName n
1981 = do n' <- reifyTTName n
1982 patbind n'
1982 patbind n'
1983 returnUnit
1983 returnUnit
1984− | n == tacN "prim__LetBind", [n, ty, tm] <- args
1984+ | n == tacN "Prim__LetBind", [n, ty, tm] <- args
1985 = do n' <- reifyTTName n
1985 = do n' <- reifyTTName n
1986 ty' <- reifyRaw ty
1986 ty' <- reifyRaw ty
1987 tm' <- reifyRaw tm
1987 tm' <- reifyRaw tm
1988 letbind n' ty' tm'
1988 letbind n' ty' tm'
1989 returnUnit
1989 returnUnit
1990− | n == tacN "prim__Compute", [] <- args
1990+ | n == tacN "Prim__Compute", [] <- args
1991 = do compute ; returnUnit
1991 = do compute ; returnUnit
1992− | n == tacN "prim__Normalise", [env, tm] <- args
1992+ | n == tacN "Prim__Normalise", [env, tm] <- args
1993 = do env' <- reifyEnv env
1993 = do env' <- reifyEnv env
1994 tm' <- reifyTT tm
1994 tm' <- reifyTT tm
1995 ctxt <- get_context
1995 ctxt <- get_context
1996 let out = normaliseAll ctxt env' (finalise tm')
1996 let out = normaliseAll ctxt env' (finalise tm')
1997 fmap fst . checkClosed $ reflect out
1997 fmap fst . checkClosed $ reflect out
1998− | n == tacN "prim__Whnf", [tm] <- args
1998+ | n == tacN "Prim__Whnf", [tm] <- args
1999 = do tm' <- reifyTT tm
1999 = do tm' <- reifyTT tm
2000 ctxt <- get_context
2000 ctxt <- get_context
2001 fmap fst . checkClosed . reflect $ whnf ctxt tm'
2001 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
2003 = do env' <- reifyEnv env
2003 = do env' <- reifyEnv env
2004 tm1' <- reifyTT tm1
2004 tm1' <- reifyTT tm1
2005 tm2' <- reifyTT tm2
2005 tm2' <- reifyTT tm2
2006 ctxt <- get_context
2006 ctxt <- get_context
2007 lift $ converts ctxt env' tm1' tm2'
2007 lift $ converts ctxt env' tm1' tm2'
2008 returnUnit
2008 returnUnit
2009− | n == tacN "prim__DeclareType", [decl] <- args
2009+ | n == tacN "Prim__DeclareType", [decl] <- args
2010 = do (RDeclare n args res) <- reifyTyDecl decl
2010 = do (RDeclare n args res) <- reifyTyDecl decl
2011 ctxt <- get_context
2011 ctxt <- get_context
2012 let mkPi arg res = RBind (argName arg)
2012 let mkPi arg res = RBind (argName arg)
@@ -2029,27 +2029,27 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2029 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
2029 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
2030 new_tyDecls e }
2030 new_tyDecls e }
2031 returnUnit
2031 returnUnit
2032− | n == tacN "prim__DefineFunction", [decl] <- args
2032+ | n == tacN "Prim__DefineFunction", [decl] <- args
2033 = do defn <- reifyFunDefn decl
2033 = do defn <- reifyFunDefn decl
2034 defineFunction defn
2034 defineFunction defn
2035 returnUnit
2035 returnUnit
2036− | n == tacN "prim__AddInstance", [cls, inst] <- args
2036+ | n == tacN "Prim__AddInstance", [cls, inst] <- args
2037 = do className <- reifyTTName cls
2037 = do className <- reifyTTName cls
2038 instName <- reifyTTName inst
2038 instName <- reifyTTName inst
2039 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
2039 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
2040 new_tyDecls e}
2040 new_tyDecls e}
2041 returnUnit
2041 returnUnit
2042− | n == tacN "prim__IsTCName", [n] <- args
2042+ | n == tacN "Prim__IsTCName", [n] <- args
2043 = do n' <- reifyTTName n
2043 = do n' <- reifyTTName n
2044 case lookupCtxtExact n' (idris_classes ist) of
2044 case lookupCtxtExact n' (idris_classes ist) of
2045 Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
2045 Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
2046 Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
2046 Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
2047− | n == tacN "prim__ResolveTC", [fn] <- args
2047+ | n == tacN "Prim__ResolveTC", [fn] <- args
2048 = do g <- goal
2048 = do g <- goal
2049 fn <- reifyTTName fn
2049 fn <- reifyTTName fn
2050 resolveTC' False True 100 g fn ist
2050 resolveTC' False True 100 g fn ist
2051 returnUnit
2051 returnUnit
2052− | n == tacN "prim__Search", [depth, hints] <- args
2052+ | n == tacN "Prim__Search", [depth, hints] <- args
2053 = do d <- eval depth
2053 = do d <- eval depth
2054 hints' <- eval hints
2054 hints' <- eval hints
2055 case (d, unList hints') of
2055 case (d, unList hints') of
@@ -2062,7 +2062,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2062 (Constant (I _), Nothing ) ->
2062 (Constant (I _), Nothing ) ->
2063 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
2063 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
2064 (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d
2064 (_, _) -> 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
2066 = do goal' <- reifyRaw goal
2066 = do goal' <- reifyRaw goal
2067 ctxt <- get_context
2067 ctxt <- get_context
2068 script <- eval script
2068 script <- eval script
@@ -2093,7 +2093,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2093 fmap fst . checkClosed $
2093 fmap fst . checkClosed $
2094 rawPair (Var $ reflm "TT", Var $ reflm "TT")
2094 rawPair (Var $ reflm "TT", Var $ reflm "TT")
2095 (tm', ty')
2095 (tm', ty')
2096− | n == tacN "prim__Metavar", [n] <- args
2096+ | n == tacN "Prim__Metavar", [n] <- args
2097 = do n' <- reifyTTName n
2097 = do n' <- reifyTTName n
2098 ctxt <- get_context
2098 ctxt <- get_context
2099 ptm <- get_term
2099 ptm <- get_term
@@ -2104,7 +2104,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2104 defer unique_used mvn
2104 defer unique_used mvn
2105 solve
2105 solve
2106 returnUnit
2106 returnUnit
2107− | n == tacN "prim__Fixity", [op'] <- args
2107+ | n == tacN "Prim__Fixity", [op'] <- args
2108 = do opTm <- eval op'
2108 = do opTm <- eval op'
2109 case opTm of
2109 case opTm of
2110 Constant (Str op) ->
2110 Constant (Str op) ->
@@ -2118,7 +2118,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2118 [f] -> fmap fst . checkClosed $ reflectFixity f
2118 [f] -> fmap fst . checkClosed $ reflectFixity f
2119 many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many
2119 many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many
2120 _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm
2120 _ -> 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
2122 = do msg' <- eval msg
2122 = do msg' <- eval msg
2123 parts <- reifyReportParts msg
2123 parts <- reifyReportParts msg
2124 debugElaborator parts
2124 debugElaborator parts