don't compile copies, unfold defs

Author: flupe

README.md

@@ -39,8 +39,10 @@ make -f CoqMakefile
 ## TODO
 
 - [ ] Type aliases (See #3)
+- [ ] Improve type compilation
+    - The (re)implementation of the type translation is currently incomplete.
+      In particular, when compiling an application, we should retrieve the type of the head and compile the elims with it.
 - [ ] Check support for Agda-specific edge cases
-  - [ ] Module applications
   - [ ] Projection-like (See #6)
 - [ ] Support primitives (ints and floats)
 - [ ] Setup compilation to Wasm/Rust using Certicoq

agda2lambox.cabal

@@ -5,6 +5,8 @@ author:              Orestis Melkonian, Carlos Tomé Cortiñas, Bohdan Liesnikov
 category:            Language, Compiler
 build-type:          Simple
 synopsis:            Compiling Agda code to λ-box.
+license:             MIT
+license-file:        LICENSE
 
 extra-doc-files:    README.md
 
@@ -26,6 +28,7 @@ executable agda2lambox
                        Agda2Lambox.Compile.Function,
                        Agda2Lambox.Compile.Inductive,
                        Agda2Lambox.Compile.Type,
+                       Agda2Lambox.Compile.TypeScheme,
                        Agda2Lambox.Compile,
                        LambdaBox.Names,
                        LambdaBox.Term,

src/Agda/Utils.hs

@@ -7,7 +7,7 @@ import Control.Applicative ( liftA2 )
 import Data.Bifunctor ( second )
 import Data.Maybe ( isJust, isNothing )
 
-import Agda.Compiler.Backend ( getUniqueCompilerPragma )
+import Agda.Compiler.Backend ( getUniqueCompilerPragma, PureTCM )
 import Agda.Syntax.Abstract.Name
 import Agda.Syntax.Internal
 import Agda.TypeChecking.Monad.Base hiding ( conArity )
@@ -27,6 +27,7 @@ import Agda.TypeChecking.Telescope (telView)
 
 import Agda.Utils.EliminateDefaults qualified as TT
 import Agda.Utils.Treeless qualified as CustomTT
+import Agda.TypeChecking.Reduce (reduceDefCopy)
 
 -- * Miscellaneous
 
@@ -82,6 +83,20 @@ isRecordProjection d
   | otherwise
   = Nothing
 
+-- | Try to unfold a definition if introduced by module application.
+maybeUnfoldCopy
+  :: PureTCM m
+  => QName -- ^ Name of the definition.
+  -> Elims
+  -> (Term -> m a)
+  -- ^ Callback if the definition is indeed a copy.
+  -> (QName -> Elims -> m a)
+  -- ^ Callback if the definition isn't a copy.
+  -> m a
+maybeUnfoldCopy f es onTerm onDef =
+  reduceDefCopy f es >>= \case
+    NoReduction ()   -> onDef f es
+    YesReduction _ t -> onTerm t
 
 {-
 lookupCtx :: MonadTCEnv m => Int -> m (String, Type)

src/Agda/Utils/EliminateDefaults.hs

@@ -26,9 +26,7 @@ import Agda.Compiler.Treeless.Subst () --instance only
 
 
 eliminateCaseDefaults :: TTerm -> TCM TTerm
-eliminateCaseDefaults term = do
-  liftIO $ putStrLn "hello"
-  tr term
+eliminateCaseDefaults = tr
   where
     tr :: TTerm -> TCM TTerm
     tr = \case

src/Agda2Lambox/Compile.hs

@@ -12,16 +12,17 @@ import Agda.Syntax.Common (Arg(..))
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.TypeChecking.Monad ( liftTCM, getConstInfo )
 import Agda.TypeChecking.Pretty
-import Agda.Utils.Monad ( whenM, ifM )
+import Agda.Utils.Monad ( whenM, ifM, unlessM, ifNotM, orM )
 
-import Agda.Utils ( hasPragma, isDataOrRecDef, treeless )
+import Agda.Utils ( hasPragma, isDataOrRecDef, treeless, isArity )
 
 import Agda2Lambox.Compile.Monad
 import Agda2Lambox.Compile.Target
 import Agda2Lambox.Compile.Utils
-import Agda2Lambox.Compile.Term      ( compileTerm )
-import Agda2Lambox.Compile.Function  ( compileFunction  )
-import Agda2Lambox.Compile.Inductive ( compileInductive )
+import Agda2Lambox.Compile.Term       ( compileTerm )
+import Agda2Lambox.Compile.Function   ( compileFunction )
+import Agda2Lambox.Compile.Inductive  ( compileInductive )
+import Agda2Lambox.Compile.TypeScheme ( compileTypeScheme )
 
 import LambdaBox.Names
 import LambdaBox.Env (GlobalEnv(..), GlobalDecl(..), ConstantBody(..))
@@ -37,8 +38,12 @@ compileDefinition :: Target t -> Definition -> CompileM (Maybe (KerName, GlobalD
 compileDefinition target defn@Defn{..} = setCurrentRange defName do
   reportSDoc "agda2lambox.compile" 1 $ "Compiling definition: " <+> prettyTCM defName
 
-  -- we skip logical definitions altogether
-  ifM (liftTCM $ isLogical $ Arg defArgInfo defType) (pure Nothing) do
+  -- we skip logical definitions altogether,
+  -- and definitions introduced by module application
+  ifM
+    (orM [ pure defCopy
+         , liftTCM $ isLogical $ Arg defArgInfo defType])
+    (pure Nothing) do
 
   -- prepend kername
   fmap (qnameToKerName defName,) <$> case theDef of
@@ -50,7 +55,13 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
 
     Constructor{conData} -> Nothing <$ requireDef conData
 
-    Function{} -> compileFunction target defn
+    Function{} -> do
+      ifNotM (liftTCM $ isArity defType) (compileFunction target defn) do
+        -- it's a type scheme
+        case target of
+          ToUntyped -> pure Nothing
+          -- we only compile it with --typed
+          ToTyped   -> Just <$> compileTypeScheme defn
 
     d | isDataOrRecDef d -> compileInductive target defn
 

src/Agda2Lambox/Compile/Function.hs

@@ -20,7 +20,7 @@ import Agda.Syntax.Common ( hasQuantityω )
 import Agda.Utils.Monad (guardWithError, whenM)
 import Agda.Utils.Lens ( (^.) )
 
-import Agda.Utils ( treeless, pp, isRecordProjection )
+import Agda.Utils ( treeless, pp, isRecordProjection, isArity )
 import Agda2Lambox.Compile.Target
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad

src/Agda2Lambox/Compile/Monad.hs

@@ -18,7 +18,7 @@ import Queue.Ephemeral ( EphemeralQueue(..) )
 import Queue.Ephemeral qualified as Queue
 
 import Agda.Syntax.Abstract (QName)
-import Agda.Compiler.Backend (getConstInfo)
+import Agda.Compiler.Backend (getConstInfo, PureTCM, HasConstInfo, HasBuiltins)
 import Agda.TypeChecking.Monad (MonadDebug, MonadTrace, MonadAddContext)
 import Agda.TypeChecking.Monad.Debug (MonadDebug, reportSDoc)
 import Agda.TypeChecking.Monad.Base hiding (initState)
@@ -51,7 +51,7 @@ newtype CompileM a = Compile (StateT CompileState TCM a)
   deriving newtype (Functor, Applicative, Monad)
   deriving newtype (MonadIO, MonadFail, MonadDebug, ReadTCState, MonadTrace)
   deriving newtype (MonadError TCErr, MonadTCEnv, MonadTCState, HasOptions, MonadTCM)
-  deriving newtype (MonadAddContext, MonadReduce)
+  deriving newtype (MonadAddContext, MonadReduce, HasConstInfo, HasBuiltins, PureTCM)
 
 -- | Require a definition to be compiled.
 requireDef :: QName -> CompileM ()

src/Agda2Lambox/Compile/Term.hs

@@ -170,7 +170,7 @@ compileLitPattern = \case
 
 compileCaseType :: CaseType -> C LBox.Inductive
 compileCaseType = \case
-  CTData qn -> do 
+  CTData qn -> do
     lift $ requireDef qn
     liftTCM $ toInductive qn
   CTNat -> do

src/Agda2Lambox/Compile/Type.hs

@@ -25,7 +25,7 @@ import qualified LambdaBox as LBox
 import Agda2Lambox.Compile.Utils ( qnameToKName, isLogical )
 import Agda2Lambox.Compile.Monad
 import Agda.Compiler.Backend (HasConstInfo(getConstInfo), Definition(Defn), AddContext (addContext))
-import Agda.Utils (isDataOrRecDef, getInductiveParams, isArity)
+import Agda.Utils (isDataOrRecDef, getInductiveParams, isArity, maybeUnfoldCopy)
 import Agda.TypeChecking.Substitute (absBody, TelV (theCore))
 import Agda.TypeChecking.Telescope (telView)
 
@@ -133,7 +133,7 @@ compileTypeTerm = \case
       TypeVar n -> pure ([], LBox.TVar n)
       Other     -> pure ([], LBox.TAny  )
 
-  Def q es -> do
+  Def q es -> maybeUnfoldCopy q es compileTypeTerm \q es -> do
     Defn{theDef = def, defType, defArgInfo, defName} <- liftTCM $ getConstInfo q
 
     isLogicalDef <- liftTCM $ isLogical $ Arg defArgInfo defType

src/Agda2Lambox/Compile/TypeScheme.hs

@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds #-}
+module Agda2Lambox.Compile.TypeScheme where
+
+import Control.Monad.IO.Class ( liftIO )
+
+import Agda.Compiler.Backend
+import Agda.TypeChecking.Telescope (telView)
+import Agda.TypeChecking.Substitute (TelV(TelV))
+
+import Agda2Lambox.Compile.Monad
+import Agda2Lambox.Compile.Target
+import Agda2Lambox.Compile.Utils
+import Agda2Lambox.Compile.Type
+import LambdaBox.Env
+
+compileTypeScheme :: Definition -> CompileM (GlobalDecl Typed)
+compileTypeScheme Defn{..} = do
+  TelV tyargs _ <- telView defType
+  liftIO $ putStrLn "compiling type scheme"
+  pure $ TypeAliasDecl $ Nothing