use dev version of agda for treeless pipeline

Author: flupe

agda2lambox.cabal

@@ -28,7 +28,7 @@ executable agda2lambox
                        Paths_agda2lambox
   autogen-modules:     Paths_agda2lambox
   build-depends:       base       >= 4.10  && < 4.22,
-                       Agda       >= 2.7   && <= 2.8,
+                       Agda       >= 2.7   && <= 2.9,
                        deepseq    >= 1.4.4 && < 1.6,
                        queues     >= 1.0.0 && < 1.2,
                        pretty-show,

cabal.project

@@ -0,0 +1,6 @@
+packages: .
+
+source-repository-package
+  type: git
+  location: https://github.com/agda/agda
+  tag: 5c29109f8212ef61b0091d62ef9c8bfdfa16cf36

src/Agda/Utils.hs

@@ -15,6 +15,14 @@ import Agda.TypeChecking.Substitute ( raise )
 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
+
 
 -- * Miscellaneous
 
@@ -39,6 +47,26 @@ isFunDef = \case
 
 isDataOrRecDef = liftA2 (||) isDataDef isRecDef
 
+-- ** toTreeless custom pipeline
+
+-- | Convert compiled clauses to treeless syntax, and return it.
+treeless :: QName -> TCM (Maybe TTerm)
+treeless = TT.toTreelessWith compilerPipeline (EagerEvaluation, TT.EraseUnused)
+  where
+  compilerPipeline v q =
+    TT.Sequential
+      -- NOTE (flupe): this is the default Agda treeless pipeline
+      --               with the builtin pass removed.
+      -- [ TT.compilerPass "builtin" (30 + v) "builtin translation" $ const TT.translateBuiltins
+      [ TT.FixedPoint 5 $ TT.Sequential
+        [ TT.compilerPass "simpl"  (30 + v) "simplification"     $ const TT.simplifyTTerm
+        , TT.compilerPass "erase"  (30 + v) "erasure"            $ TT.eraseTerms q
+        , TT.compilerPass "uncase" (30 + v) "uncase"             $ const TT.caseToSeq
+        , TT.compilerPass "aspat"  (30 + v) "@-pattern recovery" $ const TT.recoverAsPatterns
+        ]
+      , TT.compilerPass "id" (30 + v) "identity function detection" $ const (TT.detectIdentityFunctions q)
+      ]
+
 -- ** eta-expansion of constructors
 
 -- NOTE(flupe):