<div dir="ltr"><div>Hi Jonathan,</div><div><br></div><div>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?<br></div><div><br></div><div>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.</div><div><br></div><div>The `mi_decls` field isn't the right place to look, these store dehydrated unfoldings. <br></div><div><br></div><div>Cheers,</div><div><br></div><div>Matt<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Aug 6, 2024 at 3:09 PM Jonathan Arnoult <<a href="mailto:jonathan.arnoult@tweag.io">jonathan.arnoult@tweag.io</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" id="m_7045378622917173808gmail-docs-internal-guid-ec2771e9-7fff-69d3-50ee-520dbb1d05b6"><span style="font-size:11pt;font-family:Arial,sans-serif;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">Hello,</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial,sans-serif;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">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.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial,sans-serif;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">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).</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial,sans-serif;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">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?</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial,sans-serif;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">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. </span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial,sans-serif;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">Any advice is appreciated.</span></p></div>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>