beta-reducing method applications?

(Sorry for asking this here, I can't find a mailing list for users)

After some number of repeated inlineR, betaReduceR and caseReduceUnfoldR Trues, HERMIT is transforming a program to:

(+ @ Int
   (D:Num
      @ Int
      (\ (ds_a1nJ [Occ=Once!] :: Int) (ds1_a1nK [Occ=Once!] :: Int) ->
         case ds_a1nJ of _ [Occ=Dead] { I# x_a1nN [Occ=Once] ->
         case ds1_a1nK of _ [Occ=Dead] { I# y_a1nR [Occ=Once] ->
         I# (+# x_a1nN y_a1nR)
         }
         })
      (\ (ds_a1nT [Occ=Once!] :: Int) (ds1_a1nU [Occ=Once!] :: Int) ->
         case ds_a1nT of _ [Occ=Dead] { I# x_a1nX [Occ=Once] ->
         case ds1_a1nU of _ [Occ=Dead] { I# y_a1o1 [Occ=Once] ->
         I# (-# x_a1nX y_a1o1)
         }
         })
      (\ (ds_a1o3 [Occ=Once!] :: Int) (ds1_a1o4 [Occ=Once!] :: Int) ->
         case ds_a1o3 of _ [Occ=Dead] { I# x_a1o7 [Occ=Once] ->
         case ds1_a1o4 of _ [Occ=Dead] { I# y_a1ob [Occ=Once] ->
         I# (*# x_a1o7 y_a1ob)
         }
         })
      (\ (ds_a1od [Occ=Once!] :: Int) ->
         case ds_a1od of _ [Occ=Dead] { I# x_a1og [Occ=Once] ->
         I# (negateInt# x_a1og)
         })
      (\ (n_a1oi [Occ=Once!] :: Int) ->
         case n_a1oi of _ [Occ=Dead] { I# x_a1ol ->
         case tagToEnum# @ Bool (>=# x_a1ol 0) of _ [Occ=Dead] {
           False -> I# (negateInt# x_a1ol);
           True -> I# x_a1ol
         }
         })
      (\ (n_a1os [Occ=Once!] :: Int) ->
         case n_a1os of _ [Occ=Dead] { I# x_a1ov ->
         case tagToEnum# @ Bool (<# x_a1ov 0) of _ [Occ=Dead] {
           False ->
             case x_a1ov of _ [Occ=Dead] {
               __DEFAULT -> I# 1;
               0 -> I# 0
             };
           True -> I# (-1)
         }
         })
      (\ (i_a1oG :: Integer) ->
         case integerToInt i_a1oG of _ [Occ=Dead] { __DEFAULT ->
         I# (integerToInt i_a1oG)
         }))
   (I# 1)
   (I# 2))

At this point it gets stuck, but I'd like to make some more progress here. Typeclass dictionary is already resolved, so it shouldn't be too hard to find method RHS and reduce generic + to:

(\ (ds_a1nJ [Occ=Once!] :: Int) (ds1_a1nK [Occ=Once!] :: Int) ->
         case ds_a1nJ of _ [Occ=Dead] { I# x_a1nN [Occ=Once] ->
         case ds1_a1nK of _ [Occ=Dead] { I# y_a1nR [Occ=Once] ->
         I# (+# x_a1nN y_a1nR)
         }
         })

Then betaReduceR and caseReduceUnfoldR could work further and reduce the whole thing to:

I# 3

Is there a way to do that?

Thanks.

(There isn't a mailing list... reporting here on Github issues is great. Or your can email me directly if you prefer. Also, thanks for trying HERMIT!)

If you focus on the application of + and attempt to inline or unfold, does it give an error message about there not being an unfolding available? I would have expected the + to inline just fine.

If you have an example target program and script, I can try it out.

For instance, using the following target program:

main :: IO ()
main = print (2 + (3::Int))

I can:

$ hermit Math.hs
hermit<0> rhs-of 'main
print ▲ $fShowInt ((+) ▲ $fNumInt (I# 2) (I# 3))
hermit<1> app-arg
(+) ▲ $fNumInt (I# 2) (I# 3)
hermit<2> repeat (any-td (unfold <+ case-reduce-unfold))
case I# 2 of wild ▲
  I# x →
    case I# 3 of wild1 ▲
      I# y → I# ((+#) x y)

As for actually evaluating those case expressions to I# 5, I don't believe we have implemented any rewrites for actual primitive arithmetic yet. It wouldn't be hard to do, though I would check to see if GHC has that implemented somewhere that we can just lift into a HERMIT rewrite.

I just tried same commands but they produced different results:

➜  pe-plugin git:(master) ✗ cat hermit_test.hs
main :: IO ()
main = print (2 + (3 :: Int))
➜  pe-plugin git:(master) ✗ hermit hermit_test.hs
[starting HERMIT v1.0.0.1 on hermit_test.hs]
% ghc hermit_test.hs -fforce-recomp -O2 -dcore-lint -fsimple-list-literals -fexpose-all-unfoldings -fplugin=HERMIT -fplugin-opt=HERMIT:*:
[1 of 1] Compiling Main             ( hermit_test.hs, hermit_test.o )
===================== Welcome to HERMIT ======================
HERMIT is a toolkit for the interactive transformation of GHC
core language programs. Documentation on HERMIT can be found
on the HERMIT web page at:
http://www.ittc.ku.edu/csdl/fpg/software/hermit.html

You have just loaded the interactive shell. To exit, type 
"abort" or "resume" to abort or resume GHC compilation.

Type "help" for instructions on how to list or search the
available HERMIT commands.

To get started, you could try the following:
  - type "binding-of 'foo", where "foo" is a function
    defined in the module;
  - type "set-pp-type Show" to display full type information;
  - type "info" for more information about the current node;
  - to descend into a child node, type the name of the child
    ("info" includes a list of children of the current node);
  - to ascend, use the "up" command;
  - type "log" to display an activity log.
==============================================================

module Main where
  main ∷ IO ()
  main ∷ IO ()
hermit<0> rhs-of 'main
print ▲ $fShowInt ((+) ▲ $fNumInt (I# 2) (I# 3))
hermit<1> app-arg
(+) ▲ $fNumInt (I# 2) (I# 3)
hermit<2> repeat (any-td (unfold <+ case-reduce-unfold))
(+) ▲
    (D:Num ▲
           (λ ds ds1 →
              case ds of wild ▲
                I# x →
                  case ds1 of wild1 ▲
                    I# y → I# ((+#) x y))
           (λ ds ds1 →
              case ds of wild ▲
                I# x →
                  case ds1 of wild1 ▲
                    I# y → I# ((-#) x y))
           (λ ds ds1 →
              case ds of wild ▲
                I# x →
                  case ds1 of wild1 ▲
                    I# y → I# ((*#) x y))
           (λ ds →
              case ds of wild ▲
                I# x → I# (negateInt# x))
           (λ n →
              case n of wild ▲
                I# x →
                  case tagToEnum# ▲ ((>=#) x 0) of wild1 ▲
                    False → I# (negateInt# x)
                    True → I# x)
           (λ n →
              case n of wild ▲
                I# x →
                  case tagToEnum# ▲ ((<#) x 0) of wild1 ▲
                    False →
                      case x of wild2 ▲
                        _ → I# 1
                        0 → I# 0
                    True → I# (-1))
           (λ i →
              case integerToInt i of wild ▲
                _ → I# (integerToInt i)))
    (I# 2) (I# 3)
hermit<3>

HERMIT version:

[starting HERMIT v1.0.0.0 on --version]
% ghc --version -fforce-recomp -O2 -dcore-lint -fsimple-list-literals -fexpose-all-unfoldings -fplugin=HERMIT -fplugin-opt=HERMIT:*:
The Glorious Glasgow Haskell Compilation System, version 7.10.1

I also tried HEAD version but got same results. Could it be related with GHC version?

Interesting... I'm guessing the version of base that ships with 7.10 provides different unfolding information than it did with 7.8 (what I'm using). I'll set up 7.10 tonight and try.

That is most unfortunate. If you unfold instead of the repeat ... line, what error is given?

ku-fpg / hermit

beta-reducing method applications? #140