How to get unfoldings inside a GHC plugin

[Matthew Pickering]

Hi Jonathan,

If you want to make sure unfoldings are available for all ids then you can
compile a module with `-fexpose-all-unfoldings`. Perhaps you have to
compile `base` and all GHC libraries with `-fexpose-all-unfoldings` as well?

Once you have an `Id`, you can look at the unfolding using
`realIdUnfolding`, this works the same whether it is from the home package
or not.

The `mi_decls` field isn't the right place to look, these store dehydrated
unfoldings.

Cheers,

Matt

On Tue, Aug 6, 2024 at 3:09 PM Jonathan Arnoult <jonathan.arnoult at tweag.io>
wrote:

> Hello,
>
> I am working on Liquid Haskell, and I'd like to use the unfoldings of
> definitions located in interface files to unfold them in proofs.
>
> Liquid Haskell is a GHC plugin that runs in the type checking phase at the
> moment, and for analysis purposes it also compiles the module down to Core.
> I have found that unfolding information is available in the mi_decls field
> of ModIface, and in the field realUnfoldingInfo of IdInfo. However, my
> first attempts to grab for these fields yield no unfoldings either because
> they have been erased (mi_decls is filled with an error call in
> loadInterface) or they were not constructed to begin with
> (realUnfoldingInfo is set to NoUnfolding).
>
> In my setting, I have the name of a function, and I would need to retrieve
> the unfoldings (if they exist) from some environment. Does this environment
> exist already that is reachable to a plugin? Or do I need to construct it
> somehow?
>
> I also found that GHC makes a distinction between interface files in
> external packages and the home package, while I really would like to get
> the unfolding from wherever they happen to be.
>
> Any advice is appreciated.
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20240806/bd3d99d2/attachment.html>