Compile sections

HsUtils.hs

@@ -52,11 +52,14 @@ pApp c@(UnQual () (Symbol () _)) [p, q] = PInfixApp () p c q
 pApp c@(Special () Cons{}) [p, q] = PInfixApp () p c q
 pApp c ps = PApp () c ps
 
+getOp :: Exp () -> Maybe (QOp ())
+getOp (Var _ x) | isOp x = Just $ QVarOp () x
+getOp (Con _ c) | isOp c = Just $ QConOp () c
+getOp _                  = Nothing
+
 eApp :: Exp () -> [Exp ()] -> Exp ()
 eApp f (a : b : as) | Just op <- getOp f = foldl (App ()) (InfixApp () a op b) as
-  where getOp (Var _ x) | isOp x = Just $ QVarOp () x
-        getOp (Con _ c) | isOp c = Just $ QConOp () c
-        getOp _                  = Nothing
+eApp f [a]          | Just op <- getOp f = LeftSection () a op
 eApp f es = foldl (App ()) f es
 
 tApp :: Type () -> [Type ()] -> Type ()
@@ -72,7 +75,7 @@ hsLambda x e =
     p = PVar () $ hsName x
 
 getExplicitImports :: ImportSpec l -> [String]
-getExplicitImports = map pp . \case 
+getExplicitImports = map pp . \case
   IVar _ n -> [n]
   IAbs _ _ n -> [n]
   IThingAll _ n -> [n]

Main.hs

@@ -181,6 +181,7 @@ isSpecialName = show >>> \ case
     "Agda.Builtin.Unit.⊤"          -> special Hs.UnitCon
     "Agda.Builtin.Unit.tt"         -> special Hs.UnitCon
     "Haskell.Prelude.Tuple.[]"     -> special Hs.UnitCon
+    "Haskell.Prelude._∘_"          -> unqual "_._"
     _ -> Nothing
   where
     unqual n  = Just $ Hs.UnQual () $ hsName n
@@ -330,11 +331,7 @@ compileType t = do
 compileTerm :: Term -> TCM (Hs.Exp ())
 compileTerm v =
   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
@@ -349,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

lib/Haskell/Prelude.agda

@@ -1,4 +1,4 @@
-
+{-# OPTIONS --no-auto-inline #-}
 module Haskell.Prelude where
 
 open import Agda.Builtin.Unit  public
@@ -13,6 +13,18 @@ open import Agda.Builtin.Char  public
 variable
   a b c d e f g h i j k l m n o p q r s t u v w x y z : Set
 
+-- Functions --
+
+id : a → a
+id x = x
+
+infixr 9 _∘_
+_∘_ : (b → c) → (a → b) → a → c
+(f ∘ g) x = f (g x)
+
+flip : (a → b → c) → b → a → c
+flip f x y = f y x
+
 -- Tuples --
 
 infixr 5 _∷_

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,25 @@
+
+module Sections where
+
+open import Haskell.Prelude
+
+test₁ : Nat → Nat
+test₁ = 5 +_
+
+test₂ : Nat → Nat
+test₂ = _+ 5
+
+test₃ : Nat → Nat
+test₃ = _+_ 5
+
+test₄ : Nat → Nat
+test₄ = λ x → x + 5
+
+test₅ : Nat → Nat
+test₅ = λ x → 5 + x -- Agda eta-contracts this before we get to see it
+
+{-# COMPILE AGDA2HS test₁ #-}
+{-# COMPILE AGDA2HS test₂ #-}
+{-# COMPILE AGDA2HS test₃ #-}
+{-# COMPILE AGDA2HS test₄ #-}
+{-# COMPILE AGDA2HS test₅ #-}

test/Test.agda

@@ -91,6 +91,10 @@ map f [] = []
 map f (x ∷ xs) = f x ∷ map f xs
 {-# COMPILE AGDA2HS map #-}
 
+mapTest : List Nat → List Nat
+mapTest = map (id ∘ _+_ 5)
+{-# COMPILE AGDA2HS mapTest #-}
+
 -- ** Lambdas
 
 plus3 : List Nat → List Nat

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,17 @@
+module Sections where
+
+test₁ :: Integer -> Integer
+test₁ = (5 +)
+
+test₂ :: Integer -> Integer
+test₂ = (+ 5)
+
+test₃ :: Integer -> Integer
+test₃ = (5 +)
+
+test₄ :: Integer -> Integer
+test₄ = \ x -> x + 5
+
+test₅ :: Integer -> Integer
+test₅ = (5 +)
+

test/golden/Test.hs

@@ -53,6 +53,9 @@ map :: (a -> b) -> [a] -> [b]
 map f [] = []
 map f (x : xs) = f x : map f xs
 
+mapTest :: [Integer] -> [Integer]
+mapTest = map (id . (5 +))
+
 plus3 :: [Integer] -> [Integer]
 plus3 = map (\ n -> n + 3)