[ treeless ] don't generate code for functions that are always inlined

agda · Nov 6, 2015 · 966c296 · 966c296
1 parent 9f30efb
commit 966c296
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 10 deletions.
diff --git a/src/full/Agda/Compiler/MAlonzo/Compiler.hs b/src/full/Agda/Compiler/MAlonzo/Compiler.hs
@@ -268,8 +268,7 @@ definition kit Defn{defName = q, defType = ty, defCompiledRep = compiled, theDef
         return ([tsig,def] ++ ccls)
 
   functionViaTreeless :: QName -> CompiledClauses -> TCM [HS.Decl]
-  functionViaTreeless q cc = do
-    treeless <- ccToTreeless q cc
+  functionViaTreeless q cc = caseMaybeM (ccToTreeless q cc) (pure []) $ \ treeless -> do
     e <- closedTerm treeless
     let (ps, b) =
           case stripTopCoerce e of

diff --git a/src/full/Agda/Compiler/ToTreeless.hs b/src/full/Agda/Compiler/ToTreeless.hs
@@ -47,8 +47,8 @@ prettyPure :: P.Pretty a => a -> TCM Doc
 prettyPure = return . P.pretty
 
 -- | Converts compiled clauses to treeless syntax.
-ccToTreeless :: QName -> CC.CompiledClauses -> TCM C.TTerm
-ccToTreeless q cc = ifM (alwaysInline q) (pure C.TErased) $ do
+ccToTreeless :: QName -> CC.CompiledClauses -> TCM (Maybe C.TTerm)
+ccToTreeless q cc = ifM (alwaysInline q) (pure Nothing) $ Just <$> do
   reportSDoc "treeless.opt" 20 $ text "-- compiling" <+> prettyTCM q
   reportSDoc "treeless.convert" 30 $ text "-- compiled clauses:" $$ nest 2 (prettyPure cc)
   body <- casetreeTop cc

diff --git a/src/full/Agda/Compiler/UHC/FromAgda.hs b/src/full/Agda/Compiler/UHC/FromAgda.hs
@@ -51,6 +51,7 @@ import Agda.Compiler.UHC.MagicTypes
 
 import Agda.Compiler.UHC.Bridge as CA
 
+import Agda.Utils.Maybe
 import Agda.Utils.Except ( MonadError (catchError) )
 
 #include "undefined.h"
@@ -117,13 +118,14 @@ translateDefn (n, defini) = do
         lift $ reportSDoc "uhc.fromagda" 15 $ text "type:" <+> (text . show) ty
         let cc = fromMaybe __IMPOSSIBLE__ $ funCompiled f
 
-        funBody <- convertGuards <$> lift (ccToTreeless n cc)
-        lift $ reportSDoc "uhc.fromagda" 30 $ text " compiled treeless fun:" <+> (text . show) funBody
-        funBody' <- runTT $ compileTerm funBody
-        lift $ reportSDoc "uhc.fromagda" 30 $ text " compiled UHC Core fun:" <+> (text . show) funBody'
+        caseMaybeM (lift $ ccToTreeless n cc) (pure []) $ \ treeless -> do
+          let funBody = convertGuards treeless
+          lift $ reportSDoc "uhc.fromagda" 30 $ text " compiled treeless fun:" <+> (text . show) funBody
+          funBody' <- runTT $ compileTerm funBody
+          lift $ reportSDoc "uhc.fromagda" 30 $ text " compiled UHC Core fun:" <+> (text . show) funBody'
 
-        addExports [crName]
-        return [mkBind1 crName funBody']
+          addExports [crName]
+          return [mkBind1 crName funBody']
 
     Constructor{} | Just n == (nameOfSharp <$> kit) -> do
         addExports [crName]