An example of manipulating FCs for hover text

TacticModeExample.idr

module TacticModeExample

import Language.Reflection
import Language.Reflection.TTImp

%default total

%language ElabReflection

unApp' : SnocList TTImp -> TTImp -> (TTImp, List TTImp)
unApp' sx (IApp fc f x) = unApp' (sx :< x) f
unApp' sx t = (t, cast sx)

unApp : TTImp -> (TTImp, List TTImp)
unApp = unApp' [<]

unfoldDo : TTImp -> Elab (List (FC, String, List TTImp))
unfoldDo = (map reverse) . go []
    where
        fromApp : TTImp -> Elab (FC, String, List TTImp)
        fromApp term = case unApp term of
            (IVar fc name, args) => pure (fc, show name, args)
            _ => failAt (getFC term) "invalid tactic"

        go : List (FC, String, List TTImp) -> TTImp -> Elab (List (FC, String, List TTImp))
        go acc term@(IApp _ (IApp _ func arg0) arg1) = if func == `((>>))
            then go (!(fromApp arg0) :: acc) arg1
            else pure $ !(fromApp term) :: acc
        go acc term = pure $ !(fromApp term) :: acc

runTactics : List (FC, String, List TTImp) -> Elab a
runTactics [] = fail "unsolved goals"
runTactics ((fc, "exact", [arg]) :: _) = check arg
runTactics ((fc, "hoverHere", _) :: ts) = do
    auxName <- genSym "aux"
    goalName <- genSym "goal"

    -- a fake context for illustration purposes
    let ty := `({x, y : Nat} -> x = y)

    declare [
        IClaim EmptyFC MW Private [] (MkTy EmptyFC EmptyFC auxName ty),
        IDef EmptyFC auxName [
            -- note that this uses the tactic's FC for the hole
            PatClause EmptyFC (IVar EmptyFC auxName) (IHole fc (show $ goalName))
        ]
    ]

    runTactics ts
runTactics ((fc, _, _) :: _) = failAt fc "unknown tactic"

tacticMode : TTImp -> Elab a
tacticMode term = do
    tactics <- unfoldDo term
    runTactics tactics

example : Nat -> Nat
example n = %runElab tacticMode `(do
    hoverHere
    exact (S n)
)