add inlining pragma

[flupe]

Unboxed records lead to the definition of many functions (on the Agda side) that lift functionality to unboxed records by wrapping and unwrapping accordingly. However, once compiled this overhead disappears and the resulting output could be inlined.

This PR introduces the {-# COMPILE AGDA2HS name inline #-} pragma that tells agda2hs to do the inlining automatically. Underapplied inline functions will be eta-expanded so that the substitution still happens.

---

record Wrap (a : Set) : Set where
  constructor Wrapped
  field
    unwrap : a
open Wrap public
{-# COMPILE AGDA2HS Wrap unboxed #-}

mapWrap : (f : a → b) → Wrap a → Wrap b
mapWrap f (Wrapped x) = Wrapped (f x)
{-# COMPILE AGDA2HS mapWrap inline #-}

mapWrap2 : (f : a → b → c) → Wrap a → Wrap b → Wrap c
mapWrap2 f (Wrapped x) (Wrapped y) = Wrapped (f x y)
{-# COMPILE AGDA2HS mapWrap2 inline #-}

test1 : Wrap Int → Wrap Int
test1 x = mapWrap (1 +_) x
{-# COMPILE AGDA2HS test1 #-}

test2 : Wrap Int → Wrap Int → Wrap Int
test2 x y = mapWrap2 _+_ x y
{-# COMPILE AGDA2HS test2 #-}

-- partial application of inline function
test3 : Wrap Int → Wrap Int → Wrap Int
test3 x = mapWrap2 _+_ x
{-# COMPILE AGDA2HS test3 #-}

compiles to:

test1 :: Int -> Int
test1 x = 1 + x

test2 :: Int -> Int -> Int
test2 x y = x + y

test3 :: Int -> Int -> Int
test3 x = \ y -> x + y

---

Right now the names of the inserted lambdas come from the names given to the patterns in the inlined function. I suspect these could shadow names outside of where the inlined function is being used. Suggestions welcomed for making it more robust.

[flupe]

Noticed it can loop on some examples, need to fix it. Hm, seems to be caused by the fact that the record-pattern translation cannot happen if we match on one of the (erased) fields, even though inlining the Haskell code is morally fine. So we cannot use Agda's reduce machinery to do the inlining for us.

Gonna roll my own.

[jespercockx]

@flupe what's the status on this?

[flupe]

Getting back to this now.

[flupe]

Somehow #247 adding test/golden/Haskell/... made the CI unreliable, because the test themselves don't produce this file.
I thought we didn't cache test files but I removed the file anyway since this PR makes it unnecessary.

---

So the PR is ready. Instead of defining our own routine for inlining, we currently rely on Agda's unfoldDefinitionStep reduce function. This means we're overly conservative currently, as we forbid pattern-matching on anything other than unboxed records constructors.

It should be fine to allow pattern-matching on erased arguments (say, an equally type), but unfoldDefinitionStep would no longer unfold the function and we would have to implement our own matching routine. This is left for a next PR.

[jespercockx]

Thanks!