Axiomatizations aren't exported across modules

[RyanGlScott]

Tracking a feature that we've (which includes at least @rrnewton, @vikraman, and I) desired for a while: the ability to use axiomatize in one module, and be able to reference that axiomatized definition in another module.

The issue is that LH needs access to the Core definition of the axiom in order to use it in the module. @ranjitjhala proposed this step for figuring out how to integrate such a feature into Liquid Haskell:

1. Write a function emitHI which turns a Haskell file into the contents of an .hi file
2. Write a function displayHI which displays the .hi contents in a digestible format.

It might help to compile functions that have INLINEABLE annotations, since this program will tell GHC to put its unfoldings into the .hi file.

521 seems related, as @nikivazou noted that measures also need to be exported in a similar fashion.

[gridaphobe]

I wonder if we can just construct the axiomatization/measure directly from the unfolding, and bypass any fiddling with the .hi files ourselves? It should be possible, since the unfolding is supposed to be an unoptimized version of the Core.

[ranjitjhala]

We need the .hi file because, in general when analyzing module B (that imports A) we need to get a hold of the core (from reflected binders in) A, which we hope to get from the .hi file (because thats guaranteed to exist when compiling B).

On Mon, Oct 10, 2016 at 1:02 PM, Eric Seidel notifications@github.com wrote:

I wonder if we can just construct the axiomatization/measure directly from the unfolding, and bypass any fiddling with the .hi files ourselves? It should be possible, since the unfolding is supposed to be an unoptimized version of the Core.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/851#issuecomment-252731290, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuON11DfD-_23vpnf_xqDSn-bOvOnHks5qypnXgaJpZM4KS7X3 .

[gridaphobe]

Yes, but GHC will take care of that for us. I'm just suggesting we can avoid looking at (or modifying) the .hi ourselves if we just ask GHC for a function's unfolding.

[ranjitjhala]

The point here is not to modify the .hi at all, just to get a small standalone program that shows

1. how to use annotations to save the CORE in the .hi file,
2. how to use the GHC API to access the CORE from the .hi file.

On Mon, Oct 10, 2016 at 1:10 PM, Eric Seidel notifications@github.com wrote:

Yes, but GHC will take care of that for us. I'm just suggesting we can avoid looking at (or modifying) the .hi ourselves if we just ask GHC for a function's unfolding.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/851#issuecomment-252733066, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOMYRLY6r3y-kGmm5PJg-PDGxni3jks5qypvQgaJpZM4KS7X3 .

[gridaphobe]

But the CORE is already there for INLINABLE functions! It's stored as something GHC calls an "unfolding" so it can be inlined in client modules.

My point is that (1) should be unnecessary, and (2) should be a matter of asking GHC for the unfolding for a given function.

[ranjitjhala]

But the CORE is already there for

"There" is where?

—

You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/851#issuecomment-252742135, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOLhL7DrlPX6pnEj38GmM6XtF3PTZks5qyqTdgaJpZM4KS7X3 .

[gridaphobe]

In the .hi file. We should be able to use

Id.idUnfolding :: Id -> Unfolding
CoreSyn.expandUnfolding_maybe :: Unfolding -> Maybe CoreExpr

to extract the rhs of functions for which GHC keeps the Core. (This can be controlled by marking functions as INLINEABLE.)

[RyanGlScott]

Here's a script (LoadFromHI.hs) that loads an .hi file, finds all top-level Ids, typechecks their IfaceUnfoldings, and prints out the resulting CoreExprs:

#!/usr/bin/env stack
{- stack
    --resolver lts-6.9
    --install-ghc runghc
    --package ghc
-}

{-# LANGUAGE PatternGuards #-}
module Main (main) where

import BinIface
import DynFlags
import GHC
import HscMain
import IfaceSyn
import TcIface
import TcRnMonad
import Outputable

import Data.Foldable (forM_)
import System.Environment (getArgs)

main :: IO ()
main = do
  fp:_ <- getArgs
  go fp

go :: FilePath -> IO ()
go fp = do
  e <- newHscEnv unsafeGlobalDynFlags
  initTcRnIf 'i' e undefined undefined $ do
    miface <- readBinIface IgnoreHiWay QuietBinIFaceReading fp

    forM_ (mi_decls miface) $ \(_, if_decl) -> case if_decl of
      IfaceId { ifName = if_name, ifIdInfo = HasInfo if_info_items }
        | let if_info_unfoldings = filter isHsUnfold if_info_items
        , not (null if_info_unfoldings)
        -> do pprLn if_name
              forM_ if_info_unfoldings $ \(HsUnfold _ if_unfold) -> case if_unfold of
                IfCoreUnfold _ if_expr     -> tcIfaceExprAndPrint if_expr
                IfCompulsory if_expr       -> tcIfaceExprAndPrint if_expr
                IfInlineRule _ _ _ if_expr -> tcIfaceExprAndPrint if_expr
                _ -> return ()
      _ -> return ()
  where
    tcIfaceExprAndPrint :: IfaceExpr -> IfM IfLclEnv ()
    tcIfaceExprAndPrint ife = do
      ce <- tcIfaceExpr ife
      liftIO $ putStr "  "
      pprLn ce

isHsUnfold :: IfaceInfoItem -> Bool
isHsUnfold (HsUnfold{}) = True
isHsUnfold _            = False

pprLn :: (MonadIO m, Outputable a) => a -> m ()
pprLn = liftIO . putStrLn . showSDocUnsafe . ppr

On an example file:

module Example where                                                                      

foo1, foo2, foo3 :: Int                                                                   
foo1 = 1                                                                                  
foo2 = 2                                                                                  
foo3 = 3                                                                                  

{-# INLINE foo2 #-}                                                                       
{-# INLINEABLE foo3 #-}

$ ghc -O Example.hs 
[1 of 1] Compiling Example          ( Example.hs, Example.o )
$ runghc "-package ghc" LoadFromHI.hs Example.hi
foo1
  I# 1
foo2
  I# 2
foo3
  I# 3

Of course, this example won't scale up because I'm passing undefined for the global and local environments to initTcRnIf. I'm hoping (?) that LH has these values available somewhere.