Public export TTImp reflection functions

[madman-bob]

This allows using these functions in elaborator scripts.

I want to use mapMTTImp in a script, but people could plausibly want to use any of them.

[buzden]

Does using import public Language.Reflection.TTImp in the module with your elaboration script help instead of this change? I don't remember any problems with using mapTTImp and mapMTTImp from inside elaboration scripts, considering the issue #2439 (especially what's written in the comments section regarding to import public).

[madman-bob]

I already had import public before this.

Digging more deeply, the problem wasn't the script itself, but using the result of a script at the type-level.

Here's a simplified example of what I was trying to achieve, without even using a script:

import Control.Monad.State

import Language.Reflection

addName : TTImp -> State (List String) TTImp
addName v@(IVar fc (UN (Basic nm))) = do
    modify (nm ::)
    pure v
addName s = pure s

names : TTImp -> List String
names s = execState [] $ mapMTTImp addName s

checkNames : names `(x * y) = ["y", "x", "*"]
checkNames = Refl