Compile lambdas

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])

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

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