ku-fpg / hermit

Haskell Equational Reasoning Model-to-Implementation Tunnel
http://www.ittc.ku.edu/csdl/fpg/Tools/HERMIT
BSD 2-Clause "Simplified" License
49 stars 8 forks source link

Unfolding class methods? #157

Closed conal closed 8 years ago

conal commented 8 years ago

I'm unable to unfold or inline class methods in the latest HERMIT. Did something change? Is there a way to get methods inlined? An example:

...
hermit<0> application-of 'negate
negate Int $fNumInt
hermit<2> unfold
Error in expression: unfold
Rewrite failed:unfold failed: Inline failed: not a variable.
hermit<2> occurrence-of 'negate
negate
hermit<3> inline
Error in expression: inline
Rewrite failed:Inline failed: cannot find unfolding in Env or IdInfo.
hermit<3> info
Node:        Expression
Constructor: Var
Type:        forall a. Num a => a -> a

OccName:                  negate
Global: GHC.Num
Unique:                   02J
Identifier arity:         1
Identifier binding depth: binding not found in HERMIT context.
Unfolding:                No unfolding
Occurrence Info:          
Inline Pragmas:           [ALWAYS]

Path:     [prog, prog-tail, prog-tail, prog-tail, prog-tail, prog-tail, prog-head, nonrec-rhs, app-fun, app-fun]
Children: []

Free local identifiers:  
Free global identifiers: negate
Free type variables:     
Free coercion variables: 
Local bindings in scope: 
  trip2 : 4$NONREC
  trip1 : 1$NONREC
  repr1 : 5$NONREC
  ar1 : 3$NONREC
  abst1 : 2$NONREC

I'm using GHC 7.10.3.

conal commented 8 years ago

Am I crazy here? I don't remember having difficulty with inlining methods (into dictionary accessors) before.

xich commented 8 years ago

I'll have to investigate, but I likely won't have time until the weekend after next. :-(

It is possible the inlining annotations on negate changed with the new base package included in 7.10 (vs 7.8), or that 7.10 makes different decisions on what to export in interface files. The lack of unfolding info is the next big thing I'd like to tackle with HERMIT, but it will require a GHC patch, so may take a while to solve (especially with my now-reduced bandwidth).

conal commented 8 years ago

I don't know if it's even possible to declare anything about inlining of the general methods (dictionary accessors), as opposed to methods for particular instances. That's a weird thing here --- I'm just trying to expose the dictionary accessor. I can inline the dictionary, but not the accessor:

hermit<0> application-of 'negate
negate Int $fNumInt
hermit<1> [app-fun,app-fun]
negate
hermit<2> inline
Error in expression: inline
Rewrite failed:Inline failed: cannot find unfolding in Env or IdInfo.
hermit<2> back
back, unstepping : [app-fun,app-fun]
negate Int $fNumInt
hermit<1> app-arg
$fNumInt
hermit<3> inline
D:Num Int $fNumInt_$c+ $fNumInt_$c- $fNumInt_$c* $fNumInt_$cnegate
      $fNumInt_$cabs $fNumInt_$csignum $fNumInt_$cfromInteger
hermit<4> 

Thanks for letting me know about your limited availability. I wonder if anyone else could help. I'm totally blocked at this point.

conal commented 8 years ago

Are there any other active HERMIT users working with the new version?

ecaustin commented 8 years ago

I ran into this exact issue with my dissertation work. My short-term workaround was to redefine the class methods I needed locally. For example, given the module:

negate' :: Num a => a -> a
negate' x = 0 - x

f :: Int -> Int
f x = negate' x

main = print (f 1)

I can get inlining to work as desired:

hermit<0> rhs-of 'f
λ x → negate' ▲ $fNumInt x
hermit<1> any-call (unfold 'negate')
λ x → (-) ▲ $fNumInt (fromInteger ▲ $fNumInt (__integer 0)) x

I know it's not an ideal solution, but maybe this is enough to make progress until Drew has time to investigate more?

conal commented 8 years ago

Thanks, @ecaustin. I really do need to get to the methods themselves. For instance, in your code, I then would need to inline the '-' accessor for Num dictionaries, but I run into the same roadblock.

What versions of GHC and HERMIT were you using when you encountered the problem with method/accessor inlining? It worked fine for me under GHC 7.8 and HERMIT 0.5.

conal commented 8 years ago

I also tried simplify and bash to no avail:

hermit<0> application-of 'negate
negate Int $fNumInt
hermit<1> app-arg
$fNumInt
hermit<2> inline
D:Num Int $fNumInt_$c+ $fNumInt_$c- $fNumInt_$c* $fNumInt_$cnegate
      $fNumInt_$cabs $fNumInt_$csignum $fNumInt_$cfromInteger
hermit<3> up
negate Int
       (D:Num Int $fNumInt_$c+ $fNumInt_$c- $fNumInt_$c* $fNumInt_$cnegate
              $fNumInt_$cabs $fNumInt_$csignum $fNumInt_$cfromInteger)
hermit<4> simplify
Error in expression: simplify
Rewrite failed:Simplify failed: nothing to simplify.
hermit<4> bash
Error in expression: bash
Rewrite failed:bash failed: nothing to do.
hermit<4> 
conal commented 8 years ago

I just asked on the ghc-devs mailing list whether something about method accessor inlining changed between GHC 7.8.2 and 7.10.3.

ecaustin commented 8 years ago

Right, in this specific example you'd have to follow the turtles all the way down. You would need to monomorphise negate and provide a corresponding local redefinition of (-) which would pollute your code with magic hashes and primitive operations.

Again, not an ideal solution, but you should get to the same end point since you are essentially doing manually what HERMIT would have done for you automatically.

conal commented 8 years ago

I see. What I'm working on is (automatic) monomorphization. I'm rebuilding my Haskell-to-hardware compiler to make it simpler, more robust, and much faster; and monomorphization is the first phase.

ecaustin commented 8 years ago

Yikes. So doing the transformations manually would prevent any meaningful development or testing of at least the first phase of your compiler. Makes sense now why this is a major stopping point for you.

Looking at the .cabal files from my dissertation work, I was using GHC 7.8.x and HERMIT 1.0.0.0.

That's the only version of HERMIT I've ever worked with, so I've just taken it at face value that the bindings from class instances weren't carried in the HERMIT context. I wasn't aware that functionality was available in earlier versions of HERMIT.

xich commented 8 years ago
module Main where

main = print $ negate (1::Int)

If I run hermit Test.hs, I can't inline negate. If I start HERMIT after the first phase, then negate has already been inlined: hermit Test.hs +Main -p1

negate has an INLINE pragma on it, so this makes sense. Evidently GHC is finding the unfolding for negate somewhere. (ghc Test.hs -O2 -ddump-simpl-iterations supports this) Must figure out how it is doing so and why HERMIT can't see it. It could be the case that the IdInfo is just underspecified (or conservatively specified) when it comes out of the desugarer, and it gets filled in later. (by default, HERMIT runs directly after the desugarer, and before any other optimization passes)

xich commented 8 years ago

It is also possible that HERMIT is zapping the IdInfo somewhere. I remember Neil adding some zapping stuff. Investigating that now.

conal commented 8 years ago

Looking at the .cabal files from my dissertation work, I was using GHC 7.8.x and HERMIT 1.0.0.0.

Thanks. Interesting. This info suggests to me that the problem is in HERMIT, introduced between HERMIT 0.5 and 1.0, rather than in GHC between 7.8 and 7.10.

xich commented 8 years ago

Okay, I think what is happening is that GHC doesn't generate an unfolding for negate... it generates a magic BuiltInRule:

$ ghc -O2 Test.hs -ddump-rule-rewrites
[1 of 1] Compiling Main             ( Test.hs, Test.o )
Rule fired
    Rule: Class op negate
    Before: GHC.Num.negate
              TyArg GHC.Types.Int ValArg GHC.Num.$fNumInt ValArg GHC.Types.I# 1
    After:  GHC.Num.$fNumInt_$cnegate
    Cont:   Stop[BoringCtxt] GHC.Types.Int

So we at minimum need to add support for applying built-in rules... and potentially use them as an unfolding fallback.

ecaustin commented 8 years ago

For what it's worth, it doesn't seem to matter if the class instance is local vs. imported. A dummy, local redefinition:

class Num a => Num' a where
  negate' :: a -> a
  negate' x = 0 - x

instance Num' Int

Still doesn't populate the HERMIT context with its binding information: Identifier binding depth: binding not found in HERMIT context.

I can see the binding at the top level, though, and I can unfold that:

module Main where
  $dmnegate' ∷ ∀ a . Num' a → a → a
  $fNum'Int ∷ Num' Int
  $cnegate' ∷ Int → Int
  f ∷ Int → Int
  main ∷ IO ()
  main ∷ IO ()
hermit<0> occurrence-of '$cnegate' 
$cnegate'
hermit<1> unfold
$dmnegate' ▲ $fNum'Int

My HERMIT skills are a bit rusty. Is there anyway to substitute $cnegate for negate' in the rhs of 'f in this example, such that you could use local class redefinitions as a workaround?

hermit<2> top
hermit<3> rhs-of 'f
λ x → negate' ▲ $fNum'Int x

At least until Drew or whoever has time to hack in using built-in rules as an alternative unfolding mechanism?

xich commented 8 years ago

Note to self:

https://github.com/ghc/ghc/blob/f3cc34568b13abb29de7b54a5f657681e9e116ca/compiler/basicTypes/MkId.hs#L291

Edit: Given this Note, it looks like that is exactly the problem.

https://github.com/ghc/ghc/blob/2db18b8135335da2da9918b722699df684097be9/compiler/typecheck/TcInstDcls.hs#L158

ecaustin commented 8 years ago

On a related note, @conal, I'm going to send you an introductory email when I get back to my office tomorrow.

I've been doing some initial research into (possibly) using HERMIT as part of a Haskell-to-hardware workflow, though my focus is much less general than what you're trying to do with circat.

xich commented 8 years ago

@conal I created a separate issue (#159) outlining my plan to fix this. I should have this done tomorrow.

conal commented 8 years ago

@xich That's wonderful. Thanks very much for the help, and sorry to keep you up late.

xich commented 8 years ago

I just pushed a commit which should fix this for you. Please let me know if you run into problems!

conal commented 8 years ago

@xich eee34d4c8c04505e9081bdb615cddf35d40446e9 works great! I'm unstuck now. I sure appreciate your help.

hermit<0> rhs-of 'addI
\ x -> (+) Int $fNumInt x (I# 3)
hermit<1> bash
Error in expression: bash
Rewrite failed:bash failed: nothing to do.
hermit<1> lam-body
(+) Int $fNumInt x (I# 3)
hermit<2> unfold
(case $fNumInt of tpl (Int -> Int -> Int)
   D:Num tpl tpl tpl tpl tpl tpl tpl -> tpl) x (I# 3)

W00t!