Substituting from context bindings?

[conal]

Can I somehow a HERMIT context (with bindings added) to substitute type variable bindings into a type with variables? I've carefully gathered up bindings, and I want to apply them when I reach a type. I could instead do the substitution eagerly instead of saving the bindings, but then I'd make multiple passes, and I'm going for a very efficient implementation. I could instead add bindings to a Core Subst and pass it explicitly, but it seems redundant with the context mechanism.

[xich]

I'm not sure I quite understand what you want to do.

If you want to extend the context with your own information, you can use:

http://hackage.haskell.org/package/kure-2.16.12/docs/Language-KURE-ExtendableContext.html

We should have most of our operations abstracted so they will work over an arbitrary ExtendedContext, but let me know if you run into snags. There are probably some helpful projection/injection functions we could write to lift a rewrite over HermitC into a rewrite over ExtendedContext HermitC e.

If you want to substitute, you can use substCoreExpr in HERMIT.Core to invoke GHC`s substitution algorithm. For types, you would call it something like:

foo :: RewriteH Type
foo = 
  transform $ \ c ty -> 
    let tv = ... some tyvar ...
        ty' = ... some type ...
    let Type rty = substCoreExpr  tv (Type ty') (Type ty)
    return rty

If you're pulling the tv and ty' directly from the context though, you probably just want to use inlineR with some kind of guard in the front:

isVarsT :: [Var] -> TransformH CoreExpr ()
isVarsT vs = anyM (map (\v -> varT (== v)) vs) >>= guardM

isVarsT some_vs >> inlineR