--typed: more fixes

README.md

@@ -18,9 +18,11 @@ cabal install
 ```
 
 ```
-agda2lambox [AGDAFLAGS] [--out-dir DIR] [--typed] [--no-blocks] FILE
+agda2lambox [AGDAFLAGS] [--out-dir DIR] [--typed] [--rocq] [--export-all] FILE
 ```
 
+Only the definitions reachable from those marked with `{-# COMPILE AGDA2LAMBOX f #-}` get compiled; to extract a library instead, `--export-all` compiles the whole module.
+
 Then, use the [following tool][Peregrine] to further compile the generated `.ast` files to WASM, Rust, OCaml, C, and Elm.
 
 ## Setup

agda2lambox.cabal

@@ -19,8 +19,8 @@ executable agda2lambox
   main-is:             Main.hs
   other-modules:       Agda.Utils,
                        Agda.Utils.EliminateDefaults,
+                       Agda.Utils.Erase,
                        Agda.Utils.EtaExpandConstructors,
-                       Agda.Utils.Simplify,
                        Agda.Utils.Treeless,
                        Agda.Utils.ThunkLets,
                        Agda2Lambox.Compile.Target,
@@ -41,45 +41,33 @@ executable agda2lambox
                        CodeGen.SExpr,
                        Paths_agda2lambox
   autogen-modules:     Paths_agda2lambox
-  build-depends:       base       >= 4.10  && < 4.22,
-                       Agda       >= 2.8   && < 2.9,
-                       deepseq    >= 1.4.4 && < 1.6,
-                       sexpresso  >= 1.2.5 && < 1.3,
-                       pretty-show,
-                       containers,
-                       directory,
-                       filepath,
-                       text,
-                       mtl
+  build-depends:       base       >= 4.20    && < 4.22,
+                       Agda       >= 2.8     && < 2.9,
+                       deepseq    >= 1.5     && < 1.6,
+                       sexpresso  >= 1.2.5   && < 1.3,
+                       containers >= 0.7     && < 0.8,
+                       directory  >= 1.3.8.3 && < 1.4,
+                       filepath   >= 1.5.2   && < 1.6,
+                       text       >= 2.1.1   && < 2.2,
+                       mtl        >= 2.3.1   && < 2.4
   default-language:    Haskell2010
   default-extensions:
     LambdaCase RecordWildCards PatternSynonyms TupleSections
-    ViewPatterns PatternGuards
-    ScopedTypeVariables
-    TypeFamilies TypeOperators TypeApplications
-    FunctionalDependencies TypeSynonymInstances ConstraintKinds
-    DoAndIfThenElse BlockArguments MultiWayIf
-    ImportQualifiedPost NamedFieldPuns
+    ScopedTypeVariables TypeFamilies MultiParamTypeClasses
+    BlockArguments MultiWayIf ImportQualifiedPost NamedFieldPuns
 
 test-suite agda2lambox-tests
   type:                exitcode-stdio-1.0
   hs-source-dirs:      test
   main-is:             Main.hs
-  build-depends:       base       >= 4.10  && < 4.22,
-                       tasty      >= 1.4   && < 1.6,
-                       tasty-hunit >= 0.10 && < 0.11,
-                       process    >= 1.6   && < 1.7,
-                       filepath   >= 1.4   && < 1.5,
-                       directory  >= 1.3   && < 1.4,
-                       text       >= 1.2   && < 2.2
+  build-depends:       base        >= 4.20    && < 4.22,
+                       tasty       >= 1.4.2.2 && < 1.6,
+                       tasty-hunit >= 0.10    && < 0.11,
+                       process     >= 1.6.19  && < 1.7,
+                       filepath    >= 1.5.2   && < 1.6,
+                       directory   >= 1.3.8.3 && < 1.4
   build-tool-depends:  agda2lambox:agda2lambox
   default-language:    Haskell2010
   default-extensions:
-    LambdaCase RecordWildCards PatternSynonyms TupleSections
-    ViewPatterns PatternGuards
-    ScopedTypeVariables
-    TypeFamilies TypeOperators TypeApplications
-    FunctionalDependencies TypeSynonymInstances ConstraintKinds
-    DoAndIfThenElse BlockArguments MultiWayIf
-    ImportQualifiedPost
+    TupleSections BlockArguments
 

src/Agda/Utils.hs

@@ -1,35 +1,24 @@
-{-# LANGUAGE FlexibleContexts, OverloadedStrings, BangPatterns, NamedFieldPuns #-}
+{-# LANGUAGE OverloadedStrings #-}
 
 -- | Agda utilities.
 module Agda.Utils where
 
-import Control.Applicative ( liftA2 )
-import Data.Bifunctor ( second )
 import Data.Functor ( (<&>) )
-import Data.Maybe ( isJust, isNothing, catMaybes, fromMaybe )
+import Data.Maybe ( isJust, catMaybes, fromMaybe )
 import Data.Text ( Text )
 
 import Agda.Compiler.Backend ( getUniqueCompilerPragma, PureTCM, HasConstInfo (getConstInfo) )
 import Agda.Syntax.Abstract.Name
-import Agda.Syntax.Common ( defaultArg )
+import Agda.Syntax.Common ( defaultArg, namedThing, unArg )
 import Agda.Syntax.Internal
 import Agda.TypeChecking.Monad.Base hiding ( conArity )
-import Agda.TypeChecking.Datatypes ( getConstructorInfo, ConstructorInfo(..) )
 import Agda.TypeChecking.Substitute ( raise, TelV (theCore) )
 import Agda.Syntax.Common.Pretty
 import Agda.Syntax.Treeless
 
-import Agda.Compiler.ToTreeless                 qualified as TT
-import Agda.Compiler.Treeless.Builtin           qualified as TT
-import Agda.Compiler.Treeless.Erase             qualified as TT
-import Agda.Compiler.Treeless.Simplify          qualified as TT
-import Agda.Compiler.Treeless.Identity          qualified as TT
-import Agda.Compiler.Treeless.Uncase            qualified as TT
-import Agda.Compiler.Treeless.AsPatterns        qualified as TT
 import Agda.TypeChecking.Telescope (telView, telViewUpTo)
 import Agda.TypeChecking.Substitute (TelV(theTel))
 
-import Agda.Utils.EliminateDefaults qualified as TT
 import Agda.Utils.Treeless qualified as CustomTT
 import Agda.TypeChecking.Reduce (reduceDefCopy)
 
@@ -100,8 +89,8 @@ etaExpand = \case
 -- ** toTreeless custom pipeline
 
 -- | Convert compiled clauses to treeless syntax, and return it.
-treeless :: QName -> TCM (Maybe TTerm)
-treeless = CustomTT.toTreeless EagerEvaluation
+treeless :: CustomTT.Erasure -> QName -> TCM (Maybe TTerm)
+treeless er = CustomTT.toTreeless (EagerEvaluation, er)
 
 -- * projections
 
@@ -114,6 +103,15 @@ isRecordProjection d
   | otherwise
   = Nothing
 
+-- | Whether a type-level function is compiled to a type alias:
+--   it has a single clause, whose patterns are variables.
+isTypeAlias :: Defn -> Bool
+isTypeAlias = \case
+  Function{funClauses = [cl]} ->
+    all (isVarP . namedThing . unArg) (namedClausePats cl) && isJust (clauseBody cl)
+  _ -> False
+  where isVarP = \case VarP{} -> True; _ -> False
+
 -- | Try to unfold a definition if introduced by module application.
 maybeUnfoldCopy
   :: PureTCM m

src/Agda/Utils/EliminateDefaults.hs

@@ -12,7 +12,6 @@ module Agda.Utils.EliminateDefaults where
 
 import Control.Monad
 import qualified Data.List as List
-import Control.Monad.IO.Class (liftIO)
 
 import Agda.Syntax.Treeless
 import Agda.TypeChecking.Monad