properly discard with-generated in mutuals

Author: flupe

README.md

@@ -42,7 +42,7 @@ cabal run agda2lambox -- --out-dir build -itest test/Nat.agda
 - [ ] "Support" modules
 - [ ] Check support for Agda-specific edge cases
   - [x] Pattern-matching lambdas
-  - [ ] With-generated lambdas
+  - [x] With-generated lambdas
   - [ ] Module applications
   - [ ] Projection-like
 - [ ] Support literals (ints and floats)

src/Agda2Lambox/Compile/Function.hs

@@ -4,7 +4,8 @@ module Agda2Lambox.Compile.Function
   ( compileFunction
   ) where
 
-import Control.Monad ( forM, when )
+import Control.Monad ( forM, when, filterM, unless )
+import Control.Monad.IO.Class ( liftIO )
 import Data.List ( elemIndex )
 import Data.Maybe ( isNothing, fromMaybe )
 
@@ -15,7 +16,7 @@ import Agda.Compiler.Backend ( getConstInfo, funInline )
 import Agda.Syntax.Treeless ( EvaluationStrategy(EagerEvaluation) )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.Syntax.Common ( hasQuantityω )
-import Agda.Utils.Monad (guardWithError)
+import Agda.Utils.Monad (guardWithError, whenM)
 import Agda.Utils.Lens ( (^.) )
 
 import Agda.Utils ( etaExpandCtor )
@@ -32,8 +33,11 @@ isFunction _ = False
 
 -- | Convert a function body to a Lambdabox term.
 compileFunctionBody :: [QName] -> Definition -> TCM LBox.Term
-compileFunctionBody ms Defn{defName} = do
-    Just t <-toTreeless EagerEvaluation defName
+compileFunctionBody ms Defn{defName, theDef} = do
+    liftIO $ putStrLn $ prettyShow defName
+    let Function{funWith} = theDef
+    liftIO $ print funWith
+    Just t <- toTreeless EagerEvaluation defName
     compileTerm ms =<< etaExpandCtor t
 
 
@@ -42,33 +46,39 @@ shouldCompileFunction :: Definition -> Bool
 shouldCompileFunction def@Defn{theDef} | Function{..} <- theDef
   = not (theDef ^. funInline) -- not inlined (from module application)
     && isNothing funExtLam    -- not a pattern-lambda-generated function (inlined by the treeless translation)
-    && isNothing funWith      -- not a with-generated function             NOTE(flupe): ?
+    && isNothing funWith      -- not a with-generated function           (inlined by the treeless translation)
     && hasQuantityω def       -- non-erased
 
 
 -- | Convert a function definition to a λ□ declaration.
 compileFunction :: Definition -> TCM (Maybe LBox.GlobalDecl)
 compileFunction defn | not (shouldCompileFunction defn) = return Nothing
-compileFunction defn@Defn{defName, theDef} = do
-    let Function{funMutual = Just ms} = theDef
+compileFunction defn@Defn{theDef} = do
+  let Function{funMutual = Just mutuals} = theDef
 
-    -- if the function is at most recursive with itself, just compile body
-    if null ms then
-      Just. LBox.ConstantDecl . Just <$> compileFunctionBody [] defn
+  defs <- mapM getConstInfo mutuals
 
-    -- otherwise, take fixpoint
-    else do
-      mdefs :: [Definition] <- mapM getConstInfo ms
+  unless (all isFunction defs) $
+    fail "only mutually defined functions are supported."
 
-      when (any (not . isFunction) mdefs) $ fail "only mutually defined functions are supported."
+  -- the mutual functions that we actually compile
+  -- (so no with-generated functions, etc...)
+  let mdefs = filter shouldCompileFunction defs
 
-      let k = fromMaybe 0 $ elemIndex defName ms
+  -- if the function is not recursive, just compile the body
+  if null mdefs then Just. LBox.ConstantDecl . Just <$> compileFunctionBody [] defn
 
-      Just . LBox.ConstantDecl . Just . flip LBox.LFix k <$>
-        forM mdefs \def@Defn{defName} -> do
-          body <- compileFunctionBody ms def
-          return LBox.Def
-            { dName = LBox.Named $ prettyShow defName
-            , dBody = body
-            , dArgs = 0
-            }
+  -- otherwise, take fixpoint
+  else do
+
+    let mnames = map defName mdefs
+    let k = fromMaybe 0 $ elemIndex (defName defn) mnames
+
+    Just . LBox.ConstantDecl . Just . flip LBox.LFix k <$>
+      forM mdefs \def@Defn{defName} -> do
+        body <- compileFunctionBody mnames def
+        return LBox.Def
+          { dName = LBox.Named $ prettyShow defName
+          , dBody = body
+          , dArgs = 0
+          }

test/With.agda

@@ -0,0 +1,21 @@
+data Bool : Set where
+  false true : Bool
+
+infixr 7 _::_
+
+data List (A : Set) : Set where
+  []   : List A
+  _::_ : A → List A → List A
+
+filter : {A : Set} → (A → Bool) → List A → List A
+filter f [] = []
+filter f (x :: xs) with f x
+... | true  = x :: filter f xs
+... | false = filter f xs
+
+xs : List Bool
+xs = false :: true :: false :: []
+
+ys : List Bool
+ys = filter (λ b → b) xs
+{-# COMPILE AGDA2LAMBOX ys #-}