Where clauses fix

src/Agda/Utils/Treeless.hs

@@ -17,6 +17,7 @@ module Agda.Utils.Treeless
   , compilerPipeline
   , CCConfig
   , CCSubst(..)
+  , alwaysInline
   ) where
 
 import Prelude hiding ((!!))
@@ -189,13 +190,13 @@ compilerPipeline v q =
     [ FixedPoint 5 $ Sequential
       -- [ compilerPass "simpl"  (30 + v) "simplification"     $ const simplifyTTerm
       [ compilerPass "erase"  (30 + v) "erasure"            $ eraseTerms q
-      , compilerPass "uncase" (30 + v) "uncase"             $ const caseToSeq
+      -- , compilerPass "uncase" (30 + v) "uncase"             $ const caseToSeq
 
 
       --, compilerPass "aspat"  (30 + v) "@-pattern recovery" $ const recoverAsPatterns
       ]
 
-    , compilerPass "id" (30 + v) "identity function detection" $ const (detectIdentityFunctions q)
+    -- , compilerPass "id" (30 + v) "identity function detection" $ const (detectIdentityFunctions q)
 
     -- NOTE(flupe): those are custom transformations required by the backend
     , compilerPass "ctors"    (30 + v) "eta-expand constructors" $ const etaExpandConstructors

src/Agda2Lambox/Compile.hs

@@ -39,10 +39,10 @@ import LambdaBox.Term (Term(LBox))
 compile :: Target t -> [QName] -> CompileM (GlobalEnv t)
 compile t qs = do
   items <- compileLoop (compileDefinition t) qs
-  pure $ GlobalEnv $ map itemToEntry items ++ [(emptyName, emptyDecl t)]
-  where
-    itemToEntry :: CompiledItem (GlobalDecl t) -> (KerName, GlobalDecl t)
-    itemToEntry CompiledItem{..} = (qnameToKName itemName, itemValue)
+  liftTCM $ GlobalEnv . (++ [(emptyName, emptyDecl t)]) <$> mapM itemToEntry items
+    where
+      itemToEntry :: CompiledItem (GlobalDecl t) -> TCM (KerName, GlobalDecl t)
+      itemToEntry CompiledItem{..} = (,itemValue) <$> qnameToKName itemName
 
 
 compileDefinition :: Target t -> Definition -> CompileM (Maybe (GlobalDecl t))
@@ -52,12 +52,15 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
   -- retrieve compile annotation written in COMPILE pragma
   annotation <- liftTCM $ getPragmaInfo defName
 
-  reportSDoc "agda2lambox.compile" 1 $
+  reportSDoc "agda2lambox.compile" 10 $
     "Definition is annotated as such:" <+> prettyTCM annotation
 
   -- we skip definitions introduced by module application
+  if defCopy then do
+    reportSDoc "agda2lambox.compile" 10 "The definition is a copy from module application: skipping"
+    pure Nothing
 
-  if defCopy then pure Nothing else do
+  else do
 
   -- TODO: check that we indeed don't compile defs marked with @0
   --       especially record projections for erased fields
@@ -78,6 +81,7 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
 
     Function{} -> do
       ifNotM (liftTCM $ isArity defType) (compileFunction target defn) do
+        reportSDoc "agda2lambox.compile" 10 "Function is a type scheme"
         -- it's a type scheme
         case target of
           ToUntyped -> pure Nothing

src/Agda2Lambox/Compile/Function.hs

@@ -7,7 +7,7 @@ module Agda2Lambox.Compile.Function
 import Control.Monad ( forM, when, filterM, unless )
 import Control.Monad.IO.Class ( liftIO )
 import Data.List ( elemIndex )
-import Data.Maybe ( isNothing, fromMaybe )
+import Data.Maybe ( fromMaybe, isJust )
 
 import Data.Foldable (toList)
 import Agda.Syntax.Abstract.Name ( QName, qnameModule )
@@ -16,9 +16,10 @@ import Agda.TypeChecking.Pretty
 import Agda.Compiler.Backend ( getConstInfo, funInline, reportSDoc )
 import Agda.Syntax.Internal (domName)
 import Agda.Syntax.Common.Pretty ( prettyShow )
-import Agda.Syntax.Common ( hasQuantityω )
+import Agda.Syntax.Common ( hasQuantity0 )
 import Agda.Utils.Monad (guardWithError, whenM)
 import Agda.Utils.Lens ( (^.) )
+import Agda.Utils.Treeless ( alwaysInline )
 
 import Agda.Utils ( treeless, pp, isRecordProjection, isArity )
 import Agda2Lambox.Compile.Target
@@ -50,68 +51,79 @@ compileFunctionBody ms Defn{defName, theDef} = do
   compileTerm ms t
 
 
--- | Whether to compile a function definition to λ□.
-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           (inlined by the treeless translation)
-    && hasQuantityω def       -- non-erased
+-- | Whether to skip a function definition to λ□.
+shouldSkipFunction :: Definition -> TCM Bool
+shouldSkipFunction def@Defn{theDef} | Function{..} <- theDef
+  = do
+      -- NOTE(flupe): currently we use this function from Treeless
+      --              but it is NOT exported, so once we move back to using Agda's default pipeline
+      --              we will have to copy the logic here
+      inlined <- alwaysInline (defName def)
+      return $ theDef ^. funInline -- inlined (from module application)
+                 || hasQuantity0 def -- erased
+                 || inlined
+shouldSkipFunction _ = pure False
 
 -- | Convert a function definition to a λ□ declaration.
 compileFunction :: Target t -> Definition -> CompileM (Maybe (LBox.GlobalDecl t))
-compileFunction t defn | not (shouldCompileFunction defn) = pure Nothing
-compileFunction (t :: Target t) defn@Defn{defType} = do
-  let fundef@Function{funMutual = Just mutuals} = theDef defn
-
-  reportSDoc "agda2lambox.compile.function" 5 $
-    "Function mutuals:" <+> prettyTCM mutuals
-
-  defs <- liftTCM $ mapM getConstInfo mutuals
-
-  unless (all isFunction defs) $
-    genericError "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 mnames = map defName mdefs
-
-  -- (conditionally) compile type of function
-  typ <- whenTyped t $ case isRecordProjection fundef of
-    Nothing -> compileTopLevelType defType
-
-    -- if it is a (real) projection, drop the parameters from the type
-    Just (recName, _) -> do
-      Record{recPars} <- fmap theDef $ liftTCM $ getConstInfo recName
-      projTel <- telViewUpTo recPars defType
-      projType <- theCore <$> telViewUpTo recPars defType
-      let names  = map domName $ toList $ theTel projTel
-          pnames = map (maybe LBox.Anon (LBox.Named . sanitize . prettyShow)) names
-      (pnames,) <$> compileType recPars projType
-
-    -- TODO(flupe): ^ take care of projection-like functions
-    --                they should be eta-expanded somehow,
-    --                OR treated like projections
-
-  let builder :: LBox.Term -> Maybe (LBox.GlobalDecl t)
-      builder = Just . ConstantDecl . ConstantBody typ . Just
-
-  -- if the function is not recursive, just compile the body
-  if null mdefs then builder <$> compileFunctionBody [] defn
-
-  -- otherwise, take fixpoint
+compileFunction (t :: Target t) defn = do
+  inlined <- liftTCM $ alwaysInline (defName defn)
+  if inlined then do
+    reportSDoc "agda2lambox.compile.function" 5
+      "Function skipped, because either inlined, erased or with-generated."
+    pure Nothing
   else do
-    let k = fromMaybe 0 $ elemIndex (defName defn) mnames
-
-    builder . flip LBox.LFix k <$>
-      forM mdefs \def@Defn{defName} -> do
-        body <- compileFunctionBody mnames def >>= \case
-          l@LBox.LLambda{} -> pure l
-          LBox.LBox        -> pure $ LBox.LLambda LBox.Anon LBox.LBox
-          _                -> genericError "Fixpoint body must be Lambda."
-        return LBox.Def
-          { dName = qnameToName defName
-          , dBody = body
-          , dArgs = 0
-          }
+    let fundef@Function{funMutual = Just mutuals} = theDef defn
+
+    -- all defs in the mutual block
+    defs <- liftTCM $ filterM (fmap not . shouldSkipFunction) =<< mapM getConstInfo mutuals
+
+    reportSDoc "agda2lambox.compile.function" 5 $
+      "Function mutuals:" <+> prettyTCM (map defName defs)
+
+    unless (all isFunction defs) $
+      genericError "Only mutually defined functions are supported."
+
+    -- the mutual functions that we actually compile
+    -- (so no with-generated functions, etc...)
+    let mnames = map defName defs
+
+    -- (conditionally) compile type of function
+    typ <- whenTyped t $ case isRecordProjection fundef of
+      Nothing -> compileTopLevelType $ defType defn
+
+      -- if it is a (real) projection, drop the parameters from the type
+      Just (recName, _) -> do
+        Record{recPars} <- fmap theDef $ liftTCM $ getConstInfo recName
+        projTel <- telViewUpTo recPars $ defType defn
+        projType <- theCore <$> (telViewUpTo recPars $ defType defn)
+        let names  = map domName $ toList $ theTel projTel
+            pnames = map (maybe LBox.Anon (LBox.Named . sanitize . prettyShow)) names
+        (pnames,) <$> compileType recPars projType
+
+      -- TODO(flupe): ^ take care of projection-like functions
+      --                they should be eta-expanded somehow,
+      --                OR treated like projections
+
+    let builder :: LBox.Term -> Maybe (LBox.GlobalDecl t)
+        builder = Just . ConstantDecl . ConstantBody typ . Just
+
+    -- if the function is not recursive, just compile the body
+    if null defs then builder <$> compileFunctionBody [] defn
+
+    -- otherwise, take fixpoint
+    else do
+      let k = fromMaybe 0 $ elemIndex (defName defn) mnames
+
+      builder . flip LBox.LFix k <$>
+        forM defs \def@Defn{defName} -> do
+          body <- compileFunctionBody mnames def >>= \case
+            l@LBox.LLambda{} -> pure l
+            LBox.LBox        -> pure $ LBox.LLambda LBox.Anon LBox.LBox
+            _                -> genericError "Fixpoint body must be Lambda."
+          name <- liftTCM $ qnameToName defName
+          return LBox.Def
+            { dName = name
+            , dBody = body
+            , dArgs = 0
+            }

src/Agda2Lambox/Compile/Inductive.hs

@@ -166,14 +166,18 @@ actuallyConvertInductive t defn = do
             "Constructor telescope:" <+> prettyTCM conTel
           compileArgs indPars conTel
 
+        ident <- liftTCM $ qnameToIdent cname
+
         pure LBox.Constructor
-          { cstrName  = qnameToIdent cname
+          { cstrName  = ident
           , cstrArgs  = arity
           , cstrTypes = conTypeInfo
           }
 
+    ident <- liftTCM $ qnameToIdent indName
+
     pure LBox.OneInductive
-      { indName          = qnameToIdent indName
+      { indName          = ident
       , indPropositional = False        -- TODO(flupe)
       , indKElim         = LBox.IntoAny -- TODO(flupe)
       , indCtors         = ctors

src/Agda2Lambox/Compile/Term.hs

@@ -104,7 +104,7 @@ compileTermC = \case
     TermEnv{mutuals, boundVars} <- ask
     case qn `elemIndex` mutuals of
       Nothing -> do lift $ requireDef qn
-                    pure $ LConst $ qnameToKName qn
+                    liftTCM $ LConst <$> qnameToKName qn
       Just i  -> pure $ LRel  $ i + boundVars
 
   TCon q -> do

src/Agda2Lambox/Compile/Type.hs

@@ -199,7 +199,7 @@ compileTypeTerm t = do
       else do
         q <- liftTCM $ canonicalName q
         lift $ requireDef q
-        let ts = qnameToKName q
+        ts <- liftTCM $ qnameToKName q
         let args = mapMaybe isApplyElim es
         ([],) . foldl' LBox.TApp (LBox.TConst ts)
           <$> compileElims defType args

src/Agda2Lambox/Compile/Utils.hs

@@ -14,7 +14,10 @@ module Agda2Lambox.Compile.Utils
   , sanitize
   ) where
 
+import Control.Monad ( (<=<) )
 import Control.Monad.State
+import Data.Maybe ( isJust )
+import Data.Functor ( (<&>) )
 import Control.Monad.IO.Class ( liftIO )
 import Numeric ( showHex )
 import Data.Char
@@ -26,14 +29,16 @@ import Agda.Compiler.Backend
 import Agda.Syntax.Internal
 import Agda.Syntax.Abstract.Name
 import Agda.Syntax.Common.Pretty ( prettyShow, Doc )
-import Agda.Syntax.Common ( usableModality, Arg(..) )
+import Agda.Syntax.Common ( usableModality, Arg(..), NameId(..) )
 import Agda.TypeChecking.Datatypes ( getConstructors, getConstructorData )
 import Agda.TypeChecking.Level ( isLevelType )
 import Agda.TypeChecking.Monad.SizedTypes ( isSizeType )
 import Agda.TypeChecking.Monad.Base ( TCM )
 import Agda.TypeChecking.Substitute (TelV(TelV))
 import Agda.TypeChecking.Telescope (telView)
-import Agda.Utils.Monad (orM)
+import Agda.Utils.Monad ( andM, orM, ifM )
+import Agda.Utils.Treeless ( alwaysInline )
+import Agda.Utils.Functor ( (<.>) )
 
 import Agda2Lambox.Compile.Monad
 import LambdaBox qualified as LBox
@@ -44,20 +49,37 @@ modNameToModPath =
   LBox.MPFile . map (sanitize . prettyShow) . mnameToList
 
 -- | Convert and Agda definition name to a λ□ kernel name.
-qnameToKName :: QName -> LBox.KerName
+qnameToKName :: QName -> TCM LBox.KerName
 qnameToKName qn =
-  LBox.KerName
-    (modNameToModPath $ qnameModule qn)
-    (qnameToIdent qn)
+  LBox.KerName (modNameToModPath $ qnameModule qn)
+    <$> qnameToIdent qn
 
 domToName :: Dom' a b -> LBox.Name
 domToName = maybe LBox.Anon (LBox.Named . sanitize . prettyShow) . domName
 
-qnameToIdent :: QName -> LBox.Ident
-qnameToIdent = sanitize . prettyShow . qnameName
+ -- | Whether a definition has a generated name and still must be compiled
+ --   i.e not systematically inline
+isKeptGenerated :: QName -> TCM Bool
+isKeptGenerated q = andM [ isGenerated,  not <$> alwaysInline q ]
+  where
+    isGenerated :: TCM Bool
+    isGenerated = theDef <$> getConstInfo q <&> \case
+      Function{..} -> isJust funExtLam || isJust funWith
+      _            -> False
+
+qnameToIdent :: QName -> TCM LBox.Ident
+qnameToIdent q = do
+  keptGen <- isKeptGenerated q
+  -- NOTE(flupe): we only add nameId to generated names which are not inlined
+  let suffix = if keptGen then "_" ++ show idx 
+                          else ""
+  pure $ sanitize $ prettyShow name ++ suffix
+  where
+    name         = qnameName q
+    NameId idx _ = nameId name
 
-qnameToName :: QName -> LBox.Name
-qnameToName = LBox.Named . qnameToIdent
+qnameToName :: QName -> TCM LBox.Name
+qnameToName = LBox.Named <.> qnameToIdent
 
 dataOrRecDefMutuals :: Definition -> TCM [QName]
 dataOrRecDefMutuals d = do
@@ -75,7 +97,7 @@ toInductive q = do
   names <- dataOrRecMutuals q
   let repr = fromMaybe q $ listToMaybe names
   let idx  = fromMaybe 0 $ elemIndex q names
-  pure $ LBox.Inductive (qnameToKName repr) idx
+  LBox.Inductive <$> qnameToKName repr <*> pure idx
 
 
 -- | Compile a constructor application to λ□.

src/Main.hs

@@ -3,7 +3,7 @@
 -- | The agda2lambox Agda backend
 module Main (main) where
 
-import Control.Monad ( unless, filterM, when )
+import Control.Monad ( unless, filterM, when, mapM )
 import Control.Monad.IO.Class ( liftIO )
 import Control.DeepSeq ( NFData(rnf) )
 import Data.Function ( (&) )
@@ -153,4 +153,4 @@ writeModule Options{..} menv IsMain m defs = do
     getMain ToUntyped qs =
       case NEL.nonEmpty qs of
         Nothing -> genericError "No main program specified. Please use a COMPILE pragma."
-        Just ms -> pure $ SomeU (NEL.map qnameToKName ms)
+        Just ms -> liftTCM $ SomeU <$> mapM qnameToKName ms