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.arno...@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@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
