# Primitive Operators¶

gensym Generate a unique name based on some hint. Useful when establishing a new binder. NB: the generated name is unique for this run of the elaborator. Do not assume that they are globally unique. Signature: gensym : (hint : String) -> Elab TTName Substitute a guess into a hole. Substitute the focused guess throughout its scope, eliminating it and moving focus to the next element of the hole queue. Fail if the focus is not a guess. Signature: solve : Elab () Example: %language ElabReflection testFn : Nat testFn = %runElab (do fill (Z) solve)  Place a term into a hole, unifying its type. Fails if the focus is not a hole. Signature: fill : (e : Raw) -> Elab () Place a term e with type tc into the focused hole: ?h : th.e’ and convert it to a guess: ?h ≈ e:t.e’ and fail if the current focus is not a hole. The type t of the guess is constructed by unifying tc and th, which may instantiate holes that they refer to. Fail if the current focus is not a hole or if unification fails. This unification can result in the solution of further holes or the establishment of additional unsolved unification constraints. Example: %language ElabReflection testFn : Nat testFn = %runElab (do fill (Z) solve)  Attempt to apply an operator to fill the current hole, potentially solving arguments by unification. A hole is established for each argument. The return value is the list of holes established for the arguments to the function. Note that not all of the returned hole names still exist, as they may have been solved. @ op the term to apply @ argSpec - A list of booleans, one for each argument that the operator will be applied to. If true then attempt to solve the argument by unification. Signature: apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName) Example: elaborating an application of a function f that takes one implicit and two explicit arguments might invoke: apply (f) [False, True, True] Here is an example of an elab script that uses apply to insert the term plus Z (S Z) into a goal of type Nat. do [x,y] <- apply (plus) [False, False] solve focus x; fill (Z); solve focus y; fill (S Z); solve  The names of the established holes are returned. Note: This was added to the original tactic language to allow elaborator reflection. Attempt to apply an operator to fill the current hole, potentially solving arguments by matching. The return value is the list of holes established for the arguments to the function. Note that not all of the returned hole names still exist, as they may have been solved. @ op the term to apply @ argSpec instructions for finding the arguments to the term, where the Boolean states whether or not to attempt to solve the argument by matching. Signature: matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName) Move the focus to the specified hole, bringing it to the front of the hole queue. Fails if the hole does not exist. @ hole the hole to focus on Signature: focus : (hole : TTName) -> Elab () Send the currently-focused hole to the end of the hole queue and focus on the next hole. Signature: unfocus : TTName -> Elab () Convert a hole to make it suitable for bindings. The binding tactics require that a hole be directly under its binding, or else the scopes of the generated terms won’t make sense. This tactic creates a new hole of the proper form, and points the old hole at it. Signature: attack : Elab () Establish a new hole binding named n with type t, surrounding the current focus. Introduce a new hole with a specified name and type. The new hole will be focused, and the previously-focused hole will be immediately after it in the hole queue. Because this tactic introduces a new binding, you may need to ‘attack’ first. Signature: claim : TTName -> Raw -> Elab () Convert a hole into a pattern variable. Signature: patvar : TTName -> Elab () Normalise the goal. Often this is not necessary because normanisation is applied during other tactics. Signature: compute : Elab () Normalise a term in some lexical environment @ env the environment in which to compute (get one of these from getEnv) @ term the term to normalise Signature: normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT Reduce a closed term to weak-head normal form @ term the term to reduce Signature: whnf : (term : TT) -> Elab TT Check that two terms are convertible in the current context and in some environment. @ env a lexical environment to compare the terms in (see getEnv) @ term1 the first term to convert @ term2 the second term to convert Signature: convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab () Check that two terms are convertable in the current context and environment @ term1 the first term to convert @ term2 the second term to convertconverts : (term1, term2 : TT) -> Elab () converts term1 term2 = convertsInEnv !getEnv term1 term2 Find the source context for the elaboration script Signature: getSourceLocation : Elab SourceLocation Attempt to solve the current goal with the source code locationsourceLocation : Elab () sourceLocation = do loc <- getSourceLocation fill (quote loc) solve  Get the current namespace at the point of tactic execution. This allows scripts to define top-level names conveniently. The namespace is represented as a reverse-order list of strings, just as in the representation of names. Signature: currentNamespace : Elab (List String) Attempt to rewrite the goal using an equality. The tactic searches the goal for applicable subterms, and constructs a context for replace using them. In some cases, this is not possible, and replace must be called manually with an appropriate context. Because this tactic internally introduces a let binding, it requires that the hole be immediately under its binder (use ‘attack’ if it might not be). Signature: rewriteWith : Raw -> Elab () Attempt to solve the current goal with an interface dictionary @ fn the name of the definition being elaborated (to prevent Idris from looping) Signature: resolveTC : (fn : TTName) -> Elab () Use Idris’s internal proof search. Signature: search : Elab () Use Idris’s internal proof search, with more control. @ depth the search depth @ hints additional names to try Signature: search’ : (depth : Int) -> (hints : List TTName) -> Elab () Look up the declared fixity for an operator. The lookup fails if the operator does not yet have a fixity or if the string is not a valid operator. @ operator the operator string to look up Signature: operatorFixity : (operator : String) -> Elab Fixity Halt elaboration, dumping the internal state for inspection. This is intended for elaboration script developers, not for end-users. Use fail for final scripts. Signature: debug : Elab a If ‘debug’ is not the last tactic then make sure its type is sufficiently constrained. In particular, its type is Elab a, but there’s no way for Idris to find out which type was meant for a. This can be fixed by either writing an explicit type (e.g. debug {a = ()}) or by using a helper that constrains the type (such as simple in Pruviloj, e.g. simple debug as a line). %language ElabReflection idNat : Nat -> Nat idNat = %runElab (do intro {{x}} debug {a = ()} fill (Var {{x}}) solve)  Halt elaboration, dumping the internal state and displaying a message. This is intended for elaboration script developers, not for end-users. Use fail for final scripts. @ msg the message to display Signature: debugMessage : (msg : List ErrorReportPart) -> Elab a If ‘debugMessage’ is not the last tactic then make sure its type is sufficiently constrained. In particular, its type is Elab a, but there’s no way for Idris to find out which type was meant for a. This can be fixed by either writing an explicit type (e.g. debugMessage [TextPart “message”] {a = ()}) or by using a helper that constrains the type (such as simple in Pruviloj, e.g. simple debug as a line). %language ElabReflection idNat : Nat -> Nat idNat = %runElab (do intro {{x}} debugMessage [TextPart "error message"] {a = ()} fill (Var {{x}}) solve)  Create a new top-level metavariable to solve the current hole. @ name the name for the top-level variable Signature: metavar : (name : TTName) -> Elab () Recursively invoke the reflected elaborator with some goal. The result is the final term and its type. Signature: runElab : Raw -> Elab () -> Elab (TT, TT)

tryCatch tryCatch t (err => t’) will run t, and if it fails, roll back the elaboration state and run t’, but with access to the knowledge of why t failed. Signature: tryCatch : Elab a -> (Err -> Elab a) -> Elab a %language ElabReflection f : Err -> Elab () f (Msg _) = fill ("message error") f (CantUnify _ _ _ _ _ _) = fill ("unification error") f _ = fill ("other") s2 : String s2 = %runElab (do tryCatch (fill (True)) f ; solve)  Halt elaboration with an error Signature: fail : List ErrorReportPart -> Elab a Note: we may need to make sure the return type ‘a’ is sufficiently constrained. If required add an explicit type {a = ()}. Below is some code which includes ‘fail’. This will always fail but we could replace ‘True’ with some more useful condition. %language ElabReflection id1 : Elab () id1 = do intro {{x}} fill (Var {{x}}) if True then fail [TextPart "put error message here"] else solve idNat : Nat -> Nat idNat = %runElab id1