@@ -16,6 +16,8 @@ import Prelude.Monad
16import Prelude.Nat
16import Prelude.Nat
17import Language.Reflection
17import Language.Reflection
19data Fixity = Infixl Nat | Infixr Nat | Infix Nat | Prefix Nat
21data Fixity = Infixl Nat | Infixr Nat | Infix Nat | Prefix Nat
21||| Erasure annotations reflect Idris's idea of what is intended to be
23||| Erasure annotations reflect Idris's idea of what is intended to be
@@ -100,7 +102,7 @@ record Datatype where
100 constructors : List (TTName, List CtorArg, Raw)
102 constructors : List (TTName, List CtorArg, Raw)
102||| A reflected elaboration script.
104||| A reflected elaboration script.
104data Elab : Type -> Type where
106data Elab : Type -> Type where
105 -- obligatory control stuff
107 -- obligatory control stuff
106 Prim__PureElab : a -> Elab a
108 Prim__PureElab : a -> Elab a
@@ -164,7 +166,7 @@ data Elab : Type -> Type where
164-------------
166-------------
165-- Public API
167-- Public API
166-------------
168-------------
167−%access public
169+%access public export
168namespace Tactics
170namespace Tactics
169 implementation Functor Elab where
171 implementation Functor Elab where
170 map f t = Prim__BindElab t (\x => Prim__PureElab (f x))
172 map f t = Prim__BindElab t (\x => Prim__PureElab (f x))
@@ -186,31 +188,38 @@ namespace Tactics
186 x >>= f = Prim__BindElab x f
188 x >>= f = Prim__BindElab x f
188 ||| Halt elaboration with an error
190 ||| Halt elaboration with an error
189 fail : List ErrorReportPart -> Elab a
192 fail : List ErrorReportPart -> Elab a
190 fail err = Prim__Fail err
193 fail err = Prim__Fail err
192 ||| 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.
193 getEnv : Elab (List (TTName, Binder TT))
197 getEnv : Elab (List (TTName, Binder TT))
194 getEnv = Prim__Env
198 getEnv = Prim__Env
196 ||| 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.
197 getGoal : Elab (TTName, TT)
202 getGoal : Elab (TTName, TT)
198 getGoal = Prim__Goal
203 getGoal = Prim__Goal
200 ||| Get the hole queue, in order.
205 ||| Get the hole queue, in order.
201 getHoles : Elab (List TTName)
207 getHoles : Elab (List TTName)
202 getHoles = Prim__Holes
208 getHoles = Prim__Holes
204 ||| If the current hole contains a guess, return it. Otherwise, fail.
210 ||| If the current hole contains a guess, return it. Otherwise, fail.
205 getGuess : Elab TT
212 getGuess : Elab TT
206 getGuess = Prim__Guess
213 getGuess = Prim__Guess
208 ||| Look up the types of every overloading of a name.
215 ||| Look up the types of every overloading of a name.
209 lookupTy : TTName -> Elab (List (TTName, NameType, TT))
217 lookupTy : TTName -> Elab (List (TTName, NameType, TT))
210 lookupTy n = Prim__LookupTy n
218 lookupTy n = Prim__LookupTy n
212 ||| 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
213 ||| resolve uniquely.
221 ||| resolve uniquely.
214 lookupTyExact : TTName -> Elab (TTName, NameType, TT)
223 lookupTyExact : TTName -> Elab (TTName, NameType, TT)
215 lookupTyExact n = case !(lookupTy n) of
224 lookupTyExact n = case !(lookupTy n) of
216 [res] => return res
225 [res] => return res
@@ -219,12 +228,14 @@ namespace Tactics
220 ||| Find the reflected representation of all datatypes whose names
229 ||| Find the reflected representation of all datatypes whose names
221 ||| are overloadings of some name.
230 ||| are overloadings of some name.
222 lookupDatatype : TTName -> Elab (List Datatype)
232 lookupDatatype : TTName -> Elab (List Datatype)
223 lookupDatatype n = Prim__LookupDatatype n
233 lookupDatatype n = Prim__LookupDatatype n
225 ||| Find the reflected representation of a datatype, given its
235 ||| Find the reflected representation of a datatype, given its
226 ||| fully-qualified name. Fail if the name does not uniquely resolve
236 ||| fully-qualified name. Fail if the name does not uniquely resolve
227 ||| to a datatype.
237 ||| to a datatype.
228 lookupDatatypeExact : TTName -> Elab Datatype
239 lookupDatatypeExact : TTName -> Elab Datatype
229 lookupDatatypeExact n = case !(lookupDatatype n) of
240 lookupDatatypeExact n = case !(lookupDatatype n) of
230 [res] => return res
241 [res] => return res
@@ -233,12 +244,14 @@ namespace Tactics
234 ||| Find the reflected function definition of all functions whose names
245 ||| Find the reflected function definition of all functions whose names
235 ||| are overloadings of some name.
246 ||| are overloadings of some name.
236 lookupFunDefn : TTName -> Elab (List (FunDefn TT))
248 lookupFunDefn : TTName -> Elab (List (FunDefn TT))
237 lookupFunDefn n = Prim__LookupFunDefn n
249 lookupFunDefn n = Prim__LookupFunDefn n
239 ||| Find the reflected function definition of a function, given its
251 ||| Find the reflected function definition of a function, given its
240 ||| fully-qualified name. Fail if the name does not uniquely resolve
252 ||| fully-qualified name. Fail if the name does not uniquely resolve
241 ||| to a function.
253 ||| to a function.
242 lookupFunDefnExact : TTName -> Elab (FunDefn TT)
255 lookupFunDefnExact : TTName -> Elab (FunDefn TT)
243 lookupFunDefnExact n = case !(lookupFunDefn n) of
256 lookupFunDefnExact n = case !(lookupFunDefn n) of
244 [res] => return res
257 [res] => return res
@@ -246,11 +259,13 @@ namespace Tactics
246 xs => fail [TextPart "More than one function named", NamePart n]
259 xs => fail [TextPart "More than one function named", NamePart n]
248 ||| Get the argument specification for each overloading of a name.
261 ||| Get the argument specification for each overloading of a name.
249 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
263 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
250 lookupArgs n = Prim__LookupArgs n
264 lookupArgs n = Prim__LookupArgs n
252 ||| 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
253 ||| not uniquely resolve.
267 ||| not uniquely resolve.
254 lookupArgsExact : TTName -> Elab (TTName, List FunArg, Raw)
269 lookupArgsExact : TTName -> Elab (TTName, List FunArg, Raw)
255 lookupArgsExact n = case !(lookupArgs n) of
270 lookupArgsExact n = case !(lookupArgs n) of
256 [res] => return res
271 [res] => return res
@@ -261,6 +276,7 @@ namespace Tactics
262 ||| @ env the environment within which to check the type
277 ||| @ env the environment within which to check the type
263 ||| @ tm the term to check
278 ||| @ tm the term to check
264 check : (env : List (TTName, Binder TT)) -> (tm : Raw) -> Elab (TT, TT)
280 check : (env : List (TTName, Binder TT)) -> (tm : Raw) -> Elab (TT, TT)
265 check env tm = Prim__Check env tm
281 check env tm = Prim__Check env tm
@@ -269,15 +285,18 @@ namespace Tactics
270 ||| **NB**: the generated name is unique _for this run of the
286 ||| **NB**: the generated name is unique _for this run of the
271 ||| elaborator_. Do not assume that they are globally unique.
287 ||| elaborator_. Do not assume that they are globally unique.
272 gensym : (hint : String) -> Elab TTName
289 gensym : (hint : String) -> Elab TTName
273 gensym hint = Prim__Gensym hint
290 gensym hint = Prim__Gensym hint
275 ||| Substitute a guess into a hole.
292 ||| Substitute a guess into a hole.
276 solve : Elab ()
294 solve : Elab ()
277 solve = Prim__Solve
295 solve = Prim__Solve
279 ||| 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
280 ||| is not a hole.
298 ||| is not a hole.
281 fill : Raw -> Elab ()
300 fill : Raw -> Elab ()
282 fill tm = Prim__Fill tm
301 fill tm = Prim__Fill tm
@@ -295,6 +314,7 @@ namespace Tactics
295 ||| @ argSpec instructions for finding the arguments to the term,
314 ||| @ argSpec instructions for finding the arguments to the term,
296 ||| where the Boolean states whether or not to attempt to solve
315 ||| where the Boolean states whether or not to attempt to solve
297 ||| the argument by unification.
316 ||| the argument by unification.
298 apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
318 apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
299 apply tm argSpec = map snd <$> Prim__Apply tm argSpec
319 apply tm argSpec = map snd <$> Prim__Apply tm argSpec
@@ -313,6 +333,7 @@ namespace Tactics
313 ||| where the Boolean states whether or not to attempt to solve
333 ||| where the Boolean states whether or not to attempt to solve
314 ||| the argument by matching.
334 ||| the argument by matching.
316 matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
337 matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
317 matchApply tm argSpec = map snd <$> Prim__Apply tm argSpec
338 matchApply tm argSpec = map snd <$> Prim__Apply tm argSpec
@@ -320,11 +341,13 @@ namespace Tactics
320 ||| exist.
341 ||| exist.
322 ||| @ hole the hole to focus on
343 ||| @ hole the hole to focus on
323 focus : (hole : TTName) -> Elab ()
345 focus : (hole : TTName) -> Elab ()
324 focus hole = Prim__Focus hole
346 focus hole = Prim__Focus hole
326 ||| 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
327 ||| focus on the next hole.
349 ||| focus on the next hole.
328 unfocus : TTName -> Elab ()
351 unfocus : TTName -> Elab ()
329 unfocus hole = Prim__Unfocus hole
352 unfocus hole = Prim__Unfocus hole
@@ -336,6 +359,7 @@ namespace Tactics
336 ||| 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
337 ||| 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
338 ||| points the old hole at it.
361 ||| points the old hole at it.
339 attack : Elab ()
363 attack : Elab ()
340 attack = Prim__Attack
364 attack = Prim__Attack
@@ -344,6 +368,7 @@ namespace Tactics
344 ||| The new hole will be focused, and the previously-focused hole
368 ||| The new hole will be focused, and the previously-focused hole
345 ||| will be immediately after it in the hole queue. Because this
369 ||| will be immediately after it in the hole queue. Because this
346 ||| tactic introduces a new binding, you may need to `attack` first.
370 ||| tactic introduces a new binding, you may need to `attack` first.
347 claim : TTName -> Raw -> Elab ()
372 claim : TTName -> Raw -> Elab ()
348 claim n ty = Prim__Claim n ty
373 claim n ty = Prim__Claim n ty
@@ -352,6 +377,7 @@ namespace Tactics
352 ||| `attack`).
377 ||| `attack`).
354 ||| @ n the name to use for the argument
379 ||| @ n the name to use for the argument
355 intro : (n : TTName) -> Elab ()
381 intro : (n : TTName) -> Elab ()
356 intro n = Prim__Intro (Just n)
382 intro n = Prim__Intro (Just n)
@@ -361,6 +387,7 @@ namespace Tactics
362 ||| Requires that the hole be immediately under its binder (use
388 ||| Requires that the hole be immediately under its binder (use
363 ||| `attack` if it might not be).
389 ||| `attack` if it might not be).
364 intro' : Elab ()
391 intro' : Elab ()
365 intro' = Prim__Intro Nothing
392 intro' = Prim__Intro Nothing
@@ -369,10 +396,12 @@ namespace Tactics
370 ||| Requires that the hole be immediately under its binder (use
397 ||| Requires that the hole be immediately under its binder (use
371 ||| `attack` if it might not be).
398 ||| `attack` if it might not be).
372 forall : TTName -> Raw -> Elab ()
400 forall : TTName -> Raw -> Elab ()
373 forall n ty = Prim__Forall n ty
401 forall n ty = Prim__Forall n ty
375 ||| Convert a hole into a pattern variable.
403 ||| Convert a hole into a pattern variable.
376 patvar : TTName -> Elab ()
405 patvar : TTName -> Elab ()
377 patvar n = Prim__PatVar n
406 patvar n = Prim__PatVar n
@@ -380,6 +409,7 @@ namespace Tactics
381 ||| Requires that the hole be immediately under its binder (use
410 ||| Requires that the hole be immediately under its binder (use
382 ||| `attack` if it might not be).
411 ||| `attack` if it might not be).
383 patbind : TTName -> Elab ()
413 patbind : TTName -> Elab ()
384 patbind n = Prim__PatBind n
414 patbind n = Prim__PatBind n
@@ -391,10 +421,12 @@ namespace Tactics
391 ||| @ n the name to let bind
421 ||| @ n the name to let bind
392 ||| @ ty the type of the term to be let-bound
422 ||| @ ty the type of the term to be let-bound
393 ||| @ tm the term to be bound
423 ||| @ tm the term to be bound
394 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
425 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
395 letbind n ty tm = Prim__LetBind n ty tm
426 letbind n ty tm = Prim__LetBind n ty tm
397 ||| Normalise the goal.
428 ||| Normalise the goal.
398 compute : Elab ()
430 compute : Elab ()
399 compute = Prim__Compute
431 compute = Prim__Compute
@@ -402,12 +434,14 @@ namespace Tactics
403 ||| @ 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`)
404 ||| @ term the term to normalise
436 ||| @ term the term to normalise
405 normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
438 normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
406 normalise env term = Prim__Normalise env term
439 normalise env term = Prim__Normalise env term
408 ||| Reduce a closed term to weak-head normal form
441 ||| Reduce a closed term to weak-head normal form
410 ||| @ term the term to reduce
443 ||| @ term the term to reduce
411 whnf : (term : TT) -> Elab TT
445 whnf : (term : TT) -> Elab TT
412 whnf term = Prim__Whnf term
446 whnf term = Prim__Whnf term
@@ -417,6 +451,7 @@ namespace Tactics
417 ||| @ env a lexical environment to compare the terms in (see `getEnv`)
451 ||| @ env a lexical environment to compare the terms in (see `getEnv`)
418 ||| @ term1 the first term to convert
452 ||| @ term1 the first term to convert
419 ||| @ term2 the second term to convert
453 ||| @ term2 the second term to convert
420 convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab ()
455 convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab ()
421 convertsInEnv env term1 term2 = Prim__Converts env term1 term2
456 convertsInEnv env term1 term2 = Prim__Converts env term1 term2
@@ -424,14 +459,17 @@ namespace Tactics
425 ||| @ term1 the first term to convert
460 ||| @ term1 the first term to convert
426 ||| @ term2 the second term to convert
461 ||| @ term2 the second term to convert
427 converts : (term1, term2 : TT) -> Elab ()
463 converts : (term1, term2 : TT) -> Elab ()
428 converts term1 term2 = convertsInEnv !getEnv term1 term2
464 converts term1 term2 = convertsInEnv !getEnv term1 term2
430 ||| Find the source context for the elaboration script
466 ||| Find the source context for the elaboration script
431 getSourceLocation : Elab SourceLocation
468 getSourceLocation : Elab SourceLocation
432 getSourceLocation = Prim__SourceLocation
469 getSourceLocation = Prim__SourceLocation
434 ||| Attempt to solve the current goal with the source code location
471 ||| Attempt to solve the current goal with the source code location
435 sourceLocation : Elab ()
473 sourceLocation : Elab ()
436 sourceLocation = do loc <- getSourceLocation
474 sourceLocation = do loc <- getSourceLocation
437 fill (quote loc)
475 fill (quote loc)
@@ -442,6 +480,7 @@ namespace Tactics
443 ||| The namespace is represented as a reverse-order list of strings,
481 ||| The namespace is represented as a reverse-order list of strings,
444 ||| just as in the representation of names.
482 ||| just as in the representation of names.
445 currentNamespace : Elab (List String)
484 currentNamespace : Elab (List String)
446 currentNamespace = Prim__Namespace
485 currentNamespace = Prim__Namespace
@@ -455,16 +494,19 @@ namespace Tactics
455 ||| Because this tactic internally introduces a `let` binding, it
494 ||| Because this tactic internally introduces a `let` binding, it
456 ||| requires that the hole be immediately under its binder (use
495 ||| requires that the hole be immediately under its binder (use
457 ||| `attack` if it might not be).
496 ||| `attack` if it might not be).
458 rewriteWith : Raw -> Elab ()
498 rewriteWith : Raw -> Elab ()
459 rewriteWith rule = Prim__Rewrite rule
499 rewriteWith rule = Prim__Rewrite rule
461 ||| Add a type declaration to the global context.
501 ||| Add a type declaration to the global context.
462 declareType : TyDecl -> Elab ()
503 declareType : TyDecl -> Elab ()
463 declareType decl = Prim__DeclareType decl
504 declareType decl = Prim__DeclareType decl
465 ||| Define a function in the global context. The function must have
506 ||| Define a function in the global context. The function must have
466 ||| already been declared, either in ordinary Idris code or using
507 ||| already been declared, either in ordinary Idris code or using
467 ||| `declareType`.
508 ||| `declareType`.
468 defineFunction : FunDefn Raw -> Elab ()
510 defineFunction : FunDefn Raw -> Elab ()
469 defineFunction defun = Prim__DefineFunction defun
511 defineFunction defun = Prim__DefineFunction defun
@@ -472,12 +514,14 @@ namespace Tactics
473 ||| @ 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
474 ||| @ instName the name of the definition to use in implementation search
516 ||| @ instName the name of the definition to use in implementation search
475 addInstance : (ifaceName, instName : TTName) -> Elab ()
518 addInstance : (ifaceName, instName : TTName) -> Elab ()
476 addInstance ifaceName instName = Prim__AddInstance ifaceName instName
519 addInstance ifaceName instName = Prim__AddInstance ifaceName instName
478 ||| Determine whether a name denotes an interface.
521 ||| Determine whether a name denotes an interface.
480 ||| @ name a name that might denote an interface.
523 ||| @ name a name that might denote an interface.
481 isTCName : (name : TTName) -> Elab Bool
525 isTCName : (name : TTName) -> Elab Bool
482 isTCName name = Prim__IsTCName name
526 isTCName name = Prim__IsTCName name
@@ -485,10 +529,12 @@ namespace Tactics
486 ||| @ fn the name of the definition being elaborated (to prevent Idris
530 ||| @ fn the name of the definition being elaborated (to prevent Idris
487 ||| from looping)
531 ||| from looping)
488 resolveTC : (fn : TTName) -> Elab ()
533 resolveTC : (fn : TTName) -> Elab ()
489 resolveTC fn = Prim__ResolveTC fn
534 resolveTC fn = Prim__ResolveTC fn
491 ||| Use Idris's internal proof search.
536 ||| Use Idris's internal proof search.
492 search : Elab ()
538 search : Elab ()
493 search = Prim__Search 100 []
539 search = Prim__Search 100 []
@@ -496,6 +542,7 @@ namespace Tactics
497 ||| @ depth the search depth
543 ||| @ depth the search depth
498 ||| @ hints additional names to try
544 ||| @ hints additional names to try
499 search' : (depth : Int) -> (hints : List TTName) -> Elab ()
546 search' : (depth : Int) -> (hints : List TTName) -> Elab ()
500 search' depth hints = Prim__Search depth hints
547 search' depth hints = Prim__Search depth hints
@@ -505,6 +552,7 @@ namespace Tactics
505 ||| if the string is not a valid operator.
552 ||| if the string is not a valid operator.
507 ||| @ operator the operator string to look up
554 ||| @ operator the operator string to look up
508 operatorFixity : (operator : String) -> Elab Fixity
556 operatorFixity : (operator : String) -> Elab Fixity
509 operatorFixity operator = Prim__Fixity operator
557 operatorFixity operator = Prim__Fixity operator
@@ -512,6 +560,7 @@ namespace Tactics
513 ||| This is intended for elaboration script developers, not for
561 ||| This is intended for elaboration script developers, not for
514 ||| end-users. Use `fail` for final scripts.
562 ||| end-users. Use `fail` for final scripts.
515 debug : Elab a
564 debug : Elab a
516 debug = Prim__Debug []
565 debug = Prim__Debug []
@@ -522,18 +571,21 @@ namespace Tactics
522 ||| end-users. Use `fail` for final scripts.
571 ||| end-users. Use `fail` for final scripts.
524 ||| @ msg the message to display
573 ||| @ msg the message to display
525 debugMessage : (msg : List ErrorReportPart) -> Elab a
575 debugMessage : (msg : List ErrorReportPart) -> Elab a
526 debugMessage msg = Prim__Debug msg
576 debugMessage msg = Prim__Debug msg
528 ||| Create a new top-level metavariable to solve the current hole.
578 ||| Create a new top-level metavariable to solve the current hole.
530 ||| @ name the name for the top-level variable
580 ||| @ name the name for the top-level variable
531 metavar : (name : TTName) -> Elab ()
582 metavar : (name : TTName) -> Elab ()
532 metavar name = Prim__Metavar name
583 metavar name = Prim__Metavar name
534 ||| Recursively invoke the reflected elaborator with some goal.
585 ||| Recursively invoke the reflected elaborator with some goal.
536 ||| The result is the final term and its type.
587 ||| The result is the final term and its type.
537 runElab : Raw -> Elab () -> Elab (TT, TT)
589 runElab : Raw -> Elab () -> Elab (TT, TT)
538 runElab goal script = Prim__RecursiveElab goal script
590 runElab goal script = Prim__RecursiveElab goal script