Compile Agda sections to Haskell sections

Main.hs

@@ -329,13 +329,9 @@ compileType t = do
     t -> genericDocError =<< text "Bad Haskell type:" <?> prettyTCM t
 
 compileTerm :: Term -> TCM (Hs.Exp ())
-compileTerm v =
+compileTerm v = do
   case unSpine v of
-    Var x es   -> do
-      cxt <- getContext
-      reportSDoc "agda2hs.compile" 10 $ text "context:" <+> fsep
-        [ prettyTCM (Var i []) | i <- reverse [0..length cxt - 1] ]
-      (`app` es) . Hs.Var () . Hs.UnQual () . hsName =<< showTCM (Var x [])
+    Var x es   -> (`app` es) . Hs.Var () . Hs.UnQual () . hsName =<< showTCM (Var x [])
     Def f es
       | Just semantics <- isSpecialTerm f -> semantics f es
       | otherwise -> (`app` es) . Hs.Var () =<< hsQName f
@@ -350,10 +346,14 @@ compileTerm v =
       hsLambda (absName b) <$> underAbstr_ b compileTerm
     Lam v b | visible v ->
       -- System-inserted lambda, no need to preserve the name.
-      -- TODO: most likely a section, so should really reconstruct that.
       underAbstraction_ b $ \ body -> do
         x <- showTCM (Var 0 [])
-        hsLambda x <$> compileTerm body
+        let hsx = Hs.Var () $ Hs.UnQual () (hsName x)
+        body <- compileTerm body
+        return $ case body of
+          Hs.InfixApp _ a op b
+            | a == hsx -> Hs.RightSection () op b -- System-inserted visible lambdas can only come from sections
+          _            -> hsLambda x body         -- so we know x is not free in b.
     Lam _ b -> underAbstraction_ b compileTerm
     t -> genericDocError =<< text "bad term:" <?> prettyTCM t
   where

test/AllTests.agda

@@ -3,12 +3,14 @@ module AllTests where
 
 import Issue14
 import Pragmas
+import Sections
 import Test
 import Tuples
 
 {-# FOREIGN AGDA2HS
 import Issue14
 import Pragmas
+import Sections
 import Test
 import Tuples
 #-}

test/Sections.agda

@@ -0,0 +1,17 @@
+
+module Sections where
+
+open import Haskell.Prelude
+
+test₁ : Nat → Nat
+test₁ = 5 +_
+
+test₂ : Nat → Nat
+test₂ = _+ 5
+
+test₃ : Nat → Nat
+test₃ = _+_ 5
+
+{-# COMPILE AGDA2HS test₁ #-}
+{-# COMPILE AGDA2HS test₂ #-}
+{-# COMPILE AGDA2HS test₃ #-}

test/golden/AllTests.hs

@@ -2,6 +2,7 @@ module AllTests where
 
 import Issue14
 import Pragmas
+import Sections
 import Test
 import Tuples
 

test/golden/Issue14.hs

@@ -4,8 +4,8 @@ constid :: a -> b -> b
 constid x = \ x -> x
 
 sectionTest₁ :: Integer -> Integer -> Integer
-sectionTest₁ n = \ section -> section + n
+sectionTest₁ n = (+ n)
 
 sectionTest₂ :: Integer -> Integer -> Integer
-sectionTest₂ section = \ section₁ -> section₁ + section
+sectionTest₂ section = (+ section)
 

test/golden/Sections.hs

@@ -0,0 +1,11 @@
+module Sections where
+
+test₁ :: Integer -> Integer
+test₁ = (5 +)
+
+test₂ :: Integer -> Integer
+test₂ = (+ 5)
+
+test₃ :: Integer -> Integer
+test₃ = (5 +)
+