From e5f84d927c6343d0df5f940380e03348d1fdc354 Mon Sep 17 00:00:00 2001
From: Ulf Norell <ulf.norell@gmail.com>
Date: Thu, 22 Oct 2020 15:37:37 +0200
Subject: [PATCH] Compile lambdas

---
 Main.hs   | 10 ++++++++++
 README.md |  1 -
 Test.agda | 10 ++++++++++
 3 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/Main.hs b/Main.hs
index 8811b8d6..11922335 100644
--- a/Main.hs
+++ b/Main.hs
@@ -226,6 +226,8 @@ compileTerm builtins v =
     Def f es   -> (`app` es) . Hs.Var () =<< hsQName builtins f
     Con h i es -> (`app` es) . Hs.Con () =<< hsQName builtins (conName h)
     Lit (LitNat n) -> return $ Hs.Lit () $ Hs.Int () n (show n)
+    Lam v b | visible v -> hsLambda (absName b) <$> underAbstraction_ b (compileTerm builtins)
+    Lam _ b -> underAbstraction_ b (compileTerm builtins)
     t -> genericDocError =<< text "bad term:" <?> prettyTCM t
   where
     app :: Hs.Exp () -> Elims -> TCM (Hs.Exp ())
@@ -262,6 +264,14 @@ tApp :: Hs.Type () -> [Hs.Type ()] -> Hs.Type ()
 tApp (Hs.TyCon () (Hs.Special () Hs.ListCon{})) [a] = Hs.TyList () a
 tApp t vs = foldl (Hs.TyApp ()) t vs
 
+hsLambda :: String -> Hs.Exp () -> Hs.Exp ()
+hsLambda x e =
+  case e of
+    Hs.Lambda l ps b -> Hs.Lambda l (p : ps) b
+    _                -> Hs.Lambda () [p] e
+  where
+    p = Hs.PVar () $ hsName x
+
 -- FOREIGN pragmas --------------------------------------------------------
 
 type Code = (Hs.Module Hs.SrcSpanInfo, [Hs.Comment])
diff --git a/README.md b/README.md
index 662202cc..8b7b1200 100644
--- a/README.md
+++ b/README.md
@@ -4,7 +4,6 @@ Compiles a subset of Agda to readable Haskell code. See Test.agda for an example
 
 ### Future work
 
-- Compile lambdas
 - Compile if/then/else
 - Literals in patterns
 - Use some Haskell syntax ADT and a proper pretty printing library
diff --git a/Test.agda b/Test.agda
index f0be428e..9cb2b1a6 100644
--- a/Test.agda
+++ b/Test.agda
@@ -61,6 +61,16 @@ map f (x ∷ xs) = f x ∷ map f xs
 
 {-# COMPILE AGDA2HS map #-}
 
+plus3 : List Nat → List Nat
+plus3 = map (λ n → n + 3)
+
+{-# COMPILE AGDA2HS plus3 #-}
+
+doubleLambda : Nat → Nat → Nat
+doubleLambda = λ a b → a + 2 * b
+
+{-# COMPILE AGDA2HS doubleLambda #-}
+
 assoc : (a b c : Nat) → a + (b + c) ≡ (a + b) + c
 assoc zero    b c = refl
 assoc (suc a) b c rewrite assoc a b c = refl